src/HOL/Modelcheck/MuCalculus.thy
author obua
Sun, 09 May 2004 23:04:36 +0200
changeset 14722 8e739a6eaf11
parent 7295 fe09a0c5cebe
child 17272 c63e5220ed77
permissions -rw-r--r--
replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style

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

MuCalculus = Main +

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