equal
deleted
inserted
replaced
3 Author: Stefan Berghofer, TU Muenchen |
3 Author: Stefan Berghofer, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Quotient and remainder *} |
6 header {* Quotient and remainder *} |
7 |
7 |
8 theory QuotRem imports Util begin |
8 theory QuotRem |
|
9 imports Util |
|
10 begin |
|
11 |
9 text {* Derivation of quotient and remainder using program extraction. *} |
12 text {* Derivation of quotient and remainder using program extraction. *} |
10 |
13 |
11 theorem division: "\<exists>r q. a = Suc b * q + r \<and> r \<le> b" |
14 theorem division: "\<exists>r q. a = Suc b * q + r \<and> r \<le> b" |
12 proof (induct a) |
15 proof (induct a) |
13 case 0 |
16 case 0 |
40 |
43 |
41 code_module Div |
44 code_module Div |
42 contains |
45 contains |
43 test = "division 9 2" |
46 test = "division 9 2" |
44 |
47 |
45 export_code division in SML |
48 lemma "division 9 2 = (0, 3)" by eval |
46 |
49 |
47 end |
50 end |