proof of concept for algebraically founded bit lists
authorhaftmann
Wed Mar 21 20:17:25 2018 +0100 (14 months ago)
changeset 67909f55b07f4d1ee
parent 67908 537f891d8f14
child 67910 b42473502373
proof of concept for algebraically founded bit lists
src/HOL/ROOT
src/HOL/ex/Bit_Lists.thy
     1.1 --- a/src/HOL/ROOT	Wed Mar 21 19:39:24 2018 +0100
     1.2 +++ b/src/HOL/ROOT	Wed Mar 21 20:17:25 2018 +0100
     1.3 @@ -527,6 +527,7 @@
     1.4      Ballot
     1.5      BinEx
     1.6      Birthday_Paradox
     1.7 +    Bit_Lists
     1.8      Bubblesort
     1.9      CTL
    1.10      Cartouche_Examples
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Bit_Lists.thy	Wed Mar 21 20:17:25 2018 +0100
     2.3 @@ -0,0 +1,169 @@
     2.4 +(*  Author:  Florian Haftmann, TUM
     2.5 +*)
     2.6 +
     2.7 +section \<open>Proof of concept for algebraically founded lists of bits\<close>
     2.8 +
     2.9 +theory Bit_Lists
    2.10 +  imports Main
    2.11 +begin
    2.12 +
    2.13 +context comm_semiring_1
    2.14 +begin
    2.15 +
    2.16 +primrec of_unsigned :: "bool list \<Rightarrow> 'a"
    2.17 +  where "of_unsigned [] = 0"
    2.18 +  | "of_unsigned (b # bs) = of_bool b + 2 * of_unsigned bs"
    2.19 +
    2.20 +end
    2.21 +
    2.22 +context comm_ring_1
    2.23 +begin
    2.24 +
    2.25 +definition of_signed :: "bool list \<Rightarrow> 'a"
    2.26 +  where "of_signed bs = (if bs = [] then 0 else if last bs
    2.27 +    then - (of_unsigned (map Not bs) + 1) else of_unsigned bs)"
    2.28 +
    2.29 +end
    2.30 +
    2.31 +class semiring_bits = semiring_parity +
    2.32 +  assumes half_measure: "a div 2 \<noteq> a \<Longrightarrow> euclidean_size (a div 2) < euclidean_size a"
    2.33 +  \<comment> \<open>It is not clear whether this could be derived from already existing assumptions.\<close>
    2.34 +begin
    2.35 +
    2.36 +function bits_of :: "'a \<Rightarrow> bool list"
    2.37 +  where "bits_of a = odd a # (let b = a div 2 in if a = b then [] else bits_of b)"
    2.38 +  by auto
    2.39 +
    2.40 +termination
    2.41 +  by (relation "measure euclidean_size") (auto intro: half_measure)
    2.42 +
    2.43 +lemma bits_of_not_empty [simp]:
    2.44 +  "bits_of a \<noteq> []"
    2.45 +  by (induction a rule: bits_of.induct) simp_all
    2.46 +
    2.47 +lemma bits_of_0 [simp]:
    2.48 +  "bits_of 0 = [False]"
    2.49 +  by simp
    2.50 +
    2.51 +lemma bits_of_1 [simp]:
    2.52 +  "bits_of 1 = [True, False]"
    2.53 +  by simp
    2.54 +
    2.55 +lemma bits_of_double [simp]:
    2.56 +  "bits_of (a * 2) = False # (if a = 0 then [] else bits_of a)"
    2.57 +  by simp (simp add: mult_2_right)
    2.58 +
    2.59 +lemma bits_of_add_1_double [simp]:
    2.60 +  "bits_of (1 + a * 2) = True # (if a + 1 = 0 then [] else bits_of a)"
    2.61 +  by simp (simp add: mult_2_right algebra_simps)
    2.62 +
    2.63 +declare bits_of.simps [simp del]
    2.64 +
    2.65 +lemma not_last_bits_of_nat [simp]:
    2.66 +  "\<not> last (bits_of (of_nat n))"
    2.67 +  by (induction n rule: parity_induct)
    2.68 +    (use of_nat_neq_0 in \<open>simp_all add: algebra_simps\<close>)
    2.69 +
    2.70 +lemma of_unsigned_bits_of_nat:
    2.71 +  "of_unsigned (bits_of (of_nat n)) = of_nat n"
    2.72 +  by (induction n rule: parity_induct)
    2.73 +    (use of_nat_neq_0 in \<open>simp_all add: algebra_simps\<close>)
    2.74 +
    2.75 +end
    2.76 +
    2.77 +instance nat :: semiring_bits
    2.78 +  by standard simp
    2.79 +
    2.80 +lemma bits_of_Suc_double [simp]:
    2.81 +  "bits_of (Suc (n * 2)) = True # bits_of n"
    2.82 +  using bits_of_add_1_double [of n] by simp
    2.83 +
    2.84 +lemma of_unsigned_bits_of:
    2.85 +  "of_unsigned (bits_of n) = n" for n :: nat
    2.86 +  using of_unsigned_bits_of_nat [of n, where ?'a = nat] by simp
    2.87 +
    2.88 +class ring_bits = ring_parity + semiring_bits
    2.89 +begin
    2.90 +
    2.91 +lemma bits_of_minus_1 [simp]:
    2.92 +  "bits_of (- 1) = [True]"
    2.93 +  using bits_of.simps [of "- 1"] by simp
    2.94 +
    2.95 +lemma bits_of_double [simp]:
    2.96 +  "bits_of (- (a * 2)) = False # (if a = 0 then [] else bits_of (- a))"
    2.97 +  using bits_of.simps [of "- (a * 2)"] nonzero_mult_div_cancel_right [of 2 "- a"]
    2.98 +  by simp (simp add: mult_2_right)
    2.99 +
   2.100 +lemma bits_of_minus_1_diff_double [simp]:
   2.101 +  "bits_of (- 1 - a * 2) = True # (if a = 0 then [] else bits_of (- 1 - a))"
   2.102 +proof -
   2.103 +  have [simp]: "- 1 - a = - a - 1"
   2.104 +    by (simp add: algebra_simps)
   2.105 +  show ?thesis
   2.106 +    using bits_of.simps [of "- 1 - a * 2"] div_mult_self1 [of 2 "- 1" "- a"]
   2.107 +    by simp (simp add: mult_2_right algebra_simps)
   2.108 +qed
   2.109 +
   2.110 +lemma last_bits_of_neg_of_nat [simp]:
   2.111 +  "last (bits_of (- 1 - of_nat n))"
   2.112 +proof (induction n rule: parity_induct)
   2.113 +  case zero
   2.114 +  then show ?case
   2.115 +    by simp
   2.116 +next
   2.117 +  case (even n)
   2.118 +  then show ?case
   2.119 +    by (simp add: algebra_simps)
   2.120 +next
   2.121 +  case (odd n)
   2.122 +  then have "last (bits_of ((- 1 - of_nat n) * 2))"
   2.123 +    by auto
   2.124 +  also have "(- 1 - of_nat n) * 2 = - 1 - (1 + 2 * of_nat n)"
   2.125 +    by (simp add: algebra_simps)
   2.126 +  finally show ?case
   2.127 +    by simp
   2.128 +qed
   2.129 +
   2.130 +lemma of_signed_bits_of_nat:
   2.131 +  "of_signed (bits_of (of_nat n)) = of_nat n"
   2.132 +  by (simp add: of_signed_def of_unsigned_bits_of_nat)
   2.133 +
   2.134 +lemma of_signed_bits_neg_of_nat:
   2.135 +  "of_signed (bits_of (- 1 - of_nat n)) = - 1 - of_nat n"
   2.136 +proof -
   2.137 +  have "of_unsigned (map Not (bits_of (- 1 - of_nat n))) = of_nat n"
   2.138 +  proof (induction n rule: parity_induct)
   2.139 +    case zero
   2.140 +    then show ?case
   2.141 +      by simp
   2.142 +  next
   2.143 +    case (even n)
   2.144 +    then show ?case
   2.145 +      by (simp add: algebra_simps)
   2.146 +  next
   2.147 +    case (odd n)
   2.148 +    have *: "- 1 - (1 + of_nat n * 2) = - 2 - of_nat n * 2"
   2.149 +      by (simp add: algebra_simps) (metis add_assoc one_add_one)
   2.150 +    from odd show ?case
   2.151 +      using bits_of_double [of "of_nat (Suc n)"] of_nat_neq_0
   2.152 +      by (simp add: algebra_simps *)
   2.153 +  qed
   2.154 +  then show ?thesis
   2.155 +    by (simp add: of_signed_def algebra_simps)
   2.156 +qed
   2.157 +
   2.158 +lemma of_signed_bits_of_int:
   2.159 +  "of_signed (bits_of (of_int k)) = of_int k"
   2.160 +  by (cases k rule: int_cases)
   2.161 +    (simp_all add: of_signed_bits_of_nat of_signed_bits_neg_of_nat)
   2.162 +
   2.163 +end
   2.164 +
   2.165 +instance int :: ring_bits
   2.166 +  by standard auto
   2.167 +
   2.168 +lemma of_signed_bits_of:
   2.169 +  "of_signed (bits_of k) = k" for k :: int
   2.170 +  using of_signed_bits_of_int [of k, where ?'a = int] by simp
   2.171 +
   2.172 +end