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

[Lawrence Paulson]

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
> ----------------------------------------------------------------------------