src/HOL/Nat.ML
changeset 1660 8cb42cd97579
parent 1618 372880456b5b
child 1672 2c109cd2fdd0
     1.1 --- a/src/HOL/Nat.ML	Wed Apr 17 11:46:10 1996 +0200
     1.2 +++ b/src/HOL/Nat.ML	Wed Apr 17 17:59:58 1996 +0200
     1.3 @@ -291,6 +291,14 @@
     1.4  qed "gr_implies_not0";
     1.5  Addsimps [gr_implies_not0];
     1.6  
     1.7 +qed_goal "zero_less_eq" Nat.thy "0 < n = (n ~= 0)" (fn _ => [
     1.8 +	rtac iffI 1,
     1.9 +	etac gr_implies_not0 1,
    1.10 +	rtac natE 1,
    1.11 +	contr_tac 1,
    1.12 +	etac ssubst 1,
    1.13 +	rtac zero_less_Suc 1]);
    1.14 +
    1.15  (** Inductive (?) properties **)
    1.16  
    1.17  val [prem] = goal Nat.thy "Suc(m) < n ==> m<n";
    1.18 @@ -341,7 +349,8 @@
    1.19  
    1.20  goal Nat.thy "!!i. i<j ==> j<k --> Suc i < k";
    1.21  by (nat_ind_tac "k" 1);
    1.22 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
    1.23 +by (ALLGOALS (asm_simp_tac (!simpset)));
    1.24 +by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    1.25  by (fast_tac (HOL_cs addDs [Suc_lessD]) 1);
    1.26  qed_spec_mp "less_trans_Suc";
    1.27  
    1.28 @@ -354,6 +363,17 @@
    1.29  by (fast_tac (HOL_cs addIs [lessI, Suc_mono, less_SucI] addEs [lessE]) 1);
    1.30  qed "less_linear";
    1.31  
    1.32 +qed_goal "nat_less_cases" Nat.thy 
    1.33 +   "[| (m::nat)<n ==> P n m; m=n ==> P n m; n<m ==> P n m |] ==> P n m"
    1.34 +( fn prems =>
    1.35 +        [
    1.36 +        (res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1),
    1.37 +        (etac disjE 2),
    1.38 +        (etac (hd (tl (tl prems))) 1),
    1.39 +        (etac (sym RS hd (tl prems)) 1),
    1.40 +        (etac (hd prems) 1)
    1.41 +        ]);
    1.42 +
    1.43  (*Can be used with less_Suc_eq to get n=m | n<m *)
    1.44  goal Nat.thy "(~ m < n) = (n < Suc(m))";
    1.45  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.46 @@ -384,7 +404,7 @@
    1.47  qed "le_0";
    1.48  
    1.49  Addsimps [less_not_refl,
    1.50 -          less_Suc_eq, le0, le_0,
    1.51 +          (*less_Suc_eq,*) le0, le_0,
    1.52            Suc_Suc_eq, Suc_n_not_le_n,
    1.53            n_not_Suc_n, Suc_n_not_n,
    1.54            nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
    1.55 @@ -417,12 +437,12 @@
    1.56  qed "not_leE";
    1.57  
    1.58  goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n";
    1.59 -by (Simp_tac 1);
    1.60 +by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    1.61  by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1);
    1.62  qed "lessD";
    1.63  
    1.64  goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
    1.65 -by (Asm_full_simp_tac 1);
    1.66 +by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    1.67  by (fast_tac HOL_cs 1);
    1.68  qed "Suc_leD";
    1.69  
    1.70 @@ -519,3 +539,28 @@
    1.71  by (etac (rewrite_rule [le_def] Least_le RS notE) 1);
    1.72  by (rtac prem 1);
    1.73  qed "not_less_Least";
    1.74 +
    1.75 +qed_goalw "Least_Suc" Nat.thy [Least_def]
    1.76 + "[| ? n. P (Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P (Suc m))"
    1.77 + (fn prems => [
    1.78 +	cut_facts_tac prems 1,
    1.79 +	rtac select_equality 1,
    1.80 +	fold_goals_tac [Least_def],
    1.81 +	safe_tac (HOL_cs addSEs [LeastI]),
    1.82 +	res_inst_tac [("n","j")] natE 1,
    1.83 +	fast_tac HOL_cs 1,
    1.84 +	fast_tac (HOL_cs addDs [Suc_less_SucD] addDs [not_less_Least]) 1,	
    1.85 +	res_inst_tac [("n","k")] natE 1,
    1.86 +	fast_tac HOL_cs 1,
    1.87 +	hyp_subst_tac 1,
    1.88 +	rewtac Least_def,
    1.89 +	rtac (select_equality RS arg_cong RS sym) 1,
    1.90 +	safe_tac HOL_cs,
    1.91 +	dtac Suc_mono 1,
    1.92 +	fast_tac HOL_cs 1,
    1.93 +	cut_facts_tac [less_linear] 1,
    1.94 +	safe_tac HOL_cs,
    1.95 +	atac 2,
    1.96 +	fast_tac HOL_cs 2,
    1.97 +	dtac Suc_mono 1,
    1.98 +	fast_tac HOL_cs 1]);