# HG changeset patch
# User lcp
# Date 777206883 -7200
# Node ID b7f57e0ab47c3d83bd4870f14809fea539d9847b
# Parent  0b9b8eb74101b4ef0cf2038afb0840956e848ef4
HOL/ex/Term, Simult: updated for new Split

diff -r 0b9b8eb74101 -r b7f57e0ab47c ex/Simult.ML
--- a/ex/Simult.ML	Thu Aug 18 12:42:19 1994 +0200
+++ b/ex/Simult.ML	Thu Aug 18 12:48:03 1994 +0200
@@ -1,9 +1,9 @@
-(*  Title: 	HOL/ex/simult.ML
+(*  Title: 	HOL/ex/Simult.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-For simult.thy.
+For Simult.thy.
 
 Primitives for simultaneous recursive type definitions
   includes worked example of trees & forests
@@ -15,30 +15,6 @@
 
 open Simult;
 
-(*** General rules for Part ***)
-
-val prems = goalw Simult.thy [Part_def] "h(a) : A ==> h(a) : Part(A,h)";
-by (cfast_tac prems 1);
-val PartI = result();
-
-val major::prems = goalw Simult.thy [Part_def]
-    "[| a : Part(A,h);  !!z. [| a : A;  a=h(z) |] ==> P  \
-\    |] ==> P";
-by (rtac (major RS CollectE) 1);
-by (etac conjE 1);
-by (etac exE 1);
-by (REPEAT (ares_tac prems 1));
-val PartE = result();
-
-goal Simult.thy "!!A B. A<=B ==> Part(A,h) <= Part(B,h)";
-by (fast_tac (set_cs addSIs [PartI] addSEs [PartE]) 1);
-val Part_mono = result();
-
-val [prem] = goal Simult.thy "A<=B ==> Part(A,h) <= B";
-by (fast_tac (set_cs addSIs [PartI, prem RS subsetD] addSEs [PartE]) 1);
-val Part_subset = result();
-
-
 (*** Monotonicity and unfolding of the function ***)
 
 goal Simult.thy "mono(%Z.  A <*> Part(Z,In1) \
@@ -259,48 +235,43 @@
 
 (** conversion rules for TF_rec **)
 
-val prems = goalw Simult.thy [TCONS_def]
-    "[| M: Sexp;  N: Sexp |] ==> 	\
-\    TF_rec(TCONS(M,N),b,c,d) = b(M, N, TF_rec(N,b,c,d))";
+goalw Simult.thy [TCONS_def]
+    "!!M N. [| M: Sexp;  N: Sexp |] ==> 	\
+\           TF_rec(TCONS(M,N),b,c,d) = b(M, N, TF_rec(N,b,c,d))";
 by (rtac (TF_rec_unfold RS trans) 1);
-by (rtac (Case_In0 RS trans) 1);
-by (rtac (Split RS trans) 1);
-by (rewtac In0_def);
-by (simp_tac (pred_Sexp_ss addsimps prems) 1);
+by (simp_tac (HOL_ss addsimps [Case_In0, Split]) 1);
+by (asm_simp_tac (pred_Sexp_ss addsimps [In0_def]) 1);
 val TF_rec_TCONS = result();
 
 goalw Simult.thy [FNIL_def] "TF_rec(FNIL,b,c,d) = c";
 by (rtac (TF_rec_unfold RS trans) 1);
-by (rtac (Case_In1 RS trans) 1);
-by (rtac List_case_NIL 1);
+by (simp_tac (HOL_ss addsimps [Case_In1, List_case_NIL]) 1);
 val TF_rec_FNIL = result();
 
-val prems = goalw Simult.thy [FCONS_def]
-    "[| M: Sexp;  N: Sexp |] ==> 	\
-\    TF_rec(FCONS(M,N),b,c,d) = d(M, N, TF_rec(M,b,c,d), TF_rec(N,b,c,d))";
+goalw Simult.thy [FCONS_def]
+ "!!M N. [| M: Sexp;  N: Sexp |] ==> 	\
+\        TF_rec(FCONS(M,N),b,c,d) = d(M, N, TF_rec(M,b,c,d), TF_rec(N,b,c,d))";
 by (rtac (TF_rec_unfold RS trans) 1);
-by (rtac (Case_In1 RS trans) 1);
-by (rtac (List_case_CONS RS trans) 1);
-by (rewrite_goals_tac [CONS_def,In1_def]);
-by (simp_tac (pred_Sexp_ss addsimps prems) 1);
+by (simp_tac (HOL_ss addsimps [Case_In1, List_case_CONS]) 1);
+by (asm_simp_tac (pred_Sexp_ss addsimps [CONS_def,In1_def]) 1);
 val TF_rec_FCONS = result();
 
 
 (*** tree_rec, forest_rec -- by TF_rec ***)
 
 val Rep_Tree_in_Sexp =
-    Rep_Tree RS (range_Leaf_subset_Sexp RS TF_subset_Sexp RS 
-		   Part_subset RS subsetD);
+    [range_Leaf_subset_Sexp RS TF_subset_Sexp RS (Part_subset RS subset_trans),
+     Rep_Tree] MRS subsetD;
 val Rep_Forest_in_Sexp =
-    Rep_Forest RS (range_Leaf_subset_Sexp RS TF_subset_Sexp RS 
-		   Part_subset RS subsetD);
+    [range_Leaf_subset_Sexp RS TF_subset_Sexp RS (Part_subset RS subset_trans),
+     Rep_Forest] MRS subsetD;
 
 val tf_rec_simps = [TF_rec_TCONS, TF_rec_FNIL, TF_rec_FCONS,
-		 TCONS_I, FNIL_I, FCONS_I, Rep_Tree, Rep_Forest,
-		 Rep_Tree_inverse, Rep_Forest_inverse,
-		 Abs_Tree_inverse, Abs_Forest_inverse,
-		 inj_Leaf, Inv_f_f, Sexp_LeafI, range_eqI,
-		 Rep_Tree_in_Sexp, Rep_Forest_in_Sexp];
+		    TCONS_I, FNIL_I, FCONS_I, Rep_Tree, Rep_Forest,
+		    Rep_Tree_inverse, Rep_Forest_inverse,
+		    Abs_Tree_inverse, Abs_Forest_inverse,
+		    inj_Leaf, Inv_f_f, Sexp_LeafI, range_eqI,
+		    Rep_Tree_in_Sexp, Rep_Forest_in_Sexp];
 val tf_rec_ss = HOL_ss addsimps tf_rec_simps;
 
 goalw Simult.thy [tree_rec_def, forest_rec_def, Tcons_def]
diff -r 0b9b8eb74101 -r b7f57e0ab47c ex/Simult.thy
--- a/ex/Simult.thy	Thu Aug 18 12:42:19 1994 +0200
+++ b/ex/Simult.thy	Thu Aug 18 12:48:03 1994 +0200
@@ -3,8 +3,7 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Primitives for simultaneous recursive type definitions
-  includes worked example of trees & forests
+A simultaneous recursive type definition: trees & forests
 
 This is essentially the same data structure that on ex/term.ML, which is
 simpler because it uses List as a new type former.  The approach in this
@@ -19,7 +18,6 @@
 arities  tree,forest :: (term)term
 
 consts
-  Part        :: "['a set, 'a=>'a] => 'a set"
   TF          :: "'a node set set => 'a node set set"
   FNIL        :: "'a node set"
   TCONS,FCONS :: "['a node set, 'a node set] => 'a node set"
@@ -38,9 +36,6 @@
 \                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
 
 rules
-    (*operator for selecting out the various types*)
-  Part_def	"Part(A,h) == {x. x:A & (? z. x = h(z))}"
-
   TF_def	"TF(A) == lfp(%Z. A <*> Part(Z,In1) \
 \                           <+> ({Numb(0)} <+> Part(Z,In0) <*> Part(Z,In1)))"
     (*faking a type definition for tree...*)
@@ -65,9 +60,8 @@
      (*recursion*)
   TF_rec_def	
    "TF_rec(M,b,c,d) == wfrec(trancl(pred_Sexp), M, 			\
-\               %Z g. Case(Z, %U. Split(U, %x y. b(x,y,g(y))),		\
-\			      %V. List_case(V, c, 			\
-\                                           %x y. d(x,y,g(x),g(y)))))"
+\               Case(Split(%x y g. b(x,y,g(y))),		\
+\	              List_case(%g.c, %x y g. d(x,y,g(x),g(y)))))"
 
   tree_rec_def
    "tree_rec(t,b,c,d) == \
diff -r 0b9b8eb74101 -r b7f57e0ab47c ex/Term.ML
--- a/ex/Term.ML	Thu Aug 18 12:42:19 1994 +0200
+++ b/ex/Term.ML	Thu Aug 18 12:48:03 1994 +0200
@@ -145,9 +145,9 @@
     "[| M: Sexp;  N: List(Term(A));  A<=Sexp |] ==> \
 \    Term_rec(M$N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))";
 by (rtac (Term_rec_unfold RS trans) 1);
-by (rtac (Split RS trans) 1);
 by (simp_tac (HOL_ss addsimps
-      [prem2 RS Abs_map_lemma RS spec RS mp, pred_SexpI2 RS r_into_trancl,
+      [Split,
+       prem2 RS Abs_map_lemma RS spec RS mp, pred_SexpI2 RS r_into_trancl,
        prem1, prem2 RS rev_subsetD, List_subset_Sexp,
        Term_subset_Sexp, A_subset_Sexp])1);
 val Term_rec = result();
diff -r 0b9b8eb74101 -r b7f57e0ab47c ex/Term.thy
--- a/ex/Term.thy	Thu Aug 18 12:42:19 1994 +0200
+++ b/ex/Term.thy	Thu Aug 18 12:48:03 1994 +0200
@@ -40,7 +40,7 @@
      (*list recursion*)
   Term_rec_def	
    "Term_rec(M,d) == wfrec(trancl(pred_Sexp),  M, \
-\            %M g. Split(M, %x y. d(x,y, Abs_map(g,y))))"
+\            Split(%x y g. d(x,y, Abs_map(g,y))))"
 
   term_rec_def
    "term_rec(t,d) == \