# HG changeset patch
# User paulson
# Date 917861351 -3600
# Node ID f3f2560fbed94f550721dc7ae714723b363c0973
# Parent  9d5b74068bf96c6673891ee87822c9ecc217ffd4
a bit of tidying

diff -r 9d5b74068bf9 -r f3f2560fbed9 src/ZF/ex/Limit.ML
--- a/src/ZF/ex/Limit.ML	Sat Jan 30 10:42:40 1999 +0100
+++ b/src/ZF/ex/Limit.ML	Mon Feb 01 10:29:11 1999 +0100
@@ -172,7 +172,7 @@
 qed "chain_rel";
 
 Addsimps [chain_in, chain_rel];
-AddTCs   [chain_in, chain_rel];
+AddTCs   [chain_fun, chain_in, chain_rel];
 
 Goal "[|chain(D,X); cpo(D); n:nat; m:nat|] ==> rel(D,X`n,(X`(m #+ n)))";
 by (induct_tac "m" 1);
@@ -401,17 +401,17 @@
 	      simpset()));
 qed "matrix_chain_right";
 
-val prems = Goalw [matrix_def]  (* matrix_chainI *)
+val xprem::yprem::prems = Goalw [matrix_def]  (* matrix_chainI *)
     "[|!!x. x:nat==>chain(D,M`x);  !!y. y:nat==>chain(D,lam x:nat. M`x`y);   \
 \      M:nat->nat->set(D); cpo(D)|] ==> matrix(D,M)";
-by (safe_tac (claset() addSIs [ballI]));
-by (cut_inst_tac[("y1","m"),("n","n")](hd(tl prems) RS chain_rel) 2);
+by Safe_tac;
+by (cut_inst_tac[("y1","m"),("n","n")] (yprem RS chain_rel) 2);
 by (Asm_full_simp_tac 4);
 by (rtac cpo_trans 5);
-by (cut_inst_tac[("y1","m"),("n","n")](hd(tl prems) RS chain_rel) 6);
+by (cut_inst_tac[("y1","m"),("n","n")] (yprem RS chain_rel) 6);
 by (Asm_full_simp_tac 8);
-by (TRYALL(rtac (chain_fun RS apply_type)));
-brr(chain_rel::nat_succI::prems) 1;
+by (typecheck_tac (tcset() addTCs (chain_fun RS apply_type)::
+		                  xprem::yprem::prems));
 qed "matrix_chainI";
 
 val lemma = prove_goal Limit.thy
@@ -562,8 +562,7 @@
 by (Blast_tac 1);
 qed "cont2mono";
 
-Goalw [cont_def]
-    "f:cont(D,E) ==> f:set(D)->set(E)";
+Goalw [cont_def] "f:cont(D,E) ==> f:set(D)->set(E)";
 by (rtac mono_fun 1);
 by (Blast_tac 1);
 qed "cont_fun";
@@ -572,6 +571,8 @@
 by (blast_tac(claset() addSIs [cont_fun RS apply_type]) 1);
 qed "cont_map";
 
+AddTCs [comp_fun, cont_fun, cont_map];
+
 Goalw [cont_def]
     "[|f:cont(D,E); rel(D,x,y); x:set(D); y:set(D)|] ==> rel(E,f`x,f`y)";
 by (blast_tac(claset() addSIs [mono_mono]) 1);
@@ -674,9 +675,7 @@
 by (rtac lam_type 1);
 by (rtac apply_type 1);
 by (rtac (chain_in RS cf_cont RS cont_fun) 1);
-by (REPEAT (assume_tac 1));
-by (rtac chain_in 1);
-by (REPEAT (assume_tac 1));
+by Auto_tac;
 qed "matrix_lemma";
 
 Goal  (* chain_cf_lub_cont *)
@@ -701,8 +700,7 @@
 by (Asm_full_simp_tac 1);
 by (asm_simp_tac(simpset() addsimps[chain_in RS beta]) 1);
 by (dtac (matrix_lemma RS lub_matrix_diag_sym) 1);
-by (REPEAT (assume_tac 1));
-by (Asm_full_simp_tac 1);
+by Auto_tac;
 qed "chain_cf_lub_cont";
 
 Goal  (* islub_cf *)
@@ -765,7 +763,7 @@
 Goal "[|cpo(D); pcpo(E); y:cont(D,E)|]==>rel(cf(D,E),(lam x:set(D).bot(E)),y)";
 by (rtac rel_cfI 1);
 by (Asm_simp_tac 1);
-brr[bot_least, bot_in, apply_type, cont_fun, const_cont, cpo_cf, pcpo_cpo] 1;
+by (ALLGOALS (type_solver_tac (tcset() addTCs [cont_fun, const_cont]) []));
 qed "cf_least";
 
 Goal  (* pcpo_cf *)
@@ -784,15 +782,10 @@
 (* Identity and composition.                                            *)
 (*----------------------------------------------------------------------*)
 
-val id_thm = prove_goalw Perm.thy [id_def] "x:X ==> (id(X)`x) = x"
-  (fn prems => [simp_tac(simpset() addsimps prems) 1]);
-
 Goal  (* id_cont *)
     "cpo(D) ==> id(set(D)):cont(D,D)";
-by (rtac contI 1);
-by (rtac id_type 1);
-by (asm_simp_tac (simpset() addsimps[id_thm]) 1);
-by (asm_simp_tac(simpset() addsimps[id_thm, cpo_lub RS islub_in, chain_in, chain_fun RS eta]) 1);
+by (asm_simp_tac(simpset() addsimps[id_type, contI, cpo_lub RS islub_in, 
+				    chain_fun RS eta]) 1);
 qed "id_cont";
 
 AddTCs [id_cont];
@@ -806,7 +799,7 @@
 by (stac comp_cont_apply 5);
 by (rtac cont_mono 8);
 by (rtac cont_mono 9); (* 15 subgoals *)
-brr[comp_fun,cont_fun,cont_map] 1; (* proves all but the lub case *)
+by Typecheck_tac; (* proves all but the lub case *)
 by (stac comp_cont_apply 1);
 by (stac cont_lub 4);
 by (stac cont_lub 6);
@@ -1989,7 +1982,7 @@
 
 val rho_emb_id = prove_goal Limit.thy 
   "!!z. [| x:set(DD`n); n:nat|] ==> rho_emb(DD,ee,n)`x`n = x"
-  (fn prems => [asm_simp_tac(simpset() addsimps[rho_emb_apply2,eps_id,id_thm]) 1]);
+  (fn prems => [asm_simp_tac(simpset() addsimps[rho_emb_apply2,eps_id]) 1]);
 
 (* Shorter proof, 23 against 62. *)
 
@@ -2030,7 +2023,7 @@
 by (induct_tac "n" 1);
 by (rtac impI 1);
 by (asm_full_simp_tac (simpset() addsimps [e_less_eq]) 1);
-by (stac id_thm 1);
+by (stac id_conv 1);
 brr[apply_type,Dinf_prod,cpo_refl,emb_chain_cpo,nat_0I] 1;
 by (asm_full_simp_tac (simpset() addsimps [le_succ_iff]) 1);
 by (rtac impI 1);
@@ -2049,13 +2042,13 @@
   [("P",
     "%z. rel(DD ` succ(xa), \
 \    (ee ` xa O Rp(?DD46(xa) ` xa,?DD46(xa) ` succ(xa),?ee46(xa) ` xa)) ` \
-\            (x ` succ(xa)),z)")](id_thm RS subst) 6);
+\            (x ` succ(xa)),z)")](id_conv RS subst) 6);
 by (rtac rel_cf 7); 
 (* Dinf and cont_fun doesn't go well together, both Pi(_,%x._). *)
 (* brr solves 11 of 12 subgoals *)
 brr[Dinf_prod RS apply_type, cont_fun, Rp_cont, e_less_cont, emb_cont, emb_chain_emb, emb_chain_cpo, apply_type, embRp_rel, disjI1 RS (le_succ_iff RS iffD2), nat_succI] 1;
 by (asm_full_simp_tac (simpset() addsimps [e_less_eq]) 1);
-by (stac id_thm 1);
+by (stac id_conv 1);
 by (auto_tac (claset() addIs [apply_type,Dinf_prod,emb_chain_cpo], simpset()));
 val lemma1 = result();
 
@@ -2068,7 +2061,7 @@
 by (induct_tac "m" 1);
 by (rtac impI 1);
 by (asm_full_simp_tac (simpset() addsimps [e_gr_eq]) 1);
-by (stac id_thm 1);
+by (stac id_conv 1);
 brr[apply_type,Dinf_prod,cpo_refl,emb_chain_cpo,nat_0I] 1;
 by (asm_full_simp_tac (simpset() addsimps [le_succ_iff]) 1);
 by (rtac impI 1);
@@ -2079,7 +2072,7 @@
 by (stac Dinf_eq 7);
 brr[emb_chain_emb, emb_chain_cpo, Rp_cont, e_gr_cont, cont_fun, emb_cont, apply_type,Dinf_prod,nat_succI] 1;
 by (asm_full_simp_tac (simpset() addsimps [e_gr_eq]) 1);
-by (stac id_thm 1);
+by (stac id_conv 1);
 by (auto_tac (claset() addIs [apply_type,Dinf_prod,emb_chain_cpo], simpset()));
 val lemma2 = result();
 
@@ -2116,14 +2109,14 @@
 (*-----------------------------------------------*)
 (* This part is 7 lines, but 30 in HOL (75% reduction!) *)
 by (rtac fun_extension 1);
-by (stac id_thm 3);
+by (stac id_conv 3);
 by (stac comp_fun_apply 4);
 by (stac beta 7);
 by (stac rho_emb_id 8);
 brr[comp_fun, id_type, lam_type, rho_emb_fun, Dinf_prod RS apply_type, apply_type,refl] 1;
 (*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
 by (rtac rel_cfI 1); (* ------------------>>>Yields type cond, not in HOL *)
-by (stac id_thm 1);
+by (stac id_conv 1);
 by (stac comp_fun_apply 2);
 by (stac beta 5);
 by (stac rho_emb_apply1 6);
@@ -2268,8 +2261,7 @@
 by (Asm_simp_tac 1);
 brr[embRp_rel,emb_rho_emb,emb_chain_cpo,cpo_Dinf] 1;
 by (rtac rel_cfI 1);
-by (asm_simp_tac
-    (simpset() addsimps[id_thm,lub_cf,rho_emb_chain,cpo_Dinf]) 1);
+by (asm_simp_tac (simpset() addsimps[lub_cf,rho_emb_chain,cpo_Dinf]) 1);
 by (rtac rel_DinfI 1); (* Addtional assumptions *)
 by (stac lub_Dinf 1);
 brr[rho_emb_chain_apply1] 1;  
@@ -2424,7 +2416,7 @@
 by (fast_tac (claset() addIs [lam_type]) 1);
 by (asm_simp_tac 
      (simpset() setSolver type_solver_tac (tcset() addTCs [emb_cont, commute_emb])) 2);
-by (Asm_simp_tac 1);
+by (fast_tac (claset() addIs [lam_type]) 1);
 val lemma = result();
 
 Goal "[| commute(DD,ee,E,r); commute(DD,ee,G,f);   \