author | haftmann |
Fri, 20 Oct 2017 20:57:55 +0200 | |
changeset 66888 | 930abfdf8727 |
parent 66248 | df85956228c2 |
child 67091 | 1393c2340eec |
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 |
|
60758 | 10 |
section \<open>Greatest Fixpoint (Codatatype) Operation on Bounded Natural Functors\<close> |
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 |
|
66248 | 20 |
alias proj = 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 |
|
49312 | 34 |
lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A" |
57896 | 35 |
by fast |
49312 | 36 |
|
37 |
lemma equiv_proj: |
|
57896 | 38 |
assumes e: "equiv A R" and m: "z \<in> R" |
49312 | 39 |
shows "(proj R o fst) z = (proj R o snd) z" |
40 |
proof - |
|
57896 | 41 |
from m have z: "(fst z, snd z) \<in> R" by auto |
53695 | 42 |
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" |
43 |
unfolding equiv_def sym_def trans_def by blast+ |
|
44 |
then show ?thesis unfolding proj_def[abs_def] by auto |
|
49312 | 45 |
qed |
46 |
||
47 |
(* Operators: *) |
|
48 |
definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}" |
|
49 |
||
51447 | 50 |
lemma Id_on_Gr: "Id_on A = Gr A id" |
57896 | 51 |
unfolding Id_on_def Gr_def by auto |
49312 | 52 |
|
53 |
lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g" |
|
57896 | 54 |
unfolding image2_def by auto |
49312 | 55 |
|
56 |
lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b" |
|
57896 | 57 |
by auto |
49312 | 58 |
|
59 |
lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)" |
|
57896 | 60 |
unfolding image2_def Gr_def by auto |
49312 | 61 |
|
62 |
lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A" |
|
57896 | 63 |
unfolding Gr_def by simp |
49312 | 64 |
|
65 |
lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx" |
|
57896 | 66 |
unfolding Gr_def by simp |
49312 | 67 |
|
61943 | 68 |
lemma Gr_incl: "Gr A f \<subseteq> A \<times> B \<longleftrightarrow> f ` A \<subseteq> B" |
57896 | 69 |
unfolding Gr_def by auto |
49312 | 70 |
|
54485 | 71 |
lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)" |
57896 | 72 |
by blast |
54485 | 73 |
|
74 |
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 | 75 |
by blast |
54485 | 76 |
|
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61032
diff
changeset
|
77 |
lemma in_rel_Collect_case_prod_eq: "in_rel (Collect (case_prod X)) = X" |
57896 | 78 |
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
|
79 |
|
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61032
diff
changeset
|
80 |
lemma Collect_case_prod_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (case_prod (in_rel Y))" |
57896 | 81 |
by auto |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
82 |
|
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61032
diff
changeset
|
83 |
lemma Collect_case_prod_in_rel_leE: "X \<subseteq> Collect (case_prod (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R" |
57896 | 84 |
by force |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
85 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
86 |
lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)" |
57896 | 87 |
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
|
88 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
89 |
lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)" |
57896 | 90 |
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
|
91 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
92 |
lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f" |
57896 | 93 |
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
|
94 |
|
49312 | 95 |
definition relImage where |
57896 | 96 |
"relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}" |
49312 | 97 |
|
98 |
definition relInvImage where |
|
57896 | 99 |
"relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}" |
49312 | 100 |
|
101 |
lemma relImage_Gr: |
|
57896 | 102 |
"\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f" |
103 |
unfolding relImage_def Gr_def relcomp_def by auto |
|
49312 | 104 |
|
105 |
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 | 106 |
unfolding Gr_def relcomp_def image_def relInvImage_def by auto |
49312 | 107 |
|
108 |
lemma relImage_mono: |
|
57896 | 109 |
"R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f" |
110 |
unfolding relImage_def by auto |
|
49312 | 111 |
|
112 |
lemma relInvImage_mono: |
|
57896 | 113 |
"R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f" |
114 |
unfolding relInvImage_def by auto |
|
49312 | 115 |
|
51447 | 116 |
lemma relInvImage_Id_on: |
57896 | 117 |
"(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id" |
118 |
unfolding relInvImage_def Id_on_def by auto |
|
49312 | 119 |
|
120 |
lemma relInvImage_UNIV_relImage: |
|
57896 | 121 |
"R \<subseteq> relInvImage UNIV (relImage R f) f" |
122 |
unfolding relInvImage_def relImage_def by auto |
|
49312 | 123 |
|
124 |
lemma relImage_proj: |
|
57896 | 125 |
assumes "equiv A R" |
126 |
shows "relImage R (proj R) \<subseteq> Id_on (A//R)" |
|
127 |
unfolding relImage_def Id_on_def |
|
128 |
using proj_iff[OF assms] equiv_class_eq_iff[OF assms] |
|
129 |
by (auto simp: proj_preserves) |
|
49312 | 130 |
|
131 |
lemma relImage_relInvImage: |
|
61943 | 132 |
assumes "R \<subseteq> f ` A \<times> f ` A" |
57896 | 133 |
shows "relImage (relInvImage A R f) f = R" |
134 |
using assms unfolding relImage_def relInvImage_def by fast |
|
49312 | 135 |
|
136 |
lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)" |
|
57896 | 137 |
by simp |
49312 | 138 |
|
64413 | 139 |
lemma fst_diag_id: "(fst \<circ> (\<lambda>x. (x, x))) z = id z" by simp |
140 |
lemma snd_diag_id: "(snd \<circ> (\<lambda>x. (x, x))) z = id z" by simp |
|
49312 | 141 |
|
55644 | 142 |
lemma fst_diag_fst: "fst o ((\<lambda>x. (x, x)) o fst) = fst" by auto |
143 |
lemma snd_diag_fst: "snd o ((\<lambda>x. (x, x)) o fst) = fst" by auto |
|
144 |
lemma fst_diag_snd: "fst o ((\<lambda>x. (x, x)) o snd) = snd" by auto |
|
145 |
lemma snd_diag_snd: "snd o ((\<lambda>x. (x, x)) o snd) = snd" by auto |
|
49312 | 146 |
|
147 |
definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}" |
|
148 |
definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}" |
|
149 |
definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))" |
|
150 |
||
151 |
lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k" |
|
57896 | 152 |
unfolding Shift_def Succ_def by simp |
49312 | 153 |
|
154 |
lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl" |
|
57896 | 155 |
unfolding Succ_def by simp |
49312 | 156 |
|
157 |
lemmas SuccE = SuccD[elim_format] |
|
158 |
||
159 |
lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl" |
|
57896 | 160 |
unfolding Succ_def by simp |
49312 | 161 |
|
162 |
lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl" |
|
57896 | 163 |
unfolding Shift_def by simp |
49312 | 164 |
|
165 |
lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)" |
|
57896 | 166 |
unfolding Succ_def Shift_def by auto |
49312 | 167 |
|
168 |
lemma length_Cons: "length (x # xs) = Suc (length xs)" |
|
57896 | 169 |
by simp |
49312 | 170 |
|
171 |
lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)" |
|
57896 | 172 |
by simp |
49312 | 173 |
|
174 |
(*injection into the field of a cardinal*) |
|
175 |
definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r" |
|
176 |
definition "toCard A r \<equiv> SOME f. toCard_pred A r f" |
|
177 |
||
178 |
lemma ex_toCard_pred: |
|
57896 | 179 |
"\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f" |
180 |
unfolding toCard_pred_def |
|
181 |
using card_of_ordLeq[of A "Field r"] |
|
182 |
ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"] |
|
183 |
by blast |
|
49312 | 184 |
|
185 |
lemma toCard_pred_toCard: |
|
186 |
"\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)" |
|
57896 | 187 |
unfolding toCard_def using someI_ex[OF ex_toCard_pred] . |
49312 | 188 |
|
57896 | 189 |
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" |
190 |
using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast |
|
49312 | 191 |
|
192 |
definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k" |
|
193 |
||
194 |
lemma fromCard_toCard: |
|
57896 | 195 |
"\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b" |
196 |
unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj) |
|
49312 | 197 |
|
198 |
lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)" |
|
57896 | 199 |
unfolding Field_card_of csum_def by auto |
49312 | 200 |
|
201 |
lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)" |
|
57896 | 202 |
unfolding Field_card_of csum_def by auto |
49312 | 203 |
|
64413 | 204 |
lemma rec_nat_0_imp: "f = rec_nat f1 (\<lambda>n rec. f2 n rec) \<Longrightarrow> f 0 = f1" |
57896 | 205 |
by auto |
49312 | 206 |
|
64413 | 207 |
lemma rec_nat_Suc_imp: "f = rec_nat f1 (\<lambda>n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)" |
57896 | 208 |
by auto |
49312 | 209 |
|
64413 | 210 |
lemma rec_list_Nil_imp: "f = rec_list f1 (\<lambda>x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1" |
57896 | 211 |
by auto |
49312 | 212 |
|
64413 | 213 |
lemma rec_list_Cons_imp: "f = rec_list f1 (\<lambda>x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)" |
57896 | 214 |
by auto |
49312 | 215 |
|
216 |
lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y" |
|
57896 | 217 |
by simp |
49312 | 218 |
|
52731 | 219 |
definition image2p where |
220 |
"image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)" |
|
221 |
||
55463
942c2153b5b4
register 'Spec_Rules' for new-style (co)datatypes
blanchet
parents:
55415
diff
changeset
|
222 |
lemma image2pI: "R x y \<Longrightarrow> image2p f g R (f x) (g y)" |
52731 | 223 |
unfolding image2p_def by blast |
224 |
||
55463
942c2153b5b4
register 'Spec_Rules' for new-style (co)datatypes
blanchet
parents:
55415
diff
changeset
|
225 |
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 | 226 |
unfolding image2p_def by blast |
227 |
||
55945 | 228 |
lemma rel_fun_iff_geq_image2p: "rel_fun R S f g = (image2p f g R \<le> S)" |
229 |
unfolding rel_fun_def image2p_def by auto |
|
52731 | 230 |
|
55945 | 231 |
lemma rel_fun_image2p: "rel_fun R (image2p f g R) f g" |
232 |
unfolding rel_fun_def image2p_def by auto |
|
52731 | 233 |
|
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
234 |
|
60758 | 235 |
subsection \<open>Equivalence relations, quotients, and Hilbert's choice\<close> |
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
236 |
|
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
237 |
lemma equiv_Eps_in: |
64413 | 238 |
"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (\<lambda>x. x \<in> X) \<in> X" |
57896 | 239 |
apply (rule someI2_ex) |
240 |
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
|
241 |
|
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
242 |
lemma equiv_Eps_preserves: |
57896 | 243 |
assumes ECH: "equiv A r" and X: "X \<in> A//r" |
64413 | 244 |
shows "Eps (\<lambda>x. x \<in> X) \<in> A" |
57896 | 245 |
apply (rule in_mono[rule_format]) |
246 |
using assms apply (rule in_quotient_imp_subset) |
|
247 |
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
|
248 |
|
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
249 |
lemma proj_Eps: |
57896 | 250 |
assumes "equiv A r" and "X \<in> A//r" |
64413 | 251 |
shows "proj r (Eps (\<lambda>x. x \<in> X)) = X" |
57896 | 252 |
unfolding proj_def |
253 |
proof auto |
|
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
254 |
fix x assume x: "x \<in> X" |
64413 | 255 |
thus "(Eps (\<lambda>x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast |
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
256 |
next |
64413 | 257 |
fix x assume "(Eps (\<lambda>x. x \<in> X),x) \<in> r" |
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
258 |
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
|
259 |
qed |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
260 |
|
64413 | 261 |
definition univ where "univ f X == f (Eps (\<lambda>x. x \<in> X))" |
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
262 |
|
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
263 |
lemma univ_commute: |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
264 |
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
|
265 |
shows "(univ f) (proj r x) = f x" |
57896 | 266 |
proof (unfold univ_def) |
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
267 |
have prj: "proj r x \<in> A//r" using x proj_preserves by fast |
64413 | 268 |
hence "Eps (\<lambda>y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast |
269 |
moreover have "proj r (Eps (\<lambda>y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast |
|
270 |
ultimately have "(x, Eps (\<lambda>y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast |
|
271 |
thus "f (Eps (\<lambda>y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce |
|
55022
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
272 |
qed |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
273 |
|
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
274 |
lemma univ_preserves: |
57991
f50b3726266f
don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set
blanchet
parents:
57896
diff
changeset
|
275 |
assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall>x \<in> A. f x \<in> B" |
57896 | 276 |
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
|
277 |
proof |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
278 |
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
|
279 |
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
|
280 |
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
|
281 |
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
|
282 |
qed |
eeba3ba73486
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents:
54841
diff
changeset
|
283 |
|
55062 | 284 |
ML_file "Tools/BNF/bnf_gfp_util.ML" |
285 |
ML_file "Tools/BNF/bnf_gfp_tactics.ML" |
|
286 |
ML_file "Tools/BNF/bnf_gfp.ML" |
|
55538 | 287 |
ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML" |
288 |
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
|
289 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
290 |
end |