67 done |
67 done |
68 |
68 |
69 text{*We could probably instantiate some axiomatic type classes and use |
69 text{*We could probably instantiate some axiomatic type classes and use |
70 the standard infix operators.*} |
70 the standard infix operators.*} |
71 |
71 |
|
72 subsection{*A WF Ordering for The Brouwer ordinals (Michael Compton)*} |
|
73 |
|
74 text{*To define recdef style functions we need an ordering on the Brouwer |
|
75 ordinals. Start with a predecessor relation and form its transitive |
|
76 closure. *} |
|
77 |
|
78 constdefs |
|
79 brouwer_pred :: "(brouwer * brouwer) set" |
|
80 "brouwer_pred == \<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)}" |
|
81 |
|
82 brouwer_order :: "(brouwer * brouwer) set" |
|
83 "brouwer_order == brouwer_pred^+" |
|
84 |
|
85 lemma wf_brouwer_pred: "wf brouwer_pred" |
|
86 by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+) |
|
87 |
|
88 lemma wf_brouwer_order: "wf brouwer_order" |
|
89 by(unfold brouwer_order_def, rule wf_trancl[OF wf_brouwer_pred]) |
|
90 |
|
91 lemma [simp]: "(j, Succ j) : brouwer_order" |
|
92 by(auto simp add: brouwer_order_def brouwer_pred_def) |
|
93 |
|
94 lemma [simp]: "(f n, Lim f) : brouwer_order" |
|
95 by(auto simp add: brouwer_order_def brouwer_pred_def) |
|
96 |
|
97 text{*Example of a recdef*} |
|
98 consts |
|
99 add2 :: "(brouwer*brouwer) => brouwer" |
|
100 recdef add2 "inv_image brouwer_order (\<lambda> (x,y). y)" |
|
101 "add2 (i, Zero) = i" |
|
102 "add2 (i, (Succ j)) = Succ (add2 (i, j))" |
|
103 "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))" |
|
104 (hints recdef_wf: wf_brouwer_order) |
|
105 |
|
106 lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))" |
|
107 by (induct k, auto) |
|
108 |
|
109 |
72 end |
110 end |