src/HOL/Nat.ML
author oheimb
Fri, 18 Feb 2000 20:24:56 +0100
changeset 8260 87f21e25fcb6
parent 8115 c802042066e8
child 8423 3c19160b6432
permissions -rw-r--r--
added Suc_le_D
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2441
decc46a5cdb5 added nat_induct2
oheimb
parents: 2268
diff changeset
     1
(*  Title:      HOL/Nat.ML
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2441
diff changeset
     3
    Author:     Tobias Nipkow
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2441
diff changeset
     4
    Copyright   1997 TU Muenchen
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
     7
(** conversion rules for nat_rec **)
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
     8
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
     9
val [nat_rec_0, nat_rec_Suc] = nat.recs;
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    10
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    11
(*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5188
diff changeset
    12
val prems = Goal
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    13
    "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    14
by (simp_tac (simpset() addsimps prems) 1);
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    15
qed "def_nat_rec_0";
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    16
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5188
diff changeset
    17
val prems = Goal
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    18
    "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    19
by (simp_tac (simpset() addsimps prems) 1);
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    20
qed "def_nat_rec_Suc";
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    21
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    22
val [nat_case_0, nat_case_Suc] = nat.cases;
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    23
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    24
Goal "n ~= 0 ==> EX m. n = Suc m";
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    25
by (exhaust_tac "n" 1);
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    26
by (REPEAT (Blast_tac 1));
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    27
qed "not0_implies_Suc";
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    28
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5188
diff changeset
    29
Goal "m<n ==> n ~= 0";
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    30
by (exhaust_tac "n" 1);
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    31
by (ALLGOALS Asm_full_simp_tac);
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    32
qed "gr_implies_not0";
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    33
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    34
Goal "(n ~= 0) = (0 < n)";
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    35
by (exhaust_tac "n" 1);
7089
9bfb8e218b99 expandshort and tidying
paulson
parents: 7058
diff changeset
    36
by Auto_tac;
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    37
qed "neq0_conv";
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    38
AddIffs [neq0_conv];
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    39
5644
85fd64148873 Nat: added zero_neq_conv
nipkow
parents: 5316
diff changeset
    40
Goal "(0 ~= n) = (0 < n)";
6301
08245f5a436d expandshort
paulson
parents: 6115
diff changeset
    41
by (exhaust_tac "n" 1);
7089
9bfb8e218b99 expandshort and tidying
paulson
parents: 7058
diff changeset
    42
by Auto_tac;
5644
85fd64148873 Nat: added zero_neq_conv
nipkow
parents: 5316
diff changeset
    43
qed "zero_neq_conv";
85fd64148873 Nat: added zero_neq_conv
nipkow
parents: 5316
diff changeset
    44
AddIffs [zero_neq_conv];
85fd64148873 Nat: added zero_neq_conv
nipkow
parents: 5316
diff changeset
    45
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    46
(*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    47
bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    48
8115
c802042066e8 Forgot to "call" MicroJava in makefile.
nipkow
parents: 7089
diff changeset
    49
Goal "(0<n) = (EX m. n = Suc m)";
c802042066e8 Forgot to "call" MicroJava in makefile.
nipkow
parents: 7089
diff changeset
    50
by(fast_tac (claset() addIs [not0_implies_Suc]) 1);
c802042066e8 Forgot to "call" MicroJava in makefile.
nipkow
parents: 7089
diff changeset
    51
qed "gr0_conv_Suc";
c802042066e8 Forgot to "call" MicroJava in makefile.
nipkow
parents: 7089
diff changeset
    52
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    53
Goal "(~(0 < n)) = (n=0)";
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    54
by (rtac iffI 1);
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    55
 by (etac swap 1);
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    56
 by (ALLGOALS Asm_full_simp_tac);
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    57
qed "not_gr0";
6109
82b50115564c Simplified arithmetic.
nipkow
parents: 5983
diff changeset
    58
AddIffs [not_gr0];
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    59
8260
87f21e25fcb6 added Suc_le_D
oheimb
parents: 8115
diff changeset
    60
Goal "(Suc n <= m') --> (? m. m' = Suc m)";
87f21e25fcb6 added Suc_le_D
oheimb
parents: 8115
diff changeset
    61
by (induct_tac "m'" 1);
87f21e25fcb6 added Suc_le_D
oheimb
parents: 8115
diff changeset
    62
by  Auto_tac;
87f21e25fcb6 added Suc_le_D
oheimb
parents: 8115
diff changeset
    63
qed_spec_mp "Suc_le_D";
87f21e25fcb6 added Suc_le_D
oheimb
parents: 8115
diff changeset
    64
6805
52b13dfbe954 new lemma less_Suc_eq_0_disj
paulson
parents: 6433
diff changeset
    65
(*Useful in certain inductive arguments*)
52b13dfbe954 new lemma less_Suc_eq_0_disj
paulson
parents: 6433
diff changeset
    66
Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))";
52b13dfbe954 new lemma less_Suc_eq_0_disj
paulson
parents: 6433
diff changeset
    67
by (exhaust_tac "m" 1);
52b13dfbe954 new lemma less_Suc_eq_0_disj
paulson
parents: 6433
diff changeset
    68
by Auto_tac;
52b13dfbe954 new lemma less_Suc_eq_0_disj
paulson
parents: 6433
diff changeset
    69
qed "less_Suc_eq_0_disj";
52b13dfbe954 new lemma less_Suc_eq_0_disj
paulson
parents: 6433
diff changeset
    70
7058
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    71
Goalw [Least_nat_def]
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    72
 "[| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    73
by (rtac select_equality 1);
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    74
by (fold_goals_tac [Least_nat_def]);
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    75
by (safe_tac (claset() addSEs [LeastI]));
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    76
by (rename_tac "j" 1);
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    77
by (exhaust_tac "j" 1);
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    78
by (Blast_tac 1);
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    79
by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1);
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    80
by (rename_tac "k n" 1);
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    81
by (exhaust_tac "k" 1);
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    82
by (Blast_tac 1);
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    83
by (hyp_subst_tac 1);
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    84
by (rewtac Least_nat_def);
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    85
by (rtac (select_equality RS arg_cong RS sym) 1);
7089
9bfb8e218b99 expandshort and tidying
paulson
parents: 7058
diff changeset
    86
by (blast_tac (claset() addDs [Suc_mono]) 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7058
diff changeset
    87
by (cut_inst_tac [("m","m")] less_linear 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7058
diff changeset
    88
by (blast_tac (claset() addIs [Suc_mono]) 1);
7058
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    89
qed "Least_Suc";
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    90
7058
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    91
val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    92
by (rtac less_induct 1);
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    93
by (exhaust_tac "n" 1);
7089
9bfb8e218b99 expandshort and tidying
paulson
parents: 7058
diff changeset
    94
by (exhaust_tac "nat" 2);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7058
diff changeset
    95
by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
7058
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    96
qed "nat_induct2";
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    97
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    98
Goal "min 0 n = 0";
3023
01364e2f30ad Ran expandshort
paulson
parents: 2608
diff changeset
    99
by (rtac min_leastL 1);
5983
79e301a6a51b At last: linear arithmetic for nat!
nipkow
parents: 5644
diff changeset
   100
by (Simp_tac 1);
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2441
diff changeset
   101
qed "min_0L";
1301
42782316d510 Added various thms and tactics.
nipkow
parents: 1264
diff changeset
   102
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   103
Goal "min n 0 = 0";
3023
01364e2f30ad Ran expandshort
paulson
parents: 2608
diff changeset
   104
by (rtac min_leastR 1);
5983
79e301a6a51b At last: linear arithmetic for nat!
nipkow
parents: 5644
diff changeset
   105
by (Simp_tac 1);
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2441
diff changeset
   106
qed "min_0R";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   107
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   108
Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
3023
01364e2f30ad Ran expandshort
paulson
parents: 2608
diff changeset
   109
by (Simp_tac 1);
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2441
diff changeset
   110
qed "min_Suc_Suc";
1660
8cb42cd97579 *** empty log message ***
oheimb
parents: 1618
diff changeset
   111
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2441
diff changeset
   112
Addsimps [min_0L,min_0R,min_Suc_Suc];
6433
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   113
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   114
Goalw [max_def] "max 0 n = n";
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   115
by (Simp_tac 1);
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   116
qed "max_0L";
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   117
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   118
Goalw [max_def] "max n 0 = n";
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   119
by (Simp_tac 1);
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   120
qed "max_0R";
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   121
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   122
Goalw [max_def] "max (Suc m) (Suc n) = Suc(max m n)";
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   123
by (Simp_tac 1);
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   124
qed "max_Suc_Suc";
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   125
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   126
Addsimps [max_0L,max_0R,max_Suc_Suc];