Re: [isabelle] Reverse sorting



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.