- Installed specific code generator for equality enforcing that
arguments do not have function types, which would result in
an error message during compilation.
- Added test case generators for basic types.
(* Title: HOL/Extraction/QuotRem.thy
ID: $Id$
Author: Stefan Berghofer, TU Muenchen
*)
header {* Quotient and remainder *}
theory QuotRem = Main:
text {* Derivation of quotient and remainder using program extraction. *}
lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
apply (induct m)
apply (case_tac n)
apply (case_tac [3] na)
apply (simp only: nat.simps, rules?)+
done
theorem division: "\<exists>r q. a = Suc b * q + r \<and> r \<le> b"
proof (induct a)
case 0
have "0 = Suc b * 0 + 0 \<and> 0 \<le> b" by simp
thus ?case by rules
next
case (Suc a)
then obtain r q where I: "a = Suc b * q + r" and "r \<le> b" by rules
from nat_eq_dec show ?case
proof
assume "r = b"
with I have "Suc a = Suc b * (Suc q) + 0 \<and> 0 \<le> b" by simp
thus ?case by rules
next
assume "r \<noteq> b"
hence "r < b" by (simp add: order_less_le)
with I have "Suc a = Suc b * q + (Suc r) \<and> (Suc r) \<le> b" by simp
thus ?case by rules
qed
qed
extract division
text {*
The program extracted from the above proof looks as follows
@{thm [display] division_def [no_vars]}
The corresponding correctness theorem is
@{thm [display] division_correctness [no_vars]}
*}
generate_code
test = "division 9 2"
end