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.
     1 (*  Title:      HOL/Divides.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1999  University of Cambridge
     5 
     6 The division operators div, mod and the divides relation "dvd"
     7 *)
     8 
     9 theory Divides = NatArith files("Divides_lemmas.ML"):
    10 
    11 (*We use the same class for div and mod;
    12   moreover, dvd is defined whenever multiplication is*)
    13 axclass
    14   div < type
    15 
    16 instance  nat :: div ..
    17 instance  nat :: plus_ac0
    18 proof qed (rule add_commute add_assoc add_0)+
    19 
    20 consts
    21   div  :: "'a::div \<Rightarrow> 'a \<Rightarrow> 'a"          (infixl 70)
    22   mod  :: "'a::div \<Rightarrow> 'a \<Rightarrow> 'a"          (infixl 70)
    23   dvd  :: "'a::times \<Rightarrow> 'a \<Rightarrow> bool"      (infixl 50)
    24 
    25 
    26 defs
    27 
    28   mod_def:   "m mod n == wfrec (trancl pred_nat)
    29                           (%f j. if j<n | n=0 then j else f (j-n)) m"
    30 
    31   div_def:   "m div n == wfrec (trancl pred_nat) 
    32                           (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
    33 
    34 (*The definition of dvd is polymorphic!*)
    35   dvd_def:   "m dvd n == EX k. n = m*k"
    36 
    37 (*This definition helps prove the harder properties of div and mod.
    38   It is copied from IntDiv.thy; should it be overloaded?*)
    39 constdefs
    40   quorem :: "(nat*nat) * (nat*nat) => bool"
    41     "quorem == %((a,b), (q,r)).
    42                       a = b*q + r &
    43                       (if 0<b then 0<=r & r<b else b<r & r <=0)"
    44 
    45 use "Divides_lemmas.ML"
    46 
    47 lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
    48 apply(insert mod_div_equality[of m n])
    49 apply(simp only:mult_ac)
    50 done
    51 
    52 lemma split_div:
    53  "P(n div k :: nat) =
    54  ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
    55  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
    56 proof
    57   assume P: ?P
    58   show ?Q
    59   proof (cases)
    60     assume "k = 0"
    61     with P show ?Q by(simp add:DIVISION_BY_ZERO_DIV)
    62   next
    63     assume not0: "k \<noteq> 0"
    64     thus ?Q
    65     proof (simp, intro allI impI)
    66       fix i j
    67       assume n: "n = k*i + j" and j: "j < k"
    68       show "P i"
    69       proof (cases)
    70 	assume "i = 0"
    71 	with n j P show "P i" by simp
    72       next
    73 	assume "i \<noteq> 0"
    74 	with not0 n j P show "P i" by(simp add:add_ac)
    75       qed
    76     qed
    77   qed
    78 next
    79   assume Q: ?Q
    80   show ?P
    81   proof (cases)
    82     assume "k = 0"
    83     with Q show ?P by(simp add:DIVISION_BY_ZERO_DIV)
    84   next
    85     assume not0: "k \<noteq> 0"
    86     with Q have R: ?R by simp
    87     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
    88     show ?P by(simp add:mod_div_equality2)
    89   qed
    90 qed
    91 
    92 lemma split_mod:
    93  "P(n mod k :: nat) =
    94  ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
    95  (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
    96 proof
    97   assume P: ?P
    98   show ?Q
    99   proof (cases)
   100     assume "k = 0"
   101     with P show ?Q by(simp add:DIVISION_BY_ZERO_MOD)
   102   next
   103     assume not0: "k \<noteq> 0"
   104     thus ?Q
   105     proof (simp, intro allI impI)
   106       fix i j
   107       assume "n = k*i + j" "j < k"
   108       thus "P j" using not0 P by(simp add:add_ac mult_ac)
   109     qed
   110   qed
   111 next
   112   assume Q: ?Q
   113   show ?P
   114   proof (cases)
   115     assume "k = 0"
   116     with Q show ?P by(simp add:DIVISION_BY_ZERO_MOD)
   117   next
   118     assume not0: "k \<noteq> 0"
   119     with Q have R: ?R by simp
   120     from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
   121     show ?P by(simp add:mod_div_equality2)
   122   qed
   123 qed
   124 
   125 (*
   126 lemma split_div:
   127 assumes m: "m \<noteq> 0"
   128 shows "P(n div m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P i)"
   129        (is "?P = ?Q")
   130 proof
   131   assume P: ?P
   132   show ?Q
   133   proof (intro allI impI)
   134     fix i j
   135     assume n: "n = m*i + j" and j: "j < m"
   136     show "P i"
   137     proof (cases)
   138       assume "i = 0"
   139       with n j P show "P i" by simp
   140     next
   141       assume "i \<noteq> 0"
   142       with n j P show "P i" by (simp add:add_ac div_mult_self1)
   143     qed
   144   qed
   145 next
   146   assume Q: ?Q
   147   from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
   148   show ?P by(simp add:mod_div_equality2)
   149 qed
   150 
   151 lemma split_mod:
   152 assumes m: "m \<noteq> 0"
   153 shows "P(n mod m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P j)"
   154        (is "?P = ?Q")
   155 proof
   156   assume P: ?P
   157   show ?Q
   158   proof (intro allI impI)
   159     fix i j
   160     assume "n = m*i + j" "j < m"
   161     thus "P j" using m P by(simp add:add_ac mult_ac)
   162   qed
   163 next
   164   assume Q: ?Q
   165   from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
   166   show ?P by(simp add:mod_div_equality2)
   167 qed
   168 *)
   169 end