src/HOL/Modelcheck/MuCalculus.thy
author wenzelm
Thu, 30 Nov 2000 20:04:16 +0100
changeset 10548 e8c774c12105
parent 7295 fe09a0c5cebe
child 17272 c63e5220ed77
permissions -rw-r--r--
'consumes' att;
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/MuCalculus.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 Mueller, 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
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 3842
diff changeset
     7
MuCalculus = Main +
3210
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     8
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
     9
types
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 3842
diff changeset
    10
 'a pred = "'a=>bool"
3210
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    11
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    12
consts
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    13
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    14
  Charfun :: "'a set => 'a pred"
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    15
  mu     :: "('a pred => 'a pred) => 'a pred"  (binder "Mu " 10)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    16
  nu     :: "('a pred => 'a pred) => 'a pred"  (binder "Nu " 10)
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    17
  monoP  :: "('a pred => 'a pred) => bool"
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    18
7295
fe09a0c5cebe quite a lot of tuning an cleanup;
wenzelm
parents: 3842
diff changeset
    19
defs
3210
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    20
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3210
diff changeset
    21
Charfun_def      "Charfun     == (% A.% x. x:A)"
3210
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    22
monoP_def        "monoP f     == mono(Collect o f o Charfun)"
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    23
mu_def           "mu f        == Charfun(lfp(Collect o f o Charfun))"
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    24
nu_def           "nu f        == Charfun(gfp(Collect o f o Charfun))"
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    25
e80db1660614 Invoking Model Checkers in Isabelle/HOL;
mueller
parents:
diff changeset
    26
end