src/HOL/Library/Finite_Cartesian_Product.thy
 author huffman Thu Jun 11 09:03:24 2009 -0700 (2009-06-11) changeset 31563 ded2364d14d4 parent 30661 54858c8ad226 permissions -rw-r--r--
cleaned up some proofs
 chaieb@29835 ` 1` ```(* Title: HOL/Library/Finite_Cartesian_Product ``` chaieb@29835 ` 2` ``` Author: Amine Chaieb, University of Cambridge ``` chaieb@29835 ` 3` ```*) ``` chaieb@29835 ` 4` chaieb@29835 ` 5` ```header {* Definition of finite Cartesian product types. *} ``` chaieb@29835 ` 6` chaieb@29835 ` 7` ```theory Finite_Cartesian_Product ``` haftmann@30661 ` 8` ```imports Main (*FIXME: ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs.*) ``` chaieb@29835 ` 9` ```begin ``` chaieb@29835 ` 10` chaieb@29835 ` 11` ```definition hassize (infixr "hassize" 12) where ``` chaieb@29835 ` 12` ``` "(S hassize n) = (finite S \ card S = n)" ``` chaieb@29835 ` 13` chaieb@29835 ` 14` ```lemma hassize_image_inj: assumes f: "inj_on f S" and S: "S hassize n" ``` chaieb@29835 ` 15` ``` shows "f ` S hassize n" ``` chaieb@29835 ` 16` ``` using f S card_image[OF f] ``` chaieb@29835 ` 17` ``` by (simp add: hassize_def inj_on_def) ``` chaieb@29835 ` 18` chaieb@29835 ` 19` chaieb@29835 ` 20` ```subsection {* Finite Cartesian products, with indexing and lambdas. *} ``` chaieb@29835 ` 21` huffman@30582 ` 22` ```typedef (open Cart) ``` chaieb@29835 ` 23` ``` ('a, 'b) "^" (infixl "^" 15) ``` huffman@30582 ` 24` ``` = "UNIV :: ('b \ 'a) set" ``` huffman@30582 ` 25` ``` morphisms Cart_nth Cart_lambda .. ``` chaieb@29835 ` 26` huffman@30582 ` 27` ```notation Cart_nth (infixl "\$" 90) ``` chaieb@29835 ` 28` huffman@30582 ` 29` ```notation (xsymbols) Cart_lambda (binder "\" 10) ``` chaieb@29835 ` 30` chaieb@29835 ` 31` ```lemma stupid_ext: "(\x. f x = g x) \ (f = g)" ``` chaieb@29835 ` 32` ``` apply auto ``` chaieb@29835 ` 33` ``` apply (rule ext) ``` chaieb@29835 ` 34` ``` apply auto ``` chaieb@29835 ` 35` ``` done ``` chaieb@29835 ` 36` huffman@30582 ` 37` ```lemma Cart_eq: "((x:: 'a ^ 'b) = y) \ (\i. x\$i = y\$i)" ``` huffman@30582 ` 38` ``` by (simp add: Cart_nth_inject [symmetric] expand_fun_eq) ``` chaieb@29835 ` 39` huffman@30582 ` 40` ```lemma Cart_lambda_beta [simp]: "Cart_lambda g \$ i = g i" ``` huffman@30582 ` 41` ``` by (simp add: Cart_lambda_inverse) ``` chaieb@29835 ` 42` chaieb@29835 ` 43` ```lemma Cart_lambda_unique: ``` chaieb@29835 ` 44` ``` fixes f :: "'a ^ 'b" ``` huffman@30582 ` 45` ``` shows "(\i. f\$i = g i) \ Cart_lambda g = f" ``` huffman@30582 ` 46` ``` by (auto simp add: Cart_eq) ``` chaieb@29835 ` 47` huffman@30582 ` 48` ```lemma Cart_lambda_eta: "(\ i. (g\$i)) = g" ``` huffman@30582 ` 49` ``` by (simp add: Cart_eq) ``` chaieb@29835 ` 50` chaieb@29835 ` 51` ```text{* A non-standard sum to "paste" Cartesian products. *} ``` chaieb@29835 ` 52` huffman@30582 ` 53` ```definition pastecart :: "'a ^ 'm \ 'a ^ 'n \ 'a ^ ('m + 'n)" where ``` huffman@30582 ` 54` ``` "pastecart f g = (\ i. case i of Inl a \ f\$a | Inr b \ g\$b)" ``` huffman@30582 ` 55` huffman@30582 ` 56` ```definition fstcart:: "'a ^('m + 'n) \ 'a ^ 'm" where ``` huffman@30582 ` 57` ``` "fstcart f = (\ i. (f\$(Inl i)))" ``` chaieb@29835 ` 58` huffman@30582 ` 59` ```definition sndcart:: "'a ^('m + 'n) \ 'a ^ 'n" where ``` huffman@30582 ` 60` ``` "sndcart f = (\ i. (f\$(Inr i)))" ``` chaieb@29835 ` 61` huffman@30582 ` 62` ```lemma nth_pastecart_Inl [simp]: "pastecart f g \$ Inl a = f\$a" ``` huffman@30582 ` 63` ``` unfolding pastecart_def by simp ``` chaieb@29835 ` 64` huffman@30582 ` 65` ```lemma nth_pastecart_Inr [simp]: "pastecart f g \$ Inr b = g\$b" ``` huffman@30582 ` 66` ``` unfolding pastecart_def by simp ``` huffman@30582 ` 67` huffman@30582 ` 68` ```lemma nth_fstcart [simp]: "fstcart f \$ i = f \$ Inl i" ``` huffman@30582 ` 69` ``` unfolding fstcart_def by simp ``` chaieb@29835 ` 70` huffman@30582 ` 71` ```lemma nth_sndtcart [simp]: "sndcart f \$ i = f \$ Inr i" ``` huffman@30582 ` 72` ``` unfolding sndcart_def by simp ``` chaieb@29835 ` 73` huffman@30582 ` 74` ```lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \ range Inr" ``` huffman@30582 ` 75` ```by (auto, case_tac x, auto) ``` chaieb@29835 ` 76` chaieb@29835 ` 77` ```lemma fstcart_pastecart: "fstcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = x" ``` huffman@30582 ` 78` ``` by (simp add: Cart_eq) ``` chaieb@29835 ` 79` chaieb@29835 ` 80` ```lemma sndcart_pastecart: "sndcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = y" ``` huffman@30582 ` 81` ``` by (simp add: Cart_eq) ``` chaieb@29835 ` 82` chaieb@29835 ` 83` ```lemma pastecart_fst_snd: "pastecart (fstcart z) (sndcart z) = z" ``` huffman@30582 ` 84` ``` by (simp add: Cart_eq pastecart_def fstcart_def sndcart_def split: sum.split) ``` chaieb@29835 ` 85` chaieb@29835 ` 86` ```lemma pastecart_eq: "(x = y) \ (fstcart x = fstcart y) \ (sndcart x = sndcart y)" ``` chaieb@29835 ` 87` ``` using pastecart_fst_snd[of x] pastecart_fst_snd[of y] by metis ``` chaieb@29835 ` 88` chaieb@29835 ` 89` ```lemma forall_pastecart: "(\p. P p) \ (\x y. P (pastecart x y))" ``` chaieb@29835 ` 90` ``` by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart) ``` chaieb@29835 ` 91` chaieb@29835 ` 92` ```lemma exists_pastecart: "(\p. P p) \ (\x y. P (pastecart x y))" ``` chaieb@29835 ` 93` ``` by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart) ``` chaieb@29835 ` 94` chaieb@29835 ` 95` ```end ```