*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] I need a meta-or*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Wed, 31 Jul 2013 20:05:22 -0500*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <alpine.LNX.2.00.1307312226130.12702@macbroy21.informatik.tu-muenchen.de>*References*: <51F19B91.5030107@gmx.com> <alpine.LNX.2.00.1307292218240.7079@lxbroy10.informatik.tu-muenchen.de> <51F91F50.5070901@gmx.com> <alpine.LNX.2.00.1307312226130.12702@macbroy21.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 7/31/2013 3:29 PM, Makarius wrote:

Trueprop priority is 5, so dealing with the syntax of functions oftype "prop => prop" and "prop => prop => prop" is tricky:Trueprop :: "bool => prop" ("(_)" 5)If you want to play with syntax, you can always use 'notation' and'no_notation' to specify things in any way you like, but don't ask meabout suitable priorities -- this is a black art and better notchanged fundamentally.

Generally, Isabelle/Pure is not really a meta-logic, i.e. a logic toreason about other logics. It is just a logical framework, forhigher-order natural deduction based on !! and ==>.If you really want to reason about some other logic, better do it inIsabelle/HOL, and define you syntax as datatype, semantics asfunction, inference system as inductive predicate in the usual way.AFP has examples for that.

Thanks for the help, and thanks to Lars for the info about PROP.

Regards, GB notation ==> (infixr "|-" 4) (* ==> and |-, they're close relatives. *)

(*Warning!! What's below could all be bogus.*)

purity obtained from using "PROP P".

typedecl bool judgment Trueprop :: "bool => prop", though probably also to the arities statements right above them.*) abbreviation MFalse :: "prop" ("MFalse") where "MFalse == (!!P. P::bool)" theorem meta_False: "MFalse == (Trueprop False)" by(rule equal_intr_rule, auto simp only:) (*Meta not.*) abbreviation (input) meta_not_abbr :: "prop => prop" ("([~]_)" 40) where "meta_not_abbr P == (PROP P ==> MFalse)" theorem meta_not: "([~]P) == Trueprop (~P)" by(rule equal_intr_rule, auto simp only:) (*Meta or.*)

"meta_or_abbr P Q == ((PROP P ==> MFalse) ==> PROP Q)" theorem meta_or: "(P [|] Q) == Trueprop (P | Q)" by(rule equal_intr_rule, auto simp only:) (*Meta and.*)

"meta_and_abbr P Q == ((PROP P ==> (PROP Q ==> MFalse)) ==> MFalse)" theorem meta_and: "(P [&] Q) == Trueprop (P & Q)" by(rule equal_intr_rule, auto simp only:)

You do the pencil and paper scratch work 15 times, but because you cannot

rest easy.*) theorem meta_exists: "((!!x. P x ==> MFalse) ==> MFalse) == Trueprop (? x. P x)" by(rule equal_intr_rule, auto simp only:)

that's not HOL disjunction.

The ==> is at priority 1 so the parentheses have to be used as shown.*) theorem " (P,, Q |- (~E ==> ~C ==> ~D ==> B)) == (Q,, P |- E [|] B [|] C [|] D)" by(rule equal_intr_rule, auto simp only:) theorem " (P,, Q |- (~E ==> ~C ==> ~D ==> B)) == (Q,, P |- D [|] E [|] B [|] C)" by(rule equal_intr_rule, auto simp only:)

- Next by Date: Re: [isabelle] I need a meta-or
- Next by Thread: Re: [isabelle] I need a meta-or
- Cl-isabelle-users August 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