author | blanchet |
Thu, 20 Nov 2014 17:29:18 +0100 | |
changeset 59018 | ec8ea2465d2a |
parent 58889 | 5b7a9633cfa8 |
child 60758 | d8d85a8172b5 |
permissions | -rw-r--r-- |
58128 | 1 |
(* Title: HOL/BNF_Greatest_Fixpoint.thy |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
55059 | 3 |
Author: Lorenz Panny, TU Muenchen |
4 |
Author: Jasmin Blanchette, TU Muenchen |
|
57698 | 5 |
Copyright 2012, 2013, 2014 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
|
58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
58128
diff
changeset
|
7 |
Greatest fixpoint (codatatype) operation on bounded natural functors. |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
8 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
|
58889 | 10 |
section {* Greatest Fixpoint (Codatatype) Operation on Bounded Natural Functors *} |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
11 |
|
58128 | 12 |
theory BNF_Greatest_Fixpoint |
13 |
imports BNF_Fixpoint_Base String |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
14 |
keywords |
53310 | 15 |
"codatatype" :: thy_decl and |
53822 | 16 |
"primcorecursive" :: thy_goal and |
17 |
"primcorec" :: thy_decl |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
18 |
begin |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
19 |
|
58826 | 20 |
setup {* Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj} *} |
55024 | 21 |
|
55966 | 22 |
lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
57896 | 23 |
by simp |
55966 | 24 |
|
25 |
lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
|
57896 | 26 |
by (cases s) auto |
55966 | 27 |
|
54485 | 28 |
lemma not_TrueE: "\<not> True \<Longrightarrow> P" |
57896 | 29 |
by (erule notE, rule TrueI) |
54485 | 30 |
|
31 |
lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P" |
|
57896 | 32 |
by fast |
54485 | 33 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55413
diff
changeset
|
34 |
lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x" |
57896 | 35 |
by (auto split: sum.splits) |
49312 | 36 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55413
diff
changeset
|
37 |
lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f" |
57896 | 38 |
apply rule |
39 |
apply (rule ext, force split: sum.split) |
|
40 |
by (rule ext, metis case_sum_o_inj(2)) |
|
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
51447
diff
changeset
|
41 |
|
49312 | 42 |
lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A" |
57896 | 43 |
by fast |
49312 | 44 |
|
45 |
lemma equiv_proj: |
|
57896 | 46 |
assumes e: "equiv A R" and m: "z \<in> R" |
49312 | 47 |
shows "(proj R o fst) z = (proj R o snd) z" |
48 |
proof - |
|
57896 | 49 |
from m have z: "(fst z, snd z) \<in> R" by auto |
53695 | 50 |
with e have "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R" |
51 |
unfolding equiv_def sym_def trans_def by blast+ |
|
52 |
then show ?thesis unfolding proj_def[abs_def] by auto |
|
49312 | 53 |
qed |
54 |
||
55 |
(* Operators: *) |
|
56 |
definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}" |
|
57 |
||
51447 | 58 |
lemma Id_on_Gr: "Id_on A = Gr A id" |
57896 | 59 |
unfolding Id_on_def Gr_def by auto |
49312 | 60 |
|
61 |
lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g" |
|
57896 | 62 |
unfolding image2_def by auto |
49312 | 63 |
|
64 |
lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b" |
|
57896 | 65 |
by auto |
49312 | 66 |
|
67 |
lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)" |
|
57896 | 68 |
unfolding image2_def Gr_def by auto |
49312 | 69 |
|
70 |
lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A" |
|
57896 | 71 |
unfolding Gr_def by simp |
49312 | 72 |
|
73 |
lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx" |
|
57896 | 74 |
unfolding Gr_def by simp |
49312 | 75 |
|
76 |
lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B" |
|
57896 | 77 |
unfolding Gr_def by auto |
49312 | 78 |
|
54485 | 79 |
lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)" |
57896 | 80 |
by blast |
54485 | 81 |
|
82 |
lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})" |
|
57896 | 83 |
by blast |
54485 | 84 |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
85 |
lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X" |
57896 | 86 |
unfolding fun_eq_iff by auto |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
87 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
88 |
lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))" |
57896 | 89 |
by auto |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
90 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
91 |
lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R" |
57896 | 92 |
by force |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
93 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
94 |
lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)" |
57896 | 95 |
unfolding fun_eq_iff by auto |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
96 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
97 |
lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)" |
57896 | 98 |
unfolding fun_eq_iff by auto |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
99 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
100 |
lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f" |
57896 | 101 |
unfolding Gr_def Grp_def fun_eq_iff by auto |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
102 |
|
49312 | 103 |
definition relImage where |
57896 | 104 |
"relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}" |
49312 | 105 |
|
106 |
definition relInvImage where |
|
57896 | 107 |
"relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}" |
49312 | 108 |
|
109 |
lemma relImage_Gr: |
|
57896 | 110 |
"\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f" |
111 |
unfolding relImage_def Gr_def relcomp_def by auto |
|
49312 | 112 |
|
113 |
lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)^-1" |
|
57896 | 114 |
unfolding Gr_def relcomp_def image_def relInvImage_def by auto |
49312 | 115 |
|
116 |
lemma relImage_mono: |
|
57896 | 117 |
"R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f" |
118 |
unfolding relImage_def by auto |
|
49312 | 119 |
|
120 |
lemma relInvImage_mono: |
|
57896 | 121 |
"R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f" |
122 |
unfolding relInvImage_def by auto |
|
49312 | 123 |
|
51447 | 124 |
lemma relInvImage_Id_on: |
57896 | 125 |
"(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id" |
126 |
unfolding relInvImage_def Id_on_def by auto |
|
49312 | 127 |
|
128 |
lemma relInvImage_UNIV_relImage: |
|
57896 | 129 |
"R \<subseteq> relInvImage UNIV (relImage R f) f" |
130 |
unfolding relInvImage_def relImage_def by auto |
|
49312 | 131 |
|
132 |
lemma relImage_proj: |
|
57896 | 133 |
assumes "equiv A R" |
134 |
shows "relImage R (proj R) \<subseteq> Id_on (A//R)" |
|
135 |
unfolding relImage_def Id_on_def |
|
136 |
using proj_iff[OF assms] equiv_class_eq_iff[OF assms] |
|
137 |
by (auto simp: proj_preserves) |
|
49312 | 138 |
|
139 |
lemma relImage_relInvImage: |
|
57896 | 140 |
assumes "R \<subseteq> f ` A <*> f ` A" |
141 |
shows "relImage (relInvImage A R f) f = R" |
|
142 |
using assms unfolding relImage_def relInvImage_def by fast |
|
49312 | 143 |
|
144 |
lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)" |
|
57896 | 145 |
by simp |
49312 | 146 |
|
55644 | 147 |
lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z" by simp |
148 |
lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z" by simp |
|
49312 | 149 |
|
55644 | 150 |
lemma fst_diag_fst: "fst o ((\<lambda>x. (x, x)) o fst) = fst" by auto |
151 |
lemma snd_diag_fst: "snd o ((\<lambda>x. (x, x)) o fst) = fst" by auto |
|
152 |
lemma fst_diag_snd: "fst o ((\<lambda>x. (x, x)) o snd) = snd" by auto |
|
153 |
lemma snd_diag_snd: "snd o ((\<lambda>x. (x, x)) o snd) = snd" by auto |
|
49312 | 154 |
|
155 |
definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}" |
|
156 |
definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}" |
|
157 |
definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))" |
|
158 |
||
159 |
lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k" |
|
57896 | 160 |
unfolding Shift_def Succ_def by simp |
49312 | 161 |
|
162 |
lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl" |
|
57896 | 163 |
unfolding Succ_def by simp |
49312 | 164 |
|
165 |
lemmas SuccE = SuccD[elim_format] |
|
166 |
||
167 |
lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl" |
|
57896 | 168 |
unfolding Succ_def by simp |
49312 | 169 |
|
170 |
lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl" |
|
57896 | 171 |
unfolding Shift_def by simp |
49312 | 172 |
|
173 |
lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)" |
|
57896 | 174 |
unfolding Succ_def Shift_def by auto |
49312 | 175 |
|
176 |
lemma length_Cons: "length (x # xs) = Suc (length xs)" |
|
57896 | 177 |
by simp |
49312 | 178 |
|
179 |
lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)" |
|
57896 | 180 |
by simp |
49312 | 181 |
|
182 |
(*injection into the field of a cardinal*) |
|
183 |
definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r" |
|
184 |
definition "toCard A r \<equiv> SOME f. toCard_pred A r f" |
|
185 |
||
186 |
lemma ex_toCard_pred: |
|
57896 | 187 |
"\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f" |
188 |
unfolding toCard_pred_def |
|
189 |
using card_of_ordLeq[of A "Field r"] |
|
190 |
ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"] |
|
191 |
by blast |
|
49312 | 192 |
|
193 |
lemma toCard_pred_toCard: |
|
194 |
"\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)" |
|
57896 | 195 |
unfolding toCard_def using someI_ex[OF ex_toCard_pred] . |
49312 | 196 |
|
57896 | 197 |
lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> toCard A r x = toCard A r y \<longleftrightarrow> x = y" |
198 |
using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast |
|
49312 | 199 |
|
200 |
definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k" |
|
201 |
||
202 |
lemma fromCard_toCard: |
|
57896 | 203 |
"\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b" |
204 |
unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj) |
|
49312 | 205 |
|
206 |
lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)" |
|
57896 | 207 |
unfolding Field_card_of csum_def by auto |
49312 | 208 |
|
209 |
lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)" |
|
57896 | 210 |
unfolding Field_card_of csum_def by auto |
49312 | 211 |
|
55415 | 212 |
lemma rec_nat_0_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1" |
57896 | 213 |
by auto |
49312 | 214 |
|
55415 | 215 |
lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)" |
57896 | 216 |
by auto |
49312 | 217 |
|
55413
a8e96847523c
adapted theories to '{case,rec}_{list,option}' names
blanchet
parents:
55079
diff
changeset
|
218 |
lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1" |
57896 | 219 |
by auto |
49312 | 220 |
|
55413
a8e96847523c
adapted theories to '{case,rec}_{list,option}' names
blanchet
parents:
55079
diff
changeset
|
221 |
lemma rec_list_Cons_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)" |
57896 | 222 |
by auto |
49312 | 223 |
|
224 |
lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y" |
|
57896 | 225 |
by simp |
49312 | 226 |
|
52731 | 227 |
definition image2p where |
228 |
"image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)" |
|
229 |
||
55463
942c2153b5b4
register 'Spec_Rules' for new-style (co)datatypes
blanchet
parents:
55415
diff
changeset
|
230 |
lemma image2pI: "R x y \<Longrightarrow> image2p f g R (f x) (g y)" |
52731 | 231 |
unfolding image2p_def by blast |
232 |
||
55463
942c2153b5b4
register 'Spec_Rules' for new-style (co)datatypes
blanchet
parents:
55415
diff
changeset
|
233 |
lemma image2pE: "\<lbrakk>image2p f g R fx gy; (\<And>x y. fx = f x \<Longrightarrow> gy = g y \<Longrightarrow> R x y \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P" |
52731 | 234 |
unfolding image2p_def by blast |
235 |
||
55945 | 236 |
lemma rel_fun_iff_geq_image2p: "rel_fun R S f g = (image2p f g R \<le> S)" |
237 |
unfolding rel_fun_def image2p_def by auto |
|
52731 | 238 |
|
55945 | 239 |
lemma rel_fun_image2p: "rel_fun R (image2p f g R) f g" |
240 |
unfolding rel_fun_def image2p_def by auto |
|
52731 | 241 |
|
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
242 |
|
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
243 |
subsection {* Equivalence relations, quotients, and Hilbert's choice *} |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
244 |
|
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
245 |
lemma equiv_Eps_in: |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
246 |
"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X" |
57896 | 247 |
apply (rule someI2_ex) |
248 |
using in_quotient_imp_non_empty by blast |
|
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
249 |
|
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
250 |
lemma equiv_Eps_preserves: |
57896 | 251 |
assumes ECH: "equiv A r" and X: "X \<in> A//r" |
252 |
shows "Eps (%x. x \<in> X) \<in> A" |
|
253 |
apply (rule in_mono[rule_format]) |
|
254 |
using assms apply (rule in_quotient_imp_subset) |
|
255 |
by (rule equiv_Eps_in) (rule assms)+ |
|
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
256 |
|
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
257 |
lemma proj_Eps: |
57896 | 258 |
assumes "equiv A r" and "X \<in> A//r" |
259 |
shows "proj r (Eps (%x. x \<in> X)) = X" |
|
260 |
unfolding proj_def |
|
261 |
proof auto |
|
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
262 |
fix x assume x: "x \<in> X" |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
263 |
thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
264 |
next |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
265 |
fix x assume "(Eps (%x. x \<in> X),x) \<in> r" |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
266 |
thus "x \<in> X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
267 |
qed |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
268 |
|
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
269 |
definition univ where "univ f X == f (Eps (%x. x \<in> X))" |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
270 |
|
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
271 |
lemma univ_commute: |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
272 |
assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A" |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
273 |
shows "(univ f) (proj r x) = f x" |
57896 | 274 |
proof (unfold univ_def) |
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
275 |
have prj: "proj r x \<in> A//r" using x proj_preserves by fast |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
276 |
hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
277 |
moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
278 |
ultimately have "(x, Eps (%y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
279 |
thus "f (Eps (%y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
280 |
qed |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
281 |
|
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
282 |
lemma univ_preserves: |
57991
f50b3726266f
don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set
blanchet
parents:
57896
diff
changeset
|
283 |
assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall>x \<in> A. f x \<in> B" |
57896 | 284 |
shows "\<forall>X \<in> A//r. univ f X \<in> B" |
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
285 |
proof |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
286 |
fix X assume "X \<in> A//r" |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
287 |
then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast |
57991
f50b3726266f
don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set
blanchet
parents:
57896
diff
changeset
|
288 |
hence "univ f X = f x" using ECH RES univ_commute by fastforce |
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
289 |
thus "univ f X \<in> B" using x PRES by simp |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
290 |
qed |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
291 |
|
55062 | 292 |
ML_file "Tools/BNF/bnf_gfp_util.ML" |
293 |
ML_file "Tools/BNF/bnf_gfp_tactics.ML" |
|
294 |
ML_file "Tools/BNF/bnf_gfp.ML" |
|
55538 | 295 |
ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML" |
296 |
ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML" |
|
49309
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset
|
297 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
298 |
end |