Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Peano_Axioms.thy   Sprache: Isabelle

Original von: Isabelle©

section \<open>Peano's axioms for Natural Numbers\<close>

theory Peano_Axioms
  imports Main
begin

locale peano =  \<comment> \<open>or: \<^theory_text>\<open>class\<close>\<close>
  fixes zero :: 'a
  fixes succ :: "'a \ 'a"
  assumes succ_neq_zero [simp]: "succ m \ zero"
  assumes succ_inject [simp]: "succ m = succ n \ m = n"
  assumes induct [case_names zero succ, induct type: 'a]:
    "P zero \ (\n. P n \ P (succ n)) \ P n"
begin

lemma zero_neq_succ [simp]: "zero \ succ m"
  by (rule succ_neq_zero [symmetric])


text \<open>\<^medskip> Primitive recursion as a (functional) relation -- polymorphic!\<close>

inductive Rec :: "'b \ ('a \ 'b \ 'b) \ 'a \ 'b \ bool"
  for e :: 'b and r :: "'\<Rightarrow> 'b \<Rightarrow> 'b"
where
  Rec_zero: "Rec e r zero e"
| Rec_succ: "Rec e r m n \ Rec e r (succ m) (r m n)"

lemma Rec_functional: "\!y::'b. Rec e r x y" for x :: 'a
proof -
  let ?R = "Rec e r"
  show ?thesis
  proof (induct x)
    case zero
    show "\!y. ?R zero y"
    proof
      show "?R zero e" ..
      show "y = e" if "?R zero y" for y
        using that by cases simp_all
    qed
  next
    case (succ m)
    from \<open>\<exists>!y. ?R m y\<close>
    obtain y where y: "?R m y" and yy': "\y'. ?R m y' \ y = y'"
      by blast
    show "\!z. ?R (succ m) z"
    proof
      from y show "?R (succ m) (r m y)" ..
    next
      fix z
      assume "?R (succ m) z"
      then obtain u where "z = r m u" and "?R m u"
        by cases simp_all
      with yy' show "z = r m y"
        by (simp only:)
    qed
  qed
qed


text \<open>\<^medskip> The recursion operator -- polymorphic!\<close>

definition rec :: "'b \ ('a \ 'b \ 'b) \ 'a \ 'b"
  where "rec e r x = (THE y. Rec e r x y)"

lemma rec_eval:
  assumes Rec: "Rec e r x y"
  shows "rec e r x = y"
  unfolding rec_def
  using Rec_functional and Rec by (rule the1_equality)

lemma rec_zero [simp]: "rec e r zero = e"
proof (rule rec_eval)
  show "Rec e r zero e" ..
qed

lemma rec_succ [simp]: "rec e r (succ m) = r m (rec e r m)"
proof (rule rec_eval)
  let ?R = "Rec e r"
  have "?R m (rec e r m)"
    unfolding rec_def using Rec_functional by (rule theI')
  then show "?R (succ m) (r m (rec e r m))" ..
qed


text \<open>\<^medskip> Example: addition (monomorphic)\<close>

definition add :: "'a \ 'a \ 'a"
  where "add m n = rec n (\_ k. succ k) m"

lemma add_zero [simp]: "add zero n = n"
  and add_succ [simp]: "add (succ m) n = succ (add m n)"
  unfolding add_def by simp_all

lemma add_assoc: "add (add k m) n = add k (add m n)"
  by (induct k) simp_all

lemma add_zero_right: "add m zero = m"
  by (induct m) simp_all

lemma add_succ_right: "add m (succ n) = succ (add m n)"
  by (induct m) simp_all

lemma "add (succ (succ (succ zero))) (succ (succ zero)) =
    succ (succ (succ (succ (succ zero))))"
  by simp


text \<open>\<^medskip> Example: replication (polymorphic)\<close>

definition repl :: "'a \ 'b \ 'b list"
  where "repl n x = rec [] (\_ xs. x # xs) n"

lemma repl_zero [simp]: "repl zero x = []"
  and repl_succ [simp]: "repl (succ n) x = x # repl n x"
  unfolding repl_def by simp_all

lemma "repl (succ (succ (succ zero))) True = [True, True, True]"
  by simp

end


text \<open>\<^medskip> Just see that our abstract specification makes sense \dots\<close>

interpretation peano 0 Suc
proof
  fix m n
  show "Suc m \ 0" by simp
  show "Suc m = Suc n \ m = n" by simp
  show "P n"
    if zero: "P 0"
    and succ: "\n. P n \ P (Suc n)"
    for P
  proof (induct n)
    case 0
    show ?case by (rule zero)
  next
    case Suc
    then show ?case by (rule succ)
  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.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik