diff -r 3a8d722fd3ff -r 16c4ea954511 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";