src/HOL/Modelcheck/MuCalculus.thy
author nipkow
Fri Aug 28 18:52:41 2009 +0200 (2009-08-28)
changeset 32436 10cd49e0c067
parent 24327 a207114007c6
child 35416 d8d7d1b785af
permissions -rw-r--r--
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
     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 theory MuCalculus
     8 imports Main
     9 begin
    10 
    11 types
    12  'a pred = "'a=>bool"
    13 
    14 constdefs
    15   Charfun :: "'a set => 'a pred"
    16   "Charfun == (% A.% x. x:A)"
    17 
    18   monoP  :: "('a pred => 'a pred) => bool"
    19   "monoP f == mono(Collect o f o Charfun)"
    20 
    21   mu :: "('a pred => 'a pred) => 'a pred"    (binder "Mu " 10)
    22   "mu f == Charfun(lfp(Collect o f o Charfun))"
    23 
    24   nu :: "('a pred => 'a pred) => 'a pred"    (binder "Nu " 10)
    25   "nu f == Charfun(gfp(Collect o f o Charfun))"
    26 
    27 end