author | haftmann |
Fri, 01 Nov 2013 18:51:14 +0100 | |
changeset 54230 | b1d955791529 |
parent 53695 | a66d211ab34e |
child 54246 | 8fdb4dc08ed1 |
permissions | -rw-r--r-- |
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49326
diff
changeset
|
1 |
(* Title: HOL/BNF/BNF_LFP.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 |
53305 | 3 |
Author: Lorenz Panny, TU Muenchen |
4 |
Author: Jasmin Blanchette, TU Muenchen |
|
5 |
Copyright 2012, 2013 |
|
48975
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 |
Least 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
|
8 |
*) |
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 |
header {* Least 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
|
11 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
12 |
theory BNF_LFP |
53311 | 13 |
imports BNF_FP_Base |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
14 |
keywords |
53305 | 15 |
"datatype_new" :: thy_decl and |
53310 | 16 |
"datatype_new_compat" :: thy_decl and |
17 |
"primrec_new" :: 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 |
|
49312 | 20 |
lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}" |
21 |
by blast |
|
22 |
||
23 |
lemma image_Collect_subsetI: |
|
24 |
"(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B" |
|
25 |
by blast |
|
26 |
||
27 |
lemma Collect_restrict: "{x. x \<in> X \<and> P x} \<subseteq> X" |
|
28 |
by auto |
|
29 |
||
30 |
lemma prop_restrict: "\<lbrakk>x \<in> Z; Z \<subseteq> {x. x \<in> X \<and> P x}\<rbrakk> \<Longrightarrow> P x" |
|
31 |
by auto |
|
32 |
||
33 |
lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> rel.underS R j" |
|
34 |
unfolding rel.underS_def by simp |
|
35 |
||
36 |
lemma underS_E: "i \<in> rel.underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R" |
|
37 |
unfolding rel.underS_def by simp |
|
38 |
||
39 |
lemma underS_Field: "i \<in> rel.underS R j \<Longrightarrow> i \<in> Field R" |
|
40 |
unfolding rel.underS_def Field_def by auto |
|
41 |
||
42 |
lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R" |
|
43 |
unfolding Field_def by auto |
|
44 |
||
45 |
lemma fst_convol': "fst (<f, g> x) = f x" |
|
46 |
using fst_convol unfolding convol_def by simp |
|
47 |
||
48 |
lemma snd_convol': "snd (<f, g> x) = g x" |
|
49 |
using snd_convol unfolding convol_def by simp |
|
50 |
||
51 |
lemma convol_expand_snd: "fst o f = g \<Longrightarrow> <g, snd o f> = f" |
|
52 |
unfolding convol_def by auto |
|
53 |
||
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49635
diff
changeset
|
54 |
lemma convol_expand_snd': "(fst o f = g) \<Longrightarrow> (h = snd o f) \<longleftrightarrow> (<g, h> = f)" |
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49635
diff
changeset
|
55 |
by (metis convol_expand_snd snd_convol) |
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49635
diff
changeset
|
56 |
|
49312 | 57 |
definition inver where |
58 |
"inver g f A = (ALL a : A. g (f a) = a)" |
|
59 |
||
60 |
lemma bij_betw_iff_ex: |
|
61 |
"bij_betw f A B = (EX g. g ` B = A \<and> inver g f A \<and> inver f g B)" (is "?L = ?R") |
|
62 |
proof (rule iffI) |
|
63 |
assume ?L |
|
64 |
hence f: "f ` A = B" and inj_f: "inj_on f A" unfolding bij_betw_def by auto |
|
65 |
let ?phi = "% b a. a : A \<and> f a = b" |
|
66 |
have "ALL b : B. EX a. ?phi b a" using f by blast |
|
67 |
then obtain g where g: "ALL b : B. g b : A \<and> f (g b) = b" |
|
68 |
using bchoice[of B ?phi] by blast |
|
69 |
hence gg: "ALL b : f ` A. g b : A \<and> f (g b) = b" using f by blast |
|
49326 | 70 |
have gf: "inver g f A" unfolding inver_def |
71 |
by (metis (no_types) gg imageI[of _ A f] the_inv_into_f_f[OF inj_f]) |
|
49312 | 72 |
moreover have "g ` B \<le> A \<and> inver f g B" using g unfolding inver_def by blast |
73 |
moreover have "A \<le> g ` B" |
|
74 |
proof safe |
|
75 |
fix a assume a: "a : A" |
|
76 |
hence "f a : B" using f by auto |
|
77 |
moreover have "a = g (f a)" using a gf unfolding inver_def by auto |
|
78 |
ultimately show "a : g ` B" by blast |
|
79 |
qed |
|
80 |
ultimately show ?R by blast |
|
81 |
next |
|
82 |
assume ?R |
|
83 |
then obtain g where g: "g ` B = A \<and> inver g f A \<and> inver f g B" by blast |
|
84 |
show ?L unfolding bij_betw_def |
|
85 |
proof safe |
|
86 |
show "inj_on f A" unfolding inj_on_def |
|
87 |
proof safe |
|
88 |
fix a1 a2 assume a: "a1 : A" "a2 : A" and "f a1 = f a2" |
|
89 |
hence "g (f a1) = g (f a2)" by simp |
|
90 |
thus "a1 = a2" using a g unfolding inver_def by simp |
|
91 |
qed |
|
92 |
next |
|
93 |
fix a assume "a : A" |
|
94 |
then obtain b where b: "b : B" and a: "a = g b" using g by blast |
|
95 |
hence "b = f (g b)" using g unfolding inver_def by auto |
|
96 |
thus "f a : B" unfolding a using b by simp |
|
97 |
next |
|
98 |
fix b assume "b : B" |
|
99 |
hence "g b : A \<and> b = f (g b)" using g unfolding inver_def by auto |
|
100 |
thus "b : f ` A" by auto |
|
101 |
qed |
|
102 |
qed |
|
103 |
||
104 |
lemma bij_betw_ex_weakE: |
|
105 |
"\<lbrakk>bij_betw f A B\<rbrakk> \<Longrightarrow> \<exists>g. g ` B \<subseteq> A \<and> inver g f A \<and> inver f g B" |
|
106 |
by (auto simp only: bij_betw_iff_ex) |
|
107 |
||
108 |
lemma inver_surj: "\<lbrakk>g ` B \<subseteq> A; f ` A \<subseteq> B; inver g f A\<rbrakk> \<Longrightarrow> g ` B = A" |
|
109 |
unfolding inver_def by auto (rule rev_image_eqI, auto) |
|
110 |
||
111 |
lemma inver_mono: "\<lbrakk>A \<subseteq> B; inver f g B\<rbrakk> \<Longrightarrow> inver f g A" |
|
112 |
unfolding inver_def by auto |
|
113 |
||
114 |
lemma inver_pointfree: "inver f g A = (\<forall>a \<in> A. (f o g) a = a)" |
|
115 |
unfolding inver_def by simp |
|
116 |
||
117 |
lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B" |
|
118 |
unfolding bij_betw_def by auto |
|
119 |
||
120 |
lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B" |
|
121 |
unfolding bij_betw_def by auto |
|
122 |
||
123 |
lemma inverE: "\<lbrakk>inver f f' A; x \<in> A\<rbrakk> \<Longrightarrow> f (f' x) = x" |
|
124 |
unfolding inver_def by auto |
|
125 |
||
126 |
lemma bij_betw_inver1: "bij_betw f A B \<Longrightarrow> inver (inv_into A f) f A" |
|
127 |
unfolding bij_betw_def inver_def by auto |
|
128 |
||
129 |
lemma bij_betw_inver2: "bij_betw f A B \<Longrightarrow> inver f (inv_into A f) B" |
|
130 |
unfolding bij_betw_def inver_def by auto |
|
131 |
||
132 |
lemma bij_betwI: "\<lbrakk>bij_betw g B A; inver g f A; inver f g B\<rbrakk> \<Longrightarrow> bij_betw f A B" |
|
49326 | 133 |
by (drule bij_betw_imageE, unfold bij_betw_iff_ex) blast |
49312 | 134 |
|
135 |
lemma bij_betwI': |
|
136 |
"\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y); |
|
137 |
\<And>x. x \<in> X \<Longrightarrow> f x \<in> Y; |
|
138 |
\<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y" |
|
53695 | 139 |
unfolding bij_betw_def inj_on_def by blast |
49312 | 140 |
|
141 |
lemma surj_fun_eq: |
|
142 |
assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x" |
|
143 |
shows "g1 = g2" |
|
144 |
proof (rule ext) |
|
145 |
fix y |
|
146 |
from surj_on obtain x where "x \<in> X" and "y = f x" by blast |
|
147 |
thus "g1 y = g2 y" using eq_on by simp |
|
148 |
qed |
|
149 |
||
150 |
lemma Card_order_wo_rel: "Card_order r \<Longrightarrow> wo_rel r" |
|
49514 | 151 |
unfolding wo_rel_def card_order_on_def by blast |
49312 | 152 |
|
153 |
lemma Cinfinite_limit: "\<lbrakk>x \<in> Field r; Cinfinite r\<rbrakk> \<Longrightarrow> |
|
154 |
\<exists>y \<in> Field r. x \<noteq> y \<and> (x, y) \<in> r" |
|
155 |
unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit) |
|
156 |
||
157 |
lemma Card_order_trans: |
|
158 |
"\<lbrakk>Card_order r; x \<noteq> y; (x, y) \<in> r; y \<noteq> z; (y, z) \<in> r\<rbrakk> \<Longrightarrow> x \<noteq> z \<and> (x, z) \<in> r" |
|
159 |
unfolding card_order_on_def well_order_on_def linear_order_on_def |
|
160 |
partial_order_on_def preorder_on_def trans_def antisym_def by blast |
|
161 |
||
162 |
lemma Cinfinite_limit2: |
|
163 |
assumes x1: "x1 \<in> Field r" and x2: "x2 \<in> Field r" and r: "Cinfinite r" |
|
164 |
shows "\<exists>y \<in> Field r. (x1 \<noteq> y \<and> (x1, y) \<in> r) \<and> (x2 \<noteq> y \<and> (x2, y) \<in> r)" |
|
165 |
proof - |
|
166 |
from r have trans: "trans r" and total: "Total r" and antisym: "antisym r" |
|
167 |
unfolding card_order_on_def well_order_on_def linear_order_on_def |
|
168 |
partial_order_on_def preorder_on_def by auto |
|
169 |
obtain y1 where y1: "y1 \<in> Field r" "x1 \<noteq> y1" "(x1, y1) \<in> r" |
|
170 |
using Cinfinite_limit[OF x1 r] by blast |
|
171 |
obtain y2 where y2: "y2 \<in> Field r" "x2 \<noteq> y2" "(x2, y2) \<in> r" |
|
172 |
using Cinfinite_limit[OF x2 r] by blast |
|
173 |
show ?thesis |
|
174 |
proof (cases "y1 = y2") |
|
175 |
case True with y1 y2 show ?thesis by blast |
|
176 |
next |
|
177 |
case False |
|
178 |
with y1(1) y2(1) total have "(y1, y2) \<in> r \<or> (y2, y1) \<in> r" |
|
179 |
unfolding total_on_def by auto |
|
180 |
thus ?thesis |
|
181 |
proof |
|
182 |
assume *: "(y1, y2) \<in> r" |
|
183 |
with trans y1(3) have "(x1, y2) \<in> r" unfolding trans_def by blast |
|
184 |
with False y1 y2 * antisym show ?thesis by (cases "x1 = y2") (auto simp: antisym_def) |
|
185 |
next |
|
186 |
assume *: "(y2, y1) \<in> r" |
|
187 |
with trans y2(3) have "(x2, y1) \<in> r" unfolding trans_def by blast |
|
188 |
with False y1 y2 * antisym show ?thesis by (cases "x2 = y1") (auto simp: antisym_def) |
|
189 |
qed |
|
190 |
qed |
|
191 |
qed |
|
192 |
||
193 |
lemma Cinfinite_limit_finite: "\<lbrakk>finite X; X \<subseteq> Field r; Cinfinite r\<rbrakk> |
|
194 |
\<Longrightarrow> \<exists>y \<in> Field r. \<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)" |
|
195 |
proof (induct X rule: finite_induct) |
|
196 |
case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto |
|
197 |
next |
|
198 |
case (insert x X) |
|
199 |
then obtain y where y: "y \<in> Field r" "\<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)" by blast |
|
200 |
then obtain z where z: "z \<in> Field r" "x \<noteq> z \<and> (x, z) \<in> r" "y \<noteq> z \<and> (y, z) \<in> r" |
|
201 |
using Cinfinite_limit2[OF _ y(1) insert(5), of x] insert(4) by blast |
|
49326 | 202 |
show ?case |
203 |
apply (intro bexI ballI) |
|
204 |
apply (erule insertE) |
|
205 |
apply hypsubst |
|
206 |
apply (rule z(2)) |
|
207 |
using Card_order_trans[OF insert(5)[THEN conjunct2]] y(2) z(3) |
|
208 |
apply blast |
|
209 |
apply (rule z(1)) |
|
210 |
done |
|
49312 | 211 |
qed |
212 |
||
213 |
lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A" |
|
214 |
by auto |
|
215 |
||
216 |
(*helps resolution*) |
|
217 |
lemma well_order_induct_imp: |
|
218 |
"wo_rel r \<Longrightarrow> (\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> y \<in> Field r \<longrightarrow> P y \<Longrightarrow> x \<in> Field r \<longrightarrow> P x) \<Longrightarrow> |
|
219 |
x \<in> Field r \<longrightarrow> P x" |
|
220 |
by (erule wo_rel.well_order_induct) |
|
221 |
||
222 |
lemma meta_spec2: |
|
223 |
assumes "(\<And>x y. PROP P x y)" |
|
224 |
shows "PROP P x y" |
|
225 |
by (rule `(\<And>x y. PROP P x y)`) |
|
226 |
||
52731 | 227 |
lemma vimage2p_fun_rel: "(fun_rel (vimage2p f g R) R) f g" |
228 |
unfolding fun_rel_def vimage2p_def by auto |
|
229 |
||
230 |
lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)" |
|
231 |
unfolding vimage2p_def by auto |
|
232 |
||
49309
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset
|
233 |
ML_file "Tools/bnf_lfp_util.ML" |
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset
|
234 |
ML_file "Tools/bnf_lfp_tactics.ML" |
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset
|
235 |
ML_file "Tools/bnf_lfp.ML" |
53305 | 236 |
ML_file "Tools/bnf_lfp_compat.ML" |
49309
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset
|
237 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
238 |
end |