src/HOL/Proofs/Extraction/Pigeonhole.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 39157 b98909faaea8
child 43973 a907e541b127
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
wenzelm@39157
     1
(*  Title:      HOL/Proofs/Extraction/Pigeonhole.thy
berghofe@17024
     2
    Author:     Stefan Berghofer, TU Muenchen
berghofe@17024
     3
*)
berghofe@17024
     4
berghofe@17024
     5
header {* The pigeonhole principle *}
berghofe@17024
     6
haftmann@22737
     7
theory Pigeonhole
wenzelm@41413
     8
imports Util "~~/src/HOL/Library/Efficient_Nat"
haftmann@22737
     9
begin
berghofe@17024
    10
berghofe@17024
    11
text {*
berghofe@17024
    12
We formalize two proofs of the pigeonhole principle, which lead
berghofe@17024
    13
to extracted programs of quite different complexity. The original
berghofe@17024
    14
formalization of these proofs in {\sc Nuprl} is due to
berghofe@17024
    15
Aleksey Nogin \cite{Nogin-ENTCS-2000}.
berghofe@17024
    16
berghofe@17024
    17
This proof yields a polynomial program.
berghofe@17024
    18
*}
berghofe@17024
    19
berghofe@17024
    20
theorem pigeonhole:
berghofe@17024
    21
  "\<And>f. (\<And>i. i \<le> Suc n \<Longrightarrow> f i \<le> n) \<Longrightarrow> \<exists>i j. i \<le> Suc n \<and> j < i \<and> f i = f j"
berghofe@17024
    22
proof (induct n)
berghofe@17024
    23
  case 0
berghofe@17024
    24
  hence "Suc 0 \<le> Suc 0 \<and> 0 < Suc 0 \<and> f (Suc 0) = f 0" by simp
nipkow@17604
    25
  thus ?case by iprover
berghofe@17024
    26
next
berghofe@17024
    27
  case (Suc n)
berghofe@17024
    28
  {
berghofe@17024
    29
    fix k
berghofe@17024
    30
    have
berghofe@17024
    31
      "k \<le> Suc (Suc n) \<Longrightarrow>
berghofe@17024
    32
      (\<And>i j. Suc k \<le> i \<Longrightarrow> i \<le> Suc (Suc n) \<Longrightarrow> j < i \<Longrightarrow> f i \<noteq> f j) \<Longrightarrow>
berghofe@17024
    33
      (\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j)"
berghofe@17024
    34
    proof (induct k)
berghofe@17024
    35
      case 0
berghofe@17024
    36
      let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i"
berghofe@17024
    37
      have "\<not> (\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j)"
berghofe@17024
    38
      proof
wenzelm@32960
    39
        assume "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j"
wenzelm@32960
    40
        then obtain i j where i: "i \<le> Suc n" and j: "j < i"
wenzelm@32960
    41
          and f: "?f i = ?f j" by iprover
wenzelm@32960
    42
        from j have i_nz: "Suc 0 \<le> i" by simp
wenzelm@32960
    43
        from i have iSSn: "i \<le> Suc (Suc n)" by simp
wenzelm@32960
    44
        have S0SSn: "Suc 0 \<le> Suc (Suc n)" by simp
wenzelm@32960
    45
        show False
wenzelm@32960
    46
        proof cases
wenzelm@32960
    47
          assume fi: "f i = Suc n"
wenzelm@32960
    48
          show False
wenzelm@32960
    49
          proof cases
wenzelm@32960
    50
            assume fj: "f j = Suc n"
wenzelm@32960
    51
            from i_nz and iSSn and j have "f i \<noteq> f j" by (rule 0)
wenzelm@32960
    52
            moreover from fi have "f i = f j"
wenzelm@32960
    53
              by (simp add: fj [symmetric])
wenzelm@32960
    54
            ultimately show ?thesis ..
wenzelm@32960
    55
          next
wenzelm@32960
    56
            from i and j have "j < Suc (Suc n)" by simp
wenzelm@32960
    57
            with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f j"
wenzelm@32960
    58
              by (rule 0)
wenzelm@32960
    59
            moreover assume "f j \<noteq> Suc n"
wenzelm@32960
    60
            with fi and f have "f (Suc (Suc n)) = f j" by simp
wenzelm@32960
    61
            ultimately show False ..
wenzelm@32960
    62
          qed
wenzelm@32960
    63
        next
wenzelm@32960
    64
          assume fi: "f i \<noteq> Suc n"
wenzelm@32960
    65
          show False
wenzelm@32960
    66
          proof cases
wenzelm@32960
    67
            from i have "i < Suc (Suc n)" by simp
wenzelm@32960
    68
            with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f i"
wenzelm@32960
    69
              by (rule 0)
wenzelm@32960
    70
            moreover assume "f j = Suc n"
wenzelm@32960
    71
            with fi and f have "f (Suc (Suc n)) = f i" by simp
wenzelm@32960
    72
            ultimately show False ..
wenzelm@32960
    73
          next
wenzelm@32960
    74
            from i_nz and iSSn and j
wenzelm@32960
    75
            have "f i \<noteq> f j" by (rule 0)
wenzelm@32960
    76
            moreover assume "f j \<noteq> Suc n"
wenzelm@32960
    77
            with fi and f have "f i = f j" by simp
wenzelm@32960
    78
            ultimately show False ..
wenzelm@32960
    79
          qed
wenzelm@32960
    80
        qed
berghofe@17024
    81
      qed
berghofe@17024
    82
      moreover have "\<And>i. i \<le> Suc n \<Longrightarrow> ?f i \<le> n"
berghofe@17024
    83
      proof -
wenzelm@32960
    84
        fix i assume "i \<le> Suc n"
wenzelm@32960
    85
        hence i: "i < Suc (Suc n)" by simp
wenzelm@32960
    86
        have "f (Suc (Suc n)) \<noteq> f i"
wenzelm@32960
    87
          by (rule 0) (simp_all add: i)
wenzelm@32960
    88
        moreover have "f (Suc (Suc n)) \<le> Suc n"
wenzelm@32960
    89
          by (rule Suc) simp
wenzelm@32960
    90
        moreover from i have "i \<le> Suc (Suc n)" by simp
wenzelm@32960
    91
        hence "f i \<le> Suc n" by (rule Suc)
wenzelm@32960
    92
        ultimately show "?thesis i"
wenzelm@32960
    93
          by simp
berghofe@17024
    94
      qed
berghofe@17024
    95
      hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j"
wenzelm@32960
    96
        by (rule Suc)
berghofe@17024
    97
      ultimately show ?case ..
berghofe@17024
    98
    next
berghofe@17024
    99
      case (Suc k)
berghofe@25418
   100
      from search [OF nat_eq_dec] show ?case
berghofe@17024
   101
      proof
wenzelm@32960
   102
        assume "\<exists>j<Suc k. f (Suc k) = f j"
wenzelm@32960
   103
        thus ?case by (iprover intro: le_refl)
berghofe@17024
   104
      next
wenzelm@32960
   105
        assume nex: "\<not> (\<exists>j<Suc k. f (Suc k) = f j)"
wenzelm@32960
   106
        have "\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j"
wenzelm@32960
   107
        proof (rule Suc)
wenzelm@32960
   108
          from Suc show "k \<le> Suc (Suc n)" by simp
wenzelm@32960
   109
          fix i j assume k: "Suc k \<le> i" and i: "i \<le> Suc (Suc n)"
wenzelm@32960
   110
            and j: "j < i"
wenzelm@32960
   111
          show "f i \<noteq> f j"
wenzelm@32960
   112
          proof cases
wenzelm@32960
   113
            assume eq: "i = Suc k"
wenzelm@32960
   114
            show ?thesis
wenzelm@32960
   115
            proof
wenzelm@32960
   116
              assume "f i = f j"
wenzelm@32960
   117
              hence "f (Suc k) = f j" by (simp add: eq)
wenzelm@32960
   118
              with nex and j and eq show False by iprover
wenzelm@32960
   119
            qed
wenzelm@32960
   120
          next
wenzelm@32960
   121
            assume "i \<noteq> Suc k"
wenzelm@32960
   122
            with k have "Suc (Suc k) \<le> i" by simp
wenzelm@32960
   123
            thus ?thesis using i and j by (rule Suc)
wenzelm@32960
   124
          qed
wenzelm@32960
   125
        qed
wenzelm@32960
   126
        thus ?thesis by (iprover intro: le_SucI)
berghofe@17024
   127
      qed
berghofe@17024
   128
    qed
berghofe@17024
   129
  }
berghofe@17024
   130
  note r = this
berghofe@17024
   131
  show ?case by (rule r) simp_all
berghofe@17024
   132
qed
berghofe@17024
   133
berghofe@17024
   134
text {*
berghofe@17024
   135
The following proof, although quite elegant from a mathematical point of view,
berghofe@17024
   136
leads to an exponential program:
berghofe@17024
   137
*}
berghofe@17024
   138
berghofe@17024
   139
theorem pigeonhole_slow:
berghofe@17024
   140
  "\<And>f. (\<And>i. i \<le> Suc n \<Longrightarrow> f i \<le> n) \<Longrightarrow> \<exists>i j. i \<le> Suc n \<and> j < i \<and> f i = f j"
berghofe@17024
   141
proof (induct n)
berghofe@17024
   142
  case 0
berghofe@17024
   143
  have "Suc 0 \<le> Suc 0" ..
berghofe@17024
   144
  moreover have "0 < Suc 0" ..
berghofe@17024
   145
  moreover from 0 have "f (Suc 0) = f 0" by simp
nipkow@17604
   146
  ultimately show ?case by iprover
berghofe@17024
   147
next
berghofe@17024
   148
  case (Suc n)
berghofe@25418
   149
  from search [OF nat_eq_dec] show ?case
berghofe@17024
   150
  proof
berghofe@17024
   151
    assume "\<exists>j < Suc (Suc n). f (Suc (Suc n)) = f j"
nipkow@17604
   152
    thus ?case by (iprover intro: le_refl)
berghofe@17024
   153
  next
berghofe@17024
   154
    assume "\<not> (\<exists>j < Suc (Suc n). f (Suc (Suc n)) = f j)"
nipkow@17604
   155
    hence nex: "\<forall>j < Suc (Suc n). f (Suc (Suc n)) \<noteq> f j" by iprover
berghofe@17024
   156
    let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i"
berghofe@17024
   157
    have "\<And>i. i \<le> Suc n \<Longrightarrow> ?f i \<le> n"
berghofe@17024
   158
    proof -
berghofe@17024
   159
      fix i assume i: "i \<le> Suc n"
berghofe@17024
   160
      show "?thesis i"
berghofe@17024
   161
      proof (cases "f i = Suc n")
wenzelm@32960
   162
        case True
wenzelm@32960
   163
        from i and nex have "f (Suc (Suc n)) \<noteq> f i" by simp
wenzelm@32960
   164
        with True have "f (Suc (Suc n)) \<noteq> Suc n" by simp
wenzelm@32960
   165
        moreover from Suc have "f (Suc (Suc n)) \<le> Suc n" by simp
wenzelm@32960
   166
        ultimately have "f (Suc (Suc n)) \<le> n" by simp
wenzelm@32960
   167
        with True show ?thesis by simp
berghofe@17024
   168
      next
wenzelm@32960
   169
        case False
wenzelm@32960
   170
        from Suc and i have "f i \<le> Suc n" by simp
wenzelm@32960
   171
        with False show ?thesis by simp
berghofe@17024
   172
      qed
berghofe@17024
   173
    qed
berghofe@17024
   174
    hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j" by (rule Suc)
berghofe@17024
   175
    then obtain i j where i: "i \<le> Suc n" and ji: "j < i" and f: "?f i = ?f j"
nipkow@17604
   176
      by iprover
berghofe@17024
   177
    have "f i = f j"
berghofe@17024
   178
    proof (cases "f i = Suc n")
berghofe@17024
   179
      case True
berghofe@17024
   180
      show ?thesis
berghofe@17024
   181
      proof (cases "f j = Suc n")
wenzelm@32960
   182
        assume "f j = Suc n"
wenzelm@32960
   183
        with True show ?thesis by simp
berghofe@17024
   184
      next
wenzelm@32960
   185
        assume "f j \<noteq> Suc n"
wenzelm@32960
   186
        moreover from i ji nex have "f (Suc (Suc n)) \<noteq> f j" by simp
wenzelm@32960
   187
        ultimately show ?thesis using True f by simp
berghofe@17024
   188
      qed
berghofe@17024
   189
    next
berghofe@17024
   190
      case False
berghofe@17024
   191
      show ?thesis
berghofe@17024
   192
      proof (cases "f j = Suc n")
wenzelm@32960
   193
        assume "f j = Suc n"
wenzelm@32960
   194
        moreover from i nex have "f (Suc (Suc n)) \<noteq> f i" by simp
wenzelm@32960
   195
        ultimately show ?thesis using False f by simp
berghofe@17024
   196
      next
wenzelm@32960
   197
        assume "f j \<noteq> Suc n"
wenzelm@32960
   198
        with False f show ?thesis by simp
berghofe@17024
   199
      qed
berghofe@17024
   200
    qed
berghofe@17024
   201
    moreover from i have "i \<le> Suc (Suc n)" by simp
nipkow@17604
   202
    ultimately show ?thesis using ji by iprover
berghofe@17024
   203
  qed
berghofe@17024
   204
qed
berghofe@17024
   205
berghofe@17024
   206
extract pigeonhole pigeonhole_slow
berghofe@17024
   207
berghofe@17024
   208
text {*
berghofe@17024
   209
The programs extracted from the above proofs look as follows:
berghofe@17024
   210
@{thm [display] pigeonhole_def}
berghofe@17024
   211
@{thm [display] pigeonhole_slow_def}
berghofe@17024
   212
The program for searching for an element in an array is
berghofe@17024
   213
@{thm [display,eta_contract=false] search_def}
berghofe@17024
   214
The correctness statement for @{term "pigeonhole"} is
berghofe@17024
   215
@{thm [display] pigeonhole_correctness [no_vars]}
berghofe@17024
   216
berghofe@17024
   217
In order to analyze the speed of the above programs,
berghofe@17024
   218
we generate ML code from them.
berghofe@17024
   219
*}
berghofe@17024
   220
haftmann@27982
   221
instantiation nat :: default
haftmann@27982
   222
begin
haftmann@27982
   223
haftmann@27982
   224
definition "default = (0::nat)"
haftmann@27982
   225
haftmann@27982
   226
instance ..
haftmann@27982
   227
haftmann@27982
   228
end
haftmann@27982
   229
haftmann@37678
   230
instantiation prod :: (default, default) default
haftmann@27982
   231
begin
haftmann@27982
   232
haftmann@27982
   233
definition "default = (default, default)"
haftmann@27982
   234
haftmann@27982
   235
instance ..
haftmann@27982
   236
haftmann@27982
   237
end
haftmann@27982
   238
haftmann@20837
   239
definition
haftmann@23810
   240
  "test n u = pigeonhole n (\<lambda>m. m - 1)"
wenzelm@21404
   241
definition
haftmann@23810
   242
  "test' n u = pigeonhole_slow n (\<lambda>m. m - 1)"
haftmann@22507
   243
definition
haftmann@22507
   244
  "test'' u = pigeonhole 8 (op ! [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"
haftmann@20837
   245
haftmann@37287
   246
ML "timeit (@{code test} 10)" 
haftmann@37287
   247
ML "timeit (@{code test'} 10)"
haftmann@37287
   248
ML "timeit (@{code test} 20)"
haftmann@37287
   249
ML "timeit (@{code test'} 20)"
haftmann@37287
   250
ML "timeit (@{code test} 25)"
haftmann@37287
   251
ML "timeit (@{code test'} 25)"
haftmann@37287
   252
ML "timeit (@{code test} 500)"
haftmann@37287
   253
ML "timeit @{code test''}"
haftmann@37287
   254
haftmann@37287
   255
consts_code
haftmann@37287
   256
  "default :: nat" ("{* 0::nat *}")
haftmann@37287
   257
  "default :: nat \<times> nat" ("{* (0::nat, 0::nat) *}")
haftmann@37287
   258
haftmann@27436
   259
code_module PH
haftmann@22507
   260
contains
haftmann@22507
   261
  test = test
haftmann@22507
   262
  test' = test'
haftmann@22507
   263
  test'' = test''
haftmann@22507
   264
haftmann@27436
   265
ML "timeit (PH.test 10)"
haftmann@27436
   266
ML "timeit (PH.test' 10)"
haftmann@27436
   267
ML "timeit (PH.test 20)"
haftmann@27436
   268
ML "timeit (PH.test' 20)"
haftmann@27436
   269
ML "timeit (PH.test 25)"
haftmann@27436
   270
ML "timeit (PH.test' 25)"
haftmann@27436
   271
ML "timeit (PH.test 500)"
haftmann@27436
   272
ML "timeit PH.test''"
haftmann@20837
   273
berghofe@17024
   274
end
haftmann@37287
   275