On 18 May 2009, at 21:28, Artur Oliveira Gomes wrote:

Hi there,

It doesn't look like parentheses are the problem. It might be a problem with types or something else that is not visible in the pretty-printed Z that is stopping the LHS of he assumption matching the conclusion of the goal. Can you provide an example with definitions of SA etc. that can be run?

Yes, an example is attached here as follows.

Thanks in advance,

I see the problem now. Remember that the quantifier symbols in Z are used for two different language constructs: predicates and schemas. Because you used = rather than %equiv% in your lemma, the lemma proves an equation between schemas and the left-hand side doesn't match the conclusion of the goal (which is a predicate). The easiest thing to do is to change = to %equiv%, which makes the lemma into a logical equivalence between predicates rather than an equation between schemas. This makes the proof of the lemma a bit simpler too, although it does require a little trick to avoid the lemma causing a case split:

        set_goal ([],%SZT%%exists% (AState %and% BState %and% CState)'
             %spot% InitAState %and% InitBState %and% InitCState%>%);

(* lemma says conclusion %equiv% conclusion': use LEMMA_T ... rewrite_thm_tac to avoid case split *)

        a (LEMMA_T %SZT%(%exists% (AState %and% BState %and% CState)'
             %spot% InitAState %and% InitBState %and% InitCState)
                %equiv% ((%exists% AState'%spot% InitAState)
                        %and% (%exists% BState'%spot% InitBState)
                        %and% (%exists% CState'%spot% InitCState))%>% 
(* *** Goal "1" *** *)
a (REPEAT strip_tac);
(* *** Goal "1.1" *** *)
a(z_%exists%_tac %SZT%%theta%(AState')%>% THEN asm_rewrite_tac[]);
(* *** Goal "1.2" *** *)
a(z_%exists%_tac %SZT%%theta%(BState')%>% THEN asm_rewrite_tac[]);
(* *** Goal "1.3" *** *)
a(z_%exists%_tac %SZT%%theta%(CState')%>% THEN asm_rewrite_tac[]);
(* *** Goal "1.4" *** *)
a(z_%exists%_tac %SZT%%theta%((AState %and% BState %and% CState)')%>% THEN asm_rewrite_tac[]);

(* Lemma now proved and have new rewritten conclusion to prove ... *)



Proofpower mailing list

Reply via email to