src/HOL/Nat.ML
author paulson
Wed Jul 21 15:23:18 1999 +0200 (1999-07-21)
changeset 7058 8dfea70eb6b7
parent 6805 52b13dfbe954
child 7089 9bfb8e218b99
permissions -rw-r--r--
removed 2 qed_goals
     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 (Blast_tac 1);
    37 by (Blast_tac 1);
    38 qed "neq0_conv";
    39 AddIffs [neq0_conv];
    40 
    41 Goal "(0 ~= n) = (0 < n)";
    42 by (exhaust_tac "n" 1);
    43 by (Auto_tac);
    44 qed "zero_neq_conv";
    45 AddIffs [zero_neq_conv];
    46 
    47 (*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
    48 bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
    49 
    50 Goal "(~(0 < n)) = (n=0)";
    51 by (rtac iffI 1);
    52  by (etac swap 1);
    53  by (ALLGOALS Asm_full_simp_tac);
    54 qed "not_gr0";
    55 AddIffs [not_gr0];
    56 
    57 (*Useful in certain inductive arguments*)
    58 Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))";
    59 by (exhaust_tac "m" 1);
    60 by Auto_tac;
    61 qed "less_Suc_eq_0_disj";
    62 
    63 Goalw [Least_nat_def]
    64  "[| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
    65 by (rtac select_equality 1);
    66 by (fold_goals_tac [Least_nat_def]);
    67 by (safe_tac (claset() addSEs [LeastI]));
    68 by (rename_tac "j" 1);
    69 by (exhaust_tac "j" 1);
    70 by (Blast_tac 1);
    71 by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1);
    72 by (rename_tac "k n" 1);
    73 by (exhaust_tac "k" 1);
    74 by (Blast_tac 1);
    75 by (hyp_subst_tac 1);
    76 by (rewtac Least_nat_def);
    77 by (rtac (select_equality RS arg_cong RS sym) 1);
    78 by (Safe_tac);
    79 by (dtac Suc_mono 1);
    80 by (Blast_tac 1);
    81 by (cut_facts_tac [less_linear] 1);
    82 by (Safe_tac);
    83 by (atac 2);
    84 by (Blast_tac 2);
    85 by (dtac Suc_mono 1);
    86 by (Blast_tac 1);
    87 qed "Least_Suc";
    88 
    89 val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
    90 by (cut_facts_tac prems 1);
    91 by (rtac less_induct 1);
    92 by (exhaust_tac "n" 1);
    93 by (hyp_subst_tac 1);
    94 by (atac 1);
    95 by (hyp_subst_tac 1);
    96 by (exhaust_tac "nat" 1);
    97 by (hyp_subst_tac 1);
    98 by (atac 1);
    99 by (hyp_subst_tac 1);
   100 by (resolve_tac prems 1);
   101 by (dtac spec 1);
   102 by (etac mp 1);
   103 by (rtac (lessI RS less_trans) 1);
   104 by (rtac (lessI RS Suc_mono) 1);
   105 qed "nat_induct2";
   106 
   107 Goal "min 0 n = 0";
   108 by (rtac min_leastL 1);
   109 by (Simp_tac 1);
   110 qed "min_0L";
   111 
   112 Goal "min n 0 = 0";
   113 by (rtac min_leastR 1);
   114 by (Simp_tac 1);
   115 qed "min_0R";
   116 
   117 Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
   118 by (Simp_tac 1);
   119 qed "min_Suc_Suc";
   120 
   121 Addsimps [min_0L,min_0R,min_Suc_Suc];
   122 
   123 Goalw [max_def] "max 0 n = n";
   124 by (Simp_tac 1);
   125 qed "max_0L";
   126 
   127 Goalw [max_def] "max n 0 = n";
   128 by (Simp_tac 1);
   129 qed "max_0R";
   130 
   131 Goalw [max_def] "max (Suc m) (Suc n) = Suc(max m n)";
   132 by (Simp_tac 1);
   133 qed "max_Suc_Suc";
   134 
   135 Addsimps [max_0L,max_0R,max_Suc_Suc];