src/HOL/Modelcheck/MuckeSyn.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 17272 c63e5220ed77
child 21524 7843e2fd14a9
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     1 (*  Title:      HOL/Modelcheck/MuckeSyn.thy
     2     ID:         $Id$
     3     Author:     Tobias Hamberger
     4     Copyright   1999  TU Muenchen
     5 *)
     6 
     7 theory MuckeSyn
     8 imports MuCalculus
     9 uses "mucke_oracle.ML"
    10 begin
    11 
    12 (* extended with some operators and case treatment (which requires postprocessing with
    13 transform_case (from MuCalculus) (TH) *)
    14 
    15 nonterminals
    16   mutype
    17   decl decls
    18   cases_syn case_syn
    19 
    20 syntax (Mucke output)
    21   True          :: bool                                 ("true")
    22   False         :: bool                                 ("false")
    23   Not           :: "bool => bool"                       ("! _" [40] 40)
    24   If            :: "[bool, 'a, 'a] => 'a"       ("('(if'((_)')/ '((_)')/ else/ '((_)'))')" 10)
    25 
    26   "op &"        :: "[bool, bool] => bool"               (infixr "&" 35)
    27   "op |"        :: "[bool, bool] => bool"               (infixr "|" 30)
    28   "op -->"      :: "[bool, bool] => bool"               (infixr "->" 25)
    29   "op ="        :: "['a, 'a] => bool"                   ("(_ =/ _)" [51, 51] 50)
    30   "_not_equal"  :: "['a, 'a] => bool"                   ("(_ !=/ _)" [51, 51] 50)
    31 
    32   "ALL "        :: "[idts, bool] => bool"               ("'((3forall _./ _)')" [0, 10] 10)
    33   "EX "         :: "[idts, bool] => bool"               ("'((3exists _./ _)')" [0, 10] 10)
    34 
    35   "_lambda"     :: "[idts, 'a] => 'b"                   ("(3L _./ _)" 10)
    36   "_applC"      :: "[('b => 'a), cargs] => aprop"       ("(1_/ '(_'))" [1000,1000] 999)
    37   "_cargs"      :: "['a, cargs] => cargs"               ("_,/ _" [1000,1000] 1000)
    38 
    39   "_idts"       :: "[idt, idts] => idts"                ("_,/ _" [1, 0] 0)
    40 
    41   "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1_,/ _)")
    42 (* "@pttrn"     :: "[pttrn, pttrns] => pttrn"           ("_,/ _" [1, 0] 0)
    43   "_pattern"    :: "[pttrn, patterns] => pttrn"         ("_,/ _" [1, 0] 0) *)
    44 
    45   "_decl"       :: "[mutype,pttrn] => decl"             ("_ _")
    46   "_decls"      :: "[decl,decls] => decls"              ("_,/ _")
    47   ""            :: "decl => decls"                      ("_")
    48   "_mu"         :: "[decl,decls,'a pred] => 'a pred"    ("mu _ '(_') _ ;")
    49   "_mudec"      :: "[decl,decls] => 'a pred"            ("mu _ '(_') ;")
    50   "_nu"         :: "[decl,decls,'a pred] => 'a pred"    ("nu _ '(_') _ ;")
    51   "_nudec"      :: "[decl,decls] => 'a pred"            ("nu _ '(_') ;")
    52   "_fun"        :: "[decl,decls,'a pred] => 'a pred"    ("_ '(_') _ ;")
    53   "_dec"        :: "[decl,decls] => 'a pred"            ("_ '(_') ;")
    54 
    55   "_Ex"         :: "[decl,idts,'a pred] => 'a pred"     ("'((3exists _ _./ _)')")
    56   "_All"        :: "[decl,idts,'a pred] => 'a pred"     ("'((3forall _ _./ _)')")
    57 
    58   "Mu "         :: "[idts, 'a pred] => 'a pred"         ("(3mu _./ _)" 1000)
    59   "Nu "         :: "[idts, 'a pred] => 'a pred"         ("(3nu _./ _)" 1000)
    60 
    61   "_case_syntax":: "['a, cases_syn] => 'b"              ("(case*_* / _ / esac*)" 10)
    62   "_case1"      :: "['a, 'b] => case_syn"               ("(2*= _ :/ _;)" 10)
    63   ""            :: "case_syn => cases_syn"              ("_")
    64   "_case2"      :: "[case_syn, cases_syn] => cases_syn" ("_/ _")
    65 
    66 (*Terms containing a case statement must be post-processed with the
    67   ML function transform_case. There, all asterikses before the "="
    68   will be replaced by the expression between the two asterisks
    69   following "case" and the asterisk after esac will be deleted *)
    70 
    71 oracle mc_mucke_oracle ("term") =
    72   mk_mc_mucke_oracle
    73 
    74 end
    75 
    76