products/sources/formale sprachen/Isabelle/HOL/Induct/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Ordinals.thy   Sprache: Isabelle

Original von: Isabelle©
(*  Title:      HOL/Induct/Ordinals.thy
    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
*)

section \<open>Ordinals\<close>

theory Ordinals
imports Main
begin

text \<open>
  Some basic definitions of ordinal numbers.  Draws an Agda
  development (in Martin-L\"of type theory) by Peter Hancock (see
  \<^url>\<open>http://www.dcs.ed.ac.uk/home/pgh/chat.html\<close>).
\<close>

datatype ordinal =
    Zero
  | Succ ordinal
  | Limit "nat \ ordinal"

primrec pred :: "ordinal \ nat \ ordinal option"
where
  "pred Zero n = None"
| "pred (Succ a) n = Some a"
| "pred (Limit f) n = Some (f n)"

abbreviation (input) iter :: "('a \ 'a) \ nat \ ('a \ 'a)"
  where "iter f n \ f ^^ n"

definition OpLim :: "(nat \ (ordinal \ ordinal)) \ (ordinal \ ordinal)"
  where "OpLim F a = Limit (\n. F n a)"

definition OpItw :: "(ordinal \ ordinal) \ (ordinal \ ordinal)" ("\")
  where "\f = OpLim (iter f)"

primrec cantor :: "ordinal \ ordinal \ ordinal"
where
  "cantor a Zero = Succ a"
| "cantor a (Succ b) = \(\x. cantor x b) a"
| "cantor a (Limit f) = Limit (\n. cantor a (f n))"

primrec Nabla :: "(ordinal \ ordinal) \ (ordinal \ ordinal)" ("\")
where
  "\f Zero = f Zero"
| "\f (Succ a) = f (Succ (\f a))"
| "\f (Limit h) = Limit (\n. \f (h n))"

definition deriv :: "(ordinal \ ordinal) \ (ordinal \ ordinal)"
  where "deriv f = \(\f)"

primrec veblen :: "ordinal \ ordinal \ ordinal"
where
  "veblen Zero = \(OpLim (iter (cantor Zero)))"
| "veblen (Succ a) = \(OpLim (iter (veblen a)))"
| "veblen (Limit f) = \(OpLim (\n. veblen (f n)))"

definition "veb a = veblen a Zero"
definition "\\<^sub>0 = veb Zero"
definition "\\<^sub>0 = Limit (\n. iter veb n Zero)"

end

¤ Dauer der Verarbeitung: 0.17 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff