Re: [isabelle] Cl-isabelle-users Digest, Vol 96, Issue 12



On Jun 29, 2013, at 3:51 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:  normalization method introduces schematic type variables
>      in HOL/Word types (Andreas Lochbihler)
>   2. Re:  Correct handling of fixed and free variables (Makarius)
>   3.  partial_function: order of variables in induction rule
>      (Andreas Lochbihler)
>   4.  Gource Visualization (Tjark Weber)
>   5. Re:  [Hol-info] Gource Visualization (Michael Norrish)
>   6.  How do I write the sequent |- P in Isar using theorem
>      (Gottfried Barrow)
>   7. Re:  How do I write the sequent |- P in Isar using theorem
>      (Gottfried Barrow)
> 
> 
> ----------------------------------------------------------------------
> 
> Message: 1
> Date: Wed, 26 Jun 2013 08:50:08 +0200
> From: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
> Subject: Re: [isabelle] normalization method introduces schematic type
> 	variables in HOL/Word types
> To: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>
> Cc: isabelle-users <isabelle-users at cl.cam.ac.uk>
> Message-ID: <51CA8F20.7090501 at inf.ethz.ch>
> Content-Type: text/plain; charset="ISO-8859-1"; format=flowed
> 
> Hi Florian,
> 
> Thanks for looking into this.
> 
> On 25/06/13 20:12, Florian Haftmann wrote:
>> An even more minimal example:
>> 
>>> theory Foo
>>> imports "~~/src/HOL/Word/Word"
>>> begin
>>> 
>>> definition
>>>   "example = (1 + 1 :: 4 word)"
>>> 
>>> ML {* Code_Simp.dynamic_value @{theory} @{term example} *}
>>> ML {* Nbe.dynamic_value @{theory} @{term example} *}
> The last line just raises Option (line 81 of General/basics.ML). I got these exceptions 
> quite often, but I thought that I had just done something wrong.
> 
> Andreas
> 
> 
> 
> ------------------------------
> 
> Message: 2
> Date: Thu, 27 Jun 2013 11:52:54 +0200 (CEST)
> From: Makarius <makarius at sketis.net>
> Subject: Re: [isabelle] Correct handling of fixed and free variables
> To: Lars Hupel <hupel at in.tum.de>, Lars Noschinski <noschinl at in.tum.de>
> Cc: cl-isabelle-users at lists.cam.ac.uk
> Message-ID:
> 	<alpine.LNX.2.00.1306271141180.5678 at macbroy21.informatik.tu-muenchen.de>
> 	
> Content-Type: TEXT/PLAIN; format=flowed; charset=US-ASCII
> 
> On Wed, 5 Jun 2013, Lars Noschinski wrote:
> 
>> On 04.06.2013 23:07, Lars Hupel wrote:
>>> To summarize the constraints: I'd like to have a `Proof.context`-aware
>>> term parsing, which works correctly for existing schematic and locally
>>> fixed variables. Lars Noschinski also pointed out that care needs to be
>>> taken of these two different kinds of fixed variables:
>>> 
>>> notepad begin
>>>    { have P sorry } note A = this
>>>    { fix P have P sorry } note B = this
>>> end
>> 
>> These are two separate issues: if we want to use schematic variables 
>> as"holes" in the breakpoint, we need a method, whichv handles both bound and 
>> unbound schematic variables.
>> 
>> If on the other hand we want to use free variables for the holes then there 
>> is this issue which variables are too be generalized.
> 
> The usual way to do the latter is to specify the "eigen context" 
> excplicitly via some 'for' specification.
> 
> The general scheme looks like this:
> 
>   foobar for x y z
> 
> So you augment the local context by additional fixes, read/process foobar 
> (whatever that is exactly), and export the result into the original 
> context.  Thus there will be certain new schematic variables originating 
> from eigen-variables x y z.  This is similar to Pure quantification
> !!x y z. foobar within the language of propositions, but works for 
> arbitrary things within some Proof.context.
> 
> See for example the method "ind_cases" in Isabelle/HOL.  (Note that in 
> Isabelle/jEdit you can hover-click over some proof text that uses it, to 
> get quickly to the ML definition of it.  Or you say 'print_methods' and 
> hover-click over "ind_cases" in its output.)
> 
> 
> 	Makarius
> 
> 
> 
> ------------------------------
> 
> Message: 3
> Date: Fri, 28 Jun 2013 10:29:45 +0200
> From: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
> Subject: [isabelle] partial_function: order of variables in induction
> 	rule
> To: isabelle-users <isabelle-users at cl.cam.ac.uk>
> Message-ID: <51CD4979.2050900 at inf.ethz.ch>
> Content-Type: text/plain; charset="ISO-8859-1"; format=flowed
> 
> I would like to define some set-valued functions whose recursive definition does not 
> terminate. I know that such functions can in principle be defined with inductive_set, but 
> inductive_set does not allow parameters of the function to change in recursive calls (see 
> http://stackoverflow.com/questions/16603886/inductive-set-with-non-fixed-parameters). So I 
> thought I should give partial_function a try, as sets form a ccpo with the standard subset 
> ordering. Setting up partial_function for sets is straightforward, but I am have trouble 
> with the induction rule:
> 
> lemma fixp_induct_set:
>   fixes F :: "'c => 'c"
>   and U :: "'c => 'b => 'a set"
>   and C :: "('b => 'a set) => 'c"
>   and P :: "'b => 'a => bool"
>   assumes mono: "!!x. monotone (fun_ord op <=) op <= (%f. U (F (C f)) x)"
>   and eq: "f == C (ccpo.fixp (fun_lub Sup) (fun_ord op <=) (%f. U (F (C f))))"
>   and inverse2: "!!f. U (C f) = f"
>   and step: "!!f x y. [| y : U (F f) x; !!x y. y : U f x ==> P x y |] ==> P x y"
>   and enforce_variable_ordering: "x = x"
>   and elem: "y : U f x"
>   shows "P x y"
> 
> Note the bogus assumption enforce_variable_ordering. Without it, the variable y occurs 
> before x in the order of variables of the theorem. partial_function then tries to 
> instantiate them in the wrong way and I get a type error. For example:
> 
> partial_function (set) test :: "nat => int set"
> where "test n = {}"
> 
> *** exception THM 0 raised (line 1155 of "thm.ML"):
> *** instantiate: type conflict
> ***   ?y :: int
> ***   n :: nat
> *** [| !!x. monotone (fun_ord op <=) op <= (%f. ?F f x);
> ***  ?f == ccpo.fixp (fun_lub Union) (fun_ord op <=) ?F;
> ***  !!f x y. [|y : ?F f x; !!x y. y : f x ==> ?P x y|] ==> ?P x y; ?y : ?f ?x|]
> *** ==> ?P ?x ?y
> *** At command "partial_function"
> 
> With the superflous assumption enforce_variable_ordering, partial_function accepts the 
> specification. Is this a known limitation of partial_function? Is there some other way to 
> enforce the variable ordering of a theorem or to tell partial_function to instantiate 
> variables in the reversed order?
> 
> Cheers,
> Andreas
> 
> PS: If other people find partial_function for sets useful, I could add the setup to the 
> repository.
> 
> 
> 
> ------------------------------
> 
> Message: 4
> Date: Fri, 28 Jun 2013 15:45:45 +0200
> From: Tjark Weber <webertj at in.tum.de>
> Subject: [isabelle] Gource Visualization
> To: isabelle-users <isabelle-users at cl.cam.ac.uk>
> Message-ID: <1372427145.2134.11.camel at weber>
> Content-Type: text/plain; charset="ISO-8859-1"
> 
> Hi,
> 
> I've used Gource [1] to visualize the development history (as recorded
> in public repository logs) of Coq, HOL4 and Isabelle. Enjoy!
> 
> 14 years of Coq development:
> http://youtu.be/qyM4D6-623A
> 
> 14 years of HOL4 development:
> http://youtu.be/uwLMZFEiQp4
> 
> 20 years of Isabelle development:
> http://youtu.be/tF3ubZlsrsQ
> 
> Best,
> Tjark
> 
> [1] https://code.google.com/p/gource/
> 
> 
> 
> 
> ------------------------------
> 
> Message: 5
> Date: Sat, 29 Jun 2013 15:28:34 +1000
> From: Michael Norrish <michael.norrish at nicta.com.au>
> Subject: Re: [isabelle] [Hol-info] Gource Visualization
> Cc: isabelle-users <isabelle-users at cl.cam.ac.uk>,	hol-info
> 	<hol-info at lists.sourceforge.net>,	coq-club
> 	<coq-club at pauillac.inria.fr>
> Message-ID: <B83D74D4-0B64-41A5-A4F4-166E2BA84642 at nicta.com.au>
> Content-Type: text/plain;	charset=us-ascii
> 
> Cute!
> 
> Michael
> 
> On 28/06/2013, at 23:36, Tjark Weber <tjark.weber at it.uu.se> wrote:
> 
>> Hi,
>> 
>> I've used Gource [1] to visualize the development history (as recorded
>> in public repository logs) of Coq, HOL4 and Isabelle. Enjoy!
>> 
>> 14 years of Coq development:
>> http://youtu.be/qyM4D6-623A
>> 
>> 14 years of HOL4 development:
>> http://youtu.be/uwLMZFEiQp4
>> 
>> 20 years of Isabelle development:
>> http://youtu.be/tF3ubZlsrsQ
>> 
>> Best,
>> Tjark
>> 
>> [1] https://code.google.com/p/gource/
>> 
>> ------------------------------------------------------------------------------
>> This SF.net email is sponsored by Windows:
>> 
>> Build for Windows Store.
>> 
>> http://p.sf.net/sfu/windows-dev2dev
>> _______________________________________________
>> hol-info mailing list
>> hol-info at lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
> 
> 
> 
> ------------------------------
> 
> Message: 6
> Date: Sat, 29 Jun 2013 02:26:56 -0500
> From: Gottfried Barrow <gottfried.barrow at gmx.com>
> Subject: [isabelle] How do I write the sequent |- P in Isar using
> 	theorem
> To: isabelle-users <isabelle-users at cl.cam.ac.uk>
> Message-ID: <51CE8C40.6020808 at gmx.com>
> Content-Type: text/plain; charset=ISO-8859-1; format=flowed
> 
> Hi,
> 
> I'm trying to make some connections between logic vocabulary and Isar.
> 
> From https://en.wikipedia.org/wiki/Sequent, I get the sentence
> 
>    On the other hand an empty antecedent is assumed to be true, i.e.,
>    |- Sigma means that Sigma follows without any assumptions...
> 
> I'm trying to determine the right connection between sequent assumptions 
> and the meta-logic operator "==>", and how to restate a proved theorem 
> with Isar, THM, to accurately represent the sequent ( |- THM).
> 
> Say I have a sequent (A, B |- C), then I'm wanting to say that the 
> following Isar is a correct translation of that sequent:
> 
> theorem
>   assumes A and B
>   shows C
> 
> For any theorem THM I've proved in Isar, I'm trying to trivially restate 
> it as a sequent,  |- THM, but have the restatement have some meaning, 
> not be an exact restatement.
> 
> For example, say I prove this:
> 
> theorem iffIi_1:
>   assumes "A --> B" and "B --> A"
>   shows "A =  B"
> <proof>
> 
> I'd like to restate the theorem using the identifier iffIi_1, but as I 
> said above, I don't know how, so I restate it like this:
> 
> theorem iffIi_2:
>   "(A --> B) ==> (B --> A) ==> (A = B)"
> by(rule iffIi)
> 
> Here, I want to say that this represents the sequent ( |- "(A --> B) ==> 
> (B --> A) ==> (A = B)" ).
> 
> I've been thinking that the statements of iffIi_1 and iffIi_2 must be 
> exactly the same, but now I try the following and it doesn't work:
> 
> theorem
>   assumes "A --> B" and "B --> A"
>   shows "A = B"
> by(rule iffIi)
> 
> I had started thinking  `assumes "A --> B" and "B --> A"` was synonymous 
> with "(A --> B) ==> (B --> A)".
> 
> Regards,
> GB
> 
> 
> 
> 
> 
> ------------------------------
> 
> Message: 7
> Date: Sat, 29 Jun 2013 14:50:38 -0500
> From: Gottfried Barrow <gottfried.barrow at gmx.com>
> Subject: Re: [isabelle] How do I write the sequent |- P in Isar using
> 	theorem
> To: cl-isabelle-users at lists.cam.ac.uk
> Message-ID: <51CF3A8E.7000805 at gmx.com>
> Content-Type: text/plain; charset=ISO-8859-1; format=flowed
> 
> On 6/29/2013 2:26 AM, Gottfried Barrow wrote:
>> Hi,
>> 
>> I'm trying to make some connections between logic vocabulary and Isar.
> 
> Basically, I'm trying to sync up sequents notation with equivalent Isar 
> syntax being used with Isabelle/HOL. I wouldn't care about sequents, but 
> sequents are something that's resorted to a lot in many logic textbooks.
> 
> This is where a textbook would come in handy: "Sequents as Implemented 
> in Isabelle/HOL using Isar Syntax, Along with Many Tedious Examples, 
> Both Trivial and Advanced, and Likewise for Natural Deduction as 
> Implemented in Isar, for the Working Unprofessional."
> 
> It would say, "Here's a sequent, and here's its equivalent form using 
> Isar in Isabelle/HOL. Here's another sequent, but this sequent is 
> difficult to state in Isar. Here's yet another sequent, and you really 
> can't express this sequent in Isar in Isabelle/HOL."
> 
> There's a 3 page section in isar-ref.pdf titled "The sequent caclulus", 
> page 201, which I guess will help me eventually figure it out.
> 
> It says,
> 
>    For certain proofs in classical logic, it can not be called natural.
>    The sequent calculus, a generalization of natural deduction, is
>    easier to automate.
> 
> If Isabelle/HOL is completely formulated as natural deduction, then I 
> guess every Isar statement of Isabelle/HOL can be expressed as a sequent.
> 
> But then on page 203, there's a section titled "Simulating sequents by 
> natural deduction",  and it says,
> 
>    Isabelle can represent sequents directly, as in the object-logic LK.
>    But natural deduction is easier to work with, and most object-logics
>    employ it. Fortunately, we can simulate the sequent P1, ..., Pm |-
>    Q1, ..., Qn by the Isabelle formula P1 ==> ... ==> Pm ==> ~Q2 ==>
>    ... ==> ~Qn ==> Q1 where the order of the assumptions and the choice
>    of Q1 are arbitrary.
> 
> Here, the fact that the word "simulating" is being used, and the use of 
> the phrase "Fortunately, we can simulate the sequent...", makes me think 
> that I can't simulate certain sequents in Isabelle/HOL using Isar.
> 
> Maybe the discussion on page 202 explaining the sequent analogue to the 
> (-->I) will help me figure it out. It gives the rule as
> 
> P, Lambda |- Delta, Q
> --------------------------------- (-->R)
> Lambda |- Delta, P --> Q
> 
> For any proved HOL theorem THM, I'm trying to figure out how to restate 
> THM as a sequent which requires no assumptions, and do it using Isar.
> 
> I start with something trivial:
> 
> theorem TrueTrue:
>   "True"
> by(rule TrueI)
> 
> There doesn't appear to be any assumptions in TrueTrue, but there must 
> be some assumptions because TrueTrue has to be proved by TrueI, which is 
> not an exact restatement of TrueI, where TrueI resorts to using the 
> axiom refl:
> 
> lemma TrueI: "True"
>   unfolding True_def by (rule refl)
> 
> If TrueTrue is a theorem, then I say, "Surely I can express it as a 
> sequent. But what is the sequent, and what is it in Isar?"
> 
> I make an attempt to answer the question, but I use the sequent rule 
> (-->R) as a template.
> 
> I'm tempted to say the sequent is "|- True", but I say it's "|- True, 
> TrueI". In Isar I say the sequent is
> 
> theorem TrueTrue_Restate:
>   "True"
> by(rule TrueTrue)
> 
> So I decide that TrueTrue_Restate is the sequent "|- True, TrueTrue", 
> with there being a subtle difference between "|- True, TrueTrue" and "|- 
> True, TrueI", with the difference being that TrueTrue_Restate is 
> TrueTrue proving itself, which means it's using no assumptions. Using 
> theorem names, it would be "|- TrueTrue, TrueI" versus "|- TrueTrue, 
> TrueTrue_Restate" == "|- TrueTrue".
> 
> But I'm jumping through hoops to try and fit sequent notation with Isar 
> syntax. I'm trying to use "theorem" along with "by" or "proof" to prove 
> that a theorem THM is a sequent of the form "|- P", meaning that it 
> doesn't require any assumptions to be true. If I can do that, it's 
> important. If I can't, it's not important.
> 
> Regards,
> GB
> 
> 
> 
> 
> 
> End of Cl-isabelle-users Digest, Vol 96, Issue 12
> *************************************************





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