*To*: Alfio Martini <alfio.martini at acm.org>*Subject*: Re: [isabelle] Eliminating two quantifiers in structural proof*From*: Makarius <makarius at sketis.net>*Date*: Mon, 24 Sep 2012 21:52:56 +0200 (CEST)*Cc*: Edward Schwartz <edmcman at cmu.edu>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAAPnxw0bFKyUcf_puXQO+gPLHrsqVHFfqhyOTGxF=G5i22xHTQ@mail.gmail.com>*References*: <CAHPz_MptGHQPi+5mtx+OeZSBuR=2yzib5mZMH1sZJuqV5NFZJw@mail.gmail.com> <CAAPnxw0bFKyUcf_puXQO+gPLHrsqVHFfqhyOTGxF=G5i22xHTQ@mail.gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Sun, 16 Sep 2012, Alfio Martini wrote:

I am not sure if this is what you what, but in Isar is fairly natural to do such proofs. I use it to teach natural deduction to students. Here goes three proofs of this conjecture: theorem th11a: assumes prem: "∀x. ∀y. P x y" shows "P a b" proof - from prem have "∀y. P a y" by (rule spec) thus "P a b" by (rule spec) qed theorem th11b: assumes prem: "∀x. ∀y. P x y" shows "P a b" proof - from prem have "∀y. P a y" by (rule allE) thus "P a b" by (rule allE) qed theorem th11c: assumes prem: "∀x. ∀y. P x y" shows "P a b" proof - from prem have "∀y. P a y" by (rule spec[where x =a]) from this show "P a b" by (rule spec[where x=b]) qedI assume you hardly have to use the qualifieres (e(limination),d(estruction)) when working in Isar. I use this style only when I amplaying with linear scripts.

So there is a large combinatorial space of (then | from | with | ... | also | finally | moreover | ultimately) (have | show | obtain | interpret ...)

Makarius

**References**:**[isabelle] Eliminating two quantifiers in structural proof***From:*Edward Schwartz

**Re: [isabelle] Eliminating two quantifiers in structural proof***From:*Alfio Martini

- Previous by Date: Re: [isabelle] Isar feature request: bbold ... (& italics, ibold)
- Next by Date: Re: [isabelle] Eliminating two quantifiers in structural proof
- Previous by Thread: Re: [isabelle] Eliminating two quantifiers in structural proof
- Next by Thread: Re: [isabelle] Eliminating two quantifiers in structural proof
- Cl-isabelle-users September 2012 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