19 "bit n False = 2 * n" |
19 "bit n False = 2 * n" |
20 "bit n True = 2 * n + 1" |
20 "bit n True = 2 * n + 1" |
21 unfolding bit_def by simp_all |
21 unfolding bit_def by simp_all |
22 |
22 |
23 ML {* |
23 ML {* |
|
24 structure Binary = |
|
25 struct |
24 fun dest_bit (Const ("False", _)) = 0 |
26 fun dest_bit (Const ("False", _)) = 0 |
25 | dest_bit (Const ("True", _)) = 1 |
27 | dest_bit (Const ("True", _)) = 1 |
26 | dest_bit t = raise TERM ("dest_bit", [t]); |
28 | dest_bit t = raise TERM ("dest_bit", [t]); |
27 |
29 |
28 fun dest_binary (Const (@{const_name HOL.zero}, Type ("nat", _))) = 0 |
30 fun dest_binary (Const (@{const_name HOL.zero}, Type ("nat", _))) = 0 |
122 Goal.prove ctxt [] [] prop (fn _ => ALLGOALS (full_simp_tac binary_ss)); |
125 Goal.prove ctxt [] [] prop (fn _ => ALLGOALS (full_simp_tac binary_ss)); |
123 |
126 |
124 fun binary_proc proc ss ct = |
127 fun binary_proc proc ss ct = |
125 (case Thm.term_of ct of |
128 (case Thm.term_of ct of |
126 _ $ t $ u => |
129 _ $ t $ u => |
127 (case try (pairself (`dest_binary)) (t, u) of |
130 (case try (pairself (`Binary.dest_binary)) (t, u) of |
128 SOME args => proc (Simplifier.the_context ss) args |
131 SOME args => proc (Simplifier.the_context ss) args |
129 | NONE => NONE) |
132 | NONE => NONE) |
130 | _ => NONE); |
133 | _ => NONE); |
131 in |
134 in |
132 |
135 |
133 val less_eq_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) => |
136 val less_eq_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) => |
134 let val k = n - m in |
137 let val k = n - m in |
135 if k >= 0 then |
138 if k >= 0 then |
136 SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (mk_binary k))]) |
139 SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (Binary.mk_binary k))]) |
137 else |
140 else |
138 SOME (@{thm binary_less_eq(2)} OF |
141 SOME (@{thm binary_less_eq(2)} OF |
139 [prove ctxt (t == plus (plus u (mk_binary (~ k - 1))) (mk_binary 1))]) |
142 [prove ctxt (t == plus (plus u (Binary.mk_binary (~ k - 1))) (Binary.mk_binary 1))]) |
140 end); |
143 end); |
141 |
144 |
142 val less_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) => |
145 val less_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) => |
143 let val k = m - n in |
146 let val k = m - n in |
144 if k >= 0 then |
147 if k >= 0 then |
145 SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (mk_binary k))]) |
148 SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (Binary.mk_binary k))]) |
146 else |
149 else |
147 SOME (@{thm binary_less(2)} OF |
150 SOME (@{thm binary_less(2)} OF |
148 [prove ctxt (u == plus (plus t (mk_binary (~ k - 1))) (mk_binary 1))]) |
151 [prove ctxt (u == plus (plus t (Binary.mk_binary (~ k - 1))) (Binary.mk_binary 1))]) |
149 end); |
152 end); |
150 |
153 |
151 val diff_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) => |
154 val diff_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) => |
152 let val k = m - n in |
155 let val k = m - n in |
153 if k >= 0 then |
156 if k >= 0 then |
154 SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (mk_binary k))]) |
157 SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (Binary.mk_binary k))]) |
155 else |
158 else |
156 SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (mk_binary (~ k)))]) |
159 SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (Binary.mk_binary (~ k)))]) |
157 end); |
160 end); |
158 |
161 |
159 fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) => |
162 fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) => |
160 if n = 0 then NONE |
163 if n = 0 then NONE |
161 else |
164 else |
162 let val (k, l) = IntInf.divMod (m, n) |
165 let val (k, l) = IntInf.divMod (m, n) |
163 in SOME (rule OF [prove ctxt (t == plus (mult u (mk_binary k)) (mk_binary l))]) end); |
166 in SOME (rule OF [prove ctxt (t == plus (mult u (Binary.mk_binary k)) (Binary.mk_binary l))]) end); |
164 |
167 |
165 end; |
168 end; |
166 *} |
169 *} |
167 |
170 |
168 simproc_setup binary_nat_less_eq ("m <= (n::nat)") = {* K less_eq_proc *} |
171 simproc_setup binary_nat_less_eq ("m <= (n::nat)") = {* K less_eq_proc *} |
197 |
200 |
198 fun binary_tr [Const (num, _)] = |
201 fun binary_tr [Const (num, _)] = |
199 let |
202 let |
200 val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num; |
203 val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num; |
201 val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num); |
204 val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num); |
202 in syntax_consts (mk_binary n) end |
205 in syntax_consts (Binary.mk_binary n) end |
203 | binary_tr ts = raise TERM ("binary_tr", ts); |
206 | binary_tr ts = raise TERM ("binary_tr", ts); |
204 |
207 |
205 in [("_Binary", binary_tr)] end |
208 in [("_Binary", binary_tr)] end |
206 *} |
209 *} |
207 |
210 |