src/HOL/Modelcheck/MCSyn.thy
author mueller
Fri, 16 May 1997 15:29:41 +0200
changeset 3210 e80db1660614
child 3692 9f9bcce140ce
permissions -rw-r--r--
Invoking Model Checkers in Isabelle/HOL;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3210
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     1
(*  Title:      HOL/Modelcheck/MCSyn.thy
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     2
    ID:         $Id$
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     3
    Author:     Olaf M"uller, Jan Philipps, Robert Sandner
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     4
    Copyright   1997  TU Muenchen
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     5
*)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     6
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     7
MCSyn = MuCalculus + 
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     8
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     9
syntax (Eindhoven output)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    10
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    11
  True		:: bool					("TRUE")
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    12
  False		:: bool					("FALSE")
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    13
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    14
  Not		:: bool => bool				("NOT _" [40] 40)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    15
  "op &"	:: [bool, bool] => bool			(infixr "AND" 35)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    16
  "op |"	:: [bool, bool] => bool			(infixr "OR" 30)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    17
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    18
  "! " 		:: [idts, bool] => bool			("'((3A _./ _)')" [0, 10] 10)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    19
  "? "		:: [idts, bool] => bool			("'((3E _./ _)')" [0, 10] 10)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    20
  "ALL " 	:: [idts, bool] => bool			("'((3A _./ _)')" [0, 10] 10)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    21
  "EX "		:: [idts, bool] => bool			("'((3E _./ _)')" [0, 10] 10)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    22
   "_lambda"	:: [idts, 'a::logic] => 'b::logic	("(3L _./ _)" 10)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    23
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    24
  "_idts"     	:: [pttrn, idts] => idts		("_,/_" [1, 0] 0)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    25
  "_pttrn"      :: [pttrn, pttrns] => pttrn     	("_,/_" [1, 0] 0)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    26
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    27
  "Mu "		:: [idts, 'a pred] => 'a pred		("(3[mu _./ _])" 1000)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    28
  "Nu "		:: [idts, 'a pred] => 'a pred		("(3[nu _./ _])" 1000)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    29
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    30
oracle
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    31
  mk_mc_oracle
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    32
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    33
end