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

[Makarius]

On Tue, 12 Apr 2016, Lawrence Paulson wrote:


A relevant past message.


We have more messages in the archives, about blast ignoring the 
distinction of Trueprop vs. non-Trueprop propositions. This boils down to 
the following example, which is non-terminating in Isabelle2016 and 
current Isabelle/8b85a554c5c4:


lemma "(⋀P. P::bool) ⟹ PROP P" by blast


Do you still have a sense of your own src/Provers/blast.ML? It might be an 
easy exercise with our fine ML IDE to brush it up a little bit.




Date: 27 October 2014 at 20:22:02 GMT
http://stop-ttip.org  743,200 people so far


About 3 million further people have virtually joined that initiative, and 
there is another chance to participate physically, with A. Merkel and

B. Obama: http://www.ttip-demo.de


Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Lawrence Paulson]

A relevant past message.
Larry

> Begin forwarded message:
> 
> From: Makarius 
> Subject: Re: [isabelle] TERM exception in fologic.ML
> Date: 27 October 2014 at 20:22:02 GMT
> To: Slawomir Kolodynski 
> Cc: "cl-isabelle-us...@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\Y" and A2: "A\X"
>>   shows "f``(A) = {f`(x). x \ A}"
>> proof
>>   from A1 show "f``(A) \ {f`(x). x \ A}"
>> using image_iff apply_iff by auto
>>   show "{f`(x). x \ A} \ f``(A)"
>>   proof
>> fix y assume "y \ {f`(x). x \ A}"
>> then obtain x where "x\A \ y = f`(x)"
>>   by auto
>> with A1 A2 show "y \ 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
> 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[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 
> 
> Subject: [isabelle] TERM exception in fologic.ML
> Date: 23 January 2016 at 17:19:42 GMT
> To: "Cl-isabelle-us." 
> Reply-To: Slawomir Kolodynski 
> 
> 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\Y" and A2: "A\X"
>   shows "f``(A) = {f`(x). x \ A}"
> proof
>   from A1 show "f``(A) \ {f`(x). x \ A}"
> using image_iff apply_iff by auto
>   show "{f`(x). x \ A} \ f``(A)"
>   proof
> fix y assume "y \ {f`(x). x \ A}"
> then obtain x where "x\A \ y = f`(x)"
>   by auto
> with A1 A2 show "y \ 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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev