src/HOL/Extraction/Pigeonhole.thy
author haftmann
Fri, 20 Oct 2006 10:44:39 +0200
changeset 21062 876dd2695423
parent 20933 3f999b73f6d5
child 21127 c8e862897d13
permissions -rw-r--r--
slight adaption
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Extraction/Pigeonhole.thy
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
     2
    ID:         $Id$
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
     3
    Author:     Stefan Berghofer, TU Muenchen
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
     4
*)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
     5
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
     6
header {* The pigeonhole principle *}
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
     7
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
     8
theory Pigeonhole imports EfficientNat begin
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
     9
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    10
text {*
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    11
We formalize two proofs of the pigeonhole principle, which lead
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    12
to extracted programs of quite different complexity. The original
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    13
formalization of these proofs in {\sc Nuprl} is due to
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    14
Aleksey Nogin \cite{Nogin-ENTCS-2000}.
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    15
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    16
We need decidability of equality on natural numbers:
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    17
*}
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    18
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    19
lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    20
  apply (induct m)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    21
  apply (case_tac n)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    22
  apply (case_tac [3] n)
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
    23
  apply (simp only: nat.simps, iprover?)+
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    24
  done
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    25
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    26
text {*
17027
8bbe57116d13 Tuned comment.
berghofe
parents: 17024
diff changeset
    27
We can decide whether an array @{term "f"} of length @{term "l"}
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    28
contains an element @{term "x"}.
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    29
*}
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    30
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    31
lemma search: "(\<exists>j<(l::nat). (x::nat) = f j) \<or> \<not> (\<exists>j<l. x = f j)"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    32
proof (induct l)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    33
  case 0
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    34
  have "\<not> (\<exists>j<0. x = f j)"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    35
  proof
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    36
    assume "\<exists>j<0. x = f j"
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
    37
    then obtain j where j: "j < (0::nat)" by iprover
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    38
    thus "False" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    39
  qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    40
  thus ?case ..
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    41
next
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    42
  case (Suc l)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    43
  thus ?case
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    44
  proof
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    45
    assume "\<exists>j<l. x = f j"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    46
    then obtain j where j: "j < l"
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
    47
      and eq: "x = f j" by iprover
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    48
    from j have "j < Suc l" by simp
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
    49
    with eq show ?case by iprover
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    50
  next
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    51
    assume nex: "\<not> (\<exists>j<l. x = f j)"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    52
    from nat_eq_dec show ?case
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    53
    proof
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    54
      assume eq: "x = f l"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    55
      have "l < Suc l" by simp
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
    56
      with eq show ?case by iprover
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    57
    next
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    58
      assume neq: "x \<noteq> f l"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    59
      have "\<not> (\<exists>j<Suc l. x = f j)"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    60
      proof
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    61
	assume "\<exists>j<Suc l. x = f j"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    62
	then obtain j where j: "j < Suc l"
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
    63
	  and eq: "x = f j" by iprover
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    64
	show False
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    65
	proof cases
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    66
	  assume "j = l"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    67
	  with eq have "x = f l" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    68
	  with neq show False ..
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    69
	next
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    70
	  assume "j \<noteq> l"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    71
	  with j have "j < l" by simp
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
    72
	  with nex and eq show False by iprover
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    73
	qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    74
      qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    75
      thus ?case ..
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    76
    qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    77
  qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    78
qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    79
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    80
text {*
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    81
This proof yields a polynomial program.
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    82
*}
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    83
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    84
theorem pigeonhole:
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    85
  "\<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"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    86
proof (induct n)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    87
  case 0
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    88
  hence "Suc 0 \<le> Suc 0 \<and> 0 < Suc 0 \<and> f (Suc 0) = f 0" by simp
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
    89
  thus ?case by iprover
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    90
next
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    91
  case (Suc n)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    92
  {
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    93
    fix k
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    94
    have
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    95
      "k \<le> Suc (Suc n) \<Longrightarrow>
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    96
      (\<And>i j. Suc k \<le> i \<Longrightarrow> i \<le> Suc (Suc n) \<Longrightarrow> j < i \<Longrightarrow> f i \<noteq> f j) \<Longrightarrow>
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    97
      (\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j)"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    98
    proof (induct k)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
    99
      case 0
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   100
      let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   101
      have "\<not> (\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j)"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   102
      proof
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   103
	assume "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   104
      	then obtain i j where i: "i \<le> Suc n" and j: "j < i"
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
   105
	  and f: "?f i = ?f j" by iprover
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   106
      	from j have i_nz: "Suc 0 \<le> i" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   107
      	from i have iSSn: "i \<le> Suc (Suc n)" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   108
      	have S0SSn: "Suc 0 \<le> Suc (Suc n)" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   109
      	show False
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   110
      	proof cases
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   111
	  assume fi: "f i = Suc n"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   112
	  show False
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   113
	  proof cases
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   114
	    assume fj: "f j = Suc n"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   115
	    from i_nz and iSSn and j have "f i \<noteq> f j" by (rule 0)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   116
	    moreover from fi have "f i = f j"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   117
	      by (simp add: fj [symmetric])
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   118
	    ultimately show ?thesis ..
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   119
	  next
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   120
	    from i and j have "j < Suc (Suc n)" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   121
	    with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f j"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   122
	      by (rule 0)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   123
	    moreover assume "f j \<noteq> Suc n"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   124
	    with fi and f have "f (Suc (Suc n)) = f j" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   125
	    ultimately show False ..
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   126
	  qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   127
      	next
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   128
	  assume fi: "f i \<noteq> Suc n"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   129
	  show False
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   130
	  proof cases
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   131
	    from i have "i < Suc (Suc n)" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   132
	    with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f i"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   133
	      by (rule 0)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   134
	    moreover assume "f j = Suc n"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   135
	    with fi and f have "f (Suc (Suc n)) = f i" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   136
	    ultimately show False ..
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   137
	  next
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   138
	    from i_nz and iSSn and j
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   139
	    have "f i \<noteq> f j" by (rule 0)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   140
	    moreover assume "f j \<noteq> Suc n"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   141
	    with fi and f have "f i = f j" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   142
	    ultimately show False ..
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   143
	  qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   144
      	qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   145
      qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   146
      moreover have "\<And>i. i \<le> Suc n \<Longrightarrow> ?f i \<le> n"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   147
      proof -
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   148
	fix i assume "i \<le> Suc n"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   149
	hence i: "i < Suc (Suc n)" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   150
	have "f (Suc (Suc n)) \<noteq> f i"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   151
	  by (rule 0) (simp_all add: i)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   152
	moreover have "f (Suc (Suc n)) \<le> Suc n"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   153
	  by (rule Suc) simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   154
	moreover from i have "i \<le> Suc (Suc n)" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   155
	hence "f i \<le> Suc n" by (rule Suc)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   156
	ultimately show "?thesis i"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   157
	  by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   158
      qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   159
      hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   160
      	by (rule Suc)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   161
      ultimately show ?case ..
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   162
    next
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   163
      case (Suc k)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   164
      from search show ?case
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   165
      proof
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   166
	assume "\<exists>j<Suc k. f (Suc k) = f j"
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
   167
	thus ?case by (iprover intro: le_refl)
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   168
      next
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   169
	assume nex: "\<not> (\<exists>j<Suc k. f (Suc k) = f j)"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   170
	have "\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   171
	proof (rule Suc)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   172
	  from Suc show "k \<le> Suc (Suc n)" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   173
	  fix i j assume k: "Suc k \<le> i" and i: "i \<le> Suc (Suc n)"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   174
	    and j: "j < i"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   175
	  show "f i \<noteq> f j"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   176
	  proof cases
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   177
	    assume eq: "i = Suc k"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   178
	    show ?thesis
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   179
	    proof
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   180
	      assume "f i = f j"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   181
	      hence "f (Suc k) = f j" by (simp add: eq)
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
   182
	      with nex and j and eq show False by iprover
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   183
	    qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   184
	  next
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   185
	    assume "i \<noteq> Suc k"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   186
	    with k have "Suc (Suc k) \<le> i" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   187
	    thus ?thesis using i and j by (rule Suc)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   188
	  qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   189
	qed
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
   190
	thus ?thesis by (iprover intro: le_SucI)
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   191
      qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   192
    qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   193
  }
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   194
  note r = this
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   195
  show ?case by (rule r) simp_all
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   196
qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   197
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   198
text {*
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   199
The following proof, although quite elegant from a mathematical point of view,
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   200
leads to an exponential program:
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   201
*}
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   202
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   203
theorem pigeonhole_slow:
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   204
  "\<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"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   205
proof (induct n)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   206
  case 0
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   207
  have "Suc 0 \<le> Suc 0" ..
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   208
  moreover have "0 < Suc 0" ..
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   209
  moreover from 0 have "f (Suc 0) = f 0" by simp
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
   210
  ultimately show ?case by iprover
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   211
next
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   212
  case (Suc n)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   213
  from search show ?case
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   214
  proof
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   215
    assume "\<exists>j < Suc (Suc n). f (Suc (Suc n)) = f j"
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
   216
    thus ?case by (iprover intro: le_refl)
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   217
  next
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   218
    assume "\<not> (\<exists>j < Suc (Suc n). f (Suc (Suc n)) = f j)"
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
   219
    hence nex: "\<forall>j < Suc (Suc n). f (Suc (Suc n)) \<noteq> f j" by iprover
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   220
    let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   221
    have "\<And>i. i \<le> Suc n \<Longrightarrow> ?f i \<le> n"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   222
    proof -
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   223
      fix i assume i: "i \<le> Suc n"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   224
      show "?thesis i"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   225
      proof (cases "f i = Suc n")
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   226
	case True
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   227
	from i and nex have "f (Suc (Suc n)) \<noteq> f i" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   228
	with True have "f (Suc (Suc n)) \<noteq> Suc n" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   229
	moreover from Suc have "f (Suc (Suc n)) \<le> Suc n" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   230
	ultimately have "f (Suc (Suc n)) \<le> n" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   231
	with True show ?thesis by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   232
      next
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   233
	case False
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   234
	from Suc and i have "f i \<le> Suc n" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   235
	with False show ?thesis by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   236
      qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   237
    qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   238
    hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j" by (rule Suc)
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   239
    then obtain i j where i: "i \<le> Suc n" and ji: "j < i" and f: "?f i = ?f j"
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
   240
      by iprover
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   241
    have "f i = f j"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   242
    proof (cases "f i = Suc n")
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   243
      case True
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   244
      show ?thesis
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   245
      proof (cases "f j = Suc n")
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   246
	assume "f j = Suc n"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   247
	with True show ?thesis by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   248
      next
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   249
	assume "f j \<noteq> Suc n"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   250
	moreover from i ji nex have "f (Suc (Suc n)) \<noteq> f j" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   251
	ultimately show ?thesis using True f by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   252
      qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   253
    next
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   254
      case False
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   255
      show ?thesis
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   256
      proof (cases "f j = Suc n")
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   257
	assume "f j = Suc n"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   258
	moreover from i nex have "f (Suc (Suc n)) \<noteq> f i" by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   259
	ultimately show ?thesis using False f by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   260
      next
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   261
	assume "f j \<noteq> Suc n"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   262
	with False f show ?thesis by simp
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   263
      qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   264
    qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   265
    moreover from i have "i \<le> Suc (Suc n)" by simp
17604
5f30179fbf44 rules -> iprover
nipkow
parents: 17145
diff changeset
   266
    ultimately show ?thesis using ji by iprover
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   267
  qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   268
qed
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   269
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   270
extract pigeonhole pigeonhole_slow
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   271
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   272
text {*
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   273
The programs extracted from the above proofs look as follows:
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   274
@{thm [display] pigeonhole_def}
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   275
@{thm [display] pigeonhole_slow_def}
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   276
The program for searching for an element in an array is
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   277
@{thm [display,eta_contract=false] search_def}
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   278
The correctness statement for @{term "pigeonhole"} is
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   279
@{thm [display] pigeonhole_correctness [no_vars]}
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   280
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   281
In order to analyze the speed of the above programs,
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   282
we generate ML code from them.
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   283
*}
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   284
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   285
consts_code
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   286
  arbitrary :: "nat \<times> nat" ("{* (0::nat, 0::nat) *}")
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   287
17145
e623e57b0f44 Adapted to new code generator syntax.
berghofe
parents: 17027
diff changeset
   288
code_module PH
e623e57b0f44 Adapted to new code generator syntax.
berghofe
parents: 17027
diff changeset
   289
contains
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   290
  test = "\<lambda>n. pigeonhole n (\<lambda>m. m - 1)"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   291
  test' = "\<lambda>n. pigeonhole_slow n (\<lambda>m. m - 1)"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   292
  sel = "op !"
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   293
17145
e623e57b0f44 Adapted to new code generator syntax.
berghofe
parents: 17027
diff changeset
   294
ML "timeit (fn () => PH.test 10)"
e623e57b0f44 Adapted to new code generator syntax.
berghofe
parents: 17027
diff changeset
   295
ML "timeit (fn () => PH.test' 10)"
e623e57b0f44 Adapted to new code generator syntax.
berghofe
parents: 17027
diff changeset
   296
ML "timeit (fn () => PH.test 20)"
e623e57b0f44 Adapted to new code generator syntax.
berghofe
parents: 17027
diff changeset
   297
ML "timeit (fn () => PH.test' 20)"
e623e57b0f44 Adapted to new code generator syntax.
berghofe
parents: 17027
diff changeset
   298
ML "timeit (fn () => PH.test 25)"
e623e57b0f44 Adapted to new code generator syntax.
berghofe
parents: 17027
diff changeset
   299
ML "timeit (fn () => PH.test' 25)"
e623e57b0f44 Adapted to new code generator syntax.
berghofe
parents: 17027
diff changeset
   300
ML "timeit (fn () => PH.test 500)"
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   301
17145
e623e57b0f44 Adapted to new code generator syntax.
berghofe
parents: 17027
diff changeset
   302
ML "PH.pigeonhole 8 (PH.sel [0,1,2,3,4,5,6,3,7,8])"
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   303
20837
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   304
definition
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   305
  arbitrary_nat :: "nat \<times> nat"
21062
876dd2695423 slight adaption
haftmann
parents: 20933
diff changeset
   306
  [symmetric, code inline]: "arbitrary_nat = arbitrary"
20933
3f999b73f6d5 added code_constsubst
haftmann
parents: 20837
diff changeset
   307
  arbitrary_nat_subst :: "nat \<times> nat"
3f999b73f6d5 added code_constsubst
haftmann
parents: 20837
diff changeset
   308
  "arbitrary_nat_subst = (0, 0)"
20837
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   309
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   310
lemma [code func]:
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   311
  "arbitrary_nat = arbitrary_nat" ..
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   312
21062
876dd2695423 slight adaption
haftmann
parents: 20933
diff changeset
   313
code_axioms
20933
3f999b73f6d5 added code_constsubst
haftmann
parents: 20837
diff changeset
   314
  arbitrary_nat \<equiv> arbitrary_nat_subst
20837
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   315
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   316
definition
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   317
  "test n = pigeonhole n (\<lambda>m. m - 1)"
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   318
  "test' n = pigeonhole_slow n (\<lambda>m. m - 1)"
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   319
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   320
code_gen test test' "op !" (SML -)
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   321
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   322
ML "timeit (fn () => ROOT.Pigeonhole.test 10)"
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   323
ML "timeit (fn () => ROOT.Pigeonhole.test' 10)"
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   324
ML "timeit (fn () => ROOT.Pigeonhole.test 20)"
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   325
ML "timeit (fn () => ROOT.Pigeonhole.test' 20)"
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   326
ML "timeit (fn () => ROOT.Pigeonhole.test 25)"
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   327
ML "timeit (fn () => ROOT.Pigeonhole.test' 25)"
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   328
ML "timeit (fn () => ROOT.Pigeonhole.test 500)"
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   329
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   330
ML "ROOT.Pigeonhole.pigeonhole 8 (ROOT.List.nth [0,1,2,3,4,5,6,3,7,8])"
099877d83d2b added example for code_gen
haftmann
parents: 20593
diff changeset
   331
17024
ae4a8446df16 New case study: pigeonhole principle.
berghofe
parents:
diff changeset
   332
end