# HG changeset patch
# User wenzelm
# Date 1001930200 -7200
# Node ID 0c248bed5225d48fdeee0c3b3acf424c6efe8716
# Parent  be1bc3b88480581cf449d88277080b2857ffd7e8
added Ordinals example;

diff -r be1bc3b88480 -r 0c248bed5225 src/HOL/Induct/Ordinals.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Ordinals.thy	Mon Oct 01 11:56:40 2001 +0200
@@ -0,0 +1,76 @@
+(*  Title:      HOL/Induct/Tree.thy
+    ID:         $Id$
+    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+header {* Ordinals *}
+
+theory Ordinals = Main:
+
+text {*
+  Some basic definitions of ordinal numbers.  Draws an Agda
+  development (in Martin-L{\"}of type theory) by Peter Hancock (see
+  \url{http://www.dcs.ed.ac.uk/home/pgh/chat.html}).
+*}
+
+datatype ordinal =
+    Zero
+  | Succ ordinal
+  | Limit "nat => ordinal"
+
+consts
+  pred :: "ordinal => nat => ordinal option"
+primrec
+  "pred Zero n = None"
+  "pred (Succ a) n = Some a"
+  "pred (Limit f) n = Some (f n)"
+
+consts
+  iter :: "('a => 'a) => nat => ('a => 'a)"
+primrec
+  "iter f 0 = id"
+  "iter f (Suc n) = f \<circ> (iter f n)"
+
+constdefs
+  OpLim :: "(nat => (ordinal => ordinal)) => (ordinal => ordinal)"
+  "OpLim F a == Limit (\<lambda>n. F n a)"
+  OpItw :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<Squnion>")
+  "\<Squnion>f == OpLim (iter f)"
+
+consts
+  cantor :: "ordinal => ordinal => ordinal"
+primrec
+  "cantor a Zero = Succ a"
+  "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
+  "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
+
+consts
+  Nabla :: "(ordinal => ordinal) => (ordinal => ordinal)"    ("\<nabla>")
+primrec
+  "\<nabla>f Zero = f Zero"
+  "\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
+  "\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
+
+constdefs
+  deriv :: "(ordinal => ordinal) => (ordinal => ordinal)"
+  "deriv f == \<nabla>(\<Squnion>f)"
+
+consts
+  veblen :: "ordinal => ordinal => ordinal"
+primrec
+  "veblen Zero = \<nabla>(OpLim (iter (cantor Zero)))"
+  "veblen (Succ a) = \<nabla>(OpLim (iter (veblen a)))"
+  "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
+
+constdefs
+  veb :: "ordinal => ordinal"
+  "veb a == veblen a Zero"
+
+constdefs
+  epsilon0 :: ordinal    ("SOME \<^sub>0")
+  "SOME \<^sub>0 == veb Zero"
+  Gamma0 :: ordinal    ("\<Gamma>\<^sub>0")
+  "\<Gamma>\<^sub>0 == Limit (\<lambda>n. iter veb n Zero)"
+
+end
diff -r be1bc3b88480 -r 0c248bed5225 src/HOL/Induct/ROOT.ML
--- a/src/HOL/Induct/ROOT.ML	Sun Sep 30 13:42:00 2001 +0200
+++ b/src/HOL/Induct/ROOT.ML	Mon Oct 01 11:56:40 2001 +0200
@@ -3,6 +3,7 @@
 time_use_thy "Term";
 time_use_thy "ABexp";
 time_use_thy "Tree";
+time_use_thy "Ordinals";
 time_use_thy "Sigma_Algebra";
 time_use_thy "Comb";
 time_use_thy "PropLog";
diff -r be1bc3b88480 -r 0c248bed5225 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Sep 30 13:42:00 2001 +0200
+++ b/src/HOL/IsaMakefile	Mon Oct 01 11:56:40 2001 +0200
@@ -209,7 +209,7 @@
 $(LOG)/HOL-Induct.gz: $(OUT)/HOL \
   Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
   Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
-  Induct/LList.ML Induct/LList.thy Induct/Mutil.thy \
+  Induct/LList.ML Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
   Induct/PropLog.ML Induct/PropLog.thy Induct/ROOT.ML \
   Induct/Sexp.ML Induct/Sexp.thy Induct/Sigma_Algebra.thy \
   Induct/SList.ML Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \