|
1 (* Title: HOL/Library/Finite_Cartesian_Product |
|
2 ID: $Id: Finite_Cartesian_Product.thy,v 1.5 2009/01/29 22:59:46 chaieb Exp $ |
|
3 Author: Amine Chaieb, University of Cambridge |
|
4 *) |
|
5 |
|
6 header {* Definition of finite Cartesian product types. *} |
|
7 |
|
8 theory Finite_Cartesian_Product |
|
9 imports Plain SetInterval ATP_Linkup |
|
10 begin |
|
11 |
|
12 (* FIXME : ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs*) |
|
13 subsection{* Dimention of sets *} |
|
14 |
|
15 definition "dimindex (S:: 'a set) = (if finite (UNIV::'a set) then card (UNIV:: 'a set) else 1)" |
|
16 |
|
17 syntax "_type_dimindex" :: "type => nat" ("(1DIM/(1'(_')))") |
|
18 translations "DIM(t)" => "CONST dimindex (UNIV :: t set)" |
|
19 |
|
20 lemma dimindex_nonzero: "dimindex S \<noteq> 0" |
|
21 unfolding dimindex_def |
|
22 by (simp add: neq0_conv[symmetric] del: neq0_conv) |
|
23 |
|
24 lemma dimindex_ge_1: "dimindex S \<ge> 1" |
|
25 using dimindex_nonzero[of S] by arith |
|
26 lemma dimindex_univ: "dimindex (S :: 'a set) = DIM('a)" by (simp add: dimindex_def) |
|
27 |
|
28 definition hassize (infixr "hassize" 12) where |
|
29 "(S hassize n) = (finite S \<and> card S = n)" |
|
30 |
|
31 lemma dimindex_unique: " (UNIV :: 'a set) hassize n ==> DIM('a) = n" |
|
32 by (simp add: dimindex_def hassize_def) |
|
33 |
|
34 |
|
35 section{* An indexing type parametrized by base type. *} |
|
36 |
|
37 typedef 'a finite_image = "{1 .. DIM('a)}" |
|
38 using dimindex_ge_1 by auto |
|
39 |
|
40 lemma finite_image_image: "(UNIV :: 'a finite_image set) = Abs_finite_image ` {1 .. DIM('a)}" |
|
41 apply (auto simp add: Abs_finite_image_inverse image_def finite_image_def) |
|
42 apply (rule_tac x="Rep_finite_image x" in bexI) |
|
43 apply (simp_all add: Rep_finite_image_inverse Rep_finite_image) |
|
44 using Rep_finite_image[where ?'a = 'a] |
|
45 unfolding finite_image_def |
|
46 apply simp |
|
47 done |
|
48 |
|
49 text{* Dimension of such a type, and indexing over it. *} |
|
50 |
|
51 lemma inj_on_Abs_finite_image: |
|
52 "inj_on (Abs_finite_image:: _ \<Rightarrow> 'a finite_image) {1 .. DIM('a)}" |
|
53 by (auto simp add: inj_on_def finite_image_def Abs_finite_image_inject[where ?'a='a]) |
|
54 |
|
55 lemma has_size_finite_image: "(UNIV:: 'a finite_image set) hassize dimindex (S :: 'a set)" |
|
56 unfolding hassize_def finite_image_image card_image[OF inj_on_Abs_finite_image[where ?'a='a]] by (auto simp add: dimindex_def) |
|
57 |
|
58 lemma hassize_image_inj: assumes f: "inj_on f S" and S: "S hassize n" |
|
59 shows "f ` S hassize n" |
|
60 using f S card_image[OF f] |
|
61 by (simp add: hassize_def inj_on_def) |
|
62 |
|
63 lemma card_finite_image: "card (UNIV:: 'a finite_image set) = dimindex(S:: 'a set)" |
|
64 using has_size_finite_image |
|
65 unfolding hassize_def by blast |
|
66 |
|
67 lemma finite_finite_image: "finite (UNIV:: 'a finite_image set)" |
|
68 using has_size_finite_image |
|
69 unfolding hassize_def by blast |
|
70 |
|
71 lemma dimindex_finite_image: "dimindex (S:: 'a finite_image set) = dimindex(T:: 'a set)" |
|
72 unfolding card_finite_image[of T, symmetric] |
|
73 by (auto simp add: dimindex_def finite_finite_image) |
|
74 |
|
75 lemma Abs_finite_image_works: |
|
76 fixes i:: "'a finite_image" |
|
77 shows " \<exists>!n \<in> {1 .. DIM('a)}. Abs_finite_image n = i" |
|
78 unfolding Bex1_def Ex1_def |
|
79 apply (rule_tac x="Rep_finite_image i" in exI) |
|
80 using Rep_finite_image_inverse[where ?'a = 'a] |
|
81 Rep_finite_image[where ?'a = 'a] |
|
82 Abs_finite_image_inverse[where ?'a='a, symmetric] |
|
83 by (auto simp add: finite_image_def) |
|
84 |
|
85 lemma Abs_finite_image_inj: |
|
86 "i \<in> {1 .. DIM('a)} \<Longrightarrow> j \<in> {1 .. DIM('a)} |
|
87 \<Longrightarrow> (((Abs_finite_image i ::'a finite_image) = Abs_finite_image j) \<longleftrightarrow> (i = j))" |
|
88 using Abs_finite_image_works[where ?'a = 'a] |
|
89 by (auto simp add: atLeastAtMost_iff Bex1_def) |
|
90 |
|
91 lemma forall_Abs_finite_image: |
|
92 "(\<forall>k:: 'a finite_image. P k) \<longleftrightarrow> (\<forall>i \<in> {1 .. DIM('a)}. P(Abs_finite_image i))" |
|
93 unfolding Ball_def atLeastAtMost_iff Ex1_def |
|
94 using Abs_finite_image_works[where ?'a = 'a, unfolded atLeastAtMost_iff Bex1_def] |
|
95 by metis |
|
96 |
|
97 subsection {* Finite Cartesian products, with indexing and lambdas. *} |
|
98 |
|
99 typedef (Cart) |
|
100 ('a, 'b) "^" (infixl "^" 15) |
|
101 = "{f:: 'b finite_image \<Rightarrow> 'a . True}" by simp |
|
102 |
|
103 abbreviation dimset:: "('a ^ 'n) \<Rightarrow> nat set" where |
|
104 "dimset a \<equiv> {1 .. DIM('n)}" |
|
105 |
|
106 definition Cart_nth :: "'a ^ 'b \<Rightarrow> nat \<Rightarrow> 'a" (infixl "$" 90) where |
|
107 "x$i = Rep_Cart x (Abs_finite_image i)" |
|
108 |
|
109 lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)" |
|
110 apply auto |
|
111 apply (rule ext) |
|
112 apply auto |
|
113 done |
|
114 lemma Cart_eq: "((x:: 'a ^ 'b) = y) \<longleftrightarrow> (\<forall>i\<in> dimset x. x$i = y$i)" |
|
115 unfolding Cart_nth_def forall_Abs_finite_image[symmetric, where P = "\<lambda>i. Rep_Cart x i = Rep_Cart y i"] stupid_ext |
|
116 using Rep_Cart_inject[of x y] .. |
|
117 |
|
118 consts Cart_lambda :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a ^ 'b" |
|
119 notation (xsymbols) Cart_lambda (binder "\<chi>" 10) |
|
120 |
|
121 defs Cart_lambda_def: "Cart_lambda g == (SOME (f:: 'a ^ 'b). \<forall>i \<in> {1 .. DIM('b)}. f$i = g i)" |
|
122 |
|
123 lemma Cart_lambda_beta: " \<forall> i\<in> {1 .. DIM('b)}. (Cart_lambda g:: 'a ^ 'b)$i = g i" |
|
124 unfolding Cart_lambda_def |
|
125 proof (rule someI_ex) |
|
126 let ?p = "\<lambda>(i::nat) (k::'b finite_image). i \<in> {1 .. DIM('b)} \<and> (Abs_finite_image i = k)" |
|
127 let ?f = "Abs_Cart (\<lambda>k. g (THE i. ?p i k)):: 'a ^ 'b" |
|
128 let ?P = "\<lambda>f i. f$i = g i" |
|
129 let ?Q = "\<lambda>(f::'a ^ 'b). \<forall> i \<in> {1 .. DIM('b)}. ?P f i" |
|
130 {fix i |
|
131 assume i: "i \<in> {1 .. DIM('b)}" |
|
132 let ?j = "THE j. ?p j (Abs_finite_image i)" |
|
133 from theI'[where P = "\<lambda>j. ?p (j::nat) (Abs_finite_image i :: 'b finite_image)", OF Abs_finite_image_works[of "Abs_finite_image i :: 'b finite_image", unfolded Bex1_def]] |
|
134 have j: "?j \<in> {1 .. DIM('b)}" "(Abs_finite_image ?j :: 'b finite_image) = Abs_finite_image i" by blast+ |
|
135 from i j Abs_finite_image_inject[of i ?j, where ?'a = 'b] |
|
136 have th: "?j = i" by (simp add: finite_image_def) |
|
137 have "?P ?f i" |
|
138 using th |
|
139 by (simp add: Cart_nth_def Abs_Cart_inverse Rep_Cart_inverse Cart_def) } |
|
140 hence th0: "?Q ?f" .. |
|
141 with th0 show "\<exists>f. ?Q f" unfolding Ex1_def by auto |
|
142 qed |
|
143 |
|
144 lemma Cart_lambda_beta': "i\<in> {1 .. DIM('b)} \<Longrightarrow> (Cart_lambda g:: 'a ^ 'b)$i = g i" |
|
145 using Cart_lambda_beta by blast |
|
146 |
|
147 lemma Cart_lambda_unique: |
|
148 fixes f :: "'a ^ 'b" |
|
149 shows "(\<forall>i\<in> {1 .. DIM('b)}. f$i = g i) \<longleftrightarrow> Cart_lambda g = f" |
|
150 by (auto simp add: Cart_eq Cart_lambda_beta) |
|
151 |
|
152 lemma Cart_lambda_eta: "(\<chi> i. (g$i)) = g" by (simp add: Cart_eq Cart_lambda_beta) |
|
153 |
|
154 text{* A non-standard sum to "paste" Cartesian products. *} |
|
155 |
|
156 typedef ('a,'b) finite_sum = "{1 .. DIM('a) + DIM('b)}" |
|
157 apply (rule exI[where x="1"]) |
|
158 using dimindex_ge_1[of "UNIV :: 'a set"] dimindex_ge_1[of "UNIV :: 'b set"] |
|
159 by auto |
|
160 |
|
161 definition pastecart :: "'a ^ 'm \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ ('m,'n) finite_sum" where |
|
162 "pastecart f g = (\<chi> i. (if i <= DIM('m) then f$i else g$(i - DIM('m))))" |
|
163 |
|
164 definition fstcart:: "'a ^('m, 'n) finite_sum \<Rightarrow> 'a ^ 'm" where |
|
165 "fstcart f = (\<chi> i. (f$i))" |
|
166 |
|
167 definition sndcart:: "'a ^('m, 'n) finite_sum \<Rightarrow> 'a ^ 'n" where |
|
168 "sndcart f = (\<chi> i. (f$(i + DIM('m))))" |
|
169 |
|
170 lemma finite_sum_image: "(UNIV::('a,'b) finite_sum set) = Abs_finite_sum ` {1 .. DIM('a) + DIM('b)}" |
|
171 apply (auto simp add: image_def) |
|
172 apply (rule_tac x="Rep_finite_sum x" in bexI) |
|
173 apply (simp add: Rep_finite_sum_inverse) |
|
174 using Rep_finite_sum[unfolded finite_sum_def, where ?'a = 'a and ?'b = 'b] |
|
175 apply (simp add: Rep_finite_sum) |
|
176 done |
|
177 |
|
178 lemma inj_on_Abs_finite_sum: "inj_on (Abs_finite_sum :: _ \<Rightarrow> ('a,'b) finite_sum) {1 .. DIM('a) + DIM('b)}" |
|
179 using Abs_finite_sum_inject[where ?'a = 'a and ?'b = 'b] |
|
180 by (auto simp add: inj_on_def finite_sum_def) |
|
181 |
|
182 lemma dimindex_has_size_finite_sum: |
|
183 "(UNIV::('m,'n) finite_sum set) hassize (DIM('m) + DIM('n))" |
|
184 by (simp add: finite_sum_image hassize_def card_image[OF inj_on_Abs_finite_sum[where ?'a = 'm and ?'b = 'n]] del: One_nat_def) |
|
185 |
|
186 lemma dimindex_finite_sum: "DIM(('m,'n) finite_sum) = DIM('m) + DIM('n)" |
|
187 using dimindex_has_size_finite_sum[where ?'n = 'n and ?'m = 'm, unfolded hassize_def] |
|
188 by (simp add: dimindex_def) |
|
189 |
|
190 lemma fstcart_pastecart: "fstcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = x" |
|
191 by (simp add: pastecart_def fstcart_def Cart_eq Cart_lambda_beta dimindex_finite_sum) |
|
192 |
|
193 lemma sndcart_pastecart: "sndcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = y" |
|
194 by (simp add: pastecart_def sndcart_def Cart_eq Cart_lambda_beta dimindex_finite_sum) |
|
195 |
|
196 lemma pastecart_fst_snd: "pastecart (fstcart z) (sndcart z) = z" |
|
197 proof - |
|
198 {fix i |
|
199 assume H: "i \<le> DIM('b) + DIM('c)" |
|
200 "\<not> i \<le> DIM('b)" |
|
201 from H have ith: "i - DIM('b) \<in> {1 .. DIM('c)}" |
|
202 apply simp by arith |
|
203 from H have th0: "i - DIM('b) + DIM('b) = i" |
|
204 by simp |
|
205 have "(\<chi> i. (z$(i + DIM('b))) :: 'a ^ 'c)$(i - DIM('b)) = z$i" |
|
206 unfolding Cart_lambda_beta'[where g = "\<lambda> i. z$(i + DIM('b))", OF ith] th0 ..} |
|
207 thus ?thesis by (auto simp add: pastecart_def fstcart_def sndcart_def Cart_eq Cart_lambda_beta dimindex_finite_sum) |
|
208 qed |
|
209 |
|
210 lemma pastecart_eq: "(x = y) \<longleftrightarrow> (fstcart x = fstcart y) \<and> (sndcart x = sndcart y)" |
|
211 using pastecart_fst_snd[of x] pastecart_fst_snd[of y] by metis |
|
212 |
|
213 lemma forall_pastecart: "(\<forall>p. P p) \<longleftrightarrow> (\<forall>x y. P (pastecart x y))" |
|
214 by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart) |
|
215 |
|
216 lemma exists_pastecart: "(\<exists>p. P p) \<longleftrightarrow> (\<exists>x y. P (pastecart x y))" |
|
217 by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart) |
|
218 |
|
219 text{* The finiteness lemma. *} |
|
220 |
|
221 lemma finite_cart: |
|
222 "\<forall>i \<in> {1 .. DIM('n)}. finite {x. P i x} |
|
223 \<Longrightarrow> finite {v::'a ^ 'n . (\<forall>i \<in> {1 .. DIM('n)}. P i (v$i))}" |
|
224 proof- |
|
225 assume f: "\<forall>i \<in> {1 .. DIM('n)}. finite {x. P i x}" |
|
226 {fix n |
|
227 assume n: "n \<le> DIM('n)" |
|
228 have "finite {v:: 'a ^ 'n . (\<forall>i\<in> {1 .. DIM('n)}. i \<le> n \<longrightarrow> P i (v$i)) |
|
229 \<and> (\<forall>i\<in> {1 .. DIM('n)}. n < i \<longrightarrow> v$i = (SOME x. False))}" |
|
230 using n |
|
231 proof(induct n) |
|
232 case 0 |
|
233 have th0: "{v . (\<forall>i \<in> {1 .. DIM('n)}. v$i = (SOME x. False))} = |
|
234 {(\<chi> i. (SOME x. False)::'a ^ 'n)}" by (auto simp add: Cart_lambda_beta Cart_eq) |
|
235 with "0.prems" show ?case by auto |
|
236 next |
|
237 case (Suc n) |
|
238 let ?h = "\<lambda>(x::'a,v:: 'a ^ 'n). (\<chi> i. if i = Suc n then x else v$i):: 'a ^ 'n" |
|
239 let ?T = "{v\<Colon>'a ^ 'n. |
|
240 (\<forall>i\<Colon>nat\<in>{1\<Colon>nat..DIM('n)}. i \<le> Suc n \<longrightarrow> P i (v$i)) \<and> |
|
241 (\<forall>i\<Colon>nat\<in>{1\<Colon>nat..DIM('n)}. |
|
242 Suc n < i \<longrightarrow> v$i = (SOME x\<Colon>'a. False))}" |
|
243 let ?S = "{x::'a . P (Suc n) x} \<times> {v:: 'a^'n. (\<forall>i \<in> {1 .. DIM('n)}. i <= n \<longrightarrow> P i (v$i)) \<and> (\<forall>i \<in> {1 .. DIM('n)}. n < i \<longrightarrow> v$i = (SOME x. False))}" |
|
244 have th0: " ?T \<subseteq> (?h ` ?S)" |
|
245 using Suc.prems |
|
246 apply (auto simp add: image_def) |
|
247 apply (rule_tac x = "x$(Suc n)" in exI) |
|
248 apply (rule conjI) |
|
249 apply (rotate_tac) |
|
250 apply (erule ballE[where x="Suc n"]) |
|
251 apply simp |
|
252 apply simp |
|
253 apply (rule_tac x= "\<chi> i. if i = Suc n then (SOME x:: 'a. False) else (x:: 'a ^ 'n)$i:: 'a ^ 'n" in exI) |
|
254 by (simp add: Cart_eq Cart_lambda_beta) |
|
255 have th1: "finite ?S" |
|
256 apply (rule finite_cartesian_product) |
|
257 using f Suc.hyps Suc.prems by auto |
|
258 from finite_imageI[OF th1] have th2: "finite (?h ` ?S)" . |
|
259 from finite_subset[OF th0 th2] show ?case by blast |
|
260 qed} |
|
261 |
|
262 note th = this |
|
263 from this[of "DIM('n)"] f |
|
264 show ?thesis by auto |
|
265 qed |
|
266 |
|
267 |
|
268 end |