new Brouwer ordinal example
authorpaulson
Wed May 25 16:14:40 2005 +0200 (2005-05-25)
changeset 16078e1364521a250
parent 16077 c04f972bfabe
child 16079 757e1c4a8081
new Brouwer ordinal example
src/HOL/Induct/Tree.thy
     1.1 --- a/src/HOL/Induct/Tree.thy	Wed May 25 11:18:02 2005 +0200
     1.2 +++ b/src/HOL/Induct/Tree.thy	Wed May 25 16:14:40 2005 +0200
     1.3 @@ -1,6 +1,7 @@
     1.4  (*  Title:      HOL/Induct/Tree.thy
     1.5      ID:         $Id$
     1.6      Author:     Stefan Berghofer,  TU Muenchen
     1.7 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8  *)
     1.9  
    1.10  header {* Infinitely branching trees *}
    1.11 @@ -31,4 +32,41 @@
    1.12      exists_tree P ts ==> exists_tree Q (map_tree f ts)"
    1.13    by (induct ts) auto
    1.14  
    1.15 +
    1.16 +subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*}
    1.17 +
    1.18 +datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
    1.19 +
    1.20 +text{*Addition of ordinals*}
    1.21 +consts
    1.22 +  add :: "[brouwer,brouwer] => brouwer"
    1.23 +primrec
    1.24 +  "add i Zero = i"
    1.25 +  "add i (Succ j) = Succ (add i j)"
    1.26 +  "add i (Lim f) = Lim (%n. add i (f n))"
    1.27 +
    1.28 +lemma add_assoc: "add (add i j) k = add i (add j k)"
    1.29 +by (induct k, auto)
    1.30 +
    1.31 +text{*Multiplication of ordinals*}
    1.32 +consts
    1.33 +  mult :: "[brouwer,brouwer] => brouwer"
    1.34 +primrec
    1.35 +  "mult i Zero = Zero"
    1.36 +  "mult i (Succ j) = add (mult i j) i"
    1.37 +  "mult i (Lim f) = Lim (%n. mult i (f n))"
    1.38 +
    1.39 +lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
    1.40 +apply (induct k) 
    1.41 +apply (auto simp add: add_assoc) 
    1.42 +done
    1.43 +
    1.44 +lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
    1.45 +apply (induct k) 
    1.46 +apply (auto simp add: add_mult_distrib) 
    1.47 +done
    1.48 +
    1.49 +text{*We could probably instantiate some axiomatic type classes and use
    1.50 +the standard infix operators.*}
    1.51 +
    1.52  end