src/HOL/Nat.ML
author berghofe
Fri Jul 24 13:34:59 1998 +0200 (1998-07-24)
changeset 5188 633ec5f6c155
parent 5069 3ea049f7979d
child 5316 7a8975451a89
permissions -rw-r--r--
Declaration of type 'nat' as a datatype (this allows usage of
exhaust_tac and induct_tac on type 'nat'). Moved some proofs
using natE from NatDef.ML to Nat.ML.
oheimb@2441
     1
(*  Title:      HOL/Nat.ML
clasohm@923
     2
    ID:         $Id$
nipkow@2608
     3
    Author:     Tobias Nipkow
nipkow@2608
     4
    Copyright   1997 TU Muenchen
clasohm@923
     5
*)
clasohm@923
     6
berghofe@5188
     7
(** conversion rules for nat_rec **)
berghofe@5188
     8
berghofe@5188
     9
val [nat_rec_0, nat_rec_Suc] = nat.recs;
berghofe@5188
    10
berghofe@5188
    11
(*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
berghofe@5188
    12
val prems = goal thy
berghofe@5188
    13
    "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
berghofe@5188
    14
by (simp_tac (simpset() addsimps prems) 1);
berghofe@5188
    15
qed "def_nat_rec_0";
berghofe@5188
    16
berghofe@5188
    17
val prems = goal thy
berghofe@5188
    18
    "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
berghofe@5188
    19
by (simp_tac (simpset() addsimps prems) 1);
berghofe@5188
    20
qed "def_nat_rec_Suc";
berghofe@5188
    21
berghofe@5188
    22
val [nat_case_0, nat_case_Suc] = nat.cases;
berghofe@5188
    23
berghofe@5188
    24
Goal "n ~= 0 ==> EX m. n = Suc m";
berghofe@5188
    25
by (exhaust_tac "n" 1);
berghofe@5188
    26
by (REPEAT (Blast_tac 1));
berghofe@5188
    27
qed "not0_implies_Suc";
berghofe@5188
    28
berghofe@5188
    29
val prems = goal thy "m<n ==> n ~= 0";
berghofe@5188
    30
by (exhaust_tac "n" 1);
berghofe@5188
    31
by (cut_facts_tac prems 1);
berghofe@5188
    32
by (ALLGOALS Asm_full_simp_tac);
berghofe@5188
    33
qed "gr_implies_not0";
berghofe@5188
    34
berghofe@5188
    35
Goal "(n ~= 0) = (0 < n)";
berghofe@5188
    36
by (exhaust_tac "n" 1);
berghofe@5188
    37
by (Blast_tac 1);
berghofe@5188
    38
by (Blast_tac 1);
berghofe@5188
    39
qed "neq0_conv";
berghofe@5188
    40
AddIffs [neq0_conv];
berghofe@5188
    41
berghofe@5188
    42
(*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
berghofe@5188
    43
bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
berghofe@5188
    44
berghofe@5188
    45
Goal "(~(0 < n)) = (n=0)";
berghofe@5188
    46
by (rtac iffI 1);
berghofe@5188
    47
 by (etac swap 1);
berghofe@5188
    48
 by (ALLGOALS Asm_full_simp_tac);
berghofe@5188
    49
qed "not_gr0";
berghofe@5188
    50
Addsimps [not_gr0];
berghofe@5188
    51
berghofe@5188
    52
Goal "m<n ==> 0 < n";
berghofe@5188
    53
by (dtac gr_implies_not0 1);
berghofe@5188
    54
by (Asm_full_simp_tac 1);
berghofe@5188
    55
qed "gr_implies_gr0";
berghofe@5188
    56
Addsimps [gr_implies_gr0];
berghofe@5188
    57
berghofe@5188
    58
qed_goalw "Least_Suc" thy [Least_nat_def]
berghofe@5188
    59
 "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
berghofe@5188
    60
 (fn _ => [
berghofe@5188
    61
        rtac select_equality 1,
berghofe@5188
    62
        fold_goals_tac [Least_nat_def],
berghofe@5188
    63
        safe_tac (claset() addSEs [LeastI]),
berghofe@5188
    64
        rename_tac "j" 1,
berghofe@5188
    65
        exhaust_tac "j" 1,
berghofe@5188
    66
        Blast_tac 1,
berghofe@5188
    67
        blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1,
berghofe@5188
    68
        rename_tac "k n" 1,
berghofe@5188
    69
        exhaust_tac "k" 1,
berghofe@5188
    70
        Blast_tac 1,
berghofe@5188
    71
        hyp_subst_tac 1,
berghofe@5188
    72
        rewtac Least_nat_def,
berghofe@5188
    73
        rtac (select_equality RS arg_cong RS sym) 1,
berghofe@5188
    74
        Safe_tac,
berghofe@5188
    75
        dtac Suc_mono 1,
berghofe@5188
    76
        Blast_tac 1,
berghofe@5188
    77
        cut_facts_tac [less_linear] 1,
berghofe@5188
    78
        Safe_tac,
berghofe@5188
    79
        atac 2,
berghofe@5188
    80
        Blast_tac 2,
berghofe@5188
    81
        dtac Suc_mono 1,
berghofe@5188
    82
        Blast_tac 1]);
berghofe@5188
    83
berghofe@5188
    84
qed_goal "nat_induct2" thy 
berghofe@5188
    85
"[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [
berghofe@5188
    86
        cut_facts_tac prems 1,
berghofe@5188
    87
        rtac less_induct 1,
berghofe@5188
    88
        exhaust_tac "n" 1,
berghofe@5188
    89
         hyp_subst_tac 1,
berghofe@5188
    90
         atac 1,
berghofe@5188
    91
        hyp_subst_tac 1,
berghofe@5188
    92
        exhaust_tac "nat" 1,
berghofe@5188
    93
         hyp_subst_tac 1,
berghofe@5188
    94
         atac 1,
berghofe@5188
    95
        hyp_subst_tac 1,
berghofe@5188
    96
        resolve_tac prems 1,
berghofe@5188
    97
        dtac spec 1,
berghofe@5188
    98
        etac mp 1,
berghofe@5188
    99
        rtac (lessI RS less_trans) 1,
berghofe@5188
   100
        rtac (lessI RS Suc_mono) 1]);
berghofe@5188
   101
wenzelm@5069
   102
Goal "min 0 n = 0";
paulson@3023
   103
by (rtac min_leastL 1);
paulson@3023
   104
by (trans_tac 1);
nipkow@2608
   105
qed "min_0L";
nipkow@1301
   106
wenzelm@5069
   107
Goal "min n 0 = 0";
paulson@3023
   108
by (rtac min_leastR 1);
paulson@3023
   109
by (trans_tac 1);
nipkow@2608
   110
qed "min_0R";
clasohm@923
   111
wenzelm@5069
   112
Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
paulson@3023
   113
by (Simp_tac 1);
nipkow@2608
   114
qed "min_Suc_Suc";
oheimb@1660
   115
nipkow@2608
   116
Addsimps [min_0L,min_0R,min_Suc_Suc];