author  haftmann 
Sat, 05 Jul 2014 11:01:53 +0200  
changeset 57514  bdc2c6b40bf2 
parent 45170  7dd207fe7b6e 
child 58889  5b7a9633cfa8 
permissions  rwrr 
39157
b98909faaea8
more explicit HOLProofs 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 

27436  43 
lemma "division 9 2 = (0, 3)" by eval 
20593  44 

13405  45 
end 