1(*  Title:      HOL/Proofs/Extraction/QuotRem.thy
2    Author:     Stefan Berghofer, TU Muenchen
3*)
4
5section \<open>Quotient and remainder\<close>
6
7theory QuotRem
8imports Util "HOL-Library.Realizers"
9begin
10
11text \<open>Derivation of quotient and remainder using program extraction.\<close>
12
13theorem division: "\<exists>r q. a = Suc b * q + r \<and> r \<le> b"
14proof (induct a)
15  case 0
16  have "0 = Suc b * 0 + 0 \<and> 0 \<le> b" by simp
17  then show ?case by iprover
18next
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    then show ?case by iprover
26  next
27    assume "r \<noteq> b"
28    with \<open>r \<le> b\<close> 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    then show ?case by iprover
31  qed
32qed
33
34extract division
35
36text \<open>
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\<close>
42
43lemma "division 9 2 = (0, 3)" by eval
44
45end
46