I wonder if we can look at this problem, which has been around for at least 18 months. It seems to be connected with the recent modification to hyp_subst_tac, which now retains the equality. (The workaround of switching off this behaviour is not a true solution.) I took a look at this code would couldn’t make any headway. I hope that somebody else has a suggestion.
Note that this concerns Isabelle/ZF. Larry > Begin forwarded message: > > From: Slawomir Kolodynski via Cl-isabelle-users > <cl-isabelle-us...@lists.cam.ac.uk> > Subject: [isabelle] TERM exception in fologic.ML > Date: 23 January 2016 at 17:19:42 GMT > To: "Cl-isabelle-us." <cl-isabelle-us...@lists.cam.ac.uk> > Reply-To: Slawomir Kolodynski <skoko...@yahoo.com> > > Back in October 2014 I reported an error that I encountered when updating > IsarMathLib to Isabelle 2014.The error is still there in Isabelle2016-RC1. > This can be replicated by checking the following theory (in Isabelle/ZF > logic): > theory Scratch imports func > > begin > > lemma func_imagedef: assumes A1: "f:X\<rightarrow>Y" and A2: "A\<subseteq>X" > shows "f``(A) = {f`(x). x \<in> A}" > proof > from A1 show "f``(A) \<subseteq> {f`(x). x \<in> A}" > using image_iff apply_iff by auto > show "{f`(x). x \<in> A} \<subseteq> f``(A)" > proof > fix y assume "y \<in> {f`(x). x \<in> A}" > then obtain x where "x\<in>A \<and> y = f`(x)" > by auto > with A1 A2 show "y \<in> f``(A)" > using apply_iff image_iff by auto > qed > qed > > end > which gives > exception TERM raised (line 47 of "~~/src/FOL/fologic.ML"): > dest_Trueprop > ⋀f A B. > ∀a b. f ∈ Pi(A, B) ⟶ > ⟨a, b⟩ ∈ f ⟷ a ∈ A ∧ f ` a = b > in Isabelle/jEdit tooltip at the last auto keyword. > This is not a very important problem for me as I can work around it, but > maybe it's good to know that it is still there. > Slawomir Kolodynski _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev