diff -r ac50e7dedf6d -r 638b088bb840 src/HOL/Library/Finite_Cartesian_Product.thy --- a/src/HOL/Library/Finite_Cartesian_Product.thy Wed Mar 18 22:17:23 2009 +0100 +++ b/src/HOL/Library/Finite_Cartesian_Product.thy Thu Mar 19 01:29:19 2009 -0700 @@ -10,202 +10,81 @@ begin (* FIXME : ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs*) -subsection{* Dimention of sets *} - -definition "dimindex (S:: 'a set) = (if finite (UNIV::'a set) then card (UNIV:: 'a set) else 1)" - -syntax "_type_dimindex" :: "type => nat" ("(1DIM/(1'(_')))") -translations "DIM(t)" => "CONST dimindex (CONST UNIV :: t set)" - -lemma dimindex_nonzero: "dimindex S \ 0" -unfolding dimindex_def -by (simp add: neq0_conv[symmetric] del: neq0_conv) - -lemma dimindex_ge_1: "dimindex S \ 1" - using dimindex_nonzero[of S] by arith -lemma dimindex_univ: "dimindex (S :: 'a set) = DIM('a)" by (simp add: dimindex_def) definition hassize (infixr "hassize" 12) where "(S hassize n) = (finite S \ card S = n)" -lemma dimindex_unique: " (UNIV :: 'a set) hassize n ==> DIM('a) = n" -by (simp add: dimindex_def hassize_def) - - -subsection{* An indexing type parametrized by base type. *} - -typedef 'a finite_image = "{1 .. DIM('a)}" - using dimindex_ge_1 by auto - -lemma finite_image_image: "(UNIV :: 'a finite_image set) = Abs_finite_image ` {1 .. DIM('a)}" -apply (auto simp add: Abs_finite_image_inverse image_def finite_image_def) -apply (rule_tac x="Rep_finite_image x" in bexI) -apply (simp_all add: Rep_finite_image_inverse Rep_finite_image) -using Rep_finite_image[where ?'a = 'a] -unfolding finite_image_def -apply simp -done - -text{* Dimension of such a type, and indexing over it. *} - -lemma inj_on_Abs_finite_image: - "inj_on (Abs_finite_image:: _ \ 'a finite_image) {1 .. DIM('a)}" -by (auto simp add: inj_on_def finite_image_def Abs_finite_image_inject[where ?'a='a]) - -lemma has_size_finite_image: "(UNIV:: 'a finite_image set) hassize dimindex (S :: 'a set)" - unfolding hassize_def finite_image_image card_image[OF inj_on_Abs_finite_image[where ?'a='a]] by (auto simp add: dimindex_def) - lemma hassize_image_inj: assumes f: "inj_on f S" and S: "S hassize n" shows "f ` S hassize n" using f S card_image[OF f] by (simp add: hassize_def inj_on_def) -lemma card_finite_image: "card (UNIV:: 'a finite_image set) = dimindex(S:: 'a set)" -using has_size_finite_image -unfolding hassize_def by blast - -lemma finite_finite_image: "finite (UNIV:: 'a finite_image set)" -using has_size_finite_image -unfolding hassize_def by blast - -lemma dimindex_finite_image: "dimindex (S:: 'a finite_image set) = dimindex(T:: 'a set)" -unfolding card_finite_image[of T, symmetric] -by (auto simp add: dimindex_def finite_finite_image) - -lemma Abs_finite_image_works: - fixes i:: "'a finite_image" - shows " \!n \ {1 .. DIM('a)}. Abs_finite_image n = i" - unfolding Bex1_def Ex1_def - apply (rule_tac x="Rep_finite_image i" in exI) - using Rep_finite_image_inverse[where ?'a = 'a] - Rep_finite_image[where ?'a = 'a] - Abs_finite_image_inverse[where ?'a='a, symmetric] - by (auto simp add: finite_image_def) - -lemma Abs_finite_image_inj: - "i \ {1 .. DIM('a)} \ j \ {1 .. DIM('a)} - \ (((Abs_finite_image i ::'a finite_image) = Abs_finite_image j) \ (i = j))" - using Abs_finite_image_works[where ?'a = 'a] - by (auto simp add: atLeastAtMost_iff Bex1_def) - -lemma forall_Abs_finite_image: - "(\k:: 'a finite_image. P k) \ (\i \ {1 .. DIM('a)}. P(Abs_finite_image i))" -unfolding Ball_def atLeastAtMost_iff Ex1_def -using Abs_finite_image_works[where ?'a = 'a, unfolded atLeastAtMost_iff Bex1_def] -by metis subsection {* Finite Cartesian products, with indexing and lambdas. *} -typedef (Cart) +typedef (open Cart) ('a, 'b) "^" (infixl "^" 15) - = "{f:: 'b finite_image \ 'a . True}" by simp + = "UNIV :: ('b \ 'a) set" + morphisms Cart_nth Cart_lambda .. -abbreviation dimset:: "('a ^ 'n) \ nat set" where - "dimset a \ {1 .. DIM('n)}" +notation Cart_nth (infixl "$" 90) -definition Cart_nth :: "'a ^ 'b \ nat \ 'a" (infixl "$" 90) where - "x$i = Rep_Cart x (Abs_finite_image i)" +notation (xsymbols) Cart_lambda (binder "\" 10) lemma stupid_ext: "(\x. f x = g x) \ (f = g)" apply auto apply (rule ext) apply auto done -lemma Cart_eq: "((x:: 'a ^ 'b) = y) \ (\i\ dimset x. x$i = y$i)" - unfolding Cart_nth_def forall_Abs_finite_image[symmetric, where P = "\i. Rep_Cart x i = Rep_Cart y i"] stupid_ext - using Rep_Cart_inject[of x y] .. - -consts Cart_lambda :: "(nat \ 'a) \ 'a ^ 'b" -notation (xsymbols) Cart_lambda (binder "\" 10) - -defs Cart_lambda_def: "Cart_lambda g == (SOME (f:: 'a ^ 'b). \i \ {1 .. DIM('b)}. f$i = g i)" -lemma Cart_lambda_beta: " \ i\ {1 .. DIM('b)}. (Cart_lambda g:: 'a ^ 'b)$i = g i" - unfolding Cart_lambda_def -proof (rule someI_ex) - let ?p = "\(i::nat) (k::'b finite_image). i \ {1 .. DIM('b)} \ (Abs_finite_image i = k)" - let ?f = "Abs_Cart (\k. g (THE i. ?p i k)):: 'a ^ 'b" - let ?P = "\f i. f$i = g i" - let ?Q = "\(f::'a ^ 'b). \ i \ {1 .. DIM('b)}. ?P f i" - {fix i - assume i: "i \ {1 .. DIM('b)}" - let ?j = "THE j. ?p j (Abs_finite_image i)" - from theI'[where P = "\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]] - have j: "?j \ {1 .. DIM('b)}" "(Abs_finite_image ?j :: 'b finite_image) = Abs_finite_image i" by blast+ - from i j Abs_finite_image_inject[of i ?j, where ?'a = 'b] - have th: "?j = i" by (simp add: finite_image_def) - have "?P ?f i" - using th - by (simp add: Cart_nth_def Abs_Cart_inverse Rep_Cart_inverse Cart_def) } - hence th0: "?Q ?f" .. - with th0 show "\f. ?Q f" unfolding Ex1_def by auto -qed +lemma Cart_eq: "((x:: 'a ^ 'b) = y) \ (\i. x$i = y$i)" + by (simp add: Cart_nth_inject [symmetric] expand_fun_eq) -lemma Cart_lambda_beta': "i\ {1 .. DIM('b)} \ (Cart_lambda g:: 'a ^ 'b)$i = g i" - using Cart_lambda_beta by blast +lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i" + by (simp add: Cart_lambda_inverse) lemma Cart_lambda_unique: fixes f :: "'a ^ 'b" - shows "(\i\ {1 .. DIM('b)}. f$i = g i) \ Cart_lambda g = f" - by (auto simp add: Cart_eq Cart_lambda_beta) + shows "(\i. f$i = g i) \ Cart_lambda g = f" + by (auto simp add: Cart_eq) -lemma Cart_lambda_eta: "(\ i. (g$i)) = g" by (simp add: Cart_eq Cart_lambda_beta) +lemma Cart_lambda_eta: "(\ i. (g$i)) = g" + by (simp add: Cart_eq) text{* A non-standard sum to "paste" Cartesian products. *} -typedef ('a,'b) finite_sum = "{1 .. DIM('a) + DIM('b)}" - apply (rule exI[where x="1"]) - using dimindex_ge_1[of "UNIV :: 'a set"] dimindex_ge_1[of "UNIV :: 'b set"] - by auto +definition pastecart :: "'a ^ 'm \ 'a ^ 'n \ 'a ^ ('m + 'n)" where + "pastecart f g = (\ i. case i of Inl a \ f$a | Inr b \ g$b)" + +definition fstcart:: "'a ^('m + 'n) \ 'a ^ 'm" where + "fstcart f = (\ i. (f$(Inl i)))" -definition pastecart :: "'a ^ 'm \ 'a ^ 'n \ 'a ^ ('m,'n) finite_sum" where - "pastecart f g = (\ i. (if i <= DIM('m) then f$i else g$(i - DIM('m))))" +definition sndcart:: "'a ^('m + 'n) \ 'a ^ 'n" where + "sndcart f = (\ i. (f$(Inr i)))" -definition fstcart:: "'a ^('m, 'n) finite_sum \ 'a ^ 'm" where - "fstcart f = (\ i. (f$i))" - -definition sndcart:: "'a ^('m, 'n) finite_sum \ 'a ^ 'n" where - "sndcart f = (\ i. (f$(i + DIM('m))))" +lemma nth_pastecart_Inl [simp]: "pastecart f g $ Inl a = f$a" + unfolding pastecart_def by simp -lemma finite_sum_image: "(UNIV::('a,'b) finite_sum set) = Abs_finite_sum ` {1 .. DIM('a) + DIM('b)}" -apply (auto simp add: image_def) -apply (rule_tac x="Rep_finite_sum x" in bexI) -apply (simp add: Rep_finite_sum_inverse) -using Rep_finite_sum[unfolded finite_sum_def, where ?'a = 'a and ?'b = 'b] -apply (simp add: Rep_finite_sum) -done +lemma nth_pastecart_Inr [simp]: "pastecart f g $ Inr b = g$b" + unfolding pastecart_def by simp + +lemma nth_fstcart [simp]: "fstcart f $ i = f $ Inl i" + unfolding fstcart_def by simp -lemma inj_on_Abs_finite_sum: "inj_on (Abs_finite_sum :: _ \ ('a,'b) finite_sum) {1 .. DIM('a) + DIM('b)}" - using Abs_finite_sum_inject[where ?'a = 'a and ?'b = 'b] - by (auto simp add: inj_on_def finite_sum_def) +lemma nth_sndtcart [simp]: "sndcart f $ i = f $ Inr i" + unfolding sndcart_def by simp -lemma dimindex_has_size_finite_sum: - "(UNIV::('m,'n) finite_sum set) hassize (DIM('m) + DIM('n))" - 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) - -lemma dimindex_finite_sum: "DIM(('m,'n) finite_sum) = DIM('m) + DIM('n)" - using dimindex_has_size_finite_sum[where ?'n = 'n and ?'m = 'm, unfolded hassize_def] - by (simp add: dimindex_def) +lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \ range Inr" +by (auto, case_tac x, auto) lemma fstcart_pastecart: "fstcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = x" - by (simp add: pastecart_def fstcart_def Cart_eq Cart_lambda_beta dimindex_finite_sum) + by (simp add: Cart_eq) lemma sndcart_pastecart: "sndcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = y" - by (simp add: pastecart_def sndcart_def Cart_eq Cart_lambda_beta dimindex_finite_sum) + by (simp add: Cart_eq) lemma pastecart_fst_snd: "pastecart (fstcart z) (sndcart z) = z" -proof - - {fix i - assume H: "i \ DIM('b) + DIM('c)" - "\ i \ DIM('b)" - from H have ith: "i - DIM('b) \ {1 .. DIM('c)}" - apply simp by arith - from H have th0: "i - DIM('b) + DIM('b) = i" - by simp - have "(\ i. (z$(i + DIM('b))) :: 'a ^ 'c)$(i - DIM('b)) = z$i" - unfolding Cart_lambda_beta'[where g = "\ i. z$(i + DIM('b))", OF ith] th0 ..} -thus ?thesis by (auto simp add: pastecart_def fstcart_def sndcart_def Cart_eq Cart_lambda_beta dimindex_finite_sum) -qed + by (simp add: Cart_eq pastecart_def fstcart_def sndcart_def split: sum.split) lemma pastecart_eq: "(x = y) \ (fstcart x = fstcart y) \ (sndcart x = sndcart y)" using pastecart_fst_snd[of x] pastecart_fst_snd[of y] by metis @@ -216,53 +95,4 @@ lemma exists_pastecart: "(\p. P p) \ (\x y. P (pastecart x y))" by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart) -text{* The finiteness lemma. *} - -lemma finite_cart: - "\i \ {1 .. DIM('n)}. finite {x. P i x} - \ finite {v::'a ^ 'n . (\i \ {1 .. DIM('n)}. P i (v$i))}" -proof- - assume f: "\i \ {1 .. DIM('n)}. finite {x. P i x}" - {fix n - assume n: "n \ DIM('n)" - have "finite {v:: 'a ^ 'n . (\i\ {1 .. DIM('n)}. i \ n \ P i (v$i)) - \ (\i\ {1 .. DIM('n)}. n < i \ v$i = (SOME x. False))}" - using n - proof(induct n) - case 0 - have th0: "{v . (\i \ {1 .. DIM('n)}. v$i = (SOME x. False))} = - {(\ i. (SOME x. False)::'a ^ 'n)}" by (auto simp add: Cart_lambda_beta Cart_eq) - with "0.prems" show ?case by auto - next - case (Suc n) - let ?h = "\(x::'a,v:: 'a ^ 'n). (\ i. if i = Suc n then x else v$i):: 'a ^ 'n" - let ?T = "{v\'a ^ 'n. - (\i\nat\{1\nat..DIM('n)}. i \ Suc n \ P i (v$i)) \ - (\i\nat\{1\nat..DIM('n)}. - Suc n < i \ v$i = (SOME x\'a. False))}" - let ?S = "{x::'a . P (Suc n) x} \ {v:: 'a^'n. (\i \ {1 .. DIM('n)}. i <= n \ P i (v$i)) \ (\i \ {1 .. DIM('n)}. n < i \ v$i = (SOME x. False))}" - have th0: " ?T \ (?h ` ?S)" - using Suc.prems - apply (auto simp add: image_def) - apply (rule_tac x = "x$(Suc n)" in exI) - apply (rule conjI) - apply (rotate_tac) - apply (erule ballE[where x="Suc n"]) - apply simp - apply simp - apply (rule_tac x= "\ i. if i = Suc n then (SOME x:: 'a. False) else (x:: 'a ^ 'n)$i:: 'a ^ 'n" in exI) - by (simp add: Cart_eq Cart_lambda_beta) - have th1: "finite ?S" - apply (rule finite_cartesian_product) - using f Suc.hyps Suc.prems by auto - from finite_imageI[OF th1] have th2: "finite (?h ` ?S)" . - from finite_subset[OF th0 th2] show ?case by blast - qed} - - note th = this - from this[of "DIM('n)"] f - show ?thesis by auto -qed - - end