equal
deleted
inserted
replaced
41 "quorem == %((a,b), (q,r)). |
41 "quorem == %((a,b), (q,r)). |
42 a = b*q + r & |
42 a = b*q + r & |
43 (if 0<b then 0<=r & r<b else b<r & r <=0)" |
43 (if 0<b then 0<=r & r<b else b<r & r <=0)" |
44 |
44 |
45 use "Divides_lemmas.ML" |
45 use "Divides_lemmas.ML" |
|
46 |
|
47 declare dvdI [intro?] dvdE [elim?] dvd_trans [trans] |
46 |
48 |
47 lemma split_div: |
49 lemma split_div: |
48 "P(n div k :: nat) = |
50 "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)))" |
51 ((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))") |
52 (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))") |