src/HOL/ex/MT.ML
changeset 5148 74919e8f221c
parent 5143 b94cd208f073
child 5227 e5a6ace920a0
     1.1 --- a/src/HOL/ex/MT.ML	Wed Jul 15 14:13:18 1998 +0200
     1.2 +++ b/src/HOL/ex/MT.ML	Wed Jul 15 14:19:02 1998 +0200
     1.3 @@ -27,17 +27,15 @@
     1.4  by (simp_tac (simpset() addsimps prems) 1);
     1.5  qed "infsys_p1";
     1.6  
     1.7 -val prems = goal MT.thy "!!a b. P (fst (a,b)) (snd (a,b)) ==> P a b";
     1.8 +Goal "P (fst (a,b)) (snd (a,b)) ==> P a b";
     1.9  by (Asm_full_simp_tac 1);
    1.10  qed "infsys_p2";
    1.11  
    1.12 -val prems = goal MT.thy 
    1.13 - "!!a. P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
    1.14 +Goal "P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
    1.15  by (Asm_full_simp_tac 1);
    1.16  qed "infsys_pp1";
    1.17  
    1.18 -val prems = goal MT.thy 
    1.19 - "!!a. P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c";
    1.20 +Goal "P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c";
    1.21  by (Asm_full_simp_tac 1);
    1.22  qed "infsys_pp2";
    1.23  
    1.24 @@ -154,51 +152,46 @@
    1.25  by (blast_tac (claset() addSIs [exI]) 1);
    1.26  qed "eval_const";
    1.27  
    1.28 -val prems = goalw MT.thy [eval_def, eval_rel_def] 
    1.29 +Goalw [eval_def, eval_rel_def] 
    1.30    "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app ve ev";
    1.31 -by (cut_facts_tac prems 1);
    1.32  by (rtac lfp_intro2 1);
    1.33  by (rtac eval_fun_mono 1);
    1.34  by (rewtac eval_fun_def);
    1.35  by (blast_tac (claset() addSIs [exI]) 1);
    1.36  qed "eval_var2";
    1.37  
    1.38 -val prems = goalw MT.thy [eval_def, eval_rel_def] 
    1.39 +Goalw [eval_def, eval_rel_def] 
    1.40    "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)";
    1.41 -by (cut_facts_tac prems 1);
    1.42  by (rtac lfp_intro2 1);
    1.43  by (rtac eval_fun_mono 1);
    1.44  by (rewtac eval_fun_def);
    1.45  by (blast_tac (claset() addSIs [exI]) 1);
    1.46  qed "eval_fn";
    1.47  
    1.48 -val prems = goalw MT.thy [eval_def, eval_rel_def] 
    1.49 +Goalw [eval_def, eval_rel_def] 
    1.50    " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
    1.51  \   ve |- fix ev2(ev1) = e ---> v_clos(cl)";
    1.52 -by (cut_facts_tac prems 1);
    1.53  by (rtac lfp_intro2 1);
    1.54  by (rtac eval_fun_mono 1);
    1.55  by (rewtac eval_fun_def);
    1.56  by (blast_tac (claset() addSIs [exI]) 1);
    1.57  qed "eval_fix";
    1.58  
    1.59 -val prems = goalw MT.thy [eval_def, eval_rel_def]
    1.60 +Goalw [eval_def, eval_rel_def]
    1.61    " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==> \
    1.62  \   ve |- e1 @ e2 ---> v_const(c_app c1 c2)";
    1.63 -by (cut_facts_tac prems 1);
    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 (blast_tac (claset() addSIs [exI]) 1);
    1.68  qed "eval_app1";
    1.69  
    1.70 -val prems = goalw MT.thy [eval_def, eval_rel_def] 
    1.71 +Goalw [eval_def, eval_rel_def] 
    1.72    " [|  ve |- e1 ---> v_clos(<|xm,em,vem|>); \
    1.73  \       ve |- e2 ---> v2; \
    1.74  \       vem + {xm |-> v2} |- em ---> v \
    1.75  \   |] ==> \
    1.76  \   ve |- e1 @ e2 ---> v";
    1.77 -by (cut_facts_tac prems 1);
    1.78  by (rtac lfp_intro2 1);
    1.79  by (rtac eval_fun_mono 1);
    1.80  by (rewtac eval_fun_def);
    1.81 @@ -270,7 +263,7 @@
    1.82  (* Introduction rules *)
    1.83  
    1.84  Goalw [elab_def, elab_rel_def] 
    1.85 -  "!!te. c isof ty ==> te |- e_const(c) ===> ty";
    1.86 +  "c isof ty ==> te |- e_const(c) ===> ty";
    1.87  by (rtac lfp_intro2 1);
    1.88  by (rtac elab_fun_mono 1);
    1.89  by (rewtac elab_fun_def);
    1.90 @@ -278,7 +271,7 @@
    1.91  qed "elab_const";
    1.92  
    1.93  Goalw [elab_def, elab_rel_def] 
    1.94 -  "!!te. x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
    1.95 +  "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
    1.96  by (rtac lfp_intro2 1);
    1.97  by (rtac elab_fun_mono 1);
    1.98  by (rewtac elab_fun_def);
    1.99 @@ -286,7 +279,7 @@
   1.100  qed "elab_var";
   1.101  
   1.102  Goalw [elab_def, elab_rel_def] 
   1.103 -  "!!te. te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
   1.104 +  "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
   1.105  by (rtac lfp_intro2 1);
   1.106  by (rtac elab_fun_mono 1);
   1.107  by (rewtac elab_fun_def);
   1.108 @@ -294,7 +287,7 @@
   1.109  qed "elab_fn";
   1.110  
   1.111  Goalw [elab_def, elab_rel_def]
   1.112 -  "!!te. te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
   1.113 +  "te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
   1.114  \        te |- fix f(x) = e ===> ty1->ty2";
   1.115  by (rtac lfp_intro2 1);
   1.116  by (rtac elab_fun_mono 1);
   1.117 @@ -303,7 +296,7 @@
   1.118  qed "elab_fix";
   1.119  
   1.120  Goalw [elab_def, elab_rel_def] 
   1.121 -  "!!te. [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
   1.122 +  "[| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
   1.123  \        te |- e1 @ e2 ===> ty2";
   1.124  by (rtac lfp_intro2 1);
   1.125  by (rtac elab_fun_mono 1);
   1.126 @@ -425,8 +418,7 @@
   1.127  by (elab_e_elim_tac prems);
   1.128  qed "elab_const_elim_lem";
   1.129  
   1.130 -val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t";
   1.131 -by (cut_facts_tac prems 1);
   1.132 +Goal "te |- e_const(c) ===> t ==> c isof t";
   1.133  by (dtac elab_const_elim_lem 1);
   1.134  by (Blast_tac 1);
   1.135  qed "elab_const_elim";
   1.136 @@ -436,9 +428,7 @@
   1.137  by (elab_e_elim_tac prems);
   1.138  qed "elab_var_elim_lem";
   1.139  
   1.140 -val prems = goal MT.thy 
   1.141 -  "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
   1.142 -by (cut_facts_tac prems 1);
   1.143 +Goal "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
   1.144  by (dtac elab_var_elim_lem 1);
   1.145  by (Blast_tac 1);
   1.146  qed "elab_var_elim";
   1.147 @@ -451,10 +441,9 @@
   1.148  by (elab_e_elim_tac prems);
   1.149  qed "elab_fn_elim_lem";
   1.150  
   1.151 -val prems = goal MT.thy 
   1.152 +Goal 
   1.153    " te |- fn x1 => e1 ===> t ==> \
   1.154  \   (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
   1.155 -by (cut_facts_tac prems 1);
   1.156  by (dtac elab_fn_elim_lem 1);
   1.157  by (Blast_tac 1);
   1.158  qed "elab_fn_elim";
   1.159 @@ -466,10 +455,9 @@
   1.160  by (elab_e_elim_tac prems);
   1.161  qed "elab_fix_elim_lem";
   1.162  
   1.163 -val prems = goal MT.thy 
   1.164 +Goal 
   1.165    " te |- fix ev1(ev2) = e1 ===> t ==> \
   1.166  \   (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
   1.167 -by (cut_facts_tac prems 1);
   1.168  by (dtac elab_fix_elim_lem 1);
   1.169  by (Blast_tac 1);
   1.170  qed "elab_fix_elim";
   1.171 @@ -480,9 +468,8 @@
   1.172  by (elab_e_elim_tac prems);
   1.173  qed "elab_app_elim_lem";
   1.174  
   1.175 -val prems = goal MT.thy
   1.176 +Goal
   1.177   "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
   1.178 -by (cut_facts_tac prems 1);
   1.179  by (dtac elab_app_elim_lem 1);
   1.180  by (Blast_tac 1);
   1.181  qed "elab_app_elim";
   1.182 @@ -505,9 +492,7 @@
   1.183  
   1.184  (* First strong indtroduction (co-induction) rule for hasty_rel *)
   1.185  
   1.186 -val prems =
   1.187  Goalw [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel";
   1.188 -by (cut_facts_tac prems 1);
   1.189  by (rtac gfp_coind2 1);
   1.190  by (rewtac MT.hasty_fun_def);
   1.191  by (rtac CollectI 1);
   1.192 @@ -518,7 +503,7 @@
   1.193  
   1.194  (* Second strong introduction (co-induction) rule for hasty_rel *)
   1.195  
   1.196 -val prems = goalw MT.thy [hasty_rel_def]
   1.197 +Goalw [hasty_rel_def]
   1.198    " [|  te |- fn ev => e ===> t; \
   1.199  \       ve_dom(ve) = te_dom(te); \
   1.200  \       ! ev1. \
   1.201 @@ -526,7 +511,6 @@
   1.202  \         (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel \
   1.203  \   |] ==> \
   1.204  \   (v_clos(<|ev,e,ve|>),t) : hasty_rel";
   1.205 -by (cut_facts_tac prems 1);
   1.206  by (rtac gfp_coind2 1);
   1.207  by (rewtac hasty_fun_def);
   1.208  by (rtac CollectI 1);
   1.209 @@ -579,7 +563,7 @@
   1.210  qed "hasty_const";
   1.211  
   1.212  Goalw [hasty_def,hasty_env_def] 
   1.213 - "!!t. te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
   1.214 + "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
   1.215  by (rtac hasty_rel_clos_coind 1);
   1.216  by (ALLGOALS (blast_tac (claset() delrules [equalityI])));
   1.217  qed "hasty_clos";
   1.218 @@ -587,7 +571,7 @@
   1.219  (* Elimination on constants for hasty *)
   1.220  
   1.221  Goalw [hasty_def] 
   1.222 -  "!!v. v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
   1.223 +  "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
   1.224  by (rtac hasty_rel_elim 1);
   1.225  by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
   1.226  qed "hasty_elim_const_lem";
   1.227 @@ -599,17 +583,16 @@
   1.228  
   1.229  (* Elimination on closures for hasty *)
   1.230  
   1.231 -val prems = goalw MT.thy [hasty_env_def,hasty_def] 
   1.232 +Goalw [hasty_env_def,hasty_def] 
   1.233    " v hasty t ==> \
   1.234  \   ! x e ve. \
   1.235  \     v=v_clos(<|x,e,ve|>) --> (? te. te |- fn x => e ===> t & ve hastyenv te)";
   1.236 -by (cut_facts_tac prems 1);
   1.237  by (rtac hasty_rel_elim 1);
   1.238  by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
   1.239  qed "hasty_elim_clos_lem";
   1.240  
   1.241  Goal 
   1.242 -  "!!t. v_clos(<|ev,e,ve|>) hasty t ==>  \
   1.243 +  "v_clos(<|ev,e,ve|>) hasty t ==>  \
   1.244  \       ? te. te |- fn ev => e ===> t & ve hastyenv te ";
   1.245  by (dtac hasty_elim_clos_lem 1);
   1.246  by (Blast_tac 1);
   1.247 @@ -620,7 +603,7 @@
   1.248  (* ############################################################ *)
   1.249  
   1.250  Goal
   1.251 -  "!!ve. [| ve hastyenv te; v hasty t |] ==> \
   1.252 +  "[| ve hastyenv te; v hasty t |] ==> \
   1.253  \        ve + {ev |-> v} hastyenv te + {ev |=> t}";
   1.254  by (rewtac hasty_env_def);
   1.255  by (asm_full_simp_tac (simpset() delsimps mem_simps
   1.256 @@ -637,27 +620,27 @@
   1.257  (* ############################################################ *)
   1.258  
   1.259  Goal 
   1.260 -  "!!t. [| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
   1.261 +  "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
   1.262  by (dtac elab_const_elim 1);
   1.263  by (etac hasty_const 1);
   1.264  qed "consistency_const";
   1.265  
   1.266  Goalw [hasty_env_def]
   1.267 -  "!!t. [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
   1.268 +  "[| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
   1.269  \       ve_app ve ev hasty t";
   1.270  by (dtac elab_var_elim 1);
   1.271  by (Blast_tac 1);
   1.272  qed "consistency_var";
   1.273  
   1.274  Goal
   1.275 -  "!!t. [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
   1.276 +  "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
   1.277  \       v_clos(<| ev, e, ve |>) hasty t";
   1.278  by (rtac hasty_clos 1);
   1.279  by (Blast_tac 1);
   1.280  qed "consistency_fn";
   1.281  
   1.282  Goalw [hasty_env_def,hasty_def]
   1.283 -  "!!t. [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
   1.284 +  "[| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
   1.285  \      ve hastyenv te ; \
   1.286  \      te |- fix ev2  ev1  = e ===> t \
   1.287  \   |] ==> \
   1.288 @@ -684,7 +667,7 @@
   1.289  qed "consistency_fix";
   1.290  
   1.291  Goal 
   1.292 -  "!!t. [| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
   1.293 +  "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
   1.294  \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v_const(c2) hasty t; \
   1.295  \      ve hastyenv te ; te |- e1 @ e2 ===> t \
   1.296  \   |] ==> \
   1.297 @@ -700,7 +683,7 @@
   1.298  qed "consistency_app1";
   1.299  
   1.300  Goal 
   1.301 -  "!!t.  [| ! t te. \
   1.302 +  "[| ! t te. \
   1.303  \        ve hastyenv te  --> \
   1.304  \        te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
   1.305  \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v2 hasty t; \
   1.306 @@ -726,13 +709,13 @@
   1.307  by (blast_tac (claset() addIs [hasty_env1] addSDs [t_fun_inj]) 1);
   1.308  qed "consistency_app2";
   1.309  
   1.310 -val [major] = goal MT.thy 
   1.311 +Goal
   1.312    "ve |- e ---> v ==> \
   1.313  \  (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
   1.314  
   1.315  (* Proof by induction on the structure of evaluations *)
   1.316  
   1.317 -by (rtac (major RS eval_ind) 1);
   1.318 +by (etac eval_ind 1);
   1.319  by Safe_tac;
   1.320  by (DEPTH_SOLVE 
   1.321      (ares_tac [consistency_const, consistency_var, consistency_fn,
   1.322 @@ -743,9 +726,8 @@
   1.323  (* The Basic Consistency theorem                                *)
   1.324  (* ############################################################ *)
   1.325  
   1.326 -val prems = goalw MT.thy [isof_env_def,hasty_env_def] 
   1.327 +Goalw [isof_env_def,hasty_env_def] 
   1.328    "ve isofenv te ==> ve hastyenv te";
   1.329 -by (cut_facts_tac prems 1);
   1.330  by Safe_tac;
   1.331  by (etac allE 1);
   1.332  by (etac impE 1);
   1.333 @@ -756,9 +738,8 @@
   1.334  by (Asm_simp_tac 1);
   1.335  qed "basic_consistency_lem";
   1.336  
   1.337 -val prems = goal MT.thy
   1.338 +Goal
   1.339    "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
   1.340 -by (cut_facts_tac prems 1);
   1.341  by (rtac hasty_elim_const 1);
   1.342  by (dtac consistency 1);
   1.343  by (blast_tac (claset() addSIs [basic_consistency_lem]) 1);