src/HOL/Nat.ML
author nipkow
Mon Jan 10 16:06:43 2000 +0100 (2000-01-10)
changeset 8115 c802042066e8
parent 7089 9bfb8e218b99
child 8260 87f21e25fcb6
permissions -rw-r--r--
Forgot to "call" MicroJava in makefile.
Added list_all2 to List.
     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) = (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 (*Useful in certain inductive arguments*)
    61 Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))";
    62 by (exhaust_tac "m" 1);
    63 by Auto_tac;
    64 qed "less_Suc_eq_0_disj";
    65 
    66 Goalw [Least_nat_def]
    67  "[| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
    68 by (rtac select_equality 1);
    69 by (fold_goals_tac [Least_nat_def]);
    70 by (safe_tac (claset() addSEs [LeastI]));
    71 by (rename_tac "j" 1);
    72 by (exhaust_tac "j" 1);
    73 by (Blast_tac 1);
    74 by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1);
    75 by (rename_tac "k n" 1);
    76 by (exhaust_tac "k" 1);
    77 by (Blast_tac 1);
    78 by (hyp_subst_tac 1);
    79 by (rewtac Least_nat_def);
    80 by (rtac (select_equality RS arg_cong RS sym) 1);
    81 by (blast_tac (claset() addDs [Suc_mono]) 1);
    82 by (cut_inst_tac [("m","m")] less_linear 1);
    83 by (blast_tac (claset() addIs [Suc_mono]) 1);
    84 qed "Least_Suc";
    85 
    86 val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
    87 by (rtac less_induct 1);
    88 by (exhaust_tac "n" 1);
    89 by (exhaust_tac "nat" 2);
    90 by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
    91 qed "nat_induct2";
    92 
    93 Goal "min 0 n = 0";
    94 by (rtac min_leastL 1);
    95 by (Simp_tac 1);
    96 qed "min_0L";
    97 
    98 Goal "min n 0 = 0";
    99 by (rtac min_leastR 1);
   100 by (Simp_tac 1);
   101 qed "min_0R";
   102 
   103 Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
   104 by (Simp_tac 1);
   105 qed "min_Suc_Suc";
   106 
   107 Addsimps [min_0L,min_0R,min_Suc_Suc];
   108 
   109 Goalw [max_def] "max 0 n = n";
   110 by (Simp_tac 1);
   111 qed "max_0L";
   112 
   113 Goalw [max_def] "max n 0 = n";
   114 by (Simp_tac 1);
   115 qed "max_0R";
   116 
   117 Goalw [max_def] "max (Suc m) (Suc n) = Suc(max m n)";
   118 by (Simp_tac 1);
   119 qed "max_Suc_Suc";
   120 
   121 Addsimps [max_0L,max_0R,max_Suc_Suc];