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