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