[isabelle-dev] Fwd: [isabelle] TERM exception in fologic.ML

[Lawrence Paulson]

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