--- 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]