ex/Simult.ML

--- a/ex/Simult.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/ex/Simult.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -19,19 +19,19 @@
 \                      <+> ({Numb(0)} <+> Part(Z,In0) <*> Part(Z,In1)))";
 by (REPEAT (ares_tac [monoI, subset_refl, usum_mono, uprod_mono,
 		      Part_mono] 1));
-val TF_fun_mono = result();
+qed "TF_fun_mono";
 
 val TF_unfold = TF_fun_mono RS (TF_def RS def_lfp_Tarski);
 
 goalw Simult.thy [TF_def] "!!A B. A<=B ==> TF(A) <= TF(B)";
 by (REPEAT (ares_tac [lfp_mono, subset_refl, usum_mono, uprod_mono] 1));
-val TF_mono = result();
+qed "TF_mono";
 
 goalw Simult.thy [TF_def] "TF(sexp) <= sexp";
 by (rtac lfp_lowerbound 1);
 by (fast_tac (univ_cs addIs  sexp.intrs@[sexp_In0I, sexp_In1I]
                       addSEs [PartE]) 1);
-val TF_sexp = result();
+qed "TF_sexp";
 
 (* A <= sexp ==> TF(A) <= sexp *)
 val TF_subset_sexp = standard
@@ -52,14 +52,14 @@
 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();
+qed "TF_induct";
 
 (*This lemma replaces a use of subgoal_tac to prove tree_forest_induct*)
 val prems = goalw Simult.thy [Part_def]
  "! M: TF(A). (M: Part(TF(A),In0) --> P(M)) & (M: Part(TF(A),In1) --> Q(M)) \
 \ ==> (! M: Part(TF(A),In0). P(M)) & (! M: Part(TF(A),In1). Q(M))";
 by (cfast_tac prems 1);
-val TF_induct_lemma = result();
+qed "TF_induct_lemma";
 
 val uplus_cs = set_cs addSIs [PartI]
 		      addSDs [In0_inject, In1_inject]
@@ -79,7 +79,7 @@
 by (rewrite_goals_tac TF_Rep_defs);
 by (ALLGOALS (fast_tac (uplus_cs addIs prems)));
 (*29 secs??*)
-val Tree_Forest_induct = result();
+qed "Tree_Forest_induct";
 
 (*Induction for the abstract types 'a tree, 'a forest*)
 val prems = goalw Simult.thy [Tcons_def,Fnil_def,Fcons_def]
@@ -98,7 +98,7 @@
 by (ALLGOALS (fast_tac (set_cs addSEs [Abs_Tree_inverse RS subst,
                           Abs_Forest_inverse RS subst] 
 	             addSIs prems)));
-val tree_forest_induct = result();
+qed "tree_forest_induct";
 
 
 
@@ -107,22 +107,22 @@
 goal Simult.thy "inj(Rep_Tree)";
 by (rtac inj_inverseI 1);
 by (rtac Rep_Tree_inverse 1);
-val inj_Rep_Tree = result();
+qed "inj_Rep_Tree";
 
 goal Simult.thy "inj_onto(Abs_Tree,Part(TF(range(Leaf)),In0))";
 by (rtac inj_onto_inverseI 1);
 by (etac Abs_Tree_inverse 1);
-val inj_onto_Abs_Tree = result();
+qed "inj_onto_Abs_Tree";
 
 goal Simult.thy "inj(Rep_Forest)";
 by (rtac inj_inverseI 1);
 by (rtac Rep_Forest_inverse 1);
-val inj_Rep_Forest = result();
+qed "inj_Rep_Forest";
 
 goal Simult.thy "inj_onto(Abs_Forest,Part(TF(range(Leaf)),In1))";
 by (rtac inj_onto_inverseI 1);
 by (etac Abs_Forest_inverse 1);
-val inj_onto_Abs_Forest = result();
+qed "inj_onto_Abs_Forest";
 
 (** Introduction rules for constructors **)
 
@@ -137,36 +137,36 @@
 val prems = goalw Simult.thy TF_Rep_defs
     "[| a: A;  M: Part(TF(A),In1) |] ==> TCONS(a,M) : Part(TF(A),In0)";
 by (fast_tac (TF_Rep_cs addIs prems) 1);
-val TCONS_I = result();
+qed "TCONS_I";
 
 (* FNIL is a TF(A) -- this also justifies the type definition*)
 goalw Simult.thy TF_Rep_defs "FNIL: Part(TF(A),In1)";
 by (fast_tac TF_Rep_cs 1);
-val FNIL_I = result();
+qed "FNIL_I";
 
 val prems = goalw Simult.thy TF_Rep_defs
     "[| M: Part(TF(A),In0);  N: Part(TF(A),In1) |] ==> \
 \    FCONS(M,N) : Part(TF(A),In1)";
 by (fast_tac (TF_Rep_cs addIs prems) 1);
-val FCONS_I = result();
+qed "FCONS_I";
 
 (** Injectiveness of TCONS and FCONS **)
 
 goalw Simult.thy TF_Rep_defs "(TCONS(K,M)=TCONS(L,N)) = (K=L & M=N)";
 by (fast_tac TF_Rep_cs 1);
-val TCONS_TCONS_eq = result();
+qed "TCONS_TCONS_eq";
 val TCONS_inject = standard (TCONS_TCONS_eq RS iffD1 RS conjE);
 
 goalw Simult.thy TF_Rep_defs "(FCONS(K,M)=FCONS(L,N)) = (K=L & M=N)";
 by (fast_tac TF_Rep_cs 1);
-val FCONS_FCONS_eq = result();
+qed "FCONS_FCONS_eq";
 val FCONS_inject = standard (FCONS_FCONS_eq RS iffD1 RS conjE);
 
 (** Distinctness of TCONS, FNIL and FCONS **)
 
 goalw Simult.thy TF_Rep_defs "TCONS(M,N) ~= FNIL";
 by (fast_tac TF_Rep_cs 1);
-val TCONS_not_FNIL = result();
+qed "TCONS_not_FNIL";
 val FNIL_not_TCONS = standard (TCONS_not_FNIL RS not_sym);
 
 val TCONS_neq_FNIL = standard (TCONS_not_FNIL RS notE);
@@ -174,7 +174,7 @@
 
 goalw Simult.thy TF_Rep_defs "FCONS(M,N) ~= FNIL";
 by (fast_tac TF_Rep_cs 1);
-val FCONS_not_FNIL = result();
+qed "FCONS_not_FNIL";
 val FNIL_not_FCONS = standard (FCONS_not_FNIL RS not_sym);
 
 val FCONS_neq_FNIL = standard (FCONS_not_FNIL RS notE);
@@ -182,7 +182,7 @@
 
 goalw Simult.thy TF_Rep_defs "TCONS(M,N) ~= FCONS(K,L)";
 by (fast_tac TF_Rep_cs 1);
-val TCONS_not_FCONS = result();
+qed "TCONS_not_FCONS";
 val FCONS_not_TCONS = standard (TCONS_not_FCONS RS not_sym);
 
 val TCONS_neq_FCONS = standard (TCONS_not_FCONS RS notE);
@@ -206,12 +206,12 @@
 
 goalw Simult.thy [Tcons_def] "(Tcons(x,xs)=Tcons(y,ys)) = (x=y & xs=ys)";
 by (fast_tac TF_cs 1);
-val Tcons_Tcons_eq = result();
+qed "Tcons_Tcons_eq";
 val Tcons_inject = standard (Tcons_Tcons_eq RS iffD1 RS conjE);
 
 goalw Simult.thy [Fcons_def,Fnil_def] "Fcons(x,xs) ~= Fnil";
 by (fast_tac TF_cs 1);
-val Fcons_not_Fnil = result();
+qed "Fcons_not_Fnil";
 
 val Fcons_neq_Fnil = standard (Fcons_not_Fnil RS notE);;
 val Fnil_neq_Fcons = sym RS Fcons_neq_Fnil;
@@ -221,7 +221,7 @@
 
 goalw Simult.thy [Fcons_def] "(Fcons(x,xs)=Fcons(y,ys)) = (x=y & xs=ys)";
 by (fast_tac TF_cs 1);
-val Fcons_Fcons_eq = result();
+qed "Fcons_Fcons_eq";
 val Fcons_inject = standard (Fcons_Fcons_eq RS iffD1 RS conjE);
 
 
@@ -238,12 +238,12 @@
 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);
-val TF_rec_TCONS = result();
+qed "TF_rec_TCONS";
 
 goalw Simult.thy [FNIL_def] "TF_rec(FNIL,b,c,d) = c";
 by (rtac (TF_rec_unfold RS trans) 1);
 by (simp_tac (HOL_ss addsimps [Case_In1, List_case_NIL]) 1);
-val TF_rec_FNIL = result();
+qed "TF_rec_FNIL";
 
 goalw Simult.thy [FCONS_def]
  "!!M N. [| M: sexp;  N: sexp |] ==> 	\
@@ -251,7 +251,7 @@
 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);
-val TF_rec_FCONS = result();
+qed "TF_rec_FCONS";
 
 
 (*** tree_rec, forest_rec -- by TF_rec ***)
@@ -274,14 +274,14 @@
 goalw Simult.thy [tree_rec_def, forest_rec_def, Tcons_def]
     "tree_rec(Tcons(a,tf),b,c,d) = b(a,tf,forest_rec(tf,b,c,d))";
 by (simp_tac tf_rec_ss 1);
-val tree_rec_Tcons = result();
+qed "tree_rec_Tcons";
 
 goalw Simult.thy [forest_rec_def, Fnil_def] "forest_rec(Fnil,b,c,d) = c";
 by (simp_tac tf_rec_ss 1);
-val forest_rec_Fnil = result();
+qed "forest_rec_Fnil";
 
 goalw Simult.thy [tree_rec_def, forest_rec_def, Fcons_def]
     "forest_rec(Fcons(t,tf),b,c,d) = \
 \    d(t,tf,tree_rec(t,b,c,d), forest_rec(tf,b,c,d))";
 by (simp_tac tf_rec_ss 1);
-val forest_rec_Cons = result();
+qed "forest_rec_Cons";