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
     1 (*  Title:      HOL/Modelcheck/MuCalculus.thy
     2     ID:         $Id$
     3     Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     4     Copyright   1997  TU Muenchen
     5 *)
     6 
     7 MuCalculus = Main +
     8 
     9 types
    10  'a pred = "'a=>bool"
    11 
    12 consts
    13 
    14   Charfun :: "'a set => 'a pred"
    15   mu     :: "('a pred => 'a pred) => 'a pred"  (binder "Mu " 10)
    16   nu     :: "('a pred => 'a pred) => 'a pred"  (binder "Nu " 10)
    17   monoP  :: "('a pred => 'a pred) => bool"
    18 
    19 defs
    20 
    21 Charfun_def      "Charfun     == (% A.% x. x:A)"
    22 monoP_def        "monoP f     == mono(Collect o f o Charfun)"
    23 mu_def           "mu f        == Charfun(lfp(Collect o f o Charfun))"
    24 nu_def           "nu f        == Charfun(gfp(Collect o f o Charfun))"
    25 
    26 end