*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Suspicious URL: Re: TERM exception in fologic.ML*From*: Thomas Sewell <thomas.sewell at nicta.com.au>*Date*: Fri, 12 Dec 2014 14:08:08 +1100*In-reply-to*: <alpine.LNX.2.00.1410272117360.11086@lxbroy10.informatik.tu-muenchen.de>*References*: <1864084597.460696.1414438472602.JavaMail.yahoo@jws10705.mail.gq1.yahoo.com> <alpine.LNX.2.00.1410272117360.11086@lxbroy10.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.3.0

Hello Slawomir & Isabelle users. I'm sorry I missed this discussion going by. Thanks to Makarius for bringing it to my attention. The problem can be traced to the way blast_hyp_subst_tac works, and can be triggered like this (in HOL): theory Scratch imports main begin lemma "x = y ==> (!!x. True) ==> x : T ==> S <= T ==> T <= R ==> S <= R" apply blast This will happen when blast is called on any goal, in HOL or in ZF, where the goal must be nontrivial, provable by blast's internal strategy, contain a substitutable equality hypothesis, and contain some non-atomic hypothesis (a meta-forall, meta-implication or meta-equality). This has always been the case. What has changed is that auto no longer removes the equality hypothesis itself before calling blast. The problem is that blast_hyp_subst_tac just won't work if the hypotheses aren't all atomic. The TERM exception comes from the "map dest_Trueprop", but in any case the implementation won't work with meta-operators either. The trivial fix is to extend the "handle THM _ => no_tac | EQ_VAR => no_tac" in blast_hyp_subst_tac to also handle TERM exceptions. This will completely solve the current problem. I recommend somebody commit this in time for the next release, at which point [[hypsubst_thin = true]] will no longer be needed for this auto. This leaves the problem that there are three implementations of hypsubst in hypsubst.ML, one which doesn't work with Vars and two which don't work with meta-operators. I don't really know what to do about this. It doesn't help that I don't understand what constraints blast really puts on blast_hyp_subst_tac. Cheers, Thomas. On 28/10/14 07:22, Makarius wrote:

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

________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

- Previous by Date: [isabelle] Parallelising apply-style proofs
- Next by Date: [isabelle] Open postdoc position in Florianopolis/Brazil
- Previous by Thread: Re: [isabelle] Parallelising apply-style proofs
- Next by Thread: [isabelle] Open postdoc position in Florianopolis/Brazil
- Cl-isabelle-users December 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list