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



You know what it was, I just had the goal wrong. I mistyped and put "a [*] b = a [*] c". You're advice worked perfectly after I saw that...

Teach me to try to prove stuff in the wee hours of the morning!

Thanks so much for your help.

If I can bother you with another question. I wanted to get `ivr` to have a prefix unary syntax (or a postfix, the problem (I imagine) is isomorphic), once again, I just can't seem to find a suitable incantation. The big tutorial (the 200+ page one) talks about using datatypes somewhere for this purpose, But I don't see how that helps me here.

Further, another (semi-related) question. In Haskell (which is where my background lies), one can do associated datatypes, eg

	class Foo a where
		data Bar a :: * -> *
		bar :: Bar a b -> b -> (a,b)
		--whatever

is there an analog in Isabelle?

On Oct 29, 2009, at 5:45 AM, Florian Haftmann wrote:

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
method:

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,
	Florian

--

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de







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