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