equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Quotient and remainder *} |
6 header {* Quotient and remainder *} |
7 |
7 |
8 theory QuotRem imports Main begin |
8 theory QuotRem imports Main begin |
9 |
|
10 text {* Derivation of quotient and remainder using program extraction. *} |
9 text {* Derivation of quotient and remainder using program extraction. *} |
11 |
10 |
12 lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n" |
11 lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n" |
13 apply (induct m) |
12 apply (induct m) |
14 apply (case_tac n) |
13 apply (case_tac n) |
44 @{thm [display] division_def [no_vars]} |
43 @{thm [display] division_def [no_vars]} |
45 The corresponding correctness theorem is |
44 The corresponding correctness theorem is |
46 @{thm [display] division_correctness [no_vars]} |
45 @{thm [display] division_correctness [no_vars]} |
47 *} |
46 *} |
48 |
47 |
49 generate_code |
48 code_module Div |
|
49 contains |
50 test = "division 9 2" |
50 test = "division 9 2" |
51 |
51 |
52 end |
52 end |