src/HOL/Number_Theory/Binomial.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 44872 a98ef45122f3
child 45933 ee70da42e08a
permissions -rw-r--r--
Quotient_Info stores only relation maps
wenzelm@41959
     1
(*  Title:      HOL/Number_Theory/Binomial.thy
nipkow@31719
     2
    Authors:    Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow
nipkow@31719
     3
avigad@32036
     4
Defines the "choose" function, and establishes basic properties.
nipkow@31719
     5
nipkow@31719
     6
The original theory "Binomial" was by Lawrence C. Paulson, based on
nipkow@31719
     7
the work of Andy Gordon and Florian Kammueller. The approach here,
nipkow@31719
     8
which derives the definition of binomial coefficients in terms of the
nipkow@31719
     9
factorial function, is due to Jeremy Avigad. The binomial theorem was
nipkow@31719
    10
formalized by Tobias Nipkow.
nipkow@31719
    11
*)
nipkow@31719
    12
nipkow@31719
    13
header {* Binomial *}
nipkow@31719
    14
nipkow@31719
    15
theory Binomial
avigad@32036
    16
imports Cong Fact
nipkow@31719
    17
begin
nipkow@31719
    18
nipkow@31719
    19
nipkow@31719
    20
subsection {* Main definitions *}
nipkow@31719
    21
nipkow@31719
    22
class binomial =
wenzelm@44872
    23
  fixes binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
nipkow@31719
    24
nipkow@31719
    25
(* definitions for the natural numbers *)
nipkow@31719
    26
nipkow@31719
    27
instantiation nat :: binomial
nipkow@31719
    28
begin 
nipkow@31719
    29
wenzelm@44872
    30
fun binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
nipkow@31719
    31
where
nipkow@31719
    32
  "binomial_nat n k =
nipkow@31719
    33
   (if k = 0 then 1 else
nipkow@31719
    34
    if n = 0 then 0 else
nipkow@31719
    35
      (binomial (n - 1) k) + (binomial (n - 1) (k - 1)))"
nipkow@31719
    36
wenzelm@44872
    37
instance ..
nipkow@31719
    38
nipkow@31719
    39
end
nipkow@31719
    40
nipkow@31719
    41
(* definitions for the integers *)
nipkow@31719
    42
nipkow@31719
    43
instantiation int :: binomial
nipkow@31719
    44
begin 
nipkow@31719
    45
wenzelm@44872
    46
definition binomial_int :: "int => int \<Rightarrow> int" where
wenzelm@44872
    47
  "binomial_int n k =
wenzelm@44872
    48
   (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
wenzelm@44872
    49
    else 0)"
wenzelm@44872
    50
wenzelm@44872
    51
instance ..
nipkow@31719
    52
nipkow@31719
    53
end
nipkow@31719
    54
nipkow@31719
    55
nipkow@31719
    56
subsection {* Set up Transfer *}
nipkow@31719
    57
nipkow@31719
    58
lemma transfer_nat_int_binomial:
nipkow@31719
    59
  "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow> binomial (nat n) (nat k) = 
nipkow@31719
    60
      nat (binomial n k)"
avigad@32036
    61
  unfolding binomial_int_def 
nipkow@31719
    62
  by auto
nipkow@31719
    63
avigad@32036
    64
lemma transfer_nat_int_binomial_closure:
nipkow@31719
    65
  "n >= (0::int) \<Longrightarrow> k >= 0 \<Longrightarrow> binomial n k >= 0"
avigad@32036
    66
  by (auto simp add: binomial_int_def)
nipkow@31719
    67
haftmann@35644
    68
declare transfer_morphism_nat_int[transfer add return: 
avigad@32036
    69
    transfer_nat_int_binomial transfer_nat_int_binomial_closure]
nipkow@31719
    70
nipkow@31719
    71
lemma transfer_int_nat_binomial:
nipkow@31719
    72
  "binomial (int n) (int k) = int (binomial n k)"
nipkow@31719
    73
  unfolding fact_int_def binomial_int_def by auto
nipkow@31719
    74
avigad@32036
    75
lemma transfer_int_nat_binomial_closure:
nipkow@31719
    76
  "is_nat n \<Longrightarrow> is_nat k \<Longrightarrow> binomial n k >= 0"
avigad@32036
    77
  by (auto simp add: binomial_int_def)
nipkow@31719
    78
haftmann@35644
    79
declare transfer_morphism_int_nat[transfer add return: 
avigad@32036
    80
    transfer_int_nat_binomial transfer_int_nat_binomial_closure]
nipkow@31719
    81
nipkow@31719
    82
nipkow@31719
    83
subsection {* Binomial coefficients *}
nipkow@31719
    84
nipkow@31952
    85
lemma choose_zero_nat [simp]: "(n::nat) choose 0 = 1"
nipkow@31719
    86
  by simp
nipkow@31719
    87
nipkow@31952
    88
lemma choose_zero_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 0 = 1"
nipkow@31719
    89
  by (simp add: binomial_int_def)
nipkow@31719
    90
nipkow@31952
    91
lemma zero_choose_nat [rule_format,simp]: "ALL (k::nat) > n. n choose k = 0"
nipkow@31952
    92
  by (induct n rule: induct'_nat, auto)
nipkow@31719
    93
nipkow@31952
    94
lemma zero_choose_int [rule_format,simp]: "(k::int) > n \<Longrightarrow> n choose k = 0"
wenzelm@44872
    95
  unfolding binomial_int_def
wenzelm@44872
    96
  apply (cases "n < 0")
nipkow@31719
    97
  apply force
nipkow@31719
    98
  apply (simp del: binomial_nat.simps)
wenzelm@44872
    99
  done
nipkow@31719
   100
nipkow@31952
   101
lemma choose_reduce_nat: "(n::nat) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
nipkow@31719
   102
    (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
nipkow@31719
   103
  by simp
nipkow@31719
   104
nipkow@31952
   105
lemma choose_reduce_int: "(n::int) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
nipkow@31719
   106
    (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
wenzelm@44872
   107
  unfolding binomial_int_def
wenzelm@44872
   108
  apply (subst choose_reduce_nat)
wenzelm@44872
   109
    apply (auto simp del: binomial_nat.simps simp add: nat_diff_distrib)
wenzelm@44872
   110
  done
nipkow@31719
   111
nipkow@31952
   112
lemma choose_plus_one_nat: "((n::nat) + 1) choose (k + 1) = 
nipkow@31719
   113
    (n choose (k + 1)) + (n choose k)"
nipkow@31952
   114
  by (simp add: choose_reduce_nat)
nipkow@31719
   115
nipkow@31952
   116
lemma choose_Suc_nat: "(Suc n) choose (Suc k) = 
nipkow@31719
   117
    (n choose (Suc k)) + (n choose k)"
nipkow@31952
   118
  by (simp add: choose_reduce_nat One_nat_def)
nipkow@31719
   119
nipkow@31952
   120
lemma choose_plus_one_int: "n \<ge> 0 \<Longrightarrow> k \<ge> 0 \<Longrightarrow> ((n::int) + 1) choose (k + 1) = 
nipkow@31719
   121
    (n choose (k + 1)) + (n choose k)"
nipkow@31952
   122
  by (simp add: binomial_int_def choose_plus_one_nat nat_add_distrib del: binomial_nat.simps)
nipkow@31719
   123
nipkow@31719
   124
declare binomial_nat.simps [simp del]
nipkow@31719
   125
nipkow@31952
   126
lemma choose_self_nat [simp]: "((n::nat) choose n) = 1"
wenzelm@44872
   127
  by (induct n rule: induct'_nat) (auto simp add: choose_plus_one_nat)
nipkow@31719
   128
nipkow@31952
   129
lemma choose_self_int [simp]: "n \<ge> 0 \<Longrightarrow> ((n::int) choose n) = 1"
nipkow@31719
   130
  by (auto simp add: binomial_int_def)
nipkow@31719
   131
nipkow@31952
   132
lemma choose_one_nat [simp]: "(n::nat) choose 1 = n"
wenzelm@44872
   133
  by (induct n rule: induct'_nat) (auto simp add: choose_reduce_nat)
nipkow@31719
   134
nipkow@31952
   135
lemma choose_one_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 1 = n"
nipkow@31719
   136
  by (auto simp add: binomial_int_def)
nipkow@31719
   137
nipkow@31952
   138
lemma plus_one_choose_self_nat [simp]: "(n::nat) + 1 choose n = n + 1"
nipkow@31952
   139
  apply (induct n rule: induct'_nat, force)
nipkow@31719
   140
  apply (case_tac "n = 0")
nipkow@31719
   141
  apply auto
nipkow@31952
   142
  apply (subst choose_reduce_nat)
nipkow@31719
   143
  apply (auto simp add: One_nat_def)  
nipkow@31719
   144
  (* natdiff_cancel_numerals introduces Suc *)
nipkow@31719
   145
done
nipkow@31719
   146
nipkow@31952
   147
lemma Suc_choose_self_nat [simp]: "(Suc n) choose n = Suc n"
nipkow@31952
   148
  using plus_one_choose_self_nat by (simp add: One_nat_def)
nipkow@31719
   149
nipkow@31952
   150
lemma plus_one_choose_self_int [rule_format, simp]: 
nipkow@31719
   151
    "(n::int) \<ge> 0 \<longrightarrow> n + 1 choose n = n + 1"
nipkow@31719
   152
   by (auto simp add: binomial_int_def nat_add_distrib)
nipkow@31719
   153
nipkow@31719
   154
(* bounded quantification doesn't work with the unicode characters? *)
nipkow@31952
   155
lemma choose_pos_nat [rule_format]: "ALL k <= (n::nat). 
nipkow@31719
   156
    ((n::nat) choose k) > 0"
nipkow@31952
   157
  apply (induct n rule: induct'_nat) 
nipkow@31719
   158
  apply force
nipkow@31719
   159
  apply clarify
nipkow@31719
   160
  apply (case_tac "k = 0")
nipkow@31719
   161
  apply force
nipkow@31952
   162
  apply (subst choose_reduce_nat)
nipkow@31719
   163
  apply auto
wenzelm@44872
   164
  done
nipkow@31719
   165
nipkow@31952
   166
lemma choose_pos_int: "n \<ge> 0 \<Longrightarrow> k >= 0 \<Longrightarrow> k \<le> n \<Longrightarrow>
nipkow@31719
   167
    ((n::int) choose k) > 0"
nipkow@31952
   168
  by (auto simp add: binomial_int_def choose_pos_nat)
nipkow@31719
   169
nipkow@31719
   170
lemma binomial_induct [rule_format]: "(ALL (n::nat). P n n) \<longrightarrow> 
nipkow@31719
   171
    (ALL n. P (n + 1) 0) \<longrightarrow> (ALL n. (ALL k < n. P n k \<longrightarrow> P n (k + 1) \<longrightarrow>
nipkow@31719
   172
    P (n + 1) (k + 1))) \<longrightarrow> (ALL k <= n. P n k)"
nipkow@31952
   173
  apply (induct n rule: induct'_nat)
nipkow@31719
   174
  apply auto
nipkow@31719
   175
  apply (case_tac "k = 0")
nipkow@31719
   176
  apply auto
nipkow@31719
   177
  apply (case_tac "k = n + 1")
nipkow@31719
   178
  apply auto
nipkow@31719
   179
  apply (drule_tac x = n in spec) back back 
nipkow@31719
   180
  apply (drule_tac x = "k - 1" in spec) back back back
nipkow@31719
   181
  apply auto
wenzelm@44872
   182
  done
nipkow@31719
   183
nipkow@31952
   184
lemma choose_altdef_aux_nat: "(k::nat) \<le> n \<Longrightarrow> 
nipkow@31719
   185
    fact k * fact (n - k) * (n choose k) = fact n"
nipkow@31719
   186
  apply (rule binomial_induct [of _ k n])
nipkow@31719
   187
  apply auto
nipkow@31719
   188
proof -
nipkow@31719
   189
  fix k :: nat and n
nipkow@31719
   190
  assume less: "k < n"
nipkow@31719
   191
  assume ih1: "fact k * fact (n - k) * (n choose k) = fact n"
wenzelm@44872
   192
  then have one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n"
nipkow@31952
   193
    by (subst fact_plus_one_nat, auto)
wenzelm@44872
   194
  assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) =  fact n"
nipkow@31719
   195
  with less have "fact (k + 1) * fact ((n - (k + 1)) + 1) * 
nipkow@31719
   196
      (n choose (k + 1)) = (n - k) * fact n"
nipkow@31952
   197
    by (subst (2) fact_plus_one_nat, auto)
nipkow@31719
   198
  with less have two: "fact (k + 1) * fact (n - k) * (n choose (k + 1)) = 
nipkow@31719
   199
      (n - k) * fact n" by simp
nipkow@31719
   200
  have "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) =
nipkow@31719
   201
      fact (k + 1) * fact (n - k) * (n choose (k + 1)) + 
nipkow@31719
   202
      fact (k + 1) * fact (n - k) * (n choose k)" 
haftmann@36350
   203
    by (subst choose_reduce_nat, auto simp add: field_simps)
nipkow@31719
   204
  also note one
nipkow@31719
   205
  also note two
nipkow@31719
   206
  also with less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)" 
nipkow@31952
   207
    apply (subst fact_plus_one_nat)
nipkow@31719
   208
    apply (subst left_distrib [symmetric])
nipkow@31719
   209
    apply simp
nipkow@31719
   210
    done
nipkow@31719
   211
  finally show "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) = 
nipkow@31719
   212
    fact (n + 1)" .
nipkow@31719
   213
qed
nipkow@31719
   214
nipkow@31952
   215
lemma choose_altdef_nat: "(k::nat) \<le> n \<Longrightarrow> 
nipkow@31719
   216
    n choose k = fact n div (fact k * fact (n - k))"
nipkow@31952
   217
  apply (frule choose_altdef_aux_nat)
nipkow@31719
   218
  apply (erule subst)
nipkow@31719
   219
  apply (simp add: mult_ac)
wenzelm@44872
   220
  done
nipkow@31719
   221
nipkow@31719
   222
nipkow@31952
   223
lemma choose_altdef_int: 
nipkow@31719
   224
  assumes "(0::int) <= k" and "k <= n"
nipkow@31719
   225
  shows "n choose k = fact n div (fact k * fact (n - k))"
wenzelm@41541
   226
  apply (subst tsub_eq [symmetric], rule assms)
nipkow@31952
   227
  apply (rule choose_altdef_nat [transferred])
wenzelm@41541
   228
  using assms apply auto
wenzelm@41541
   229
  done
nipkow@31719
   230
nipkow@31952
   231
lemma choose_dvd_nat: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
nipkow@31952
   232
  unfolding dvd_def apply (frule choose_altdef_aux_nat)
nipkow@31719
   233
  (* why don't blast and auto get this??? *)
nipkow@31719
   234
  apply (rule exI)
nipkow@31719
   235
  apply (erule sym)
wenzelm@44872
   236
  done
nipkow@31719
   237
nipkow@31952
   238
lemma choose_dvd_int: 
nipkow@31719
   239
  assumes "(0::int) <= k" and "k <= n"
nipkow@31719
   240
  shows "fact k * fact (n - k) dvd fact n"
wenzelm@41541
   241
  apply (subst tsub_eq [symmetric], rule assms)
nipkow@31952
   242
  apply (rule choose_dvd_nat [transferred])
wenzelm@41541
   243
  using assms apply auto
wenzelm@41541
   244
  done
nipkow@31719
   245
nipkow@31719
   246
(* generalizes Tobias Nipkow's proof to any commutative semiring *)
nipkow@31719
   247
theorem binomial: "(a+b::'a::{comm_ring_1,power})^n = 
nipkow@31719
   248
  (SUM k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" (is "?P n")
nipkow@31952
   249
proof (induct n rule: induct'_nat)
nipkow@31719
   250
  show "?P 0" by simp
nipkow@31719
   251
next
nipkow@31719
   252
  fix n
nipkow@31719
   253
  assume ih: "?P n"
nipkow@31719
   254
  have decomp: "{0..n+1} = {0} Un {n+1} Un {1..n}"
nipkow@31719
   255
    by auto
nipkow@31719
   256
  have decomp2: "{0..n} = {0} Un {1..n}"
nipkow@31719
   257
    by auto
nipkow@31719
   258
  have decomp3: "{1..n+1} = {n+1} Un {1..n}"
nipkow@31719
   259
    by auto
nipkow@31719
   260
  have "(a+b)^(n+1) = 
nipkow@31719
   261
      (a+b) * (SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
wenzelm@41541
   262
    using ih by simp
nipkow@31719
   263
  also have "... =  a*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +
nipkow@31719
   264
                   b*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
nipkow@31719
   265
    by (rule distrib)
nipkow@31719
   266
  also have "... = (SUM k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
nipkow@31719
   267
                  (SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))"
nipkow@31719
   268
    by (subst (1 2) power_plus_one, simp add: setsum_right_distrib mult_ac)
nipkow@31719
   269
  also have "... = (SUM k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) +
nipkow@31719
   270
                  (SUM k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))"
wenzelm@41541
   271
    by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le
wenzelm@41541
   272
      field_simps One_nat_def del:setsum_cl_ivl_Suc)
nipkow@31719
   273
  also have "... = a^(n+1) + b^(n+1) +
nipkow@31719
   274
                  (SUM k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) +
nipkow@31719
   275
                  (SUM k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))"
nipkow@31719
   276
    by (simp add: decomp2 decomp3)
nipkow@31719
   277
  also have
nipkow@31719
   278
      "... = a^(n+1) + b^(n+1) + 
nipkow@31719
   279
         (SUM k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))"
haftmann@36350
   280
    by (auto simp add: field_simps setsum_addf [symmetric]
nipkow@31952
   281
      choose_reduce_nat)
nipkow@31719
   282
  also have "... = (SUM k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))"
haftmann@36350
   283
    using decomp by (simp add: field_simps)
nipkow@31719
   284
  finally show "?P (n + 1)" by simp
nipkow@31719
   285
qed
nipkow@31719
   286
nipkow@41340
   287
lemma card_subsets_nat:
nipkow@31719
   288
  fixes S :: "'a set"
nipkow@41340
   289
  shows "finite S \<Longrightarrow> card {T. T \<le> S \<and> card T = k} = card S choose k"
nipkow@41340
   290
proof (induct arbitrary: k set: finite)
wenzelm@44872
   291
  case empty
wenzelm@44872
   292
  show ?case by (auto simp add: Collect_conv_if)
nipkow@41340
   293
next
nipkow@41340
   294
  case (insert x F)
nipkow@41340
   295
  note iassms = insert(1,2)
nipkow@41340
   296
  note ih = insert(3)
nipkow@41340
   297
  show ?case
nipkow@41340
   298
  proof (induct k rule: induct'_nat)
nipkow@41340
   299
    case zero
nipkow@41340
   300
    from iassms have "{T. T \<le> (insert x F) \<and> card T = 0} = {{}}"
nipkow@41340
   301
      by (auto simp: finite_subset)
wenzelm@44872
   302
    then show ?case by auto
nipkow@41340
   303
  next
nipkow@41340
   304
    case (plus1 k)
nipkow@41340
   305
    from iassms have fin: "finite (insert x F)" by auto
wenzelm@44872
   306
    then have "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
nipkow@41340
   307
      {T. T \<le> F & card T = k + 1} Un 
nipkow@41340
   308
      {T. T \<le> insert x F & x : T & card T = k + 1}"
wenzelm@41541
   309
      by auto
nipkow@41340
   310
    with iassms fin have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = 
nipkow@41340
   311
      card ({T. T \<subseteq> F \<and> card T = k + 1}) + 
nipkow@41340
   312
      card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1})"
nipkow@41340
   313
      apply (subst card_Un_disjoint [symmetric])
nipkow@41340
   314
      apply auto
nipkow@41340
   315
        (* note: nice! Didn't have to say anything here *)
nipkow@41340
   316
      done
nipkow@41340
   317
    also from ih have "card ({T. T \<subseteq> F \<and> card T = k + 1}) = 
nipkow@41340
   318
      card F choose (k+1)" by auto
nipkow@41340
   319
    also have "card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}) =
nipkow@41340
   320
      card ({T. T <= F & card T = k})"
nipkow@41340
   321
    proof -
nipkow@41340
   322
      let ?f = "%T. T Un {x}"
nipkow@41340
   323
      from iassms have "inj_on ?f {T. T <= F & card T = k}"
wenzelm@41541
   324
        unfolding inj_on_def by auto
wenzelm@44872
   325
      then have "card ({T. T <= F & card T = k}) = 
nipkow@41340
   326
        card(?f ` {T. T <= F & card T = k})"
nipkow@41340
   327
        by (rule card_image [symmetric])
nipkow@41340
   328
      also have "?f ` {T. T <= F & card T = k} = 
nipkow@41340
   329
        {T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}" (is "?L=?R")
nipkow@41340
   330
      proof-
nipkow@41340
   331
        { fix S assume "S \<subseteq> F"
wenzelm@44872
   332
          then have "card(insert x S) = card S +1"
nipkow@41340
   333
            using iassms by (auto simp: finite_subset) }
nipkow@41340
   334
        moreover
nipkow@41340
   335
        { fix T assume 1: "T \<subseteq> insert x F" "x : T" "card T = k+1"
nipkow@41340
   336
          let ?S = "T - {x}"
nipkow@41340
   337
          have "?S <= F & card ?S = k \<and> T = insert x ?S"
nipkow@41340
   338
            using 1 fin by (auto simp: finite_subset) }
nipkow@41340
   339
        ultimately show ?thesis by(auto simp: image_def)
nipkow@31719
   340
      qed
nipkow@41340
   341
      finally show ?thesis by (rule sym)
nipkow@31719
   342
    qed
nipkow@41340
   343
    also from ih have "card ({T. T <= F & card T = k}) = card F choose k"
nipkow@41340
   344
      by auto
nipkow@41340
   345
    finally have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = 
nipkow@41340
   346
      card F choose (k + 1) + (card F choose k)".
nipkow@41340
   347
    with iassms choose_plus_one_nat show ?case
nipkow@41340
   348
      by (auto simp del: card.insert)
nipkow@31719
   349
  qed
nipkow@31719
   350
qed
nipkow@31719
   351
nipkow@31719
   352
end