# HG changeset patch
# User lcp
# Date 776968645 -7200
# Node ID 61dc99226f8f6aeeca1da9873c94b3d7739b4b50
# Parent  35c70ab82940169c0b22df1c642cf7852f3abd99
ZF/ex/Brouwer.thy,.ML: new example of wellordering types

diff -r 35c70ab82940 -r 61dc99226f8f src/ZF/ex/Brouwer.thy
--- a/src/ZF/ex/Brouwer.thy	Mon Aug 15 18:31:29 1994 +0200
+++ b/src/ZF/ex/Brouwer.thy	Mon Aug 15 18:37:25 1994 +0200
@@ -3,16 +3,27 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-Datatype definition of the Brouwer ordinals -- demonstrates infinite branching
+Infinite branching datatype definitions
+  (1) the Brouwer ordinals
+  (2) the Martin-Löf wellordering type
 *)
 
 Brouwer = InfDatatype +
 consts
   brouwer :: "i"
+  Well    :: "[i,i=>i]=>i"
  
 datatype <= "Vfrom(0, csucc(nat))"
   "brouwer" = Zero | Suc ("b: brouwer") | Lim ("h: nat -> brouwer")
   monos	      "[Pi_mono]"
   type_intrs  "inf_datatype_intrs"
 
+(*The union with nat ensures that the cardinal is infinite*)
+datatype <= "Vfrom(A Un (UN x:A. B(x)), csucc(nat Un |UN x:A. B(x)|))"
+  "Well(A,B)" = Sup ("a:A", "f: B(a) -> Well(A,B)")
+  monos	      "[Pi_mono]"
+  type_intrs  "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]   \
+\	       @ inf_datatype_intrs"
+
+
 end