Re: [isabelle] resolve current subgoal with matching premise



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.