src/HOL/Nat.ML
changeset 5188 633ec5f6c155
parent 5069 3ea049f7979d
child 5316 7a8975451a89
     1.1 --- a/src/HOL/Nat.ML	Fri Jul 24 13:30:28 1998 +0200
     1.2 +++ b/src/HOL/Nat.ML	Fri Jul 24 13:34:59 1998 +0200
     1.3 @@ -4,6 +4,101 @@
     1.4      Copyright   1997 TU Muenchen
     1.5  *)
     1.6  
     1.7 +(** conversion rules for nat_rec **)
     1.8 +
     1.9 +val [nat_rec_0, nat_rec_Suc] = nat.recs;
    1.10 +
    1.11 +(*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
    1.12 +val prems = goal thy
    1.13 +    "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
    1.14 +by (simp_tac (simpset() addsimps prems) 1);
    1.15 +qed "def_nat_rec_0";
    1.16 +
    1.17 +val prems = goal thy
    1.18 +    "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
    1.19 +by (simp_tac (simpset() addsimps prems) 1);
    1.20 +qed "def_nat_rec_Suc";
    1.21 +
    1.22 +val [nat_case_0, nat_case_Suc] = nat.cases;
    1.23 +
    1.24 +Goal "n ~= 0 ==> EX m. n = Suc m";
    1.25 +by (exhaust_tac "n" 1);
    1.26 +by (REPEAT (Blast_tac 1));
    1.27 +qed "not0_implies_Suc";
    1.28 +
    1.29 +val prems = goal thy "m<n ==> n ~= 0";
    1.30 +by (exhaust_tac "n" 1);
    1.31 +by (cut_facts_tac prems 1);
    1.32 +by (ALLGOALS Asm_full_simp_tac);
    1.33 +qed "gr_implies_not0";
    1.34 +
    1.35 +Goal "(n ~= 0) = (0 < n)";
    1.36 +by (exhaust_tac "n" 1);
    1.37 +by (Blast_tac 1);
    1.38 +by (Blast_tac 1);
    1.39 +qed "neq0_conv";
    1.40 +AddIffs [neq0_conv];
    1.41 +
    1.42 +(*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
    1.43 +bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
    1.44 +
    1.45 +Goal "(~(0 < n)) = (n=0)";
    1.46 +by (rtac iffI 1);
    1.47 + by (etac swap 1);
    1.48 + by (ALLGOALS Asm_full_simp_tac);
    1.49 +qed "not_gr0";
    1.50 +Addsimps [not_gr0];
    1.51 +
    1.52 +Goal "m<n ==> 0 < n";
    1.53 +by (dtac gr_implies_not0 1);
    1.54 +by (Asm_full_simp_tac 1);
    1.55 +qed "gr_implies_gr0";
    1.56 +Addsimps [gr_implies_gr0];
    1.57 +
    1.58 +qed_goalw "Least_Suc" thy [Least_nat_def]
    1.59 + "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
    1.60 + (fn _ => [
    1.61 +        rtac select_equality 1,
    1.62 +        fold_goals_tac [Least_nat_def],
    1.63 +        safe_tac (claset() addSEs [LeastI]),
    1.64 +        rename_tac "j" 1,
    1.65 +        exhaust_tac "j" 1,
    1.66 +        Blast_tac 1,
    1.67 +        blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1,
    1.68 +        rename_tac "k n" 1,
    1.69 +        exhaust_tac "k" 1,
    1.70 +        Blast_tac 1,
    1.71 +        hyp_subst_tac 1,
    1.72 +        rewtac Least_nat_def,
    1.73 +        rtac (select_equality RS arg_cong RS sym) 1,
    1.74 +        Safe_tac,
    1.75 +        dtac Suc_mono 1,
    1.76 +        Blast_tac 1,
    1.77 +        cut_facts_tac [less_linear] 1,
    1.78 +        Safe_tac,
    1.79 +        atac 2,
    1.80 +        Blast_tac 2,
    1.81 +        dtac Suc_mono 1,
    1.82 +        Blast_tac 1]);
    1.83 +
    1.84 +qed_goal "nat_induct2" thy 
    1.85 +"[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [
    1.86 +        cut_facts_tac prems 1,
    1.87 +        rtac less_induct 1,
    1.88 +        exhaust_tac "n" 1,
    1.89 +         hyp_subst_tac 1,
    1.90 +         atac 1,
    1.91 +        hyp_subst_tac 1,
    1.92 +        exhaust_tac "nat" 1,
    1.93 +         hyp_subst_tac 1,
    1.94 +         atac 1,
    1.95 +        hyp_subst_tac 1,
    1.96 +        resolve_tac prems 1,
    1.97 +        dtac spec 1,
    1.98 +        etac mp 1,
    1.99 +        rtac (lessI RS less_trans) 1,
   1.100 +        rtac (lessI RS Suc_mono) 1]);
   1.101 +
   1.102  Goal "min 0 n = 0";
   1.103  by (rtac min_leastL 1);
   1.104  by (trans_tac 1);