equal
deleted
inserted
replaced
|
1 theory Complete_Lattice |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 locale Complete_Lattice = |
|
6 fixes L :: "'a::order set" and Glb :: "'a set \<Rightarrow> 'a" |
|
7 assumes Glb_lower: "A \<subseteq> L \<Longrightarrow> a \<in> A \<Longrightarrow> Glb A \<le> a" |
|
8 and Glb_greatest: "b : L \<Longrightarrow> \<forall>a\<in>A. b \<le> a \<Longrightarrow> b \<le> Glb A" |
|
9 and Glb_in_L: "A \<subseteq> L \<Longrightarrow> Glb A : L" |
|
10 begin |
|
11 |
|
12 definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where |
|
13 "lfp f = Glb {a : L. f a \<le> a}" |
|
14 |
|
15 lemma index_lfp: "lfp f : L" |
|
16 by(auto simp: lfp_def intro: Glb_in_L) |
|
17 |
|
18 lemma lfp_lowerbound: |
|
19 "\<lbrakk> a : L; f a \<le> a \<rbrakk> \<Longrightarrow> lfp f \<le> a" |
|
20 by (auto simp add: lfp_def intro: Glb_lower) |
|
21 |
|
22 lemma lfp_greatest: |
|
23 "\<lbrakk> a : L; \<And>u. \<lbrakk> u : L; f u \<le> u\<rbrakk> \<Longrightarrow> a \<le> u \<rbrakk> \<Longrightarrow> a \<le> lfp f" |
|
24 by (auto simp add: lfp_def intro: Glb_greatest) |
|
25 |
|
26 lemma lfp_unfold: assumes "\<And>x. f x : L \<longleftrightarrow> x : L" |
|
27 and mono: "mono f" shows "lfp f = f (lfp f)" |
|
28 proof- |
|
29 note assms(1)[simp] index_lfp[simp] |
|
30 have 1: "f (lfp f) \<le> lfp f" |
|
31 apply(rule lfp_greatest) |
|
32 apply simp |
|
33 by (blast intro: lfp_lowerbound monoD[OF mono] order_trans) |
|
34 have "lfp f \<le> f (lfp f)" |
|
35 by (fastforce intro: 1 monoD[OF mono] lfp_lowerbound) |
|
36 with 1 show ?thesis by(blast intro: order_antisym) |
|
37 qed |
|
38 |
|
39 end |
|
40 |
|
41 end |
|
42 |