*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Reverse sorting*From*: "W. Douglas Maurer" <maurer at email.gwu.edu>*Date*: Sun, 4 Oct 2015 20:34:44 -0400*In-reply-to*: <mailman.29241.1443984286.2651.cl-isabelle-users@lists.cam.ac.uk>*References*: <mailman.29241.1443984286.2651.cl-isabelle-users@lists.cam.ac.uk>

Your question has an answer that is independent of any specific system such as Isabelle. Any sorting algorithm has a parameter which is a Boolean comparison function of two arguments. Let's call the function LEQ, and let's call the arguments A and B. Typically LEQ(A, B) returns true if A <= B in some sense, and it returns false otherwise. To do a reverse sort, simply redefine LEQ(A, B) to return true if A >= B in that same sense, and to return false otherwise. Now call your sort program with the new LEQ as its actual parameter, and you will automatically get a reverse sort. Sent from my iPhone > On Oct 4, 2015, at 2:44 PM, cl-isabelle-users-request at lists.cam.ac.uk wrote: > > Send Cl-isabelle-users mailing list submissions to > cl-isabelle-users at lists.cam.ac.uk > > To subscribe or unsubscribe via the World Wide Web, visit > https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users > or, via email, send a message with subject or body 'help' to > cl-isabelle-users-request at lists.cam.ac.uk > > You can reach the person managing the list at > cl-isabelle-users-owner at lists.cam.ac.uk > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Cl-isabelle-users digest..." > > > Today's Topics: > > 1. Re: Font substitution and handling in Isabelle/jEdit (Makarius) > 2. Re: Build problems on Windows (Makarius) > 3. Code generation for reverse sorting (Christian Sternagel) > 4. universal quantifiers vs. schematic variables (noam neer) > 5. Re: universal quantifiers vs. schematic variables (David Cock) > 6. Re: universal quantifiers vs. schematic variables > (Jasmin Blanchette) > 7. Re: universal quantifiers vs. schematic variables (David Cock) > 8. Re: universal quantifiers vs. schematic variables (Lars Hupel) > 9. Re: universal quantifiers vs. schematic variables (David Cock) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Fri, 2 Oct 2015 20:58:33 +0200 (CEST) > From: Makarius <makarius at sketis.net> > Subject: Re: [isabelle] Font substitution and handling in > Isabelle/jEdit > To: Rafal Kolanski <xs at xaph.net> > Cc: isabelle-users <isabelle-users at cl.cam.ac.uk> > Message-ID: > <alpine.LNX.2.00.1510022055510.6749 at lxbroy10.informatik.tu-muenchen.de> > > Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed > >> On Tue, 15 Sep 2015, Rafal Kolanski wrote: >> >> There is a small update to this. Because some fonts (e.g. IsabelleText) >> are dynamically inserted at Isabelle plugin load into the graphics >> context *after* jEdit has loaded all properties ("settings"), jEdit >> doesn't see them. > > I have recently made various reforms in the isabelle.Main vs. jedit.jar > initialization sequence, which is relevant for the coming winter release > of Isabelle2016. > > If there are remaining problems, we should continue the discussion on the > isabelle-dev mailing list. The current point of reference is changeset > be3a5fee11e3. > > > Makarius > > > > ------------------------------ > > Message: 2 > Date: Fri, 2 Oct 2015 23:36:39 +0200 (CEST) > From: Makarius <makarius at sketis.net> > Subject: Re: [isabelle] Build problems on Windows > To: Lars Hupel <hupel at in.tum.de> > Cc: cl-isabelle-users at lists.cam.ac.uk > Message-ID: > <alpine.LNX.2.00.1510022333370.10979 at lxbroy10.informatik.tu-muenchen.de> > > Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed > > On Sat, 19 Sep 2015, Lars Hupel wrote: > >>> What happens with the shell command-line tool? >> >> I'm not sure how to invoke that. This is a headless installation where I >> simply extracted the Tarball (which worked perfectly on the other machine). > > Headless installation on Windows is not expected: you need to go through > isabelle.Main and its special tricks for Cygwin initialization. In > Isabelle2015 this requires to run the end-user application. > > I've started to rework that for the coming release. We probably need to > discuss further fine-points separately, e.g. to make a generic jar bundle > that excludes the jdk. > > > Makarius > > > > > ------------------------------ > > Message: 3 > Date: Sat, 3 Oct 2015 21:59:53 +0200 > From: Christian Sternagel <c.sternagel at gmail.com> > Subject: [isabelle] Code generation for reverse sorting > To: "cl-isabelle-users at lists.cam.ac.uk" > <cl-isabelle-users at lists.cam.ac.uk> > Message-ID: <561033B9.1000806 at gmail.com> > Content-Type: text/plain; charset=utf-8 > > Dear all, > > for those of you who do not regularly check stackoverflow but might have > an answer to my question there (yes I am looking at you Florian ;) ) I'm > brazenly posting the link to my question here > > http://stackoverflow.com/q/32926842/476803 > > In short, my question is: What is the easiest way to generate code for a > sorting algorithm that sorts its argument in reverse order, while > building on top of the existing List.sort? > > cheers > > chris > > > > ------------------------------ > > Message: 4 > Date: Sun, 4 Oct 2015 20:47:53 +0300 > From: noam neer <noamneer at gmail.com> > Subject: [isabelle] universal quantifiers vs. schematic variables > To: "cl-isabelle-users at lists.cam.ac.uk" > <cl-isabelle-users at lists.cam.ac.uk> > Message-ID: > <CAGOKs08m2EpBhQcrCb5n6t0VqtpesC2T1iia32d9rA0oCfhtcQ at mail.gmail.com> > Content-Type: text/plain; charset=UTF-8 > > if "P" is a previously defined predicate and I want to prove it always > holds, it seems I can do it in two ways. the first uses the universal > quantifier as in > lemma "!x. P(x)" > .... > and the second uses schematic variables, as in > lemma "P(x)" > ... > if I'm not mistaken each of these can be used to prove the other, so they > are logically equivalent. the only differences I could find were in the way > the proved lemmas can be used in proofs, where usually the second > formulation is easier to use. my question is if this is indeed the case, > and if so why does Isabelle offer two different ways to say the same thing. > comparing to the case of --> and ==>, the different arrows are also > logically equivalent but they are intended for different situations, but I > couldn't find such distinction in the universal case. > > thanx. > > > ------------------------------ > > Message: 5 > Date: Sun, 4 Oct 2015 11:02:56 -0700 > From: David Cock <david.cock at inf.ethz.ch> > Subject: Re: [isabelle] universal quantifiers vs. schematic variables > To: <cl-isabelle-users at lists.cam.ac.uk> > Message-ID: <561169D0.1020100 at inf.ethz.ch> > Content-Type: text/plain; charset="utf-8"; format=flowed > > Noam, > You'll probably get answers from more knowledgable persons than I, > but 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. In the second case, you know that P holds > for some (particular, unspecified) x, but you don't know whether that is > equal to y. > > David > >> On 04/10/15 10:47, noam neer wrote: >> if "P" is a previously defined predicate and I want to prove it always >> holds, it seems I can do it in two ways. the first uses the universal >> quantifier as in >> lemma "!x. P(x)" >> .... >> and the second uses schematic variables, as in >> lemma "P(x)" >> ... >> if I'm not mistaken each of these can be used to prove the other, so they >> are logically equivalent. the only differences I could find were in the way >> the proved lemmas can be used in proofs, where usually the second >> formulation is easier to use. my question is if this is indeed the case, >> and if so why does Isabelle offer two different ways to say the same thing. >> comparing to the case of --> and ==>, the different arrows are also >> logically equivalent but they are intended for different situations, but I >> couldn't find such distinction in the universal case. >> >> thanx. > > > > > ------------------------------ > > Message: 6 > Date: Sun, 4 Oct 2015 20:19:20 +0200 > From: Jasmin Blanchette <jasmin.blanchette at inria.fr> > Subject: Re: [isabelle] universal quantifiers vs. schematic variables > To: David Cock <david.cock at inf.ethz.ch> > Cc: cl-isabelle-users at lists.cam.ac.uk > Message-ID: <AEB8C84A-3BCD-4D97-B8C6-006C6345D1CA at inria.fr> > Content-Type: text/plain; charset=us-ascii > > 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 > > > > > ------------------------------ > > Message: 7 > Date: Sun, 4 Oct 2015 11:22:30 -0700 > From: David Cock <david.cock at inf.ethz.ch> > Subject: Re: [isabelle] universal quantifiers vs. schematic variables > To: Jasmin Blanchette <jasmin.blanchette at inria.fr> > Cc: cl-isabelle-users at lists.cam.ac.uk > Message-ID: <56116E66.7030606 at inf.ethz.ch> > Content-Type: text/plain; charset="windows-1252"; format=flowed > > 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 > > > > > ------------------------------ > > Message: 8 > Date: Sun, 4 Oct 2015 20:24:40 +0200 > From: Lars Hupel <hupel at in.tum.de> > Subject: Re: [isabelle] universal quantifiers vs. schematic variables > To: noam neer <noamneer at gmail.com>, > "cl-isabelle-users at lists.cam.ac.uk" > <cl-isabelle-users at lists.cam.ac.uk> > Message-ID: <56116EE8.1020007 at in.tum.de> > Content-Type: text/plain; charset=utf-8 > > Hi, > >> if "P" is a previously defined predicate and I want to prove it always >> holds, it seems I can do it in two ways. the first uses the universal >> quantifier as in >> lemma "!x. P(x)" >> .... >> and the second uses schematic variables, as in >> lemma "P(x)" >> ... >> if I'm not mistaken each of these can be used to prove the other, so they >> are logically equivalent. the only differences I could find were in the way >> the proved lemmas can be used in proofs, where usually the second >> formulation is easier to use. > > first of all, your assessment is correct. Nitpicking: In the second > formulation, you use the free variable 'x', which ? after proving the > lemma ? gets generalized to a schematic variable. You can recognize > schematic variables by the prefixed question mark (e.g. '?x'). > >> and if so why does Isabelle offer two different ways to say the same thing. >> comparing to the case of --> and ==>, the different arrows are also >> logically equivalent but they are intended for different situations, but I >> couldn't find such distinction in the universal case. > > I don't have an insight into the early history of Isabelle. I have the > understanding that the notion of schematic has been there for a long > time. The only explanation I can offer is that schematic variables can > be easily instantiated. For example, if you have the theorem 'P ?x', you > can substitute '?x' by something arbitrary, without having to know about > the universal quantifier. In the explicitly-quantified case (be it HOL > quantification or Pure quantification), the 'x' would be a bound > variable and you would need to know more. Essentially, schematic > variables allow for easy *outermost* quantification. > > Cheers > Lars > > > > ------------------------------ > > Message: 9 > Date: Sun, 4 Oct 2015 11:44:40 -0700 > From: David Cock <david.cock at inf.ethz.ch> > Subject: Re: [isabelle] universal quantifiers vs. schematic variables > To: <cl-isabelle-users at lists.cam.ac.uk> > Message-ID: <56117398.3070207 at inf.ethz.ch> > Content-Type: text/plain; charset="windows-1252"; format=flowed > > 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 > > > > > End of Cl-isabelle-users Digest, Vol 124, Issue 3 > *************************************************

- Previous by Date: Re: [isabelle] universal quantifiers vs. schematic variables
- Next by Date: Re: [isabelle] universal quantifiers vs. schematic variables
- Previous by Thread: Re: [isabelle] universal quantifiers vs. schematic variables
- Next by Thread: [isabelle] 2nd CfP MILS Prague 19 Jan 2016
- 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