[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.