src/HOL/ex/MT.ML
changeset 1820 e381e1c51689
parent 1584 3d59c407bd36
child 2935 998cb95fdd43
     1.1 --- a/src/HOL/ex/MT.ML	Fri Jun 21 11:57:00 1996 +0200
     1.2 +++ b/src/HOL/ex/MT.ML	Fri Jun 21 12:18:50 1996 +0200
     1.3 @@ -35,11 +35,11 @@
     1.4  (* ############################################################ *)
     1.5  
     1.6  val infsys_mono_tac =
     1.7 -  (rewtac subset_def) THEN (safe_tac HOL_cs) THEN (rtac ballI 1) THEN
     1.8 +  (rewtac subset_def) THEN (safe_tac (claset_of "HOL")) THEN (rtac ballI 1) THEN
     1.9    (rtac CollectI 1) THEN (dtac CollectD 1) THEN
    1.10    REPEAT 
    1.11      ( (TRY ((etac disjE 1) THEN (rtac disjI2 2) THEN (rtac disjI1 1))) THEN
    1.12 -      (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac set_cs 1)
    1.13 +      (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac ((claset_of "Fun")delrules [equalityI]) 1)
    1.14      );
    1.15  
    1.16  val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";
    1.17 @@ -102,7 +102,7 @@
    1.18  by (rtac (monoh RS monoD) 1);
    1.19  by (rtac (UnE RS subsetI) 1);
    1.20  by (assume_tac 1);
    1.21 -by (fast_tac (set_cs addSIs [cih]) 1);
    1.22 +by (fast_tac (!claset addSIs [cih]) 1);
    1.23  by (rtac (monoh RS monoD RS subsetD) 1);
    1.24  by (rtac Un_upper2 1);
    1.25  by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
    1.26 @@ -169,7 +169,7 @@
    1.27  by (rtac lfp_intro2 1);
    1.28  by (rtac eval_fun_mono 1);
    1.29  by (rewtac eval_fun_def);
    1.30 -by (fast_tac set_cs 1);
    1.31 +by (Fast_tac 1);
    1.32  qed "eval_const";
    1.33  
    1.34  val prems = goalw MT.thy [eval_def, eval_rel_def] 
    1.35 @@ -178,7 +178,7 @@
    1.36  by (rtac lfp_intro2 1);
    1.37  by (rtac eval_fun_mono 1);
    1.38  by (rewtac eval_fun_def);
    1.39 -by (fast_tac set_cs 1);
    1.40 +by (Fast_tac 1);
    1.41  qed "eval_var2";
    1.42  
    1.43  val prems = goalw MT.thy [eval_def, eval_rel_def] 
    1.44 @@ -187,7 +187,7 @@
    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 set_cs 1);
    1.49 +by (Fast_tac 1);
    1.50  qed "eval_fn";
    1.51  
    1.52  val prems = goalw MT.thy [eval_def, eval_rel_def] 
    1.53 @@ -197,7 +197,7 @@
    1.54  by (rtac lfp_intro2 1);
    1.55  by (rtac eval_fun_mono 1);
    1.56  by (rewtac eval_fun_def);
    1.57 -by (fast_tac set_cs 1);
    1.58 +by (Fast_tac 1);
    1.59  qed "eval_fix";
    1.60  
    1.61  val prems = goalw MT.thy [eval_def, eval_rel_def]
    1.62 @@ -207,7 +207,7 @@
    1.63  by (rtac lfp_intro2 1);
    1.64  by (rtac eval_fun_mono 1);
    1.65  by (rewtac eval_fun_def);
    1.66 -by (fast_tac set_cs 1);
    1.67 +by (Fast_tac 1);
    1.68  qed "eval_app1";
    1.69  
    1.70  val prems = goalw MT.thy [eval_def, eval_rel_def] 
    1.71 @@ -220,7 +220,7 @@
    1.72  by (rtac lfp_intro2 1);
    1.73  by (rtac eval_fun_mono 1);
    1.74  by (rewtac eval_fun_def);
    1.75 -by (fast_tac (set_cs addSIs [disjI2]) 1);
    1.76 +by (fast_tac (!claset addSIs [disjI2]) 1);
    1.77  qed "eval_app2";
    1.78  
    1.79  (* Strong elimination, induction on evaluations *)
    1.80 @@ -248,9 +248,9 @@
    1.81  by (rtac eval_fun_mono 1);
    1.82  by (rewtac eval_fun_def);
    1.83  by (dtac CollectD 1);
    1.84 -by (safe_tac HOL_cs);
    1.85 +by (safe_tac (!claset));
    1.86  by (ALLGOALS (resolve_tac prems));
    1.87 -by (ALLGOALS (fast_tac set_cs));
    1.88 +by (ALLGOALS (Fast_tac));
    1.89  qed "eval_ind0";
    1.90  
    1.91  val prems = goal MT.thy 
    1.92 @@ -293,7 +293,7 @@
    1.93  by (rtac lfp_intro2 1);
    1.94  by (rtac elab_fun_mono 1);
    1.95  by (rewtac elab_fun_def);
    1.96 -by (fast_tac set_cs 1);
    1.97 +by (Fast_tac 1);
    1.98  qed "elab_const";
    1.99  
   1.100  val prems = goalw MT.thy [elab_def, elab_rel_def] 
   1.101 @@ -302,7 +302,7 @@
   1.102  by (rtac lfp_intro2 1);
   1.103  by (rtac elab_fun_mono 1);
   1.104  by (rewtac elab_fun_def);
   1.105 -by (fast_tac set_cs 1);
   1.106 +by (Fast_tac 1);
   1.107  qed "elab_var";
   1.108  
   1.109  val prems = goalw MT.thy [elab_def, elab_rel_def] 
   1.110 @@ -311,7 +311,7 @@
   1.111  by (rtac lfp_intro2 1);
   1.112  by (rtac elab_fun_mono 1);
   1.113  by (rewtac elab_fun_def);
   1.114 -by (fast_tac set_cs 1);
   1.115 +by (Fast_tac 1);
   1.116  qed "elab_fn";
   1.117  
   1.118  val prems = goalw MT.thy [elab_def, elab_rel_def]
   1.119 @@ -321,7 +321,7 @@
   1.120  by (rtac lfp_intro2 1);
   1.121  by (rtac elab_fun_mono 1);
   1.122  by (rewtac elab_fun_def);
   1.123 -by (fast_tac set_cs 1);
   1.124 +by (Fast_tac 1);
   1.125  qed "elab_fix";
   1.126  
   1.127  val prems = goalw MT.thy [elab_def, elab_rel_def] 
   1.128 @@ -331,7 +331,7 @@
   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 (set_cs addSIs [disjI2]) 1);
   1.133 +by (fast_tac (!claset addSIs [disjI2]) 1);
   1.134  qed "elab_app";
   1.135  
   1.136  (* Strong elimination, induction on elaborations *)
   1.137 @@ -359,9 +359,9 @@
   1.138  by (rtac elab_fun_mono 1);
   1.139  by (rewtac elab_fun_def);
   1.140  by (dtac CollectD 1);
   1.141 -by (safe_tac HOL_cs);
   1.142 +by (safe_tac (!claset));
   1.143  by (ALLGOALS (resolve_tac prems));
   1.144 -by (ALLGOALS (fast_tac set_cs));
   1.145 +by (ALLGOALS (Fast_tac));
   1.146  qed "elab_ind0";
   1.147  
   1.148  val prems = goal MT.thy
   1.149 @@ -410,9 +410,9 @@
   1.150  by (rtac elab_fun_mono 1);
   1.151  by (rewtac elab_fun_def);
   1.152  by (dtac CollectD 1);
   1.153 -by (safe_tac HOL_cs);
   1.154 +by (safe_tac (!claset));
   1.155  by (ALLGOALS (resolve_tac prems));
   1.156 -by (ALLGOALS (fast_tac set_cs));
   1.157 +by (ALLGOALS (Fast_tac));
   1.158  qed "elab_elim0";
   1.159  
   1.160  val prems = goal MT.thy
   1.161 @@ -441,7 +441,7 @@
   1.162  fun elab_e_elim_tac p = 
   1.163    ( (rtac elab_elim 1) THEN 
   1.164      (resolve_tac p 1) THEN 
   1.165 -    (REPEAT (fast_tac (e_ext_cs HOL_cs) 1))
   1.166 +    (REPEAT (fast_tac (e_ext_cs (claset_of "HOL")) 1))
   1.167    );
   1.168  
   1.169  val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
   1.170 @@ -451,7 +451,7 @@
   1.171  val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t";
   1.172  by (cut_facts_tac prems 1);
   1.173  by (dtac elab_const_elim_lem 1);
   1.174 -by (fast_tac prop_cs 1);
   1.175 +by (Fast_tac 1);
   1.176  qed "elab_const_elim";
   1.177  
   1.178  val prems = goal MT.thy 
   1.179 @@ -463,7 +463,7 @@
   1.180    "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
   1.181  by (cut_facts_tac prems 1);
   1.182  by (dtac elab_var_elim_lem 1);
   1.183 -by (fast_tac prop_cs 1);
   1.184 +by (Fast_tac 1);
   1.185  qed "elab_var_elim";
   1.186  
   1.187  val prems = goal MT.thy 
   1.188 @@ -479,7 +479,7 @@
   1.189  \   (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
   1.190  by (cut_facts_tac prems 1);
   1.191  by (dtac elab_fn_elim_lem 1);
   1.192 -by (fast_tac prop_cs 1);
   1.193 +by (Fast_tac 1);
   1.194  qed "elab_fn_elim";
   1.195  
   1.196  val prems = goal MT.thy 
   1.197 @@ -494,7 +494,7 @@
   1.198  \   (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
   1.199  by (cut_facts_tac prems 1);
   1.200  by (dtac elab_fix_elim_lem 1);
   1.201 -by (fast_tac prop_cs 1);
   1.202 +by (Fast_tac 1);
   1.203  qed "elab_fix_elim";
   1.204  
   1.205  val prems = goal MT.thy 
   1.206 @@ -507,7 +507,7 @@
   1.207   "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
   1.208  by (cut_facts_tac prems 1);
   1.209  by (dtac elab_app_elim_lem 1);
   1.210 -by (fast_tac prop_cs 1);
   1.211 +by (Fast_tac 1);
   1.212  qed "elab_app_elim";
   1.213  
   1.214  (* ############################################################ *)
   1.215 @@ -534,7 +534,7 @@
   1.216  by (rewtac MT.hasty_fun_def);
   1.217  by (rtac CollectI 1);
   1.218  by (rtac disjI1 1);
   1.219 -by (fast_tac HOL_cs 1);
   1.220 +by (Fast_tac 1);
   1.221  by (rtac mono_hasty_fun 1);
   1.222  qed "hasty_rel_const_coind";
   1.223  
   1.224 @@ -553,7 +553,7 @@
   1.225  by (rewtac hasty_fun_def);
   1.226  by (rtac CollectI 1);
   1.227  by (rtac disjI2 1);
   1.228 -by (fast_tac HOL_cs 1);
   1.229 +by (fast_tac (claset_of "HOL") 1);
   1.230  by (rtac mono_hasty_fun 1);
   1.231  qed "hasty_rel_clos_coind";
   1.232  
   1.233 @@ -574,9 +574,9 @@
   1.234  by (rewtac hasty_fun_def);
   1.235  by (dtac CollectD 1);
   1.236  by (fold_goals_tac [hasty_fun_def]);
   1.237 -by (safe_tac HOL_cs);
   1.238 +by (safe_tac (!claset));
   1.239  by (ALLGOALS (resolve_tac prems));
   1.240 -by (ALLGOALS (fast_tac set_cs));
   1.241 +by (ALLGOALS (Fast_tac));
   1.242  qed "hasty_rel_elim0";
   1.243  
   1.244  val prems = goal MT.thy 
   1.245 @@ -605,7 +605,7 @@
   1.246    "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
   1.247  by (cut_facts_tac prems 1);
   1.248  by (rtac hasty_rel_clos_coind 1);
   1.249 -by (ALLGOALS (fast_tac set_cs));
   1.250 +by (ALLGOALS (Fast_tac));
   1.251  qed "hasty_clos";
   1.252  
   1.253  (* Elimination on constants for hasty *)
   1.254 @@ -614,12 +614,12 @@
   1.255    "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
   1.256  by (cut_facts_tac prems 1);
   1.257  by (rtac hasty_rel_elim 1);
   1.258 -by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));
   1.259 +by (ALLGOALS (fast_tac (v_ext_cs (claset_of "HOL"))));
   1.260  qed "hasty_elim_const_lem";
   1.261  
   1.262  val prems = goal MT.thy "v_const(c) hasty t ==> c isof t";
   1.263  by (cut_facts_tac (prems RL [hasty_elim_const_lem]) 1);
   1.264 -by (fast_tac HOL_cs 1);
   1.265 +by (Fast_tac 1);
   1.266  qed "hasty_elim_const";
   1.267  
   1.268  (* Elimination on closures for hasty *)
   1.269 @@ -630,14 +630,14 @@
   1.270  \     v=v_clos(<|x,e,ve|>) --> (? te.te |- fn x => e ===> t & ve hastyenv te)";
   1.271  by (cut_facts_tac prems 1);
   1.272  by (rtac hasty_rel_elim 1);
   1.273 -by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));
   1.274 +by (ALLGOALS (fast_tac (v_ext_cs (claset_of "HOL"))));
   1.275  qed "hasty_elim_clos_lem";
   1.276  
   1.277  val prems = goal MT.thy 
   1.278    "v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===>\
   1.279    \t & ve hastyenv te ";
   1.280  by (cut_facts_tac (prems RL [hasty_elim_clos_lem]) 1);
   1.281 -by (fast_tac HOL_cs 1);
   1.282 +by (Fast_tac 1);
   1.283  qed "hasty_elim_clos";
   1.284  
   1.285  (* ############################################################ *)
   1.286 @@ -650,10 +650,10 @@
   1.287  by (rewtac hasty_env_def);
   1.288  by (asm_full_simp_tac (!simpset delsimps mem_simps
   1.289                                  addsimps [ve_dom_owr, te_dom_owr]) 1);
   1.290 -by (safe_tac HOL_cs);
   1.291 +by (safe_tac (claset_of "HOL"));
   1.292  by (excluded_middle_tac "ev=x" 1);
   1.293  by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
   1.294 -by (fast_tac set_cs 1);
   1.295 +by (Fast_tac 1);
   1.296  by (asm_simp_tac (!simpset addsimps [ve_app_owr1, te_app_owr1]) 1);
   1.297  qed "hasty_env1";
   1.298  
   1.299 @@ -673,7 +673,7 @@
   1.300  \   ve_app ve ev hasty t";
   1.301  by (cut_facts_tac prems 1);
   1.302  by (dtac elab_var_elim 1);
   1.303 -by (fast_tac HOL_cs 1);
   1.304 +by (Fast_tac 1);
   1.305  qed "consistency_var";
   1.306  
   1.307  val prems = goal MT.thy
   1.308 @@ -681,7 +681,7 @@
   1.309  \   v_clos(<| ev, e, ve |>) hasty t";
   1.310  by (cut_facts_tac prems 1);
   1.311  by (rtac hasty_clos 1);
   1.312 -by (fast_tac prop_cs 1);
   1.313 +by (Fast_tac 1);
   1.314  qed "consistency_fn";
   1.315  
   1.316  val prems = goalw MT.thy [hasty_env_def,hasty_def]
   1.317 @@ -692,7 +692,7 @@
   1.318  \   v_clos(cl) hasty t";
   1.319  by (cut_facts_tac prems 1);
   1.320  by (dtac elab_fix_elim 1);
   1.321 -by (safe_tac HOL_cs);
   1.322 +by (safe_tac (claset_of "HOL"));
   1.323  (*Do a single unfolding of cl*)
   1.324  by ((forward_tac [ssubst] 1) THEN (assume_tac 2));
   1.325  by (rtac hasty_rel_clos_coind 1);
   1.326 @@ -700,16 +700,16 @@
   1.327  by (asm_simp_tac (!simpset addsimps [ve_dom_owr, te_dom_owr]) 1);
   1.328  
   1.329  by (asm_simp_tac (!simpset delsimps mem_simps addsimps [ve_dom_owr]) 1);
   1.330 -by (safe_tac HOL_cs);
   1.331 +by (safe_tac (claset_of "HOL"));
   1.332  by (excluded_middle_tac "ev2=ev1a" 1);
   1.333  by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
   1.334 -by (fast_tac set_cs 1);
   1.335 +by (Fast_tac 1);
   1.336  
   1.337  by (asm_simp_tac (!simpset delsimps mem_simps
   1.338                             addsimps [ve_app_owr1, te_app_owr1]) 1);
   1.339  by (hyp_subst_tac 1);
   1.340  by (etac subst 1);
   1.341 -by (fast_tac set_cs 1);
   1.342 +by (Fast_tac 1);
   1.343  qed "consistency_fix";
   1.344  
   1.345  val prems = goal MT.thy 
   1.346 @@ -720,13 +720,13 @@
   1.347  \   v_const(c_app c1 c2) hasty t";
   1.348  by (cut_facts_tac prems 1);
   1.349  by (dtac elab_app_elim 1);
   1.350 -by (safe_tac HOL_cs);
   1.351 +by (safe_tac (!claset));
   1.352  by (rtac hasty_const 1);
   1.353  by (rtac isof_app 1);
   1.354  by (rtac hasty_elim_const 1);
   1.355 -by (fast_tac HOL_cs 1);
   1.356 +by (Fast_tac 1);
   1.357  by (rtac hasty_elim_const 1);
   1.358 -by (fast_tac HOL_cs 1);
   1.359 +by (Fast_tac 1);
   1.360  qed "consistency_app1";
   1.361  
   1.362  val prems = goal MT.thy 
   1.363 @@ -742,7 +742,7 @@
   1.364  \   v hasty t";
   1.365  by (cut_facts_tac prems 1);
   1.366  by (dtac elab_app_elim 1);
   1.367 -by (safe_tac HOL_cs);
   1.368 +by (safe_tac (!claset));
   1.369  by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
   1.370  by (assume_tac 1);
   1.371  by (etac impE 1);
   1.372 @@ -752,12 +752,12 @@
   1.373  by (etac impE 1);
   1.374  by (assume_tac 1);
   1.375  by (dtac hasty_elim_clos 1);
   1.376 -by (safe_tac HOL_cs);
   1.377 +by (safe_tac (!claset));
   1.378  by (dtac elab_fn_elim 1);
   1.379 -by (safe_tac HOL_cs);
   1.380 +by (safe_tac (!claset));
   1.381  by (dtac t_fun_inj 1);
   1.382 -by (safe_tac prop_cs);
   1.383 -by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (fast_tac HOL_cs 1));
   1.384 +by (safe_tac (!claset));
   1.385 +by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (Fast_tac 1));
   1.386  qed "consistency_app2";
   1.387  
   1.388  val [major] = goal MT.thy 
   1.389 @@ -767,7 +767,7 @@
   1.390  (* Proof by induction on the structure of evaluations *)
   1.391  
   1.392  by (rtac (major RS eval_ind) 1);
   1.393 -by (safe_tac HOL_cs);
   1.394 +by (safe_tac (!claset));
   1.395  by (DEPTH_SOLVE 
   1.396      (ares_tac [consistency_const, consistency_var, consistency_fn,
   1.397                 consistency_fix, consistency_app1, consistency_app2] 1));
   1.398 @@ -780,7 +780,7 @@
   1.399  val prems = goalw MT.thy [isof_env_def,hasty_env_def] 
   1.400    "ve isofenv te ==> ve hastyenv te";
   1.401  by (cut_facts_tac prems 1);
   1.402 -by (safe_tac HOL_cs);
   1.403 +by (safe_tac (!claset));
   1.404  by (etac allE 1);
   1.405  by (etac impE 1);
   1.406  by (assume_tac 1);
   1.407 @@ -795,7 +795,7 @@
   1.408  by (cut_facts_tac prems 1);
   1.409  by (rtac hasty_elim_const 1);
   1.410  by (dtac consistency 1);
   1.411 -by (fast_tac (HOL_cs addSIs [basic_consistency_lem]) 1);
   1.412 +by (fast_tac (!claset addSIs [basic_consistency_lem]) 1);
   1.413  qed "basic_consistency";
   1.414  
   1.415