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

Reply via email to