Email Gateway (Aug 19 2022 at 12:48): Email Gateway (Aug 19 2022 at 12:48):From: Peter Lammich <lammich@in.tum.de>
Refering to RC-2:
Here is a minimal example:
lemma "finite {(q, q', _). R q \<and> P q' q}"
apply simp
*** Tactic failed
*** The error(s) above occurred for the goal statement:
*** {(q, ab). R q \<and> (case ab of (q', uu_) \<Rightarrow> P q' q)} =
*** {(q, ab) |q ab. R q \<and> (case ab of (q', uu_) \<Rightarrow> P q'
q)}
*** (line 7 of "/home/lammich/devel/isabelle/Scratch.thy")
*** At command "apply" (line 7 of
"/home/lammich/devel/isabelle/Scratch.thy")
Exception trace - Tactic failed
The error(s) above occurred for the goal statement:
{(q, ab). R q \<and> (case ab of (q', uu_) \<Rightarrow> P q' q)} =
{(q, ab) |q ab. R q \<and> (case ab of (q', uu_) \<Rightarrow> P q' q)}
(line 7 of "/home/lammich/devel/isabelle/Scratch.thy")
Goal.prove_common(7)
Set_Comprehension_Pointfree.comprehension_conv(2)
Conv.then_conv(3)
Set_Comprehension_Pointfree.conv(2)
Set_Comprehension_Pointfree.simproc(2)
Raw_Simplifier.rewritec(4)proc_rews(1)
Raw_Simplifier.rewritec(4)
Raw_Simplifier.bottomc(3)botc(3)
Raw_Simplifier.bottomc(3)subc(3)appc(1)
Raw_Simplifier.bottomc(3)subc(3)
Raw_Simplifier.bottomc(3)botc(3)
Raw_Simplifier.bottomc(3)try_botc(1)(1)
Conv.gconv_rule(3)
Tactical.THEN(1)(1)
Seq.maps(2)(1)
Seq.maps(2)(1)
Seq.filter(2)copy(1)(1)
Seq.append(2)copy(1)(1)
Seq.append(2)copy(1)(1)
Seq.map(2)(1)
Seq.map(2)(1)
Seq.map(2)(1)
Seq.map(2)(1)
Seq.append(2)copy(1)(1)
Seq.first_result(2)result(2)
Seq.first_result(2)
Toplevel.proofs'(1)(1)(1)
Email Gateway (Aug 19 2022 at 12:48):From: Makarius <makarius@sketis.net>
Just another crash of the Set_Comprehension_Pointfree simproc. I see the
same in Isabelle2013, which indicates that any attempts to repair it are
for the release after Isabelle2013-1.
Makarius
Last updated: Apr 25 2024 at 01:08 UTC