76 apply (rule_tac x="f c" in rev_bexI) |
76 apply (rule_tac x="f c" in rev_bexI) |
77 apply (erule imageI) |
77 apply (erule imageI) |
78 apply (simp add: f) |
78 apply (simp add: f) |
79 done |
79 done |
80 |
80 |
81 lemma adm_ideal: "adm (\<lambda>A. ideal (Rep_cset A))" |
|
82 unfolding ideal_def by (intro adm_lemmas adm_set_lemmas) |
|
83 |
|
84 lemma cpodef_ideal_lemma: |
|
85 "(\<exists>x. x \<in> {S. ideal (Rep_cset S)}) \<and> adm (\<lambda>x. x \<in> {S. ideal (Rep_cset S)})" |
|
86 apply (simp add: adm_ideal) |
|
87 apply (rule exI [where x="Abs_cset {x. x \<preceq> arbitrary}"]) |
|
88 apply (simp add: ideal_principal) |
|
89 done |
|
90 |
|
91 lemma lub_image_principal: |
81 lemma lub_image_principal: |
92 assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y" |
82 assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y" |
93 shows "(\<Squnion>x\<in>{x. x \<preceq> y}. f x) = f y" |
83 shows "(\<Squnion>x\<in>{x. x \<preceq> y}. f x) = f y" |
94 apply (rule thelubI) |
84 apply (rule thelubI) |
95 apply (rule is_lub_maximal) |
85 apply (rule is_lub_maximal) |
96 apply (rule ub_imageI) |
86 apply (rule ub_imageI) |
97 apply (simp add: f) |
87 apply (simp add: f) |
98 apply (rule imageI) |
88 apply (rule imageI) |
99 apply (simp add: r_refl) |
89 apply (simp add: r_refl) |
100 done |
90 done |
|
91 |
|
92 text {* The set of ideals is a cpo *} |
|
93 |
|
94 lemma ideal_UN: |
|
95 fixes A :: "nat \<Rightarrow> 'a set" |
|
96 assumes ideal_A: "\<And>i. ideal (A i)" |
|
97 assumes chain_A: "\<And>i j. i \<le> j \<Longrightarrow> A i \<subseteq> A j" |
|
98 shows "ideal (\<Union>i. A i)" |
|
99 apply (rule idealI) |
|
100 apply (cut_tac idealD1 [OF ideal_A], fast) |
|
101 apply (clarify, rename_tac i j) |
|
102 apply (drule subsetD [OF chain_A [OF le_maxI1]]) |
|
103 apply (drule subsetD [OF chain_A [OF le_maxI2]]) |
|
104 apply (drule (1) idealD2 [OF ideal_A]) |
|
105 apply blast |
|
106 apply clarify |
|
107 apply (drule (1) idealD3 [OF ideal_A]) |
|
108 apply fast |
|
109 done |
|
110 |
|
111 lemma typedef_ideal_po: |
|
112 fixes Abs :: "'a set \<Rightarrow> 'b::sq_ord" |
|
113 assumes type: "type_definition Rep Abs {S. ideal S}" |
|
114 assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y" |
|
115 shows "OFCLASS('b, po_class)" |
|
116 apply (intro_classes, unfold less) |
|
117 apply (rule subset_refl) |
|
118 apply (erule (1) subset_trans) |
|
119 apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) |
|
120 apply (erule (1) subset_antisym) |
|
121 done |
|
122 |
|
123 lemma |
|
124 fixes Abs :: "'a set \<Rightarrow> 'b::po" |
|
125 assumes type: "type_definition Rep Abs {S. ideal S}" |
|
126 assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y" |
|
127 assumes S: "chain S" |
|
128 shows typedef_ideal_lub: "range S <<| Abs (\<Union>i. Rep (S i))" |
|
129 and typedef_ideal_rep_contlub: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))" |
|
130 proof - |
|
131 have 1: "ideal (\<Union>i. Rep (S i))" |
|
132 apply (rule ideal_UN) |
|
133 apply (rule type_definition.Rep [OF type, unfolded mem_Collect_eq]) |
|
134 apply (subst less [symmetric]) |
|
135 apply (erule chain_mono [OF S]) |
|
136 done |
|
137 hence 2: "Rep (Abs (\<Union>i. Rep (S i))) = (\<Union>i. Rep (S i))" |
|
138 by (simp add: type_definition.Abs_inverse [OF type]) |
|
139 show 3: "range S <<| Abs (\<Union>i. Rep (S i))" |
|
140 apply (rule is_lubI) |
|
141 apply (rule is_ubI) |
|
142 apply (simp add: less 2, fast) |
|
143 apply (simp add: less 2 is_ub_def, fast) |
|
144 done |
|
145 hence 4: "(\<Squnion>i. S i) = Abs (\<Union>i. Rep (S i))" |
|
146 by (rule thelubI) |
|
147 show 5: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))" |
|
148 by (simp add: 4 2) |
|
149 qed |
|
150 |
|
151 lemma typedef_ideal_cpo: |
|
152 fixes Abs :: "'a set \<Rightarrow> 'b::po" |
|
153 assumes type: "type_definition Rep Abs {S. ideal S}" |
|
154 assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y" |
|
155 shows "OFCLASS('b, cpo_class)" |
|
156 by (default, rule exI, erule typedef_ideal_lub [OF type less]) |
101 |
157 |
102 end |
158 end |
103 |
159 |
104 interpretation sq_le: preorder ["sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"] |
160 interpretation sq_le: preorder ["sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"] |
105 apply unfold_locales |
161 apply unfold_locales |