src/HOL/Modelcheck/MuCalculus.thy

+(*  Title:      HOL/Modelcheck/MuCalculus.thy
+    ID:         $Id$
+    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
+    Copyright   1997  TU Muenchen
+*)
+
+MuCalculus = HOL + Inductive +
+
+types
+ 'a pred = "'a=>bool" 
+
+consts
+
+  Charfun :: "'a set => 'a pred"
+  mu     :: "('a pred => 'a pred) => 'a pred"  (binder "Mu " 10)
+  nu     :: "('a pred => 'a pred) => 'a pred"  (binder "Nu " 10)
+  monoP  :: "('a pred => 'a pred) => bool"
+
+defs 
+
+Charfun_def      "Charfun     == (% A.% x.x:A)"
+monoP_def        "monoP f     == mono(Collect o f o Charfun)"
+mu_def           "mu f        == Charfun(lfp(Collect o f o Charfun))"
+nu_def           "nu f        == Charfun(gfp(Collect o f o Charfun))"
+
+end
+ 
+