src/HOL/NumberTheory/Finite2.thy
author paulson
Fri Mar 05 11:43:55 2004 +0100 (2004-03-05)
changeset 14434 5f14c1207499
parent 14430 5cb24165a2e1
child 14485 ea2707645af8
permissions -rw-r--r--
patch to NumberTheory problems caused by Parity
     1 (*  Title:      HOL/Quadratic_Reciprocity/Finite2.thy
     2     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     3     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4 *)
     5 
     6 header {*Finite Sets and Finite Sums*}
     7 
     8 theory Finite2 = Main + IntFact:;
     9 
    10 text{*These are useful for combinatorial and number-theoretic counting
    11 arguments.*}
    12 
    13 text{*Note.  This theory is being revised.  See the web page
    14 \url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
    15 
    16 (******************************************************************)
    17 (*                                                                *)
    18 (* gsetprod: A generalized set product function, for ints only.   *)
    19 (* Note that "setprod", as defined in IntFact, is equivalent to   *)
    20 (*   our "gsetprod id".                                           *) 
    21 (*                                                                *)
    22 (******************************************************************)
    23 
    24 consts
    25   gsetprod :: "('a => int) => 'a set => int"
    26 
    27 defs
    28   gsetprod_def: "gsetprod f A ==  if finite A then fold (op * o f) 1 A else 1";
    29 
    30 lemma gsetprod_empty [simp]: "gsetprod f {} = 1";
    31   by (auto simp add: gsetprod_def)
    32 
    33 lemma gsetprod_insert [simp]: "[| finite A; a \<notin> A |] ==> 
    34     gsetprod f (insert a A) = f a * gsetprod f A";
    35   by (simp add: gsetprod_def LC_def LC.fold_insert)
    36 
    37 (******************************************************************)
    38 (*                                                                *)
    39 (* Useful properties of sums and products                         *)
    40 (*                                                                *)
    41 (******************************************************************);
    42 
    43 subsection {* Useful properties of sums and products *}
    44 
    45 lemma setprod_gsetprod_id: "setprod A = gsetprod id A";
    46   by (auto simp add: setprod_def gsetprod_def)
    47 
    48 lemma setsum_same_function: "[| finite S; \<forall>x \<in> S. f x = g x |] ==> 
    49     setsum f S = setsum g S";
    50 by (induct set: Finites, auto)
    51 
    52 lemma gsetprod_same_function: "[| finite S; \<forall>x \<in> S. f x = g x |] ==> 
    53   gsetprod f S = gsetprod g S";
    54 by (induct set: Finites, auto)
    55 
    56 lemma setsum_same_function_zcong: 
    57    "[| finite S; \<forall>x \<in> S. [f x = g x](mod m) |] 
    58      ==> [setsum f S = setsum g S] (mod m)";
    59    by (induct set: Finites, auto simp add: zcong_zadd)
    60 
    61 lemma gsetprod_same_function_zcong: 
    62    "[| finite S; \<forall>x \<in> S. [f x = g x](mod m) |] 
    63      ==> [gsetprod f S = gsetprod g S] (mod m)";
    64 by (induct set: Finites, auto simp add: zcong_zmult)
    65 
    66 lemma gsetprod_Un_Int: "finite A ==> finite B
    67     ==> gsetprod g (A \<union> B) * gsetprod g (A \<inter> B) = 
    68     gsetprod g A * gsetprod g B";
    69   apply (induct set: Finites)
    70 by (auto simp add: Int_insert_left insert_absorb)
    71 
    72 lemma gsetprod_Un_disjoint: "[| finite A; finite B; A \<inter> B = {} |] ==> 
    73     gsetprod g (A \<union> B) = gsetprod g A * gsetprod g B";
    74   apply (subst gsetprod_Un_Int [symmetric])
    75 by auto
    76 
    77 lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)";
    78   apply (induct set: Finites)
    79 by (auto simp add: zadd_zmult_distrib2)
    80 
    81 lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) = 
    82     int(c) * int(card X)";
    83   apply (induct set: Finites)
    84   apply (auto simp add: zadd_zmult_distrib2)
    85 done
    86 
    87 lemma setsum_minus: "finite A ==> setsum (%x. ((f x)::int) - g x) A = 
    88   setsum f A - setsum g A";
    89   by (induct set: Finites, auto)
    90 
    91 lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A = 
    92     c * setsum f A";
    93   apply (induct set: Finites, auto)
    94   by (auto simp only: zadd_zmult_distrib2) 
    95 
    96 lemma setsum_non_neg: "[| finite A; \<forall>x \<in> A. (0::int) \<le> f x |] ==>
    97     0 \<le>  setsum f A";
    98   by (induct set: Finites, auto)
    99 
   100 lemma gsetprod_const: "finite X ==> gsetprod (%x. (c :: int)) X = c ^ (card X)";
   101   apply (induct set: Finites)
   102 by auto
   103 
   104 (******************************************************************)
   105 (*                                                                *)
   106 (* Cardinality of some explicit finite sets                       *)
   107 (*                                                                *)
   108 (******************************************************************);
   109 
   110 subsection {* Cardinality of explicit finite sets *}
   111 
   112 lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B";
   113 by (simp add: finite_subset finite_imageI)
   114 
   115 lemma bdd_nat_set_l_finite: "finite { y::nat . y < x}";
   116 apply (rule_tac N = "{y. y < x}" and n = x in bounded_nat_set_is_finite)
   117 by auto
   118 
   119 lemma bdd_nat_set_le_finite: "finite { y::nat . y \<le> x  }";
   120 apply (subgoal_tac "{ y::nat . y \<le> x  } = { y::nat . y < Suc x}")
   121 by (auto simp add: bdd_nat_set_l_finite)
   122 
   123 lemma  bdd_int_set_l_finite: "finite { x::int . 0 \<le> x & x < n}";
   124 apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq> 
   125     int ` {(x :: nat). x < nat n}");
   126 apply (erule finite_surjI)
   127 apply (auto simp add: bdd_nat_set_l_finite image_def)
   128 apply (rule_tac x = "nat x" in exI, simp) 
   129 done
   130 
   131 lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}";
   132 apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
   133 apply (erule ssubst)
   134 apply (rule bdd_int_set_l_finite)
   135 by auto
   136 
   137 lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}";
   138 apply (subgoal_tac "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}")
   139 by (auto simp add: bdd_int_set_l_finite finite_subset)
   140 
   141 lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}";
   142 apply (subgoal_tac "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}")
   143 by (auto simp add: bdd_int_set_le_finite finite_subset)
   144 
   145 lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x";
   146 apply (induct_tac x, force)
   147 proof -;
   148   fix n::nat;
   149   assume "card {y. y < n} = n"; 
   150   have "{y. y < Suc n} = insert n {y. y < n}";
   151     by auto
   152   then have "card {y. y < Suc n} = card (insert n {y. y < n})";
   153     by auto
   154   also have "... = Suc (card {y. y < n})";
   155     apply (rule card_insert_disjoint)
   156     by (auto simp add: bdd_nat_set_l_finite)
   157   finally show "card {y. y < Suc n} = Suc n"; 
   158     by (simp add: prems)
   159 qed;
   160 
   161 lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x";
   162 apply (subgoal_tac "{ y::nat. y \<le> x} = { y::nat. y < Suc x}")
   163 by (auto simp add: card_bdd_nat_set_l)
   164 
   165 lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n";
   166 proof -;
   167   fix n::int;
   168   assume "0 \<le> n";
   169   have "finite {y. y < nat n}";
   170     by (rule bdd_nat_set_l_finite)
   171   moreover have "inj_on (%y. int y) {y. y < nat n}";
   172     by (auto simp add: inj_on_def)
   173   ultimately have "card (int ` {y. y < nat n}) = card {y. y < nat n}";
   174     by (rule card_image)
   175   also from prems have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}";
   176     apply (auto simp add: zless_nat_eq_int_zless image_def)
   177     apply (rule_tac x = "nat x" in exI)
   178     by (auto simp add: nat_0_le)
   179   also; have "card {y. y < nat n} = nat n" 
   180     by (rule card_bdd_nat_set_l)
   181   finally show "card {y. 0 \<le> y & y < n} = nat n"; .;
   182 qed;
   183 
   184 lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} = 
   185   nat n + 1";
   186 apply (subgoal_tac "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}")
   187 apply (insert card_bdd_int_set_l [of "n+1"])
   188 by (auto simp add: nat_add_distrib)
   189 
   190 lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==> 
   191     card {x. 0 < x & x \<le> n} = nat n";
   192 proof -;
   193   fix n::int;
   194   assume "0 \<le> n";
   195   have "finite {x. 0 \<le> x & x < n}";
   196     by (rule bdd_int_set_l_finite)
   197   moreover have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}";
   198     by (auto simp add: inj_on_def)
   199   ultimately have "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) = 
   200      card {x. 0 \<le> x & x < n}";
   201     by (rule card_image)
   202   also from prems have "... = nat n";
   203     by (rule card_bdd_int_set_l)
   204   also; have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}";
   205     apply (auto simp add: image_def)
   206     apply (rule_tac x = "x - 1" in exI)
   207     by arith
   208   finally; show "card {x. 0 < x & x \<le> n} = nat n";.;
   209 qed;
   210 
   211 lemma card_bdd_int_set_l_l: "0 < (n::int) ==> 
   212     card {x. 0 < x & x < n} = nat n - 1";
   213   apply (subgoal_tac "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}")
   214   apply (insert card_bdd_int_set_l_le [of "n - 1"])
   215   by (auto simp add: nat_diff_distrib)
   216 
   217 lemma int_card_bdd_int_set_l_l: "0 < n ==> 
   218     int(card {x. 0 < x & x < n}) = n - 1";
   219   apply (auto simp add: card_bdd_int_set_l_l)
   220   apply (subgoal_tac "Suc 0 \<le> nat n")
   221   apply (auto simp add: zdiff_int [THEN sym])
   222   apply (subgoal_tac "0 < nat n", arith)
   223   by (simp add: zero_less_nat_eq)
   224 
   225 lemma int_card_bdd_int_set_l_le: "0 \<le> n ==> 
   226     int(card {x. 0 < x & x \<le> n}) = n";
   227   by (auto simp add: card_bdd_int_set_l_le)
   228 
   229 (******************************************************************)
   230 (*                                                                *)
   231 (* Cartesian products of finite sets                              *)
   232 (*                                                                *)
   233 (******************************************************************)
   234 
   235 subsection {* Cardinality of finite cartesian products *}
   236 
   237 lemma insert_Sigma [simp]: "~(A = {}) ==>
   238   (insert x A) <*> B = ({ x } <*> B) \<union> (A <*> B)";
   239   by blast
   240 
   241 lemma cartesian_product_finite: "[| finite A; finite B |] ==> 
   242     finite (A <*> B)";
   243   apply (rule_tac F = A in finite_induct)
   244   by auto
   245 
   246 lemma cartesian_product_card_a [simp]: "finite A ==> 
   247     card({x} <*> A) = card(A)"; 
   248   apply (subgoal_tac "inj_on (%y .(x,y)) A");
   249   apply (frule card_image, assumption)
   250   apply (subgoal_tac "(Pair x ` A) = {x} <*> A");
   251   by (auto simp add: inj_on_def)
   252 
   253 lemma cartesian_product_card [simp]: "[| finite A; finite B |] ==> 
   254   card (A <*> B) = card(A) * card(B)";
   255   apply (rule_tac F = A in finite_induct, auto)
   256   done
   257 
   258 (******************************************************************)
   259 (*                                                                *)
   260 (* Sums and products over finite sets                             *)
   261 (*                                                                *)
   262 (******************************************************************)
   263 
   264 subsection {* Reindexing sums and products *}
   265 
   266 lemma sum_prop [rule_format]: "finite B ==>
   267                   inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B";
   268 apply (rule finite_induct, assumption, force)
   269 apply (rule impI, auto)
   270 apply (simp add: inj_on_def)
   271 apply (subgoal_tac "f x \<notin> f ` F")
   272 apply (subgoal_tac "finite (f ` F)");
   273 apply (auto simp add: setsum_insert)
   274 by (simp add: inj_on_def) 
   275 
   276 lemma sum_prop_id: "finite B ==> inj_on f B ==> 
   277     setsum f B = setsum id (f ` B)";
   278 by (auto simp add: sum_prop id_o)
   279 
   280 lemma prod_prop [rule_format]: "finite B ==>
   281         inj_on f B --> gsetprod h (f ` B) = gsetprod (h \<circ> f) B";
   282   apply (rule finite_induct, assumption, force)
   283   apply (rule impI)
   284   apply (auto simp add: inj_on_def)
   285   apply (subgoal_tac "f x \<notin> f ` F")
   286   apply (subgoal_tac "finite (f ` F)");
   287 by (auto simp add: gsetprod_insert)
   288 
   289 lemma prod_prop_id: "[| finite B; inj_on f B |] ==> 
   290     gsetprod id (f ` B) = (gsetprod f B)";
   291   by (simp add: prod_prop id_o)
   292 
   293 subsection {* Lemmas for counting arguments *}
   294 
   295 lemma finite_union_finite_subsets: "[| finite A; \<forall>X \<in> A. finite X |] ==> 
   296     finite (Union A)";
   297 apply (induct set: Finites)
   298 by auto
   299 
   300 lemma finite_index_UNION_finite_sets: "finite A ==> 
   301     (\<forall>x \<in> A. finite (f x)) --> finite (UNION A f)";
   302 by (induct_tac rule: finite_induct, auto)
   303 
   304 lemma card_union_disjoint_sets: "finite A ==> 
   305     ((\<forall>X \<in> A. finite X) & (\<forall>X \<in> A. \<forall>Y \<in> A. X \<noteq> Y --> X \<inter> Y = {})) ==> 
   306     card (Union A) = setsum card A";
   307   apply auto
   308   apply (induct set: Finites, auto)
   309   apply (frule_tac B = "Union F" and A = x in card_Un_Int)
   310 by (auto simp add: finite_union_finite_subsets)
   311 
   312 (*
   313   We just duplicated something in the standard library: the next lemma 
   314   is setsum_UN_disjoint in Finite_Set
   315 
   316 lemma setsum_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
   317     ((\<forall>x \<in> A. finite (g x)) & 
   318     (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) --> 
   319       setsum f (UNION A g) = setsum (%x. setsum f (g x)) A";
   320 apply (induct_tac rule: finite_induct)
   321 apply (assumption, simp, clarify)
   322 apply (subgoal_tac "g x \<inter> (UNION F g) = {}");
   323 apply (subgoal_tac "finite (UNION F g)");
   324 apply (simp add: setsum_Un_disjoint)
   325 by (auto simp add: finite_index_UNION_finite_sets)
   326 
   327 *)
   328 
   329 lemma int_card_eq_setsum [rule_format]: "finite A ==> 
   330     int (card A) = setsum (%x. 1) A";
   331   by (erule finite_induct, auto)
   332 
   333 lemma card_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
   334     ((\<forall>x \<in> A. finite (g x)) & 
   335     (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) --> 
   336       card (UNION A g) = setsum (%x. card (g x)) A";
   337 apply clarify
   338 apply (frule_tac f = "%x.(1::nat)" and A = g in 
   339     setsum_UN_disjoint);
   340 apply assumption+;
   341 apply (subgoal_tac "finite (UNION A g)");
   342 apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)");
   343 apply (auto simp only: card_eq_setsum)
   344 apply (erule setsum_same_function)
   345 by (auto simp add: card_eq_setsum)
   346 
   347 lemma int_card_indexed_union_disjoint_sets [rule_format]: "finite A ==> 
   348     ((\<forall>x \<in> A. finite (g x)) & 
   349     (\<forall>x \<in> A. \<forall>y \<in> A. x \<noteq> y --> (g x) \<inter> (g y) = {})) --> 
   350        int(card (UNION A g)) = setsum (%x. int( card (g x))) A";
   351 apply clarify
   352 apply (frule_tac f = "%x.(1::int)" and A = g in 
   353     setsum_UN_disjoint);
   354 apply assumption+;
   355 apply (subgoal_tac "finite (UNION A g)");
   356 apply (subgoal_tac "(\<Sum>x \<in> UNION A g. 1) = (\<Sum>x \<in> A. \<Sum>x \<in> g x. 1)");
   357 apply (auto simp only: int_card_eq_setsum)
   358 apply (erule setsum_same_function)
   359 by (auto simp add: int_card_eq_setsum)
   360 
   361 lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; 
   362     g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A";
   363 apply (frule_tac h = g and f = f in sum_prop, auto)
   364 apply (subgoal_tac "setsum g B = setsum g (f ` A)");
   365 apply (simp add: inj_on_def)
   366 apply (subgoal_tac "card A = card B")
   367 apply (drule_tac A = "f ` A" and B = B in card_seteq)
   368 apply (auto simp add: card_image)
   369 apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
   370 apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
   371 by auto
   372 
   373 lemma gsetprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A; 
   374     g ` B \<subseteq> A; inj_on g B |] ==> gsetprod g B = gsetprod (g \<circ> f) A";
   375   apply (frule_tac h = g and f = f in prod_prop, auto) 
   376   apply (subgoal_tac "gsetprod g B = gsetprod g (f ` A)"); 
   377   apply (simp add: inj_on_def)
   378   apply (subgoal_tac "card A = card B")
   379   apply (drule_tac A = "f ` A" and B = B in card_seteq)
   380   apply (auto simp add: card_image)
   381   apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
   382 by (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
   383 
   384 lemma setsum_union_disjoint_sets [rule_format]: "finite A ==> 
   385     ((\<forall>X \<in> A. finite X) & (\<forall>X \<in> A. \<forall>Y \<in> A. X \<noteq> Y --> X \<inter> Y = {})) 
   386     --> setsum f (Union A) = setsum (%x. setsum f x) A";
   387 apply (induct_tac rule: finite_induct)
   388 apply (assumption, simp, clarify)
   389 apply (subgoal_tac "x \<inter> (Union F) = {}");
   390 apply (subgoal_tac "finite (Union F)");
   391   by (auto simp add: setsum_Un_disjoint Union_def)
   392 
   393 lemma gsetprod_union_disjoint_sets [rule_format]: "[| 
   394     finite (A :: int set set); 
   395     (\<forall>X \<in> A. finite (X :: int set));
   396     (\<forall>X \<in> A. (\<forall>Y \<in> A. (X :: int set) \<noteq> (Y :: int set) --> 
   397       (X \<inter> Y) = {})) |] ==> 
   398   ( gsetprod (f :: int => int) (Union A) = gsetprod (%x. gsetprod f x) A)";
   399   apply (induct set: Finites)
   400   apply (auto simp add: gsetprod_empty) 
   401   apply (subgoal_tac "gsetprod f (x \<union> Union F) = 
   402     gsetprod f x * gsetprod f (Union F)");
   403   apply simp
   404   apply (rule gsetprod_Un_disjoint)
   405 by (auto simp add: gsetprod_Un_disjoint Union_def)
   406 
   407 lemma gsetprod_disjoint_sets: "[| finite A;
   408     \<forall>X \<in> A. finite X; 
   409     \<forall>X \<in> A. \<forall>Y \<in> A. (X \<noteq> Y --> X \<inter> Y = {}) |] ==> 
   410   gsetprod id (Union A) = gsetprod (gsetprod id) A";
   411   apply (rule_tac f = id in gsetprod_union_disjoint_sets)
   412   by auto
   413 
   414 lemma setprod_disj_sets: "[| finite (A::int set set);
   415     \<forall>X \<in> A. finite X;
   416     \<forall>X \<in> A. \<forall>Y \<in> A. (X \<noteq> Y --> X \<inter> Y = {}) |] ==> 
   417   setprod (Union A) = gsetprod (%x. setprod x) A";
   418   by (auto simp add: setprod_gsetprod_id gsetprod_disjoint_sets)
   419 
   420 end;