author | traytel |
Wed, 03 Jul 2013 16:53:27 +0200 | |
changeset 52505 | e62f3fd2035e |
parent 51925 | e3b7917186f1 |
child 52634 | 7c4b56bac189 |
permissions | -rw-r--r-- |
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49328
diff
changeset
|
1 |
(* Title: HOL/BNF/BNF_GFP.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 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
3 |
Copyright 2012 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
4 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
5 |
Greatest fixed point operation on bounded natural functors. |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
7 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
8 |
header {* Greatest Fixed Point Operation on Bounded Natural Functors *} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
theory BNF_GFP |
51850
106afdf5806c
renamed a few FP-related files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries
blanchet
parents:
51804
diff
changeset
|
11 |
imports BNF_FP_Basic Equiv_Relations_More "~~/src/HOL/Library/Sublist" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
12 |
keywords |
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51782
diff
changeset
|
13 |
"codatatype" :: thy_decl |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
14 |
begin |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
15 |
|
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
51447
diff
changeset
|
16 |
lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)" |
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
51447
diff
changeset
|
17 |
unfolding o_def by (auto split: sum.splits) |
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
51447
diff
changeset
|
18 |
|
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
51447
diff
changeset
|
19 |
lemma sum_case_comp_Inl: "sum_case f g \<circ> Inl = f" |
49312 | 20 |
unfolding comp_def by simp |
21 |
||
22 |
lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x" |
|
23 |
by (auto split: sum.splits) |
|
24 |
||
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
51447
diff
changeset
|
25 |
lemma sum_case_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> sum_case g h = f" |
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
51447
diff
changeset
|
26 |
by (metis sum_case_comp_Inl sum_case_o_inj(2) surjective_sum) |
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
51447
diff
changeset
|
27 |
|
49312 | 28 |
lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A" |
29 |
by auto |
|
30 |
||
31 |
lemma equiv_triv1: |
|
32 |
assumes "equiv A R" and "(a, b) \<in> R" and "(a, c) \<in> R" |
|
33 |
shows "(b, c) \<in> R" |
|
34 |
using assms unfolding equiv_def sym_def trans_def by blast |
|
35 |
||
36 |
lemma equiv_triv2: |
|
37 |
assumes "equiv A R" and "(a, b) \<in> R" and "(b, c) \<in> R" |
|
38 |
shows "(a, c) \<in> R" |
|
39 |
using assms unfolding equiv_def trans_def by blast |
|
40 |
||
41 |
lemma equiv_proj: |
|
42 |
assumes e: "equiv A R" and "z \<in> R" |
|
43 |
shows "(proj R o fst) z = (proj R o snd) z" |
|
44 |
proof - |
|
45 |
from assms(2) have z: "(fst z, snd z) \<in> R" by auto |
|
46 |
have P: "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" by (erule equiv_triv1[OF e z]) |
|
47 |
have "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R" by (erule equiv_triv2[OF e z]) |
|
48 |
with P show ?thesis unfolding proj_def[abs_def] by auto |
|
49 |
qed |
|
50 |
||
51 |
(* Operators: *) |
|
52 |
definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}" |
|
53 |
||
54 |
||
51447 | 55 |
lemma Id_onD: "(a, b) \<in> Id_on A \<Longrightarrow> a = b" |
56 |
unfolding Id_on_def by simp |
|
49312 | 57 |
|
51447 | 58 |
lemma Id_onD': "x \<in> Id_on A \<Longrightarrow> fst x = snd x" |
59 |
unfolding Id_on_def by auto |
|
49312 | 60 |
|
51447 | 61 |
lemma Id_on_fst: "x \<in> Id_on A \<Longrightarrow> fst x \<in> A" |
62 |
unfolding Id_on_def by auto |
|
49312 | 63 |
|
51447 | 64 |
lemma Id_on_UNIV: "Id_on UNIV = Id" |
65 |
unfolding Id_on_def by auto |
|
49312 | 66 |
|
51447 | 67 |
lemma Id_on_Comp: "Id_on A = Id_on A O Id_on A" |
68 |
unfolding Id_on_def by auto |
|
49312 | 69 |
|
51447 | 70 |
lemma Id_on_Gr: "Id_on A = Gr A id" |
71 |
unfolding Id_on_def Gr_def by auto |
|
49312 | 72 |
|
51447 | 73 |
lemma Id_on_UNIV_I: "x = y \<Longrightarrow> (x, y) \<in> Id_on UNIV" |
74 |
unfolding Id_on_def by auto |
|
49312 | 75 |
|
76 |
lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g" |
|
77 |
unfolding image2_def by auto |
|
78 |
||
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
79 |
lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)" |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
80 |
by auto |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
81 |
|
49312 | 82 |
lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b" |
83 |
by auto |
|
84 |
||
85 |
lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)" |
|
86 |
unfolding image2_def Gr_def by auto |
|
87 |
||
88 |
lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A" |
|
89 |
unfolding Gr_def by simp |
|
90 |
||
91 |
lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx" |
|
92 |
unfolding Gr_def by simp |
|
93 |
||
94 |
lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B" |
|
95 |
unfolding Gr_def by auto |
|
96 |
||
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
97 |
lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X" |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
98 |
unfolding fun_eq_iff by auto |
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 Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))" |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
101 |
by auto |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
102 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
103 |
lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R" |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
104 |
by force |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
105 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
106 |
lemma Collect_split_in_relI: "x \<in> X \<Longrightarrow> x \<in> Collect (split (in_rel X))" |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
107 |
by auto |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
108 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
109 |
lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)" |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
110 |
unfolding fun_eq_iff by auto |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
111 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
112 |
lemmas conversep_in_rel_Id_on = |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
113 |
trans[OF conversep_in_rel arg_cong[of _ _ in_rel, OF converse_Id_on]] |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
114 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
115 |
lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)" |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
116 |
unfolding fun_eq_iff by auto |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
117 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
118 |
lemmas relcompp_in_rel_Id_on = |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
119 |
trans[OF relcompp_in_rel arg_cong[of _ _ in_rel, OF Id_on_Comp[symmetric]]] |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
120 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
121 |
lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f" |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
122 |
unfolding Gr_def Grp_def fun_eq_iff by auto |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
123 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
124 |
lemma in_rel_Id_on_UNIV: "in_rel (Id_on UNIV) = op =" |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
125 |
unfolding fun_eq_iff by auto |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51850
diff
changeset
|
126 |
|
49312 | 127 |
definition relImage where |
128 |
"relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}" |
|
129 |
||
130 |
definition relInvImage where |
|
131 |
"relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}" |
|
132 |
||
133 |
lemma relImage_Gr: |
|
134 |
"\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f" |
|
135 |
unfolding relImage_def Gr_def relcomp_def by auto |
|
136 |
||
137 |
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" |
|
138 |
unfolding Gr_def relcomp_def image_def relInvImage_def by auto |
|
139 |
||
140 |
lemma relImage_mono: |
|
141 |
"R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f" |
|
142 |
unfolding relImage_def by auto |
|
143 |
||
144 |
lemma relInvImage_mono: |
|
145 |
"R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f" |
|
146 |
unfolding relInvImage_def by auto |
|
147 |
||
51447 | 148 |
lemma relInvImage_Id_on: |
149 |
"(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id" |
|
150 |
unfolding relInvImage_def Id_on_def by auto |
|
49312 | 151 |
|
152 |
lemma relInvImage_UNIV_relImage: |
|
153 |
"R \<subseteq> relInvImage UNIV (relImage R f) f" |
|
154 |
unfolding relInvImage_def relImage_def by auto |
|
155 |
||
156 |
lemma equiv_Image: "equiv A R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> a \<in> A \<and> b \<in> A \<and> R `` {a} = R `` {b})" |
|
157 |
unfolding equiv_def refl_on_def Image_def by (auto intro: transD symD) |
|
158 |
||
159 |
lemma relImage_proj: |
|
160 |
assumes "equiv A R" |
|
51447 | 161 |
shows "relImage R (proj R) \<subseteq> Id_on (A//R)" |
162 |
unfolding relImage_def Id_on_def |
|
163 |
using proj_iff[OF assms] equiv_class_eq_iff[OF assms] |
|
164 |
by (auto simp: proj_preserves) |
|
49312 | 165 |
|
166 |
lemma relImage_relInvImage: |
|
167 |
assumes "R \<subseteq> f ` A <*> f ` A" |
|
168 |
shows "relImage (relInvImage A R f) f = R" |
|
169 |
using assms unfolding relImage_def relInvImage_def by fastforce |
|
170 |
||
171 |
lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)" |
|
172 |
by simp |
|
173 |
||
174 |
lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z" |
|
175 |
by simp |
|
176 |
||
177 |
lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z" |
|
178 |
by simp |
|
179 |
||
180 |
lemma Collect_restrict': "{(x, y) | x y. phi x y \<and> P x y} \<subseteq> {(x, y) | x y. phi x y}" |
|
181 |
by auto |
|
182 |
||
183 |
lemma image_convolD: "\<lbrakk>(a, b) \<in> <f, g> ` X\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> X \<and> a = f x \<and> b = g x" |
|
184 |
unfolding convol_def by auto |
|
185 |
||
186 |
(*Extended Sublist*) |
|
187 |
||
188 |
definition prefCl where |
|
50058
bb1fadeba35e
import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
traytel
parents:
49635
diff
changeset
|
189 |
"prefCl Kl = (\<forall> kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)" |
49312 | 190 |
definition PrefCl where |
50058
bb1fadeba35e
import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
traytel
parents:
49635
diff
changeset
|
191 |
"PrefCl A n = (\<forall>kl kl'. kl \<in> A n \<and> prefixeq kl' kl \<longrightarrow> (\<exists>m\<le>n. kl' \<in> A m))" |
49312 | 192 |
|
193 |
lemma prefCl_UN: |
|
194 |
"\<lbrakk>\<And>n. PrefCl A n\<rbrakk> \<Longrightarrow> prefCl (\<Union>n. A n)" |
|
195 |
unfolding prefCl_def PrefCl_def by fastforce |
|
196 |
||
197 |
definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}" |
|
198 |
definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}" |
|
199 |
definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))" |
|
200 |
||
201 |
lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k" |
|
202 |
unfolding Shift_def Succ_def by simp |
|
203 |
||
204 |
lemma Shift_clists: "Kl \<subseteq> Field (clists r) \<Longrightarrow> Shift Kl k \<subseteq> Field (clists r)" |
|
205 |
unfolding Shift_def clists_def Field_card_of by auto |
|
206 |
||
207 |
lemma Shift_prefCl: "prefCl Kl \<Longrightarrow> prefCl (Shift Kl k)" |
|
208 |
unfolding prefCl_def Shift_def |
|
209 |
proof safe |
|
210 |
fix kl1 kl2 |
|
50058
bb1fadeba35e
import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
traytel
parents:
49635
diff
changeset
|
211 |
assume "\<forall>kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl" |
bb1fadeba35e
import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
traytel
parents:
49635
diff
changeset
|
212 |
"prefixeq kl1 kl2" "k # kl2 \<in> Kl" |
bb1fadeba35e
import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
traytel
parents:
49635
diff
changeset
|
213 |
thus "k # kl1 \<in> Kl" using Cons_prefixeq_Cons[of k kl1 k kl2] by blast |
49312 | 214 |
qed |
215 |
||
216 |
lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl" |
|
217 |
unfolding Shift_def by simp |
|
218 |
||
219 |
lemma prefCl_Succ: "\<lbrakk>prefCl Kl; k # kl \<in> Kl\<rbrakk> \<Longrightarrow> k \<in> Succ Kl []" |
|
220 |
unfolding Succ_def proof |
|
221 |
assume "prefCl Kl" "k # kl \<in> Kl" |
|
50058
bb1fadeba35e
import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
traytel
parents:
49635
diff
changeset
|
222 |
moreover have "prefixeq (k # []) (k # kl)" by auto |
49312 | 223 |
ultimately have "k # [] \<in> Kl" unfolding prefCl_def by blast |
224 |
thus "[] @ [k] \<in> Kl" by simp |
|
225 |
qed |
|
226 |
||
227 |
lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl" |
|
228 |
unfolding Succ_def by simp |
|
229 |
||
230 |
lemmas SuccE = SuccD[elim_format] |
|
231 |
||
232 |
lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl" |
|
233 |
unfolding Succ_def by simp |
|
234 |
||
235 |
lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl" |
|
236 |
unfolding Shift_def by simp |
|
237 |
||
238 |
lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)" |
|
239 |
unfolding Succ_def Shift_def by auto |
|
240 |
||
241 |
lemma ShiftI: "k # kl \<in> Kl \<Longrightarrow> kl \<in> Shift Kl k" |
|
242 |
unfolding Shift_def by simp |
|
243 |
||
244 |
lemma Func_cexp: "|Func A B| =o |B| ^c |A|" |
|
245 |
unfolding cexp_def Field_card_of by (simp only: card_of_refl) |
|
246 |
||
247 |
lemma clists_bound: "A \<in> Field (cpow (clists r)) - {{}} \<Longrightarrow> |A| \<le>o clists r" |
|
248 |
unfolding cpow_def clists_def Field_card_of by (auto simp: card_of_mono1) |
|
249 |
||
250 |
lemma cpow_clists_czero: "\<lbrakk>A \<in> Field (cpow (clists r)) - {{}}; |A| =o czero\<rbrakk> \<Longrightarrow> False" |
|
51782
84e7225f5ab6
removed unnecessary assumptions in some theorems about cardinal exponentiation
traytel
parents:
51739
diff
changeset
|
251 |
unfolding cpow_def clists_def card_of_ordIso_czero_iff_empty by auto |
49312 | 252 |
|
253 |
lemma incl_UNION_I: |
|
254 |
assumes "i \<in> I" and "A \<subseteq> F i" |
|
255 |
shows "A \<subseteq> UNION I F" |
|
256 |
using assms by auto |
|
257 |
||
258 |
lemma Nil_clists: "{[]} \<subseteq> Field (clists r)" |
|
259 |
unfolding clists_def Field_card_of by auto |
|
260 |
||
261 |
lemma Cons_clists: |
|
262 |
"\<lbrakk>x \<in> Field r; xs \<in> Field (clists r)\<rbrakk> \<Longrightarrow> x # xs \<in> Field (clists r)" |
|
263 |
unfolding clists_def Field_card_of by auto |
|
264 |
||
265 |
lemma length_Cons: "length (x # xs) = Suc (length xs)" |
|
266 |
by simp |
|
267 |
||
268 |
lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)" |
|
269 |
by simp |
|
270 |
||
271 |
(*injection into the field of a cardinal*) |
|
272 |
definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r" |
|
273 |
definition "toCard A r \<equiv> SOME f. toCard_pred A r f" |
|
274 |
||
275 |
lemma ex_toCard_pred: |
|
276 |
"\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f" |
|
277 |
unfolding toCard_pred_def |
|
278 |
using card_of_ordLeq[of A "Field r"] |
|
279 |
ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"] |
|
280 |
by blast |
|
281 |
||
282 |
lemma toCard_pred_toCard: |
|
283 |
"\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)" |
|
284 |
unfolding toCard_def using someI_ex[OF ex_toCard_pred] . |
|
285 |
||
286 |
lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> |
|
287 |
toCard A r x = toCard A r y \<longleftrightarrow> x = y" |
|
288 |
using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast |
|
289 |
||
290 |
lemma toCard: "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> toCard A r b \<in> Field r" |
|
291 |
using toCard_pred_toCard unfolding toCard_pred_def by blast |
|
292 |
||
293 |
definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k" |
|
294 |
||
295 |
lemma fromCard_toCard: |
|
296 |
"\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b" |
|
297 |
unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj) |
|
298 |
||
299 |
(* pick according to the weak pullback *) |
|
300 |
definition pickWP where |
|
51446 | 301 |
"pickWP A p1 p2 b1 b2 \<equiv> SOME a. a \<in> A \<and> p1 a = b1 \<and> p2 a = b2" |
49312 | 302 |
|
303 |
lemma pickWP_pred: |
|
304 |
assumes "wpull A B1 B2 f1 f2 p1 p2" and |
|
305 |
"b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2" |
|
51446 | 306 |
shows "\<exists> a. a \<in> A \<and> p1 a = b1 \<and> p2 a = b2" |
307 |
using assms unfolding wpull_def by blast |
|
49312 | 308 |
|
309 |
lemma pickWP: |
|
310 |
assumes "wpull A B1 B2 f1 f2 p1 p2" and |
|
311 |
"b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2" |
|
312 |
shows "pickWP A p1 p2 b1 b2 \<in> A" |
|
313 |
"p1 (pickWP A p1 p2 b1 b2) = b1" |
|
314 |
"p2 (pickWP A p1 p2 b1 b2) = b2" |
|
51446 | 315 |
unfolding pickWP_def using assms someI_ex[OF pickWP_pred] by fastforce+ |
49312 | 316 |
|
317 |
lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)" |
|
318 |
unfolding Field_card_of csum_def by auto |
|
319 |
||
320 |
lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)" |
|
321 |
unfolding Field_card_of csum_def by auto |
|
322 |
||
323 |
lemma nat_rec_0: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1" |
|
324 |
by auto |
|
325 |
||
326 |
lemma nat_rec_Suc: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)" |
|
327 |
by auto |
|
328 |
||
329 |
lemma list_rec_Nil: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1" |
|
330 |
by auto |
|
331 |
||
332 |
lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)" |
|
333 |
by auto |
|
334 |
||
335 |
lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y" |
|
336 |
by simp |
|
337 |
||
51925 | 338 |
lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)" |
339 |
by auto |
|
340 |
||
49309
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset
|
341 |
ML_file "Tools/bnf_gfp_util.ML" |
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset
|
342 |
ML_file "Tools/bnf_gfp_tactics.ML" |
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset
|
343 |
ML_file "Tools/bnf_gfp.ML" |
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset
|
344 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
345 |
end |