Re: [isabelle] Reverse sorting

• 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
• 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
>
> 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.