# HG changeset patch
# User lcp
# Date 776967927 -7200
# Node ID e62519a8497d0a5ad36d677416f7ba3e8040b03e
# Parent  b1bf18e83302053eacff50d678bfc87e77d018d4
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold

diff -r b1bf18e83302 -r e62519a8497d src/ZF/List.ML
--- a/src/ZF/List.ML	Mon Aug 15 18:15:09 1994 +0200
+++ b/src/ZF/List.ML	Mon Aug 15 18:25:27 1994 +0200
@@ -24,12 +24,10 @@
 	   ares_tac prems i];
 
 goal List.thy "list(A) = {0} + (A * list(A))";
-by (rtac (list.unfold RS trans) 1);
-bws list.con_defs;
-br equalityI 1;
-by (fast_tac sum_cs 1);
-by (fast_tac (sum_cs addIs datatype_intrs
-		     addDs [list.dom_subset RS subsetD]) 1);
+let open list;  val rew = rewrite_rule con_defs in  
+by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+                     addEs [rew elim]) 1)
+end;
 val list_unfold = result();
 
 (**  Lemmas to justify using "list" in other recursive type definitions **)
@@ -48,6 +46,7 @@
 			    Pair_in_univ]) 1);
 val list_univ = result();
 
+(*These two theorems are unused -- useful??*)
 val list_subset_univ = standard ([list_mono, list_univ] MRS subset_trans);
 
 goal List.thy "!!l A B. [| l: list(A);  A <= univ(B) |] ==> l: univ(B)";
diff -r b1bf18e83302 -r e62519a8497d src/ZF/ex/Brouwer.ML
--- a/src/ZF/ex/Brouwer.ML	Mon Aug 15 18:15:09 1994 +0200
+++ b/src/ZF/ex/Brouwer.ML	Mon Aug 15 18:25:27 1994 +0200
@@ -3,19 +3,20 @@
     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
 *)
 
 open Brouwer;
 
+(** The Brouwer ordinals **)
+
 goal Brouwer.thy "brouwer = {0} + brouwer + (nat -> brouwer)";
-by (rtac (brouwer.unfold RS trans) 1);
-bws brouwer.con_defs;
-br equalityI 1;
-by (fast_tac sum_cs 1);
-by (fast_tac (sum_cs addIs inf_datatype_intrs
- 	             addDs [brouwer.dom_subset RS subsetD]
- 	             addEs [fun_into_Vcsucc]) 1);
+let open brouwer;  val rew = rewrite_rule con_defs in  
+by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+                     addEs [rew elim]) 1)
+end;
 val brouwer_unfold = result();
 
 (*A nicer induction rule than the standard one*)
@@ -31,3 +32,33 @@
 by (fast_tac (ZF_cs addEs [fun_weaken_type]) 1);
 by (fast_tac (ZF_cs addDs [apply_type]) 1);
 val brouwer_induct2 = result();
+
+
+(** The Martin-Löf wellordering type **)
+
+goal Brouwer.thy "Well(A,B) = (SUM x:A. B(x) -> Well(A,B))";
+let open Well;  val rew = rewrite_rule con_defs in  
+by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+                     addEs [rew elim]) 1)
+end;
+val Well_unfold = result();
+
+(*A nicer induction rule than the standard one*)
+val major::prems = goal Brouwer.thy
+    "[| w: Well(A,B);  							\
+\	!!a f. [| a: A;  f: B(a) -> Well(A,B);  ALL y: B(a). P(f`y)	\
+\            |] ==> P(Sup(a,f))						\
+\    |] ==> P(w)";
+by (rtac (major RS Well.induct) 1);
+by (REPEAT_SOME (ares_tac prems));
+by (fast_tac (ZF_cs addEs [fun_weaken_type]) 1);
+by (fast_tac (ZF_cs addDs [apply_type]) 1);
+val Well_induct2 = result();
+
+
+(*In fact it's isomorphic to nat, but we need a recursion operator for
+  Well to prove this.*)
+goal Brouwer.thy "Well(bool, %x.x) = 1 + (1 -> Well(bool, %x.x))";
+by (resolve_tac [Well_unfold RS trans] 1);
+by (simp_tac (ZF_ss addsimps [Sigma_bool, Pi_empty1, succ_def]) 1);
+val Well_bool_unfold = result();