author | paulson <lp15@cam.ac.uk> |
Mon, 30 May 2022 12:46:11 +0100 | |
changeset 75494 | eded3fe9e600 |
parent 68383 | 93a42bd62ede |
child 80914 | d97fdabd9e2b |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Completion.thy |
27404 | 2 |
Author: Brian Huffman |
3 |
*) |
|
4 |
||
62175 | 5 |
section \<open>Defining algebraic domains by ideal completion\<close> |
27404 | 6 |
|
7 |
theory Completion |
|
65380
ae93953746fc
eliminated Plain_HOLCF.thy (see also 8e92772bc0e8): it was modeled after HOL/Plain.thy which was discontinued later;
wenzelm
parents:
65379
diff
changeset
|
8 |
imports Cfun |
27404 | 9 |
begin |
10 |
||
62175 | 11 |
subsection \<open>Ideals over a preorder\<close> |
27404 | 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}" |
|
68383 | 44 |
apply (rule idealI) |
45 |
apply (rule exI [where x = z]) |
|
46 |
apply (fast intro: r_refl) |
|
47 |
apply (rule bexI [where x = z], fast) |
|
48 |
apply (fast intro: r_refl) |
|
49 |
apply (fast intro: r_trans) |
|
50 |
done |
|
27404 | 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 |
|
62175 | 55 |
text \<open>The set of ideals is a cpo\<close> |
27404 | 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)" |
|
68383 | 62 |
apply (rule idealI) |
63 |
using idealD1 [OF ideal_A] apply fast |
|
64 |
apply (clarify) |
|
65 |
subgoal for i j |
|
66 |
apply (drule subsetD [OF chain_A [OF max.cobounded1]]) |
|
67 |
apply (drule subsetD [OF chain_A [OF max.cobounded2]]) |
|
68 |
apply (drule (1) idealD2 [OF ideal_A]) |
|
69 |
apply blast |
|
70 |
done |
|
71 |
apply clarify |
|
72 |
apply (drule (1) idealD3 [OF ideal_A]) |
|
73 |
apply fast |
|
74 |
done |
|
27404 | 75 |
|
76 |
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
|
77 |
fixes Abs :: "'a set \<Rightarrow> 'b::below" |
27404 | 78 |
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
|
79 |
assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y" |
27404 | 80 |
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
|
81 |
apply (intro_classes, unfold below) |
27404 | 82 |
apply (rule subset_refl) |
83 |
apply (erule (1) subset_trans) |
|
84 |
apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) |
|
85 |
apply (erule (1) subset_antisym) |
|
86 |
done |
|
87 |
||
88 |
lemma |
|
89 |
fixes Abs :: "'a set \<Rightarrow> 'b::po" |
|
90 |
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
|
91 |
assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y" |
27404 | 92 |
assumes S: "chain S" |
93 |
shows typedef_ideal_lub: "range S <<| Abs (\<Union>i. Rep (S i))" |
|
40769 | 94 |
and typedef_ideal_rep_lub: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))" |
27404 | 95 |
proof - |
96 |
have 1: "ideal (\<Union>i. Rep (S i))" |
|
97 |
apply (rule ideal_UN) |
|
98 |
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
|
99 |
apply (subst below [symmetric]) |
27404 | 100 |
apply (erule chain_mono [OF S]) |
101 |
done |
|
102 |
hence 2: "Rep (Abs (\<Union>i. Rep (S i))) = (\<Union>i. Rep (S i))" |
|
103 |
by (simp add: type_definition.Abs_inverse [OF type]) |
|
104 |
show 3: "range S <<| Abs (\<Union>i. Rep (S i))" |
|
105 |
apply (rule is_lubI) |
|
106 |
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
|
107 |
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
|
108 |
apply (simp add: below 2 is_ub_def, fast) |
27404 | 109 |
done |
110 |
hence 4: "(\<Squnion>i. S i) = Abs (\<Union>i. Rep (S i))" |
|
40771 | 111 |
by (rule lub_eqI) |
27404 | 112 |
show 5: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))" |
113 |
by (simp add: 4 2) |
|
114 |
qed |
|
115 |
||
116 |
lemma typedef_ideal_cpo: |
|
117 |
fixes Abs :: "'a set \<Rightarrow> 'b::po" |
|
118 |
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
|
119 |
assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y" |
27404 | 120 |
shows "OFCLASS('b, cpo_class)" |
61169 | 121 |
by standard (rule exI, erule typedef_ideal_lub [OF type below]) |
27404 | 122 |
|
123 |
end |
|
124 |
||
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 |
interpretation below: preorder "below :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool" |
27404 | 126 |
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
|
127 |
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
|
128 |
apply (erule (1) below_trans) |
27404 | 129 |
done |
130 |
||
62175 | 131 |
subsection \<open>Lemmas about least upper bounds\<close> |
27404 | 132 |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
133 |
lemma is_ub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> lub S" |
40771 | 134 |
apply (erule exE, drule is_lub_lub) |
27404 | 135 |
apply (drule is_lubD1) |
136 |
apply (erule (1) is_ubD) |
|
137 |
done |
|
138 |
||
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
139 |
lemma is_lub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x" |
40771 | 140 |
by (erule exE, drule is_lub_lub, erule is_lubD2) |
27404 | 141 |
|
65379 | 142 |
|
62175 | 143 |
subsection \<open>Locale for ideal completion\<close> |
28133 | 144 |
|
65379 | 145 |
hide_const (open) Filter.principal |
146 |
||
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
147 |
locale ideal_completion = preorder + |
27404 | 148 |
fixes principal :: "'a::type \<Rightarrow> 'b::cpo" |
149 |
fixes rep :: "'b::cpo \<Rightarrow> 'a::type set" |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
150 |
assumes ideal_rep: "\<And>x. ideal (rep x)" |
40769 | 151 |
assumes rep_lub: "\<And>Y. chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))" |
27404 | 152 |
assumes rep_principal: "\<And>a. rep (principal a) = {b. b \<preceq> a}" |
41033 | 153 |
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
|
154 |
assumes countable: "\<exists>f::'a \<Rightarrow> nat. inj f" |
27404 | 155 |
begin |
156 |
||
28133 | 157 |
lemma rep_mono: "x \<sqsubseteq> y \<Longrightarrow> rep x \<subseteq> rep y" |
158 |
apply (frule bin_chain) |
|
40769 | 159 |
apply (drule rep_lub) |
40771 | 160 |
apply (simp only: lub_eqI [OF is_lub_bin_chain]) |
28133 | 161 |
apply (rule subsetI, rule UN_I [where a=0], simp_all) |
162 |
done |
|
163 |
||
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
|
164 |
lemma below_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y" |
41033 | 165 |
by (rule iffI [OF rep_mono belowI]) |
28133 | 166 |
|
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
|
167 |
lemma principal_below_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x" |
41033 | 168 |
unfolding below_def rep_principal |
169 |
by (auto intro: r_refl elim: idealD3 [OF ideal_rep]) |
|
28133 | 170 |
|
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
|
171 |
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
|
172 |
by (simp add: principal_below_iff_mem_rep rep_principal) |
28133 | 173 |
|
174 |
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
|
175 |
unfolding po_eq_conv [where 'a='b] principal_below_iff .. |
28133 | 176 |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
177 |
lemma eq_iff: "x = y \<longleftrightarrow> rep x = rep y" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
178 |
unfolding po_eq_conv below_def by auto |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
179 |
|
28133 | 180 |
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
|
181 |
by (simp only: principal_below_iff) |
28133 | 182 |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
183 |
lemma ch2ch_principal [simp]: |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
184 |
"\<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
|
185 |
by (simp add: chainI principal_mono) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
186 |
|
62175 | 187 |
subsubsection \<open>Principal ideals approximate all elements\<close> |
39974
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 compact_principal [simp]: "compact (principal a)" |
40769 | 190 |
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
|
191 |
|
62175 | 192 |
text \<open>Construct a chain whose lub is the same as a given ideal\<close> |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
193 |
|
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
194 |
lemma obtain_principal_chain: |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
195 |
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
|
196 |
proof - |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
197 |
obtain count :: "'a \<Rightarrow> nat" where inj: "inj count" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
198 |
using countable .. |
63040 | 199 |
define enum where "enum i = (THE a. count a = i)" for i |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
200 |
have enum_count [simp]: "\<And>x. enum (count x) = x" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
201 |
unfolding enum_def by (simp add: inj_eq [OF inj]) |
63040 | 202 |
define a where "a = (LEAST i. enum i \<in> rep x)" |
203 |
define b where "b i = (LEAST j. enum j \<in> rep x \<and> \<not> enum j \<preceq> enum i)" for i |
|
204 |
define c where "c i j = (LEAST k. enum k \<in> rep x \<and> enum i \<preceq> enum k \<and> enum j \<preceq> enum k)" for i j |
|
205 |
define P where "P i \<longleftrightarrow> (\<exists>j. enum j \<in> rep x \<and> \<not> enum j \<preceq> enum i)" for i |
|
206 |
define X where "X = rec_nat a (\<lambda>n i. if P i then c i (b i) else i)" |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
207 |
have X_0: "X 0 = a" unfolding X_def by simp |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
208 |
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
|
209 |
unfolding X_def by simp |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
210 |
have a_mem: "enum a \<in> rep x" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
211 |
unfolding a_def |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
212 |
apply (rule LeastI_ex) |
68383 | 213 |
apply (insert ideal_rep [of x]) |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
214 |
apply (drule idealD1) |
68383 | 215 |
apply (clarify) |
216 |
subgoal for a by (rule exI [where x="count a"]) simp |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
217 |
done |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
218 |
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
|
219 |
\<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
|
220 |
unfolding P_def b_def by (erule LeastI2_ex, simp) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
221 |
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
|
222 |
\<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
|
223 |
unfolding c_def |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
224 |
apply (drule (1) idealD2 [OF ideal_rep], clarify) |
68383 | 225 |
subgoal for \<dots> z by (rule LeastI2 [where a="count z"], simp, simp) |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
226 |
done |
68383 | 227 |
have X_mem: "enum (X n) \<in> rep x" for n |
228 |
proof (induct n) |
|
229 |
case 0 |
|
230 |
then show ?case by (simp add: X_0 a_mem) |
|
231 |
next |
|
232 |
case (Suc n) |
|
233 |
with b c show ?case by (auto simp: X_Suc) |
|
234 |
qed |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
235 |
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
|
236 |
apply (clarsimp simp add: X_Suc r_refl) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
237 |
apply (simp add: b c X_mem) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
238 |
done |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
239 |
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
|
240 |
unfolding b_def by (drule not_less_Least, simp) |
68383 | 241 |
have X_covers: "\<forall>k\<le>n. enum k \<in> rep x \<longrightarrow> enum k \<preceq> enum (X n)" for n |
242 |
proof (induct n) |
|
243 |
case 0 |
|
244 |
then show ?case |
|
245 |
apply (clarsimp simp add: X_0 a_def) |
|
246 |
apply (drule Least_le [where k=0], simp add: r_refl) |
|
247 |
done |
|
248 |
next |
|
249 |
case (Suc n) |
|
250 |
then show ?case |
|
251 |
apply clarsimp |
|
252 |
apply (erule le_SucE) |
|
253 |
apply (rule r_trans [OF _ X_chain], simp) |
|
254 |
apply (cases "P (X n)", simp add: X_Suc) |
|
255 |
apply (rule linorder_cases [where x="b (X n)" and y="Suc n"]) |
|
256 |
apply (simp only: less_Suc_eq_le) |
|
257 |
apply (drule spec, drule (1) mp, simp add: b X_mem) |
|
258 |
apply (simp add: c X_mem) |
|
259 |
apply (drule (1) less_b) |
|
260 |
apply (erule r_trans) |
|
261 |
apply (simp add: b c X_mem) |
|
262 |
apply (simp add: X_Suc) |
|
263 |
apply (simp add: P_def) |
|
264 |
done |
|
265 |
qed |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
266 |
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
|
267 |
by (simp add: X_chain) |
68383 | 268 |
have "x = (\<Squnion>n. principal (enum (X n)))" |
40769 | 269 |
apply (simp add: eq_iff rep_lub 1 rep_principal) |
68383 | 270 |
apply auto |
271 |
subgoal for a |
|
272 |
apply (subgoal_tac "\<exists>i. a = enum i", erule exE) |
|
273 |
apply (rule_tac x=i in exI, simp add: X_covers) |
|
274 |
apply (rule_tac x="count a" in exI, simp) |
|
275 |
done |
|
276 |
subgoal |
|
277 |
apply (erule idealD3 [OF ideal_rep]) |
|
278 |
apply (rule X_mem) |
|
279 |
done |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
280 |
done |
68383 | 281 |
with 1 show ?thesis .. |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
282 |
qed |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
283 |
|
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
284 |
lemma principal_induct: |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
285 |
assumes adm: "adm P" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
286 |
assumes P: "\<And>a. P (principal a)" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
287 |
shows "P x" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
288 |
apply (rule obtain_principal_chain [of x]) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
289 |
apply (simp add: admD [OF adm] P) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
290 |
done |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
291 |
|
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
292 |
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
|
293 |
apply (rule obtain_principal_chain [of x]) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
294 |
apply (drule adm_compact_neq [OF _ cont_id]) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
295 |
apply (subgoal_tac "chain (\<lambda>i. principal (Y i))") |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
296 |
apply (drule (2) admD2, fast, simp) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
297 |
done |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
298 |
|
62175 | 299 |
subsection \<open>Defining functions in terms of basis elements\<close> |
28133 | 300 |
|
301 |
definition |
|
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
302 |
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
|
303 |
"extension = (\<lambda>f. (\<Lambda> x. lub (f ` rep x)))" |
28133 | 304 |
|
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
305 |
lemma extension_lemma: |
27404 | 306 |
fixes f :: "'a::type \<Rightarrow> 'c::cpo" |
307 |
assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" |
|
308 |
shows "\<exists>u. f ` rep x <<| u" |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
309 |
proof - |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
310 |
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
|
311 |
and x: "x = (\<Squnion>i. principal (Y i))" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
312 |
by (rule obtain_principal_chain [of x]) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
313 |
have chain: "chain (\<lambda>i. f (Y i))" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
314 |
by (rule chainI, simp add: f_mono Y) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
315 |
have rep_x: "rep x = (\<Union>n. {a. a \<preceq> Y n})" |
40769 | 316 |
by (simp add: x rep_lub Y rep_principal) |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
317 |
have "f ` rep x <<| (\<Squnion>n. f (Y n))" |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
318 |
apply (rule is_lubI) |
68383 | 319 |
apply (rule ub_imageI) |
320 |
subgoal for a |
|
321 |
apply (clarsimp simp add: rep_x) |
|
322 |
apply (drule f_mono) |
|
323 |
apply (erule below_lub [OF chain]) |
|
324 |
done |
|
40500
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40002
diff
changeset
|
325 |
apply (rule lub_below [OF chain]) |
68383 | 326 |
subgoal for \<dots> n |
327 |
apply (drule ub_imageD [where x="Y n"]) |
|
328 |
apply (simp add: rep_x, fast intro: r_refl) |
|
329 |
apply assumption |
|
330 |
done |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
331 |
done |
68383 | 332 |
then show ?thesis .. |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
333 |
qed |
27404 | 334 |
|
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
335 |
lemma extension_beta: |
27404 | 336 |
fixes f :: "'a::type \<Rightarrow> 'c::cpo" |
337 |
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
|
338 |
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
|
339 |
unfolding extension_def |
27404 | 340 |
proof (rule beta_cfun) |
341 |
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
|
342 |
using f_mono by (rule extension_lemma) |
27404 | 343 |
show cont: "cont (\<lambda>x. lub (f ` rep x))" |
344 |
apply (rule contI2) |
|
345 |
apply (rule monofunI) |
|
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
346 |
apply (rule is_lub_thelub_ex [OF lub ub_imageI]) |
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
347 |
apply (rule is_ub_thelub_ex [OF lub imageI]) |
27404 | 348 |
apply (erule (1) subsetD [OF rep_mono]) |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
349 |
apply (rule is_lub_thelub_ex [OF lub ub_imageI]) |
40769 | 350 |
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
|
351 |
apply (erule rev_below_trans [OF is_ub_thelub]) |
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset
|
352 |
apply (erule is_ub_thelub_ex [OF lub imageI]) |
27404 | 353 |
done |
354 |
qed |
|
355 |
||
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
356 |
lemma extension_principal: |
27404 | 357 |
fixes f :: "'a::type \<Rightarrow> 'c::cpo" |
358 |
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
|
359 |
shows "extension f\<cdot>(principal a) = f a" |
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
360 |
apply (subst extension_beta, erule f_mono) |
27404 | 361 |
apply (subst rep_principal) |
41033 | 362 |
apply (rule lub_eqI) |
363 |
apply (rule is_lub_maximal) |
|
364 |
apply (rule ub_imageI) |
|
365 |
apply (simp add: f_mono) |
|
366 |
apply (rule imageI) |
|
367 |
apply (simp add: r_refl) |
|
27404 | 368 |
done |
369 |
||
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
370 |
lemma extension_mono: |
27404 | 371 |
assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" |
372 |
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
|
373 |
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
|
374 |
shows "extension f \<sqsubseteq> extension g" |
68383 | 375 |
apply (rule cfun_belowI) |
376 |
apply (simp only: extension_beta f_mono g_mono) |
|
377 |
apply (rule is_lub_thelub_ex) |
|
378 |
apply (rule extension_lemma, erule f_mono) |
|
379 |
apply (rule ub_imageI) |
|
380 |
subgoal for x a |
|
381 |
apply (rule below_trans [OF below]) |
|
382 |
apply (rule is_ub_thelub_ex) |
|
383 |
apply (rule extension_lemma, erule g_mono) |
|
384 |
apply (erule imageI) |
|
385 |
done |
|
386 |
done |
|
27404 | 387 |
|
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
388 |
lemma cont_extension: |
41182 | 389 |
assumes f_mono: "\<And>a b x. a \<preceq> b \<Longrightarrow> f x a \<sqsubseteq> f x b" |
390 |
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
|
391 |
shows "cont (\<lambda>x. extension (\<lambda>a. f x a))" |
41182 | 392 |
apply (rule contI2) |
393 |
apply (rule monofunI) |
|
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
394 |
apply (rule extension_mono, erule f_mono, erule f_mono) |
41182 | 395 |
apply (erule cont2monofunE [OF f_cont]) |
396 |
apply (rule cfun_belowI) |
|
397 |
apply (rule principal_induct, simp) |
|
398 |
apply (simp only: contlub_cfun_fun) |
|
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset
|
399 |
apply (simp only: extension_principal f_mono) |
41182 | 400 |
apply (simp add: cont2contlubE [OF f_cont]) |
401 |
done |
|
402 |
||
27404 | 403 |
end |
404 |
||
39984 | 405 |
lemma (in preorder) typedef_ideal_completion: |
406 |
fixes Abs :: "'a set \<Rightarrow> 'b::cpo" |
|
407 |
assumes type: "type_definition Rep Abs {S. ideal S}" |
|
408 |
assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y" |
|
409 |
assumes principal: "\<And>a. principal a = Abs {b. b \<preceq> a}" |
|
410 |
assumes countable: "\<exists>f::'a \<Rightarrow> nat. inj f" |
|
411 |
shows "ideal_completion r principal Rep" |
|
412 |
proof |
|
413 |
interpret type_definition Rep Abs "{S. ideal S}" by fact |
|
414 |
fix a b :: 'a and x y :: 'b and Y :: "nat \<Rightarrow> 'b" |
|
415 |
show "ideal (Rep x)" |
|
416 |
using Rep [of x] by simp |
|
417 |
show "chain Y \<Longrightarrow> Rep (\<Squnion>i. Y i) = (\<Union>i. Rep (Y i))" |
|
40769 | 418 |
using type below by (rule typedef_ideal_rep_lub) |
39984 | 419 |
show "Rep (principal a) = {b. b \<preceq> a}" |
420 |
by (simp add: principal Abs_inverse ideal_principal) |
|
421 |
show "Rep x \<subseteq> Rep y \<Longrightarrow> x \<sqsubseteq> y" |
|
422 |
by (simp only: below) |
|
423 |
show "\<exists>f::'a \<Rightarrow> nat. inj f" |
|
424 |
by (rule countable) |
|
425 |
qed |
|
426 |
||
27404 | 427 |
end |