Re: [isabelle] resolve current subgoal with matching premise



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.