src/HOL/Divides.ML
author paulson
Wed, 23 Sep 1998 10:12:01 +0200
changeset 5537 c2bd39a2c0ee
parent 5498 7b81cae2774f
child 5983 79e301a6a51b
permissions -rw-r--r--
deleted needless parentheses
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Divides.ML
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
     2
    ID:         $Id$
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
     5
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
     6
The division operators div, mod and the divides relation "dvd"
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
     7
*)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
     8
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
     9
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    10
(** Less-then properties **)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    11
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    12
val wf_less_trans = [eq_reflection, wf_pred_nat RS wf_trancl] MRS 
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    13
                    def_wfrec RS trans;
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    14
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    15
(*** Remainder ***)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    16
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4811
diff changeset
    17
Goal "(%m. m mod n) = wfrec (trancl pred_nat) \
5415
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
    18
\                           (%f j. if j<n then j else f (j-n))";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    19
by (simp_tac (simpset() addsimps [mod_def]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    20
qed "mod_eq";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    21
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    22
Goal "m<n ==> m mod n = m";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    23
by (rtac (mod_eq RS wf_less_trans) 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    24
by (Asm_simp_tac 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    25
qed "mod_less";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    26
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    27
Goal "[| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    28
by (rtac (mod_eq RS wf_less_trans) 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    29
by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    30
qed "mod_geq";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    31
5415
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
    32
(*Avoids the ugly ~m<n above*)
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
    33
Goal "[| 0<n;  n<=m |] ==> m mod n = (m-n) mod n";
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
    34
by (asm_simp_tac (simpset() addsimps [mod_geq, not_less_iff_le]) 1);
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
    35
qed "le_mod_geq";
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
    36
4774
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
    37
(*NOT suitable for rewriting: loops*)
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    38
Goal "0<n ==> m mod n = (if m<n then m else (m-n) mod n)";
4774
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
    39
by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1);
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
    40
qed "mod_if";
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
    41
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4811
diff changeset
    42
Goal "m mod 1 = 0";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    43
by (induct_tac "m" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    44
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_less, mod_geq])));
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    45
qed "mod_1";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    46
Addsimps [mod_1];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    47
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    48
Goal "0<n ==> n mod n = 0";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    49
by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    50
qed "mod_self";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    51
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    52
Goal "0<n ==> (m+n) mod n = m mod n";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    53
by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    54
by (stac (mod_geq RS sym) 2);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    55
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
    56
qed "mod_add_self2";
4810
d55e2fee2084 New laws for mod
paulson
parents: 4774
diff changeset
    57
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    58
Goal "0<n ==> (n+m) mod n = m mod n";
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
    59
by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1);
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
    60
qed "mod_add_self1";
4810
d55e2fee2084 New laws for mod
paulson
parents: 4774
diff changeset
    61
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4811
diff changeset
    62
Goal "!!n. 0<n ==> (m + k*n) mod n = m mod n";
4810
d55e2fee2084 New laws for mod
paulson
parents: 4774
diff changeset
    63
by (induct_tac "k" 1);
5537
c2bd39a2c0ee deleted needless parentheses
paulson
parents: 5498
diff changeset
    64
by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [mod_add_self1])));
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
    65
qed "mod_mult_self1";
4810
d55e2fee2084 New laws for mod
paulson
parents: 4774
diff changeset
    66
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    67
Goal "0<n ==> (m + n*k) mod n = m mod n";
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
    68
by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1);
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
    69
qed "mod_mult_self2";
4810
d55e2fee2084 New laws for mod
paulson
parents: 4774
diff changeset
    70
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
    71
Addsimps [mod_mult_self1, mod_mult_self2];
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    72
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    73
Goal "[| 0<k; 0<n |] ==> (m mod n)*k = (m*k) mod (n*k)";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    74
by (res_inst_tac [("n","m")] less_induct 1);
4774
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
    75
by (stac mod_if 1);
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
    76
by (Asm_simp_tac 1);
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
    77
by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq, 
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
    78
				      diff_less, diff_mult_distrib]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    79
qed "mod_mult_distrib";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    80
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    81
Goal "[| 0<k; 0<n |] ==> k*(m mod n) = (k*m) mod (k*n)";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    82
by (res_inst_tac [("n","m")] less_induct 1);
4774
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
    83
by (stac mod_if 1);
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
    84
by (Asm_simp_tac 1);
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
    85
by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq, 
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
    86
				      diff_less, diff_mult_distrib2]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    87
qed "mod_mult_distrib2";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    88
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    89
Goal "0<n ==> m*n mod n = 0";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    90
by (induct_tac "m" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    91
by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5143
diff changeset
    92
by (dres_inst_tac [("m","na*n")] mod_add_self2 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    93
by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    94
qed "mod_mult_self_is_0";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    95
Addsimps [mod_mult_self_is_0];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    96
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    97
(*** Quotient ***)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    98
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4811
diff changeset
    99
Goal "(%m. m div n) = wfrec (trancl pred_nat) \
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   100
                        \            (%f j. if j<n then 0 else Suc (f (j-n)))";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   101
by (simp_tac (simpset() addsimps [div_def]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   102
qed "div_eq";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   103
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   104
Goal "m<n ==> m div n = 0";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   105
by (rtac (div_eq RS wf_less_trans) 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   106
by (Asm_simp_tac 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   107
qed "div_less";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   108
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   109
Goal "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   110
by (rtac (div_eq RS wf_less_trans) 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   111
by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   112
qed "div_geq";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   113
5415
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
   114
(*Avoids the ugly ~m<n above*)
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
   115
Goal "[| 0<n;  n<=m |] ==> m div n = Suc((m-n) div n)";
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
   116
by (asm_simp_tac (simpset() addsimps [div_geq, not_less_iff_le]) 1);
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
   117
qed "le_div_geq";
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
   118
4774
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
   119
(*NOT suitable for rewriting: loops*)
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   120
Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
4774
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
   121
by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
   122
qed "div_if";
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
   123
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   124
(*Main Result about quotient and remainder.*)
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   125
Goal "0<n ==> (m div n)*n + m mod n = m";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   126
by (res_inst_tac [("n","m")] less_induct 1);
4774
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
   127
by (stac mod_if 1);
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
   128
by (ALLGOALS (asm_simp_tac 
5537
c2bd39a2c0ee deleted needless parentheses
paulson
parents: 5498
diff changeset
   129
	      (simpset() addsimps [add_assoc, div_less, div_geq,
c2bd39a2c0ee deleted needless parentheses
paulson
parents: 5498
diff changeset
   130
				   add_diff_inverse, diff_less])));
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   131
qed "mod_div_equality";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   132
4358
aa22fcb46a5d Added thm mult_div_cancel
nipkow
parents: 4356
diff changeset
   133
(* a simple rearrangement of mod_div_equality: *)
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   134
Goal "0<k ==> k*(m div k) = m - (m mod k)";
4423
a129b817b58a expandshort;
wenzelm
parents: 4385
diff changeset
   135
by (dres_inst_tac [("m","m")] mod_div_equality 1);
4358
aa22fcb46a5d Added thm mult_div_cancel
nipkow
parents: 4356
diff changeset
   136
by (EVERY1[etac subst, simp_tac (simpset() addsimps mult_ac),
aa22fcb46a5d Added thm mult_div_cancel
nipkow
parents: 4356
diff changeset
   137
           K(IF_UNSOLVED no_tac)]);
aa22fcb46a5d Added thm mult_div_cancel
nipkow
parents: 4356
diff changeset
   138
qed "mult_div_cancel";
aa22fcb46a5d Added thm mult_div_cancel
nipkow
parents: 4356
diff changeset
   139
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4811
diff changeset
   140
Goal "m div 1 = m";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   141
by (induct_tac "m" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   142
by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_less, div_geq])));
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   143
qed "div_1";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   144
Addsimps [div_1];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   145
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   146
Goal "0<n ==> n div n = 1";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   147
by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   148
qed "div_self";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   149
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   150
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   151
Goal "0<n ==> (m+n) div n = Suc (m div n)";
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   152
by (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n)" 1);
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   153
by (stac (div_geq RS sym) 2);
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   154
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   155
qed "div_add_self2";
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   156
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   157
Goal "0<n ==> (n+m) div n = Suc (m div n)";
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   158
by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1);
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   159
qed "div_add_self1";
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   160
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4811
diff changeset
   161
Goal "!!n. 0<n ==> (m + k*n) div n = k + m div n";
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   162
by (induct_tac "k" 1);
5537
c2bd39a2c0ee deleted needless parentheses
paulson
parents: 5498
diff changeset
   163
by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [div_add_self1])));
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   164
qed "div_mult_self1";
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   165
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   166
Goal "0<n ==> (m + n*k) div n = k + m div n";
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   167
by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1);
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   168
qed "div_mult_self2";
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   169
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   170
Addsimps [div_mult_self1, div_mult_self2];
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   171
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   172
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   173
(* Monotonicity of div in first argument *)
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   174
Goal "0<k ==> ALL m. m <= n --> (m div k) <= (n div k)";
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   175
by (res_inst_tac [("n","n")] less_induct 1);
3718
d78cf498a88c Minor tidying to use Clarify_tac, etc.
paulson
parents: 3496
diff changeset
   176
by (Clarify_tac 1);
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   177
by (case_tac "n<k" 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   178
(* 1  case n<k *)
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   179
by (subgoal_tac "m<k" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   180
by (asm_simp_tac (simpset() addsimps [div_less]) 1);
3496
32e7edc609fd Simplified the new proofs about division
paulson
parents: 3484
diff changeset
   181
by (trans_tac 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   182
(* 2  case n >= k *)
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   183
by (case_tac "m<k" 1);
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   184
(* 2.1  case m<k *)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   185
by (asm_simp_tac (simpset() addsimps [div_less]) 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   186
(* 2.2  case m>=k *)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   187
by (asm_simp_tac (simpset() addsimps [div_geq, diff_less, diff_le_mono]) 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   188
qed_spec_mp "div_le_mono";
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   189
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   190
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   191
(* Antimonotonicity of div in second argument *)
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   192
Goal "[| 0<m; m<=n |] ==> (k div n) <= (k div m)";
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   193
by (subgoal_tac "0<n" 1);
3496
32e7edc609fd Simplified the new proofs about division
paulson
parents: 3484
diff changeset
   194
 by (trans_tac 2);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   195
by (res_inst_tac [("n","k")] less_induct 1);
3496
32e7edc609fd Simplified the new proofs about division
paulson
parents: 3484
diff changeset
   196
by (Simp_tac 1);
32e7edc609fd Simplified the new proofs about division
paulson
parents: 3484
diff changeset
   197
by (rename_tac "k" 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   198
by (case_tac "k<n" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   199
 by (asm_simp_tac (simpset() addsimps [div_less]) 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   200
by (subgoal_tac "~(k<m)" 1);
3496
32e7edc609fd Simplified the new proofs about division
paulson
parents: 3484
diff changeset
   201
 by (trans_tac 2);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   202
by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   203
by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5278
diff changeset
   204
by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 2));
5318
72bf8039b53f expandshort
paulson
parents: 5316
diff changeset
   205
by (rtac le_trans 1);
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5278
diff changeset
   206
by (Asm_simp_tac 1);
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5278
diff changeset
   207
by (asm_simp_tac (simpset() addsimps [diff_less]) 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   208
qed "div_le_mono2";
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   209
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   210
Goal "0<n ==> m div n <= m";
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   211
by (subgoal_tac "m div n <= m div 1" 1);
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   212
by (Asm_full_simp_tac 1);
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   213
by (rtac div_le_mono2 1);
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   214
by (ALLGOALS trans_tac);
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   215
qed "div_le_dividend";
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   216
Addsimps [div_le_dividend];
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   217
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   218
(* Similar for "less than" *)
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   219
Goal "1<n ==> (0 < m) --> (m div n < m)";
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   220
by (res_inst_tac [("n","m")] less_induct 1);
3496
32e7edc609fd Simplified the new proofs about division
paulson
parents: 3484
diff changeset
   221
by (Simp_tac 1);
32e7edc609fd Simplified the new proofs about division
paulson
parents: 3484
diff changeset
   222
by (rename_tac "m" 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   223
by (case_tac "m<n" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   224
 by (asm_full_simp_tac (simpset() addsimps [div_less]) 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   225
by (subgoal_tac "0<n" 1);
3496
32e7edc609fd Simplified the new proofs about division
paulson
parents: 3484
diff changeset
   226
 by (trans_tac 2);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   227
by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   228
by (case_tac "n<m" 1);
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   229
 by (subgoal_tac "(m-n) div n < (m-n)" 1);
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   230
  by (REPEAT (ares_tac [impI,less_trans_Suc] 1));
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   231
  by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   232
 by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   233
(* case n=m *)
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   234
by (subgoal_tac "m=n" 1);
3496
32e7edc609fd Simplified the new proofs about division
paulson
parents: 3484
diff changeset
   235
 by (trans_tac 2);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   236
by (asm_simp_tac (simpset() addsimps [div_less]) 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   237
qed_spec_mp "div_less_dividend";
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   238
Addsimps [div_less_dividend];
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   239
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   240
(*** Further facts about mod (mainly for the mutilated chess board ***)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   241
5278
a903b66822e2 even more tidying of Goal commands
paulson
parents: 5183
diff changeset
   242
Goal "0<n ==> Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   243
by (res_inst_tac [("n","m")] less_induct 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   244
by (excluded_middle_tac "Suc(na)<n" 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   245
(* case Suc(na) < n *)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   246
by (forward_tac [lessI RS less_trans] 2);
5355
paulson
parents: 5334
diff changeset
   247
by (asm_simp_tac (simpset() addsimps [mod_less, less_not_refl3]) 2);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   248
(* case n <= Suc(na) *)
5415
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
   249
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, le_Suc_eq, 
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
   250
					   mod_geq]) 1);
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
   251
by (etac disjE 1);
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
   252
 by (asm_simp_tac (simpset() addsimps [mod_less]) 2);
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
   253
by (asm_simp_tac (simpset() addsimps [Suc_diff_le, le_diff_less, 
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
   254
				      le_mod_geq]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   255
qed "mod_Suc";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   256
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   257
Goal "0<n ==> m mod n < n";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   258
by (res_inst_tac [("n","m")] less_induct 1);
5498
7b81cae2774f tidying
paulson
parents: 5415
diff changeset
   259
by (case_tac "na<n" 1);
7b81cae2774f tidying
paulson
parents: 5415
diff changeset
   260
(*case n le na*)
7b81cae2774f tidying
paulson
parents: 5415
diff changeset
   261
by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   262
(*case na<n*)
5498
7b81cae2774f tidying
paulson
parents: 5415
diff changeset
   263
by (asm_simp_tac (simpset() addsimps [mod_less]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   264
qed "mod_less_divisor";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   265
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   266
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   267
(** Evens and Odds **)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   268
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   269
(*With less_zeroE, causes case analysis on b<2*)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   270
AddSEs [less_SucE];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   271
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   272
Goal "b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   273
by (subgoal_tac "k mod 2 < 2" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   274
by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4477
diff changeset
   275
by (Asm_simp_tac 1);
4356
0dfd34f0d33d Replaced n ~= 0 by 0 < n
nipkow
parents: 4089
diff changeset
   276
by Safe_tac;
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   277
qed "mod2_cases";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   278
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4811
diff changeset
   279
Goal "Suc(Suc(m)) mod 2 = m mod 2";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   280
by (subgoal_tac "m mod 2 < 2" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   281
by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
3724
f33e301a89f5 Step_tac -> Safe_tac
paulson
parents: 3718
diff changeset
   282
by Safe_tac;
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   283
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc])));
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   284
qed "mod2_Suc_Suc";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   285
Addsimps [mod2_Suc_Suc];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   286
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4811
diff changeset
   287
Goal "(0 < m mod 2) = (m mod 2 = 1)";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   288
by (subgoal_tac "m mod 2 < 2" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   289
by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4423
diff changeset
   290
by Auto_tac;
4356
0dfd34f0d33d Replaced n ~= 0 by 0 < n
nipkow
parents: 4089
diff changeset
   291
qed "mod2_gr_0";
0dfd34f0d33d Replaced n ~= 0 by 0 < n
nipkow
parents: 4089
diff changeset
   292
Addsimps [mod2_gr_0];
0dfd34f0d33d Replaced n ~= 0 by 0 < n
nipkow
parents: 4089
diff changeset
   293
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4811
diff changeset
   294
Goal "(m+m) mod 2 = 0";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   295
by (induct_tac "m" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   296
by (simp_tac (simpset() addsimps [mod_less]) 1);
3427
e7cef2081106 Removed a few redundant additions of simprules or classical rules
paulson
parents: 3366
diff changeset
   297
by (Asm_simp_tac 1);
4385
f6d019eefa1e Got rid of mod2_neq_0
paulson
parents: 4358
diff changeset
   298
qed "mod2_add_self_eq_0";
f6d019eefa1e Got rid of mod2_neq_0
paulson
parents: 4358
diff changeset
   299
Addsimps [mod2_add_self_eq_0];
f6d019eefa1e Got rid of mod2_neq_0
paulson
parents: 4358
diff changeset
   300
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4811
diff changeset
   301
Goal "((m+m)+n) mod 2 = n mod 2";
4385
f6d019eefa1e Got rid of mod2_neq_0
paulson
parents: 4358
diff changeset
   302
by (induct_tac "m" 1);
f6d019eefa1e Got rid of mod2_neq_0
paulson
parents: 4358
diff changeset
   303
by (simp_tac (simpset() addsimps [mod_less]) 1);
f6d019eefa1e Got rid of mod2_neq_0
paulson
parents: 4358
diff changeset
   304
by (Asm_simp_tac 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   305
qed "mod2_add_self";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   306
Addsimps [mod2_add_self];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   307
5498
7b81cae2774f tidying
paulson
parents: 5415
diff changeset
   308
(*Restore the default*)
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   309
Delrules [less_SucE];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   310
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   311
(*** More division laws ***)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   312
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   313
Goal "0<n ==> m*n div n = m";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   314
by (cut_inst_tac [("m", "m*n")] mod_div_equality 1);
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3427
diff changeset
   315
by (assume_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   316
by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   317
qed "div_mult_self_is_m";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   318
Addsimps [div_mult_self_is_m];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   319
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   320
(*Cancellation law for division*)
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   321
Goal "[| 0<n; 0<k |] ==> (k*m) div (k*n) = m div n";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   322
by (res_inst_tac [("n","m")] less_induct 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   323
by (case_tac "na<n" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   324
by (asm_simp_tac (simpset() addsimps [div_less, zero_less_mult_iff, 
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   325
                                     mult_less_mono2]) 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   326
by (subgoal_tac "~ k*na < k*n" 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   327
by (asm_simp_tac
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   328
     (simpset() addsimps [zero_less_mult_iff, div_geq,
5415
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
   329
			  diff_mult_distrib2 RS sym, diff_less]) 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   330
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, 
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   331
                                          le_refl RS mult_le_mono]) 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   332
qed "div_cancel";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   333
Addsimps [div_cancel];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   334
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   335
Goal "[| 0<n; 0<k |] ==> (k*m) mod (k*n) = k * (m mod n)";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   336
by (res_inst_tac [("n","m")] less_induct 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   337
by (case_tac "na<n" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   338
by (asm_simp_tac (simpset() addsimps [mod_less, zero_less_mult_iff, 
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   339
                                     mult_less_mono2]) 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   340
by (subgoal_tac "~ k*na < k*n" 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   341
by (asm_simp_tac
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   342
     (simpset() addsimps [zero_less_mult_iff, mod_geq,
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   343
                         diff_mult_distrib2 RS sym, diff_less]) 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   344
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, 
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   345
                                          le_refl RS mult_le_mono]) 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   346
qed "mult_mod_distrib";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   347
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   348
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   349
(************************************************)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   350
(** Divides Relation                           **)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   351
(************************************************)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   352
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4811
diff changeset
   353
Goalw [dvd_def] "m dvd 0";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   354
by (blast_tac (claset() addIs [mult_0_right RS sym]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   355
qed "dvd_0_right";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   356
Addsimps [dvd_0_right];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   357
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   358
Goalw [dvd_def] "0 dvd m ==> m = 0";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   359
by (fast_tac (claset() addss simpset()) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   360
qed "dvd_0_left";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   361
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4811
diff changeset
   362
Goalw [dvd_def] "1 dvd k";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   363
by (Simp_tac 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   364
qed "dvd_1_left";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   365
AddIffs [dvd_1_left];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   366
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4811
diff changeset
   367
Goalw [dvd_def] "m dvd m";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   368
by (blast_tac (claset() addIs [mult_1_right RS sym]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   369
qed "dvd_refl";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   370
Addsimps [dvd_refl];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   371
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   372
Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd p";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   373
by (blast_tac (claset() addIs [mult_assoc] ) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   374
qed "dvd_trans";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   375
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   376
Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m=n";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   377
by (fast_tac (claset() addDs [mult_eq_self_implies_10]
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   378
                     addss (simpset() addsimps [mult_assoc, mult_eq_1_iff])) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   379
qed "dvd_anti_sym";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   380
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   381
Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m + n)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   382
by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   383
qed "dvd_add";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   384
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   385
Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   386
by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   387
qed "dvd_diff";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   388
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   389
Goal "[| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3427
diff changeset
   390
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   391
by (blast_tac (claset() addIs [dvd_add]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   392
qed "dvd_diffD";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   393
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   394
Goalw [dvd_def] "k dvd n ==> k dvd (m*n)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   395
by (blast_tac (claset() addIs [mult_left_commute]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   396
qed "dvd_mult";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   397
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   398
Goal "k dvd m ==> k dvd (m*n)";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   399
by (stac mult_commute 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   400
by (etac dvd_mult 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   401
qed "dvd_mult2";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   402
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   403
(* k dvd (m*k) *)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   404
AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   405
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   406
Goalw [dvd_def] "[| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
3718
d78cf498a88c Minor tidying to use Clarify_tac, etc.
paulson
parents: 3496
diff changeset
   407
by (Clarify_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   408
by (full_simp_tac (simpset() addsimps [zero_less_mult_iff]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   409
by (res_inst_tac 
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   410
    [("x", "(((k div ka)*ka + k mod ka) - ((f*k) div (f*ka)) * ka)")] 
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   411
    exI 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   412
by (asm_simp_tac (simpset() addsimps [diff_mult_distrib2, 
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   413
                                     mult_mod_distrib, add_mult_distrib2]) 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   414
qed "dvd_mod";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   415
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   416
Goal "[| k dvd (m mod n); k dvd n; 0<n |] ==> k dvd m";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   417
by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   418
by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2);
4356
0dfd34f0d33d Replaced n ~= 0 by 0 < n
nipkow
parents: 4089
diff changeset
   419
by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   420
qed "dvd_mod_imp_dvd";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   421
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   422
Goalw [dvd_def]  "!!k. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   423
by (etac exE 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   424
by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   425
by (Blast_tac 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   426
qed "dvd_mult_cancel";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   427
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   428
Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> (i*j) dvd (m*n)";
3718
d78cf498a88c Minor tidying to use Clarify_tac, etc.
paulson
parents: 3496
diff changeset
   429
by (Clarify_tac 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   430
by (res_inst_tac [("x","k*ka")] exI 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   431
by (asm_simp_tac (simpset() addsimps mult_ac) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   432
qed "mult_dvd_mono";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   433
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   434
Goalw [dvd_def] "(i*j) dvd k ==> i dvd k";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   435
by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   436
by (Blast_tac 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   437
qed "dvd_mult_left";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   438
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   439
Goalw [dvd_def] "[| k dvd n; 0 < n |] ==> k <= n";
3718
d78cf498a88c Minor tidying to use Clarify_tac, etc.
paulson
parents: 3496
diff changeset
   440
by (Clarify_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   441
by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff])));
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3427
diff changeset
   442
by (etac conjE 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3427
diff changeset
   443
by (rtac le_trans 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3427
diff changeset
   444
by (rtac (le_refl RS mult_le_mono) 2);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   445
by (etac Suc_leI 2);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   446
by (Simp_tac 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   447
qed "dvd_imp_le";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   448
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   449
Goalw [dvd_def] "0<k ==> (k dvd n) = (n mod k = 0)";
3724
f33e301a89f5 Step_tac -> Safe_tac
paulson
parents: 3718
diff changeset
   450
by Safe_tac;
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   451
by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   452
by (eres_inst_tac [("t","n")] (mod_div_equality RS subst) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   453
by (stac mult_commute 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   454
by (Asm_simp_tac 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   455
by (Blast_tac 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   456
qed "dvd_eq_mod_eq_0";