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
```