author | wenzelm |
Fri, 01 Jul 2016 16:52:35 +0200 | |
changeset 63361 | d10eab0672f9 |
parent 61986 | 2461779da2b8 |
child 66258 | 2b83dd24b301 |
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 |
||
61986 | 5 |
section \<open>Quotient and remainder\<close> |
13405 | 6 |
|
27436 | 7 |
theory QuotRem |
8 |
imports Util |
|
9 |
begin |
|
10 |
||
61986 | 11 |
text \<open>Derivation of quotient and remainder using program extraction.\<close> |
13405 | 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 |
|
63361 | 17 |
then show ?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 |
|
63361 | 25 |
then show ?case by iprover |
13931 | 26 |
next |
27 |
assume "r \<noteq> b" |
|
61986 | 28 |
with \<open>r \<le> b\<close> 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 |
63361 | 30 |
then show ?case by iprover |
13931 | 31 |
qed |
32 |
qed |
|
13405 | 33 |
|
34 |
extract division |
|
35 |
||
61986 | 36 |
text \<open> |
13405 | 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]} |
|
61986 | 41 |
\<close> |
13405 | 42 |
|
27436 | 43 |
lemma "division 9 2 = (0, 3)" by eval |
20593 | 44 |
|
13405 | 45 |
end |