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!
Lucas Cavalcante

PS.: Is not 'isabelle-interface' supported by emacs22?

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