author | wenzelm |
Mon, 06 Sep 2010 14:18:16 +0200 | |
changeset 39157 | b98909faaea8 |
parent 36862 | src/HOL/Extraction/QuotRem.thy@952b2b102a0a |
child 45170 | 7dd207fe7b6e |
permissions | -rw-r--r-- |
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
36862
diff
changeset
|
1 |
(* Title: HOL/Proofs/Extraction/QuotRem.thy |
13405 | 2 |
Author: Stefan Berghofer, TU Muenchen |
3 |
*) |
|
4 |
||
5 |
header {* Quotient and remainder *} |
|
6 |
||
27436 | 7 |
theory QuotRem |
8 |
imports Util |
|
9 |
begin |
|
10 |
||
13405 | 11 |
text {* Derivation of quotient and remainder using program extraction. *} |
12 |
||
13931 | 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 |
|
17604 | 17 |
thus ?case by iprover |
13931 | 18 |
next |
19 |
case (Suc a) |
|
17604 | 20 |
then obtain r q where I: "a = Suc b * q + r" and "r \<le> b" by iprover |
13931 | 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 |
|
17604 | 25 |
thus ?case by iprover |
13931 | 26 |
next |
27 |
assume "r \<noteq> b" |
|
23373 | 28 |
with `r \<le> b` have "r < b" by (simp add: order_less_le) |
13931 | 29 |
with I have "Suc a = Suc b * q + (Suc r) \<and> (Suc r) \<le> b" by simp |
17604 | 30 |
thus ?case by iprover |
13931 | 31 |
qed |
32 |
qed |
|
13405 | 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 |
||
27982 | 43 |
lemma "division 9 2 = (0, 3)" by evaluation |
27436 | 44 |
lemma "division 9 2 = (0, 3)" by eval |
20593 | 45 |
|
13405 | 46 |
end |