equal
deleted
inserted
replaced
9 theory Lfp |
9 theory Lfp |
10 imports Set |
10 imports Set |
11 begin |
11 begin |
12 |
12 |
13 definition |
13 definition |
14 lfp :: "['a set=>'a set] => 'a set" (*least fixed point*) |
14 lfp :: "['a set=>'a set] => 'a set" where -- "least fixed point" |
15 "lfp(f) == Inter({u. f(u) <= u})" |
15 "lfp(f) == Inter({u. f(u) <= u})" |
16 |
16 |
17 (* lfp(f) is the greatest lower bound of {u. f(u) <= u} *) |
17 (* lfp(f) is the greatest lower bound of {u. f(u) <= u} *) |
18 |
18 |
19 lemma lfp_lowerbound: "[| f(A) <= A |] ==> lfp(f) <= A" |
19 lemma lfp_lowerbound: "[| f(A) <= A |] ==> lfp(f) <= A" |