Re: [isabelle] Set_Comprehension_Pointfree simproc produces unexpected "tactic failed" exception



On Thu, 7 Nov 2013, Peter Lammich wrote:

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)
Set_Comprehension_Pointfree.simproc(2)

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





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