[isabelle-dev] Fwd: [isabelle] TERM exception in fologic.ML
Lawrence Paulson
lp15 at cam.ac.uk
Tue Apr 12 15:36:51 CEST 2016
A relevant past message.
Larry
> Begin forwarded message:
>
> From: Makarius <makarius at sketis.net>
> Subject: Re: [isabelle] TERM exception in fologic.ML
> Date: 27 October 2014 at 20:22:02 GMT
> To: Slawomir Kolodynski <skokodyn at yahoo.com>
> Cc: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>
>
> 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
> ----------------------------------------------------------------------------
More information about the isabelle-dev
mailing list