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

diff -r 61dc99226f8f -r f0d16216e394 src/ZF/ex/Data.ML
--- a/src/ZF/ex/Data.ML	Mon Aug 15 18:37:25 1994 +0200
+++ b/src/ZF/ex/Data.ML	Mon Aug 15 18:38:38 1994 +0200
@@ -10,15 +10,10 @@
 open Data;
 
 goal Data.thy "data(A,B) = ({0} + A) + (A*B + A*B*data(A,B))";
-by (rtac (data.unfold RS trans) 1);
-bws data.con_defs;
-br equalityI 1;
-by (fast_tac sum_cs 1);
-(*for this direction, fast_tac is just too slow!*)
-by (safe_tac sum_cs);
-by (REPEAT_FIRST (swap_res_tac [refl, conjI, disjCI, exI]));
-by (REPEAT (fast_tac (sum_cs addIs datatype_intrs
-  		             addDs [data.dom_subset RS subsetD]) 1));
+let open data;  val rew = rewrite_rule con_defs in  
+by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+                     addEs [rew elim]) 1)
+end;
 val data_unfold = result();
 
 (**  Lemmas to justify using "data" in other recursive type definitions **)
diff -r 61dc99226f8f -r f0d16216e394 src/ZF/ex/LList.ML
--- a/src/ZF/ex/LList.ML	Mon Aug 15 18:37:25 1994 +0200
+++ b/src/ZF/ex/LList.ML	Mon Aug 15 18:38:38 1994 +0200
@@ -16,13 +16,10 @@
 val LNil_LCons_iff = llist.mk_free "~ LNil=LCons(a,l)";
 
 goal LList.thy "llist(A) = {0} <+> (A <*> llist(A))";
-by (rtac (llist.unfold RS trans) 1);
-bws llist.con_defs;
-br equalityI 1;
-by (fast_tac qsum_cs 1);
-by (fast_tac (qsum_cs addIs codatatype_intrs
-		      addDs [llist.dom_subset RS subsetD]
- 	              addSEs [QSigmaE]) 1);
+let open llist;  val rew = rewrite_rule con_defs in  
+by (fast_tac (qsum_cs addSIs (equalityI :: map rew intrs)
+                      addEs [rew elim]) 1)
+end;
 val llist_unfold = result();
 
 (*** Lemmas to justify using "llist" in other recursive type definitions ***)
diff -r 61dc99226f8f -r f0d16216e394 src/ZF/ex/Ntree.ML
--- a/src/ZF/ex/Ntree.ML	Mon Aug 15 18:37:25 1994 +0200
+++ b/src/ZF/ex/Ntree.ML	Mon Aug 15 18:38:38 1994 +0200
@@ -12,13 +12,10 @@
 open Ntree;
 
 goal Ntree.thy "ntree(A) = A * (UN n: nat. n -> ntree(A))";
-by (rtac (ntree.unfold RS trans) 1);
-bws ntree.con_defs;
-br equalityI 1;
-by (fast_tac sum_cs 1);
-by (fast_tac (sum_cs addIs datatype_intrs
- 	             addDs [ntree.dom_subset RS subsetD]
- 	             addEs [nat_fun_into_univ]) 1);
+let open ntree;  val rew = rewrite_rule con_defs in  
+by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+                     addEs [rew elim]) 1)
+end;
 val ntree_unfold = result();
 
 (*A nicer induction rule than the standard one*)
diff -r 61dc99226f8f -r f0d16216e394 src/ZF/ex/TF.ML
--- a/src/ZF/ex/TF.ML	Mon Aug 15 18:37:25 1994 +0200
+++ b/src/ZF/ex/TF.ML	Mon Aug 15 18:38:38 1994 +0200
@@ -31,23 +31,17 @@
 
 (** NOT useful, but interesting... **)
 
-(*The (refl RS conjI RS exI RS exI) avoids considerable search!*)
-val unfold_cs = sum_cs addSIs [PartI, refl RS conjI RS exI RS exI]
-                    addIs datatype_intrs
-                    addDs [tree_forest.dom_subset RS subsetD]
-	            addSEs ([PartE] @ datatype_elims @ tree_forest.free_SEs);
-
-goalw TF.thy (tl tree_forest.defs)
+goalw TF.thy (tl tree_forest.defs) 
     "tree_forest(A) = (A*forest(A)) + ({0} + tree(A)*forest(A))";
-by (rtac (tree_forest.unfold RS trans) 1);
-by (rewrite_goals_tac tree_forest.con_defs);
-by (rtac equalityI 1);
-by (fast_tac unfold_cs 1);
-by (fast_tac unfold_cs 1);
+let open tree_forest;  
+    val rew = rewrite_rule (con_defs @ tl defs) in  
+by (fast_tac (sum_cs addSIs (equalityI :: PartI :: (map rew intrs RL [PartD1]))
+                     addEs [PartE, rew elim]) 1)
+end;
 val tree_forest_unfold = result();
 
-val tree_forest_unfold' = rewrite_rule (tl tree_forest.defs) tree_forest_unfold;
-
+val tree_forest_unfold' = rewrite_rule (tl tree_forest.defs) 
+                          tree_forest_unfold;
 
 goalw TF.thy (tl tree_forest.defs)
     "tree(A) = {Inl(x). x: A*forest(A)}";
diff -r 61dc99226f8f -r f0d16216e394 src/ZF/ex/Term.ML
--- a/src/ZF/ex/Term.ML	Mon Aug 15 18:37:25 1994 +0200
+++ b/src/ZF/ex/Term.ML	Mon Aug 15 18:38:38 1994 +0200
@@ -10,13 +10,10 @@
 open Term;
 
 goal Term.thy "term(A) = A * list(term(A))";
-by (rtac (term.unfold RS trans) 1);
-bws term.con_defs;
-br equalityI 1;
-by (fast_tac sum_cs 1);
-by (fast_tac (sum_cs addIs datatype_intrs
- 	             addDs [term.dom_subset RS subsetD]
- 	             addEs [list_into_univ]) 1);
+let open term;  val rew = rewrite_rule con_defs in  
+by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+                     addEs [rew elim]) 1)
+end;
 val term_unfold = result();
 
 (*Induction on term(A) followed by induction on List *)