Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Proofs/Extraction/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 16.11.2025 mit Größe 8 kB

Quellcode-Bibliothek Pigeonhole.thy Sprache: 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>\<open>"Nogin-ENTCS-2000"\<close>.

  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

quality100%

¤ 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.0.16Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.