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