Re: [isabelle] I need a meta-or



It's a syntax priority problem.

Trueprop priority is 5, so dealing with the syntax of functions of type "prop => prop" and "prop => prop => prop" is tricky:

   Trueprop :: "bool => prop"   ("(_)" 5)

I haven't figured out the rules completely, but it seems I have what I need.

However, the rules don't make complete sense. For this meta_not_abbr, the function form "meta_not_abbr P" gets a coercion error, but notation with a priority of 40 works, or even 4:

   abbreviation (input) meta_not_abbr :: "prop => prop"  where
      "meta_not_abbr P == (PROP P ==> False)"

   notation meta_not_abbr ("~~~ _" 40)

   theorem
      "meta_not_abbr P" (* coercion error *)

   theorem
      "(~~~ (~~~ P)) == Trueprop (P)"
   by(rule equal_intr_rule, auto simp only:)

I then have my meta_or_abbr. The function form "meta_or_abbr P Q" also gets a coercion error, but infixr notation with priority less than 5 works, and notation ("mOr _ _") also works:

   abbreviation (input) meta_or_abbr :: "prop => prop => prop"  where
      "meta_or_abbr P Q == ((PROP P ==> False) ==> PROP Q)"

   notation
      meta_or_abbr (infixr "+++" 4) and
      meta_or_abbr ("mOr _ _")

   theorem
      "(P +++ Q +++ R) == Trueprop (P | Q | R)"
   by(rule equal_intr_rule, auto simp only:)

   theorem
      "(mOr P Q) == Trueprop (P | Q)"
   by(rule equal_intr_rule, auto simp only:)

   theorem
      "meta_or_abbr P Q" (* coercion error *)

Here are the four connective hybrids. I know why I need one of them:

theorem meta_not:
  "(P ==> False) == Trueprop (~P)"
by(rule equal_intr_rule, auto simp only:)


theorem meta_or:
  "((P ==> False) ==> Q) == Trueprop (P | Q)"
by(rule equal_intr_rule, auto simp only:)


theorem meta_and:
  "((P ==> (Q ==> False)) ==> False) == Trueprop (P & Q)"
by(rule equal_intr_rule, auto simp only:)


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





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