3210
|
1 |
(* Title: HOL/Modelcheck/MuCalculus.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Olaf Mueller, Jan Philipps, Robert Sandner
|
|
4 |
Copyright 1997 TU Muenchen
|
|
5 |
*)
|
|
6 |
|
17272
|
7 |
theory MuCalculus
|
|
8 |
imports Main
|
|
9 |
begin
|
3210
|
10 |
|
|
11 |
types
|
7295
|
12 |
'a pred = "'a=>bool"
|
3210
|
13 |
|
17272
|
14 |
constdefs
|
3210
|
15 |
Charfun :: "'a set => 'a pred"
|
17272
|
16 |
"Charfun == (% A.% x. x:A)"
|
|
17 |
|
3210
|
18 |
monoP :: "('a pred => 'a pred) => bool"
|
17272
|
19 |
"monoP f == mono(Collect o f o Charfun)"
|
3210
|
20 |
|
17272
|
21 |
mu :: "('a pred => 'a pred) => 'a pred" (binder "Mu " 10)
|
|
22 |
"mu f == Charfun(lfp(Collect o f o Charfun))"
|
3210
|
23 |
|
17272
|
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 ()) *}
|
3210
|
28 |
|
|
29 |
end
|