src/HOL/Nat.ML
author wenzelm
Thu Jun 22 23:04:34 2000 +0200 (2000-06-22)
changeset 9108 9fff97d29837
parent 8942 6aad5381ba83
child 9436 62bb04ab4b01
permissions -rw-r--r--
bind_thm(s);
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;
wenzelm@9108
    10
bind_thm ("nat_rec_0", nat_rec_0);
wenzelm@9108
    11
bind_thm ("nat_rec_Suc", nat_rec_Suc);
berghofe@5188
    12
berghofe@5188
    13
(*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
paulson@5316
    14
val prems = Goal
berghofe@5188
    15
    "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
berghofe@5188
    16
by (simp_tac (simpset() addsimps prems) 1);
berghofe@5188
    17
qed "def_nat_rec_0";
berghofe@5188
    18
paulson@5316
    19
val prems = Goal
berghofe@5188
    20
    "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
berghofe@5188
    21
by (simp_tac (simpset() addsimps prems) 1);
berghofe@5188
    22
qed "def_nat_rec_Suc";
berghofe@5188
    23
berghofe@5188
    24
val [nat_case_0, nat_case_Suc] = nat.cases;
wenzelm@9108
    25
bind_thm ("nat_case_0", nat_case_0);
wenzelm@9108
    26
bind_thm ("nat_case_Suc", nat_case_Suc);
berghofe@5188
    27
berghofe@5188
    28
Goal "n ~= 0 ==> EX m. n = Suc m";
wenzelm@8442
    29
by (case_tac "n" 1);
berghofe@5188
    30
by (REPEAT (Blast_tac 1));
berghofe@5188
    31
qed "not0_implies_Suc";
berghofe@5188
    32
paulson@8942
    33
Goal "!!n::nat. m<n ==> n ~= 0";
wenzelm@8442
    34
by (case_tac "n" 1);
berghofe@5188
    35
by (ALLGOALS Asm_full_simp_tac);
berghofe@5188
    36
qed "gr_implies_not0";
berghofe@5188
    37
paulson@8942
    38
Goal "!!n::nat. (n ~= 0) = (0 < n)";
wenzelm@8442
    39
by (case_tac "n" 1);
paulson@7089
    40
by Auto_tac;
berghofe@5188
    41
qed "neq0_conv";
berghofe@5188
    42
AddIffs [neq0_conv];
berghofe@5188
    43
paulson@8942
    44
Goal "!!n::nat. (0 ~= n) = (0 < n)";
wenzelm@8442
    45
by (case_tac "n" 1);
paulson@7089
    46
by Auto_tac;
nipkow@5644
    47
qed "zero_neq_conv";
nipkow@5644
    48
AddIffs [zero_neq_conv];
nipkow@5644
    49
berghofe@5188
    50
(*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
berghofe@5188
    51
bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
berghofe@5188
    52
nipkow@8115
    53
Goal "(0<n) = (EX m. n = Suc m)";
nipkow@8115
    54
by(fast_tac (claset() addIs [not0_implies_Suc]) 1);
nipkow@8115
    55
qed "gr0_conv_Suc";
nipkow@8115
    56
paulson@8942
    57
Goal "!!n::nat. (~(0 < n)) = (n=0)";
berghofe@5188
    58
by (rtac iffI 1);
berghofe@5188
    59
 by (etac swap 1);
berghofe@5188
    60
 by (ALLGOALS Asm_full_simp_tac);
berghofe@5188
    61
qed "not_gr0";
nipkow@6109
    62
AddIffs [not_gr0];
berghofe@5188
    63
oheimb@8260
    64
Goal "(Suc n <= m') --> (? m. m' = Suc m)";
oheimb@8260
    65
by (induct_tac "m'" 1);
oheimb@8260
    66
by  Auto_tac;
oheimb@8260
    67
qed_spec_mp "Suc_le_D";
oheimb@8260
    68
paulson@6805
    69
(*Useful in certain inductive arguments*)
paulson@6805
    70
Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))";
wenzelm@8442
    71
by (case_tac "m" 1);
paulson@6805
    72
by Auto_tac;
paulson@6805
    73
qed "less_Suc_eq_0_disj";
paulson@6805
    74
paulson@7058
    75
Goalw [Least_nat_def]
paulson@7058
    76
 "[| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
paulson@7058
    77
by (rtac select_equality 1);
paulson@7058
    78
by (fold_goals_tac [Least_nat_def]);
paulson@7058
    79
by (safe_tac (claset() addSEs [LeastI]));
paulson@7058
    80
by (rename_tac "j" 1);
wenzelm@8442
    81
by (case_tac "j" 1);
paulson@7058
    82
by (Blast_tac 1);
paulson@7058
    83
by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1);
paulson@7058
    84
by (rename_tac "k n" 1);
wenzelm@8442
    85
by (case_tac "k" 1);
paulson@7058
    86
by (Blast_tac 1);
paulson@7058
    87
by (hyp_subst_tac 1);
paulson@7058
    88
by (rewtac Least_nat_def);
paulson@7058
    89
by (rtac (select_equality RS arg_cong RS sym) 1);
paulson@7089
    90
by (blast_tac (claset() addDs [Suc_mono]) 1);
paulson@7089
    91
by (cut_inst_tac [("m","m")] less_linear 1);
paulson@7089
    92
by (blast_tac (claset() addIs [Suc_mono]) 1);
paulson@7058
    93
qed "Least_Suc";
berghofe@5188
    94
paulson@7058
    95
val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
paulson@7058
    96
by (rtac less_induct 1);
wenzelm@8442
    97
by (case_tac "n" 1);
wenzelm@8442
    98
by (case_tac "nat" 2);
paulson@7089
    99
by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
paulson@7058
   100
qed "nat_induct2";
berghofe@5188
   101
paulson@8942
   102
Goal "min 0 n = (0::nat)";
paulson@3023
   103
by (rtac min_leastL 1);
nipkow@5983
   104
by (Simp_tac 1);
nipkow@2608
   105
qed "min_0L";
nipkow@1301
   106
paulson@8942
   107
Goal "min n 0 = (0::nat)";
paulson@3023
   108
by (rtac min_leastR 1);
nipkow@5983
   109
by (Simp_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];
nipkow@6433
   117
paulson@8942
   118
Goalw [max_def] "max 0 n = (n::nat)";
nipkow@6433
   119
by (Simp_tac 1);
nipkow@6433
   120
qed "max_0L";
nipkow@6433
   121
paulson@8942
   122
Goalw [max_def] "max n 0 = (n::nat)";
nipkow@6433
   123
by (Simp_tac 1);
nipkow@6433
   124
qed "max_0R";
nipkow@6433
   125
nipkow@6433
   126
Goalw [max_def] "max (Suc m) (Suc n) = Suc(max m n)";
nipkow@6433
   127
by (Simp_tac 1);
nipkow@6433
   128
qed "max_Suc_Suc";
nipkow@6433
   129
nipkow@6433
   130
Addsimps [max_0L,max_0R,max_Suc_Suc];