*To*: David Cock <david.cock at inf.ethz.ch>*Subject*: Re: [isabelle] universal quantifiers vs. schematic variables*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Sun, 4 Oct 2015 23:51:25 -0300*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <56117398.3070207@inf.ethz.ch>*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>*Sender*: alfio.martini at gmail.com

Dear Users, Let's try that again. > > If you prove: > > lemma "P x" > by(whatever) > > then (assuming x was completely unbound at that point), you've obviously > done something at least as hard as proving > > lemma "!x. P x" > > i.e. proving something about a concrete x, without assuming anything in > particular about it, and thus your proof could in principle be reapplied to > any other concrete value. Isabelle "knows" this, and thus transparently > lifts your result to the schematic lemma "P ?x", ie. a lemma with a named > hole where x should be. That hole can be filled with whatever you like, > and so, as Jasmin pointed out, you've effectively got a universally > quantified result. > 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. Indeed, once the theorem is proved, the object logic variable 'n' is lifted into a schematic variable by Isabelle. Best! On Sun, Oct 4, 2015 at 3:44 PM, David Cock <david.cock at inf.ethz.ch> wrote: > Let's try that again. > > If you prove: > > lemma "P x" > by(whatever) > > then (assuming x was completely unbound at that point), you've obviously > done something at least as hard as proving > > lemma "!x. P x" > > i.e. proving something about a concrete x, without assuming anything in > particular about it, and thus your proof could in principle be reapplied to > any other concrete value. Isabelle "knows" this, and thus transparently > lifts your result to the schematic lemma "P ?x", ie. a lemma with a named > hole where x should be. That hole can be filled with whatever you like, > and so, as Jasmin pointed out, you've effectively got a universally > quantified result. > > Schematics in the conclusion (e.g. in a subgoal) can work differently. If > at some point you end up with a subgoal of the form "P ?x", you can prove > it by substituting a *particular* x that satisfies (P x). For example, you > can prove "?x = (0::nat)" with "by(refl)" (i.e. substituting 0), but that > proof obviously *doesn't* generalise to all possible substitutions. > > In summary, propositions with schematics are a *bit* like universally > quantified formulae, but not quite. The semantics get more complicated > when a given schematic appears multiple times e.g. in assumption and > conclusions. In that case, by instantiating a schematic, you're making a > (potentially unsafe) *choice* in your proof - you may end up in an > unprovable state, even for a true theorem. > > Larry could presumably shine more light on the design decisions here, but > schematics are (as far as I understand) a more fundamental part of the term > rewriting system, with something more of an "operational" semantics i.e. it > does what it does, while "!" is the quantifier of Pure, with a specific > logical interpretation. > > Dave > > > On 04/10/15 11:22, David Cock wrote: > >> Grr, sorry, hit send without proofreading. That second one should have >> been >> >> P x => P y >> >> i.e. an *unbound*, not a schematic name. >> >> Noam: in your example, it's not clear whether you have an actual >> schematic, or just an unbound (blue) variable. >> >> David >> >> On 04/10/15 11:19, Jasmin Blanchette wrote: >> >>> David, >>> >>> you've just discovered one of Isabelle's most fundamental quirks. As >>>> theorems, you're right that they're (logically) equivalent, but they differ >>>> if they appear as assumptions i.e. >>>> >>>> (!x. P x) => P y >>>> >>>> holds, but >>>> >>>> P ?x => P y >>>> >>>> does not (necessarily) hold. >>>> >>> Huh? >>> >>> schematic_lemma "P ?x ==> P y" >>> by assumption >>> >>> Cheers, >>> >>> Jasmin >>> >>> >> >> > > -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) www.inf.pucrs.br/alfio Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica 90619-900 -Porto Alegre - RS - Brasil

**Follow-Ups**:**Re: [isabelle] universal quantifiers vs. schematic variables***From:*Lars Noschinski

**Re: [isabelle] universal quantifiers vs. schematic variables***From:*Larry Paulson

**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

- Previous by Date: Re: [isabelle] Reverse sorting
- Next by Date: [isabelle] 2nd CfP MILS Prague 19 Jan 2016
- 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