src/HOL/ex/MT.ML
changeset 1266 3ae9fe3c0f68
parent 1047 5133479a37cf
child 1465 5d7a7e439cec
     1.1 --- a/src/HOL/ex/MT.ML	Wed Oct 04 13:11:57 1995 +0100
     1.2 +++ b/src/HOL/ex/MT.ML	Wed Oct 04 13:12:14 1995 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title: 	HOL/ex/mt.ML
     1.5 +(*  Title: 	HOL/ex/MT.ML
     1.6      ID:         $Id$
     1.7      Author: 	Jacob Frost, Cambridge University Computer Laboratory
     1.8      Copyright   1993  University of Cambridge
     1.9 @@ -39,21 +39,21 @@
    1.10      );
    1.11  
    1.12  val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";
    1.13 -by (simp_tac (prod_ss addsimps prems) 1);
    1.14 +by (simp_tac (!simpset addsimps prems) 1);
    1.15  qed "infsys_p1";
    1.16  
    1.17  val prems = goal MT.thy "!!a b. P (fst (a,b)) (snd (a,b)) ==> P a b";
    1.18 -by (asm_full_simp_tac prod_ss 1);
    1.19 +by (Asm_full_simp_tac 1);
    1.20  qed "infsys_p2";
    1.21  
    1.22  val prems = goal MT.thy 
    1.23   "!!a. P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
    1.24 -by (asm_full_simp_tac prod_ss 1);
    1.25 +by (Asm_full_simp_tac 1);
    1.26  qed "infsys_pp1";
    1.27  
    1.28  val prems = goal MT.thy 
    1.29   "!!a. P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c";
    1.30 -by (asm_full_simp_tac prod_ss 1);
    1.31 +by (Asm_full_simp_tac 1);
    1.32  qed "infsys_pp2";
    1.33  
    1.34  (* ############################################################ *)
    1.35 @@ -175,7 +175,7 @@
    1.36  by (rtac eval_fun_mono 1);
    1.37  by (rewtac eval_fun_def);
    1.38  by (fast_tac set_cs 1);
    1.39 -qed "eval_var";
    1.40 +qed "eval_var2";
    1.41  
    1.42  val prems = goalw MT.thy [eval_def, eval_rel_def] 
    1.43    "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)";
    1.44 @@ -499,8 +499,8 @@
    1.45  by (elab_e_elim_tac prems);
    1.46  qed "elab_app_elim_lem";
    1.47  
    1.48 -val prems = goal MT.thy 
    1.49 -  "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
    1.50 +val prems = goal MT.thy
    1.51 + "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
    1.52  by (cut_facts_tac prems 1);
    1.53  by (dtac elab_app_elim_lem 1);
    1.54  by (fast_tac prop_cs 1);
    1.55 @@ -523,7 +523,8 @@
    1.56  
    1.57  (* First strong indtroduction (co-induction) rule for hasty_rel *)
    1.58  
    1.59 -val prems = goalw MT.thy [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel";
    1.60 +val prems =
    1.61 +  goalw MT.thy [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel";
    1.62  by (cut_facts_tac prems 1);
    1.63  by (rtac gfp_coind2 1);
    1.64  by (rewtac MT.hasty_fun_def);
    1.65 @@ -629,7 +630,8 @@
    1.66  qed "hasty_elim_clos_lem";
    1.67  
    1.68  val prems = goal MT.thy 
    1.69 -  "v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===> t & ve hastyenv te ";
    1.70 +  "v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===>\
    1.71 +  \t & ve hastyenv te ";
    1.72  by (cut_facts_tac (prems RL [hasty_elim_clos_lem]) 1);
    1.73  by (fast_tac HOL_cs 1);
    1.74  qed "hasty_elim_clos";
    1.75 @@ -642,12 +644,13 @@
    1.76    "!!ve. [| ve hastyenv te; v hasty t |] ==> \
    1.77  \        ve + {ev |-> v} hastyenv te + {ev |=> t}";
    1.78  by (rewtac hasty_env_def);
    1.79 -by (asm_full_simp_tac (HOL_ss addsimps [ve_dom_owr, te_dom_owr]) 1);
    1.80 +by (asm_full_simp_tac (!simpset delsimps mem_simps
    1.81 +                                addsimps [ve_dom_owr, te_dom_owr]) 1);
    1.82  by (safe_tac HOL_cs);
    1.83  by (excluded_middle_tac "ev=x" 1);
    1.84 -by (asm_full_simp_tac (HOL_ss addsimps [ve_app_owr2, te_app_owr2]) 1);
    1.85 +by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
    1.86  by (fast_tac set_cs 1);
    1.87 -by (asm_simp_tac (HOL_ss addsimps [ve_app_owr1, te_app_owr1]) 1);
    1.88 +by (asm_simp_tac (!simpset addsimps [ve_app_owr1, te_app_owr1]) 1);
    1.89  qed "hasty_env1";
    1.90  
    1.91  (* ############################################################ *)
    1.92 @@ -690,15 +693,16 @@
    1.93  by ((forward_tac [ssubst] 1) THEN (assume_tac 2));
    1.94  by (rtac hasty_rel_clos_coind 1);
    1.95  by (etac elab_fn 1);
    1.96 -by (asm_simp_tac (HOL_ss addsimps [ve_dom_owr, te_dom_owr]) 1);
    1.97 +by (asm_simp_tac (!simpset addsimps [ve_dom_owr, te_dom_owr]) 1);
    1.98  
    1.99 -by (asm_simp_tac (HOL_ss addsimps [ve_dom_owr]) 1);
   1.100 +by (asm_simp_tac (!simpset delsimps mem_simps addsimps [ve_dom_owr]) 1);
   1.101  by (safe_tac HOL_cs);
   1.102  by (excluded_middle_tac "ev2=ev1a" 1);
   1.103 -by (asm_full_simp_tac (HOL_ss addsimps [ve_app_owr2, te_app_owr2]) 1);
   1.104 +by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
   1.105  by (fast_tac set_cs 1);
   1.106  
   1.107 -by (asm_simp_tac (HOL_ss addsimps [ve_app_owr1, te_app_owr1]) 1);
   1.108 +by (asm_simp_tac (!simpset delsimps mem_simps
   1.109 +                           addsimps [ve_app_owr1, te_app_owr1]) 1);
   1.110  by (hyp_subst_tac 1);
   1.111  by (etac subst 1);
   1.112  by (fast_tac set_cs 1);
   1.113 @@ -779,7 +783,7 @@
   1.114  by (etac exE 1);
   1.115  by (etac conjE 1);
   1.116  by (dtac hasty_const 1);
   1.117 -by (asm_simp_tac HOL_ss 1);
   1.118 +by (Asm_simp_tac 1);
   1.119  qed "basic_consistency_lem";
   1.120  
   1.121  val prems = goal MT.thy
   1.122 @@ -789,5 +793,3 @@
   1.123  by (dtac consistency 1);
   1.124  by (fast_tac (HOL_cs addSIs [basic_consistency_lem]) 1);
   1.125  qed "basic_consistency";
   1.126 -
   1.127 -