# HG changeset patch
# User paulson
# Date 1117030480 -7200
# Node ID e1364521a25054a8630e02fc343ceb93657f2163
# Parent  c04f972bfabeb4389106f78d83f735171680982d
new Brouwer ordinal example

diff -r c04f972bfabe -r e1364521a250 src/HOL/Induct/Tree.thy
--- a/src/HOL/Induct/Tree.thy	Wed May 25 11:18:02 2005 +0200
+++ b/src/HOL/Induct/Tree.thy	Wed May 25 16:14:40 2005 +0200
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Induct/Tree.thy
     ID:         $Id$
     Author:     Stefan Berghofer,  TU Muenchen
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
 header {* Infinitely branching trees *}
@@ -31,4 +32,41 @@
     exists_tree P ts ==> exists_tree Q (map_tree f ts)"
   by (induct ts) auto
 
+
+subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*}
+
+datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
+
+text{*Addition of ordinals*}
+consts
+  add :: "[brouwer,brouwer] => brouwer"
+primrec
+  "add i Zero = i"
+  "add i (Succ j) = Succ (add i j)"
+  "add i (Lim f) = Lim (%n. add i (f n))"
+
+lemma add_assoc: "add (add i j) k = add i (add j k)"
+by (induct k, auto)
+
+text{*Multiplication of ordinals*}
+consts
+  mult :: "[brouwer,brouwer] => brouwer"
+primrec
+  "mult i Zero = Zero"
+  "mult i (Succ j) = add (mult i j) i"
+  "mult i (Lim f) = Lim (%n. mult i (f n))"
+
+lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
+apply (induct k) 
+apply (auto simp add: add_assoc) 
+done
+
+lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
+apply (induct k) 
+apply (auto simp add: add_mult_distrib) 
+done
+
+text{*We could probably instantiate some axiomatic type classes and use
+the standard infix operators.*}
+
 end