*To*: Thomas Sewell <thomas.sewell at nicta.com.au>*Subject*: Re: [isabelle] TERM exception in fologic.ML*From*: Makarius <makarius at sketis.net>*Date*: Tue, 28 Apr 2015 16:01:19 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <548A5C18.2000907@nicta.com.au>*References*: <1864084597.460696.1414438472602.JavaMail.yahoo@jws10705.mail.gq1.yahoo.com> <alpine.LNX.2.00.1410272117360.11086@lxbroy10.informatik.tu-muenchen.de> <548A5C18.2000907@nicta.com.au>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 12 Dec 2014, Thomas Sewell wrote:

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 willcompletely solve the current problem. I recommend somebody commit thisin time for the next release, at which point [[hypsubst_thin = true]]will no longer be needed for this auto.

Makarius

# HG changeset patch # User wenzelm # Date 1430229197 -7200 # Tue Apr 28 15:53:17 2015 +0200 # Node ID 7d523eefe09f67418506d84b9fd2faa0e17dfae1 # Parent 18267ceb10b5d55806af77f89a88ade687e0b10b test; diff -r 18267ceb10b5 -r 7d523eefe09f src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Tue Apr 28 11:48:44 2015 +0200 +++ b/src/Provers/hypsubst.ML Tue Apr 28 15:53:17 2015 +0200 @@ -286,7 +286,7 @@ inst_subst_tac ctxt symopt (if symopt then ssubst else Data.subst) i, all_imp_intr_tac ctxt hyps i]) end - handle THM _ => no_tac | EQ_VAR => no_tac); + handle TERM _ => no_tac | THM _ => no_tac | EQ_VAR => no_tac); (*apply an equality or definition ONCE; fails unless the substitution has an effect*)

**Follow-Ups**:**Re: [isabelle] TERM exception in fologic.ML***From:*Larry Paulson

- Previous by Date: [isabelle] [2015-RC2] print_cases and underscore case names
- Next by Date: Re: [isabelle] TERM exception in fologic.ML
- Previous by Thread: [isabelle] [2015-RC2] print_cases and underscore case names
- Next by Thread: Re: [isabelle] TERM exception in fologic.ML
- Cl-isabelle-users April 2015 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