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