Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Util.thy Sprache: Isabelle

Original von: Isabelle^©

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

section \<open>Auxiliary lemmas used in program extraction examples\<close>

theory Util
imports Main
begin

text \<open>Decidability of equality on natural numbers.\<close>

lemma nat_eq_dec: "\n::nat. m = n \ m \ n"
  apply (induct m)
  apply (case_tac n)
  apply (case_tac [3] n)
  apply (simp only: nat.simps, iprover?)+
  done

text \<open>
  Well-founded induction on natural numbers, derived using the standard
  structural induction rule.
\<close>

lemma nat_wf_ind:
  assumes R: "\x::nat. (\y. y < x \ P y) \ P x"
  shows "P z"
proof (rule R)
  show "\y. y < z \ P y"
  proof (induct z)
    case 0
    then show ?case by simp
  next
    case (Suc n y)
    from nat_eq_dec show ?case
    proof
      assume ny: "n = y"
      have "P n"
        by (rule R) (rule Suc)
      with ny show ?case by simp
    next
      assume "n \ y"
      with Suc have "y < n" by simp
      then show ?case by (rule Suc)
    qed
  qed
qed

text \<open>Bounded search for a natural number satisfying a decidable predicate.\<close>

lemma search:
  assumes dec: "\x::nat. P x \ \ P x"
  shows "(\x \ (\x
proof (induct y)
  case 0
  show ?case by simp
next
  case (Suc z)
  then show ?case
  proof
    assume "\x
    then obtain x where le: "x < z" and P: "P x" by iprover
    from le have "x < Suc z" by simp
    with P show ?case by iprover
  next
    assume nex: "\ (\x
    from dec show ?case
    proof
      assume P: "P z"
      have "z < Suc z" by simp
      with P show ?thesis by iprover
    next
      assume nP: "\ P z"
      have "\ (\x
      proof
        assume "\x
        then obtain x where le: "x < Suc z" and P: "P x" by iprover
        have "x < z"
        proof (cases "x = z")
          case True
          with nP and P show ?thesis by simp
        next
          case False
          with le show ?thesis by simp
        qed
        with P have "\x
        with nex show False ..
      qed
      then show ?case by iprover
    qed
  qed
qed

end

¤ Dauer der Verarbeitung: 0.0 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.