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

## Advertising

Hi there,It doesn't look like parentheses are the problem. It might be aproblem with types or something else that is not visible in thepretty-printed Z that is stopping the LHS of he assumption matchingthe conclusion of the goal. Can you provide an example withdefinitions 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))%>% rewrite_thm_tac); (* *** 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 ... *) Regards, Rob. _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com