src/HOL/Divides.thy
author paulson
Thu Jul 24 18:23:00 2003 +0200 (2003-07-24)
changeset 14131 a4fc8b1af5e7
parent 13882 2266550ab316
child 14208 144f45277d5a
permissions -rw-r--r--
declarations moved from PreList.thy
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)
berghofe@13882
    93
  apply (simp_all add: quorem_def)
berghofe@13882
    94
  apply arith
berghofe@13882
    95
  apply (rule conjI)
berghofe@13882
    96
  apply (rule_tac P="%x. n * (m div n) \<le> x" in
berghofe@13882
    97
    subst [OF mod_div_equality [of _ n]])
berghofe@13882
    98
  apply (simp only: add: mult_ac)
berghofe@13882
    99
  apply (rule_tac P="%x. x < n + n * (m div n)" in
berghofe@13882
   100
    subst [OF mod_div_equality [of _ n]])
berghofe@13882
   101
  apply (simp only: add: mult_ac add_ac)
berghofe@13882
   102
  apply (rule add_less_mono1)
berghofe@13882
   103
  apply simp
berghofe@13882
   104
  done
berghofe@13882
   105
berghofe@13882
   106
theorem split_div':
berghofe@13882
   107
  "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
berghofe@13882
   108
   (\<exists>q. (n * q <= m \<and> m < n * (Suc q)) \<and> P q))"
berghofe@13882
   109
  apply (case_tac "0 < n")
berghofe@13882
   110
  apply (simp only: add: split_div_lemma)
berghofe@13882
   111
  apply (simp_all add: DIVISION_BY_ZERO_DIV)
berghofe@13882
   112
  done
berghofe@13882
   113
nipkow@13189
   114
lemma split_mod:
nipkow@13189
   115
 "P(n mod k :: nat) =
nipkow@13189
   116
 ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
nipkow@13189
   117
 (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
nipkow@13189
   118
proof
nipkow@13189
   119
  assume P: ?P
nipkow@13189
   120
  show ?Q
nipkow@13189
   121
  proof (cases)
nipkow@13189
   122
    assume "k = 0"
nipkow@13189
   123
    with P show ?Q by(simp add:DIVISION_BY_ZERO_MOD)
nipkow@13189
   124
  next
nipkow@13189
   125
    assume not0: "k \<noteq> 0"
nipkow@13189
   126
    thus ?Q
nipkow@13189
   127
    proof (simp, intro allI impI)
nipkow@13189
   128
      fix i j
nipkow@13189
   129
      assume "n = k*i + j" "j < k"
nipkow@13189
   130
      thus "P j" using not0 P by(simp add:add_ac mult_ac)
nipkow@13189
   131
    qed
nipkow@13189
   132
  qed
nipkow@13189
   133
next
nipkow@13189
   134
  assume Q: ?Q
nipkow@13189
   135
  show ?P
nipkow@13189
   136
  proof (cases)
nipkow@13189
   137
    assume "k = 0"
nipkow@13189
   138
    with Q show ?P by(simp add:DIVISION_BY_ZERO_MOD)
nipkow@13189
   139
  next
nipkow@13189
   140
    assume not0: "k \<noteq> 0"
nipkow@13189
   141
    with Q have R: ?R by simp
nipkow@13189
   142
    from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
nipkow@13517
   143
    show ?P by simp
nipkow@13189
   144
  qed
nipkow@13189
   145
qed
nipkow@13189
   146
berghofe@13882
   147
theorem mod_div_equality': "(m::nat) mod n = m - (m div n) * n"
berghofe@13882
   148
  apply (rule_tac P="%x. m mod n = x - (m div n) * n" in
berghofe@13882
   149
    subst [OF mod_div_equality [of _ n]])
berghofe@13882
   150
  apply arith
berghofe@13882
   151
  done
berghofe@13882
   152
nipkow@13189
   153
(*
nipkow@13189
   154
lemma split_div:
nipkow@13152
   155
assumes m: "m \<noteq> 0"
nipkow@13152
   156
shows "P(n div m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P i)"
nipkow@13152
   157
       (is "?P = ?Q")
nipkow@13152
   158
proof
nipkow@13152
   159
  assume P: ?P
nipkow@13152
   160
  show ?Q
nipkow@13152
   161
  proof (intro allI impI)
nipkow@13152
   162
    fix i j
nipkow@13152
   163
    assume n: "n = m*i + j" and j: "j < m"
nipkow@13152
   164
    show "P i"
nipkow@13152
   165
    proof (cases)
nipkow@13152
   166
      assume "i = 0"
nipkow@13152
   167
      with n j P show "P i" by simp
nipkow@13152
   168
    next
nipkow@13152
   169
      assume "i \<noteq> 0"
nipkow@13152
   170
      with n j P show "P i" by (simp add:add_ac div_mult_self1)
nipkow@13152
   171
    qed
nipkow@13152
   172
  qed
nipkow@13152
   173
next
nipkow@13152
   174
  assume Q: ?Q
nipkow@13152
   175
  from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
nipkow@13517
   176
  show ?P by simp
nipkow@13152
   177
qed
nipkow@13152
   178
nipkow@13152
   179
lemma split_mod:
nipkow@13152
   180
assumes m: "m \<noteq> 0"
nipkow@13152
   181
shows "P(n mod m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P j)"
nipkow@13152
   182
       (is "?P = ?Q")
nipkow@13152
   183
proof
nipkow@13152
   184
  assume P: ?P
nipkow@13152
   185
  show ?Q
nipkow@13152
   186
  proof (intro allI impI)
nipkow@13152
   187
    fix i j
nipkow@13152
   188
    assume "n = m*i + j" "j < m"
nipkow@13152
   189
    thus "P j" using m P by(simp add:add_ac mult_ac)
nipkow@13152
   190
  qed
nipkow@13152
   191
next
nipkow@13152
   192
  assume Q: ?Q
nipkow@13152
   193
  from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
nipkow@13517
   194
  show ?P by simp
nipkow@13152
   195
qed
nipkow@13189
   196
*)
paulson@3366
   197
end