src/HOL/Nat.ML
author wenzelm
Mon Mar 13 16:23:34 2000 +0100 (2000-03-13)
changeset 8442 96023903c2df
parent 8423 3c19160b6432
child 8942 6aad5381ba83
permissions -rw-r--r--
case_tac now subsumes both boolean and datatype cases;
     1 (*  Title:      HOL/Nat.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1997 TU Muenchen
     5 *)
     6 
     7 (** conversion rules for nat_rec **)
     8 
     9 val [nat_rec_0, nat_rec_Suc] = nat.recs;
    10 
    11 (*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
    12 val prems = Goal
    13     "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
    14 by (simp_tac (simpset() addsimps prems) 1);
    15 qed "def_nat_rec_0";
    16 
    17 val prems = Goal
    18     "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
    19 by (simp_tac (simpset() addsimps prems) 1);
    20 qed "def_nat_rec_Suc";
    21 
    22 val [nat_case_0, nat_case_Suc] = nat.cases;
    23 
    24 Goal "n ~= 0 ==> EX m. n = Suc m";
    25 by (case_tac "n" 1);
    26 by (REPEAT (Blast_tac 1));
    27 qed "not0_implies_Suc";
    28 
    29 Goal "m<n ==> n ~= 0";
    30 by (case_tac "n" 1);
    31 by (ALLGOALS Asm_full_simp_tac);
    32 qed "gr_implies_not0";
    33 
    34 Goal "(n ~= 0) = (0 < n)";
    35 by (case_tac "n" 1);
    36 by Auto_tac;
    37 qed "neq0_conv";
    38 AddIffs [neq0_conv];
    39 
    40 Goal "(0 ~= n) = (0 < n)";
    41 by (case_tac "n" 1);
    42 by Auto_tac;
    43 qed "zero_neq_conv";
    44 AddIffs [zero_neq_conv];
    45 
    46 (*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
    47 bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
    48 
    49 Goal "(0<n) = (EX m. n = Suc m)";
    50 by(fast_tac (claset() addIs [not0_implies_Suc]) 1);
    51 qed "gr0_conv_Suc";
    52 
    53 Goal "(~(0 < n)) = (n=0)";
    54 by (rtac iffI 1);
    55  by (etac swap 1);
    56  by (ALLGOALS Asm_full_simp_tac);
    57 qed "not_gr0";
    58 AddIffs [not_gr0];
    59 
    60 Goal "(Suc n <= m') --> (? m. m' = Suc m)";
    61 by (induct_tac "m'" 1);
    62 by  Auto_tac;
    63 qed_spec_mp "Suc_le_D";
    64 
    65 (*Useful in certain inductive arguments*)
    66 Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))";
    67 by (case_tac "m" 1);
    68 by Auto_tac;
    69 qed "less_Suc_eq_0_disj";
    70 
    71 Goalw [Least_nat_def]
    72  "[| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
    73 by (rtac select_equality 1);
    74 by (fold_goals_tac [Least_nat_def]);
    75 by (safe_tac (claset() addSEs [LeastI]));
    76 by (rename_tac "j" 1);
    77 by (case_tac "j" 1);
    78 by (Blast_tac 1);
    79 by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1);
    80 by (rename_tac "k n" 1);
    81 by (case_tac "k" 1);
    82 by (Blast_tac 1);
    83 by (hyp_subst_tac 1);
    84 by (rewtac Least_nat_def);
    85 by (rtac (select_equality RS arg_cong RS sym) 1);
    86 by (blast_tac (claset() addDs [Suc_mono]) 1);
    87 by (cut_inst_tac [("m","m")] less_linear 1);
    88 by (blast_tac (claset() addIs [Suc_mono]) 1);
    89 qed "Least_Suc";
    90 
    91 val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
    92 by (rtac less_induct 1);
    93 by (case_tac "n" 1);
    94 by (case_tac "nat" 2);
    95 by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
    96 qed "nat_induct2";
    97 
    98 Goal "min 0 n = 0";
    99 by (rtac min_leastL 1);
   100 by (Simp_tac 1);
   101 qed "min_0L";
   102 
   103 Goal "min n 0 = 0";
   104 by (rtac min_leastR 1);
   105 by (Simp_tac 1);
   106 qed "min_0R";
   107 
   108 Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
   109 by (Simp_tac 1);
   110 qed "min_Suc_Suc";
   111 
   112 Addsimps [min_0L,min_0R,min_Suc_Suc];
   113 
   114 Goalw [max_def] "max 0 n = n";
   115 by (Simp_tac 1);
   116 qed "max_0L";
   117 
   118 Goalw [max_def] "max n 0 = n";
   119 by (Simp_tac 1);
   120 qed "max_0R";
   121 
   122 Goalw [max_def] "max (Suc m) (Suc n) = Suc(max m n)";
   123 by (Simp_tac 1);
   124 qed "max_Suc_Suc";
   125 
   126 Addsimps [max_0L,max_0R,max_Suc_Suc];