### Re: [ProofPower] Z Schemas - Help with Initialization and Precondition calculus

On Tuesday 24 March 2009 05:07:09 Artur Oliveira Gomes wrote: I'm having hard times to achieve some proofs of preciondition and initialization using ProofPower. The file attached contains 3 examples that I still can not prove. If anyone could help me out with those proofs, I will be thankful. These are all existential conjectures. ProofPower is sometimes quite dumb about these things (sometimes quite smart), it only really knows about the kinds of existential proofs which are necessary for proving consistency of things like recursive definitions (and that stuff only really works for HOL its not so good in Z). So usually you will have to come up with a witness for the existential goal yourself. In the case of an existential with a schema as the signature the witness will usually be a binding display. So for each of your proofs you must come up with the binding display of a witness for your conjecture, i.e. a binding which satisfies the body of the existential, and then offer it up using exists-tac. Then you have to prove that your witness does satisfy the predicate. (I didn't check whether you are trying to prove the right thing!) regards, Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Z Schemas - Help with Initialization and Precondition calculus

Roger, In the case of an existential with a schema as the signature the witness will usually be a binding display. So for each of your proofs you must come up with the binding display of a witness for your conjecture, i.e. a binding which satisfies the body of the existential, and then offer it up using exists-tac. Then you have to prove that your witness does satisfy the predicate. That is exactly what I am doing. Except for those examples, I can do it fine. I just did not included in the file few steps until the exist-tac. The problem is: only for those cases, what I choose as witness does not satisfy the predicate. I sent the file in order to see if someone could find the right witness for each of the three goals. ;-) Regards, -- Artur Oliveira Gomes ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Z Schemas - Help with Initialization and Precondition calculus

Artur, On Tuesday 24 March 2009 10:35:51 Artur Oliveira Gomes wrote: The problem is: only for those cases, what I choose as witness does not satisfy the predicate. Well, any sequence of length 1 (or zero?) does for the first case. Proof attached. If you still can't crack the other two send me your best attempt. Roger (*01*) =SML open_theory z_library; delete_theory temp; new_theory temp; new_parent z_reals; =TEX (*defs*) �Z � TYPES ::= AA | BB | CC � �ZAX � TYPE : � TYPES ��� � TYPE = {AA, BB} � �Z �EXAMPLE � {a:TYPE; b:� � (a,b)} � �ZAX � Example : EXAMPLE � �Z �S_EXAMPLES � {s:seq EXAMPLE | � � i,j: dom s � | i � j � � m1,m2: ran s � | m1 = s(i) � m2 = s(j) � � m1.2 � m2.2} � �Z � S_Example � �Example� � �ZAX � S_Example2 : seq EXAMPLE ��� � dom S_Example2 = {1} � (*State*) � AState ��� � a, b, c: S_EXAMPLES ��� (*init of State*) � InitAState ��� � AState' ��� �Z � IA_State � (a' � S_Example2, b' � S_Example2, c' � S_Example2) � (*02*) � Sch ��� � a:�;b,c:� ��� � Sch1 ��� � Sch ��� � a=true ��� � Sch2 ��� � Sch ��� � b=10 ��� �Z � NSch � Sch1 � Sch2 � (*Schema*) � BState ��� � var: NSch ��� (*init of State*) � InitBState ��� � BState' �� � var' � Sch2 ��� � CState ��� � counter: � ��� (*init of State*) � InitCState ��� � CState' ��� �Z � State � AState � BState � CState � �Z � St � [StComp : State] � (*03*) � Op1 �� � �St ��� � � State; State' | � StComp = �State � StComp' = �State' � � counter' = counter + 1 � � �(State \�s (counter))' � = �(State \�s (counter)) (*Initialization Proofs Is it this correct? If so, how can its initialization be proved?*) push_pc z_library_ext; (*01*) set_goal ([], �� AState' � InitAState�); a (z_�_tac �IA_State�); a (rewrite_tac [z_get_spec �InitAState�, z_get_spec �AState�, z_get_spec �S_EXAMPLES�, z_get_spec �IA_State�, z_get_spec �S_Example2�, z_get_spec �Example�]); a (REPEAT z_strip_tac THEN POP_ASM_T ante_tac THEN asm_rewrite_tac[]); (...) (*02*) set_goal ([], �� BState' � InitBState�); (...) (*Precondition Proofs *) (*03*) set_goal ([], �� �St � pre Op1�); (...) ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Z Schemas - Help with Initialization and Precondition calculus

Roger, When I execute: a (REPEAT z_strip_tac THEN POP_ASM_T ante_tac THEN asm_rewrite_tac[]); ProofPower returns the following message: :# :# Exception- Fail * the assumption list is empty [POP_ASM_T.9302] * raised Exception+ Fail * the assumption list is empty [POP_ASM_T.9302] * raised Is everything fine? Artur 2009/3/24 Roger Bishop Jones r...@rbjones.com Artur, On Tuesday 24 March 2009 10:35:51 Artur Oliveira Gomes wrote: The problem is: only for those cases, what I choose as witness does not satisfy the predicate. Well, any sequence of length 1 (or zero?) does for the first case. Proof attached. If you still can't crack the other two send me your best attempt. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com -- Artur Oliveira Gomes ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com