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
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)
is there an analog in Isabelle?
On Oct 29, 2009, at 5:45 AM, Florian Haftmann wrote:
class Group =
fixes oper :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "[*]"
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"
What I would recommend from a pragmatic point of view is to use the
assumes a_eq_c: "a = c"
shows "(a [*] b = c [*] b) \<and> (b [*] a = b [*] c)"
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
Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and