*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Cl-isabelle-users Digest, Vol 96, Issue 12*From*: Tim Kremann <twkrema at orion.ncsc.mil>*Date*: Mon, 1 Jul 2013 10:10:01 -0400*In-reply-to*: <mailman.35376.1372535461.23908.cl-isabelle-users@lists.cam.ac.uk>*References*: <mailman.35376.1372535461.23908.cl-isabelle-users@lists.cam.ac.uk>

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

- Previous by Date: Re: [isabelle] Question about Sledgehammer
- Next by Date: Re: [isabelle] How do I write the sequent |- P in Isar using theorem
- Previous by Thread: Re: [isabelle] Question about Sledgehammer
- Next by Thread: [isabelle] Remaining uses of DVI files?
- Cl-isabelle-users July 2013 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