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