src/HOL/ex/MT.ML
changeset 2935 998cb95fdd43
parent 1820 e381e1c51689
child 3842 b55686a7b22c
     1.1 --- a/src/HOL/ex/MT.ML	Fri Apr 11 11:33:51 1997 +0200
     1.2 +++ b/src/HOL/ex/MT.ML	Fri Apr 11 15:21:36 1997 +0200
     1.3 @@ -17,30 +17,11 @@
     1.4  
     1.5  open MT;
     1.6  
     1.7 -(*Limit cyclic unifications during monotonicity proofs*)
     1.8 -val orig_search_bound = !Unify.search_bound;
     1.9 -Unify.search_bound := 8;
    1.10 -
    1.11 -val prems = goal MT.thy "~a:{b} ==> ~a=b";
    1.12 -by (cut_facts_tac prems 1);
    1.13 -by (rtac notI 1);
    1.14 -by (dtac notE 1);
    1.15 -by (hyp_subst_tac 1);
    1.16 -by (rtac singletonI 1);
    1.17 -by (assume_tac 1);
    1.18 -qed "notsingletonI";
    1.19 -
    1.20  (* ############################################################ *)
    1.21  (* Inference systems                                            *)
    1.22  (* ############################################################ *)
    1.23  
    1.24 -val infsys_mono_tac =
    1.25 -  (rewtac subset_def) THEN (safe_tac (claset_of "HOL")) THEN (rtac ballI 1) THEN
    1.26 -  (rtac CollectI 1) THEN (dtac CollectD 1) THEN
    1.27 -  REPEAT 
    1.28 -    ( (TRY ((etac disjE 1) THEN (rtac disjI2 2) THEN (rtac disjI1 1))) THEN
    1.29 -      (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac ((claset_of "Fun")delrules [equalityI]) 1)
    1.30 -    );
    1.31 +val infsys_mono_tac = (REPEAT (ares_tac (basic_monos@[allI,impI]) 1));
    1.32  
    1.33  val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";
    1.34  by (simp_tac (!simpset addsimps prems) 1);
    1.35 @@ -102,7 +83,7 @@
    1.36  by (rtac (monoh RS monoD) 1);
    1.37  by (rtac (UnE RS subsetI) 1);
    1.38  by (assume_tac 1);
    1.39 -by (fast_tac (!claset addSIs [cih]) 1);
    1.40 +by (blast_tac (!claset addSIs [cih]) 1);
    1.41  by (rtac (monoh RS monoD RS subsetD) 1);
    1.42  by (rtac Un_upper2 1);
    1.43  by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
    1.44 @@ -169,7 +150,8 @@
    1.45  by (rtac lfp_intro2 1);
    1.46  by (rtac eval_fun_mono 1);
    1.47  by (rewtac eval_fun_def);
    1.48 -by (Fast_tac 1);
    1.49 +	(*Naughty!  But the quantifiers are nested VERY deeply...*)
    1.50 +by (blast_tac (!claset addSIs [exI]) 1);
    1.51  qed "eval_const";
    1.52  
    1.53  val prems = goalw MT.thy [eval_def, eval_rel_def] 
    1.54 @@ -178,7 +160,7 @@
    1.55  by (rtac lfp_intro2 1);
    1.56  by (rtac eval_fun_mono 1);
    1.57  by (rewtac eval_fun_def);
    1.58 -by (Fast_tac 1);
    1.59 +by (blast_tac (!claset addSIs [exI]) 1);
    1.60  qed "eval_var2";
    1.61  
    1.62  val prems = goalw MT.thy [eval_def, eval_rel_def] 
    1.63 @@ -187,7 +169,7 @@
    1.64  by (rtac lfp_intro2 1);
    1.65  by (rtac eval_fun_mono 1);
    1.66  by (rewtac eval_fun_def);
    1.67 -by (Fast_tac 1);
    1.68 +by (blast_tac (!claset addSIs [exI]) 1);
    1.69  qed "eval_fn";
    1.70  
    1.71  val prems = goalw MT.thy [eval_def, eval_rel_def] 
    1.72 @@ -197,7 +179,7 @@
    1.73  by (rtac lfp_intro2 1);
    1.74  by (rtac eval_fun_mono 1);
    1.75  by (rewtac eval_fun_def);
    1.76 -by (Fast_tac 1);
    1.77 +by (blast_tac (!claset addSIs [exI]) 1);
    1.78  qed "eval_fix";
    1.79  
    1.80  val prems = goalw MT.thy [eval_def, eval_rel_def]
    1.81 @@ -207,7 +189,7 @@
    1.82  by (rtac lfp_intro2 1);
    1.83  by (rtac eval_fun_mono 1);
    1.84  by (rewtac eval_fun_def);
    1.85 -by (Fast_tac 1);
    1.86 +by (blast_tac (!claset addSIs [exI]) 1);
    1.87  qed "eval_app1";
    1.88  
    1.89  val prems = goalw MT.thy [eval_def, eval_rel_def] 
    1.90 @@ -220,7 +202,7 @@
    1.91  by (rtac lfp_intro2 1);
    1.92  by (rtac eval_fun_mono 1);
    1.93  by (rewtac eval_fun_def);
    1.94 -by (fast_tac (!claset addSIs [disjI2]) 1);
    1.95 +by (blast_tac (!claset addSIs [disjI2]) 1);
    1.96  qed "eval_app2";
    1.97  
    1.98  (* Strong elimination, induction on evaluations *)
    1.99 @@ -250,7 +232,7 @@
   1.100  by (dtac CollectD 1);
   1.101  by (safe_tac (!claset));
   1.102  by (ALLGOALS (resolve_tac prems));
   1.103 -by (ALLGOALS (Fast_tac));
   1.104 +by (ALLGOALS (Blast_tac));
   1.105  qed "eval_ind0";
   1.106  
   1.107  val prems = goal MT.thy 
   1.108 @@ -287,51 +269,46 @@
   1.109  
   1.110  (* Introduction rules *)
   1.111  
   1.112 -val prems = goalw MT.thy [elab_def, elab_rel_def] 
   1.113 -  "c isof ty ==> te |- e_const(c) ===> ty";
   1.114 -by (cut_facts_tac prems 1);
   1.115 +goalw MT.thy [elab_def, elab_rel_def] 
   1.116 +  "!!te. c isof ty ==> te |- e_const(c) ===> ty";
   1.117  by (rtac lfp_intro2 1);
   1.118  by (rtac elab_fun_mono 1);
   1.119  by (rewtac elab_fun_def);
   1.120 -by (Fast_tac 1);
   1.121 +by (blast_tac (!claset addSIs [exI]) 1);
   1.122  qed "elab_const";
   1.123  
   1.124 -val prems = goalw MT.thy [elab_def, elab_rel_def] 
   1.125 -  "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
   1.126 -by (cut_facts_tac prems 1);
   1.127 +goalw MT.thy [elab_def, elab_rel_def] 
   1.128 +  "!!te. x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
   1.129  by (rtac lfp_intro2 1);
   1.130  by (rtac elab_fun_mono 1);
   1.131  by (rewtac elab_fun_def);
   1.132 -by (Fast_tac 1);
   1.133 +by (blast_tac (!claset addSIs [exI]) 1);
   1.134  qed "elab_var";
   1.135  
   1.136 -val prems = goalw MT.thy [elab_def, elab_rel_def] 
   1.137 -  "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
   1.138 -by (cut_facts_tac prems 1);
   1.139 +goalw MT.thy [elab_def, elab_rel_def] 
   1.140 +  "!!te. te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
   1.141  by (rtac lfp_intro2 1);
   1.142  by (rtac elab_fun_mono 1);
   1.143  by (rewtac elab_fun_def);
   1.144 -by (Fast_tac 1);
   1.145 +by (blast_tac (!claset addSIs [exI]) 1);
   1.146  qed "elab_fn";
   1.147  
   1.148 -val prems = goalw MT.thy [elab_def, elab_rel_def]
   1.149 -  " te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
   1.150 -\   te |- fix f(x) = e ===> ty1->ty2";
   1.151 -by (cut_facts_tac prems 1);
   1.152 +goalw MT.thy [elab_def, elab_rel_def]
   1.153 +  "!!te. te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
   1.154 +\        te |- fix f(x) = e ===> ty1->ty2";
   1.155  by (rtac lfp_intro2 1);
   1.156  by (rtac elab_fun_mono 1);
   1.157  by (rewtac elab_fun_def);
   1.158 -by (Fast_tac 1);
   1.159 +by (blast_tac (!claset addSIs [exI]) 1);
   1.160  qed "elab_fix";
   1.161  
   1.162 -val prems = goalw MT.thy [elab_def, elab_rel_def] 
   1.163 -  " [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
   1.164 -\   te |- e1 @ e2 ===> ty2";
   1.165 -by (cut_facts_tac prems 1);
   1.166 +goalw MT.thy [elab_def, elab_rel_def] 
   1.167 +  "!!te. [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
   1.168 +\        te |- e1 @ e2 ===> ty2";
   1.169  by (rtac lfp_intro2 1);
   1.170  by (rtac elab_fun_mono 1);
   1.171  by (rewtac elab_fun_def);
   1.172 -by (fast_tac (!claset addSIs [disjI2]) 1);
   1.173 +by (blast_tac (!claset addSIs [disjI2]) 1);
   1.174  qed "elab_app";
   1.175  
   1.176  (* Strong elimination, induction on elaborations *)
   1.177 @@ -361,7 +338,7 @@
   1.178  by (dtac CollectD 1);
   1.179  by (safe_tac (!claset));
   1.180  by (ALLGOALS (resolve_tac prems));
   1.181 -by (ALLGOALS (Fast_tac));
   1.182 +by (ALLGOALS (Blast_tac));
   1.183  qed "elab_ind0";
   1.184  
   1.185  val prems = goal MT.thy
   1.186 @@ -412,7 +389,7 @@
   1.187  by (dtac CollectD 1);
   1.188  by (safe_tac (!claset));
   1.189  by (ALLGOALS (resolve_tac prems));
   1.190 -by (ALLGOALS (Fast_tac));
   1.191 +by (ALLGOALS (Blast_tac));
   1.192  qed "elab_elim0";
   1.193  
   1.194  val prems = goal MT.thy
   1.195 @@ -441,7 +418,7 @@
   1.196  fun elab_e_elim_tac p = 
   1.197    ( (rtac elab_elim 1) THEN 
   1.198      (resolve_tac p 1) THEN 
   1.199 -    (REPEAT (fast_tac (e_ext_cs (claset_of "HOL")) 1))
   1.200 +    (REPEAT (blast_tac (e_ext_cs HOL_cs) 1))
   1.201    );
   1.202  
   1.203  val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
   1.204 @@ -451,7 +428,7 @@
   1.205  val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t";
   1.206  by (cut_facts_tac prems 1);
   1.207  by (dtac elab_const_elim_lem 1);
   1.208 -by (Fast_tac 1);
   1.209 +by (Blast_tac 1);
   1.210  qed "elab_const_elim";
   1.211  
   1.212  val prems = goal MT.thy 
   1.213 @@ -463,7 +440,7 @@
   1.214    "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
   1.215  by (cut_facts_tac prems 1);
   1.216  by (dtac elab_var_elim_lem 1);
   1.217 -by (Fast_tac 1);
   1.218 +by (Blast_tac 1);
   1.219  qed "elab_var_elim";
   1.220  
   1.221  val prems = goal MT.thy 
   1.222 @@ -479,7 +456,7 @@
   1.223  \   (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
   1.224  by (cut_facts_tac prems 1);
   1.225  by (dtac elab_fn_elim_lem 1);
   1.226 -by (Fast_tac 1);
   1.227 +by (Blast_tac 1);
   1.228  qed "elab_fn_elim";
   1.229  
   1.230  val prems = goal MT.thy 
   1.231 @@ -494,7 +471,7 @@
   1.232  \   (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
   1.233  by (cut_facts_tac prems 1);
   1.234  by (dtac elab_fix_elim_lem 1);
   1.235 -by (Fast_tac 1);
   1.236 +by (Blast_tac 1);
   1.237  qed "elab_fix_elim";
   1.238  
   1.239  val prems = goal MT.thy 
   1.240 @@ -507,7 +484,7 @@
   1.241   "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
   1.242  by (cut_facts_tac prems 1);
   1.243  by (dtac elab_app_elim_lem 1);
   1.244 -by (Fast_tac 1);
   1.245 +by (Blast_tac 1);
   1.246  qed "elab_app_elim";
   1.247  
   1.248  (* ############################################################ *)
   1.249 @@ -518,7 +495,8 @@
   1.250  
   1.251  goalw MT.thy [mono_def,MT.hasty_fun_def] "mono(hasty_fun)";
   1.252  by infsys_mono_tac;
   1.253 -bind_thm("mono_hasty_fun",  result());
   1.254 +by (Blast_tac 1);
   1.255 +qed "mono_hasty_fun";
   1.256  
   1.257  (* 
   1.258    Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it 
   1.259 @@ -534,7 +512,7 @@
   1.260  by (rewtac MT.hasty_fun_def);
   1.261  by (rtac CollectI 1);
   1.262  by (rtac disjI1 1);
   1.263 -by (Fast_tac 1);
   1.264 +by (Blast_tac 1);
   1.265  by (rtac mono_hasty_fun 1);
   1.266  qed "hasty_rel_const_coind";
   1.267  
   1.268 @@ -553,7 +531,7 @@
   1.269  by (rewtac hasty_fun_def);
   1.270  by (rtac CollectI 1);
   1.271  by (rtac disjI2 1);
   1.272 -by (fast_tac (claset_of "HOL") 1);
   1.273 +by (blast_tac HOL_cs 1);
   1.274  by (rtac mono_hasty_fun 1);
   1.275  qed "hasty_rel_clos_coind";
   1.276  
   1.277 @@ -575,8 +553,7 @@
   1.278  by (dtac CollectD 1);
   1.279  by (fold_goals_tac [hasty_fun_def]);
   1.280  by (safe_tac (!claset));
   1.281 -by (ALLGOALS (resolve_tac prems));
   1.282 -by (ALLGOALS (Fast_tac));
   1.283 +by (REPEAT (ares_tac prems 1));
   1.284  qed "hasty_rel_elim0";
   1.285  
   1.286  val prems = goal MT.thy 
   1.287 @@ -597,29 +574,27 @@
   1.288  
   1.289  (* Introduction rules for hasty *)
   1.290  
   1.291 -val prems = goalw MT.thy [hasty_def] "c isof t ==> v_const(c) hasty t";
   1.292 -by (resolve_tac (prems RL [hasty_rel_const_coind]) 1);
   1.293 +goalw MT.thy [hasty_def] "!!c. c isof t ==> v_const(c) hasty t";
   1.294 +by (etac hasty_rel_const_coind 1);
   1.295  qed "hasty_const";
   1.296  
   1.297 -val prems = goalw MT.thy [hasty_def,hasty_env_def] 
   1.298 -  "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
   1.299 -by (cut_facts_tac prems 1);
   1.300 +goalw MT.thy [hasty_def,hasty_env_def] 
   1.301 + "!!t. te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
   1.302  by (rtac hasty_rel_clos_coind 1);
   1.303 -by (ALLGOALS (Fast_tac));
   1.304 +by (ALLGOALS (blast_tac (!claset delrules [equalityI])));
   1.305  qed "hasty_clos";
   1.306  
   1.307  (* Elimination on constants for hasty *)
   1.308  
   1.309 -val prems = goalw MT.thy [hasty_def] 
   1.310 -  "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
   1.311 -by (cut_facts_tac prems 1);
   1.312 +goalw MT.thy [hasty_def] 
   1.313 +  "!!v. v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
   1.314  by (rtac hasty_rel_elim 1);
   1.315 -by (ALLGOALS (fast_tac (v_ext_cs (claset_of "HOL"))));
   1.316 +by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
   1.317  qed "hasty_elim_const_lem";
   1.318  
   1.319 -val prems = goal MT.thy "v_const(c) hasty t ==> c isof t";
   1.320 -by (cut_facts_tac (prems RL [hasty_elim_const_lem]) 1);
   1.321 -by (Fast_tac 1);
   1.322 +goal MT.thy "!!c. v_const(c) hasty t ==> c isof t";
   1.323 +by (dtac hasty_elim_const_lem 1);
   1.324 +by (Blast_tac 1);
   1.325  qed "hasty_elim_const";
   1.326  
   1.327  (* Elimination on closures for hasty *)
   1.328 @@ -630,14 +605,14 @@
   1.329  \     v=v_clos(<|x,e,ve|>) --> (? te.te |- fn x => e ===> t & ve hastyenv te)";
   1.330  by (cut_facts_tac prems 1);
   1.331  by (rtac hasty_rel_elim 1);
   1.332 -by (ALLGOALS (fast_tac (v_ext_cs (claset_of "HOL"))));
   1.333 +by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
   1.334  qed "hasty_elim_clos_lem";
   1.335  
   1.336 -val prems = goal MT.thy 
   1.337 -  "v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===>\
   1.338 -  \t & ve hastyenv te ";
   1.339 -by (cut_facts_tac (prems RL [hasty_elim_clos_lem]) 1);
   1.340 -by (Fast_tac 1);
   1.341 +goal MT.thy 
   1.342 +  "!!t. v_clos(<|ev,e,ve|>) hasty t ==>  \
   1.343 +\       ? te.te |- fn ev => e ===> t & ve hastyenv te ";
   1.344 +by (dtac hasty_elim_clos_lem 1);
   1.345 +by (Blast_tac 1);
   1.346  qed "hasty_elim_clos";
   1.347  
   1.348  (* ############################################################ *)
   1.349 @@ -650,10 +625,10 @@
   1.350  by (rewtac hasty_env_def);
   1.351  by (asm_full_simp_tac (!simpset delsimps mem_simps
   1.352                                  addsimps [ve_dom_owr, te_dom_owr]) 1);
   1.353 -by (safe_tac (claset_of "HOL"));
   1.354 +by (safe_tac HOL_cs);
   1.355  by (excluded_middle_tac "ev=x" 1);
   1.356  by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
   1.357 -by (Fast_tac 1);
   1.358 +by (Blast_tac 1);
   1.359  by (asm_simp_tac (!simpset addsimps [ve_app_owr1, te_app_owr1]) 1);
   1.360  qed "hasty_env1";
   1.361  
   1.362 @@ -661,38 +636,34 @@
   1.363  (* The Consistency theorem                                      *)
   1.364  (* ############################################################ *)
   1.365  
   1.366 -val prems = goal MT.thy 
   1.367 -  "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
   1.368 -by (cut_facts_tac prems 1);
   1.369 +goal MT.thy 
   1.370 +  "!!t. [| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
   1.371  by (dtac elab_const_elim 1);
   1.372  by (etac hasty_const 1);
   1.373  qed "consistency_const";
   1.374  
   1.375 -val prems = goalw MT.thy [hasty_env_def]
   1.376 -  " [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
   1.377 -\   ve_app ve ev hasty t";
   1.378 -by (cut_facts_tac prems 1);
   1.379 +goalw MT.thy [hasty_env_def]
   1.380 +  "!!t. [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
   1.381 +\       ve_app ve ev hasty t";
   1.382  by (dtac elab_var_elim 1);
   1.383 -by (Fast_tac 1);
   1.384 +by (Blast_tac 1);
   1.385  qed "consistency_var";
   1.386  
   1.387 -val prems = goal MT.thy
   1.388 -  " [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
   1.389 -\   v_clos(<| ev, e, ve |>) hasty t";
   1.390 -by (cut_facts_tac prems 1);
   1.391 +goal MT.thy
   1.392 +  "!!t. [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
   1.393 +\       v_clos(<| ev, e, ve |>) hasty t";
   1.394  by (rtac hasty_clos 1);
   1.395 -by (Fast_tac 1);
   1.396 +by (Blast_tac 1);
   1.397  qed "consistency_fn";
   1.398  
   1.399 -val prems = goalw MT.thy [hasty_env_def,hasty_def]
   1.400 -  " [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
   1.401 +goalw MT.thy [hasty_env_def,hasty_def]
   1.402 +  "!!t. [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
   1.403  \      ve hastyenv te ; \
   1.404  \      te |- fix ev2  ev1  = e ===> t \
   1.405  \   |] ==> \
   1.406  \   v_clos(cl) hasty t";
   1.407 -by (cut_facts_tac prems 1);
   1.408  by (dtac elab_fix_elim 1);
   1.409 -by (safe_tac (claset_of "HOL"));
   1.410 +by (safe_tac HOL_cs);
   1.411  (*Do a single unfolding of cl*)
   1.412  by ((forward_tac [ssubst] 1) THEN (assume_tac 2));
   1.413  by (rtac hasty_rel_clos_coind 1);
   1.414 @@ -700,37 +671,36 @@
   1.415  by (asm_simp_tac (!simpset addsimps [ve_dom_owr, te_dom_owr]) 1);
   1.416  
   1.417  by (asm_simp_tac (!simpset delsimps mem_simps addsimps [ve_dom_owr]) 1);
   1.418 -by (safe_tac (claset_of "HOL"));
   1.419 +by (safe_tac HOL_cs);
   1.420  by (excluded_middle_tac "ev2=ev1a" 1);
   1.421  by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
   1.422 -by (Fast_tac 1);
   1.423 +by (Blast_tac 1);
   1.424  
   1.425  by (asm_simp_tac (!simpset delsimps mem_simps
   1.426                             addsimps [ve_app_owr1, te_app_owr1]) 1);
   1.427  by (hyp_subst_tac 1);
   1.428  by (etac subst 1);
   1.429 -by (Fast_tac 1);
   1.430 +by (Blast_tac 1);
   1.431  qed "consistency_fix";
   1.432  
   1.433 -val prems = goal MT.thy 
   1.434 -  " [| ! t te. ve hastyenv te  --> te |- e1 ===> t --> v_const(c1) hasty t; \
   1.435 +goal MT.thy 
   1.436 +  "!!t. [| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
   1.437  \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v_const(c2) hasty t; \
   1.438  \      ve hastyenv te ; te |- e1 @ e2 ===> t \
   1.439  \   |] ==> \
   1.440  \   v_const(c_app c1 c2) hasty t";
   1.441 -by (cut_facts_tac prems 1);
   1.442  by (dtac elab_app_elim 1);
   1.443  by (safe_tac (!claset));
   1.444  by (rtac hasty_const 1);
   1.445  by (rtac isof_app 1);
   1.446  by (rtac hasty_elim_const 1);
   1.447 -by (Fast_tac 1);
   1.448 +by (Blast_tac 1);
   1.449  by (rtac hasty_elim_const 1);
   1.450 -by (Fast_tac 1);
   1.451 +by (Blast_tac 1);
   1.452  qed "consistency_app1";
   1.453  
   1.454 -val prems = goal MT.thy 
   1.455 -  " [| ! t te. \
   1.456 +goal MT.thy 
   1.457 +  "!!t.  [| ! t te. \
   1.458  \        ve hastyenv te  --> \
   1.459  \        te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
   1.460  \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v2 hasty t; \
   1.461 @@ -740,7 +710,6 @@
   1.462  \      te |- e1 @ e2 ===> t \
   1.463  \   |] ==> \
   1.464  \   v hasty t";
   1.465 -by (cut_facts_tac prems 1);
   1.466  by (dtac elab_app_elim 1);
   1.467  by (safe_tac (!claset));
   1.468  by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
   1.469 @@ -754,10 +723,7 @@
   1.470  by (dtac hasty_elim_clos 1);
   1.471  by (safe_tac (!claset));
   1.472  by (dtac elab_fn_elim 1);
   1.473 -by (safe_tac (!claset));
   1.474 -by (dtac t_fun_inj 1);
   1.475 -by (safe_tac (!claset));
   1.476 -by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (Fast_tac 1));
   1.477 +by (blast_tac (!claset addIs [hasty_env1] addSDs [t_fun_inj]) 1);
   1.478  qed "consistency_app2";
   1.479  
   1.480  val [major] = goal MT.thy 
   1.481 @@ -795,10 +761,7 @@
   1.482  by (cut_facts_tac prems 1);
   1.483  by (rtac hasty_elim_const 1);
   1.484  by (dtac consistency 1);
   1.485 -by (fast_tac (!claset addSIs [basic_consistency_lem]) 1);
   1.486 +by (blast_tac (!claset addSIs [basic_consistency_lem]) 1);
   1.487  qed "basic_consistency";
   1.488  
   1.489 -
   1.490 -Unify.search_bound := orig_search_bound;
   1.491 -
   1.492  writeln"Reached end of file.";