tidying, removing obsolete lemmas about 0=... and 1=...
authorpaulson
Wed Dec 20 12:14:26 2000 +0100 (2000-12-20)
changeset 107100c8d58332658
parent 10709 7a29b71d6352
child 10711 a9f6994fb906
tidying, removing obsolete lemmas about 0=... and 1=...
src/HOL/Integ/nat_bin.ML
src/HOL/Nat.ML
     1.1 --- a/src/HOL/Integ/nat_bin.ML	Wed Dec 20 12:13:59 2000 +0100
     1.2 +++ b/src/HOL/Integ/nat_bin.ML	Wed Dec 20 12:14:26 2000 +0100
     1.3 @@ -309,8 +309,7 @@
     1.4  
     1.5  AddIffs (map rename_numerals
     1.6  	 [Suc_not_Zero, Zero_not_Suc, zero_less_Suc, not_less0, less_one, 
     1.7 -	  le0, le_0_eq, 
     1.8 -	  neq0_conv, zero_neq_conv, not_gr0]);
     1.9 +	  le0, le_0_eq, neq0_conv, not_gr0]);
    1.10  
    1.11  (** Arith **)
    1.12  
    1.13 @@ -323,12 +322,12 @@
    1.14  (*Non-trivial simplifications*)	 
    1.15  val other_renamed_arith_simps =
    1.16      map rename_numerals
    1.17 -	[diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
    1.18 -	 mult_is_0, zero_is_mult, zero_less_mult_iff, mult_eq_1_iff];
    1.19 +	[diff_is_0_eq, zero_less_diff,
    1.20 +	 mult_is_0, zero_less_mult_iff, mult_eq_1_iff];
    1.21  
    1.22  Addsimps (basic_renamed_arith_simps @ other_renamed_arith_simps);
    1.23  
    1.24 -AddIffs (map rename_numerals [add_is_0, zero_is_add, add_gr_0]);
    1.25 +AddIffs (map rename_numerals [add_is_0, add_gr_0]);
    1.26  
    1.27  Goal "Suc n = n + #1";
    1.28  by (asm_simp_tac numeral_ss 1);
    1.29 @@ -359,7 +358,6 @@
    1.30  
    1.31  (*various theorems that aren't in the default simpset*)
    1.32  bind_thm ("add_is_one'", rename_numerals add_is_1);
    1.33 -bind_thm ("one_is_add'", rename_numerals one_is_add);
    1.34  bind_thm ("zero_induct'", rename_numerals zero_induct);
    1.35  bind_thm ("diff_self_eq_0'", rename_numerals diff_self_eq_0);
    1.36  bind_thm ("mult_eq_self_implies_10'", rename_numerals mult_eq_self_implies_10);
     2.1 --- a/src/HOL/Nat.ML	Wed Dec 20 12:13:59 2000 +0100
     2.2 +++ b/src/HOL/Nat.ML	Wed Dec 20 12:14:26 2000 +0100
     2.3 @@ -43,12 +43,6 @@
     2.4  qed "neq0_conv";
     2.5  AddIffs [neq0_conv];
     2.6  
     2.7 -Goal "!!n::nat. (0 ~= n) = (0 < n)";
     2.8 -by (case_tac "n" 1);
     2.9 -by Auto_tac;
    2.10 -qed "zero_neq_conv";
    2.11 -AddIffs [zero_neq_conv];
    2.12 -
    2.13  (*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
    2.14  bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
    2.15  
    2.16 @@ -235,22 +229,11 @@
    2.17  qed "add_is_0";
    2.18  AddIffs [add_is_0];
    2.19  
    2.20 -Goal "!!m::nat. (0 = m+n) = (m=0 & n=0)";
    2.21 -by (case_tac "m" 1);
    2.22 -by (Auto_tac);
    2.23 -qed "zero_is_add";
    2.24 -AddIffs [zero_is_add];
    2.25 -
    2.26  Goal "!!m::nat. (m+n=1) = (m=1 & n=0 | m=0 & n=1)";
    2.27  by (case_tac "m" 1);
    2.28  by (Auto_tac);
    2.29  qed "add_is_1";
    2.30  
    2.31 -Goal "!!m::nat. (1=m+n) = (m=1 & n=0 | m=0 & n=1)";
    2.32 -by (case_tac "m" 1);
    2.33 -by (Auto_tac);
    2.34 -qed "one_is_add";
    2.35 -
    2.36  Goal "!!m::nat. (0<m+n) = (0<m | 0<n)";
    2.37  by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
    2.38  qed "add_gr_0";
    2.39 @@ -445,13 +428,7 @@
    2.40  by (induct_tac "n" 2);
    2.41  by (ALLGOALS Asm_simp_tac);
    2.42  qed "mult_is_0";
    2.43 -
    2.44 -Goal "!!m::nat. (0 = m*n) = (0=m | 0=n)";
    2.45 -by (stac eq_commute 1 THEN stac mult_is_0 1);
    2.46 -by Auto_tac;
    2.47 -qed "zero_is_mult";
    2.48 -
    2.49 -Addsimps [mult_is_0, zero_is_mult];
    2.50 +Addsimps [mult_is_0];
    2.51  
    2.52  
    2.53  (*** Difference ***)
    2.54 @@ -552,12 +529,7 @@
    2.55  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    2.56  by (ALLGOALS Asm_simp_tac);
    2.57  qed "diff_is_0_eq";
    2.58 -
    2.59 -Goal "!!m::nat. (0 = m-n) = (m <= n)";
    2.60 -by (stac (diff_is_0_eq RS sym) 1);
    2.61 -by (rtac eq_sym_conv 1);
    2.62 -qed "zero_is_diff_eq";
    2.63 -Addsimps [diff_is_0_eq, zero_is_diff_eq];
    2.64 +Addsimps [diff_is_0_eq];
    2.65  
    2.66  Goal "!!m::nat. (0<n-m) = (m<n)";
    2.67  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);