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