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