equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 section \<open>Quotient and remainder\<close> |
5 section \<open>Quotient and remainder\<close> |
6 |
6 |
7 theory QuotRem |
7 theory QuotRem |
8 imports "HOL-Library.Old_Datatype" Util |
8 imports Util "HOL-Library.Realizers" |
9 begin |
9 begin |
10 |
10 |
11 text \<open>Derivation of quotient and remainder using program extraction.\<close> |
11 text \<open>Derivation of quotient and remainder using program extraction.\<close> |
12 |
12 |
13 theorem division: "\<exists>r q. a = Suc b * q + r \<and> r \<le> b" |
13 theorem division: "\<exists>r q. a = Suc b * q + r \<and> r \<le> b" |