My first response to Artur Gomes was a bit rushed
and probably didn't help much, so I had another
look.
I fiddled around with his script to confirm that
the precondition of Op is SS, and then did
a direct proof.
The amended script is attached.
I don't have a systematic method to offer, not having
done this kind of work with Z myself, so the proof
is ad hoc.
It is, of course, crucially important, before trying to
prove an existential goal using a witness, to be sure that
you have a witness which satisfies the predicate in the
existential (explicit and implicit).
Roger Jones
open_theory "z_library";
force_delete_theory "teste" handle Fail _ => ();
new_theory "test";
new_parent "z_reals";
open_theory "test";
set_pc "z_library_ext";
(*State and components*)
� StA �����������
� a1:�
�������
� a1 � real 20 ..�R real 30
���������������
� StB �����������
� b1:�
�������
� b1 � real 30 ..�R real 40
���������������
�Z
� St � StA � StB
�
�Z
� SS � [SScomp:St]
�
(*
Operations
*)
(*Using SS state*)
� Op �����������
� �SS;
� out_a1! : �
�������
� � St; St' |
� SScomp = �St � SScomp' = �St' �
� out_a1!=a1 �
� �St = �St'
���������������
(*Using St state*)
� Op1 �����������
� �St;
� out_a1! : �
�������
� out_a1!=a1 �
� �St = �St'
���������������
(*pre-condition*)
(*For Op1*)
set_goal ([], �pre Op1 � true�);
a (rewrite_tac[z_get_spec�pre Op1�]);
a (z_�_tac �(a1'� a1,b1'� b1,
out_a1! � a1)�
THEN rewrite_tac[]);
a (rewrite_tac[z_get_spec�Op1�]);
a (rewrite_tac[z_get_spec�St�]);
a (rewrite_tac[z_get_spec�StA�]);
a (rewrite_tac[z_get_spec�StB�]);
a (rewrite_tac[z_get_spec���]);
(*For Op*)
set_goal ([], �pre Op � true�);
a (rewrite_tac[z_get_spec�pre Op�]);
a (z_�_tac �(SScomp'� SScomp,
out_a1! � SScomp.a1)�
THEN rewrite_tac[]);
a (rewrite_tac[z_get_spec�Op�]);
a (rewrite_tac[z_get_spec���]);
a (rewrite_tac[z_get_spec�SS�]);
a (rewrite_tac[z_get_spec�St�]);
a (rewrite_tac[z_get_spec�StA�]);
a (rewrite_tac[z_get_spec�StB�]);
a (rewrite_tac[z_get_spec���]);
a (REPEAT strip_tac);
set_labelled_goal "3";
a (z_�_tac �(a1 � SScomp.a1, b1 � SScomp.b1, a1' � SScomp.a1, b1' �
SScomp.b1)�
THEN rewrite_tac[]);
set_goal ([], �(pre Op) = SS�);
a (rewrite_tac[z_get_spec�Op�] THEN REPEAT z_�_tac THEN rewrite_tac[]);
a (REPEAT strip_tac THEN asm_rewrite_tac[]);
a (z_�_tac �(SScomp' � (a1 � x1, b1 � x2), out_a1! � x1)�
THEN asm_rewrite_tac[]);
a (POP_ASM_T ante_tac);
a (rewrite_tac (map get_spec [�SS�, �St�, �StA�, �StB�]));
a (strip_tac THEN asm_rewrite_tac[]);
a (z_�_tac �(a1 � x1, b1 � x2, a1' � x1, b1' � x2)�
THEN asm_rewrite_tac[]);
z_type_of �SScomp'�;
(*Are these all the preconditions, including the existential quantifier? Is it
part of the preconditions of the operation?*)_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
