src/HOL/Nat.ML
changeset 11464 ddea204de5bc
parent 11337 9d6d6a8966b9
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/Nat.ML	Mon Aug 06 13:12:06 2001 +0200
     1.2 +++ b/src/HOL/Nat.ML	Mon Aug 06 13:43:24 2001 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4  by Auto_tac;
     1.5  qed "less_Suc_eq_0_disj";
     1.6  
     1.7 -val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
     1.8 +val prems = Goal "[| P 0; P(1'); !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
     1.9  by (rtac nat_less_induct 1);
    1.10  by (case_tac "n" 1);
    1.11  by (case_tac "nat" 2);
    1.12 @@ -157,7 +157,7 @@
    1.13  (* Could be (and is, below) generalized in various ways;
    1.14     However, none of the generalizations are currently in the simpset,
    1.15     and I dread to think what happens if I put them in *)
    1.16 -Goal "0 < n ==> Suc(n-1) = n";
    1.17 +Goal "0 < n ==> Suc(n-1') = n";
    1.18  by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
    1.19  qed "Suc_pred";
    1.20  Addsimps [Suc_pred];
    1.21 @@ -238,11 +238,16 @@
    1.22  qed "add_is_0";
    1.23  AddIffs [add_is_0];
    1.24  
    1.25 -Goal "!!m::nat. (m+n=1) = (m=1 & n=0 | m=0 & n=1)";
    1.26 +Goal "(m+n=1') = (m=1' & n=0 | m=0 & n=1')";
    1.27  by (case_tac "m" 1);
    1.28  by (Auto_tac);
    1.29  qed "add_is_1";
    1.30  
    1.31 +Goal "(1' = m+n) = (m=1' & n=0 | m=0 & n=1')";
    1.32 +by (case_tac "m" 1);
    1.33 +by (Auto_tac);
    1.34 +qed "one_is_add";
    1.35 +
    1.36  Goal "!!m::nat. (0<m+n) = (0<m | 0<n)";
    1.37  by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
    1.38  qed "add_gr_0";
    1.39 @@ -633,14 +638,14 @@
    1.40  qed "zero_less_mult_iff";
    1.41  Addsimps [zero_less_mult_iff];
    1.42  
    1.43 -Goal "(1 <= m*n) = (1<=m & 1<=n)";
    1.44 +Goal "(1' <= m*n) = (1<=m & 1<=n)";
    1.45  by (induct_tac "m" 1);
    1.46  by (case_tac "n" 2);
    1.47  by (ALLGOALS Asm_simp_tac);
    1.48  qed "one_le_mult_iff";
    1.49  Addsimps [one_le_mult_iff];
    1.50  
    1.51 -Goal "(m*n = 1) = (m=1 & n=1)";
    1.52 +Goal "(m*n = 1') = (m=1 & n=1)";
    1.53  by (induct_tac "m" 1);
    1.54  by (Simp_tac 1);
    1.55  by (induct_tac "n" 1);
    1.56 @@ -649,6 +654,12 @@
    1.57  qed "mult_eq_1_iff";
    1.58  Addsimps [mult_eq_1_iff];
    1.59  
    1.60 +Goal "(1' = m*n) = (m=1 & n=1)";
    1.61 +by(rtac (mult_eq_1_iff RSN (2,trans)) 1);
    1.62 +by (fast_tac (claset() addss simpset()) 1);
    1.63 +qed "one_eq_mult_iff";
    1.64 +Addsimps [one_eq_mult_iff];
    1.65 +
    1.66  Goal "!!m::nat. (m*k < n*k) = (0<k & m<n)";
    1.67  by (safe_tac (claset() addSIs [mult_less_mono1]));
    1.68  by (case_tac "k" 1);