Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Pigeonhole.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Proofs/Extraction/Pigeonhole.thy
    Author:     Stefan Berghofer, TU Muenchen
*)

section \<open>The pigeonhole principle\<close>

theory Pigeonhole
imports Util "HOL-Library.Realizers" "HOL-Library.Code_Target_Numeral"
begin

text \<open>
  We formalize two proofs of the pigeonhole principle, which lead
  to extracted programs of quite different complexity. The original
  formalization of these proofs in {\sc Nuprl} is due to
  Aleksey Nogin @{cite "Nogin-ENTCS-2000"}.

  This proof yields a polynomial program.
\<close>

theorem pigeonhole:
  "\f. (\i. i \ Suc n \ f i \ n) \ \i j. i \ Suc n \ j < i \ f i = f j"
proof (induct n)
  case 0
  then have "Suc 0 \ Suc 0 \ 0 < Suc 0 \ f (Suc 0) = f 0" by simp
  then show ?case by iprover
next
  case (Suc n)
  have r:
    "k \ Suc (Suc n) \
    (\<And>i j. Suc k \<le> i \<Longrightarrow> i \<le> Suc (Suc n) \<Longrightarrow> j < i \<Longrightarrow> f i \<noteq> f j) \<Longrightarrow>
    (\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j)" for k
  proof (induct k)
    case 0
    let ?f = "\i. if f i = Suc n then f (Suc (Suc n)) else f i"
    have "\ (\i j. i \ Suc n \ j < i \ ?f i = ?f j)"
    proof
      assume "\i j. i \ Suc n \ j < i \ ?f i = ?f j"
      then obtain i j where i: "i \ Suc n" and j: "j < i" and f: "?f i = ?f j"
        by iprover
      from j have i_nz: "Suc 0 \ i" by simp
      from i have iSSn: "i \ Suc (Suc n)" by simp
      have S0SSn: "Suc 0 \ Suc (Suc n)" by simp
      show False
      proof cases
        assume fi: "f i = Suc n"
        show False
        proof cases
          assume fj: "f j = Suc n"
          from i_nz and iSSn and j have "f i \ f j" by (rule 0)
          moreover from fi have "f i = f j"
            by (simp add: fj [symmetric])
          ultimately show ?thesis ..
        next
          from i and j have "j < Suc (Suc n)" by simp
          with S0SSn and le_refl have "f (Suc (Suc n)) \ f j"
            by (rule 0)
          moreover assume "f j \ Suc n"
          with fi and f have "f (Suc (Suc n)) = f j" by simp
          ultimately show False ..
        qed
      next
        assume fi: "f i \ Suc n"
        show False
        proof cases
          from i have "i < Suc (Suc n)" by simp
          with S0SSn and le_refl have "f (Suc (Suc n)) \ f i"
            by (rule 0)
          moreover assume "f j = Suc n"
          with fi and f have "f (Suc (Suc n)) = f i" by simp
          ultimately show False ..
        next
          from i_nz and iSSn and j
          have "f i \ f j" by (rule 0)
          moreover assume "f j \ Suc n"
          with fi and f have "f i = f j" by simp
          ultimately show False ..
        qed
      qed
    qed
    moreover have "?f i \ n" if "i \ Suc n" for i
    proof -
      from that have i: "i < Suc (Suc n)" by simp
      have "f (Suc (Suc n)) \ f i"
        by (rule 0) (simp_all add: i)
      moreover have "f (Suc (Suc n)) \ Suc n"
        by (rule Suc) simp
      moreover from i have "i \ Suc (Suc n)" by simp
      then have "f i \ Suc n" by (rule Suc)
      ultimately show ?thesis
        by simp
    qed
    then have "\i j. i \ Suc n \ j < i \ ?f i = ?f j"
      by (rule Suc)
    ultimately show ?case ..
  next
    case (Suc k)
    from search [OF nat_eq_dec] show ?case
    proof
      assume "\j
      then show ?case by (iprover intro: le_refl)
    next
      assume nex: "\ (\j
      have "\i j. i \ k \ j < i \ f i = f j"
      proof (rule Suc)
        from Suc show "k \ Suc (Suc n)" by simp
        fix i j assume k: "Suc k \ i" and i: "i \ Suc (Suc n)"
          and j: "j < i"
        show "f i \ f j"
        proof cases
          assume eq: "i = Suc k"
          show ?thesis
          proof
            assume "f i = f j"
            then have "f (Suc k) = f j" by (simp add: eq)
            with nex and j and eq show False by iprover
          qed
        next
          assume "i \ Suc k"
          with k have "Suc (Suc k) \ i" by simp
          then show ?thesis using i and j by (rule Suc)
        qed
      qed
      then show ?thesis by (iprover intro: le_SucI)
    qed
  qed
  show ?case by (rule r) simp_all
qed

text \<open>
  The following proof, although quite elegant from a mathematical point of view,
  leads to an exponential program:
\<close>

theorem pigeonhole_slow:
  "\f. (\i. i \ Suc n \ f i \ n) \ \i j. i \ Suc n \ j < i \ f i = f j"
proof (induct n)
  case 0
  have "Suc 0 \ Suc 0" ..
  moreover have "0 < Suc 0" ..
  moreover from 0 have "f (Suc 0) = f 0" by simp
  ultimately show ?case by iprover
next
  case (Suc n)
  from search [OF nat_eq_dec] show ?case
  proof
    assume "\j < Suc (Suc n). f (Suc (Suc n)) = f j"
    then show ?case by (iprover intro: le_refl)
  next
    assume "\ (\j < Suc (Suc n). f (Suc (Suc n)) = f j)"
    then have nex: "\j < Suc (Suc n). f (Suc (Suc n)) \ f j" by iprover
    let ?f = "\i. if f i = Suc n then f (Suc (Suc n)) else f i"
    have "\i. i \ Suc n \ ?f i \ n"
    proof -
      fix i assume i: "i \ Suc n"
      show "?thesis i"
      proof (cases "f i = Suc n")
        case True
        from i and nex have "f (Suc (Suc n)) \ f i" by simp
        with True have "f (Suc (Suc n)) \ Suc n" by simp
        moreover from Suc have "f (Suc (Suc n)) \ Suc n" by simp
        ultimately have "f (Suc (Suc n)) \ n" by simp
        with True show ?thesis by simp
      next
        case False
        from Suc and i have "f i \ Suc n" by simp
        with False show ?thesis by simp
      qed
    qed
    then have "\i j. i \ Suc n \ j < i \ ?f i = ?f j" by (rule Suc)
    then obtain i j where i: "i \ Suc n" and ji: "j < i" and f: "?f i = ?f j"
      by iprover
    have "f i = f j"
    proof (cases "f i = Suc n")
      case True
      show ?thesis
      proof (cases "f j = Suc n")
        assume "f j = Suc n"
        with True show ?thesis by simp
      next
        assume "f j \ Suc n"
        moreover from i ji nex have "f (Suc (Suc n)) \ f j" by simp
        ultimately show ?thesis using True f by simp
      qed
    next
      case False
      show ?thesis
      proof (cases "f j = Suc n")
        assume "f j = Suc n"
        moreover from i nex have "f (Suc (Suc n)) \ f i" by simp
        ultimately show ?thesis using False f by simp
      next
        assume "f j \ Suc n"
        with False f show ?thesis by simp
      qed
    qed
    moreover from i have "i \ Suc (Suc n)" by simp
    ultimately show ?thesis using ji by iprover
  qed
qed

extract pigeonhole pigeonhole_slow

text \<open>
  The programs extracted from the above proofs look as follows:
  @{thm [display] pigeonhole_def}
  @{thm [display] pigeonhole_slow_def}
  The program for searching for an element in an array is
  @{thm [display,eta_contract=false] search_def}
  The correctness statement for \<^term>\<open>pigeonhole\<close> is
  @{thm [display] pigeonhole_correctness [no_vars]}

  In order to analyze the speed of the above programs,
  we generate ML code from them.
\<close>

instantiation nat :: default
begin

definition "default = (0::nat)"

instance ..

end

instantiation prod :: (default, default) default
begin

definition "default = (default, default)"

instance ..

end

definition "test n u = pigeonhole (nat_of_integer n) (\m. m - 1)"
definition "test' n u = pigeonhole_slow (nat_of_integer n) (\m. m - 1)"
definition "test'' u = pigeonhole 8 (List.nth [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"

ML_val "timeit (@{code test} 10)"
ML_val "timeit (@{code test'} 10)"
ML_val "timeit (@{code test} 20)"
ML_val "timeit (@{code test'} 20)"
ML_val "timeit (@{code test} 25)"
ML_val "timeit (@{code test'} 25)"
ML_val "timeit (@{code test} 500)"
ML_val "timeit @{code test''}"

end

¤ Dauer der Verarbeitung: 0.6 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.