1 theory IntEx2 |
|
2 imports "Quotient_Int" |
|
3 begin |
|
4 |
|
5 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*} |
|
6 |
|
7 (* |
|
8 context ring_1 |
|
9 begin |
|
10 |
|
11 |
|
12 definition |
|
13 of_int :: "int \<Rightarrow> 'a" |
|
14 where |
|
15 "of_int |
|
16 *) |
|
17 |
|
18 |
|
19 subsection {* Binary representation *} |
|
20 |
|
21 text {* |
|
22 This formalization defines binary arithmetic in terms of the integers |
|
23 rather than using a datatype. This avoids multiple representations (leading |
|
24 zeroes, etc.) See @{text "ZF/Tools/twos-compl.ML"}, function @{text |
|
25 int_of_binary}, for the numerical interpretation. |
|
26 |
|
27 The representation expects that @{text "(m mod 2)"} is 0 or 1, |
|
28 even if m is negative; |
|
29 For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus |
|
30 @{text "-5 = (-3)*2 + 1"}. |
|
31 |
|
32 This two's complement binary representation derives from the paper |
|
33 "An Efficient Representation of Arithmetic for Term Rewriting" by |
|
34 Dave Cohen and Phil Watson, Rewriting Techniques and Applications, |
|
35 Springer LNCS 488 (240-251), 1991. |
|
36 *} |
|
37 |
|
38 subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *} |
|
39 |
|
40 definition |
|
41 Pls :: int where |
|
42 [code del]: "Pls = 0" |
|
43 |
|
44 definition |
|
45 Min :: int where |
|
46 [code del]: "Min = - 1" |
|
47 |
|
48 definition |
|
49 Bit0 :: "int \<Rightarrow> int" where |
|
50 [code del]: "Bit0 k = k + k" |
|
51 |
|
52 definition |
|
53 Bit1 :: "int \<Rightarrow> int" where |
|
54 [code del]: "Bit1 k = 1 + k + k" |
|
55 |
|
56 class number = -- {* for numeric types: nat, int, real, \dots *} |
|
57 fixes number_of :: "int \<Rightarrow> 'a" |
|
58 |
|
59 (*use "~~/src/HOL/Tools/numeral.ML" |
|
60 |
|
61 syntax |
|
62 "_Numeral" :: "num_const \<Rightarrow> 'a" ("_") |
|
63 |
|
64 use "~~/src/HOL/Tools/numeral_syntax.ML" |
|
65 |
|
66 setup NumeralSyntax.setup |
|
67 |
|
68 abbreviation |
|
69 "Numeral0 \<equiv> number_of Pls" |
|
70 |
|
71 abbreviation |
|
72 "Numeral1 \<equiv> number_of (Bit1 Pls)" |
|
73 |
|
74 lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)" |
|
75 -- {* Unfold all @{text let}s involving constants *} |
|
76 unfolding Let_def .. |
|
77 |
|
78 definition |
|
79 succ :: "int \<Rightarrow> int" where |
|
80 [code del]: "succ k = k + 1" |
|
81 |
|
82 definition |
|
83 pred :: "int \<Rightarrow> int" where |
|
84 [code del]: "pred k = k - 1" |
|
85 |
|
86 lemmas |
|
87 max_number_of [simp] = max_def |
|
88 [of "number_of u" "number_of v", standard, simp] |
|
89 and |
|
90 min_number_of [simp] = min_def |
|
91 [of "number_of u" "number_of v", standard, simp] |
|
92 -- {* unfolding @{text minx} and @{text max} on numerals *} |
|
93 |
|
94 lemmas numeral_simps = |
|
95 succ_def pred_def Pls_def Min_def Bit0_def Bit1_def |
|
96 |
|
97 text {* Removal of leading zeroes *} |
|
98 |
|
99 lemma Bit0_Pls [simp, code_post]: |
|
100 "Bit0 Pls = Pls" |
|
101 unfolding numeral_simps by simp |
|
102 |
|
103 lemma Bit1_Min [simp, code_post]: |
|
104 "Bit1 Min = Min" |
|
105 unfolding numeral_simps by simp |
|
106 |
|
107 lemmas normalize_bin_simps = |
|
108 Bit0_Pls Bit1_Min |
|
109 *) |
|
110 |
|
111 end |
|