Re: [isabelle] resolve current subgoal with matching premise



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.