inserted Suc_less_eq explictly in a few proofs.
authornipkow
Mon Apr 22 15:42:20 1996 +0200 (1996-04-22)
changeset 1669e56cdf711729
parent 1668 8ead1fe65aad
child 1670 d706a6dce930
inserted Suc_less_eq explictly in a few proofs.
inserted o_def explictly in a few proofs because the new split_tac causes
fewer eta-expansions which some of the rewrites need.

Indented proof in I.ML
src/HOL/MiniML/I.ML
src/HOL/MiniML/W.ML
     1.1 --- a/src/HOL/MiniML/I.ML	Fri Apr 19 11:33:24 1996 +0200
     1.2 +++ b/src/HOL/MiniML/I.ML	Mon Apr 22 15:42:20 1996 +0200
     1.3 @@ -1,45 +1,40 @@
     1.4  open I;
     1.5  
     1.6 -Unify.trace_bound := 45;
     1.7 -Unify.search_bound := 50;
     1.8 -
     1.9  goal thy
    1.10    "! a m s s' t n.  \
    1.11  \    (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) -->   \
    1.12  \    ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )";
    1.13  by (expr.induct_tac "e" 1);
    1.14  
    1.15 -(* case Var n *)
    1.16 -by (simp_tac (!simpset addsimps [app_subst_list]
    1.17 -    setloop (split_tac [expand_if])) 1);
    1.18 -by (fast_tac (HOL_cs addss !simpset) 1);
    1.19 -
    1.20 -(* case Abs e *)
    1.21 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
    1.22 -by (strip_tac 1);
    1.23 -by (rtac conjI 1);
    1.24 +  (* case Var n *)
    1.25 +  by (simp_tac (!simpset addsimps [app_subst_list]
    1.26 +      setloop (split_tac [expand_if])) 1);
    1.27 +  by (fast_tac (HOL_cs addss !simpset) 1);
    1.28  
    1.29 -by (strip_tac 1);
    1.30 -by (REPEAT (etac allE 1));
    1.31 -by (etac impE 1);
    1.32 -by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2);
    1.33 -by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
    1.34 -    less_imp_le,lessI]) 1); 
    1.35 + (* case Abs e *)
    1.36 + by (asm_full_simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
    1.37 + by (strip_tac 1);
    1.38 + by (rtac conjI 1);
    1.39 +  by (strip_tac 1);
    1.40 +  by (REPEAT (etac allE 1));
    1.41 +  by (etac impE 1);
    1.42 +   by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2);
    1.43 +  by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
    1.44 +                              less_imp_le,lessI]) 1); 
    1.45  
    1.46 -by (strip_tac 1);
    1.47 -by (REPEAT (etac allE 1));
    1.48 -by (etac impE 1);
    1.49 -by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2);
    1.50 -by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
    1.51 -    less_imp_le,lessI]) 1); 
    1.52 + by (strip_tac 1);
    1.53 + by (REPEAT (etac allE 1));
    1.54 + by (etac impE 1);
    1.55 +  by (fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])) 2);
    1.56 + by (fast_tac (HOL_cs addIs [new_tv_Suc_list RS mp,new_tv_subst_le,
    1.57 +                             less_imp_le,lessI]) 1);
    1.58  
    1.59  (* case App e1 e2 *)
    1.60  by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
    1.61  by (strip_tac 1);
    1.62  by (rename_tac "s1' t1 n1 s2' t2 n2 sa" 1);
    1.63  by (rtac conjI 1);
    1.64 -by (fast_tac (HOL_cs addss !simpset) 1);
    1.65 -
    1.66 + by (fast_tac (HOL_cs addss !simpset) 1);
    1.67  by (strip_tac 1);
    1.68  by (rename_tac "s1 t1' n1'" 1);
    1.69  by (eres_inst_tac [("x","a")] allE 1);
    1.70 @@ -54,70 +49,64 @@
    1.71  by (eres_inst_tac [("x","s2'")] allE 1);
    1.72  by (eres_inst_tac [("x","t2")] allE 1);
    1.73  by (eres_inst_tac [("x","n2")] allE 1);
    1.74 -
    1.75  by (rtac conjI 1);
    1.76 -by (strip_tac 1);
    1.77 -by (mp_tac 1);
    1.78 -by (mp_tac 1);
    1.79 -by (etac exE 1);
    1.80 -by (etac conjE 1);
    1.81 -by (etac impE 1);
    1.82 -by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
    1.83 -by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
    1.84 -by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
    1.85 -    addss !simpset) 1);
    1.86 -by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel])) 1);
    1.87 -
    1.88 + by (strip_tac 1);
    1.89 + by (mp_tac 1);
    1.90 + by (mp_tac 1);
    1.91 + by (etac exE 1);
    1.92 + by (etac conjE 1);
    1.93 + by (etac impE 1);
    1.94 +  by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
    1.95 +  by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
    1.96 +  by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
    1.97 +                       addss !simpset) 1);
    1.98 + by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel])) 1);
    1.99  by (strip_tac 1);
   1.100  by (rename_tac "s2 t2' n2'" 1);
   1.101  by (rtac conjI 1);
   1.102 + by (strip_tac 1);
   1.103 + by (mp_tac 1);
   1.104 + by (mp_tac 1);
   1.105 + by (etac exE 1);
   1.106 + by (etac conjE 1);
   1.107 + by (etac impE 1);
   1.108 +  by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
   1.109 +  by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
   1.110 +  by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
   1.111 +                       addss !simpset) 1);
   1.112 + by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel,subst_comp_te])) 1);
   1.113  by (strip_tac 1);
   1.114  by (mp_tac 1);
   1.115  by (mp_tac 1);
   1.116  by (etac exE 1);
   1.117  by (etac conjE 1);
   1.118  by (etac impE 1);
   1.119 -by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
   1.120 -by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
   1.121 -by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
   1.122 -    addss !simpset) 1);
   1.123 -by (fast_tac (HOL_cs addss (!simpset addsimps [subst_comp_tel,subst_comp_te])) 1);
   1.124 -
   1.125 -by (strip_tac 1);
   1.126 -by (mp_tac 1);
   1.127 -by (mp_tac 1);
   1.128 -by (etac exE 1);
   1.129 -by (etac conjE 1);
   1.130 -by (etac impE 1);
   1.131 -by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
   1.132 -by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
   1.133 -by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
   1.134 -    addss !simpset) 1);
   1.135 -
   1.136 + by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); 
   1.137 + by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
   1.138 + by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
   1.139 +                      addss !simpset) 1);
   1.140  by (mp_tac 1);
   1.141  by (REPEAT (eresolve_tac [exE,conjE] 1));
   1.142 -by (REPEAT 
   1.143 -    ((asm_full_simp_tac (!simpset addsimps [subst_comp_tel,subst_comp_te]) 1) THEN
   1.144 -     (REPEAT (etac conjE 1)) THEN (hyp_subst_tac 1) ));
   1.145 +by (REPEAT(EVERY1
   1.146 +     [asm_full_simp_tac (!simpset addsimps [subst_comp_tel,subst_comp_te]),
   1.147 +      REPEAT o etac conjE, hyp_subst_tac]));
   1.148  by (rtac exI 1);
   1.149  by (safe_tac HOL_cs);
   1.150 -by (fast_tac HOL_cs 1);
   1.151 -by (Simp_tac 2);
   1.152 -
   1.153 +  by (fast_tac HOL_cs 1);
   1.154 + by (simp_tac (!simpset addsimps [o_def,subst_comp_te]) 2);
   1.155  by (subgoal_tac "new_tv n2 s & new_tv n2 r & new_tv n2 ra" 1);
   1.156 -by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
   1.157 + by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1);
   1.158  by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1));
   1.159  by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1));
   1.160  by (safe_tac HOL_cs);
   1.161 -by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
   1.162 -    addss !simpset) 1);
   1.163 -by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
   1.164 -    addss !simpset) 1);
   1.165 +  by (fast_tac (HOL_cs addDs[sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
   1.166 +                       addss !simpset) 1);
   1.167 + by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] 
   1.168 +                      addss !simpset) 1);
   1.169  by (dres_inst_tac [("e","expr1")] (sym RS W_var_geD) 1);
   1.170  by ((dtac new_tv_subst_tel 1) THEN (atac 1));
   1.171  by ((dres_inst_tac [("ts","$ s a")] new_tv_list_le 1) THEN (atac 1));
   1.172  by ((dtac new_tv_subst_tel 1) THEN (atac 1));
   1.173  by (fast_tac (HOL_cs addDs [new_tv_W] addss 
   1.174      (!simpset addsimps [subst_comp_tel])) 1);
   1.175 -
   1.176  qed_spec_mp "I_correct_wrt_W";
     2.1 --- a/src/HOL/MiniML/W.ML	Fri Apr 19 11:33:24 1996 +0200
     2.2 +++ b/src/HOL/MiniML/W.ML	Mon Apr 22 15:42:20 1996 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4  (* stronger version of Suc_leD *)
     2.5  goalw Nat.thy [le_def] 
     2.6          "!!m. Suc m <= n ==> m < n";
     2.7 -by (Asm_full_simp_tac 1);
     2.8 +by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
     2.9  by (cut_facts_tac [less_linear] 1);
    2.10  by (fast_tac HOL_cs 1);
    2.11  qed "Suc_le_lessD";
    2.12 @@ -42,7 +42,7 @@
    2.13  by (simp_tac (HOL_ss addsimps [subst_comp_tel RS sym]) 1);
    2.14  by ( (rtac has_type_cl_sub 1) THEN (rtac has_type_cl_sub 1));
    2.15  by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
    2.16 -by (asm_full_simp_tac (!simpset addsimps [subst_comp_tel RS sym,has_type_cl_sub,eq_sym_conv]) 1);
    2.17 +by (asm_full_simp_tac (!simpset addsimps [subst_comp_tel RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1);
    2.18  qed_spec_mp "W_correct";
    2.19  
    2.20  val has_type_casesE = map(has_type.mk_cases expr.simps)
    2.21 @@ -77,7 +77,7 @@
    2.22  by (etac conjE 1);
    2.23  by (res_inst_tac [("j","na")] le_trans 1); 
    2.24  by (Asm_simp_tac 1);
    2.25 -by (asm_simp_tac (!simpset addsimps [Suc_leD]) 1);
    2.26 +by (Asm_simp_tac 1);
    2.27  qed_spec_mp "W_var_ge";
    2.28  
    2.29  Addsimps [W_var_ge];
    2.30 @@ -128,7 +128,7 @@
    2.31  by (eres_inst_tac [("x","sa")] allE 1);
    2.32  by (eres_inst_tac [("x","ta")] allE 1);
    2.33  by (eres_inst_tac [("x","nb")] allE 1);
    2.34 -by( asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1);
    2.35 +by( asm_full_simp_tac (!simpset addsimps [o_def,rotate_Ok]) 1);
    2.36  by (rtac conjI 1);
    2.37  by (rtac new_tv_subst_comp_2 1);
    2.38  by (rtac new_tv_subst_comp_2 1);
    2.39 @@ -177,7 +177,8 @@
    2.40  by (eres_inst_tac [("x","t")] allE 1);
    2.41  by (eres_inst_tac [("x","na")] allE 1);
    2.42  by (eres_inst_tac [("x","v")] allE 1);
    2.43 -by (fast_tac (HOL_cs addIs [cod_app_subst] addss !simpset) 1);
    2.44 +by (fast_tac (HOL_cs addIs [cod_app_subst]
    2.45 +                     addss (!simpset addsimps [less_Suc_eq])) 1);
    2.46  
    2.47  (* case App e1 e2 *)
    2.48  by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
    2.49 @@ -197,7 +198,7 @@
    2.50  by (eres_inst_tac [("x","nb")] allE 1);
    2.51  by (eres_inst_tac [("x","v")] allE 1);
    2.52  by (safe_tac (empty_cs addSIs [conjI,impI] addSEs [conjE]) ); 
    2.53 -by (asm_full_simp_tac (!simpset addsimps [rotate_Ok]) 1);
    2.54 +by (asm_full_simp_tac (!simpset addsimps [rotate_Ok,o_def]) 1);
    2.55  by (dtac W_var_geD 1);
    2.56  by (dtac W_var_geD 1);
    2.57  by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) );