# Theory MuckeSyn

Up to index of Isabelle/HOL/Modelcheck

theory MuckeSyn
imports MuCalculus
uses mucke_oracle.ML [MuckeSyn.ML]
begin

    (*  Title:      HOL/Modelcheck/MuckeSyn.thy
        ID:         $Id: MuckeSyn.thy,v 1.7 2005/09/06 14:24:55 wenzelm Exp $
        Author:     Tobias Hamberger
        Copyright   1999  TU Muenchen
    *)

    theory MuckeSyn
    imports MuCalculus
    uses "mucke_oracle.ML"
    begin

    (* extended with some operators and case treatment (which requires postprocessing with
    transform_case (from MuCalculus) (TH) *)

    nonterminals
      mutype
      decl decls
      cases_syn case_syn

    syntax (Mucke output)
      True          :: bool                                 ("true")
      False         :: bool                                 ("false")
      Not           :: "bool => bool"                       ("! _" [40] 40)
      If            :: "[bool, 'a, 'a] => 'a"       ("('(if'((_)')/ '((_)')/ else/ '((_)'))')" 10)

      "op &"        :: "[bool, bool] => bool"               (infixr "&" 35)
      "op |"        :: "[bool, bool] => bool"               (infixr "|" 30)
      "op -->"      :: "[bool, bool] => bool"               (infixr "->" 25)
      "op ="        :: "['a, 'a] => bool"                   ("(_ =/ _)" [51, 51] 50)
      "_not_equal"  :: "['a, 'a] => bool"                   ("(_ !=/ _)" [51, 51] 50)

      "ALL "        :: "[idts, bool] => bool"               ("'((3forall _./ _)')" [0, 10] 10)
      "EX "         :: "[idts, bool] => bool"               ("'((3exists _./ _)')" [0, 10] 10)

      "_lambda"     :: "[idts, 'a] => 'b"                   ("(3L _./ _)" 10)
      "_applC"      :: "[('b => 'a), cargs] => aprop"       ("(1_/ '(_'))" [1000,1000] 999)
      "_cargs"      :: "['a, cargs] => cargs"               ("_,/ _" [1000,1000] 1000)

      "_idts"       :: "[idt, idts] => idts"                ("_,/ _" [1, 0] 0)

      "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1_,/ _)")
    (* "@pttrn"     :: "[pttrn, pttrns] => pttrn"           ("_,/ _" [1, 0] 0)
      "_pattern"    :: "[pttrn, patterns] => pttrn"         ("_,/ _" [1, 0] 0) *)

      "_decl"       :: "[mutype,pttrn] => decl"             ("_ _")
      "_decls"      :: "[decl,decls] => decls"              ("_,/ _")
      ""            :: "decl => decls"                      ("_")
      "_mu"         :: "[decl,decls,'a pred] => 'a pred"    ("mu _ '(_') _ ;")
      "_mudec"      :: "[decl,decls] => 'a pred"            ("mu _ '(_') ;")
      "_nu"         :: "[decl,decls,'a pred] => 'a pred"    ("nu _ '(_') _ ;")
      "_nudec"      :: "[decl,decls] => 'a pred"            ("nu _ '(_') ;")
      "_fun"        :: "[decl,decls,'a pred] => 'a pred"    ("_ '(_') _ ;")
      "_dec"        :: "[decl,decls] => 'a pred"            ("_ '(_') ;")

      "_Ex"         :: "[decl,idts,'a pred] => 'a pred"     ("'((3exists _ _./ _)')")
      "_All"        :: "[decl,idts,'a pred] => 'a pred"     ("'((3forall _ _./ _)')")

      "Mu "         :: "[idts, 'a pred] => 'a pred"         ("(3mu _./ _)" 1000)
      "Nu "         :: "[idts, 'a pred] => 'a pred"         ("(3nu _./ _)" 1000)

      "_case_syntax":: "['a, cases_syn] => 'b"              ("(case*_* / _ / esac*)" 10)
      "_case1"      :: "['a, 'b] => case_syn"               ("(2*= _ :/ _;)" 10)
      ""            :: "case_syn => cases_syn"              ("_")
      "_case2"      :: "[case_syn, cases_syn] => cases_syn" ("_/ _")

    (*Terms containing a case statement must be post-processed with the
      ML function transform_case. There, all asterikses before the "="
      will be replaced by the expression between the two asterisks
      following "case" and the asterisk after esac will be deleted *)

    oracle mc_mucke_oracle ("term") =
      mk_mc_mucke_oracle

    end

theorem ext_rl:

      (!!x. f x == g x) ==> f == g

theorem pair_eta_expand:

      f = (%(x, y). f (x, y))