src/HOL/Nat.ML
author paulson
Tue Jul 27 17:19:31 1999 +0200 (1999-07-27)
changeset 7089 9bfb8e218b99
parent 7058 8dfea70eb6b7
child 8115 c802042066e8
permissions -rw-r--r--
expandshort and tidying
     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 (exhaust_tac "n" 1);
    26 by (REPEAT (Blast_tac 1));
    27 qed "not0_implies_Suc";
    28 
    29 Goal "m<n ==> n ~= 0";
    30 by (exhaust_tac "n" 1);
    31 by (ALLGOALS Asm_full_simp_tac);
    32 qed "gr_implies_not0";
    33 
    34 Goal "(n ~= 0) = (0 < n)";
    35 by (exhaust_tac "n" 1);
    36 by Auto_tac;
    37 qed "neq0_conv";
    38 AddIffs [neq0_conv];
    39 
    40 Goal "(0 ~= n) = (0 < n)";
    41 by (exhaust_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)) = (n=0)";
    50 by (rtac iffI 1);
    51  by (etac swap 1);
    52  by (ALLGOALS Asm_full_simp_tac);
    53 qed "not_gr0";
    54 AddIffs [not_gr0];
    55 
    56 (*Useful in certain inductive arguments*)
    57 Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))";
    58 by (exhaust_tac "m" 1);
    59 by Auto_tac;
    60 qed "less_Suc_eq_0_disj";
    61 
    62 Goalw [Least_nat_def]
    63  "[| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
    64 by (rtac select_equality 1);
    65 by (fold_goals_tac [Least_nat_def]);
    66 by (safe_tac (claset() addSEs [LeastI]));
    67 by (rename_tac "j" 1);
    68 by (exhaust_tac "j" 1);
    69 by (Blast_tac 1);
    70 by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1);
    71 by (rename_tac "k n" 1);
    72 by (exhaust_tac "k" 1);
    73 by (Blast_tac 1);
    74 by (hyp_subst_tac 1);
    75 by (rewtac Least_nat_def);
    76 by (rtac (select_equality RS arg_cong RS sym) 1);
    77 by (blast_tac (claset() addDs [Suc_mono]) 1);
    78 by (cut_inst_tac [("m","m")] less_linear 1);
    79 by (blast_tac (claset() addIs [Suc_mono]) 1);
    80 qed "Least_Suc";
    81 
    82 val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
    83 by (rtac less_induct 1);
    84 by (exhaust_tac "n" 1);
    85 by (exhaust_tac "nat" 2);
    86 by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
    87 qed "nat_induct2";
    88 
    89 Goal "min 0 n = 0";
    90 by (rtac min_leastL 1);
    91 by (Simp_tac 1);
    92 qed "min_0L";
    93 
    94 Goal "min n 0 = 0";
    95 by (rtac min_leastR 1);
    96 by (Simp_tac 1);
    97 qed "min_0R";
    98 
    99 Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
   100 by (Simp_tac 1);
   101 qed "min_Suc_Suc";
   102 
   103 Addsimps [min_0L,min_0R,min_Suc_Suc];
   104 
   105 Goalw [max_def] "max 0 n = n";
   106 by (Simp_tac 1);
   107 qed "max_0L";
   108 
   109 Goalw [max_def] "max n 0 = n";
   110 by (Simp_tac 1);
   111 qed "max_0R";
   112 
   113 Goalw [max_def] "max (Suc m) (Suc n) = Suc(max m n)";
   114 by (Simp_tac 1);
   115 qed "max_Suc_Suc";
   116 
   117 Addsimps [max_0L,max_0R,max_Suc_Suc];