[isabelle] induction: list



Dear users and developers,

I have defined this function:

consts foldl :: "('a * 'b => 'b) => 'b => 'a list => 'b"
primrec
"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.