Re: [isabelle] induction: list
You have overlooked the warning about induct_tac in section 2.4.5 in the
tutorial: the induction variable should not appear in the premises.
Use method "induct" instead.
I believe foldl is already defined in Isabelle2005 - it certainly is now.
And finally I recommend you try to prove a different lemma, because that
one is wrong. Try command quickcheck or think about it.
Lucas Cavalcante schrieb:
Dear users and developers,
I have defined this function:
consts foldl :: "('a * 'b => 'b) => 'b => 'a list => 'b"
"foldl f e  = e"
"foldl f e (x#xs) = foldl f (f (x,e)) xs"
Then I tried to prove this lemma:
lemma a1: "foldl f z x = foldl f y x ==> z = y"
But when I used the 'induct_tac' command over the variable 'x' (apply
(induct_tac x)) It resulted on these subgoals:
goal (lemma (a1), 2 subgoals):
1. foldl f z x = foldl f y x ==> z = y
2. !!a list. [| foldl f z x = foldl f y x; z = y |] ==> z = y
Why 'x' is not been replaced by '' in first subgoal and 'a#list' in the
second one, as it should be?
I thank you in advance for any clarification concerning my above doubts!
PS.: Is not 'isabelle-interface' supported by emacs22?
This archive was generated by a fusion of
Pipermail (Mailman edition) and