Re: [isabelle] TERM exception in fologic.ML



On Mon, 27 Oct 2014, Slawomir Kolodynski wrote:

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

A TERM exception is indeed an internal breakdown. With some fiddling, I managed to get an exception trace as follows (via Poly/ML 5.3.0):

List.map(2)
List.map(2)
List.map(2)
List.map(2)
Hypsubst().blast_hyp_subst_tac(1)(2)
Tactical.CSUBGOAL(3)
Tactical.CSUBGOAL(3)
Tactical.CSUBGOAL(3)
Tactical.EVY(1)(1)
Blast().raw_blast(4)cont(3)
Blast().prove(4)prv(4)closeF(1)
Blast().prove(4)prv(4)
Blast().prove(4)prv(4)deeper(1)
Blast().prove(4)prv(4)
Blast().prove(4)prv(4)closeF(1)
Blast().prove(4)prv(4)
Blast().prove(4)prv(4)closeF(1)
Blast().prove(4)prv(4)
Blast().prove(4)prv(4)deeper(1)
Blast().prove(4)prv(4)
Blast().prove(4)prv(4)deeper(1)
Blast().prove(4)prv(4)
Blast().prove(4)prv(4)deeper(1)
Blast().prove(4)prv(4)
Blast().prove(4)prv(4)
Blast().prove(4)
Blast().raw_blast(4)


This indicates that it is related to the following change from NEWS:

* Standard tactics and proof methods such as "clarsimp", "auto" and
"safe" now preserve equality hypotheses "x = expr" where x is a free
variable.  Locale assumptions and chained facts containing "x"
continue to be useful.  The new method "hypsubst_thin" and the
configuration option "hypsubst_thin" (within the attribute name space)
restore the previous behavior.  INCOMPATIBILITY, especially where
induction is done after these methods or when the names of free and
bound variables clash.  As first approximation, old proofs may be
repaired by "using [[hypsubst_thin = true]]" in the critical spot.


So your proof works again like this:

  using [[hypsubst_thin = true]] by auto

Although that can only be a temporary workaround.

Thomas Sewell who made the hypsubst change should be able to say more about this situation.


	Makarius

----------------------------------------------------------------------------
                   http://stop-ttip.org  743,200 people so far
----------------------------------------------------------------------------


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