--- a/doc-src/TutorialI/Overview/LNCS/Ordinal.thy Mon Jul 30 16:40:21 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-theory Ordinal imports Main begin
-
-datatype ordinal = Zero | Succ ordinal | Limit "nat \<Rightarrow> ordinal"
-
-consts
- pred :: "ordinal \<Rightarrow> nat \<Rightarrow> ordinal option"
-primrec
- "pred Zero n = None"
- "pred (Succ a) n = Some a"
- "pred (Limit f) n = Some (f n)"
-
-definition OpLim :: "(nat \<Rightarrow> (ordinal \<Rightarrow> ordinal)) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" where
- "OpLim F a \<equiv> Limit (\<lambda>n. F n a)"
-
-definition OpItw :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" ("\<Squnion>") where
- "\<Squnion>f \<equiv> OpLim (power f)"
-
-consts
- cantor :: "ordinal \<Rightarrow> ordinal \<Rightarrow> 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 \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> 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))"
-
-definition deriv :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" where
- "deriv f \<equiv> \<nabla>(\<Squnion>f)"
-
-consts
- veblen :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal"
-primrec
- "veblen Zero = \<nabla>(OpLim (power (cantor Zero)))"
- "veblen (Succ a) = \<nabla>(OpLim (power (veblen a)))"
- "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
-
-definition veb :: "ordinal \<Rightarrow> ordinal" where
- "veb a \<equiv> veblen a Zero"
-
-definition epsilon0 :: ordinal ("\<epsilon>\<^sub>0") where
- "\<epsilon>\<^sub>0 \<equiv> veb Zero"
-
-definition Gamma0 :: ordinal ("\<Gamma>\<^sub>0") where
- "\<Gamma>\<^sub>0 \<equiv> Limit (\<lambda>n. (veb^n) Zero)"
-thm Gamma0_def
-
-end