Re: [isabelle] resolve current subgoal with matching premise



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.