*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Equivalent to schematic_lemma inside proof blocks*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 29 Jun 2015 09:10:10 +0200*Cc*: Johannes Hölzl <hoelzl at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1506151620510.53111@lxbroy10.informatik.tu-muenchen.de>*References*: <5559C325.4030909@inf.ethz.ch> <1431950411.31939.5.camel@in.tum.de> <5559EB39.1040506@inf.ethz.ch> <alpine.LNX.2.00.1506151620510.53111@lxbroy10.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.7.0

Hi Makarius,

Andreas On 15/06/15 16:23, Makarius wrote:

On Mon, 18 May 2015, Andreas Lochbihler wrote:Meanwhile, I found out how to do it in forward-reasoning style with guess inside a proof block. lemma start: "[| TERM x; foo x m; foo x m ==> thesis |] ==> thesis" by assumption notepad begin have "TERM a_very_large_expression" by(simp add: term_def) then guess by(rule start)(rule syntactic_analysis_rules)+ then have "foo a_very_large_expression (245 * x + 7 * y + 3)" by(rule foo_mono) simp end Of course, the computation performed by the syntactic_analysis_rules cannot be written in Isar, but that's fine. The TERM expression is only needed to instantiate the expression in the start rule. By slightly changing the start rule, I can even obtain an abbreviation for the compound term as an equation during the guess step (without ever having to write it down :-) ).Does it mean everything works out, or are there pending questions? Almost arbitrary tricks may be played. The standard Isar policies merely try to make non-sense hard. BTW, the canonical proof for "TERM x" is "." -- is is considered vacuous within Isabelle/Pure. Makarius

**References**:

- Previous by Date: Re: [isabelle] Lost indexname in instantiated theorem: Eisbach messes up "of" and "where" attributes, when instantiating with "TYPE(...)"
- Next by Date: Re: [isabelle] Eisbach: HOL vs. Pure
- Previous by Thread: Re: [isabelle] Equivalent to schematic_lemma inside proof blocks
- Next by Thread: Re: [isabelle] build tool and moving of files
- Cl-isabelle-users June 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