Modified proofs because of added "triv_forall_equality".
authornipkow
Fri Feb 07 14:13:58 1997 +0100 (1997-02-07)
changeset 25963b4ad6c7726f
parent 2595 548f8ed89a80
child 2597 8b523426e1a4
Modified proofs because of added "triv_forall_equality".
src/HOL/Integ/Integ.ML
src/HOL/W0/W.ML
src/HOL/ex/LList.ML
     1.1 --- a/src/HOL/Integ/Integ.ML	Fri Feb 07 14:13:20 1997 +0100
     1.2 +++ b/src/HOL/Integ/Integ.ML	Fri Feb 07 14:13:58 1997 +0100
     1.3 @@ -577,11 +577,12 @@
     1.4  by (safe_tac (!claset));
     1.5  by (asm_full_simp_tac (!simpset addsimps [zadd, zminus]) 1);
     1.6  by (safe_tac (!claset addSDs [less_eq_Suc_add]));
     1.7 +by (rename_tac "k" 1);
     1.8  by (res_inst_tac [("x","k")] exI 1);
     1.9  by (asm_full_simp_tac (!simpset delsimps [add_Suc, add_Suc_right]
    1.10                                  addsimps ([add_Suc RS sym] @ add_ac)) 1);
    1.11  (*To cancel x2, rename it to be first!*)
    1.12 -by (rename_tac "a b c" 1);
    1.13 +by (rename_tac "a b" 1);
    1.14  by (asm_full_simp_tac (!simpset delsimps [add_Suc_right]
    1.15                                  addsimps (add_left_cancel::add_ac)) 1);
    1.16  qed "zless_eq_zadd_Suc";
     2.1 --- a/src/HOL/W0/W.ML	Fri Feb 07 14:13:20 1997 +0100
     2.2 +++ b/src/HOL/W0/W.ML	Fri Feb 07 14:13:58 1997 +0100
     2.3 @@ -219,7 +219,6 @@
     2.4  		     addss !simpset) 1); 
     2.5  qed_spec_mp "free_tv_W"; 
     2.6  
     2.7 -
     2.8  (* Completeness of W w.r.t. has_type *)
     2.9  goal thy
    2.10   "!s' a t' n. $s' a |- e :: t' --> new_tv n a -->     \
    2.11 @@ -347,9 +346,8 @@
    2.12  by (rtac conjI 1);
    2.13  by (dres_inst_tac [("x","ma")] fun_cong 2);
    2.14  by ( asm_full_simp_tac (!simpset addsimps [eq_sym_conv]) 2);
    2.15 -by (simp_tac (!simpset addsimps [subst_comp_tel RS sym]) 1);
    2.16 -by (res_inst_tac [("ts2","($ sa ($ s a))")] ((subst_comp_tel RS sym) RSN 
    2.17 -    (2,trans)) 1);
    2.18 +by (simp_tac (!simpset addsimps [o_def,subst_comp_tel RS sym]) 1);
    2.19 +by (rtac ((subst_comp_tel RS sym) RSN (2,trans)) 1);
    2.20  by ( asm_full_simp_tac (!simpset addsimps [o_def,eq_sym_conv]) 1);
    2.21  (** LEVEL 90 **)
    2.22  by (rtac eq_free_eq_subst_tel 1);
     3.1 --- a/src/HOL/ex/LList.ML	Fri Feb 07 14:13:20 1997 +0100
     3.2 +++ b/src/HOL/ex/LList.ML	Fri Feb 07 14:13:58 1997 +0100
     3.3 @@ -297,15 +297,19 @@
     3.4  \    !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
     3.5  \ ==> h1=h2";
     3.6  by (rtac (ntrunc_equality RS ext) 1);
     3.7 +by (rename_tac "x k" 1);
     3.8  by (res_inst_tac [("x", "x")] spec 1);
     3.9  by (res_inst_tac [("n", "k")] less_induct 1);
    3.10 +by (rename_tac "n" 1);
    3.11  by (rtac allI 1);
    3.12 +by (rename_tac "y" 1);
    3.13  by (stac prem1 1);
    3.14  by (stac prem2 1);
    3.15  by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
    3.16  by (strip_tac 1);
    3.17  by (res_inst_tac [("n", "n")] natE 1);
    3.18 -by (res_inst_tac [("n", "xb")] natE 2);
    3.19 +by (rename_tac "m" 2);
    3.20 +by (res_inst_tac [("n", "m")] natE 2);
    3.21  by (ALLGOALS(asm_simp_tac(!simpset addsimps
    3.22              [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS, less_Suc_eq])));
    3.23  result();