src/HOL/Divides.thy
author nipkow
Fri May 31 07:53:37 2002 +0200 (2002-05-31)
changeset 13189 81ed5c6de890
parent 13152 2a54f99b44b3
child 13517 42efec18f5b2
permissions -rw-r--r--
Now arith can deal with div/mod arbitrary nat numerals.
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
nipkow@13152
    47
lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
nipkow@13152
    48
apply(insert mod_div_equality[of m n])
nipkow@13152
    49
apply(simp only:mult_ac)
nipkow@13152
    50
done
nipkow@13152
    51
nipkow@13152
    52
lemma split_div:
nipkow@13189
    53
 "P(n div k :: nat) =
nipkow@13189
    54
 ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
nipkow@13189
    55
 (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
nipkow@13189
    56
proof
nipkow@13189
    57
  assume P: ?P
nipkow@13189
    58
  show ?Q
nipkow@13189
    59
  proof (cases)
nipkow@13189
    60
    assume "k = 0"
nipkow@13189
    61
    with P show ?Q by(simp add:DIVISION_BY_ZERO_DIV)
nipkow@13189
    62
  next
nipkow@13189
    63
    assume not0: "k \<noteq> 0"
nipkow@13189
    64
    thus ?Q
nipkow@13189
    65
    proof (simp, intro allI impI)
nipkow@13189
    66
      fix i j
nipkow@13189
    67
      assume n: "n = k*i + j" and j: "j < k"
nipkow@13189
    68
      show "P i"
nipkow@13189
    69
      proof (cases)
nipkow@13189
    70
	assume "i = 0"
nipkow@13189
    71
	with n j P show "P i" by simp
nipkow@13189
    72
      next
nipkow@13189
    73
	assume "i \<noteq> 0"
nipkow@13189
    74
	with not0 n j P show "P i" by(simp add:add_ac)
nipkow@13189
    75
      qed
nipkow@13189
    76
    qed
nipkow@13189
    77
  qed
nipkow@13189
    78
next
nipkow@13189
    79
  assume Q: ?Q
nipkow@13189
    80
  show ?P
nipkow@13189
    81
  proof (cases)
nipkow@13189
    82
    assume "k = 0"
nipkow@13189
    83
    with Q show ?P by(simp add:DIVISION_BY_ZERO_DIV)
nipkow@13189
    84
  next
nipkow@13189
    85
    assume not0: "k \<noteq> 0"
nipkow@13189
    86
    with Q have R: ?R by simp
nipkow@13189
    87
    from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
nipkow@13189
    88
    show ?P by(simp add:mod_div_equality2)
nipkow@13189
    89
  qed
nipkow@13189
    90
qed
nipkow@13189
    91
nipkow@13189
    92
lemma split_mod:
nipkow@13189
    93
 "P(n mod k :: nat) =
nipkow@13189
    94
 ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
nipkow@13189
    95
 (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
nipkow@13189
    96
proof
nipkow@13189
    97
  assume P: ?P
nipkow@13189
    98
  show ?Q
nipkow@13189
    99
  proof (cases)
nipkow@13189
   100
    assume "k = 0"
nipkow@13189
   101
    with P show ?Q by(simp add:DIVISION_BY_ZERO_MOD)
nipkow@13189
   102
  next
nipkow@13189
   103
    assume not0: "k \<noteq> 0"
nipkow@13189
   104
    thus ?Q
nipkow@13189
   105
    proof (simp, intro allI impI)
nipkow@13189
   106
      fix i j
nipkow@13189
   107
      assume "n = k*i + j" "j < k"
nipkow@13189
   108
      thus "P j" using not0 P by(simp add:add_ac mult_ac)
nipkow@13189
   109
    qed
nipkow@13189
   110
  qed
nipkow@13189
   111
next
nipkow@13189
   112
  assume Q: ?Q
nipkow@13189
   113
  show ?P
nipkow@13189
   114
  proof (cases)
nipkow@13189
   115
    assume "k = 0"
nipkow@13189
   116
    with Q show ?P by(simp add:DIVISION_BY_ZERO_MOD)
nipkow@13189
   117
  next
nipkow@13189
   118
    assume not0: "k \<noteq> 0"
nipkow@13189
   119
    with Q have R: ?R by simp
nipkow@13189
   120
    from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
nipkow@13189
   121
    show ?P by(simp add:mod_div_equality2)
nipkow@13189
   122
  qed
nipkow@13189
   123
qed
nipkow@13189
   124
nipkow@13189
   125
(*
nipkow@13189
   126
lemma split_div:
nipkow@13152
   127
assumes m: "m \<noteq> 0"
nipkow@13152
   128
shows "P(n div m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P i)"
nipkow@13152
   129
       (is "?P = ?Q")
nipkow@13152
   130
proof
nipkow@13152
   131
  assume P: ?P
nipkow@13152
   132
  show ?Q
nipkow@13152
   133
  proof (intro allI impI)
nipkow@13152
   134
    fix i j
nipkow@13152
   135
    assume n: "n = m*i + j" and j: "j < m"
nipkow@13152
   136
    show "P i"
nipkow@13152
   137
    proof (cases)
nipkow@13152
   138
      assume "i = 0"
nipkow@13152
   139
      with n j P show "P i" by simp
nipkow@13152
   140
    next
nipkow@13152
   141
      assume "i \<noteq> 0"
nipkow@13152
   142
      with n j P show "P i" by (simp add:add_ac div_mult_self1)
nipkow@13152
   143
    qed
nipkow@13152
   144
  qed
nipkow@13152
   145
next
nipkow@13152
   146
  assume Q: ?Q
nipkow@13152
   147
  from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
nipkow@13152
   148
  show ?P by(simp add:mod_div_equality2)
nipkow@13152
   149
qed
nipkow@13152
   150
nipkow@13152
   151
lemma split_mod:
nipkow@13152
   152
assumes m: "m \<noteq> 0"
nipkow@13152
   153
shows "P(n mod m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P j)"
nipkow@13152
   154
       (is "?P = ?Q")
nipkow@13152
   155
proof
nipkow@13152
   156
  assume P: ?P
nipkow@13152
   157
  show ?Q
nipkow@13152
   158
  proof (intro allI impI)
nipkow@13152
   159
    fix i j
nipkow@13152
   160
    assume "n = m*i + j" "j < m"
nipkow@13152
   161
    thus "P j" using m P by(simp add:add_ac mult_ac)
nipkow@13152
   162
  qed
nipkow@13152
   163
next
nipkow@13152
   164
  assume Q: ?Q
nipkow@13152
   165
  from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
nipkow@13152
   166
  show ?P by(simp add:mod_div_equality2)
nipkow@13152
   167
qed
nipkow@13189
   168
*)
paulson@3366
   169
end