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
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@17272
     7
theory MuCalculus
wenzelm@17272
     8
imports Main
wenzelm@17272
     9
begin
mueller@3210
    10
mueller@3210
    11
types
wenzelm@7295
    12
 'a pred = "'a=>bool"
mueller@3210
    13
wenzelm@17272
    14
constdefs
mueller@3210
    15
  Charfun :: "'a set => 'a pred"
wenzelm@17272
    16
  "Charfun == (% A.% x. x:A)"
wenzelm@17272
    17
mueller@3210
    18
  monoP  :: "('a pred => 'a pred) => bool"
wenzelm@17272
    19
  "monoP f == mono(Collect o f o Charfun)"
mueller@3210
    20
wenzelm@17272
    21
  mu :: "('a pred => 'a pred) => 'a pred"    (binder "Mu " 10)
wenzelm@17272
    22
  "mu f == Charfun(lfp(Collect o f o Charfun))"
mueller@3210
    23
wenzelm@17272
    24
  nu :: "('a pred => 'a pred) => 'a pred"    (binder "Nu " 10)
wenzelm@17272
    25
  "nu f == Charfun(gfp(Collect o f o Charfun))"
wenzelm@17272
    26
wenzelm@17272
    27
ML {* use_legacy_bindings (the_context ()) *}
mueller@3210
    28
mueller@3210
    29
end