added type constraint ::nat because 0 is now overloaded
authorpaulson
Tue May 23 18:28:11 2000 +0200 (2000-05-23)
changeset 89426aad5381ba83
parent 8941 df06883c1dcf
child 8943 a4f8be72f585
added type constraint ::nat because 0 is now overloaded
src/HOL/Nat.ML
src/HOL/NatDef.ML
     1.1 --- a/src/HOL/Nat.ML	Tue May 23 18:24:48 2000 +0200
     1.2 +++ b/src/HOL/Nat.ML	Tue May 23 18:28:11 2000 +0200
     1.3 @@ -26,18 +26,18 @@
     1.4  by (REPEAT (Blast_tac 1));
     1.5  qed "not0_implies_Suc";
     1.6  
     1.7 -Goal "m<n ==> n ~= 0";
     1.8 +Goal "!!n::nat. m<n ==> n ~= 0";
     1.9  by (case_tac "n" 1);
    1.10  by (ALLGOALS Asm_full_simp_tac);
    1.11  qed "gr_implies_not0";
    1.12  
    1.13 -Goal "(n ~= 0) = (0 < n)";
    1.14 +Goal "!!n::nat. (n ~= 0) = (0 < n)";
    1.15  by (case_tac "n" 1);
    1.16  by Auto_tac;
    1.17  qed "neq0_conv";
    1.18  AddIffs [neq0_conv];
    1.19  
    1.20 -Goal "(0 ~= n) = (0 < n)";
    1.21 +Goal "!!n::nat. (0 ~= n) = (0 < n)";
    1.22  by (case_tac "n" 1);
    1.23  by Auto_tac;
    1.24  qed "zero_neq_conv";
    1.25 @@ -50,7 +50,7 @@
    1.26  by(fast_tac (claset() addIs [not0_implies_Suc]) 1);
    1.27  qed "gr0_conv_Suc";
    1.28  
    1.29 -Goal "(~(0 < n)) = (n=0)";
    1.30 +Goal "!!n::nat. (~(0 < n)) = (n=0)";
    1.31  by (rtac iffI 1);
    1.32   by (etac swap 1);
    1.33   by (ALLGOALS Asm_full_simp_tac);
    1.34 @@ -95,12 +95,12 @@
    1.35  by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
    1.36  qed "nat_induct2";
    1.37  
    1.38 -Goal "min 0 n = 0";
    1.39 +Goal "min 0 n = (0::nat)";
    1.40  by (rtac min_leastL 1);
    1.41  by (Simp_tac 1);
    1.42  qed "min_0L";
    1.43  
    1.44 -Goal "min n 0 = 0";
    1.45 +Goal "min n 0 = (0::nat)";
    1.46  by (rtac min_leastR 1);
    1.47  by (Simp_tac 1);
    1.48  qed "min_0R";
    1.49 @@ -111,11 +111,11 @@
    1.50  
    1.51  Addsimps [min_0L,min_0R,min_Suc_Suc];
    1.52  
    1.53 -Goalw [max_def] "max 0 n = n";
    1.54 +Goalw [max_def] "max 0 n = (n::nat)";
    1.55  by (Simp_tac 1);
    1.56  qed "max_0L";
    1.57  
    1.58 -Goalw [max_def] "max n 0 = n";
    1.59 +Goalw [max_def] "max n 0 = (n::nat)";
    1.60  by (Simp_tac 1);
    1.61  qed "max_0R";
    1.62  
     2.1 --- a/src/HOL/NatDef.ML	Tue May 23 18:24:48 2000 +0200
     2.2 +++ b/src/HOL/NatDef.ML	Tue May 23 18:28:11 2000 +0200
     2.3 @@ -184,13 +184,9 @@
     2.4                    eresolve_tac (prems@[asm_rl, Pair_inject])));
     2.5  qed "lessE";
     2.6  
     2.7 -Goal "~ n<0";
     2.8 -by (rtac notI 1);
     2.9 -by (etac lessE 1);
    2.10 -by (etac Zero_neq_Suc 1);
    2.11 -by (etac Zero_neq_Suc 1);
    2.12 +Goal "~ n < (0::nat)";
    2.13 +by (blast_tac (claset() addEs [lessE]) 1);
    2.14  qed "not_less0";
    2.15 -
    2.16  AddIffs [not_less0];
    2.17  
    2.18  (* n<0 ==> R *)
    2.19 @@ -312,7 +308,7 @@
    2.20  (*  m<=n ==> m < Suc n  *)
    2.21  bind_thm ("le_imp_less_Suc", less_Suc_eq_le RS iffD2);
    2.22  
    2.23 -Goalw [le_def] "0 <= n";
    2.24 +Goalw [le_def] "(0::nat) <= n";
    2.25  by (rtac not_less0 1);
    2.26  qed "le0";
    2.27  AddIffs [le0];
    2.28 @@ -321,7 +317,7 @@
    2.29  by (Simp_tac 1);
    2.30  qed "Suc_n_not_le_n";
    2.31  
    2.32 -Goalw [le_def] "(i <= 0) = (i = 0)";
    2.33 +Goalw [le_def] "!!i::nat. (i <= 0) = (i = 0)";
    2.34  by (nat_ind_tac "i" 1);
    2.35  by (ALLGOALS Asm_simp_tac);
    2.36  qed "le_0_eq";