src/HOL/Modelcheck/MuCalculus.thy

tuned;

(*  Title:      HOL/Modelcheck/MuCalculus.thy
    ID:         $Id$
    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
    Copyright   1997  TU Muenchen
*)

theory MuCalculus
imports Main
begin

types
 'a pred = "'a=>bool"

constdefs
  Charfun :: "'a set => 'a pred"
  "Charfun == (% A.% x. x:A)"

  monoP  :: "('a pred => 'a pred) => bool"
  "monoP f == mono(Collect o f o Charfun)"

  mu :: "('a pred => 'a pred) => 'a pred"    (binder "Mu " 10)
  "mu f == Charfun(lfp(Collect o f o Charfun))"

  nu :: "('a pred => 'a pred) => 'a pred"    (binder "Nu " 10)
  "nu f == Charfun(gfp(Collect o f o Charfun))"

ML {* use_legacy_bindings (the_context ()) *}

end