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