src/HOL/Nat.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10450 60ddd5fdf93b
child 10558 09a91221ced1
permissions -rw-r--r--
hide many names from Datatype_Universe.
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$
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
     3
    Author:     Lawrence C Paulson and Tobias Nipkow
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
     4
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
     5
Proofs about natural numbers and elementary arithmetic: addition,
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
     6
multiplication, etc.  Some from the Hoare example from Norbert Galm.
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
     9
(** conversion rules for nat_rec **)
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
val [nat_rec_0, nat_rec_Suc] = nat.recs;
9108
9fff97d29837 bind_thm(s);
wenzelm
parents: 8942
diff changeset
    12
bind_thm ("nat_rec_0", nat_rec_0);
9fff97d29837 bind_thm(s);
wenzelm
parents: 8942
diff changeset
    13
bind_thm ("nat_rec_Suc", nat_rec_Suc);
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    14
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    15
(*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
    16
val prems = Goal
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    17
    "[| !!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
    18
by (simp_tac (simpset() addsimps prems) 1);
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    19
qed "def_nat_rec_0";
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    20
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5188
diff changeset
    21
val prems = Goal
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    22
    "[| !!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
    23
by (simp_tac (simpset() addsimps prems) 1);
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    24
qed "def_nat_rec_Suc";
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    25
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    26
val [nat_case_0, nat_case_Suc] = nat.cases;
9108
9fff97d29837 bind_thm(s);
wenzelm
parents: 8942
diff changeset
    27
bind_thm ("nat_case_0", nat_case_0);
9fff97d29837 bind_thm(s);
wenzelm
parents: 8942
diff changeset
    28
bind_thm ("nat_case_Suc", nat_case_Suc);
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    29
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    30
Goal "n ~= 0 ==> EX m. n = Suc m";
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    31
by (case_tac "n" 1);
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    32
by (REPEAT (Blast_tac 1));
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    33
qed "not0_implies_Suc";
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    34
8942
6aad5381ba83 added type constraint ::nat because 0 is now overloaded
paulson
parents: 8442
diff changeset
    35
Goal "!!n::nat. m<n ==> n ~= 0";
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    36
by (case_tac "n" 1);
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    37
by (ALLGOALS Asm_full_simp_tac);
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    38
qed "gr_implies_not0";
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    39
8942
6aad5381ba83 added type constraint ::nat because 0 is now overloaded
paulson
parents: 8442
diff changeset
    40
Goal "!!n::nat. (n ~= 0) = (0 < n)";
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    41
by (case_tac "n" 1);
7089
9bfb8e218b99 expandshort and tidying
paulson
parents: 7058
diff changeset
    42
by Auto_tac;
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    43
qed "neq0_conv";
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    44
AddIffs [neq0_conv];
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    45
8942
6aad5381ba83 added type constraint ::nat because 0 is now overloaded
paulson
parents: 8442
diff changeset
    46
Goal "!!n::nat. (0 ~= n) = (0 < n)";
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    47
by (case_tac "n" 1);
7089
9bfb8e218b99 expandshort and tidying
paulson
parents: 7058
diff changeset
    48
by Auto_tac;
5644
85fd64148873 Nat: added zero_neq_conv
nipkow
parents: 5316
diff changeset
    49
qed "zero_neq_conv";
85fd64148873 Nat: added zero_neq_conv
nipkow
parents: 5316
diff changeset
    50
AddIffs [zero_neq_conv];
85fd64148873 Nat: added zero_neq_conv
nipkow
parents: 5316
diff changeset
    51
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    52
(*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
    53
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
    54
8115
c802042066e8 Forgot to "call" MicroJava in makefile.
nipkow
parents: 7089
diff changeset
    55
Goal "(0<n) = (EX m. n = Suc m)";
c802042066e8 Forgot to "call" MicroJava in makefile.
nipkow
parents: 7089
diff changeset
    56
by(fast_tac (claset() addIs [not0_implies_Suc]) 1);
c802042066e8 Forgot to "call" MicroJava in makefile.
nipkow
parents: 7089
diff changeset
    57
qed "gr0_conv_Suc";
c802042066e8 Forgot to "call" MicroJava in makefile.
nipkow
parents: 7089
diff changeset
    58
8942
6aad5381ba83 added type constraint ::nat because 0 is now overloaded
paulson
parents: 8442
diff changeset
    59
Goal "!!n::nat. (~(0 < n)) = (n=0)";
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    60
by (rtac iffI 1);
10173
1d097572d23b got rid of a swap
paulson
parents: 9969
diff changeset
    61
 by (rtac ccontr 1);
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    62
 by (ALLGOALS Asm_full_simp_tac);
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    63
qed "not_gr0";
6109
82b50115564c Simplified arithmetic.
nipkow
parents: 5983
diff changeset
    64
AddIffs [not_gr0];
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    65
8260
87f21e25fcb6 added Suc_le_D
oheimb
parents: 8115
diff changeset
    66
Goal "(Suc n <= m') --> (? m. m' = Suc m)";
87f21e25fcb6 added Suc_le_D
oheimb
parents: 8115
diff changeset
    67
by (induct_tac "m'" 1);
87f21e25fcb6 added Suc_le_D
oheimb
parents: 8115
diff changeset
    68
by  Auto_tac;
87f21e25fcb6 added Suc_le_D
oheimb
parents: 8115
diff changeset
    69
qed_spec_mp "Suc_le_D";
87f21e25fcb6 added Suc_le_D
oheimb
parents: 8115
diff changeset
    70
6805
52b13dfbe954 new lemma less_Suc_eq_0_disj
paulson
parents: 6433
diff changeset
    71
(*Useful in certain inductive arguments*)
52b13dfbe954 new lemma less_Suc_eq_0_disj
paulson
parents: 6433
diff changeset
    72
Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))";
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    73
by (case_tac "m" 1);
6805
52b13dfbe954 new lemma less_Suc_eq_0_disj
paulson
parents: 6433
diff changeset
    74
by Auto_tac;
52b13dfbe954 new lemma less_Suc_eq_0_disj
paulson
parents: 6433
diff changeset
    75
qed "less_Suc_eq_0_disj";
52b13dfbe954 new lemma less_Suc_eq_0_disj
paulson
parents: 6433
diff changeset
    76
7058
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    77
Goalw [Least_nat_def]
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    78
 "[| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9870
diff changeset
    79
by (rtac some_equality 1);
7058
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    80
by (fold_goals_tac [Least_nat_def]);
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    81
by (safe_tac (claset() addSEs [LeastI]));
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    82
by (rename_tac "j" 1);
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    83
by (case_tac "j" 1);
7058
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    84
by (Blast_tac 1);
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    85
by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1);
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    86
by (rename_tac "k n" 1);
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    87
by (case_tac "k" 1);
7058
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    88
by (Blast_tac 1);
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    89
by (hyp_subst_tac 1);
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    90
by (rewtac Least_nat_def);
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9870
diff changeset
    91
by (rtac (some_equality RS arg_cong RS sym) 1);
7089
9bfb8e218b99 expandshort and tidying
paulson
parents: 7058
diff changeset
    92
by (blast_tac (claset() addDs [Suc_mono]) 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7058
diff changeset
    93
by (cut_inst_tac [("m","m")] less_linear 1);
9bfb8e218b99 expandshort and tidying
paulson
parents: 7058
diff changeset
    94
by (blast_tac (claset() addIs [Suc_mono]) 1);
7058
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    95
qed "Least_Suc";
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
    96
7058
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
    97
val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
9870
2374ba026fc6 less_induct -> nat_less_induct
nipkow
parents: 9637
diff changeset
    98
by (rtac nat_less_induct 1);
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    99
by (case_tac "n" 1);
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
   100
by (case_tac "nat" 2);
7089
9bfb8e218b99 expandshort and tidying
paulson
parents: 7058
diff changeset
   101
by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
7058
8dfea70eb6b7 removed 2 qed_goals
paulson
parents: 6805
diff changeset
   102
qed "nat_induct2";
5188
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents: 5069
diff changeset
   103
8942
6aad5381ba83 added type constraint ::nat because 0 is now overloaded
paulson
parents: 8442
diff changeset
   104
Goal "min 0 n = (0::nat)";
3023
01364e2f30ad Ran expandshort
paulson
parents: 2608
diff changeset
   105
by (rtac min_leastL 1);
5983
79e301a6a51b At last: linear arithmetic for nat!
nipkow
parents: 5644
diff changeset
   106
by (Simp_tac 1);
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2441
diff changeset
   107
qed "min_0L";
1301
42782316d510 Added various thms and tactics.
nipkow
parents: 1264
diff changeset
   108
8942
6aad5381ba83 added type constraint ::nat because 0 is now overloaded
paulson
parents: 8442
diff changeset
   109
Goal "min n 0 = (0::nat)";
3023
01364e2f30ad Ran expandshort
paulson
parents: 2608
diff changeset
   110
by (rtac min_leastR 1);
5983
79e301a6a51b At last: linear arithmetic for nat!
nipkow
parents: 5644
diff changeset
   111
by (Simp_tac 1);
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2441
diff changeset
   112
qed "min_0R";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   113
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   114
Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
3023
01364e2f30ad Ran expandshort
paulson
parents: 2608
diff changeset
   115
by (Simp_tac 1);
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2441
diff changeset
   116
qed "min_Suc_Suc";
1660
8cb42cd97579 *** empty log message ***
oheimb
parents: 1618
diff changeset
   117
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2441
diff changeset
   118
Addsimps [min_0L,min_0R,min_Suc_Suc];
6433
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   119
8942
6aad5381ba83 added type constraint ::nat because 0 is now overloaded
paulson
parents: 8442
diff changeset
   120
Goalw [max_def] "max 0 n = (n::nat)";
6433
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   121
by (Simp_tac 1);
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   122
qed "max_0L";
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   123
8942
6aad5381ba83 added type constraint ::nat because 0 is now overloaded
paulson
parents: 8442
diff changeset
   124
Goalw [max_def] "max n 0 = (n::nat)";
6433
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   125
by (Simp_tac 1);
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   126
qed "max_0R";
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   127
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   128
Goalw [max_def] "max (Suc m) (Suc n) = Suc(max m n)";
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   129
by (Simp_tac 1);
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   130
qed "max_Suc_Suc";
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   131
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   132
Addsimps [max_0L,max_0R,max_Suc_Suc];
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   133
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   134
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   135
(*** Basic rewrite rules for the arithmetic operators ***)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   136
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   137
(** Difference **)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   138
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   139
Goal "0 - n = (0::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   140
by (induct_tac "n" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   141
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   142
qed "diff_0_eq_0";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   143
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   144
(*Must simplify BEFORE the induction!  (Else we get a critical pair)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   145
  Suc(m) - Suc(n)   rewrites to   pred(Suc(m) - n)  *)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   146
Goal "Suc(m) - Suc(n) = m - n";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   147
by (Simp_tac 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   148
by (induct_tac "n" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   149
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   150
qed "diff_Suc_Suc";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   151
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   152
Addsimps [diff_0_eq_0, diff_Suc_Suc];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   153
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   154
(* Could be (and is, below) generalized in various ways;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   155
   However, none of the generalizations are currently in the simpset,
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   156
   and I dread to think what happens if I put them in *)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   157
Goal "0 < n ==> Suc(n-1) = n";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   158
by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   159
qed "Suc_pred";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   160
Addsimps [Suc_pred];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   161
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   162
Delsimps [diff_Suc];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   163
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   164
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   165
(**** Inductive properties of the operators ****)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   166
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   167
(*** Addition ***)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   168
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   169
Goal "m + 0 = (m::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   170
by (induct_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   171
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   172
qed "add_0_right";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   173
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   174
Goal "m + Suc(n) = Suc(m+n)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   175
by (induct_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   176
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   177
qed "add_Suc_right";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   178
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   179
Addsimps [add_0_right,add_Suc_right];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   180
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   181
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   182
(*Associative law for addition*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   183
Goal "(m + n) + k = m + ((n + k)::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   184
by (induct_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   185
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   186
qed "add_assoc";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   187
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   188
(*Commutative law for addition*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   189
Goal "m + n = n + (m::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   190
by (induct_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   191
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   192
qed "add_commute";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   193
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   194
Goal "x+(y+z)=y+((x+z)::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   195
by (rtac (add_commute RS trans) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   196
by (rtac (add_assoc RS trans) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   197
by (rtac (add_commute RS arg_cong) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   198
qed "add_left_commute";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   199
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   200
(*Addition is an AC-operator*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   201
bind_thms ("add_ac", [add_assoc, add_commute, add_left_commute]);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   202
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   203
Goal "(k + m = k + n) = (m=(n::nat))";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   204
by (induct_tac "k" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   205
by (Simp_tac 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   206
by (Asm_simp_tac 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   207
qed "add_left_cancel";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   208
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   209
Goal "(m + k = n + k) = (m=(n::nat))";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   210
by (induct_tac "k" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   211
by (Simp_tac 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   212
by (Asm_simp_tac 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   213
qed "add_right_cancel";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   214
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   215
Goal "(k + m <= k + n) = (m<=(n::nat))";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   216
by (induct_tac "k" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   217
by (Simp_tac 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   218
by (Asm_simp_tac 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   219
qed "add_left_cancel_le";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   220
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   221
Goal "(k + m < k + n) = (m<(n::nat))";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   222
by (induct_tac "k" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   223
by (Simp_tac 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   224
by (Asm_simp_tac 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   225
qed "add_left_cancel_less";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   226
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   227
Addsimps [add_left_cancel, add_right_cancel,
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   228
          add_left_cancel_le, add_left_cancel_less];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   229
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   230
(** Reasoning about m+0=0, etc. **)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   231
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   232
Goal "!!m::nat. (m+n = 0) = (m=0 & n=0)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   233
by (case_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   234
by (Auto_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   235
qed "add_is_0";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   236
AddIffs [add_is_0];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   237
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   238
Goal "!!m::nat. (0 = m+n) = (m=0 & n=0)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   239
by (case_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   240
by (Auto_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   241
qed "zero_is_add";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   242
AddIffs [zero_is_add];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   243
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   244
Goal "!!m::nat. (m+n=1) = (m=1 & n=0 | m=0 & n=1)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   245
by (case_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   246
by (Auto_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   247
qed "add_is_1";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   248
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   249
Goal "!!m::nat. (1=m+n) = (m=1 & n=0 | m=0 & n=1)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   250
by (case_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   251
by (Auto_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   252
qed "one_is_add";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   253
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   254
Goal "!!m::nat. (0<m+n) = (0<m | 0<n)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   255
by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   256
qed "add_gr_0";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   257
AddIffs [add_gr_0];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   258
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   259
Goal "!!m::nat. m + n = m ==> n = 0";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   260
by (dtac (add_0_right RS ssubst) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   261
by (asm_full_simp_tac (simpset() addsimps [add_assoc]
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   262
                                 delsimps [add_0_right]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   263
qed "add_eq_self_zero";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   264
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   265
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   266
(**** Additional theorems about "less than" ****)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   267
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   268
(*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   269
Goal "m<n --> (EX k. n=Suc(m+k))";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   270
by (induct_tac "n" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   271
by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less])));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   272
by (blast_tac (claset() addSEs [less_SucE]
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   273
                        addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   274
qed_spec_mp "less_eq_Suc_add";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   275
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   276
Goal "n <= ((m + n)::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   277
by (induct_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   278
by (ALLGOALS Simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   279
by (etac le_SucI 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   280
qed "le_add2";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   281
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   282
Goal "n <= ((n + m)::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   283
by (simp_tac (simpset() addsimps add_ac) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   284
by (rtac le_add2 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   285
qed "le_add1";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   286
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   287
bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans)));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   288
bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   289
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   290
Goal "(m<n) = (EX k. n=Suc(m+k))";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   291
by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   292
qed "less_iff_Suc_add";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   293
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   294
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   295
(*"i <= j ==> i <= j+m"*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   296
bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   297
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   298
(*"i <= j ==> i <= m+j"*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   299
bind_thm ("trans_le_add2", le_add2 RSN (2,le_trans));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   300
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   301
(*"i < j ==> i < j+m"*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   302
bind_thm ("trans_less_add1", le_add1 RSN (2,less_le_trans));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   303
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   304
(*"i < j ==> i < m+j"*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   305
bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   306
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   307
Goal "i+j < (k::nat) --> i<k";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   308
by (induct_tac "j" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   309
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   310
by (blast_tac (claset() addDs [Suc_lessD]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   311
qed_spec_mp "add_lessD1";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   312
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   313
Goal "~ (i+j < (i::nat))";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   314
by (rtac notI 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   315
by (etac (add_lessD1 RS less_irrefl) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   316
qed "not_add_less1";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   317
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   318
Goal "~ (j+i < (i::nat))";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   319
by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   320
qed "not_add_less2";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   321
AddIffs [not_add_less1, not_add_less2];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   322
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   323
Goal "m+k<=n --> m<=(n::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   324
by (induct_tac "k" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   325
by (ALLGOALS (asm_simp_tac (simpset() addsimps le_simps)));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   326
qed_spec_mp "add_leD1";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   327
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   328
Goal "m+k<=n ==> k<=(n::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   329
by (full_simp_tac (simpset() addsimps [add_commute]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   330
by (etac add_leD1 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   331
qed_spec_mp "add_leD2";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   332
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   333
Goal "m+k<=n ==> m<=n & k<=(n::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   334
by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   335
bind_thm ("add_leE", result() RS conjE);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   336
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   337
(*needs !!k for add_ac to work*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   338
Goal "!!k:: nat. [| k<l;  m+l = k+n |] ==> m<n";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   339
by (force_tac (claset(),
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   340
              simpset() delsimps [add_Suc_right]
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   341
                        addsimps [less_iff_Suc_add,
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   342
                                  add_Suc_right RS sym] @ add_ac) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   343
qed "less_add_eq_less";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   344
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   345
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   346
(*** Monotonicity of Addition ***)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   347
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   348
(*strict, in 1st argument*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   349
Goal "i < j ==> i + k < j + (k::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   350
by (induct_tac "k" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   351
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   352
qed "add_less_mono1";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   353
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   354
(*strict, in both arguments*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   355
Goal "[|i < j; k < l|] ==> i + k < j + (l::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   356
by (rtac (add_less_mono1 RS less_trans) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   357
by (REPEAT (assume_tac 1));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   358
by (induct_tac "j" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   359
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   360
qed "add_less_mono";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   361
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   362
(*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   363
val [lt_mono,le] = Goal
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   364
     "[| !!i j::nat. i<j ==> f(i) < f(j);       \
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   365
\        i <= j                                 \
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   366
\     |] ==> f(i) <= (f(j)::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   367
by (cut_facts_tac [le] 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   368
by (asm_full_simp_tac (simpset() addsimps [order_le_less]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   369
by (blast_tac (claset() addSIs [lt_mono]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   370
qed "less_mono_imp_le_mono";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   371
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   372
(*non-strict, in 1st argument*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   373
Goal "i<=j ==> i + k <= j + (k::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   374
by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   375
by (etac add_less_mono1 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   376
by (assume_tac 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   377
qed "add_le_mono1";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   378
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   379
(*non-strict, in both arguments*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   380
Goal "[|i<=j;  k<=l |] ==> i + k <= j + (l::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   381
by (etac (add_le_mono1 RS le_trans) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   382
by (simp_tac (simpset() addsimps [add_commute]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   383
qed "add_le_mono";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   384
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   385
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   386
(*** Multiplication ***)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   387
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   388
(*right annihilation in product*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   389
Goal "!!m::nat. m * 0 = 0";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   390
by (induct_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   391
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   392
qed "mult_0_right";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   393
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   394
(*right successor law for multiplication*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   395
Goal  "m * Suc(n) = m + (m * n)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   396
by (induct_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   397
by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   398
qed "mult_Suc_right";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   399
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   400
Addsimps [mult_0_right, mult_Suc_right];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   401
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   402
Goal "1 * n = n";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   403
by (Asm_simp_tac 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   404
qed "mult_1";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   405
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   406
Goal "n * 1 = n";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   407
by (Asm_simp_tac 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   408
qed "mult_1_right";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   409
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   410
(*Commutative law for multiplication*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   411
Goal "m * n = n * (m::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   412
by (induct_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   413
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   414
qed "mult_commute";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   415
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   416
(*addition distributes over multiplication*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   417
Goal "(m + n)*k = (m*k) + ((n*k)::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   418
by (induct_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   419
by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   420
qed "add_mult_distrib";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   421
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   422
Goal "k*(m + n) = (k*m) + ((k*n)::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   423
by (induct_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   424
by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   425
qed "add_mult_distrib2";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   426
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   427
(*Associative law for multiplication*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   428
Goal "(m * n) * k = m * ((n * k)::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   429
by (induct_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   430
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib])));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   431
qed "mult_assoc";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   432
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   433
Goal "x*(y*z) = y*((x*z)::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   434
by (rtac trans 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   435
by (rtac mult_commute 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   436
by (rtac trans 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   437
by (rtac mult_assoc 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   438
by (rtac (mult_commute RS arg_cong) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   439
qed "mult_left_commute";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   440
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   441
bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   442
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   443
Goal "!!m::nat. (m*n = 0) = (m=0 | n=0)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   444
by (induct_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   445
by (induct_tac "n" 2);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   446
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   447
qed "mult_is_0";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   448
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   449
Goal "!!m::nat. (0 = m*n) = (0=m | 0=n)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   450
by (stac eq_commute 1 THEN stac mult_is_0 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   451
by Auto_tac;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   452
qed "zero_is_mult";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   453
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   454
Addsimps [mult_is_0, zero_is_mult];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   455
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   456
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   457
(*** Difference ***)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   458
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   459
Goal "!!m::nat. m - m = 0";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   460
by (induct_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   461
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   462
qed "diff_self_eq_0";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   463
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   464
Addsimps [diff_self_eq_0];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   465
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   466
(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   467
Goal "~ m<n --> n+(m-n) = (m::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   468
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   469
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   470
qed_spec_mp "add_diff_inverse";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   471
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   472
Goal "n<=m ==> n+(m-n) = (m::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   473
by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   474
qed "le_add_diff_inverse";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   475
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   476
Goal "n<=m ==> (m-n)+n = (m::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   477
by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   478
qed "le_add_diff_inverse2";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   479
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   480
Addsimps  [le_add_diff_inverse, le_add_diff_inverse2];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   481
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   482
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   483
(*** More results about difference ***)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   484
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   485
Goal "n <= m ==> Suc(m)-n = Suc(m-n)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   486
by (etac rev_mp 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   487
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   488
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   489
qed "Suc_diff_le";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   490
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   491
Goal "m - n < Suc(m)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   492
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   493
by (etac less_SucE 3);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   494
by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   495
qed "diff_less_Suc";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   496
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   497
Goal "m - n <= (m::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   498
by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   499
by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_SucI])));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   500
qed "diff_le_self";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   501
Addsimps [diff_le_self];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   502
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   503
(* j<k ==> j-n < k *)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   504
bind_thm ("less_imp_diff_less", diff_le_self RS le_less_trans);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   505
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   506
Goal "!!i::nat. i-j-k = i - (j+k)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   507
by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   508
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   509
qed "diff_diff_left";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   510
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   511
Goal "(Suc m - n) - Suc k = m - n - k";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   512
by (simp_tac (simpset() addsimps [diff_diff_left]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   513
qed "Suc_diff_diff";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   514
Addsimps [Suc_diff_diff];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   515
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   516
Goal "0<n ==> n - Suc i < n";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   517
by (case_tac "n" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   518
by Safe_tac;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   519
by (asm_simp_tac (simpset() addsimps le_simps) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   520
qed "diff_Suc_less";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   521
Addsimps [diff_Suc_less];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   522
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   523
(*This and the next few suggested by Florian Kammueller*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   524
Goal "!!i::nat. i-j-k = i-k-j";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   525
by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   526
qed "diff_commute";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   527
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   528
Goal "k <= (j::nat) --> (i + j) - k = i + (j - k)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   529
by (res_inst_tac [("m","j"),("n","k")] diff_induct 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   530
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   531
qed_spec_mp "diff_add_assoc";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   532
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   533
Goal "k <= (j::nat) --> (j + i) - k = (j - k) + i";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   534
by (asm_simp_tac (simpset() addsimps [add_commute, diff_add_assoc]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   535
qed_spec_mp "diff_add_assoc2";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   536
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   537
Goal "(n+m) - n = (m::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   538
by (induct_tac "n" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   539
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   540
qed "diff_add_inverse";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   541
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   542
Goal "(m+n) - n = (m::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   543
by (simp_tac (simpset() addsimps [diff_add_assoc]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   544
qed "diff_add_inverse2";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   545
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   546
Goal "i <= (j::nat) ==> (j-i=k) = (j=k+i)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   547
by Safe_tac;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   548
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_add_inverse2])));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   549
qed "le_imp_diff_is_add";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   550
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   551
Goal "!!m::nat. (m-n = 0) = (m <= n)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   552
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   553
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   554
qed "diff_is_0_eq";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   555
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   556
Goal "!!m::nat. (0 = m-n) = (m <= n)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   557
by (stac (diff_is_0_eq RS sym) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   558
by (rtac eq_sym_conv 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   559
qed "zero_is_diff_eq";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   560
Addsimps [diff_is_0_eq, zero_is_diff_eq];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   561
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   562
Goal "!!m::nat. (0<n-m) = (m<n)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   563
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   564
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   565
qed "zero_less_diff";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   566
Addsimps [zero_less_diff];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   567
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   568
Goal "i < j  ==> EX k::nat. 0<k & i+k = j";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   569
by (res_inst_tac [("x","j - i")] exI 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   570
by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   571
qed "less_imp_add_positive";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   572
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   573
Goal "P(k) --> (ALL n. P(Suc(n))--> P(n)) --> P(k-i)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   574
by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   575
by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   576
qed "zero_induct_lemma";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   577
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   578
val prems = Goal "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   579
by (rtac (diff_self_eq_0 RS subst) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   580
by (rtac (zero_induct_lemma RS mp RS mp) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   581
by (REPEAT (ares_tac ([impI,allI]@prems) 1));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   582
qed "zero_induct";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   583
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   584
Goal "(k+m) - (k+n) = m - (n::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   585
by (induct_tac "k" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   586
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   587
qed "diff_cancel";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   588
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   589
Goal "(m+k) - (n+k) = m - (n::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   590
by (asm_simp_tac
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   591
    (simpset() addsimps [diff_cancel, inst "n" "k" add_commute]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   592
qed "diff_cancel2";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   593
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   594
Goal "n - (n+m) = (0::nat)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   595
by (induct_tac "n" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   596
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   597
qed "diff_add_0";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   598
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   599
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   600
(** Difference distributes over multiplication **)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   601
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   602
Goal "!!m::nat. (m - n) * k = (m * k) - (n * k)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   603
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   604
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel])));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   605
qed "diff_mult_distrib" ;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   606
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   607
Goal "!!m::nat. k * (m - n) = (k * m) - (k * n)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   608
val mult_commute_k = read_instantiate [("m","k")] mult_commute;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   609
by (simp_tac (simpset() addsimps [diff_mult_distrib, mult_commute_k]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   610
qed "diff_mult_distrib2" ;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   611
(*NOT added as rewrites, since sometimes they are used from right-to-left*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   612
10450
60ddd5fdf93b nat_distrib;
wenzelm
parents: 10173
diff changeset
   613
bind_thms ("nat_distrib",
60ddd5fdf93b nat_distrib;
wenzelm
parents: 10173
diff changeset
   614
  [add_mult_distrib, add_mult_distrib2, diff_mult_distrib, diff_mult_distrib2]);
60ddd5fdf93b nat_distrib;
wenzelm
parents: 10173
diff changeset
   615
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   616
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   617
(*** Monotonicity of Multiplication ***)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   618
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   619
Goal "i <= (j::nat) ==> i*k<=j*k";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   620
by (induct_tac "k" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   621
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   622
qed "mult_le_mono1";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   623
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   624
Goal "i <= (j::nat) ==> k*i <= k*j";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   625
by (dtac mult_le_mono1 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   626
by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   627
qed "mult_le_mono2";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   628
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   629
(* <= monotonicity, BOTH arguments*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   630
Goal "[| i <= (j::nat); k <= l |] ==> i*k <= j*l";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   631
by (etac (mult_le_mono1 RS le_trans) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   632
by (etac mult_le_mono2 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   633
qed "mult_le_mono";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   634
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   635
(*strict, in 1st argument; proof is by induction on k>0*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   636
Goal "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   637
by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   638
by (Asm_simp_tac 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   639
by (induct_tac "x" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   640
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   641
qed "mult_less_mono2";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   642
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   643
Goal "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   644
by (dtac mult_less_mono2 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   645
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   646
qed "mult_less_mono1";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   647
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   648
Goal "!!m::nat. (0 < m*n) = (0<m & 0<n)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   649
by (induct_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   650
by (case_tac "n" 2);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   651
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   652
qed "zero_less_mult_iff";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   653
Addsimps [zero_less_mult_iff];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   654
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   655
Goal "(1 <= m*n) = (1<=m & 1<=n)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   656
by (induct_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   657
by (case_tac "n" 2);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   658
by (ALLGOALS Asm_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   659
qed "one_le_mult_iff";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   660
Addsimps [one_le_mult_iff];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   661
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   662
Goal "(m*n = 1) = (m=1 & n=1)";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   663
by (induct_tac "m" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   664
by (Simp_tac 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   665
by (induct_tac "n" 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   666
by (Simp_tac 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   667
by (fast_tac (claset() addss simpset()) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   668
qed "mult_eq_1_iff";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   669
Addsimps [mult_eq_1_iff];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   670
9637
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   671
Goal "!!m::nat. (m*k < n*k) = (0<k & m<n)";
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   672
by (safe_tac (claset() addSIs [mult_less_mono1]));
9637
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   673
by (case_tac "k" 1);
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   674
by Auto_tac;  
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   675
by (full_simp_tac (simpset() delsimps [le_0_eq]
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   676
			     addsimps [linorder_not_le RS sym]) 1);
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   677
by (blast_tac (claset() addIs [mult_le_mono1]) 1); 
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   678
qed "mult_less_cancel2";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   679
9637
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   680
Goal "!!m::nat. (k*m < k*n) = (0<k & m<n)";
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   681
by (simp_tac (simpset() addsimps [mult_less_cancel2, 
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   682
                                  inst "m" "k" mult_commute]) 1);
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   683
qed "mult_less_cancel1";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   684
Addsimps [mult_less_cancel1, mult_less_cancel2];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   685
9637
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   686
Goal "!!m::nat. (m*k <= n*k) = (0<k --> m<=n)";
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   687
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   688
by Auto_tac;  
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   689
qed "mult_le_cancel2";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   690
9637
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   691
Goal "!!m::nat. (k*m <= k*n) = (0<k --> m<=n)";
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   692
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   693
by Auto_tac;  
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   694
qed "mult_le_cancel1";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   695
Addsimps [mult_le_cancel1, mult_le_cancel2];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   696
9637
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   697
Goal "(m*k = n*k) = (m=n | (k = (0::nat)))";
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   698
by (cut_facts_tac [less_linear] 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   699
by Safe_tac;
9637
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   700
by Auto_tac; 	
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   701
by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   702
by (ALLGOALS Asm_full_simp_tac);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   703
qed "mult_cancel2";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   704
9637
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   705
Goal "(k*m = k*n) = (m=n | (k = (0::nat)))";
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   706
by (simp_tac (simpset() addsimps [mult_cancel2, inst "m" "k" mult_commute]) 1);
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   707
qed "mult_cancel1";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   708
Addsimps [mult_cancel1, mult_cancel2];
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   709
9637
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   710
Goal "(Suc k * m < Suc k * n) = (m < n)";
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   711
by (stac mult_less_cancel1 1);
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   712
by (Simp_tac 1);
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   713
qed "Suc_mult_less_cancel1";
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   714
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   715
Goal "(Suc k * m <= Suc k * n) = (m <= n)";
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   716
by (stac mult_le_cancel1 1);
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   717
by (Simp_tac 1);
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   718
qed "Suc_mult_le_cancel1";
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   719
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   720
Goal "(Suc k * m = Suc k * n) = (m = n)";
9637
47d39a31eb2f better rules for cancellation of common factors across comparisons
paulson
parents: 9436
diff changeset
   721
by (stac mult_cancel1 1);
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   722
by (Simp_tac 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   723
qed "Suc_mult_cancel1";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   724
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   725
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   726
(*Lemma for gcd*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   727
Goal "!!m::nat. m = m*n ==> n=1 | m=0";
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   728
by (dtac sym 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   729
by (rtac disjCI 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   730
by (rtac nat_less_cases 1 THEN assume_tac 2);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   731
by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   732
by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1);
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9108
diff changeset
   733
qed "mult_eq_self_implies_10";