obsolete;
authorwenzelm
Wed May 29 23:11:21 2013 +0200 (2013-05-29)
changeset 522260d3165844048
parent 52225 568b2cd65d50
child 52227 f9e68ba3f004
obsolete;
src/HOL/ROOT
src/HOL/ex/Binary.thy
     1.1 --- a/src/HOL/ROOT	Wed May 29 18:55:37 2013 +0200
     1.2 +++ b/src/HOL/ROOT	Wed May 29 23:11:21 2013 +0200
     1.3 @@ -506,7 +506,6 @@
     1.4      Higher_Order_Logic
     1.5      Abstract_NAT
     1.6      Guess
     1.7 -    Binary
     1.8      Fundefs
     1.9      Induction_Schema
    1.10      LocaleTest2
     2.1 --- a/src/HOL/ex/Binary.thy	Wed May 29 18:55:37 2013 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,303 +0,0 @@
     2.4 -(*  Title:      HOL/ex/Binary.thy
     2.5 -    Author:     Makarius
     2.6 -*)
     2.7 -
     2.8 -header {* Simple and efficient binary numerals *}
     2.9 -
    2.10 -theory Binary
    2.11 -imports Main
    2.12 -begin
    2.13 -
    2.14 -subsection {* Binary representation of natural numbers *}
    2.15 -
    2.16 -definition
    2.17 -  bit :: "nat \<Rightarrow> bool \<Rightarrow> nat" where
    2.18 -  "bit n b = (if b then 2 * n + 1 else 2 * n)"
    2.19 -
    2.20 -lemma bit_simps:
    2.21 -    "bit n False = 2 * n"
    2.22 -    "bit n True = 2 * n + 1"
    2.23 -  unfolding bit_def by simp_all
    2.24 -
    2.25 -ML {*
    2.26 -  fun dest_bit (Const (@{const_name False}, _)) = 0
    2.27 -    | dest_bit (Const (@{const_name True}, _)) = 1
    2.28 -    | dest_bit t = raise TERM ("dest_bit", [t]);
    2.29 -
    2.30 -  fun dest_binary (Const (@{const_name Groups.zero}, Type (@{type_name nat}, _))) = 0
    2.31 -    | dest_binary (Const (@{const_name Groups.one}, Type (@{type_name nat}, _))) = 1
    2.32 -    | dest_binary (Const (@{const_name bit}, _) $ bs $ b) = 2 * dest_binary bs + dest_bit b
    2.33 -    | dest_binary t = raise TERM ("dest_binary", [t]);
    2.34 -
    2.35 -  fun mk_bit 0 = @{term False}
    2.36 -    | mk_bit 1 = @{term True}
    2.37 -    | mk_bit _ = raise TERM ("mk_bit", []);
    2.38 -
    2.39 -  fun mk_binary 0 = @{term "0::nat"}
    2.40 -    | mk_binary 1 = @{term "1::nat"}
    2.41 -    | mk_binary n =
    2.42 -        if n < 0 then raise TERM ("mk_binary", [])
    2.43 -        else
    2.44 -          let val (q, r) = Integer.div_mod n 2
    2.45 -          in @{term bit} $ mk_binary q $ mk_bit r end;
    2.46 -*}
    2.47 -
    2.48 -
    2.49 -subsection {* Direct operations -- plain normalization *}
    2.50 -
    2.51 -lemma binary_norm:
    2.52 -    "bit 0 False = 0"
    2.53 -    "bit 0 True = 1"
    2.54 -  unfolding bit_def by simp_all
    2.55 -
    2.56 -lemma binary_add:
    2.57 -    "n + 0 = n"
    2.58 -    "0 + n = n"
    2.59 -    "1 + 1 = bit 1 False"
    2.60 -    "bit n False + 1 = bit n True"
    2.61 -    "bit n True + 1 = bit (n + 1) False"
    2.62 -    "1 + bit n False = bit n True"
    2.63 -    "1 + bit n True = bit (n + 1) False"
    2.64 -    "bit m False + bit n False = bit (m + n) False"
    2.65 -    "bit m False + bit n True = bit (m + n) True"
    2.66 -    "bit m True + bit n False = bit (m + n) True"
    2.67 -    "bit m True + bit n True = bit ((m + n) + 1) False"
    2.68 -  by (simp_all add: bit_simps)
    2.69 -
    2.70 -lemma binary_mult:
    2.71 -    "n * 0 = 0"
    2.72 -    "0 * n = 0"
    2.73 -    "n * 1 = n"
    2.74 -    "1 * n = n"
    2.75 -    "bit m True * n = bit (m * n) False + n"
    2.76 -    "bit m False * n = bit (m * n) False"
    2.77 -    "n * bit m True = bit (m * n) False + n"
    2.78 -    "n * bit m False = bit (m * n) False"
    2.79 -  by (simp_all add: bit_simps)
    2.80 -
    2.81 -lemmas binary_simps = binary_norm binary_add binary_mult
    2.82 -
    2.83 -
    2.84 -subsection {* Indirect operations -- ML will produce witnesses *}
    2.85 -
    2.86 -lemma binary_less_eq:
    2.87 -  fixes n :: nat
    2.88 -  shows "n \<equiv> m + k \<Longrightarrow> (m \<le> n) \<equiv> True"
    2.89 -    and "m \<equiv> n + k + 1 \<Longrightarrow> (m \<le> n) \<equiv> False"
    2.90 -  by simp_all
    2.91 -
    2.92 -lemma binary_less:
    2.93 -  fixes n :: nat
    2.94 -  shows "m \<equiv> n + k \<Longrightarrow> (m < n) \<equiv> False"
    2.95 -    and "n \<equiv> m + k + 1 \<Longrightarrow> (m < n) \<equiv> True"
    2.96 -  by simp_all
    2.97 -
    2.98 -lemma binary_diff:
    2.99 -  fixes n :: nat
   2.100 -  shows "m \<equiv> n + k \<Longrightarrow> m - n \<equiv> k"
   2.101 -    and "n \<equiv> m + k \<Longrightarrow> m - n \<equiv> 0"
   2.102 -  by simp_all
   2.103 -
   2.104 -lemma binary_divmod:
   2.105 -  fixes n :: nat
   2.106 -  assumes "m \<equiv> n * k + l" and "0 < n" and "l < n"
   2.107 -  shows "m div n \<equiv> k"
   2.108 -    and "m mod n \<equiv> l"
   2.109 -proof -
   2.110 -  from `m \<equiv> n * k + l` have "m = l + k * n" by simp
   2.111 -  with `0 < n` and `l < n` show "m div n \<equiv> k" and "m mod n \<equiv> l" by simp_all
   2.112 -qed
   2.113 -
   2.114 -ML {*
   2.115 -local
   2.116 -  infix ==;
   2.117 -  val op == = Logic.mk_equals;
   2.118 -  fun plus m n = @{term "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"} $ m $ n;
   2.119 -  fun mult m n = @{term "times :: nat \<Rightarrow> nat \<Rightarrow> nat"} $ m $ n;
   2.120 -
   2.121 -  val binary_ss =
   2.122 -    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms binary_simps});
   2.123 -  fun prove ctxt prop =
   2.124 -    Goal.prove ctxt [] [] prop
   2.125 -      (fn _ => ALLGOALS (full_simp_tac (put_simpset binary_ss ctxt)));
   2.126 -
   2.127 -  fun binary_proc proc ctxt ct =
   2.128 -    (case Thm.term_of ct of
   2.129 -      _ $ t $ u =>
   2.130 -      (case try (pairself (`dest_binary)) (t, u) of
   2.131 -        SOME args => proc ctxt args
   2.132 -      | NONE => NONE)
   2.133 -    | _ => NONE);
   2.134 -in
   2.135 -
   2.136 -val less_eq_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   2.137 -  let val k = n - m in
   2.138 -    if k >= 0 then
   2.139 -      SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (mk_binary k))])
   2.140 -    else
   2.141 -      SOME (@{thm binary_less_eq(2)} OF
   2.142 -        [prove ctxt (t == plus (plus u (mk_binary (~ k - 1))) (mk_binary 1))])
   2.143 -  end);
   2.144 -
   2.145 -val less_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   2.146 -  let val k = m - n in
   2.147 -    if k >= 0 then
   2.148 -      SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (mk_binary k))])
   2.149 -    else
   2.150 -      SOME (@{thm binary_less(2)} OF
   2.151 -        [prove ctxt (u == plus (plus t (mk_binary (~ k - 1))) (mk_binary 1))])
   2.152 -  end);
   2.153 -
   2.154 -val diff_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   2.155 -  let val k = m - n in
   2.156 -    if k >= 0 then
   2.157 -      SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (mk_binary k))])
   2.158 -    else
   2.159 -      SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (mk_binary (~ k)))])
   2.160 -  end);
   2.161 -
   2.162 -fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
   2.163 -  if n = 0 then NONE
   2.164 -  else
   2.165 -    let val (k, l) = Integer.div_mod m n
   2.166 -    in SOME (rule OF [prove ctxt (t == plus (mult u (mk_binary k)) (mk_binary l))]) end);
   2.167 -
   2.168 -end;
   2.169 -*}
   2.170 -
   2.171 -simproc_setup binary_nat_less_eq ("m <= (n::nat)") = {* K less_eq_proc *}
   2.172 -simproc_setup binary_nat_less ("m < (n::nat)") = {* K less_proc *}
   2.173 -simproc_setup binary_nat_diff ("m - (n::nat)") = {* K diff_proc *}
   2.174 -simproc_setup binary_nat_div ("m div (n::nat)") = {* K (divmod_proc @{thm binary_divmod(1)}) *}
   2.175 -simproc_setup binary_nat_mod ("m mod (n::nat)") = {* K (divmod_proc @{thm binary_divmod(2)}) *}
   2.176 -
   2.177 -method_setup binary_simp = {*
   2.178 -  Scan.succeed (fn ctxt => SIMPLE_METHOD'
   2.179 -    (full_simp_tac
   2.180 -      (put_simpset HOL_basic_ss ctxt
   2.181 -        addsimps @{thms binary_simps}
   2.182 -        addsimprocs
   2.183 -         [@{simproc binary_nat_less_eq},
   2.184 -          @{simproc binary_nat_less},
   2.185 -          @{simproc binary_nat_diff},
   2.186 -          @{simproc binary_nat_div},
   2.187 -          @{simproc binary_nat_mod}])))
   2.188 -*}
   2.189 -
   2.190 -
   2.191 -subsection {* Concrete syntax *}
   2.192 -
   2.193 -syntax
   2.194 -  "_Binary" :: "num_const \<Rightarrow> 'a"    ("$_")
   2.195 -
   2.196 -parse_translation {*
   2.197 -  let
   2.198 -    val syntax_consts =
   2.199 -      map_aterms (fn Const (c, T) => Const (Lexicon.mark_const c, T) | a => a);
   2.200 -
   2.201 -    fun binary_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ binary_tr [t] $ u
   2.202 -      | binary_tr [Const (num, _)] =
   2.203 -          let
   2.204 -            val {leading_zeros = z, value = n, ...} = Lexicon.read_xnum num;
   2.205 -            val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
   2.206 -          in syntax_consts (mk_binary n) end
   2.207 -      | binary_tr ts = raise TERM ("binary_tr", ts);
   2.208 -
   2.209 -  in [(@{syntax_const "_Binary"}, K binary_tr)] end
   2.210 -*}
   2.211 -
   2.212 -
   2.213 -subsection {* Examples *}
   2.214 -
   2.215 -lemma "$6 = 6"
   2.216 -  by (simp add: bit_simps)
   2.217 -
   2.218 -lemma "bit (bit (bit 0 False) False) True = 1"
   2.219 -  by (simp add: bit_simps)
   2.220 -
   2.221 -lemma "bit (bit (bit 0 False) False) True = bit 0 True"
   2.222 -  by (simp add: bit_simps)
   2.223 -
   2.224 -lemma "$5 + $3 = $8"
   2.225 -  by binary_simp
   2.226 -
   2.227 -lemma "$5 * $3 = $15"
   2.228 -  by binary_simp
   2.229 -
   2.230 -lemma "$5 - $3 = $2"
   2.231 -  by binary_simp
   2.232 -
   2.233 -lemma "$3 - $5 = 0"
   2.234 -  by binary_simp
   2.235 -
   2.236 -lemma "$123456789 - $123 = $123456666"
   2.237 -  by binary_simp
   2.238 -
   2.239 -lemma "$1111111111222222222233333333334444444444 - $998877665544332211 =
   2.240 -  $1111111111222222222232334455668900112233"
   2.241 -  by binary_simp
   2.242 -
   2.243 -lemma "(1111111111222222222233333333334444444444::nat) - 998877665544332211 =
   2.244 -  1111111111222222222232334455668900112233"
   2.245 -  by simp
   2.246 -
   2.247 -lemma "(1111111111222222222233333333334444444444::int) - 998877665544332211 =
   2.248 -  1111111111222222222232334455668900112233"
   2.249 -  by simp
   2.250 -
   2.251 -lemma "$1111111111222222222233333333334444444444 * $998877665544332211 =
   2.252 -    $1109864072938022197293802219729380221972383090160869185684"
   2.253 -  by binary_simp
   2.254 -
   2.255 -lemma "$1111111111222222222233333333334444444444 * $998877665544332211 -
   2.256 -      $5555555555666666666677777777778888888888 =
   2.257 -    $1109864072938022191738246664062713555294605312381980296796"
   2.258 -  by binary_simp
   2.259 -
   2.260 -lemma "$42 < $4 = False"
   2.261 -  by binary_simp
   2.262 -
   2.263 -lemma "$4 < $42 = True"
   2.264 -  by binary_simp
   2.265 -
   2.266 -lemma "$42 <= $4 = False"
   2.267 -  by binary_simp
   2.268 -
   2.269 -lemma "$4 <= $42 = True"
   2.270 -  by binary_simp
   2.271 -
   2.272 -lemma "$1111111111222222222233333333334444444444 < $998877665544332211 = False"
   2.273 -  by binary_simp
   2.274 -
   2.275 -lemma "$998877665544332211 < $1111111111222222222233333333334444444444 = True"
   2.276 -  by binary_simp
   2.277 -
   2.278 -lemma "$1111111111222222222233333333334444444444 <= $998877665544332211 = False"
   2.279 -  by binary_simp
   2.280 -
   2.281 -lemma "$998877665544332211 <= $1111111111222222222233333333334444444444 = True"
   2.282 -  by binary_simp
   2.283 -
   2.284 -lemma "$1234 div $23 = $53"
   2.285 -  by binary_simp
   2.286 -
   2.287 -lemma "$1234 mod $23 = $15"
   2.288 -  by binary_simp
   2.289 -
   2.290 -lemma "$1111111111222222222233333333334444444444 div $998877665544332211 =
   2.291 -    $1112359550673033707875"
   2.292 -  by binary_simp
   2.293 -
   2.294 -lemma "$1111111111222222222233333333334444444444 mod $998877665544332211 =
   2.295 -    $42245174317582819"
   2.296 -  by binary_simp
   2.297 -
   2.298 -lemma "(1111111111222222222233333333334444444444::int) div 998877665544332211 =
   2.299 -    1112359550673033707875"
   2.300 -  by simp  -- {* legacy numerals: 30 times slower *}
   2.301 -
   2.302 -lemma "(1111111111222222222233333333334444444444::int) mod 998877665544332211 =
   2.303 -    42245174317582819"
   2.304 -  by simp  -- {* legacy numerals: 30 times slower *}
   2.305 -
   2.306 -end