Re: [isabelle] A Newbie question about forward-proofs.

Hi Joe,

> class Group =
>   fixes oper :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "[*]" 65)
>   and ivr :: "'a \<Rightarrow> 'a"
>   and e :: "'a"
>   assumes grp_assoc: "a [*] (b [*] c) = (a [*] b) [*] c"
>   and grp_id_propR [simp]: "a [*] e = a"
>   and grp_inv_propR [simp]: "(ivr a [*] a) [*] b = b"
> begin

What I would recommend from a pragmatic point of view is to use the simp

> lemma grp_mult_id:
>   assumes a_eq_c: "a = c"
>   shows "(a [*] b = c [*] b) \<and> (b [*] a = b [*] c)"
> proof
>   have refl: "b [*] a = b [*] a" ..
>   from refl and a_eq_c have "b [*] a = b [*] c" by simp

"simp" invokes an automated proof tool which performs equational
rewriting using assumptions in a goal and a predefined set of rewrite
rules (see the Isabelle tutorial for more information on this).

Intermediate results in a proof are stated using "have".  Assumptions
"assume" are part the resulting theorem of a proof and therefore must
fit to an outer proof obligation, which is not the case in your proof
because "b [*] a = b [*] a" is not part of the assumptions of the lemma.

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.