*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Equivalent to schematic_lemma inside proof blocks*From*: Makarius <makarius at sketis.net>*Date*: Mon, 15 Jun 2015 16:23:32 +0200 (CEST)*Cc*: Johannes Hölzl <hoelzl at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5559EB39.1040506@inf.ethz.ch>*References*: <5559C325.4030909@inf.ethz.ch> <1431950411.31939.5.camel@in.tum.de> <5559EB39.1040506@inf.ethz.ch>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Mon, 18 May 2015, Andreas Lochbihler wrote:

Meanwhile, I found out how to do it in forward-reasoning style withguess inside a proof block.lemma start: "[| TERM x; foo x m; foo x m ==> thesis |] ==> thesis" byassumptionnotepad 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 endOf course, the computation performed by the syntactic_analysis_rulescannot be written in Isar, but that's fine. The TERM expression is onlyneeded to instantiate the expression in the start rule. By slightlychanging the start rule, I can even obtain an abbreviation for thecompound term as an equation during the guess step (without ever havingto write it down :-) ).

Makarius

**Follow-Ups**:**Re: [isabelle] Equivalent to schematic_lemma inside proof blocks***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] simp warnings for cong rules
- Next by Date: Re: [isabelle] Strange interaction between ambiguous syntax and dummy patterns
- Previous by Thread: Re: [isabelle] simp warnings for cong rules
- Next by Thread: Re: [isabelle] Equivalent to schematic_lemma inside proof blocks
- 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