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