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