*To*: Alfio Martini <alfio.martini at acm.org>*Subject*: Re: [isabelle] universal quantifiers vs. schematic variables*From*: Larry Paulson <lp15 at cam.ac.uk>*Date*: Mon, 5 Oct 2015 11:43:25 +0100*Cc*: David Cock <david.cock at inf.ethz.ch>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAAPnxw2StF-cAYAKJVvDHPOd+cLGPrkGNf6oEAH46JAPvkzOzA@mail.gmail.com>*References*: <CAGOKs08m2EpBhQcrCb5n6t0VqtpesC2T1iia32d9rA0oCfhtcQ@mail.gmail.com> <561169D0.1020100@inf.ethz.ch> <AEB8C84A-3BCD-4D97-B8C6-006C6345D1CA@inria.fr> <56116E66.7030606@inf.ethz.ch> <56117398.3070207@inf.ethz.ch> <CAAPnxw2StF-cAYAKJVvDHPOd+cLGPrkGNf6oEAH46JAPvkzOzA@mail.gmail.com>

The answer to this question is simple: induction rules are formulated in this way in Isabelle because Martin-LÃf used the same approach in his constructive type theory. He arrived at this formulation by following the idea of natural deduction consistently. In natural deduction, every inference rule introduces or eliminates a distinguished symbol, and Martin-LÃf recognised that in the case of induction rules, the symbol being eliminated was the premise ân is a natural numberâ. He used a similar approach with the elimination rules for finite sums and products, generalised sums, etc. One does not have to be a constructivist to to recognise that his was the right approach, and that attaching a universal quantifier to the conclusion is superfluous. Larry Paulson > On 5 Oct 2015, at 03:51, Alfio Martini <alfio.martini at acm.org> wrote: > > This for me is a very good explanation for something that has always > puzzled me, i.e., the way induction rules are formalized > in Isabelle. For instance, the rule nat_induct0 is formalized as follows: > > lemma nat_induct0: > fixes n > assumes "P 0" and "ân. P n â P (Suc n)" > shows "P n" > > If I would formulate this rule, I would (unnecessarily I see), write the > conclusion as "!n. P n", since this is what the rule allows me > to infer if the premises are satisfied. From the logical point of view, it > would have a clearer and more natural reading.

**References**:**[isabelle] universal quantifiers vs. schematic variables***From:*noam neer

**Re: [isabelle] universal quantifiers vs. schematic variables***From:*David Cock

**Re: [isabelle] universal quantifiers vs. schematic variables***From:*Jasmin Blanchette

**Re: [isabelle] universal quantifiers vs. schematic variables***From:*David Cock

**Re: [isabelle] universal quantifiers vs. schematic variables***From:*David Cock

**Re: [isabelle] universal quantifiers vs. schematic variables***From:*Alfio Martini

- Previous by Date: Re: [isabelle] universal quantifiers vs. schematic variables
- Next by Date: Re: [isabelle] apply a rewriting-lemma only once
- Previous by Thread: Re: [isabelle] universal quantifiers vs. schematic variables
- Next by Thread: Re: [isabelle] universal quantifiers vs. schematic variables
- Cl-isabelle-users October 2015 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