src/HOL/Modelcheck/MuCalculus.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 17272 c63e5220ed77
child 24327 a207114007c6
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     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 ML {* use_legacy_bindings (the_context ()) *}
    28 
    29 end