Email Gateway (Aug 18 2022 at 10:54): Email Gateway (Aug 18 2022 at 10:54):From: Lucas Cavalcante <thesupervisar@gmail.com>
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):
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?
Email Gateway (Aug 18 2022 at 10:54):From: Tobias Nipkow <nipkow@in.tum.de>
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.
Tobias
Lucas Cavalcante schrieb:
Email Gateway (Aug 18 2022 at 10:54):From: Makarius <makarius@sketis.net>
This script does not really do anything more than handing over to the
interface configured in the Isabelle settings, which is normally a version
of Proof General.
So the question is if your version of Proof General works with emacs22.
At least the more recent development snapshots of Proof General seem to
work fine when started via isabelle-interface -p emacs22
Makarius
Last updated: May 03 2024 at 08:18 UTC