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

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

If there's a &&&, then it seems there should be the complete suite ofbasic meta operatorsIn principle you could define all the standard connectives ofIsabelle/HOL in Isabelle/Pure as well, but what is the point?

Makarius,

The purpose of Isabelle/Pure is to provide a framework forhigher-order natural deduction, with declarative rule structureindicated by the connectives !! and ==> (i.e. Minimal Higher-orderLogic). Anything beyond that is not really pure.

theorem "A ==> (B ==> C)" It's only natural that I think I should be able to do: abbreviation imp2 :: "prop => prop => prop" (infixr "=+>" 15) where "imp2 P Q == (P ==> Q)" theorem "A =+> (B =+> C)"

I do this: theorem "(A ==> False) ==> (~A)" using[[simp_trace]] apply(auto simp only:) done The simp trace shows this: [1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM: (A ==> False) ==> ~A [1]Adding rewrite rule "??.unknown": A == True

Regards, GB notation ==> (infixr "|-" 4) abbreviation mFalse :: "prop" ("mFalse") where "mFalse == (!!P Q. P == Q::bool)" abbreviation (input) seqr :: "bool => bool => prop" (infixr "||" 9) where "seqr P Q == ((P ==> mFalse) ==> Q)" abbreviation (input) seql :: "bool => prop => prop" (infixr "|||" 9) where "seql P Q == ((P ==> mFalse) ==> PROP Q)" theorem mF_EQ_False: "mFalse == (Trueprop False)" by(rule equal_intr_rule, metis, presburger) (*3ms with False in abbreviation. 18ms with meta-False used in abbreviation and no mF_EQ_False simp rule. 3ms with meta-False used in abbreviation and simp rule mF_EQ_False.*) theorem " (A |- (~E ==> ~C ==> ~D ==> B)) ==> (A |- (E ||| B ||| C || D))" apply(auto simp only: mF_EQ_False) done theorem meta_not_EQ_not: "(P ==> (!!P Q. P == Q::bool)) == (Trueprop (~P))" apply(simp only: mF_EQ_False not_def) apply(rule equal_intr_rule) by(auto) theorem meta_exists_EQ_exists: "(!!Q. (!!x. P x ==> Q) ==> Q) == (Trueprop (? x. P x))" apply(rule equal_intr_rule) by(auto simp only:)

**References**:**[isabelle] I need a meta-or***From:*Gottfried Barrow

**Re: [isabelle] I need a meta-or***From:*Makarius

- Previous by Date: Re: [isabelle] Replacing COMP
- Next by Date: Re: [isabelle] Replacing COMP
- Previous by Thread: Re: [isabelle] I need a meta-or
- Next by Thread: Re: [isabelle] I need a meta-or
- 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