src/HOL/Nat.ML
author nipkow
Wed Oct 14 11:50:48 1998 +0200 (1998-10-14)
changeset 5644 85fd64148873
parent 5316 7a8975451a89
child 5983 79e301a6a51b
permissions -rw-r--r--
Nat: added zero_neq_conv
List: added nth/update lemmas.
     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 Addsimps [not_gr0];
    56 
    57 Goal "m<n ==> 0 < n";
    58 by (dtac gr_implies_not0 1);
    59 by (Asm_full_simp_tac 1);
    60 qed "gr_implies_gr0";
    61 Addsimps [gr_implies_gr0];
    62 
    63 qed_goalw "Least_Suc" thy [Least_nat_def]
    64  "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
    65  (fn _ => [
    66         rtac select_equality 1,
    67         fold_goals_tac [Least_nat_def],
    68         safe_tac (claset() addSEs [LeastI]),
    69         rename_tac "j" 1,
    70         exhaust_tac "j" 1,
    71         Blast_tac 1,
    72         blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1,
    73         rename_tac "k n" 1,
    74         exhaust_tac "k" 1,
    75         Blast_tac 1,
    76         hyp_subst_tac 1,
    77         rewtac Least_nat_def,
    78         rtac (select_equality RS arg_cong RS sym) 1,
    79         Safe_tac,
    80         dtac Suc_mono 1,
    81         Blast_tac 1,
    82         cut_facts_tac [less_linear] 1,
    83         Safe_tac,
    84         atac 2,
    85         Blast_tac 2,
    86         dtac Suc_mono 1,
    87         Blast_tac 1]);
    88 
    89 qed_goal "nat_induct2" thy 
    90 "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [
    91         cut_facts_tac prems 1,
    92         rtac less_induct 1,
    93         exhaust_tac "n" 1,
    94          hyp_subst_tac 1,
    95          atac 1,
    96         hyp_subst_tac 1,
    97         exhaust_tac "nat" 1,
    98          hyp_subst_tac 1,
    99          atac 1,
   100         hyp_subst_tac 1,
   101         resolve_tac prems 1,
   102         dtac spec 1,
   103         etac mp 1,
   104         rtac (lessI RS less_trans) 1,
   105         rtac (lessI RS Suc_mono) 1]);
   106 
   107 Goal "min 0 n = 0";
   108 by (rtac min_leastL 1);
   109 by (trans_tac 1);
   110 qed "min_0L";
   111 
   112 Goal "min n 0 = 0";
   113 by (rtac min_leastR 1);
   114 by (trans_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];