Simplified a few proofs because of improved simplification.
authornipkow
Wed Jul 23 17:44:15 1997 +0200 (1997-07-23)
changeset 35694467015d5080
parent 3568 36ff1ab12021
child 3570 d3662f90c453
Simplified a few proofs because of improved simplification.
src/HOL/W0/I.ML
src/HOL/W0/W.ML
     1.1 --- a/src/HOL/W0/I.ML	Wed Jul 23 17:43:42 1997 +0200
     1.2 +++ b/src/HOL/W0/I.ML	Wed Jul 23 17:44:15 1997 +0200
     1.3 @@ -98,7 +98,7 @@
     1.4  by (mp_tac 1);
     1.5  by (REPEAT (eresolve_tac [exE,conjE] 1));
     1.6  by (REPEAT(EVERY1
     1.7 -     [asm_full_simp_tac (!simpset addsimps [subst_comp_tel,subst_comp_te]),
     1.8 +     [asm_full_simp_tac (!simpset addsimps [subst_comp_tel,subst_comp_te,o_def]),
     1.9        REPEAT o etac conjE, hyp_subst_tac]));
    1.10  (** LEVEL 70 **)
    1.11  by (subgoal_tac "new_tv n2 s & new_tv n2 r & new_tv n2 ra" 1);
    1.12 @@ -139,6 +139,8 @@
    1.13  
    1.14  val lemma = I_correct_wrt_W COMP swap_prems_rl;
    1.15  
    1.16 +Addsimps [split_paired_Ex];
    1.17 +
    1.18  goal I.thy "!a m s. \
    1.19  \  new_tv m a & new_tv m s --> I e a m s = Fail --> W e ($s a) m = Fail";
    1.20  by (expr.induct_tac "e" 1);
    1.21 @@ -146,35 +148,28 @@
    1.22                          setloop (split_tac [expand_if])) 1);
    1.23   by (Simp_tac 1);
    1.24   by (strip_tac 1);
    1.25 - by (rtac conjI 1);
    1.26 -  by (strip_tac 1);
    1.27 -  by (subgoal_tac "TVar m # $ s a = $s(TVar m # a)" 1);
    1.28 -   by (asm_simp_tac (HOL_ss addsimps
    1.29 + by (subgoal_tac "TVar m # $ s a = $s(TVar m # a)" 1);
    1.30 +  by (asm_simp_tac (HOL_ss addsimps
    1.31          [new_tv_Suc_list, lessI RS less_imp_le RS new_tv_subst_le]) 1);
    1.32 -  by (etac conjE 1);
    1.33 -  by (dtac (new_tv_not_free_tv RS not_free_impl_id) 1);
    1.34 -  by (Asm_simp_tac 1);
    1.35 - by (strip_tac 1);
    1.36 - by (etac exE 1);
    1.37 - by (split_all_tac 1);
    1.38 - by (Full_simp_tac 1);
    1.39 -(** LEVEL 15 **)
    1.40 + by (etac conjE 1);
    1.41 + by (dtac (new_tv_not_free_tv RS not_free_impl_id) 1);
    1.42 + by (Asm_simp_tac 1);
    1.43 +(** LEVEL 9 **)
    1.44  by (Asm_simp_tac 1);
    1.45  by (strip_tac 1);
    1.46 -by (etac exE 1);
    1.47 +by (REPEAT(etac exE 1));
    1.48  by (REPEAT(etac conjE 1));
    1.49 -by (split_all_tac 1);
    1.50 -by (Full_simp_tac 1);
    1.51  by (dtac lemma 1);
    1.52   by (fast_tac HOL_cs 1);
    1.53 -(** LEVEL 23 **)
    1.54 +(** LEVEL 15 **)
    1.55  by (etac exE 1);
    1.56  by (etac conjE 1);
    1.57  by (hyp_subst_tac 1);
    1.58  by (Asm_simp_tac 1);
    1.59 +by (REPEAT(resolve_tac [exI,conjI,refl] 1));
    1.60  by (etac disjE 1);
    1.61   by (rtac disjI1 1);
    1.62 -(** LEVEL 29 **)
    1.63 +(** LEVEL 22 **)
    1.64   by (full_simp_tac (!simpset addsimps [o_def,subst_comp_tel]) 1);
    1.65   by (EVERY[etac allE 1, etac allE 1, etac allE 1,
    1.66            etac impE 1, etac impE 2, atac 2, atac 2]);
    1.67 @@ -184,21 +179,19 @@
    1.68    by (fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1);
    1.69   by (fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1);
    1.70  by (rtac disjI2 1);
    1.71 -by (etac exE 1);
    1.72 -by (split_all_tac 1);
    1.73 +by (REPEAT(etac exE 1));
    1.74  by (etac conjE 1);
    1.75 -(** LEVEL 40 **)
    1.76 -by (Full_simp_tac 1);
    1.77 +(** LEVEL 32 **)
    1.78  by (dtac lemma 1);
    1.79   by (rtac conjI 1);
    1.80    by (fast_tac (HOL_cs addIs [W_var_ge RS new_tv_list_le]) 1);
    1.81   by (rtac new_tv_subst_comp_1 1);
    1.82 -   by (fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1);
    1.83 +  by (fast_tac (HOL_cs addIs [W_var_ge RS new_tv_subst_le]) 1);
    1.84   by (fast_tac (HOL_cs addSIs [new_tv_subst_tel]addIs[new_tv_W RS conjunct1])1);
    1.85  by (etac exE 1);
    1.86  by (etac conjE 1);
    1.87  by (hyp_subst_tac 1);
    1.88 -(** LEVEL 50 **)
    1.89 +(** LEVEL 41 **)
    1.90  by (asm_full_simp_tac (!simpset addsimps
    1.91       [o_def,subst_comp_te RS sym,subst_comp_tel RS sym]) 1);
    1.92  qed_spec_mp "I_complete_wrt_W";
     2.1 --- a/src/HOL/W0/W.ML	Wed Jul 23 17:43:42 1997 +0200
     2.2 +++ b/src/HOL/W0/W.ML	Wed Jul 23 17:44:15 1997 +0200
     2.3 @@ -230,9 +230,6 @@
     2.4                setloop (split_tac [expand_if])) 1);
     2.5  by (eresolve_tac has_type_casesE 1); 
     2.6  by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv,app_subst_list]) 1);
     2.7 -by (res_inst_tac [("x","id_subst")] exI 1);
     2.8 -by (res_inst_tac [("x","nth nat a")] exI 1);
     2.9 -by (Simp_tac 1);
    2.10  by (res_inst_tac [("x","s'")] exI 1);
    2.11  by (Asm_simp_tac 1);
    2.12  
    2.13 @@ -337,9 +334,6 @@
    2.14  by (safe_tac HOL_cs);
    2.15  by (dtac mgu_Ok 1);
    2.16  by ( fast_tac (HOL_cs addss !simpset) 1);
    2.17 -by (REPEAT (resolve_tac [exI,conjI] 1));
    2.18 -by (fast_tac HOL_cs 1);
    2.19 -by (fast_tac HOL_cs 1);
    2.20  by ((dtac mgu_mg 1) THEN (atac 1));
    2.21  by (etac exE 1);
    2.22  by (res_inst_tac [("x","rb")] exI 1);