src/HOL/Old_Number_Theory/Finite2.thy
author wenzelm
Sat, 20 Aug 2011 23:36:18 +0200
changeset 44339 eda6aef75939
parent 41413 64cd30d6b0b8
child 44766 d4d33a4d7548
permissions -rw-r--r--
odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38159
e9b4835a54ee modernized specifications;
wenzelm
parents: 32479
diff changeset
     1
(*  Title:      HOL/Old_Number_Theory/Finite2.thy
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     2
    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     3
*)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     4
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     5
header {*Finite Sets and Finite Sums*}
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     6
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
     7
theory Finite2
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 40786
diff changeset
     8
imports IntFact "~~/src/HOL/Library/Infinite_Set"
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
     9
begin
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    10
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    11
text{*
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    12
  These are useful for combinatorial and number-theoretic counting
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    13
  arguments.
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    14
*}
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    15
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    16
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    17
subsection {* Useful properties of sums and products *}
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    18
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    19
lemma setsum_same_function_zcong:
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    20
  assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    21
  shows "[setsum f S = setsum g S] (mod m)"
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    22
proof cases
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    23
  assume "finite S"
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    24
  thus ?thesis using a by induct (simp_all add: zcong_zadd)
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    25
next
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    26
  assume "infinite S" thus ?thesis by(simp add:setsum_def)
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    27
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    28
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    29
lemma setprod_same_function_zcong:
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    30
  assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    31
  shows "[setprod f S = setprod g S] (mod m)"
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    32
proof cases
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    33
  assume "finite S"
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    34
  thus ?thesis using a by induct (simp_all add: zcong_zmult)
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    35
next
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    36
  assume "infinite S" thus ?thesis by(simp add:setprod_def)
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    37
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    38
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    39
lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
22274
ce1459004c8d Adapted to changes in Finite_Set theory.
berghofe
parents: 20809
diff changeset
    40
  apply (induct set: finite)
15047
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 14981
diff changeset
    41
  apply (auto simp add: left_distrib right_distrib int_eq_of_nat)
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 14981
diff changeset
    42
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    43
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    44
lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    45
    int(c) * int(card X)"
22274
ce1459004c8d Adapted to changes in Finite_Set theory.
berghofe
parents: 20809
diff changeset
    46
  apply (induct set: finite)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    47
  apply (auto simp add: zadd_zmult_distrib2)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    48
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    49
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    50
lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    51
    c * setsum f A"
22274
ce1459004c8d Adapted to changes in Finite_Set theory.
berghofe
parents: 20809
diff changeset
    52
  by (induct set: finite) (auto simp add: zadd_zmult_distrib2)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    53
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    54
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    55
subsection {* Cardinality of explicit finite sets *}
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    56
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    57
lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
40786
0a54cfc9add3 gave more standard finite set rules simp and intro attribute
nipkow
parents: 38159
diff changeset
    58
by (simp add: finite_subset)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    59
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    60
lemma bdd_nat_set_l_finite: "finite {y::nat . y < x}"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    61
  by (rule bounded_nat_set_is_finite) blast
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    62
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    63
lemma bdd_nat_set_le_finite: "finite {y::nat . y \<le> x}"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    64
proof -
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    65
  have "{y::nat . y \<le> x} = {y::nat . y < Suc x}" by auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    66
  then show ?thesis by (auto simp add: bdd_nat_set_l_finite)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    67
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    68
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    69
lemma  bdd_int_set_l_finite: "finite {x::int. 0 \<le> x & x < n}"
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    70
  apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq>
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    71
      int ` {(x :: nat). x < nat n}")
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    72
   apply (erule finite_surjI)
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    73
   apply (auto simp add: bdd_nat_set_l_finite image_def)
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    74
  apply (rule_tac x = "nat x" in exI, simp)
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    75
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    76
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    77
lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}"
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    78
  apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    79
   apply (erule ssubst)
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    80
   apply (rule bdd_int_set_l_finite)
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    81
  apply auto
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    82
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    83
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    84
lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    85
proof -
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    86
  have "{x::int. 0 < x & x < n} \<subseteq> {x::int. 0 \<le> x & x < n}"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    87
    by auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    88
  then show ?thesis by (auto simp add: bdd_int_set_l_finite finite_subset)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    89
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    90
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    91
lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x \<le> n}"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    92
proof -
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    93
  have "{x::int. 0 < x & x \<le> n} \<subseteq> {x::int. 0 \<le> x & x \<le> n}"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    94
    by auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    95
  then show ?thesis by (auto simp add: bdd_int_set_le_finite finite_subset)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    96
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    97
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
    98
lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
    99
proof (induct x)
20369
7e03c3ed1a18 tuned proofs;
wenzelm
parents: 20217
diff changeset
   100
  case 0
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   101
  show "card {y::nat . y < 0} = 0" by simp
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   102
next
20369
7e03c3ed1a18 tuned proofs;
wenzelm
parents: 20217
diff changeset
   103
  case (Suc n)
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   104
  have "{y. y < Suc n} = insert n {y. y < n}"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   105
    by auto
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   106
  then have "card {y. y < Suc n} = card (insert n {y. y < n})"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   107
    by auto
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   108
  also have "... = Suc (card {y. y < n})"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   109
    by (rule card_insert_disjoint) (auto simp add: bdd_nat_set_l_finite)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   110
  finally show "card {y. y < Suc n} = Suc n"
20369
7e03c3ed1a18 tuned proofs;
wenzelm
parents: 20217
diff changeset
   111
    using `card {y. y < n} = n` by simp
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   112
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   113
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   114
lemma card_bdd_nat_set_le: "card { y::nat. y \<le> x} = Suc x"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   115
proof -
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   116
  have "{y::nat. y \<le> x} = { y::nat. y < Suc x}"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   117
    by auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   118
  then show ?thesis by (auto simp add: card_bdd_nat_set_l)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   119
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   120
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   121
lemma card_bdd_int_set_l: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y < n} = nat n"
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   122
proof -
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   123
  assume "0 \<le> n"
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   124
  have "inj_on (%y. int y) {y. y < nat n}"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   125
    by (auto simp add: inj_on_def)
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   126
  hence "card (int ` {y. y < nat n}) = card {y. y < nat n}"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   127
    by (rule card_image)
20369
7e03c3ed1a18 tuned proofs;
wenzelm
parents: 20217
diff changeset
   128
  also from `0 \<le> n` have "int ` {y. y < nat n} = {y. 0 \<le> y & y < n}"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   129
    apply (auto simp add: zless_nat_eq_int_zless image_def)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   130
    apply (rule_tac x = "nat x" in exI)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   131
    apply (auto simp add: nat_0_le)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   132
    done
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   133
  also have "card {y. y < nat n} = nat n"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   134
    by (rule card_bdd_nat_set_l)
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   135
  finally show "card {y. 0 \<le> y & y < n} = nat n" .
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   136
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   137
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   138
lemma card_bdd_int_set_le: "0 \<le> (n::int) ==> card {y. 0 \<le> y & y \<le> n} =
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   139
  nat n + 1"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   140
proof -
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   141
  assume "0 \<le> n"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   142
  moreover have "{y. 0 \<le> y & y \<le> n} = {y. 0 \<le> y & y < n+1}" by auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   143
  ultimately show ?thesis
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   144
    using card_bdd_int_set_l [of "n + 1"]
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   145
    by (auto simp add: nat_add_distrib)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   146
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   147
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   148
lemma card_bdd_int_set_l_le: "0 \<le> (n::int) ==>
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   149
    card {x. 0 < x & x \<le> n} = nat n"
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   150
proof -
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   151
  assume "0 \<le> n"
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   152
  have "inj_on (%x. x+1) {x. 0 \<le> x & x < n}"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   153
    by (auto simp add: inj_on_def)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   154
  hence "card ((%x. x+1) ` {x. 0 \<le> x & x < n}) =
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   155
     card {x. 0 \<le> x & x < n}"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   156
    by (rule card_image)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   157
  also from `0 \<le> n` have "... = nat n"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   158
    by (rule card_bdd_int_set_l)
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   159
  also have "(%x. x + 1) ` {x. 0 \<le> x & x < n} = {x. 0 < x & x<= n}"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   160
    apply (auto simp add: image_def)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   161
    apply (rule_tac x = "x - 1" in exI)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   162
    apply arith
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   163
    done
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   164
  finally show "card {x. 0 < x & x \<le> n} = nat n" .
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   165
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   166
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   167
lemma card_bdd_int_set_l_l: "0 < (n::int) ==>
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   168
  card {x. 0 < x & x < n} = nat n - 1"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   169
proof -
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   170
  assume "0 < n"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   171
  moreover have "{x. 0 < x & x < n} = {x. 0 < x & x \<le> n - 1}"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   172
    by simp
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   173
  ultimately show ?thesis
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   174
    using insert card_bdd_int_set_l_le [of "n - 1"]
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   175
    by (auto simp add: nat_diff_distrib)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   176
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   177
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   178
lemma int_card_bdd_int_set_l_l: "0 < n ==>
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   179
    int(card {x. 0 < x & x < n}) = n - 1"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   180
  apply (auto simp add: card_bdd_int_set_l_l)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   181
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   182
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   183
lemma int_card_bdd_int_set_l_le: "0 \<le> n ==>
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   184
    int(card {x. 0 < x & x \<le> n}) = n"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   185
  by (auto simp add: card_bdd_int_set_l_le)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   186
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   187
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   188
subsection {* Cardinality of finite cartesian products *}
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   189
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   190
(* FIXME could be useful in general but not needed here
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   191
lemma insert_Sigma [simp]: "(insert x A) <*> B = ({ x } <*> B) \<union> (A <*> B)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   192
  by blast
15402
97204f3b4705 REorganized Finite_Set
nipkow
parents: 15392
diff changeset
   193
 *)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   194
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   195
text {* Lemmas for counting arguments. *}
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   196
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   197
lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   198
    g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A"
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   199
  apply (frule_tac h = g and f = f in setsum_reindex)
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   200
  apply (subgoal_tac "setsum g B = setsum g (f ` A)")
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   201
   apply (simp add: inj_on_def)
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   202
  apply (subgoal_tac "card A = card B")
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   203
   apply (drule_tac A = "f ` A" and B = B in card_seteq)
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   204
     apply (auto simp add: card_image)
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   205
  apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   206
  apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   207
    apply auto
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   208
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   209
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   210
lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   211
    g ` B \<subseteq> A; inj_on g B |] ==> setprod g B = setprod (g \<circ> f) A"
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15109
diff changeset
   212
  apply (frule_tac h = g and f = f in setprod_reindex)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   213
  apply (subgoal_tac "setprod g B = setprod g (f ` A)")
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   214
   apply (simp add: inj_on_def)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   215
  apply (subgoal_tac "card A = card B")
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   216
   apply (drule_tac A = "f ` A" and B = B in card_seteq)
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   217
     apply (auto simp add: card_image)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   218
  apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   219
  apply (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   220
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   221
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 15402
diff changeset
   222
end