src/HOL/Divides.thy
author nipkow
Wed May 15 13:49:51 2002 +0200 (2002-05-15)
changeset 13152 2a54f99b44b3
parent 12338 de0f4a63baa5
child 13189 81ed5c6de890
permissions -rw-r--r--
Divides.ML -> Divides_lemmas.ML
Converted Divides.thy to Isar.
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@13152
    53
assumes m: "m \<noteq> 0"
nipkow@13152
    54
shows "P(n div m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P i)"
nipkow@13152
    55
       (is "?P = ?Q")
nipkow@13152
    56
proof
nipkow@13152
    57
  assume P: ?P
nipkow@13152
    58
  show ?Q
nipkow@13152
    59
  proof (intro allI impI)
nipkow@13152
    60
    fix i j
nipkow@13152
    61
    assume n: "n = m*i + j" and j: "j < m"
nipkow@13152
    62
    show "P i"
nipkow@13152
    63
    proof (cases)
nipkow@13152
    64
      assume "i = 0"
nipkow@13152
    65
      with n j P show "P i" by simp
nipkow@13152
    66
    next
nipkow@13152
    67
      assume "i \<noteq> 0"
nipkow@13152
    68
      with n j P show "P i" by (simp add:add_ac div_mult_self1)
nipkow@13152
    69
    qed
nipkow@13152
    70
  qed
nipkow@13152
    71
next
nipkow@13152
    72
  assume Q: ?Q
nipkow@13152
    73
  from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
nipkow@13152
    74
  show ?P by(simp add:mod_div_equality2)
nipkow@13152
    75
qed
nipkow@13152
    76
nipkow@13152
    77
lemma split_mod:
nipkow@13152
    78
assumes m: "m \<noteq> 0"
nipkow@13152
    79
shows "P(n mod m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P j)"
nipkow@13152
    80
       (is "?P = ?Q")
nipkow@13152
    81
proof
nipkow@13152
    82
  assume P: ?P
nipkow@13152
    83
  show ?Q
nipkow@13152
    84
  proof (intro allI impI)
nipkow@13152
    85
    fix i j
nipkow@13152
    86
    assume "n = m*i + j" "j < m"
nipkow@13152
    87
    thus "P j" using m P by(simp add:add_ac mult_ac)
nipkow@13152
    88
  qed
nipkow@13152
    89
next
nipkow@13152
    90
  assume Q: ?Q
nipkow@13152
    91
  from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
nipkow@13152
    92
  show ?P by(simp add:mod_div_equality2)
nipkow@13152
    93
qed
nipkow@13152
    94
paulson@3366
    95
end