|
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 |
|
|
|
7 |
MuCalculus = HOL + Inductive +
|
|
|
8 |
|
|
|
9 |
types
|
|
|
10 |
'a pred = "'a=>bool"
|
|
|
11 |
|
|
|
12 |
consts
|
|
|
13 |
|
|
|
14 |
Charfun :: "'a set => 'a pred"
|
|
|
15 |
mu :: "('a pred => 'a pred) => 'a pred" (binder "Mu " 10)
|
|
|
16 |
nu :: "('a pred => 'a pred) => 'a pred" (binder "Nu " 10)
|
|
|
17 |
monoP :: "('a pred => 'a pred) => bool"
|
|
|
18 |
|
|
|
19 |
defs
|
|
|
20 |
|
|
3842
|
21 |
Charfun_def "Charfun == (% A.% x. x:A)"
|
|
3210
|
22 |
monoP_def "monoP f == mono(Collect o f o Charfun)"
|
|
|
23 |
mu_def "mu f == Charfun(lfp(Collect o f o Charfun))"
|
|
|
24 |
nu_def "nu f == Charfun(gfp(Collect o f o Charfun))"
|
|
|
25 |
|
|
|
26 |
end
|
|
|
27 |
|
|
|
28 |
|