more tidying
authorpaulson
Fri Jun 30 12:49:11 2000 +0200 (2000-06-30)
changeset 92108a080ade1a8c
parent 9209 862c8b83ab55
child 9211 6236c5285bd8
more tidying
src/ZF/ex/Limit.ML
     1.1 --- a/src/ZF/ex/Limit.ML	Fri Jun 30 12:31:57 2000 +0200
     1.2 +++ b/src/ZF/ex/Limit.ML	Fri Jun 30 12:49:11 2000 +0200
     1.3 @@ -55,14 +55,12 @@
     1.4  \                rel(D,x,z);  \
     1.5  \       !!x y. [| rel(D,x,y); rel(D,y,x); x:set(D); y:set(D)|] ==> x=y |] ==> \
     1.6  \    po(D)";
     1.7 -by Safe_tac;
     1.8 -by (REPEAT (ares_tac prems 1));
     1.9 +by (blast_tac (claset() addIs prems) 1);
    1.10  qed "poI";
    1.11  
    1.12  val prems = Goalw [cpo_def]
    1.13      "[| po(D); !!X. chain(D,X) ==> islub(D,X,x(D,X))|] ==> cpo(D)";
    1.14 -by (safe_tac (claset() addSIs [exI]));
    1.15 -by (REPEAT (ares_tac prems 1));
    1.16 +by (blast_tac (claset() addIs prems) 1);
    1.17  qed "cpoI";
    1.18  
    1.19  Goalw [cpo_def] "cpo(D) ==> po(D)";
    1.20 @@ -114,19 +112,17 @@
    1.21  
    1.22  val prems = Goalw [islub_def]  (* islubI *)
    1.23      "[|isub(D,X,x); !!y. isub(D,X,y) ==> rel(D,x,y)|] ==> islub(D,X,x)";
    1.24 -by Safe_tac;
    1.25 -by (REPEAT(ares_tac prems 1));
    1.26 +by (blast_tac (claset() addIs prems) 1);
    1.27  qed "islubI";
    1.28  
    1.29  val prems = Goalw [isub_def]  (* isubI *)
    1.30      "[|x:set(D);  !!n. n:nat ==> rel(D,X`n,x)|] ==> isub(D,X,x)";
    1.31 -by Safe_tac;
    1.32 -by (REPEAT(ares_tac prems 1));
    1.33 +by (blast_tac (claset() addIs prems) 1);
    1.34  qed "isubI";
    1.35  
    1.36  val prems = Goalw [isub_def]  (* isubE *)
    1.37      "[|isub(D,X,x); [|x:set(D);  !!n. n:nat==>rel(D,X`n,x)|] ==> P \
    1.38 -\         |] ==> P";
    1.39 +\    |] ==> P";
    1.40  by (asm_simp_tac (simpset() addsimps prems) 1);
    1.41  qed "isubE";
    1.42  
    1.43 @@ -140,7 +136,7 @@
    1.44  
    1.45  Goal "[|islub(D,X,x); islub(D,X,y); cpo(D)|] ==> x = y";
    1.46  by (blast_tac (claset() addIs [cpo_antisym,islub_least,
    1.47 -			       islub_isub,islub_in]) 1);
    1.48 +                               islub_isub,islub_in]) 1);
    1.49  qed "islub_unique";
    1.50  
    1.51  (*----------------------------------------------------------------------*)
    1.52 @@ -155,9 +151,10 @@
    1.53  (* Theorems about chains.                                               *)
    1.54  (*----------------------------------------------------------------------*)
    1.55  
    1.56 -val chainI = prove_goalw Limit.thy [chain_def]
    1.57 - "!!z.[|X:nat->set(D);  !!n. n:nat ==> rel(D,X`n,X`succ(n))|] ==> chain(D,X)"
    1.58 - (fn prems => [Asm_simp_tac 1]);
    1.59 +val prems = Goalw [chain_def]
    1.60 + "[|X:nat->set(D);  !!n. n:nat ==> rel(D,X`n,X`succ(n))|] ==> chain(D,X)";
    1.61 +by (blast_tac (claset() addIs prems) 1);
    1.62 +qed "chainI";
    1.63  
    1.64  Goalw [chain_def] "chain(D,X) ==> X : nat -> set(D)";
    1.65  by (Asm_simp_tac 1);
    1.66 @@ -176,21 +173,14 @@
    1.67  
    1.68  Goal "[|chain(D,X); cpo(D); n:nat; m:nat|] ==> rel(D,X`n,(X`(m #+ n)))";
    1.69  by (induct_tac "m" 1);
    1.70 -by (ALLGOALS Simp_tac);
    1.71 -by (rtac cpo_trans 1);
    1.72 -by Auto_tac;
    1.73 +by (auto_tac (claset() addIs [cpo_trans], simpset()));  
    1.74  qed "chain_rel_gen_add";
    1.75  
    1.76  Goal  (* chain_rel_gen *)
    1.77      "[|n le m; chain(D,X); cpo(D); n:nat; m:nat|] ==> rel(D,X`n,X`m)";
    1.78 -by (rtac impE 1);  (* The first three steps prepare for the induction proof *)
    1.79 -by (assume_tac 3);
    1.80 -by (assume_tac 2);
    1.81 +by (etac rev_mp 1);  (*prepare the induction*)
    1.82  by (induct_tac "m" 1);
    1.83 -by Safe_tac;
    1.84 -by (Asm_full_simp_tac 1);
    1.85 -by (rtac cpo_trans 2);
    1.86 -by (auto_tac (claset(),
    1.87 +by (auto_tac (claset() addIs [cpo_trans],
    1.88  	      simpset() addsimps [le_iff]));
    1.89  qed "chain_rel_gen";
    1.90  
    1.91 @@ -226,8 +216,8 @@
    1.92  
    1.93  val prems = goal Limit.thy  (* bot_unique *)
    1.94      "[| pcpo(D); x:set(D); !!y. y:set(D) ==> rel(D,x,y)|] ==> x = bot(D)";
    1.95 -by (rtac cpo_antisym 1);
    1.96 -brr(pcpo_cpo::bot_in::bot_least::prems) 1;
    1.97 +by (blast_tac (claset() addIs ([cpo_antisym,pcpo_cpo,bot_in,bot_least]@
    1.98 +                               prems)) 1);
    1.99  qed "bot_unique";
   1.100  
   1.101  (*----------------------------------------------------------------------*)
   1.102 @@ -255,12 +245,7 @@
   1.103  
   1.104  Goalw [isub_def,suffix_def]  (* isub_suffix *)
   1.105      "[|chain(D,X); cpo(D); n:nat|] ==> isub(D,suffix(X,n),x) <-> isub(D,X,x)";
   1.106 -by (Asm_simp_tac 1);
   1.107 -by Safe_tac;
   1.108 -by (blast_tac (claset() addIs [chain_in, add_type]) 2);
   1.109 -by (rtac cpo_trans 1);
   1.110 -by (rtac chain_rel_gen_add 2);
   1.111 -by Auto_tac;
   1.112 +by (auto_tac (claset() addIs [cpo_trans, chain_rel_gen_add], simpset()));
   1.113  qed "isub_suffix";
   1.114  
   1.115  Goalw [islub_def]  (* islub_suffix *)
   1.116 @@ -277,53 +262,28 @@
   1.117  (* Dominate and subchain.                                               *) 
   1.118  (*----------------------------------------------------------------------*)
   1.119  
   1.120 -val dominateI = prove_goalw Limit.thy [dominate_def]
   1.121 +val prems = Goalw [dominate_def]
   1.122    "[| !!m. m:nat ==> n(m):nat; !!m. m:nat ==> rel(D,X`m,Y`n(m))|] ==>   \
   1.123 -\  dominate(D,X,Y)"
   1.124 -  (fn prems => [rtac ballI 1,rtac bexI 1,REPEAT(ares_tac prems 1)]);
   1.125 +\  dominate(D,X,Y)";
   1.126 +by (blast_tac (claset() addIs prems) 1);
   1.127 +qed "dominateI"; 
   1.128  
   1.129 -val [dom,isub,cpo,X,Y] = goal Limit.thy
   1.130 +Goalw [isub_def, dominate_def]
   1.131    "[|dominate(D,X,Y); isub(D,Y,x); cpo(D);  \
   1.132  \    X:nat->set(D); Y:nat->set(D)|] ==> isub(D,X,x)";
   1.133 -by (rewtac isub_def);
   1.134 -by (rtac conjI 1);
   1.135 -by (rtac (rewrite_rule[isub_def]isub RS conjunct1) 1);
   1.136 -by (rtac ballI 1);
   1.137 -by (rtac (rewrite_rule[dominate_def]dom RS bspec RS bexE) 1);
   1.138 -by (assume_tac 1);
   1.139 -by (rtac cpo_trans 1);
   1.140 -by (rtac cpo 1);
   1.141 -by (assume_tac 1);
   1.142 -by (rtac (rewrite_rule[isub_def]isub RS conjunct2 RS bspec) 1);
   1.143 -by (assume_tac 1);
   1.144 -by (etac (X RS apply_type) 1);
   1.145 -by (etac (Y RS apply_type) 1);
   1.146 -by (rtac (rewrite_rule[isub_def]isub RS conjunct1) 1);
   1.147 +by Auto_tac;  
   1.148 +by (blast_tac (claset() addIs [cpo_trans] addDs [apply_type]) 1);
   1.149  qed "dominate_isub";
   1.150  
   1.151 -val [dom,Xlub,Ylub,cpo,X,Y] = goal Limit.thy
   1.152 +Goalw [islub_def]
   1.153    "[|dominate(D,X,Y); islub(D,X,x); islub(D,Y,y); cpo(D);  \
   1.154  \    X:nat->set(D); Y:nat->set(D)|] ==> rel(D,x,y)";
   1.155 -val Xub = rewrite_rule[islub_def]Xlub RS conjunct1;
   1.156 -val Yub = rewrite_rule[islub_def]Ylub RS conjunct1;
   1.157 -val Xub_y = Yub RS (dom RS dominate_isub);
   1.158 -val lem = Xub_y RS (rewrite_rule[islub_def]Xlub RS conjunct2 RS spec RS mp);
   1.159 -by (rtac (Y RS (X RS (cpo RS lem))) 1);
   1.160 +by (blast_tac (claset() addIs [dominate_isub]) 1);
   1.161  qed "dominate_islub";
   1.162  
   1.163 -val prems = Goalw [subchain_def]  (* subchainE *)
   1.164 -    "[|subchain(X,Y); n:nat;  !!m. [|m:nat; X`n = Y`(n #+ m)|] ==> Q|] ==> Q";
   1.165 -by (rtac (hd prems RS bspec RS bexE) 1);
   1.166 -by (resolve_tac prems 2);
   1.167 -by (assume_tac 3);
   1.168 -by (REPEAT(ares_tac prems 1));
   1.169 -qed "subchainE";
   1.170 -
   1.171 -Goal "[|subchain(Y,X); isub(D,X,x)|] ==> isub(D,Y,x)";
   1.172 -by (rtac isubI 1);
   1.173 -by (safe_tac (claset() addSEs [isubE, subchainE]));
   1.174 -by (assume_tac 1);
   1.175 -by (Asm_simp_tac 1);
   1.176 +Goalw [isub_def, subchain_def]
   1.177 +     "[|subchain(Y,X); isub(D,X,x)|] ==> isub(D,Y,x)";
   1.178 +by Auto_tac;  
   1.179  qed "subchain_isub";
   1.180  
   1.181  Goal "[|dominate(D,X,Y); subchain(Y,X); islub(D,X,x); islub(D,Y,y); cpo(D);  \
   1.182 @@ -346,8 +306,7 @@
   1.183  qed "matrix_in_fun";
   1.184  
   1.185  Goal "[|matrix(D,M); n:nat; m:nat|] ==> M`n`m : set(D)";
   1.186 -by (rtac apply_type 1);
   1.187 -by (REPEAT(ares_tac[matrix_in_fun] 1));
   1.188 +by (blast_tac (claset() addIs [apply_funtype, matrix_in_fun]) 1);
   1.189  qed "matrix_in";
   1.190  
   1.191  Goalw [matrix_def]  (* matrix_rel_1_0 *)
   1.192 @@ -376,23 +335,14 @@
   1.193  
   1.194  Goalw [chain_def]  (* matrix_chain_diag *)
   1.195      "matrix(D,M) ==> chain(D,lam n:nat. M`n`n)";
   1.196 -by Safe_tac;
   1.197 -by (rtac lam_type 1);
   1.198 -by (rtac matrix_in 1);
   1.199 -by (REPEAT(ares_tac prems 1));
   1.200 -by (Asm_simp_tac 1);
   1.201 -by (rtac matrix_rel_1_1 1);
   1.202 -by (REPEAT(ares_tac prems 1));
   1.203 +by (auto_tac (claset() addIs [lam_type, matrix_in, matrix_rel_1_1], 
   1.204 +              simpset()));
   1.205  qed "matrix_chain_diag";
   1.206  
   1.207  Goalw [chain_def]  (* matrix_chain_left *)
   1.208      "[|matrix(D,M); n:nat|] ==> chain(D,M`n)";
   1.209 -by Safe_tac;
   1.210 -by (rtac apply_type 1);
   1.211 -by (rtac matrix_fun 1);
   1.212 -by (REPEAT(ares_tac prems 1));
   1.213 -by (rtac matrix_rel_0_1 1);
   1.214 -by (REPEAT(ares_tac prems 1));
   1.215 +by (auto_tac (claset() addIs [matrix_fun RS apply_type, matrix_in, 
   1.216 +                              matrix_rel_0_1],   simpset()));
   1.217  qed "matrix_chain_left";
   1.218  
   1.219  Goalw [chain_def]  (* matrix_chain_right *)
   1.220 @@ -487,35 +437,33 @@
   1.221  by (rewtac dominate_def);
   1.222  by (rtac ballI 1);
   1.223  by (rtac bexI 1);
   1.224 -by (assume_tac 2);
   1.225 -by (Asm_simp_tac 1);
   1.226 +by Auto_tac;  
   1.227  by (asm_simp_tac (simpset() addsimps 
   1.228  		  [matrix_chain_left RS chain_fun RS eta]) 1);
   1.229  by (rtac islub_ub 1);
   1.230  by (rtac cpo_lub 1);
   1.231 -by (REPEAT(ares_tac 
   1.232 -[matrix_chain_left,matrix_chain_diag,chain_fun,matrix_chain_lub] 1));
   1.233 -by (rtac isub_lemma 1);
   1.234 -by (REPEAT(assume_tac 1));
   1.235 +by (REPEAT(ares_tac [matrix_chain_left,matrix_chain_diag,chain_fun,
   1.236 +                     matrix_chain_lub, isub_lemma] 1));
   1.237  qed "isub_eq";
   1.238  
   1.239 -val lemma1 = prove_goalw Limit.thy [lub_def]  
   1.240 +Goalw [lub_def]  
   1.241      "lub(D,(lam n:nat. lub(D,lam m:nat. M`n`m))) =   \
   1.242 -\    (THE x. islub(D, (lam n:nat. lub(D,lam m:nat. M`n`m)), x))"
   1.243 - (fn _ => [Fast_tac 1]);
   1.244 +\    (THE x. islub(D, (lam n:nat. lub(D,lam m:nat. M`n`m)), x))";
   1.245 +by (Blast_tac 1);
   1.246 +qed "lemma1";
   1.247  
   1.248 -val lemma2 = prove_goalw Limit.thy [lub_def]  
   1.249 +Goalw [lub_def]  
   1.250      "lub(D,(lam n:nat. M`n`n)) =   \
   1.251 -\    (THE x. islub(D, (lam n:nat. M`n`n), x))"
   1.252 - (fn _ => [Fast_tac 1]);
   1.253 +\    (THE x. islub(D, (lam n:nat. M`n`n), x))";
   1.254 +by (Blast_tac 1);
   1.255 +qed "lemma2";
   1.256  
   1.257  Goal  (* lub_matrix_diag *)
   1.258      "[|matrix(D,M); cpo(D)|] ==>  \
   1.259  \    lub(D,(lam n:nat. lub(D,lam m:nat. M`n`m))) =  \
   1.260  \    lub(D,(lam n:nat. M`n`n))";
   1.261  by (simp_tac (simpset() addsimps [lemma1,lemma2]) 1);
   1.262 -by (rewtac islub_def);
   1.263 -by (asm_simp_tac (simpset() addsimps [isub_eq]) 1);
   1.264 +by (asm_simp_tac (simpset() addsimps [islub_def, isub_eq]) 1);
   1.265  qed "lub_matrix_diag";
   1.266  
   1.267  Goal  (* lub_matrix_diag_sym *)
   1.268 @@ -618,10 +566,7 @@
   1.269  val prems = goal Limit.thy
   1.270      "[|!!x. x:set(D) ==> rel(E,f`x,g`x); f:cont(D,E); g:cont(D,E)|] ==> \
   1.271  \    rel(cf(D,E),f,g)";
   1.272 -by (rtac rel_I 1);
   1.273 -by (simp_tac (simpset() addsimps [cf_def]) 1);
   1.274 -by Safe_tac;
   1.275 -by (REPEAT (ares_tac prems 1));
   1.276 +by (asm_simp_tac (simpset() addsimps [rel_I, cf_def]@prems) 1);
   1.277  qed "rel_cfI";
   1.278  
   1.279  Goalw [rel_def,cf_def] "[|rel(cf(D,E),f,g); x:set(D)|] ==> rel(E,f`x,g`x)";
   1.280 @@ -635,47 +580,31 @@
   1.281  Goal  (* chain_cf *)
   1.282      "[| chain(cf(D,E),X); x:set(D)|] ==> chain(E,lam n:nat. X`n`x)";
   1.283  by (rtac chainI 1);
   1.284 -by (rtac lam_type 1);
   1.285 -by (rtac apply_type 1);
   1.286 -by (assume_tac 2);
   1.287 -by (REPEAT(ares_tac[cont_fun,cf_cont,chain_in] 1));
   1.288 +by (blast_tac (claset() addIs [lam_type, apply_funtype, cont_fun,
   1.289 +                               cf_cont,chain_in]) 1);
   1.290  by (Asm_simp_tac 1);
   1.291 -by (REPEAT(ares_tac[rel_cf,chain_rel] 1));
   1.292 +by (blast_tac (claset() addIs [rel_cf,chain_rel]) 1);
   1.293  qed "chain_cf";
   1.294  
   1.295  Goal  (* matrix_lemma *)
   1.296      "[|chain(cf(D,E),X); chain(D,Xa); cpo(D); cpo(E) |] ==>   \
   1.297  \    matrix(E,lam x:nat. lam xa:nat. X`x`(Xa`xa))";
   1.298  by (rtac matrix_chainI 1);
   1.299 -by (Asm_simp_tac 1);
   1.300 -by (Asm_simp_tac 2);
   1.301 +by Auto_tac;  
   1.302  by (rtac chainI 1);
   1.303 -by (rtac lam_type 1);
   1.304 -by (rtac apply_type 1);
   1.305 -by (rtac (chain_in RS cf_cont RS cont_fun) 1);
   1.306 -by (REPEAT(assume_tac 1));
   1.307 -by (rtac chain_in 1);
   1.308 -by (REPEAT(assume_tac 1));
   1.309 +by (blast_tac (claset() addIs [lam_type, apply_funtype, cont_fun,
   1.310 +                               cf_cont,chain_in]) 1);
   1.311  by (Asm_simp_tac 1);
   1.312 -by (rtac cont_mono 1);
   1.313 -by (rtac (chain_in RS cf_cont) 1);
   1.314 -by (REPEAT (assume_tac 1));
   1.315 -brr [chain_rel,chain_in,nat_succI] 1;
   1.316 +by (blast_tac (claset() addIs [cont_mono, nat_succI, chain_rel,
   1.317 +                               cf_cont,chain_in]) 1);
   1.318  by (rtac chainI 1);
   1.319 -by (rtac lam_type 1);
   1.320 -by (rtac apply_type 1);
   1.321 -by (rtac (chain_in RS cf_cont RS cont_fun) 1);
   1.322 -by (REPEAT(assume_tac 1));
   1.323 -by (rtac chain_in 1);
   1.324 -by (REPEAT(assume_tac 1));
   1.325 +by (blast_tac (claset() addIs [lam_type, apply_funtype, cont_fun,
   1.326 +                               cf_cont,chain_in]) 1);
   1.327  by (Asm_simp_tac 1);
   1.328  by (rtac rel_cf 1);
   1.329  brr [chain_in,chain_rel] 1;
   1.330 -by (rtac lam_type 1);
   1.331 -by (rtac lam_type 1);
   1.332 -by (rtac apply_type 1);
   1.333 -by (rtac (chain_in RS cf_cont RS cont_fun) 1);
   1.334 -by Auto_tac;
   1.335 +by (blast_tac (claset() addIs [lam_type, apply_funtype, cont_fun,
   1.336 +                               cf_cont,chain_in]) 1);
   1.337  qed "matrix_lemma";
   1.338  
   1.339  Goal  (* chain_cf_lub_cont *)
   1.340 @@ -697,8 +626,7 @@
   1.341  by (asm_simp_tac(simpset() addsimps[chain_in RS cf_cont RS cont_lub]) 1);
   1.342  by (forward_tac[matrix_lemma RS lub_matrix_diag]1);
   1.343  by (REPEAT (assume_tac 1));
   1.344 -by (Asm_full_simp_tac 1);
   1.345 -by (asm_simp_tac(simpset() addsimps[chain_in RS beta]) 1);
   1.346 +by (asm_full_simp_tac(simpset() addsimps[chain_in RS beta]) 1);
   1.347  by (dtac (matrix_lemma RS lub_matrix_diag_sym) 1);
   1.348  by Auto_tac;
   1.349  qed "chain_cf_lub_cont";
   1.350 @@ -774,8 +702,8 @@
   1.351  
   1.352  Goal  (* bot_cf *)
   1.353      "[|cpo(D); pcpo(E)|] ==> bot(cf(D,E)) = (lam x:set(D).bot(E))";
   1.354 -by (rtac (bot_unique RS sym) 1);
   1.355 -brr[pcpo_cf, cf_least, bot_in RS const_cont RS cont_cf, cf_cont, pcpo_cpo] 1;
   1.356 +by (blast_tac (claset() addIs [bot_unique RS sym, pcpo_cf, cf_least, 
   1.357 +                   bot_in RS const_cont RS cont_cf, cf_cont, pcpo_cpo])1);
   1.358  qed "bot_cf";
   1.359  
   1.360  (*----------------------------------------------------------------------*)
   1.361 @@ -873,34 +801,20 @@
   1.362  by (Fast_tac 1);
   1.363  qed "projpairI";
   1.364  
   1.365 -val prems = Goalw [projpair_def]  (* projpairE *)
   1.366 -    "[| projpair(D,E,e,p);   \
   1.367 -\       [| e:cont(D,E); p:cont(E,D); p O e = id(set(D));   \
   1.368 -\          rel(cf(E,E))(e O p)(id(set(E)))|] ==> Q |] ==> Q";
   1.369 -by (rtac (hd(tl prems)) 1);
   1.370 -by (REPEAT(asm_simp_tac(simpset() addsimps[hd prems]) 1));
   1.371 -qed "projpairE";
   1.372 -
   1.373 -Goal "projpair(D,E,e,p) ==> e:cont(D,E)";
   1.374 -by (etac projpairE 1);
   1.375 -by (assume_tac 1);
   1.376 +Goalw [projpair_def] "projpair(D,E,e,p) ==> e:cont(D,E)";
   1.377 +by Auto_tac;  
   1.378  qed "projpair_e_cont";
   1.379  
   1.380 -Goal  (* projpair_p_cont *)
   1.381 -    "projpair(D,E,e,p) ==> p:cont(E,D)";
   1.382 -by (etac projpairE 1);
   1.383 -by (assume_tac 1);
   1.384 +Goalw [projpair_def] "projpair(D,E,e,p) ==> p:cont(E,D)";
   1.385 +by Auto_tac;  
   1.386  qed "projpair_p_cont";
   1.387  
   1.388 -Goal "projpair(D,E,e,p) ==> p O e = id(set(D))";
   1.389 -by (etac projpairE 1);
   1.390 -by (assume_tac 1);
   1.391 +Goalw [projpair_def] "projpair(D,E,e,p) ==> p O e = id(set(D))";
   1.392 +by Auto_tac;  
   1.393  qed "projpair_eq";
   1.394  
   1.395 -Goal  (* projpair_rel *)
   1.396 -    "projpair(D,E,e,p) ==> rel(cf(E,E))(e O p)(id(set(E)))";
   1.397 -by (etac projpairE 1);
   1.398 -by (assume_tac 1);
   1.399 +Goalw [projpair_def] "projpair(D,E,e,p) ==> rel(cf(E,E))(e O p)(id(set(E)))";
   1.400 +by Auto_tac;  
   1.401  qed "projpair_rel";
   1.402  
   1.403  val projpairDs = [projpair_e_cont,projpair_p_cont,projpair_eq,projpair_rel];
   1.404 @@ -998,17 +912,17 @@
   1.405  by (blast_tac (claset() addIs [projpair_unique RS iffD1]) 1);
   1.406  qed "embRp";
   1.407  
   1.408 -val embI = prove_goalw Limit.thy [emb_def]
   1.409 -    "!!x. projpair(D,E,e,p) ==> emb(D,E,e)"
   1.410 -  (fn prems => [Fast_tac 1]);
   1.411 +Goalw [emb_def] "projpair(D,E,e,p) ==> emb(D,E,e)";
   1.412 +by Auto_tac;  
   1.413 +qed "embI";
   1.414  
   1.415  Goal "[|projpair(D,E,e,p); cpo(D); cpo(E)|] ==> Rp(D,E,e) = p";
   1.416  by (blast_tac (claset() addIs [embRp, embI, projpair_unique RS iffD1]) 1);
   1.417  qed "Rp_unique";
   1.418  
   1.419 -val emb_cont = prove_goalw Limit.thy [emb_def]
   1.420 -    "emb(D,E,e) ==> e:cont(D,E)"
   1.421 -  (fn prems => [rtac(hd prems RS exE) 1,rtac projpair_e_cont 1,atac 1]);
   1.422 +Goalw [emb_def] "emb(D,E,e) ==> e:cont(D,E)";
   1.423 +by (blast_tac (claset() addIs [projpair_e_cont]) 1);
   1.424 +qed "emb_cont";
   1.425  
   1.426  (* The following three theorems have cpo asms due to THE (uniqueness). *)
   1.427  
   1.428 @@ -1018,16 +932,12 @@
   1.429  
   1.430  AddTCs [emb_cont, Rp_cont];
   1.431  
   1.432 -val id_apply = prove_goalw Perm.thy [id_def]
   1.433 -    "!!z. x:A ==> id(A)`x = x"
   1.434 -  (fn prems => [Asm_simp_tac 1]);
   1.435 -
   1.436  Goal  (* embRp_eq_thm *)
   1.437      "[|emb(D,E,e); x:set(D); cpo(D); cpo(E)|] ==> Rp(D,E,e)`(e`x) = x";
   1.438  by (rtac (comp_fun_apply RS subst) 1);
   1.439  brr[Rp_cont,emb_cont,cont_fun] 1;
   1.440  by (stac embRp_eq 1);
   1.441 -by (auto_tac (claset() addIs [id_apply], simpset()));
   1.442 +by (auto_tac (claset() addIs [id_conv], simpset()));
   1.443  qed "embRp_eq_thm";
   1.444  
   1.445  
   1.446 @@ -1206,9 +1116,9 @@
   1.447  brr(prems@[subsetD]) 1;
   1.448  qed "subcpoI";
   1.449  
   1.450 -val subcpo_subset = prove_goalw Limit.thy [subcpo_def]  
   1.451 -    "!!x. subcpo(D,E) ==> set(D)<=set(E)"
   1.452 -  (fn prems => [Fast_tac 1]);
   1.453 +Goalw [subcpo_def] "subcpo(D,E) ==> set(D)<=set(E)";
   1.454 +by Auto_tac;  
   1.455 +qed "subcpo_subset";
   1.456  
   1.457  Goalw [subcpo_def]  
   1.458      "[|subcpo(D,E); x:set(D); y:set(D)|] ==> rel(D,x,y)<->rel(E,x,y)";
   1.459 @@ -1307,28 +1217,17 @@
   1.460  by (Asm_full_simp_tac 1);
   1.461  qed "rel_mkcpoE";
   1.462  
   1.463 -val rel_mkcpo = prove_goalw Limit.thy [mkcpo_def,rel_def,set_def]
   1.464 -    "!!z. [|x:set(D); y:set(D)|] ==> rel(mkcpo(D,P),x,y) <-> rel(D,x,y)"
   1.465 - (fn prems => [Asm_simp_tac 1]);
   1.466 -
   1.467 -(* The HOL proof is simpler, problems due to cpos as purely in upair. *)
   1.468 -(* And chains as set functions. *)
   1.469 +Goalw [mkcpo_def,rel_def,set_def]
   1.470 +    "[|x:set(D); y:set(D)|] ==> rel(mkcpo(D,P),x,y) <-> rel(D,x,y)";
   1.471 +by Auto_tac;  
   1.472 +qed "rel_mkcpo";
   1.473  
   1.474  Goal  (* chain_mkcpo *)
   1.475      "chain(mkcpo(D,P),X) ==> chain(D,X)";
   1.476  by (rtac chainI 1);
   1.477 -(*---begin additional---*)
   1.478 -by (rtac Pi_type 1);
   1.479 -brr[chain_fun] 1;
   1.480 -brr[chain_in RS mkcpoD1] 1;
   1.481 -(*---end additional---*)
   1.482 -by (rtac (rel_mkcpo RS iffD1) 1);
   1.483 -(*---begin additional---*)
   1.484 -by (rtac mkcpoD1 1); 
   1.485 -by (rtac mkcpoD1 2); 
   1.486 -brr[chain_in,nat_succI] 1; 
   1.487 -(*---end additional---*)
   1.488 -by (auto_tac (claset() addIs [chain_rel], simpset()));
   1.489 +by (blast_tac (claset() addIs [Pi_type, chain_fun, chain_in RS mkcpoD1]) 1);
   1.490 +by (blast_tac (claset() addIs [rel_mkcpo RS iffD1, chain_rel, mkcpoD1, 
   1.491 +                               chain_in,nat_succI]) 1);
   1.492  qed "chain_mkcpo";
   1.493  
   1.494  val prems = goal Limit.thy  (* subcpo_mkcpo *)
   1.495 @@ -1969,7 +1868,7 @@
   1.496  brr[emb_chain_emb, e_less_cont RS cont_fun RS apply_type, emb_chain_cpo, nat_succI] 1;
   1.497  by (asm_simp_tac(simpset() addsimps[eps_e_less]) 1);
   1.498  by (dtac asm_rl 1);
   1.499 -by (asm_full_simp_tac(simpset() addsimps[eps_succ_Rp, e_less_eq, id_apply, nat_succI]) 1);
   1.500 +by (asm_full_simp_tac(simpset() addsimps[eps_succ_Rp, e_less_eq, id_conv, nat_succI]) 1);
   1.501  qed "rho_emb_fun";
   1.502  
   1.503  val rho_emb_apply1 = prove_goalw Limit.thy [rho_emb_def]