author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Mon, 26 Apr 2010 15:14:14 +0200 | |
changeset 36352 | f71978e47cd5 |
parent 35416 | d8d7d1b785af |
permissions | -rw-r--r-- |
3210 | 1 |
(* Title: HOL/Modelcheck/MuCalculus.thy |
2 |
Author: Olaf Mueller, Jan Philipps, Robert Sandner |
|
3 |
Copyright 1997 TU Muenchen |
|
4 |
*) |
|
5 |
||
17272 | 6 |
theory MuCalculus |
7 |
imports Main |
|
8 |
begin |
|
3210 | 9 |
|
10 |
types |
|
7295 | 11 |
'a pred = "'a=>bool" |
3210 | 12 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
24327
diff
changeset
|
13 |
definition Charfun :: "'a set => 'a pred" where |
17272 | 14 |
"Charfun == (% A.% x. x:A)" |
15 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
24327
diff
changeset
|
16 |
definition monoP :: "('a pred => 'a pred) => bool" where |
17272 | 17 |
"monoP f == mono(Collect o f o Charfun)" |
3210 | 18 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
24327
diff
changeset
|
19 |
definition mu :: "('a pred => 'a pred) => 'a pred" (binder "Mu " 10) where |
17272 | 20 |
"mu f == Charfun(lfp(Collect o f o Charfun))" |
3210 | 21 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
24327
diff
changeset
|
22 |
definition nu :: "('a pred => 'a pred) => 'a pred" (binder "Nu " 10) where |
17272 | 23 |
"nu f == Charfun(gfp(Collect o f o Charfun))" |
24 |
||
3210 | 25 |
end |