src/HOL/Modelcheck/MuCalculus.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 7295 fe09a0c5cebe
child 17272 c63e5220ed77
permissions -rw-r--r--
Constant "If" is now local
mueller@3210
     1
(*  Title:      HOL/Modelcheck/MuCalculus.thy
mueller@3210
     2
    ID:         $Id$
mueller@3210
     3
    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
mueller@3210
     4
    Copyright   1997  TU Muenchen
mueller@3210
     5
*)
mueller@3210
     6
wenzelm@7295
     7
MuCalculus = Main +
mueller@3210
     8
mueller@3210
     9
types
wenzelm@7295
    10
 'a pred = "'a=>bool"
mueller@3210
    11
mueller@3210
    12
consts
mueller@3210
    13
mueller@3210
    14
  Charfun :: "'a set => 'a pred"
mueller@3210
    15
  mu     :: "('a pred => 'a pred) => 'a pred"  (binder "Mu " 10)
mueller@3210
    16
  nu     :: "('a pred => 'a pred) => 'a pred"  (binder "Nu " 10)
mueller@3210
    17
  monoP  :: "('a pred => 'a pred) => bool"
mueller@3210
    18
wenzelm@7295
    19
defs
mueller@3210
    20
wenzelm@3842
    21
Charfun_def      "Charfun     == (% A.% x. x:A)"
mueller@3210
    22
monoP_def        "monoP f     == mono(Collect o f o Charfun)"
mueller@3210
    23
mu_def           "mu f        == Charfun(lfp(Collect o f o Charfun))"
mueller@3210
    24
nu_def           "nu f        == Charfun(gfp(Collect o f o Charfun))"
mueller@3210
    25
mueller@3210
    26
end