equal
deleted
inserted
replaced
1 (* Title: HOL/Modelcheck/MuCalculus.thy |
|
2 Author: Olaf Mueller, Jan Philipps, Robert Sandner |
|
3 Copyright 1997 TU Muenchen |
|
4 *) |
|
5 |
|
6 theory MuCalculus |
|
7 imports Main |
|
8 begin |
|
9 |
|
10 types |
|
11 'a pred = "'a=>bool" |
|
12 |
|
13 definition Charfun :: "'a set => 'a pred" where |
|
14 "Charfun == (% A.% x. x:A)" |
|
15 |
|
16 definition monoP :: "('a pred => 'a pred) => bool" where |
|
17 "monoP f == mono(Collect o f o Charfun)" |
|
18 |
|
19 definition mu :: "('a pred => 'a pred) => 'a pred" (binder "Mu " 10) where |
|
20 "mu f == Charfun(lfp(Collect o f o Charfun))" |
|
21 |
|
22 definition nu :: "('a pred => 'a pred) => 'a pred" (binder "Nu " 10) where |
|
23 "nu f == Charfun(gfp(Collect o f o Charfun))" |
|
24 |
|
25 end |
|