--- a/ex/Simult.ML Wed Aug 24 18:49:29 1994 +0200
+++ b/ex/Simult.ML Thu Aug 25 10:47:33 1994 +0200
@@ -3,13 +3,11 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-For Simult.thy.
-
Primitives for simultaneous recursive type definitions
includes worked example of 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
+simpler because it uses list as a new type former. The approach in this
file may be superior for other simultaneous recursions.
*)
@@ -29,15 +27,15 @@
by (REPEAT (ares_tac [lfp_mono, subset_refl, usum_mono, uprod_mono] 1));
val TF_mono = result();
-goalw Simult.thy [TF_def] "TF(Sexp) <= Sexp";
+goalw Simult.thy [TF_def] "TF(sexp) <= sexp";
by (rtac lfp_lowerbound 1);
-by (fast_tac (univ_cs addIs [Sexp_NumbI,Sexp_In0I,Sexp_In1I,Sexp_SconsI]
+by (fast_tac (univ_cs addIs sexp.intrs@[sexp_In0I, sexp_In1I]
addSEs [PartE]) 1);
-val TF_Sexp = result();
+val TF_sexp = result();
-(* A <= Sexp ==> TF(A) <= Sexp *)
-val TF_subset_Sexp = standard
- (TF_mono RS (TF_Sexp RSN (2,subset_trans)));
+(* A <= sexp ==> TF(A) <= sexp *)
+val TF_subset_sexp = standard
+ (TF_mono RS (TF_sexp RSN (2,subset_trans)));
(** Elimination -- structural induction on the set TF **)
@@ -51,8 +49,7 @@
\ !!M N. [| M: Part(TF(A),In0); N: Part(TF(A),In1); R(M); R(N) \
\ |] ==> R(FCONS(M,N)) \
\ |] ==> R(i)";
-by (rtac (major RS (TF_def RS def_induct)) 1);
-by (rtac TF_fun_mono 1);
+by (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1);
by (fast_tac (set_cs addIs (prems@[PartI])
addEs [usumE, uprodE, PartE]) 1);
val TF_induct = result();
@@ -228,19 +225,19 @@
val Fcons_inject = standard (Fcons_Fcons_eq RS iffD1 RS conjE);
-(*** TF_rec -- by wf recursion on pred_Sexp ***)
+(*** TF_rec -- by wf recursion on pred_sexp ***)
val TF_rec_unfold =
- wf_pred_Sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
+ wf_pred_sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
(** conversion rules for TF_rec **)
goalw Simult.thy [TCONS_def]
- "!!M N. [| M: Sexp; N: Sexp |] ==> \
+ "!!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 (simp_tac (HOL_ss addsimps [Case_In0, Split]) 1);
-by (asm_simp_tac (pred_Sexp_ss addsimps [In0_def]) 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";
@@ -249,29 +246,29 @@
val TF_rec_FNIL = result();
goalw Simult.thy [FCONS_def]
- "!!M N. [| M: Sexp; N: Sexp |] ==> \
+ "!!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 (simp_tac (HOL_ss addsimps [Case_In1, List_case_CONS]) 1);
-by (asm_simp_tac (pred_Sexp_ss addsimps [CONS_def,In1_def]) 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 =
- [range_Leaf_subset_Sexp RS TF_subset_Sexp RS (Part_subset RS subset_trans),
+val Rep_Tree_in_sexp =
+ [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans),
Rep_Tree] MRS subsetD;
-val Rep_Forest_in_Sexp =
- [range_Leaf_subset_Sexp RS TF_subset_Sexp RS (Part_subset RS subset_trans),
+val Rep_Forest_in_sexp =
+ [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];
+ 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]