[isabelle] TERM exception in fologic.ML



When I was updating the IsarMathLib project for Isabelle 2014 I got the following:
*** exception TERM raised (line 47 of "~~/src/FOL/fologic.ML"):
*** dest_Trueprop
*** !!f A B. ALL a b. f : Pi(A, B) --> <a, b> : f <-> a : A & f ` a = b
*** At command "by" (line 605 of "~/Projects/IsarMathLib/isarmathlib-1.9.1/IsarMathLib/func1.thy")
*** exception TERM raised (line 47 of "~~/src/FOL/fologic.ML"):
*** dest_Trueprop
*** !!a A B. a : Sigma(A, B) --> <fst(a), snd(a)> = a
*** At command "by" (line 296 of "~/Projects/IsarMathLib/isarmathlib-1.9.1/IsarMathLib/Topology_ZF_10.thy")

I was able to work around this by rewriting the proofs slightly. I understand that the TERM exceptions are not just failures to check a proof but some internal errors (?), so I just wanted to report this for consideration for the next release.
The exception can be replicated by checking the following theory (in 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

Regards,,Slawomir Kolodynski http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)


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