equal
deleted
inserted
replaced
|
1 (* Title: HOL/Proofs/Extraction/QuotRem.thy |
|
2 Author: Stefan Berghofer, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* Quotient and remainder *} |
|
6 |
|
7 theory QuotRem |
|
8 imports Util |
|
9 begin |
|
10 |
|
11 text {* Derivation of quotient and remainder using program extraction. *} |
|
12 |
|
13 theorem division: "\<exists>r q. a = Suc b * q + r \<and> r \<le> b" |
|
14 proof (induct a) |
|
15 case 0 |
|
16 have "0 = Suc b * 0 + 0 \<and> 0 \<le> b" by simp |
|
17 thus ?case by iprover |
|
18 next |
|
19 case (Suc a) |
|
20 then obtain r q where I: "a = Suc b * q + r" and "r \<le> b" by iprover |
|
21 from nat_eq_dec show ?case |
|
22 proof |
|
23 assume "r = b" |
|
24 with I have "Suc a = Suc b * (Suc q) + 0 \<and> 0 \<le> b" by simp |
|
25 thus ?case by iprover |
|
26 next |
|
27 assume "r \<noteq> b" |
|
28 with `r \<le> b` have "r < b" by (simp add: order_less_le) |
|
29 with I have "Suc a = Suc b * q + (Suc r) \<and> (Suc r) \<le> b" by simp |
|
30 thus ?case by iprover |
|
31 qed |
|
32 qed |
|
33 |
|
34 extract division |
|
35 |
|
36 text {* |
|
37 The program extracted from the above proof looks as follows |
|
38 @{thm [display] division_def [no_vars]} |
|
39 The corresponding correctness theorem is |
|
40 @{thm [display] division_correctness [no_vars]} |
|
41 *} |
|
42 |
|
43 lemma "division 9 2 = (0, 3)" by evaluation |
|
44 lemma "division 9 2 = (0, 3)" by eval |
|
45 |
|
46 end |