src/HOL/ex/MT.ML
changeset 1047 5133479a37cf
parent 972 e61b058d58d2
child 1266 3ae9fe3c0f68
     1.1 --- a/src/HOL/ex/MT.ML	Thu Apr 13 15:08:39 1995 +0200
     1.2 +++ b/src/HOL/ex/MT.ML	Thu Apr 13 15:13:27 1995 +0200
     1.3 @@ -11,6 +11,8 @@
     1.4  Written up as
     1.5      Jacob Frost, A Case Study of Co-induction in Isabelle/HOL
     1.6      Report 308, Computer Lab, University of Cambridge (1993).
     1.7 +
     1.8 +NEEDS TO USE INDUCTIVE DEFS PACKAGE
     1.9  *)
    1.10  
    1.11  open MT;
    1.12 @@ -24,15 +26,6 @@
    1.13  by (assume_tac 1);
    1.14  qed "notsingletonI";
    1.15  
    1.16 -val prems = goalw MT.thy [Un_def]
    1.17 -  "[| c : A Un B; c : A & ~c : B ==> P; c : B ==> P |] ==> P";
    1.18 -by (cut_facts_tac prems 1);bd CollectD 1;be disjE 1;
    1.19 -by (cut_facts_tac [excluded_middle] 1);be disjE 1;
    1.20 -by (resolve_tac prems 1);br conjI 1;ba 1;ba 1;
    1.21 -by (eresolve_tac prems 1);
    1.22 -by (eresolve_tac prems 1);
    1.23 -qed "UnSE";
    1.24 -
    1.25  (* ############################################################ *)
    1.26  (* Inference systems                                            *)
    1.27  (* ############################################################ *)
    1.28 @@ -46,35 +39,21 @@
    1.29      );
    1.30  
    1.31  val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";
    1.32 -by (rtac (fst_conv RS ssubst) 1);
    1.33 -by (rtac (snd_conv RS ssubst) 1);
    1.34 -by (resolve_tac prems 1);
    1.35 +by (simp_tac (prod_ss addsimps prems) 1);
    1.36  qed "infsys_p1";
    1.37  
    1.38 -val prems = goal MT.thy "P (fst (a,b)) (snd (a,b)) ==> P a b";
    1.39 -by (cut_facts_tac prems 1);
    1.40 -by (dtac (fst_conv RS subst) 1);
    1.41 -by (dtac (snd_conv RS subst) 1);
    1.42 -by (assume_tac 1);
    1.43 +val prems = goal MT.thy "!!a b. P (fst (a,b)) (snd (a,b)) ==> P a b";
    1.44 +by (asm_full_simp_tac prod_ss 1);
    1.45  qed "infsys_p2";
    1.46  
    1.47  val prems = goal MT.thy 
    1.48 -  "P a b c ==> P (fst(fst ((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
    1.49 -by (rtac (fst_conv RS ssubst) 1);
    1.50 -by (rtac (fst_conv RS ssubst) 1);
    1.51 -by (rtac (snd_conv RS ssubst) 1);
    1.52 -by (rtac (snd_conv RS ssubst) 1);
    1.53 -by (resolve_tac prems 1);
    1.54 + "!!a. P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
    1.55 +by (asm_full_simp_tac prod_ss 1);
    1.56  qed "infsys_pp1";
    1.57  
    1.58  val prems = goal MT.thy 
    1.59 -  "P (fst(fst ((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c)) ==> P a b c";
    1.60 -by (cut_facts_tac prems 1);
    1.61 -by (dtac (fst_conv RS subst) 1);
    1.62 -by (dtac (fst_conv RS subst) 1);
    1.63 -by (dtac (snd_conv RS subst) 1);
    1.64 -by (dtac (snd_conv RS subst) 1);
    1.65 -by (assume_tac 1);
    1.66 + "!!a. P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c";
    1.67 +by (asm_full_simp_tac prod_ss 1);
    1.68  qed "infsys_pp2";
    1.69  
    1.70  (* ############################################################ *)
    1.71 @@ -86,22 +65,27 @@
    1.72  val prems = goal MT.thy "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)";
    1.73  by (rtac subsetD 1);
    1.74  by (rtac lfp_lemma2 1);
    1.75 -by (resolve_tac prems 1);brs prems 1;
    1.76 +by (resolve_tac prems 1);
    1.77 +by (resolve_tac prems 1);
    1.78  qed "lfp_intro2";
    1.79  
    1.80  val prems = goal MT.thy
    1.81    " [| x:lfp(f); mono(f); !!y. y:f(lfp(f)) ==> P(y) |] ==> \
    1.82  \   P(x)";
    1.83  by (cut_facts_tac prems 1);
    1.84 -by (resolve_tac prems 1);br subsetD 1;
    1.85 -by (rtac lfp_lemma3 1);ba 1;ba 1;
    1.86 +by (resolve_tac prems 1);
    1.87 +by (rtac subsetD 1);
    1.88 +by (rtac lfp_lemma3 1);
    1.89 +by (assume_tac 1);
    1.90 +by (assume_tac 1);
    1.91  qed "lfp_elim2";
    1.92  
    1.93  val prems = goal MT.thy
    1.94    " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x.P(x)}) ==> P(y) |] ==> \
    1.95  \   P(x)";
    1.96  by (cut_facts_tac prems 1);
    1.97 -by (etac induct 1);ba 1;
    1.98 +by (etac induct 1);
    1.99 +by (assume_tac 1);
   1.100  by (eresolve_tac prems 1);
   1.101  qed "lfp_ind2";
   1.102  
   1.103 @@ -112,7 +96,8 @@
   1.104  val [cih,monoh] = goal MT.thy "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)";
   1.105  by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1);
   1.106  by (rtac (monoh RS monoD) 1);
   1.107 -by (rtac (UnE RS subsetI) 1);ba 1;
   1.108 +by (rtac (UnE RS subsetI) 1);
   1.109 +by (assume_tac 1);
   1.110  by (fast_tac (set_cs addSIs [cih]) 1);
   1.111  by (rtac (monoh RS monoD RS subsetD) 1);
   1.112  by (rtac Un_upper2 1);
   1.113 @@ -121,7 +106,11 @@
   1.114  
   1.115  val [gfph,monoh,caseh] = goal MT.thy 
   1.116    "[| x:gfp(f); mono(f); !! y. y:f(gfp(f)) ==> P(y) |] ==> P(x)";
   1.117 -by (rtac caseh 1);br subsetD 1;br gfp_lemma2 1;br monoh 1;br gfph 1;
   1.118 +by (rtac caseh 1);
   1.119 +by (rtac subsetD 1);
   1.120 +by (rtac gfp_lemma2 1);
   1.121 +by (rtac monoh 1);
   1.122 +by (rtac gfph 1);
   1.123  qed "gfp_elim2";
   1.124  
   1.125  (* ############################################################ *)
   1.126 @@ -176,8 +165,7 @@
   1.127  by (rtac lfp_intro2 1);
   1.128  by (rtac eval_fun_mono 1);
   1.129  by (rewtac eval_fun_def);
   1.130 -by (rtac CollectI 1);br disjI1 1;
   1.131 -by (fast_tac HOL_cs 1);
   1.132 +by (fast_tac set_cs 1);
   1.133  qed "eval_const";
   1.134  
   1.135  val prems = goalw MT.thy [eval_def, eval_rel_def] 
   1.136 @@ -186,8 +174,7 @@
   1.137  by (rtac lfp_intro2 1);
   1.138  by (rtac eval_fun_mono 1);
   1.139  by (rewtac eval_fun_def);
   1.140 -by (rtac CollectI 1);br disjI2 1;br disjI1 1;
   1.141 -by (fast_tac HOL_cs 1);
   1.142 +by (fast_tac set_cs 1);
   1.143  qed "eval_var";
   1.144  
   1.145  val prems = goalw MT.thy [eval_def, eval_rel_def] 
   1.146 @@ -196,8 +183,7 @@
   1.147  by (rtac lfp_intro2 1);
   1.148  by (rtac eval_fun_mono 1);
   1.149  by (rewtac eval_fun_def);
   1.150 -by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI1 1;
   1.151 -by (fast_tac HOL_cs 1);
   1.152 +by (fast_tac set_cs 1);
   1.153  qed "eval_fn";
   1.154  
   1.155  val prems = goalw MT.thy [eval_def, eval_rel_def] 
   1.156 @@ -207,8 +193,7 @@
   1.157  by (rtac lfp_intro2 1);
   1.158  by (rtac eval_fun_mono 1);
   1.159  by (rewtac eval_fun_def);
   1.160 -by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1;
   1.161 -by (fast_tac HOL_cs 1);
   1.162 +by (fast_tac set_cs 1);
   1.163  qed "eval_fix";
   1.164  
   1.165  val prems = goalw MT.thy [eval_def, eval_rel_def]
   1.166 @@ -218,8 +203,7 @@
   1.167  by (rtac lfp_intro2 1);
   1.168  by (rtac eval_fun_mono 1);
   1.169  by (rewtac eval_fun_def);
   1.170 -by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1;
   1.171 -by (fast_tac HOL_cs 1);
   1.172 +by (fast_tac set_cs 1);
   1.173  qed "eval_app1";
   1.174  
   1.175  val prems = goalw MT.thy [eval_def, eval_rel_def] 
   1.176 @@ -232,8 +216,7 @@
   1.177  by (rtac lfp_intro2 1);
   1.178  by (rtac eval_fun_mono 1);
   1.179  by (rewtac eval_fun_def);
   1.180 -by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;
   1.181 -by (fast_tac HOL_cs 1);
   1.182 +by (fast_tac (set_cs addSIs [disjI2]) 1);
   1.183  qed "eval_app2";
   1.184  
   1.185  (* Strong elimination, induction on evaluations *)
   1.186 @@ -306,8 +289,7 @@
   1.187  by (rtac lfp_intro2 1);
   1.188  by (rtac elab_fun_mono 1);
   1.189  by (rewtac elab_fun_def);
   1.190 -by (rtac CollectI 1);br disjI1 1;
   1.191 -by (fast_tac HOL_cs 1);
   1.192 +by (fast_tac set_cs 1);
   1.193  qed "elab_const";
   1.194  
   1.195  val prems = goalw MT.thy [elab_def, elab_rel_def] 
   1.196 @@ -316,8 +298,7 @@
   1.197  by (rtac lfp_intro2 1);
   1.198  by (rtac elab_fun_mono 1);
   1.199  by (rewtac elab_fun_def);
   1.200 -by (rtac CollectI 1);br disjI2 1;br disjI1 1;
   1.201 -by (fast_tac HOL_cs 1);
   1.202 +by (fast_tac set_cs 1);
   1.203  qed "elab_var";
   1.204  
   1.205  val prems = goalw MT.thy [elab_def, elab_rel_def] 
   1.206 @@ -326,8 +307,7 @@
   1.207  by (rtac lfp_intro2 1);
   1.208  by (rtac elab_fun_mono 1);
   1.209  by (rewtac elab_fun_def);
   1.210 -by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI1 1;
   1.211 -by (fast_tac HOL_cs 1);
   1.212 +by (fast_tac set_cs 1);
   1.213  qed "elab_fn";
   1.214  
   1.215  val prems = goalw MT.thy [elab_def, elab_rel_def]
   1.216 @@ -337,8 +317,7 @@
   1.217  by (rtac lfp_intro2 1);
   1.218  by (rtac elab_fun_mono 1);
   1.219  by (rewtac elab_fun_def);
   1.220 -by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1;
   1.221 -by (fast_tac HOL_cs 1);
   1.222 +by (fast_tac set_cs 1);
   1.223  qed "elab_fix";
   1.224  
   1.225  val prems = goalw MT.thy [elab_def, elab_rel_def] 
   1.226 @@ -348,8 +327,7 @@
   1.227  by (rtac lfp_intro2 1);
   1.228  by (rtac elab_fun_mono 1);
   1.229  by (rewtac elab_fun_def);
   1.230 -by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;
   1.231 -by (fast_tac HOL_cs 1);
   1.232 +by (fast_tac (set_cs addSIs [disjI2]) 1);
   1.233  qed "elab_app";
   1.234  
   1.235  (* Strong elimination, induction on elaborations *)
   1.236 @@ -549,7 +527,8 @@
   1.237  by (cut_facts_tac prems 1);
   1.238  by (rtac gfp_coind2 1);
   1.239  by (rewtac MT.hasty_fun_def);
   1.240 -by (rtac CollectI 1);br disjI1 1;
   1.241 +by (rtac CollectI 1);
   1.242 +by (rtac disjI1 1);
   1.243  by (fast_tac HOL_cs 1);
   1.244  by (rtac mono_hasty_fun 1);
   1.245  qed "hasty_rel_const_coind";
   1.246 @@ -567,7 +546,8 @@
   1.247  by (cut_facts_tac prems 1);
   1.248  by (rtac gfp_coind2 1);
   1.249  by (rewtac hasty_fun_def);
   1.250 -by (rtac CollectI 1);br disjI2 1;
   1.251 +by (rtac CollectI 1);
   1.252 +by (rtac disjI2 1);
   1.253  by (fast_tac HOL_cs 1);
   1.254  by (rtac mono_hasty_fun 1);
   1.255  qed "hasty_rel_clos_coind";
   1.256 @@ -658,27 +638,16 @@
   1.257  (* The pointwise extension of hasty to environments             *)
   1.258  (* ############################################################ *)
   1.259  
   1.260 -val prems = goal MT.thy
   1.261 -  "[| ve hastyenv te; v hasty t |] ==> \
   1.262 -\  ve + {ev |-> v} hastyenv te + {ev |=> t}";
   1.263 -by (cut_facts_tac prems 1);
   1.264 -by (SELECT_GOAL (rewtac hasty_env_def) 1);
   1.265 +goal MT.thy
   1.266 +  "!!ve. [| ve hastyenv te; v hasty t |] ==> \
   1.267 +\        ve + {ev |-> v} hastyenv te + {ev |=> t}";
   1.268 +by (rewtac hasty_env_def);
   1.269 +by (asm_full_simp_tac (HOL_ss addsimps [ve_dom_owr, te_dom_owr]) 1);
   1.270  by (safe_tac HOL_cs);
   1.271 -by (rtac (ve_dom_owr RS ssubst) 1);
   1.272 -by (rtac (te_dom_owr RS ssubst) 1);
   1.273 -by (etac subst 1);br refl 1;
   1.274 -
   1.275 -by (dtac (ve_dom_owr RS subst) 1);back();back();back();
   1.276 -by (etac UnSE 1);be conjE 1;
   1.277 -by (dtac notsingletonI 1);bd not_sym 1;
   1.278 -by (rtac (ve_app_owr2 RS ssubst) 1);ba 1;
   1.279 -by (rtac (te_app_owr2 RS ssubst) 1);ba 1;
   1.280 -by (fast_tac HOL_cs 1);
   1.281 -by (dtac singletonD 1);by (hyp_subst_tac 1);
   1.282 -
   1.283 -by (rtac (ve_app_owr1 RS ssubst) 1);
   1.284 -by (rtac (te_app_owr1 RS ssubst) 1);
   1.285 -by (assume_tac 1);
   1.286 +by (excluded_middle_tac "ev=x" 1);
   1.287 +by (asm_full_simp_tac (HOL_ss addsimps [ve_app_owr2, te_app_owr2]) 1);
   1.288 +by (fast_tac set_cs 1);
   1.289 +by (asm_simp_tac (HOL_ss addsimps [ve_app_owr1, te_app_owr1]) 1);
   1.290  qed "hasty_env1";
   1.291  
   1.292  (* ############################################################ *)
   1.293 @@ -717,29 +686,20 @@
   1.294  by (cut_facts_tac prems 1);
   1.295  by (dtac elab_fix_elim 1);
   1.296  by (safe_tac HOL_cs);
   1.297 -by ((forward_tac [ssubst] 1) THEN (assume_tac 2) THEN 
   1.298 -    (rtac hasty_rel_clos_coind 1));
   1.299 +(*Do a single unfolding of cl*)
   1.300 +by ((forward_tac [ssubst] 1) THEN (assume_tac 2));
   1.301 +by (rtac hasty_rel_clos_coind 1);
   1.302  by (etac elab_fn 1);
   1.303 -
   1.304 -by (rtac (ve_dom_owr RS ssubst) 1);
   1.305 -by (rtac (te_dom_owr RS ssubst) 1);
   1.306 -by ((etac subst 1) THEN (rtac refl 1));
   1.307 +by (asm_simp_tac (HOL_ss addsimps [ve_dom_owr, te_dom_owr]) 1);
   1.308  
   1.309 -by (rtac (ve_dom_owr RS ssubst) 1);
   1.310 +by (asm_simp_tac (HOL_ss addsimps [ve_dom_owr]) 1);
   1.311  by (safe_tac HOL_cs);
   1.312 -by (dtac (Un_commute RS subst) 1);
   1.313 -by (etac UnSE 1);
   1.314 -
   1.315 -by (safe_tac HOL_cs);
   1.316 -by (dtac notsingletonI 1);bd not_sym 1;
   1.317 -by (rtac (ve_app_owr2 RS ssubst) 1);ba 1;
   1.318 -by (rtac (te_app_owr2 RS ssubst) 1);ba 1;
   1.319 +by (excluded_middle_tac "ev2=ev1a" 1);
   1.320 +by (asm_full_simp_tac (HOL_ss addsimps [ve_app_owr2, te_app_owr2]) 1);
   1.321  by (fast_tac set_cs 1);
   1.322  
   1.323 -by (etac singletonE 1);
   1.324 +by (asm_simp_tac (HOL_ss addsimps [ve_app_owr1, te_app_owr1]) 1);
   1.325  by (hyp_subst_tac 1);
   1.326 -by (rtac (ve_app_owr1 RS ssubst) 1);
   1.327 -by (rtac (te_app_owr1 RS ssubst) 1);
   1.328  by (etac subst 1);
   1.329  by (fast_tac set_cs 1);
   1.330  qed "consistency_fix";
   1.331 @@ -775,8 +735,14 @@
   1.332  by (cut_facts_tac prems 1);
   1.333  by (dtac elab_app_elim 1);
   1.334  by (safe_tac HOL_cs);
   1.335 -by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));ba 1;be impE 1;ba 1;
   1.336 -by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));ba 1;be impE 1;ba 1;
   1.337 +by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
   1.338 +by (assume_tac 1);
   1.339 +by (etac impE 1);
   1.340 +by (assume_tac 1);
   1.341 +by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
   1.342 +by (assume_tac 1);
   1.343 +by (etac impE 1);
   1.344 +by (assume_tac 1);
   1.345  by (dtac hasty_elim_clos 1);
   1.346  by (safe_tac HOL_cs);
   1.347  by (dtac elab_fn_elim 1);
   1.348 @@ -786,20 +752,17 @@
   1.349  by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (fast_tac HOL_cs 1));
   1.350  qed "consistency_app2";
   1.351  
   1.352 -val prems = goal MT.thy 
   1.353 -  "ve |- e ---> v ==> (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
   1.354 +val [major] = goal MT.thy 
   1.355 +  "ve |- e ---> v ==> \
   1.356 +\  (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
   1.357  
   1.358  (* Proof by induction on the structure of evaluations *)
   1.359  
   1.360 -by (resolve_tac (prems RL [eval_ind]) 1);
   1.361 +by (rtac (major RS eval_ind) 1);
   1.362  by (safe_tac HOL_cs);
   1.363 -
   1.364 -by (rtac consistency_const 1);ba 1;ba 1;
   1.365 -by (rtac consistency_var 1);ba 1;ba 1;ba 1;
   1.366 -by (rtac consistency_fn 1);ba 1;ba 1;
   1.367 -by (rtac consistency_fix 1);ba 1;ba 1;ba 1;
   1.368 -by (rtac consistency_app1 1);ba 1;ba 1;ba 1;ba 1;
   1.369 -by (rtac consistency_app2 1);ba 5;ba 4;ba 3;ba 2;ba 1;
   1.370 +by (DEPTH_SOLVE 
   1.371 +    (ares_tac [consistency_const, consistency_var, consistency_fn,
   1.372 +	       consistency_fix, consistency_app1, consistency_app2] 1));
   1.373  qed "consistency";
   1.374  
   1.375  (* ############################################################ *)
   1.376 @@ -810,9 +773,13 @@
   1.377    "ve isofenv te ==> ve hastyenv te";
   1.378  by (cut_facts_tac prems 1);
   1.379  by (safe_tac HOL_cs);
   1.380 -by (etac allE 1);be impE 1;ba 1;be exE 1;be conjE 1;
   1.381 +by (etac allE 1);
   1.382 +by (etac impE 1);
   1.383 +by (assume_tac 1);
   1.384 +by (etac exE 1);
   1.385 +by (etac conjE 1);
   1.386  by (dtac hasty_const 1);
   1.387 -by ((rtac ssubst 1) THEN (assume_tac 1) THEN (assume_tac 1));
   1.388 +by (asm_simp_tac HOL_ss 1);
   1.389  qed "basic_consistency_lem";
   1.390  
   1.391  val prems = goal MT.thy