[isabelle-dev] Fwd: [isabelle] TERM exception in fologic.ML
Lawrence Paulson
lp15 at cam.ac.uk
Tue Apr 12 15:36:16 CEST 2016
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-users at 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-users at lists.cam.ac.uk>
> Reply-To: Slawomir Kolodynski <skokodyn at 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
More information about the isabelle-dev
mailing list