src/HOL/Divides.thy
author paulson
Fri Sep 26 10:34:57 2003 +0200 (2003-09-26)
changeset 14208 144f45277d5a
parent 14131 a4fc8b1af5e7
child 14267 b963e9cee2a0
permissions -rw-r--r--
misc tidying
paulson@3366
     1
(*  Title:      HOL/Divides.thy
paulson@3366
     2
    ID:         $Id$
paulson@3366
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@6865
     4
    Copyright   1999  University of Cambridge
paulson@3366
     5
paulson@3366
     6
The division operators div, mod and the divides relation "dvd"
paulson@3366
     7
*)
paulson@3366
     8
nipkow@13152
     9
theory Divides = NatArith files("Divides_lemmas.ML"):
paulson@3366
    10
wenzelm@8902
    11
(*We use the same class for div and mod;
paulson@6865
    12
  moreover, dvd is defined whenever multiplication is*)
paulson@6865
    13
axclass
wenzelm@12338
    14
  div < type
paulson@6865
    15
nipkow@13152
    16
instance  nat :: div ..
nipkow@13152
    17
instance  nat :: plus_ac0
nipkow@13152
    18
proof qed (rule add_commute add_assoc add_0)+
paulson@6865
    19
paulson@3366
    20
consts
nipkow@13152
    21
  div  :: "'a::div \<Rightarrow> 'a \<Rightarrow> 'a"          (infixl 70)
nipkow@13152
    22
  mod  :: "'a::div \<Rightarrow> 'a \<Rightarrow> 'a"          (infixl 70)
nipkow@13152
    23
  dvd  :: "'a::times \<Rightarrow> 'a \<Rightarrow> bool"      (infixl 50)
paulson@3366
    24
paulson@3366
    25
paulson@3366
    26
defs
paulson@6865
    27
nipkow@13152
    28
  mod_def:   "m mod n == wfrec (trancl pred_nat)
paulson@7029
    29
                          (%f j. if j<n | n=0 then j else f (j-n)) m"
paulson@6865
    30
nipkow@13152
    31
  div_def:   "m div n == wfrec (trancl pred_nat) 
paulson@7029
    32
                          (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
paulson@3366
    33
paulson@6865
    34
(*The definition of dvd is polymorphic!*)
nipkow@13152
    35
  dvd_def:   "m dvd n == EX k. n = m*k"
paulson@3366
    36
paulson@10559
    37
(*This definition helps prove the harder properties of div and mod.
paulson@10559
    38
  It is copied from IntDiv.thy; should it be overloaded?*)
paulson@10559
    39
constdefs
paulson@10559
    40
  quorem :: "(nat*nat) * (nat*nat) => bool"
paulson@10559
    41
    "quorem == %((a,b), (q,r)).
paulson@10559
    42
                      a = b*q + r &
paulson@10559
    43
                      (if 0<b then 0<=r & r<b else b<r & r <=0)"
paulson@10559
    44
nipkow@13152
    45
use "Divides_lemmas.ML"
nipkow@13152
    46
paulson@14131
    47
declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]
paulson@14131
    48
nipkow@13152
    49
lemma split_div:
nipkow@13189
    50
 "P(n div k :: nat) =
nipkow@13189
    51
 ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
nipkow@13189
    52
 (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
nipkow@13189
    53
proof
nipkow@13189
    54
  assume P: ?P
nipkow@13189
    55
  show ?Q
nipkow@13189
    56
  proof (cases)
nipkow@13189
    57
    assume "k = 0"
nipkow@13189
    58
    with P show ?Q by(simp add:DIVISION_BY_ZERO_DIV)
nipkow@13189
    59
  next
nipkow@13189
    60
    assume not0: "k \<noteq> 0"
nipkow@13189
    61
    thus ?Q
nipkow@13189
    62
    proof (simp, intro allI impI)
nipkow@13189
    63
      fix i j
nipkow@13189
    64
      assume n: "n = k*i + j" and j: "j < k"
nipkow@13189
    65
      show "P i"
nipkow@13189
    66
      proof (cases)
nipkow@13189
    67
	assume "i = 0"
nipkow@13189
    68
	with n j P show "P i" by simp
nipkow@13189
    69
      next
nipkow@13189
    70
	assume "i \<noteq> 0"
nipkow@13189
    71
	with not0 n j P show "P i" by(simp add:add_ac)
nipkow@13189
    72
      qed
nipkow@13189
    73
    qed
nipkow@13189
    74
  qed
nipkow@13189
    75
next
nipkow@13189
    76
  assume Q: ?Q
nipkow@13189
    77
  show ?P
nipkow@13189
    78
  proof (cases)
nipkow@13189
    79
    assume "k = 0"
nipkow@13189
    80
    with Q show ?P by(simp add:DIVISION_BY_ZERO_DIV)
nipkow@13189
    81
  next
nipkow@13189
    82
    assume not0: "k \<noteq> 0"
nipkow@13189
    83
    with Q have R: ?R by simp
nipkow@13189
    84
    from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
nipkow@13517
    85
    show ?P by simp
nipkow@13189
    86
  qed
nipkow@13189
    87
qed
nipkow@13189
    88
berghofe@13882
    89
lemma split_div_lemma:
berghofe@13882
    90
  "0 < n \<Longrightarrow> (n * q <= m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"
berghofe@13882
    91
  apply (rule iffI)
berghofe@13882
    92
  apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
paulson@14208
    93
  apply (simp_all add: quorem_def, arith)
berghofe@13882
    94
  apply (rule conjI)
berghofe@13882
    95
  apply (rule_tac P="%x. n * (m div n) \<le> x" in
berghofe@13882
    96
    subst [OF mod_div_equality [of _ n]])
berghofe@13882
    97
  apply (simp only: add: mult_ac)
berghofe@13882
    98
  apply (rule_tac P="%x. x < n + n * (m div n)" in
berghofe@13882
    99
    subst [OF mod_div_equality [of _ n]])
berghofe@13882
   100
  apply (simp only: add: mult_ac add_ac)
paulson@14208
   101
  apply (rule add_less_mono1, simp)
berghofe@13882
   102
  done
berghofe@13882
   103
berghofe@13882
   104
theorem split_div':
berghofe@13882
   105
  "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
berghofe@13882
   106
   (\<exists>q. (n * q <= m \<and> m < n * (Suc q)) \<and> P q))"
berghofe@13882
   107
  apply (case_tac "0 < n")
berghofe@13882
   108
  apply (simp only: add: split_div_lemma)
berghofe@13882
   109
  apply (simp_all add: DIVISION_BY_ZERO_DIV)
berghofe@13882
   110
  done
berghofe@13882
   111
nipkow@13189
   112
lemma split_mod:
nipkow@13189
   113
 "P(n mod k :: nat) =
nipkow@13189
   114
 ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
nipkow@13189
   115
 (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
nipkow@13189
   116
proof
nipkow@13189
   117
  assume P: ?P
nipkow@13189
   118
  show ?Q
nipkow@13189
   119
  proof (cases)
nipkow@13189
   120
    assume "k = 0"
nipkow@13189
   121
    with P show ?Q by(simp add:DIVISION_BY_ZERO_MOD)
nipkow@13189
   122
  next
nipkow@13189
   123
    assume not0: "k \<noteq> 0"
nipkow@13189
   124
    thus ?Q
nipkow@13189
   125
    proof (simp, intro allI impI)
nipkow@13189
   126
      fix i j
nipkow@13189
   127
      assume "n = k*i + j" "j < k"
nipkow@13189
   128
      thus "P j" using not0 P by(simp add:add_ac mult_ac)
nipkow@13189
   129
    qed
nipkow@13189
   130
  qed
nipkow@13189
   131
next
nipkow@13189
   132
  assume Q: ?Q
nipkow@13189
   133
  show ?P
nipkow@13189
   134
  proof (cases)
nipkow@13189
   135
    assume "k = 0"
nipkow@13189
   136
    with Q show ?P by(simp add:DIVISION_BY_ZERO_MOD)
nipkow@13189
   137
  next
nipkow@13189
   138
    assume not0: "k \<noteq> 0"
nipkow@13189
   139
    with Q have R: ?R by simp
nipkow@13189
   140
    from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
nipkow@13517
   141
    show ?P by simp
nipkow@13189
   142
  qed
nipkow@13189
   143
qed
nipkow@13189
   144
berghofe@13882
   145
theorem mod_div_equality': "(m::nat) mod n = m - (m div n) * n"
berghofe@13882
   146
  apply (rule_tac P="%x. m mod n = x - (m div n) * n" in
berghofe@13882
   147
    subst [OF mod_div_equality [of _ n]])
berghofe@13882
   148
  apply arith
berghofe@13882
   149
  done
berghofe@13882
   150
nipkow@13189
   151
(*
nipkow@13189
   152
lemma split_div:
nipkow@13152
   153
assumes m: "m \<noteq> 0"
nipkow@13152
   154
shows "P(n div m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P i)"
nipkow@13152
   155
       (is "?P = ?Q")
nipkow@13152
   156
proof
nipkow@13152
   157
  assume P: ?P
nipkow@13152
   158
  show ?Q
nipkow@13152
   159
  proof (intro allI impI)
nipkow@13152
   160
    fix i j
nipkow@13152
   161
    assume n: "n = m*i + j" and j: "j < m"
nipkow@13152
   162
    show "P i"
nipkow@13152
   163
    proof (cases)
nipkow@13152
   164
      assume "i = 0"
nipkow@13152
   165
      with n j P show "P i" by simp
nipkow@13152
   166
    next
nipkow@13152
   167
      assume "i \<noteq> 0"
nipkow@13152
   168
      with n j P show "P i" by (simp add:add_ac div_mult_self1)
nipkow@13152
   169
    qed
nipkow@13152
   170
  qed
nipkow@13152
   171
next
nipkow@13152
   172
  assume Q: ?Q
nipkow@13152
   173
  from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
nipkow@13517
   174
  show ?P by simp
nipkow@13152
   175
qed
nipkow@13152
   176
nipkow@13152
   177
lemma split_mod:
nipkow@13152
   178
assumes m: "m \<noteq> 0"
nipkow@13152
   179
shows "P(n mod m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P j)"
nipkow@13152
   180
       (is "?P = ?Q")
nipkow@13152
   181
proof
nipkow@13152
   182
  assume P: ?P
nipkow@13152
   183
  show ?Q
nipkow@13152
   184
  proof (intro allI impI)
nipkow@13152
   185
    fix i j
nipkow@13152
   186
    assume "n = m*i + j" "j < m"
nipkow@13152
   187
    thus "P j" using m P by(simp add:add_ac mult_ac)
nipkow@13152
   188
  qed
nipkow@13152
   189
next
nipkow@13152
   190
  assume Q: ?Q
nipkow@13152
   191
  from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
nipkow@13517
   192
  show ?P by simp
nipkow@13152
   193
qed
nipkow@13189
   194
*)
paulson@3366
   195
end