*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] resolve current subgoal with matching premise*From*: Peter Lammich <lammich at in.tum.de>*Date*: Fri, 05 Dec 2014 16:09:30 +0100*In-reply-to*: <5481C604.2060008@in.tum.de>*References*: <5480CDAE.4090307@gmail.com> <94C2957A-B4C7-42ED-B349-3F3C8F583730@in.tum.de> <5B9C47B8-4C4C-4762-80BB-15BBA02D90A5@gmail.com> <54817D7F.1020704@gmail.com> <C381B664-9A9A-4131-9620-0D0481E41233@cam.ac.uk> <5481C032.4000405@gmail.com> <60BCD6BD-4F4E-44C9-B3D7-EA88ECE04939@cam.ac.uk> <5481C604.2060008@in.tum.de>

On Fr, 2014-12-05 at 15:49 +0100, Dmitriy Traytel wrote: > Well, the Subgoal.FOCUS combinator gives one at least some structure > (fixes and assumes) in the hands. > > So try: > > apply (tactic ‹HEADGOAL (Subgoal.FOCUS (fn {prems, ...} => HEADGOAL > (resolve_tac prems)) @{context})›) > > I believe Peter's solution is similar (but using CSUBGOAL instead). It does. I have copied it from the implementation of the "assumption"-method. Correct handling of schematics was important in my use-case (program synthesis, involving recursion-combinator), thus I could not use FOCUS. -- Peter > > Dmitriy > > On 05.12.2014 15:30, Lawrence Paulson wrote: > > I don’t know how to generate structured proofs by a package. I assume that it would be necessary to generate calls to the underlying abstract machine. I am not aware that this has been done before. > > > > Larry Paulson > > > > > >> On 5 Dec 2014, at 14:24, Christian Sternagel <c.sternagel at gmail.com> wrote: > >> > >> For a manual proof in Isar I completely agree. However, this is just a single example of many that are automatically generated inside a package. And the tactic should work for all generated goals (whose shape depends on the underlying datatype). For making the tactic structured - also I might be wrong since I never tried very hard - it seemed that I would have to do a lot of awkward code about how many premises and IHs are there and at what positions do they fit together etc. I had at least the feeling that such things should be left to some automatic search. But of course I would be delighted to be convinced otherwise. > >> > >> cheers > >> > >> chris > >> > >> On 12/05/2014 03:09 PM, Lawrence Paulson wrote: > >>> In this sort of situation, I would make every effort to switch to a structured proof style, when the induction hypothesis could be applied as an ordinary rule using the most primitive methods. > >>> > >>> Larry Paulson > >>> > >>> > >>>> On 5 Dec 2014, at 09:40, Christian Sternagel <c.sternagel at gmail.com> wrote: > >>>> > >>>> Thanks for the hint Jasmin! > >>>> > >>>> your suggestion looks promising, but unfortunately the last "erule meta_mp" fails on my actual subgoal, which looks as follows: > >>>> > >>>> goal (1 subgoal): > >>>> 1. ⋀x1a x2a p y z x ya yb xa xb yc. > >>>> (⋀x2aa x2aaa x2aaaa x2aaaaa. > >>>> x2aa ∈ set_tree x2a ⟹ > >>>> x2aaa ∈ Basic_BNFs.fsts x2aa ⟹ > >>>> x2aaaa ∈ set x2aaa ⟹ > >>>> x2aaaaa ∈ set_tree x2aaaa ⟹ > >>>> (⋀y. y ∈ set_nested x2aaaaa ⟹ show_law s y) ⟹ > >>>> show_law (showsp_nested s) x2aaaaa) ⟹ > >>>> (⋀y. y ∈ insert x1a > >>>> (UNION > >>>> (⋃x∈set_tree x2a. > >>>> ⋃x∈Basic_BNFs.fsts x. > >>>> UNION (set x) set_tree) > >>>> set_nested) ⟹ > >>>> show_law s y) ⟹ > >>>> yb ∈ set_tree x2a ⟹ > >>>> xa ∈ Basic_BNFs.fsts yb ⟹ > >>>> xb ∈ set xa ⟹ > >>>> yc ∈ set_tree xb ⟹ show_law (showsp_nested s) yc > >>>> > >>>> cheers > >>>> > >>>> chris > >>>> > >>>> On 12/04/2014 10:39 PM, Jasmin Christian Blanchette wrote: > >>>>> Am 04.12.2014 um 22:37 schrieb Jasmin Christian Blanchette <jasmin.blanchette at gmail.com>: > >>>>> > >>>>>> You could try > >>>>>> > >>>>>> apply ((drule meta_spec)+, erule meta_mp) > >>>>>> > >>>>>> E.g.: > >>>>>> > >>>>>> lemma "!! a1 aJ aN. > >>>>>> (!! b1 bK. q b1 bK) ==> > >>>>>> (!! i1 iI iM. r i1 iI iM ==> P iI) ==> > >>>>>> (!! z1 zL. s z1 zL) ==> P aJ" > >>>>>> apply ((drule meta_spec)+, erule meta_mp) > >>>>> I forgot: The example looks more impressive if you add > >>>>> > >>>>> consts P :: "nat ⇒ bool" > >>>>> consts q :: "nat ⇒ nat ⇒ bool" > >>>>> consts r :: "nat ⇒ nat ⇒ nat ⇒ bool" > >>>>> consts s :: "nat ⇒ nat ⇒ bool" > >>>>> > >>>>> Jasmin > >>>>> > > > >

**Follow-Ups**:**Re: [isabelle] resolve current subgoal with matching premise***From:*Christian Sternagel

**References**:**[isabelle] resolve current subgoal with matching premise***From:*Christian Sternagel

**Re: [isabelle] resolve current subgoal with matching premise***From:*Jasmin Christian Blanchette

**Re: [isabelle] resolve current subgoal with matching premise***From:*Jasmin Christian Blanchette

**Re: [isabelle] resolve current subgoal with matching premise***From:*Christian Sternagel

**Re: [isabelle] resolve current subgoal with matching premise***From:*Lawrence Paulson

**Re: [isabelle] resolve current subgoal with matching premise***From:*Christian Sternagel

**Re: [isabelle] resolve current subgoal with matching premise***From:*Lawrence Paulson

**Re: [isabelle] resolve current subgoal with matching premise***From:*Dmitriy Traytel

- Previous by Date: Re: [isabelle] resolve current subgoal with matching premise
- Next by Date: Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing
- Previous by Thread: Re: [isabelle] resolve current subgoal with matching premise
- Next by Thread: Re: [isabelle] resolve current subgoal with matching premise
- 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