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
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
