# [isabelle] I need a meta-or

Hi,

`There's the meta-and, &&&, but I need a meta-or, so I don't have to
``define two meta-or operators to keep from using PROP. After giving a
``summary, I show what I found in pure_thy.ML, but I don't know how to
``make it work.
`
As it is, I have to define two meta-or operators to not have to use PROP:
definition orbb :: "bool ⇒ bool ⇒ prop" (infixr "||" 15) where
"orbb P Q == (!!R. (P ==> R) ==> (Q ==> R) ==> R)"
definition orbp :: "bool ⇒ prop ⇒ prop" (infixr "|||" 15) where
"orbp P Q == (!!R. (P ==> R) ==> (PROP Q ==> R) ==> R)"
(*Life is messy with two operators.*)
theorem
"(A ||| (B || C)) ==> (A | (B | C))"
apply(simp add: orbb_def orbp_def)
by(smt)
(*Life is clean with &&&.*)
theorem
"(A &&& (B &&& C)) ==> (A & (B & C))"
by(linarith)

`If there's a &&&, then it seems there should be the complete suite of
``basic meta operators, along the lines of lines 175 to 183 in HOL.thy.
`
In pure_thy.ML, I found these lines for &&&:
val typ = Simple_Syntax.read_typ;
val prop = Simple_Syntax.read_prop;
val const = Lexicon.mark_const;

`Sign.add_syntax_i [(const "Pure.conjunction", typ "prop => prop =>
``prop", Infixr ("&&&", 2))];
``Sign.add_consts_i [(Binding.name "conjunction", typ "prop => prop =>
``prop", NoSyn)];
`(Global_Theory.add_defs false o map Thm.no_attributes)

`[(Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==>
``B ==> C) ==> C)")];
`Sign.hide_const false "Pure.conjunction";

`I tried to modify them like this to get my meta-or, but I can't make it
``work:
`
ML{*
val typ = Simple_Syntax.read_typ;
val prop = Simple_Syntax.read_prop;
val const = Lexicon.mark_const;

`Sign.add_syntax_i [(const "MFZ.meta_or", typ "prop => prop => prop",
``Infixr ("|||", 2))];
``Sign.add_consts_i [(Binding.name "meta_or", typ "prop => prop => prop",
``NoSyn)];
`(Global_Theory.add_defs false o map Thm.no_attributes)

`[(Binding.name "meta_or_def", prop "(A ||| B) == (!!R::prop. (P ==> R)
``==> (Q ==> R) ==> R)")];
`Sign.hide_const false "MFZ.meta_or";
*}
If anyone can do a quick edit to make that work, I would appreciate it.
Thanks,
GB

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