author | wenzelm |
Tue, 29 Mar 2011 17:47:11 +0200 | |
changeset 42151 | 4da4fc77664b |
parent 41529 | ba60efa2fd08 |
child 54863 | 82acc20ded73 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Completion.thy |
27404 | 2 |
Author: Brian Huffman |
3 |
*) |
|
4 |
||
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
5 |
header {* Defining algebraic domains by ideal completion *} |
27404 | 6 |
|
7 |
theory Completion |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40500
diff
changeset
|
8 |
imports Plain_HOLCF |
27404 | 9 |
begin |
10 |
||
11 |
subsection {* Ideals over a preorder *} |
|
12 |
||
13 |
locale preorder = |
|
14 |
fixes r :: "'a::type \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50) |
|
15 |
assumes r_refl: "x \<preceq> x" |
|
16 |
assumes r_trans: "\<lbrakk>x \<preceq> y; y \<preceq> z\<rbrakk> \<Longrightarrow> x \<preceq> z" |
|
17 |
begin |
|
18 |
||
19 |
definition |
|
20 |
ideal :: "'a set \<Rightarrow> bool" where |
|
21 |
"ideal A = ((\<exists>x. x \<in> A) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<exists>z\<in>A. x \<preceq> z \<and> y \<preceq> z) \<and> |
|
22 |
(\<forall>x y. x \<preceq> y \<longrightarrow> y \<in> A \<longrightarrow> x \<in> A))" |
|
23 |
||
24 |
lemma idealI: |
|
25 |
assumes "\<exists>x. x \<in> A" |
|
26 |
assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. x \<preceq> z \<and> y \<preceq> z" |
|
27 |
assumes "\<And>x y. \<lbrakk>x \<preceq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A" |
|
28 |
shows "ideal A" |
|
41529 | 29 |
unfolding ideal_def using assms by fast |
27404 | 30 |
|
31 |
lemma idealD1: |
|
32 |
"ideal A \<Longrightarrow> \<exists>x. x \<in> A" |
|
33 |
unfolding ideal_def by fast |
|
34 |
||
35 |
lemma idealD2: |
|
36 |
"\<lbrakk>ideal A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. x \<preceq> z \<and> y \<preceq> z" |
|
37 |
unfolding ideal_def by fast |
|
38 |
||
39 |
lemma idealD3: |
|
40 |
"\<lbrakk>ideal A; x \<preceq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A" |
|
41 |
unfolding ideal_def by fast |
|
42 |
||
43 |
lemma ideal_principal: "ideal {x. x \<preceq> z}" |
|
44 |
apply (rule idealI) |
|
45 |
apply (rule_tac x=z in exI) |
|
46 |
apply (fast intro: r_refl) |
|
47 |
apply (rule_tac x=z in bexI, fast) |
|
48 |
apply (fast intro: r_refl) |
|
49 |
apply (fast intro: r_trans) |
|
50 |
done |
|
51 |
||
40888
28cd51cff70c
reformulate lemma preorder.ex_ideal, and use it for typedefs
huffman
parents:
40774
diff
changeset
|
52 |
lemma ex_ideal: "\<exists>A. A \<in> {A. ideal A}" |
28cd51cff70c
reformulate lemma preorder.ex_ideal, and use it for typedefs
huffman
parents:
40774
diff
changeset
|
53 |
by (fast intro: ideal_principal) |
27404 | 54 |
|
55 |
text {* The set of ideals is a cpo *} |
|
56 |
||
57 |
lemma ideal_UN: |
|
58 |
fixes A :: "nat \<Rightarrow> 'a set" |
|
59 |
assumes ideal_A: "\<And>i. ideal (A i)" |
|
60 |
assumes chain_A: "\<And>i j. i \<le> j \<Longrightarrow> A i \<subseteq> A j" |
|
61 |
shows "ideal (\<Union>i. A i)" |
|
62 |
apply (rule idealI) |
|
63 |
apply (cut_tac idealD1 [OF ideal_A], fast) |
|
64 |
apply (clarify, rename_tac i j) |
|
65 |
apply (drule subsetD [OF chain_A [OF le_maxI1]]) |
|
66 |
apply (drule subsetD [OF chain_A [OF le_maxI2]]) |
|
67 |
apply (drule (1) idealD2 [OF ideal_A]) |
|
68 |
apply blast |
|
69 |
apply clarify |
|
70 |
apply (drule (1) idealD3 [OF ideal_A]) |
|
71 |
apply fast |
|
72 |
done |
|
73 |
||
74 |
lemma typedef_ideal_po: |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
75 |
fixes Abs :: "'a set \<Rightarrow> 'b::below" |
27404 | 76 |
assumes type: "type_definition Rep Abs {S. ideal S}" |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
77 |
assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y" |
27404 | 78 |
shows "OFCLASS('b, po_class)" |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
79 |
apply (intro_classes, unfold below) |
27404 | 80 |
apply (rule subset_refl) |
81 |
apply (erule (1) subset_trans) |
|
82 |
apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) |
|
83 |
apply (erule (1) subset_antisym) |
|
84 |
done |
|
85 |
||
86 |
lemma |
|
87 |
fixes Abs :: "'a set \<Rightarrow> 'b::po" |
|
88 |
assumes type: "type_definition Rep Abs {S. ideal S}" |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
89 |
assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y" |
27404 | 90 |
assumes S: "chain S" |
91 |
shows typedef_ideal_lub: "range S <<| Abs (\<Union>i. Rep (S i))" |
|
40769 | 92 |
and typedef_ideal_rep_lub: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))" |
27404 | 93 |
proof - |
94 |
have 1: "ideal (\<Union>i. Rep (S i))" |
|
95 |
apply (rule ideal_UN) |
|
96 |
apply (rule type_definition.Rep [OF type, unfolded mem_Collect_eq]) |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
97 |
apply (subst below [symmetric]) |
27404 | 98 |
apply (erule chain_mono [OF S]) |
99 |
done |
|
100 |
hence 2: "Rep (Abs (\<Union>i. Rep (S i))) = (\<Union>i. Rep (S i))" |
|
101 |
by (simp add: type_definition.Abs_inverse [OF type]) |
|
102 |
show 3: "range S <<| Abs (\<Union>i. Rep (S i))" |
|
103 |
apply (rule is_lubI) |
|
104 |
apply (rule is_ubI) |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
105 |
apply (simp add: below 2, fast) |
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
106 |
apply (simp add: below 2 is_ub_def, fast) |
27404 | 107 |
done |
108 |
hence 4: "(\<Squnion>i. S i) = Abs (\<Union>i. Rep (S i))" |
|
40771 | 109 |
by (rule lub_eqI) |
27404 | 110 |
show 5: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))" |
111 |
by (simp add: 4 2) |
|
112 |
qed |
|
113 |
||
114 |
lemma typedef_ideal_cpo: |
|
115 |
fixes Abs :: "'a set \<Rightarrow> 'b::po" |
|
116 |
assumes type: "type_definition Rep Abs {S. ideal S}" |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
117 |
assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y" |
27404 | 118 |
shows "OFCLASS('b, cpo_class)" |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
119 |
by (default, rule exI, erule typedef_ideal_lub [OF type below]) |
27404 | 120 |
|
121 |
end |
|
122 |
||
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
123 |
interpretation below: preorder "below :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool" |
27404 | 124 |
apply unfold_locales |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
125 |
apply (rule below_refl) |
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
126 |
apply (erule (1) below_trans) |
27404 | 127 |
done |
128 |
||
28133 | 129 |
subsection {* Lemmas about least upper bounds *} |
27404 | 130 |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
131 |
lemma is_ub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> lub S" |
40771 | 132 |
apply (erule exE, drule is_lub_lub) |
27404 | 133 |
apply (drule is_lubD1) |
134 |
apply (erule (1) is_ubD) |
|
135 |
done |
|
136 |
||
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
137 |
lemma is_lub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x" |
40771 | 138 |
by (erule exE, drule is_lub_lub, erule is_lubD2) |
27404 | 139 |
|
28133 | 140 |
subsection {* Locale for ideal completion *} |
141 |
||
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
142 |
locale ideal_completion = preorder + |
27404 | 143 |
fixes principal :: "'a::type \<Rightarrow> 'b::cpo" |
144 |
fixes rep :: "'b::cpo \<Rightarrow> 'a::type set" |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
145 |
assumes ideal_rep: "\<And>x. ideal (rep x)" |
40769 | 146 |
assumes rep_lub: "\<And>Y. chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))" |
27404 | 147 |
assumes rep_principal: "\<And>a. rep (principal a) = {b. b \<preceq> a}" |
41033 | 148 |
assumes belowI: "\<And>x y. rep x \<subseteq> rep y \<Longrightarrow> x \<sqsubseteq> y" |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
149 |
assumes countable: "\<exists>f::'a \<Rightarrow> nat. inj f" |
27404 | 150 |
begin |
151 |
||
28133 | 152 |
lemma rep_mono: "x \<sqsubseteq> y \<Longrightarrow> rep x \<subseteq> rep y" |
153 |
apply (frule bin_chain) |
|
40769 | 154 |
apply (drule rep_lub) |
40771 | 155 |
apply (simp only: lub_eqI [OF is_lub_bin_chain]) |
28133 | 156 |
apply (rule subsetI, rule UN_I [where a=0], simp_all) |
157 |
done |
|
158 |
||
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
159 |
lemma below_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y" |
41033 | 160 |
by (rule iffI [OF rep_mono belowI]) |
28133 | 161 |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
162 |
lemma principal_below_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x" |
41033 | 163 |
unfolding below_def rep_principal |
164 |
by (auto intro: r_refl elim: idealD3 [OF ideal_rep]) |
|
28133 | 165 |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
166 |
lemma principal_below_iff [simp]: "principal a \<sqsubseteq> principal b \<longleftrightarrow> a \<preceq> b" |
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
167 |
by (simp add: principal_below_iff_mem_rep rep_principal) |
28133 | 168 |
|
169 |
lemma principal_eq_iff: "principal a = principal b \<longleftrightarrow> a \<preceq> b \<and> b \<preceq> a" |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
170 |
unfolding po_eq_conv [where 'a='b] principal_below_iff .. |
28133 | 171 |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
172 |
lemma eq_iff: "x = y \<longleftrightarrow> rep x = rep y" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
173 |
unfolding po_eq_conv below_def by auto |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
174 |
|
28133 | 175 |
lemma principal_mono: "a \<preceq> b \<Longrightarrow> principal a \<sqsubseteq> principal b" |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
176 |
by (simp only: principal_below_iff) |
28133 | 177 |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
178 |
lemma ch2ch_principal [simp]: |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
179 |
"\<forall>i. Y i \<preceq> Y (Suc i) \<Longrightarrow> chain (\<lambda>i. principal (Y i))" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
180 |
by (simp add: chainI principal_mono) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
181 |
|
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
182 |
subsubsection {* Principal ideals approximate all elements *} |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
183 |
|
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
184 |
lemma compact_principal [simp]: "compact (principal a)" |
40769 | 185 |
by (rule compactI2, simp add: principal_below_iff_mem_rep rep_lub) |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
186 |
|
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
187 |
text {* Construct a chain whose lub is the same as a given ideal *} |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
188 |
|
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
189 |
lemma obtain_principal_chain: |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
190 |
obtains Y where "\<forall>i. Y i \<preceq> Y (Suc i)" and "x = (\<Squnion>i. principal (Y i))" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
191 |
proof - |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
192 |
obtain count :: "'a \<Rightarrow> nat" where inj: "inj count" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
193 |
using countable .. |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
194 |
def enum \<equiv> "\<lambda>i. THE a. count a = i" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
195 |
have enum_count [simp]: "\<And>x. enum (count x) = x" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
196 |
unfolding enum_def by (simp add: inj_eq [OF inj]) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
197 |
def a \<equiv> "LEAST i. enum i \<in> rep x" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
198 |
def b \<equiv> "\<lambda>i. LEAST j. enum j \<in> rep x \<and> \<not> enum j \<preceq> enum i" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
199 |
def c \<equiv> "\<lambda>i j. LEAST k. enum k \<in> rep x \<and> enum i \<preceq> enum k \<and> enum j \<preceq> enum k" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
200 |
def P \<equiv> "\<lambda>i. \<exists>j. enum j \<in> rep x \<and> \<not> enum j \<preceq> enum i" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
201 |
def X \<equiv> "nat_rec a (\<lambda>n i. if P i then c i (b i) else i)" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
202 |
have X_0: "X 0 = a" unfolding X_def by simp |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
203 |
have X_Suc: "\<And>n. X (Suc n) = (if P (X n) then c (X n) (b (X n)) else X n)" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
204 |
unfolding X_def by simp |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
205 |
have a_mem: "enum a \<in> rep x" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
206 |
unfolding a_def |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
207 |
apply (rule LeastI_ex) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
208 |
apply (cut_tac ideal_rep [of x]) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
209 |
apply (drule idealD1) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
210 |
apply (clarify, rename_tac a) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
211 |
apply (rule_tac x="count a" in exI, simp) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
212 |
done |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
213 |
have b: "\<And>i. P i \<Longrightarrow> enum i \<in> rep x |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
214 |
\<Longrightarrow> enum (b i) \<in> rep x \<and> \<not> enum (b i) \<preceq> enum i" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
215 |
unfolding P_def b_def by (erule LeastI2_ex, simp) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
216 |
have c: "\<And>i j. enum i \<in> rep x \<Longrightarrow> enum j \<in> rep x |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
217 |
\<Longrightarrow> enum (c i j) \<in> rep x \<and> enum i \<preceq> enum (c i j) \<and> enum j \<preceq> enum (c i j)" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
218 |
unfolding c_def |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
219 |
apply (drule (1) idealD2 [OF ideal_rep], clarify) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
220 |
apply (rule_tac a="count z" in LeastI2, simp, simp) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
221 |
done |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
222 |
have X_mem: "\<And>n. enum (X n) \<in> rep x" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
223 |
apply (induct_tac n) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
224 |
apply (simp add: X_0 a_mem) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
225 |
apply (clarsimp simp add: X_Suc, rename_tac n) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
226 |
apply (simp add: b c) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
227 |
done |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
228 |
have X_chain: "\<And>n. enum (X n) \<preceq> enum (X (Suc n))" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
229 |
apply (clarsimp simp add: X_Suc r_refl) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
230 |
apply (simp add: b c X_mem) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
231 |
done |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
232 |
have less_b: "\<And>n i. n < b i \<Longrightarrow> enum n \<in> rep x \<Longrightarrow> enum n \<preceq> enum i" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
233 |
unfolding b_def by (drule not_less_Least, simp) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
234 |
have X_covers: "\<And>n. \<forall>k\<le>n. enum k \<in> rep x \<longrightarrow> enum k \<preceq> enum (X n)" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
235 |
apply (induct_tac n) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
236 |
apply (clarsimp simp add: X_0 a_def) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
237 |
apply (drule_tac k=0 in Least_le, simp add: r_refl) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
238 |
apply (clarsimp, rename_tac n k) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
239 |
apply (erule le_SucE) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
240 |
apply (rule r_trans [OF _ X_chain], simp) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
241 |
apply (case_tac "P (X n)", simp add: X_Suc) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
242 |
apply (rule_tac x="b (X n)" and y="Suc n" in linorder_cases) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
243 |
apply (simp only: less_Suc_eq_le) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
244 |
apply (drule spec, drule (1) mp, simp add: b X_mem) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
245 |
apply (simp add: c X_mem) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
246 |
apply (drule (1) less_b) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
247 |
apply (erule r_trans) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
248 |
apply (simp add: b c X_mem) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
249 |
apply (simp add: X_Suc) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
250 |
apply (simp add: P_def) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
251 |
done |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
252 |
have 1: "\<forall>i. enum (X i) \<preceq> enum (X (Suc i))" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
253 |
by (simp add: X_chain) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
254 |
have 2: "x = (\<Squnion>n. principal (enum (X n)))" |
40769 | 255 |
apply (simp add: eq_iff rep_lub 1 rep_principal) |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
256 |
apply (auto, rename_tac a) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
257 |
apply (subgoal_tac "\<exists>i. a = enum i", erule exE) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
258 |
apply (rule_tac x=i in exI, simp add: X_covers) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
259 |
apply (rule_tac x="count a" in exI, simp) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
260 |
apply (erule idealD3 [OF ideal_rep]) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
261 |
apply (rule X_mem) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
262 |
done |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
263 |
from 1 2 show ?thesis .. |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
264 |
qed |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
265 |
|
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
266 |
lemma principal_induct: |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
267 |
assumes adm: "adm P" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
268 |
assumes P: "\<And>a. P (principal a)" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
269 |
shows "P x" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
270 |
apply (rule obtain_principal_chain [of x]) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
271 |
apply (simp add: admD [OF adm] P) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
272 |
done |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
273 |
|
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
274 |
lemma compact_imp_principal: "compact x \<Longrightarrow> \<exists>a. x = principal a" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
275 |
apply (rule obtain_principal_chain [of x]) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
276 |
apply (drule adm_compact_neq [OF _ cont_id]) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
277 |
apply (subgoal_tac "chain (\<lambda>i. principal (Y i))") |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
278 |
apply (drule (2) admD2, fast, simp) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
279 |
done |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
280 |
|
28133 | 281 |
subsection {* Defining functions in terms of basis elements *} |
282 |
||
283 |
definition |
|
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
284 |
extension :: "('a::type \<Rightarrow> 'c::cpo) \<Rightarrow> 'b \<rightarrow> 'c" where |
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
285 |
"extension = (\<lambda>f. (\<Lambda> x. lub (f ` rep x)))" |
28133 | 286 |
|
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
287 |
lemma extension_lemma: |
27404 | 288 |
fixes f :: "'a::type \<Rightarrow> 'c::cpo" |
289 |
assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" |
|
290 |
shows "\<exists>u. f ` rep x <<| u" |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
291 |
proof - |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
292 |
obtain Y where Y: "\<forall>i. Y i \<preceq> Y (Suc i)" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
293 |
and x: "x = (\<Squnion>i. principal (Y i))" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
294 |
by (rule obtain_principal_chain [of x]) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
295 |
have chain: "chain (\<lambda>i. f (Y i))" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
296 |
by (rule chainI, simp add: f_mono Y) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
297 |
have rep_x: "rep x = (\<Union>n. {a. a \<preceq> Y n})" |
40769 | 298 |
by (simp add: x rep_lub Y rep_principal) |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
299 |
have "f ` rep x <<| (\<Squnion>n. f (Y n))" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
300 |
apply (rule is_lubI) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
301 |
apply (rule ub_imageI, rename_tac a) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
302 |
apply (clarsimp simp add: rep_x) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
303 |
apply (drule f_mono) |
40500
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40002
diff
changeset
|
304 |
apply (erule below_lub [OF chain]) |
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40002
diff
changeset
|
305 |
apply (rule lub_below [OF chain]) |
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40002
diff
changeset
|
306 |
apply (drule_tac x="Y n" in ub_imageD) |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
307 |
apply (simp add: rep_x, fast intro: r_refl) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
308 |
apply assumption |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
309 |
done |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
310 |
thus ?thesis .. |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
311 |
qed |
27404 | 312 |
|
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
313 |
lemma extension_beta: |
27404 | 314 |
fixes f :: "'a::type \<Rightarrow> 'c::cpo" |
315 |
assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" |
|
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
316 |
shows "extension f\<cdot>x = lub (f ` rep x)" |
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
317 |
unfolding extension_def |
27404 | 318 |
proof (rule beta_cfun) |
319 |
have lub: "\<And>x. \<exists>u. f ` rep x <<| u" |
|
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
320 |
using f_mono by (rule extension_lemma) |
27404 | 321 |
show cont: "cont (\<lambda>x. lub (f ` rep x))" |
322 |
apply (rule contI2) |
|
323 |
apply (rule monofunI) |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
324 |
apply (rule is_lub_thelub_ex [OF lub ub_imageI]) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
325 |
apply (rule is_ub_thelub_ex [OF lub imageI]) |
27404 | 326 |
apply (erule (1) subsetD [OF rep_mono]) |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
327 |
apply (rule is_lub_thelub_ex [OF lub ub_imageI]) |
40769 | 328 |
apply (simp add: rep_lub, clarify) |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
329 |
apply (erule rev_below_trans [OF is_ub_thelub]) |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
330 |
apply (erule is_ub_thelub_ex [OF lub imageI]) |
27404 | 331 |
done |
332 |
qed |
|
333 |
||
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
334 |
lemma extension_principal: |
27404 | 335 |
fixes f :: "'a::type \<Rightarrow> 'c::cpo" |
336 |
assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" |
|
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
337 |
shows "extension f\<cdot>(principal a) = f a" |
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
338 |
apply (subst extension_beta, erule f_mono) |
27404 | 339 |
apply (subst rep_principal) |
41033 | 340 |
apply (rule lub_eqI) |
341 |
apply (rule is_lub_maximal) |
|
342 |
apply (rule ub_imageI) |
|
343 |
apply (simp add: f_mono) |
|
344 |
apply (rule imageI) |
|
345 |
apply (simp add: r_refl) |
|
27404 | 346 |
done |
347 |
||
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
348 |
lemma extension_mono: |
27404 | 349 |
assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" |
350 |
assumes g_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> g a \<sqsubseteq> g b" |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
351 |
assumes below: "\<And>a. f a \<sqsubseteq> g a" |
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
352 |
shows "extension f \<sqsubseteq> extension g" |
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39984
diff
changeset
|
353 |
apply (rule cfun_belowI) |
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
354 |
apply (simp only: extension_beta f_mono g_mono) |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
355 |
apply (rule is_lub_thelub_ex) |
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
356 |
apply (rule extension_lemma, erule f_mono) |
27404 | 357 |
apply (rule ub_imageI, rename_tac a) |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
30729
diff
changeset
|
358 |
apply (rule below_trans [OF below]) |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
359 |
apply (rule is_ub_thelub_ex) |
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
360 |
apply (rule extension_lemma, erule g_mono) |
27404 | 361 |
apply (erule imageI) |
362 |
done |
|
363 |
||
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
364 |
lemma cont_extension: |
41182 | 365 |
assumes f_mono: "\<And>a b x. a \<preceq> b \<Longrightarrow> f x a \<sqsubseteq> f x b" |
366 |
assumes f_cont: "\<And>a. cont (\<lambda>x. f x a)" |
|
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
367 |
shows "cont (\<lambda>x. extension (\<lambda>a. f x a))" |
41182 | 368 |
apply (rule contI2) |
369 |
apply (rule monofunI) |
|
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
370 |
apply (rule extension_mono, erule f_mono, erule f_mono) |
41182 | 371 |
apply (erule cont2monofunE [OF f_cont]) |
372 |
apply (rule cfun_belowI) |
|
373 |
apply (rule principal_induct, simp) |
|
374 |
apply (simp only: contlub_cfun_fun) |
|
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
375 |
apply (simp only: extension_principal f_mono) |
41182 | 376 |
apply (simp add: cont2contlubE [OF f_cont]) |
377 |
done |
|
378 |
||
27404 | 379 |
end |
380 |
||
39984 | 381 |
lemma (in preorder) typedef_ideal_completion: |
382 |
fixes Abs :: "'a set \<Rightarrow> 'b::cpo" |
|
383 |
assumes type: "type_definition Rep Abs {S. ideal S}" |
|
384 |
assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y" |
|
385 |
assumes principal: "\<And>a. principal a = Abs {b. b \<preceq> a}" |
|
386 |
assumes countable: "\<exists>f::'a \<Rightarrow> nat. inj f" |
|
387 |
shows "ideal_completion r principal Rep" |
|
388 |
proof |
|
389 |
interpret type_definition Rep Abs "{S. ideal S}" by fact |
|
390 |
fix a b :: 'a and x y :: 'b and Y :: "nat \<Rightarrow> 'b" |
|
391 |
show "ideal (Rep x)" |
|
392 |
using Rep [of x] by simp |
|
393 |
show "chain Y \<Longrightarrow> Rep (\<Squnion>i. Y i) = (\<Union>i. Rep (Y i))" |
|
40769 | 394 |
using type below by (rule typedef_ideal_rep_lub) |
39984 | 395 |
show "Rep (principal a) = {b. b \<preceq> a}" |
396 |
by (simp add: principal Abs_inverse ideal_principal) |
|
397 |
show "Rep x \<subseteq> Rep y \<Longrightarrow> x \<sqsubseteq> y" |
|
398 |
by (simp only: below) |
|
399 |
show "\<exists>f::'a \<Rightarrow> nat. inj f" |
|
400 |
by (rule countable) |
|
401 |
qed |
|
402 |
||
27404 | 403 |
end |