src/HOL/Modelcheck/MuckeSyn.thy

added Pure/subgoal.ML;

(*  Title:      HOL/Modelcheck/MuckeSyn.thy
    ID:         $Id$
    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