src/HOL/Divides.ML
author wenzelm
Fri, 26 Oct 2001 23:58:21 +0200
changeset 11952 b10f1e8862f4
parent 11701 3d51fbf81c17
child 12304 8df202daf55d
permissions -rw-r--r--
* Pure: method 'atomize' presents local goal premises as object-level statements (atomic meta-level propositions); setup controlled via rewrite rules declarations of 'atomize' attribute; example application: 'induct' method with proper rule statements in improper proof *scripts*;
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
9108
9fff97d29837 bind_thm(s);
wenzelm
parents: 8935
diff changeset
    12
bind_thm ("wf_less_trans", [eq_reflection, wf_pred_nat RS wf_trancl] MRS 
9fff97d29837 bind_thm(s);
wenzelm
parents: 8935
diff changeset
    13
                    def_wfrec RS trans);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    14
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4811
diff changeset
    15
Goal "(%m. m mod n) = wfrec (trancl pred_nat) \
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    16
\                           (%f j. if j<n | n=0 then j else f (j-n))";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    17
by (simp_tac (simpset() addsimps [mod_def]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    18
qed "mod_eq";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    19
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    20
Goal "(%m. m div n) = wfrec (trancl pred_nat) \
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    21
\            (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))";
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    22
by (simp_tac (simpset() addsimps [div_def]) 1);
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    23
qed "div_eq";
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    24
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    25
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    26
(** Aribtrary definitions for division by zero.  Useful to simplify 
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    27
    certain equations **)
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    28
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8860
diff changeset
    29
Goal "a div 0 = (0::nat)";
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    30
by (rtac (div_eq RS wf_less_trans) 1);
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    31
by (Asm_simp_tac 1);
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    32
qed "DIVISION_BY_ZERO_DIV";  (*NOT for adding to default simpset*)
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    33
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8860
diff changeset
    34
Goal "a mod 0 = (a::nat)";
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    35
by (rtac (mod_eq RS wf_less_trans) 1);
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    36
by (Asm_simp_tac 1);
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    37
qed "DIVISION_BY_ZERO_MOD";  (*NOT for adding to default simpset*)
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    38
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    39
fun div_undefined_case_tac s i =
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    40
  case_tac s i THEN 
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    41
  Full_simp_tac (i+1) THEN
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    42
  asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_DIV, 
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    43
				    DIVISION_BY_ZERO_MOD]) i;
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    44
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    45
(*** Remainder ***)
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    46
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 6073
diff changeset
    47
Goal "m<n ==> m mod n = (m::nat)";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    48
by (rtac (mod_eq RS wf_less_trans) 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    49
by (Asm_simp_tac 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    50
qed "mod_less";
8393
c7772d3787c3 mod_less, div_less are now default simprules
paulson
parents: 7499
diff changeset
    51
Addsimps [mod_less];
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    52
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    53
Goal "~ m < (n::nat) ==> m mod n = (m-n) mod n";
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    54
by (div_undefined_case_tac "n=0" 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    55
by (rtac (mod_eq RS wf_less_trans) 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    56
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
    57
qed "mod_geq";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    58
5415
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
    59
(*Avoids the ugly ~m<n above*)
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    60
Goal "(n::nat) <= m ==> m mod n = (m-n) mod n";
5415
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
    61
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
    62
qed "le_mod_geq";
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
    63
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    64
Goal "m mod (n::nat) = (if m<n then m else (m-n) mod n)";
8393
c7772d3787c3 mod_less, div_less are now default simprules
paulson
parents: 7499
diff changeset
    65
by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
4774
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
    66
qed "mod_if";
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
    67
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11593
diff changeset
    68
Goal "m mod Suc 0 = 0";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    69
by (induct_tac "m" 1);
8393
c7772d3787c3 mod_less, div_less are now default simprules
paulson
parents: 7499
diff changeset
    70
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_geq])));
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    71
qed "mod_1";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    72
Addsimps [mod_1];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    73
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8860
diff changeset
    74
Goal "n mod n = (0::nat)";
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    75
by (div_undefined_case_tac "n=0" 1);
8393
c7772d3787c3 mod_less, div_less are now default simprules
paulson
parents: 7499
diff changeset
    76
by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    77
qed "mod_self";
10559
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
    78
Addsimps [mod_self];
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    79
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    80
Goal "(m+n) mod n = m mod (n::nat)";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    81
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
    82
by (stac (mod_geq RS sym) 2);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
    83
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
    84
qed "mod_add_self2";
4810
d55e2fee2084 New laws for mod
paulson
parents: 4774
diff changeset
    85
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    86
Goal "(n+m) mod n = m mod (n::nat)";
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
    87
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
    88
qed "mod_add_self1";
4810
d55e2fee2084 New laws for mod
paulson
parents: 4774
diff changeset
    89
8783
9edcc005ebd9 removed obsolete "evenness" proofs
paulson
parents: 8698
diff changeset
    90
Addsimps [mod_add_self1, mod_add_self2];
9edcc005ebd9 removed obsolete "evenness" proofs
paulson
parents: 8698
diff changeset
    91
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    92
Goal "(m + k*n) mod n = m mod (n::nat)";
4810
d55e2fee2084 New laws for mod
paulson
parents: 4774
diff changeset
    93
by (induct_tac "k" 1);
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    94
by (ALLGOALS
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    95
    (asm_simp_tac 
8783
9edcc005ebd9 removed obsolete "evenness" proofs
paulson
parents: 8698
diff changeset
    96
     (simpset() addsimps [read_instantiate [("y","n")] add_left_commute])));
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
    97
qed "mod_mult_self1";
4810
d55e2fee2084 New laws for mod
paulson
parents: 4774
diff changeset
    98
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
    99
Goal "(m + n*k) mod n = m mod (n::nat)";
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   100
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
   101
qed "mod_mult_self2";
4810
d55e2fee2084 New laws for mod
paulson
parents: 4774
diff changeset
   102
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   103
Addsimps [mod_mult_self1, mod_mult_self2];
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   104
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   105
Goal "(m mod n) * (k::nat) = (m*k) mod (n*k)";
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   106
by (div_undefined_case_tac "n=0" 1);
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   107
by (div_undefined_case_tac "k=0" 1);
9870
2374ba026fc6 less_induct -> nat_less_induct
nipkow
parents: 9637
diff changeset
   108
by (induct_thm_tac nat_less_induct "m" 1);
4774
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
   109
by (stac mod_if 1);
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
   110
by (Asm_simp_tac 1);
8393
c7772d3787c3 mod_less, div_less are now default simprules
paulson
parents: 7499
diff changeset
   111
by (asm_simp_tac (simpset() addsimps [mod_geq, 
4774
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
   112
				      diff_less, diff_mult_distrib]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   113
qed "mod_mult_distrib";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   114
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   115
Goal "(k::nat) * (m mod n) = (k*m) mod (k*n)";
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   116
by (asm_simp_tac 
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   117
    (simpset() addsimps [read_instantiate [("m","k")] mult_commute, 
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   118
			 mod_mult_distrib]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   119
qed "mod_mult_distrib2";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   120
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8860
diff changeset
   121
Goal "(m*n) mod n = (0::nat)";
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   122
by (div_undefined_case_tac "n=0" 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   123
by (induct_tac "m" 1);
8393
c7772d3787c3 mod_less, div_less are now default simprules
paulson
parents: 7499
diff changeset
   124
by (Asm_simp_tac 1);
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   125
by (rename_tac "k" 1);
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   126
by (cut_inst_tac [("m","k*n"),("n","n")] mod_add_self2 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   127
by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   128
qed "mod_mult_self_is_0";
7082
f444e632cdf5 new cancellation laws
paulson
parents: 7059
diff changeset
   129
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8860
diff changeset
   130
Goal "(n*m) mod n = (0::nat)";
7082
f444e632cdf5 new cancellation laws
paulson
parents: 7059
diff changeset
   131
by (simp_tac (simpset() addsimps [mult_commute, mod_mult_self_is_0]) 1);
f444e632cdf5 new cancellation laws
paulson
parents: 7059
diff changeset
   132
qed "mod_mult_self1_is_0";
f444e632cdf5 new cancellation laws
paulson
parents: 7059
diff changeset
   133
Addsimps [mod_mult_self_is_0, mod_mult_self1_is_0];
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   134
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   135
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   136
(*** Quotient ***)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   137
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8860
diff changeset
   138
Goal "m<n ==> m div n = (0::nat)";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   139
by (rtac (div_eq RS wf_less_trans) 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   140
by (Asm_simp_tac 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   141
qed "div_less";
8393
c7772d3787c3 mod_less, div_less are now default simprules
paulson
parents: 7499
diff changeset
   142
Addsimps [div_less];
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   143
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   144
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
   145
by (rtac (div_eq RS wf_less_trans) 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   146
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
   147
qed "div_geq";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   148
5415
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
   149
(*Avoids the ugly ~m<n above*)
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
   150
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
   151
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
   152
qed "le_div_geq";
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
   153
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   154
Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
8393
c7772d3787c3 mod_less, div_less are now default simprules
paulson
parents: 7499
diff changeset
   155
by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
4774
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
   156
qed "div_if";
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
   157
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   158
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   159
(*Main Result about quotient and remainder.*)
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   160
Goal "(m div n)*n + m mod n = (m::nat)";
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   161
by (div_undefined_case_tac "n=0" 1);
9870
2374ba026fc6 less_induct -> nat_less_induct
nipkow
parents: 9637
diff changeset
   162
by (induct_thm_tac nat_less_induct "m" 1);
4774
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
   163
by (stac mod_if 1);
b4760a833480 Tidied proofs by getting rid of case_tac
paulson
parents: 4686
diff changeset
   164
by (ALLGOALS (asm_simp_tac 
8393
c7772d3787c3 mod_less, div_less are now default simprules
paulson
parents: 7499
diff changeset
   165
	      (simpset() addsimps [add_assoc, div_geq,
5537
c2bd39a2c0ee deleted needless parentheses
paulson
parents: 5498
diff changeset
   166
				   add_diff_inverse, diff_less])));
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   167
qed "mod_div_equality";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   168
4358
aa22fcb46a5d Added thm mult_div_cancel
nipkow
parents: 4356
diff changeset
   169
(* a simple rearrangement of mod_div_equality: *)
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   170
Goal "(n::nat) * (m div n) = m - (m mod n)";
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   171
by (cut_inst_tac [("m","m"),("n","n")] mod_div_equality 1);
9912
paulson
parents: 9881
diff changeset
   172
by (full_simp_tac (simpset() addsimps mult_ac) 1);
paulson
parents: 9881
diff changeset
   173
by (arith_tac 1);
4358
aa22fcb46a5d Added thm mult_div_cancel
nipkow
parents: 4356
diff changeset
   174
qed "mult_div_cancel";
aa22fcb46a5d Added thm mult_div_cancel
nipkow
parents: 4356
diff changeset
   175
10559
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   176
Goal "0<n ==> m mod n < (n::nat)";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   177
by (induct_thm_tac nat_less_induct "m" 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   178
by (case_tac "na<n" 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   179
(*case n le na*)
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   180
by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   181
(*case na<n*)
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   182
by (Asm_simp_tac 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   183
qed "mod_less_divisor";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   184
Addsimps [mod_less_divisor];
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   185
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   186
(*** More division laws ***)
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   187
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   188
Goal "0<n ==> (m*n) div n = (m::nat)";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   189
by (cut_inst_tac [("m", "m*n"),("n","n")] mod_div_equality 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   190
by Auto_tac;
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   191
qed "div_mult_self_is_m";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   192
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   193
Goal "0<n ==> (n*m) div n = (m::nat)";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   194
by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self_is_m]) 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   195
qed "div_mult_self1_is_m";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   196
Addsimps [div_mult_self_is_m, div_mult_self1_is_m];
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   197
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   198
(*mod_mult_distrib2 above is the counterpart for remainder*)
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   199
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   200
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   201
(*** Proving facts about div and mod using quorem ***)
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   202
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   203
Goal "[| b*q' + r'  <= b*q + r;  0 < b;  r < b |] \
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   204
\     ==> q' <= (q::nat)";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   205
by (rtac leI 1); 
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   206
by (stac less_iff_Suc_add 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   207
by (auto_tac (claset(), simpset() addsimps [add_mult_distrib2]));   
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   208
qed "unique_quotient_lemma";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   209
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   210
Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |] \
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   211
\     ==> q = q'";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   212
by (asm_full_simp_tac 
10600
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   213
    (simpset() addsimps split_ifs @ [Divides.quorem_def]) 1);
10559
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   214
by Auto_tac;  
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   215
by (REPEAT 
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   216
    (blast_tac (claset() addIs [order_antisym]
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   217
			 addDs [order_eq_refl RS unique_quotient_lemma, 
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   218
				sym]) 1));
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   219
qed "unique_quotient";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   220
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   221
Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |] \
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   222
\     ==> r = r'";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   223
by (subgoal_tac "q = q'" 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   224
by (blast_tac (claset() addIs [unique_quotient]) 2);
10600
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   225
by (asm_full_simp_tac (simpset() addsimps [Divides.quorem_def]) 1);
10559
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   226
qed "unique_remainder";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   227
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   228
Goal "0 < b ==> quorem ((a, b), (a div b, a mod b))";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   229
by (cut_inst_tac [("m","a"),("n","b")] mod_div_equality 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   230
by (auto_tac
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   231
    (claset() addEs [sym],
10600
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   232
     simpset() addsimps mult_ac@[Divides.quorem_def]));
10559
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   233
qed "quorem_div_mod";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   234
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   235
Goal "[| quorem((a,b),(q,r));  0 < b |] ==> a div b = q";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   236
by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   237
qed "quorem_div";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   238
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   239
Goal "[| quorem((a,b),(q,r));  0 < b |] ==> a mod b = r";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   240
by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   241
qed "quorem_mod";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   242
10600
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   243
(** A dividend of zero **)
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   244
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   245
Goal "0 div m = (0::nat)";
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   246
by (div_undefined_case_tac "m=0" 1);
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   247
by (Asm_simp_tac 1);
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   248
qed "div_0"; 
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   249
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   250
Goal "0 mod m = (0::nat)";
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   251
by (div_undefined_case_tac "m=0" 1);
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   252
by (Asm_simp_tac 1);
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   253
qed "mod_0"; 
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   254
Addsimps [div_0, mod_0];
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   255
10559
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   256
(** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   257
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   258
Goal "[| quorem((b,c),(q,r));  0 < c |] \
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   259
\     ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   260
by (cut_inst_tac [("m", "a*r"), ("n","c")] mod_div_equality 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   261
by (auto_tac
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   262
    (claset(),
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   263
     simpset() addsimps split_ifs@mult_ac@
10600
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   264
                        [Divides.quorem_def, add_mult_distrib2]));
10559
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   265
val lemma = result();
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   266
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   267
Goal "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   268
by (div_undefined_case_tac "c = 0" 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   269
by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   270
qed "div_mult1_eq";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   271
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   272
Goal "(a*b) mod c = a*(b mod c) mod (c::nat)";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   273
by (div_undefined_case_tac "c = 0" 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   274
by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   275
qed "mod_mult1_eq";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   276
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   277
Goal "(a*b) mod (c::nat) = ((a mod c) * b) mod c";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   278
by (rtac trans 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   279
by (res_inst_tac [("s","b*a mod c")] trans 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   280
by (rtac mod_mult1_eq 2);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   281
by (ALLGOALS (simp_tac (simpset() addsimps [mult_commute])));
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   282
qed "mod_mult1_eq'";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   283
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   284
Goal "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   285
by (rtac (mod_mult1_eq' RS trans) 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   286
by (rtac mod_mult1_eq 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   287
qed "mod_mult_distrib_mod";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   288
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   289
(** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   290
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   291
Goal "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  0 < c |] \
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   292
\     ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   293
by (cut_inst_tac [("m", "ar+br"), ("n","c")] mod_div_equality 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   294
by (auto_tac
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   295
    (claset(),
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   296
     simpset() addsimps split_ifs@mult_ac@
10600
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   297
                        [Divides.quorem_def, add_mult_distrib2]));
10559
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   298
val lemma = result();
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   299
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   300
(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   301
Goal "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   302
by (div_undefined_case_tac "c = 0" 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   303
by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   304
			       MRS lemma RS quorem_div]) 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   305
qed "div_add1_eq";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   306
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   307
Goal "(a+b) mod (c::nat) = (a mod c + b mod c) mod c";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   308
by (div_undefined_case_tac "c = 0" 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   309
by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   310
			       MRS lemma RS quorem_mod]) 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   311
qed "mod_add1_eq";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   312
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   313
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   314
(*** proving  a div (b*c) = (a div b) div c ***)
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   315
10600
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   316
(** first, a lemma to bound the remainder **)
10559
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   317
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   318
Goal "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   319
by (cut_inst_tac [("m","q"),("n","c")] mod_less_divisor 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   320
by (dres_inst_tac [("m","q mod c")] less_imp_Suc_add 2); 
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   321
by Auto_tac;  
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   322
by (eres_inst_tac [("P","%x. ?lhs < ?rhs x")] ssubst 1); 
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   323
by (asm_simp_tac (simpset() addsimps [add_mult_distrib2]) 1);
10600
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   324
val mod_lemma = result();
10559
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   325
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   326
Goal "[| quorem ((a,b), (q,r));  0 < b;  0 < c |] \
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   327
\     ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   328
by (cut_inst_tac [("m", "q"), ("n","c")] mod_div_equality 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   329
by (auto_tac  
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   330
    (claset(),
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   331
     simpset() addsimps mult_ac@
10600
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   332
                        [Divides.quorem_def, add_mult_distrib2 RS sym,
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   333
			 mod_lemma]));
10559
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   334
val lemma = result();
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   335
10600
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   336
Goal "a div (b*c) = (a div b) div (c::nat)";
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   337
by (div_undefined_case_tac "b=0" 1);
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   338
by (div_undefined_case_tac "c=0" 1);
10559
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   339
by (force_tac (claset(),
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   340
	       simpset() addsimps [quorem_div_mod RS lemma RS quorem_div]) 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   341
qed "div_mult2_eq";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   342
10600
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   343
Goal "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)";
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   344
by (div_undefined_case_tac "b=0" 1);
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   345
by (div_undefined_case_tac "c=0" 1);
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   346
by (cut_inst_tac [("m", "a"), ("n","b")] mod_div_equality 1);
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   347
by (auto_tac (claset(),
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   348
	       simpset() addsimps [mult_commute, 
322475c2cb75 deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
paulson
parents: 10559
diff changeset
   349
				   quorem_div_mod RS lemma RS quorem_mod]));
10559
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   350
qed "mod_mult2_eq";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   351
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   352
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   353
(*** Cancellation of common factors in "div" ***)
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   354
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   355
Goal "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   356
by (stac div_mult2_eq 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   357
by Auto_tac;
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   358
val lemma1 = result();
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   359
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   360
Goal "(0::nat) < c ==> (c*a) div (c*b) = a div b";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   361
by (div_undefined_case_tac "b = 0" 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   362
by (auto_tac
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   363
    (claset(), 
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   364
     simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, 
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   365
			 lemma1, lemma2]));
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   366
qed "div_mult_mult1";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   367
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   368
Goal "(0::nat) < c ==> (a*c) div (b*c) = a div b";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   369
by (dtac div_mult_mult1 1);
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   370
by (auto_tac (claset(), simpset() addsimps [mult_commute]));
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   371
qed "div_mult_mult2";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   372
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   373
Addsimps [div_mult_mult1, div_mult_mult2];
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   374
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   375
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   376
(*** Distribution of factors over "mod"
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   377
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   378
Could prove these as in Integ/IntDiv.ML, but we already have
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   379
mod_mult_distrib and mod_mult_distrib2 above!
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   380
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   381
Goal "(c*a) mod (c*b) = (c::nat) * (a mod b)";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   382
qed "mod_mult_mult1";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   383
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   384
Goal "(a*c) mod (b*c) = (a mod b) * (c::nat)";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   385
qed "mod_mult_mult2";
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   386
 ***)
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   387
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   388
(*** Further facts about div and mod ***)
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   389
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11593
diff changeset
   390
Goal "m div Suc 0 = m";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   391
by (induct_tac "m" 1);
8393
c7772d3787c3 mod_less, div_less are now default simprules
paulson
parents: 7499
diff changeset
   392
by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_geq])));
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   393
qed "div_1";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   394
Addsimps [div_1];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   395
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8860
diff changeset
   396
Goal "0<n ==> n div n = (1::nat)";
8393
c7772d3787c3 mod_less, div_less are now default simprules
paulson
parents: 7499
diff changeset
   397
by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   398
qed "div_self";
10559
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   399
Addsimps [div_self];
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   400
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   401
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
   402
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
   403
by (stac (div_geq RS sym) 2);
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   404
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   405
qed "div_add_self2";
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   406
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   407
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
   408
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
   409
qed "div_add_self1";
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   410
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8860
diff changeset
   411
Goal "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n";
10559
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   412
by (stac div_add1_eq 1); 
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   413
by (stac div_mult1_eq 1); 
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10195
diff changeset
   414
by (Asm_simp_tac 1); 
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   415
qed "div_mult_self1";
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   416
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8860
diff changeset
   417
Goal "0<n ==> (m + n*k) div n = k + m div (n::nat)";
4811
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   418
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
   419
qed "div_mult_self2";
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   420
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   421
Addsimps [div_mult_self1, div_mult_self2];
7a98aa1f9a9d Renamed mod_XXX_cancel to mod_XXX_self
paulson
parents: 4810
diff changeset
   422
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   423
(* Monotonicity of div in first argument *)
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   424
Goal "ALL m::nat. m <= n --> (m div k) <= (n div k)";
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   425
by (div_undefined_case_tac "k=0" 1);
9870
2374ba026fc6 less_induct -> nat_less_induct
nipkow
parents: 9637
diff changeset
   426
by (induct_thm_tac nat_less_induct "n" 1);
3718
d78cf498a88c Minor tidying to use Clarify_tac, etc.
paulson
parents: 3496
diff changeset
   427
by (Clarify_tac 1);
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   428
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
   429
(* 1  case n<k *)
8393
c7772d3787c3 mod_less, div_less are now default simprules
paulson
parents: 7499
diff changeset
   430
by (Asm_simp_tac 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   431
(* 2  case n >= k *)
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   432
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
   433
(* 2.1  case m<k *)
8393
c7772d3787c3 mod_less, div_less are now default simprules
paulson
parents: 7499
diff changeset
   434
by (Asm_simp_tac 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   435
(* 2.2  case m>=k *)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   436
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
   437
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
   438
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   439
(* Antimonotonicity of div in second argument *)
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8860
diff changeset
   440
Goal "!!m::nat. [| 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
   441
by (subgoal_tac "0<n" 1);
6073
fba734ba6894 Refined arith tactic.
nipkow
parents: 5983
diff changeset
   442
 by (Asm_simp_tac 2);
9870
2374ba026fc6 less_induct -> nat_less_induct
nipkow
parents: 9637
diff changeset
   443
by (induct_thm_tac nat_less_induct "k" 1);
3496
32e7edc609fd Simplified the new proofs about division
paulson
parents: 3484
diff changeset
   444
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
   445
by (case_tac "k<n" 1);
8393
c7772d3787c3 mod_less, div_less are now default simprules
paulson
parents: 7499
diff changeset
   446
 by (Asm_simp_tac 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   447
by (subgoal_tac "~(k<m)" 1);
6073
fba734ba6894 Refined arith tactic.
nipkow
parents: 5983
diff changeset
   448
 by (Asm_simp_tac 2);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   449
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
   450
by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   451
 by (REPEAT (ares_tac [div_le_mono,diff_le_mono2] 2));
5318
72bf8039b53f expandshort
paulson
parents: 5316
diff changeset
   452
by (rtac le_trans 1);
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5278
diff changeset
   453
by (Asm_simp_tac 1);
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5278
diff changeset
   454
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
   455
qed "div_le_mono2";
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   456
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   457
Goal "m div n <= (m::nat)";
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   458
by (div_undefined_case_tac "n=0" 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   459
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
   460
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
   461
by (rtac div_le_mono2 1);
6073
fba734ba6894 Refined arith tactic.
nipkow
parents: 5983
diff changeset
   462
by (ALLGOALS Asm_simp_tac);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   463
qed "div_le_dividend";
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   464
Addsimps [div_le_dividend];
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   465
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   466
(* Similar for "less than" *)
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8860
diff changeset
   467
Goal "!!n::nat. 1<n ==> (0 < m) --> (m div n < m)";
9870
2374ba026fc6 less_induct -> nat_less_induct
nipkow
parents: 9637
diff changeset
   468
by (induct_thm_tac nat_less_induct "m" 1);
3496
32e7edc609fd Simplified the new proofs about division
paulson
parents: 3484
diff changeset
   469
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
   470
by (case_tac "m<n" 1);
8393
c7772d3787c3 mod_less, div_less are now default simprules
paulson
parents: 7499
diff changeset
   471
 by (Asm_full_simp_tac 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   472
by (subgoal_tac "0<n" 1);
6073
fba734ba6894 Refined arith tactic.
nipkow
parents: 5983
diff changeset
   473
 by (Asm_simp_tac 2);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   474
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
   475
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
   476
 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
   477
  by (REPEAT (ares_tac [impI,less_trans_Suc] 1));
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   478
  by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   479
 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
   480
(* case n=m *)
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   481
by (subgoal_tac "m=n" 1);
6073
fba734ba6894 Refined arith tactic.
nipkow
parents: 5983
diff changeset
   482
 by (Asm_simp_tac 2);
8393
c7772d3787c3 mod_less, div_less are now default simprules
paulson
parents: 7499
diff changeset
   483
by (Asm_simp_tac 1);
3484
1e93eb09ebb9 Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents: 3457
diff changeset
   484
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
   485
Addsimps [div_less_dividend];
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   486
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   487
(*** Further facts about mod (mainly for the mutilated chess board ***)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   488
10964
afc1dfc5a92d the 0<n premise was unnecessary
paulson
parents: 10789
diff changeset
   489
Goal "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
afc1dfc5a92d the 0<n premise was unnecessary
paulson
parents: 10789
diff changeset
   490
by (div_undefined_case_tac "n=0" 1);
9870
2374ba026fc6 less_induct -> nat_less_induct
nipkow
parents: 9637
diff changeset
   491
by (induct_thm_tac nat_less_induct "m" 1);
8860
paulson
parents: 8783
diff changeset
   492
by (case_tac "Suc(na)<n" 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   493
(* case Suc(na) < n *)
8860
paulson
parents: 8783
diff changeset
   494
by (forward_tac [lessI RS less_trans] 1 
paulson
parents: 8783
diff changeset
   495
    THEN asm_simp_tac (simpset() addsimps [less_not_refl3]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   496
(* case n <= Suc(na) *)
5415
13a199e94877 tidying; moved diff_less to Arith.ML
paulson
parents: 5355
diff changeset
   497
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
   498
					   mod_geq]) 1);
8860
paulson
parents: 8783
diff changeset
   499
by (auto_tac (claset(), 
paulson
parents: 8783
diff changeset
   500
	      simpset() addsimps [Suc_diff_le, diff_less, le_mod_geq]));
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   501
qed "mod_Suc";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   502
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   503
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   504
(************************************************)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   505
(** Divides Relation                           **)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   506
(************************************************)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   507
11593
ab08d61966b1 AddXIs [dvdI]; AddXEs [dvdE];
wenzelm
parents: 11464
diff changeset
   508
Goalw [dvd_def] "n = m * k ==> m dvd n";
11373
ef11fb6e6c58 a couple of new theorems
paulson
parents: 11365
diff changeset
   509
by (Blast_tac 1); 
ef11fb6e6c58 a couple of new theorems
paulson
parents: 11365
diff changeset
   510
qed "dvdI";
11593
ab08d61966b1 AddXIs [dvdI]; AddXEs [dvdE];
wenzelm
parents: 11464
diff changeset
   511
AddXIs [dvdI];
11373
ef11fb6e6c58 a couple of new theorems
paulson
parents: 11365
diff changeset
   512
11365
6d5698df0413 new material from the Sylow proof
paulson
parents: 11313
diff changeset
   513
Goalw [dvd_def] "!!P. [|m dvd n;  !!k. n = m*k ==> P|] ==> P";
6d5698df0413 new material from the Sylow proof
paulson
parents: 11313
diff changeset
   514
by (Blast_tac 1); 
6d5698df0413 new material from the Sylow proof
paulson
parents: 11313
diff changeset
   515
qed "dvdE";
11593
ab08d61966b1 AddXIs [dvdI]; AddXEs [dvdE];
wenzelm
parents: 11464
diff changeset
   516
AddXEs [dvdE];
11365
6d5698df0413 new material from the Sylow proof
paulson
parents: 11313
diff changeset
   517
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8860
diff changeset
   518
Goalw [dvd_def] "m dvd (0::nat)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   519
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
   520
qed "dvd_0_right";
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   521
AddIffs [dvd_0_right];
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   522
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8860
diff changeset
   523
Goalw [dvd_def] "0 dvd m ==> m = (0::nat)";
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 6073
diff changeset
   524
by Auto_tac;
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   525
qed "dvd_0_left";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   526
11373
ef11fb6e6c58 a couple of new theorems
paulson
parents: 11365
diff changeset
   527
Goal "(0 dvd (m::nat)) = (m = 0)";
ef11fb6e6c58 a couple of new theorems
paulson
parents: 11365
diff changeset
   528
by (blast_tac (claset() addIs [dvd_0_left]) 1); 
ef11fb6e6c58 a couple of new theorems
paulson
parents: 11365
diff changeset
   529
qed "dvd_0_left_iff";
ef11fb6e6c58 a couple of new theorems
paulson
parents: 11365
diff changeset
   530
AddIffs [dvd_0_left_iff];
ef11fb6e6c58 a couple of new theorems
paulson
parents: 11365
diff changeset
   531
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11593
diff changeset
   532
Goalw [dvd_def] "Suc 0 dvd k";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   533
by (Simp_tac 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   534
qed "dvd_1_left";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   535
AddIffs [dvd_1_left];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   536
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11593
diff changeset
   537
Goal "(m dvd Suc 0) = (m = Suc 0)";
11365
6d5698df0413 new material from the Sylow proof
paulson
parents: 11313
diff changeset
   538
by (simp_tac (simpset() addsimps [dvd_def]) 1); 
6d5698df0413 new material from the Sylow proof
paulson
parents: 11313
diff changeset
   539
qed "dvd_1_iff_1";
6d5698df0413 new material from the Sylow proof
paulson
parents: 11313
diff changeset
   540
Addsimps [dvd_1_iff_1];
6d5698df0413 new material from the Sylow proof
paulson
parents: 11313
diff changeset
   541
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 6073
diff changeset
   542
Goalw [dvd_def] "m dvd (m::nat)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   543
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
   544
qed "dvd_refl";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   545
Addsimps [dvd_refl];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   546
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 6073
diff changeset
   547
Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd (p::nat)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   548
by (blast_tac (claset() addIs [mult_assoc] ) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   549
qed "dvd_trans";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   550
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 6073
diff changeset
   551
Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m = (n::nat)";
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 6073
diff changeset
   552
by (force_tac (claset() addDs [mult_eq_self_implies_10],
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 6073
diff changeset
   553
	       simpset() addsimps [mult_assoc, mult_eq_1_iff]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   554
qed "dvd_anti_sym";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   555
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 6073
diff changeset
   556
Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   557
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
   558
qed "dvd_add";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   559
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 6073
diff changeset
   560
Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   561
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
   562
qed "dvd_diff";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   563
10789
260fa2c67e3e Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents: 10600
diff changeset
   564
Goal "[| k dvd m-n; k dvd n; n<=m |] ==> k dvd (m::nat)";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3427
diff changeset
   565
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   566
by (blast_tac (claset() addIs [dvd_add]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   567
qed "dvd_diffD";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   568
11365
6d5698df0413 new material from the Sylow proof
paulson
parents: 11313
diff changeset
   569
Goal "[| k dvd m-n; k dvd m; n<=m |] ==> k dvd (n::nat)";
6d5698df0413 new material from the Sylow proof
paulson
parents: 11313
diff changeset
   570
by (dres_inst_tac [("m","m")] dvd_diff 1);
6d5698df0413 new material from the Sylow proof
paulson
parents: 11313
diff changeset
   571
by Auto_tac;  
6d5698df0413 new material from the Sylow proof
paulson
parents: 11313
diff changeset
   572
qed "dvd_diffD1";
6d5698df0413 new material from the Sylow proof
paulson
parents: 11313
diff changeset
   573
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 6073
diff changeset
   574
Goalw [dvd_def] "k dvd n ==> k dvd (m*n :: nat)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   575
by (blast_tac (claset() addIs [mult_left_commute]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   576
qed "dvd_mult";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   577
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 6073
diff changeset
   578
Goal "k dvd m ==> k dvd (m*n :: nat)";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   579
by (stac mult_commute 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   580
by (etac dvd_mult 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   581
qed "dvd_mult2";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   582
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   583
(* k dvd (m*k) *)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   584
AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   585
10789
260fa2c67e3e Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents: 10600
diff changeset
   586
Goal "(k dvd n + k) = (k dvd (n::nat))";
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7493
diff changeset
   587
by (rtac iffI 1);
23e090051cb8 isatool expandshort;
wenzelm
parents: 7493
diff changeset
   588
by (etac dvd_add 2);
23e090051cb8 isatool expandshort;
wenzelm
parents: 7493
diff changeset
   589
by (rtac dvd_refl 2);
7493
e6f74eebfab3 added theorem dvd_reduce
oheimb
parents: 7082
diff changeset
   590
by (subgoal_tac "n = (n+k)-k" 1);
e6f74eebfab3 added theorem dvd_reduce
oheimb
parents: 7082
diff changeset
   591
by  (Simp_tac 2);
7499
23e090051cb8 isatool expandshort;
wenzelm
parents: 7493
diff changeset
   592
by (etac ssubst 1);
23e090051cb8 isatool expandshort;
wenzelm
parents: 7493
diff changeset
   593
by (etac dvd_diff 1);
23e090051cb8 isatool expandshort;
wenzelm
parents: 7493
diff changeset
   594
by (rtac dvd_refl 1);
7493
e6f74eebfab3 added theorem dvd_reduce
oheimb
parents: 7082
diff changeset
   595
qed "dvd_reduce";
e6f74eebfab3 added theorem dvd_reduce
oheimb
parents: 7082
diff changeset
   596
11383
paulson
parents: 11373
diff changeset
   597
Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n";
paulson
parents: 11373
diff changeset
   598
by (div_undefined_case_tac "n=0" 1);
paulson
parents: 11373
diff changeset
   599
by Auto_tac; 
paulson
parents: 11373
diff changeset
   600
by (blast_tac (claset() addIs [mod_mult_distrib2 RS sym]) 1);  
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   601
qed "dvd_mod";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   602
10789
260fa2c67e3e Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents: 10600
diff changeset
   603
Goal "[| (k::nat) dvd m mod n;  k dvd n |] ==> k dvd m";
260fa2c67e3e Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents: 10600
diff changeset
   604
by (subgoal_tac "k dvd (m div n)*n + m mod n" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   605
by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2);
4356
0dfd34f0d33d Replaced n ~= 0 by 0 < n
nipkow
parents: 4089
diff changeset
   606
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
   607
qed "dvd_mod_imp_dvd";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   608
10789
260fa2c67e3e Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents: 10600
diff changeset
   609
Goal "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)";
9881
d9ea690001ce strengthened dvd_mod & proofed dvd_mod_iff
paulson
parents: 9870
diff changeset
   610
by (blast_tac (claset() addIs [dvd_mod_imp_dvd, dvd_mod]) 1); 
d9ea690001ce strengthened dvd_mod & proofed dvd_mod_iff
paulson
parents: 9870
diff changeset
   611
qed "dvd_mod_iff";
d9ea690001ce strengthened dvd_mod & proofed dvd_mod_iff
paulson
parents: 9870
diff changeset
   612
10789
260fa2c67e3e Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents: 10600
diff changeset
   613
Goalw [dvd_def]  "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n";
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   614
by (etac exE 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   615
by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   616
qed "dvd_mult_cancel";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   617
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11593
diff changeset
   618
Goal "0<m ==> (m*n dvd m) = (n = (1::nat))";
11396
48fc0db9b896 new lemmas
paulson
parents: 11383
diff changeset
   619
by Auto_tac;  
48fc0db9b896 new lemmas
paulson
parents: 11383
diff changeset
   620
by (subgoal_tac "m*n dvd m*1" 1);
48fc0db9b896 new lemmas
paulson
parents: 11383
diff changeset
   621
by (dtac dvd_mult_cancel 1); 
48fc0db9b896 new lemmas
paulson
parents: 11383
diff changeset
   622
by Auto_tac;  
48fc0db9b896 new lemmas
paulson
parents: 11383
diff changeset
   623
qed "dvd_mult_cancel1";
48fc0db9b896 new lemmas
paulson
parents: 11383
diff changeset
   624
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11593
diff changeset
   625
Goal "0<m ==> (n*m dvd m) = (n = (1::nat))";
11396
48fc0db9b896 new lemmas
paulson
parents: 11383
diff changeset
   626
by (stac mult_commute 1); 
48fc0db9b896 new lemmas
paulson
parents: 11383
diff changeset
   627
by (etac dvd_mult_cancel1 1); 
48fc0db9b896 new lemmas
paulson
parents: 11383
diff changeset
   628
qed "dvd_mult_cancel2";
48fc0db9b896 new lemmas
paulson
parents: 11383
diff changeset
   629
10789
260fa2c67e3e Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents: 10600
diff changeset
   630
Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)";
3718
d78cf498a88c Minor tidying to use Clarify_tac, etc.
paulson
parents: 3496
diff changeset
   631
by (Clarify_tac 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   632
by (res_inst_tac [("x","k*ka")] exI 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   633
by (asm_simp_tac (simpset() addsimps mult_ac) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   634
qed "mult_dvd_mono";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   635
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 6073
diff changeset
   636
Goalw [dvd_def] "(i*j :: nat) dvd k ==> i dvd k";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   637
by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   638
by (Blast_tac 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   639
qed "dvd_mult_left";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   640
11313
04c8da2e0917 new theorem dvd_mult_right
paulson
parents: 10964
diff changeset
   641
Goalw [dvd_def] "(i*j :: nat) dvd k ==> j dvd k";
04c8da2e0917 new theorem dvd_mult_right
paulson
parents: 10964
diff changeset
   642
by (Clarify_tac 1);
04c8da2e0917 new theorem dvd_mult_right
paulson
parents: 10964
diff changeset
   643
by (res_inst_tac [("x","i*k")] exI 1);
04c8da2e0917 new theorem dvd_mult_right
paulson
parents: 10964
diff changeset
   644
by (simp_tac (simpset() addsimps mult_ac) 1);
04c8da2e0917 new theorem dvd_mult_right
paulson
parents: 10964
diff changeset
   645
qed "dvd_mult_right";
04c8da2e0917 new theorem dvd_mult_right
paulson
parents: 10964
diff changeset
   646
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8860
diff changeset
   647
Goalw [dvd_def] "[| k dvd n; 0 < n |] ==> k <= (n::nat)";
3718
d78cf498a88c Minor tidying to use Clarify_tac, etc.
paulson
parents: 3496
diff changeset
   648
by (Clarify_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 4059
diff changeset
   649
by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff])));
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3427
diff changeset
   650
by (etac conjE 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3427
diff changeset
   651
by (rtac le_trans 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3427
diff changeset
   652
by (rtac (le_refl RS mult_le_mono) 2);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   653
by (etac Suc_leI 2);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   654
by (Simp_tac 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   655
qed "dvd_imp_le";
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   656
8935
548901d05a0e added type constraint ::nat because 0 is now overloaded
paulson
parents: 8860
diff changeset
   657
Goalw [dvd_def] "!!k::nat. (k dvd n) = (n mod k = 0)";
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   658
by (div_undefined_case_tac "k=0" 1);
3724
f33e301a89f5 Step_tac -> Safe_tac
paulson
parents: 3718
diff changeset
   659
by Safe_tac;
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   660
by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 7007
diff changeset
   661
by (res_inst_tac [("t","n"),("n1","k")] (mod_div_equality RS subst) 1);
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   662
by (stac mult_commute 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   663
by (Asm_simp_tac 1);
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
   664
qed "dvd_eq_mod_eq_0";
10195
325b6279ae4f new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents: 9912
diff changeset
   665
11593
ab08d61966b1 AddXIs [dvdI]; AddXEs [dvdE];
wenzelm
parents: 11464
diff changeset
   666
Goal "n dvd m ==> n * (m div n) = (m::nat)";
ab08d61966b1 AddXIs [dvdI]; AddXEs [dvdE];
wenzelm
parents: 11464
diff changeset
   667
by (subgoal_tac "m mod n = 0" 1);
ab08d61966b1 AddXIs [dvdI]; AddXEs [dvdE];
wenzelm
parents: 11464
diff changeset
   668
 by (asm_full_simp_tac (simpset() addsimps [mult_div_cancel]) 1);
ab08d61966b1 AddXIs [dvdI]; AddXEs [dvdE];
wenzelm
parents: 11464
diff changeset
   669
by (asm_full_simp_tac (HOL_basic_ss addsimps [dvd_eq_mod_eq_0]) 1);
ab08d61966b1 AddXIs [dvdI]; AddXEs [dvdE];
wenzelm
parents: 11464
diff changeset
   670
qed "dvd_mult_div_cancel";
ab08d61966b1 AddXIs [dvdI]; AddXEs [dvdE];
wenzelm
parents: 11464
diff changeset
   671
10195
325b6279ae4f new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents: 9912
diff changeset
   672
Goal "(m mod d = 0) = (EX q::nat. m = d*q)";
325b6279ae4f new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents: 9912
diff changeset
   673
by (auto_tac (claset(), 
325b6279ae4f new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents: 9912
diff changeset
   674
     simpset() addsimps [dvd_eq_mod_eq_0 RS sym, dvd_def]));  
325b6279ae4f new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents: 9912
diff changeset
   675
qed "mod_eq_0_iff";
325b6279ae4f new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents: 9912
diff changeset
   676
AddSDs [mod_eq_0_iff RS iffD1];
325b6279ae4f new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents: 9912
diff changeset
   677
325b6279ae4f new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents: 9912
diff changeset
   678
(*Loses information, namely we also have r<d provided d is nonzero*)
325b6279ae4f new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents: 9912
diff changeset
   679
Goal "(m mod d = r) ==> EX q::nat. m = r + q*d";
325b6279ae4f new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents: 9912
diff changeset
   680
by (cut_inst_tac [("m","m")] mod_div_equality 1);
325b6279ae4f new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents: 9912
diff changeset
   681
by (full_simp_tac (simpset() addsimps add_ac) 1); 
325b6279ae4f new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents: 9912
diff changeset
   682
by (blast_tac (claset() addIs [sym]) 1); 
325b6279ae4f new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents: 9912
diff changeset
   683
qed "mod_eqD";
325b6279ae4f new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents: 9912
diff changeset
   684