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