*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] I want to print axiomatization info*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Mon, 09 Jul 2012 14:28:01 -0500*In-reply-to*: <10A31E58-2DD6-4D38-B4DF-789080095575@cam.ac.uk>*References*: <4FF8DFF9.4040304@gmx.com> <9BD4C787-4163-4D60-A87F-D7285EE940DF@cam.ac.uk> <4FF9AA7E.4020902@gmx.com> <10A31E58-2DD6-4D38-B4DF-789080095575@cam.ac.uk>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Larry,

P & Q == !R. ((P--> Q-->R) --> R) == (R = (%x.True)). ((P--> Q-->R) --> R) == (R = (%x.((%y::bool. y) = (%y. y))). ((P--> Q-->R) --> R)

Regards, GB On 7/8/2012 1:12 PM, Lawrence Paulson wrote:

I imagine that the following paper (Church, 1940) has all the information you need: http://www.classes.cs.uchicago.edu/archive/2007/spring/32001-1/papers/church-1940.pdf However, Isabelle's formalism includes a much richer variety of types, including type variables and type constructors. As I recall, essentially the same system of axioms is used in HOL. Larry Paulson On 8 Jul 2012, at 16:42, Gottfried Barrow wrote:I might could eventually figure out the reasoning behind your defs in HOL.thy, like for these: LINE: 178 of src/HOL/HOL.thy defs True_def: "True == ((%x::bool. x) = (%x. x))" All_def: "All(P) == (P = (%x. True))" Ex_def: "Ex(P) == !Q. (!x. P x --> Q) --> Q" False_def: "False == (!P. P)" not_def: "~ P == P-->False" and_def: "P& Q == !R. (P-->Q-->R) --> R" or_def: "P | Q == !R. (P-->R) --> (Q-->R) --> R" Ex1_def: "Ex1(P) == ? x. P(x)& (! y. P(y) --> y=x)" I'm thinking that parts of your "Interactive Proof with Cambridge LCF" and your "The Foundation of a Generic Theorem Prover" will eventually help me out, that you directly implement into HOL.thy some of the logic definitions in your LCF book. It'll take time for me to find that out.

**Follow-Ups**:**Re: [isabelle] I want to print axiomatization info***From:*Lawrence Paulson

**References**:**[isabelle] I want to print axiomatization info***From:*Gottfried Barrow

**Re: [isabelle] I want to print axiomatization info***From:*Lawrence Paulson

**Re: [isabelle] I want to print axiomatization info***From:*Gottfried Barrow

**Re: [isabelle] I want to print axiomatization info***From:*Lawrence Paulson

- Previous by Date: [isabelle] Annotations in Simpl
- Next by Date: Re: [isabelle] I want to print axiomatization info
- Previous by Thread: Re: [isabelle] I want to print axiomatization info
- Next by Thread: Re: [isabelle] I want to print axiomatization info
- Cl-isabelle-users July 2012 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