theory eggman imports Main begin

type_synonym bit = "bool"

abbreviation B0 where "B0 == False"
abbreviation B1 where "B1 == True"

(* Note that all bitvectors are stored in LSB-first order *)

fun binary_to_nat :: "bit list \<Rightarrow> nat"
where
  "binary_to_nat [] = 0"
| "binary_to_nat (b # l) = (if b then 1 else 0) + 2 * binary_to_nat l"

fun nat_to_binary :: "nat \<Rightarrow> bit list"
where
  "nat_to_binary n = 
    (if n = 0 then [] else (if even n then B0 else B1) # nat_to_binary (n div 2))"

(* Remove any leading zeroes. Note that the bitvector for 0 is the empty list. *)
fun trim :: "bit list \<Rightarrow> bit list"
where 
  "trim [] = []"
| "trim (B0 # l) = (if trim l = [] then [] else B0 # trim l)"
| "trim (B1 # l) = B1 # trim l"

value "trim [B0,B1,B0,B0]"
value "trim [B1,B0,B1,B0,B1]"
value "trim [B1,B0,B1,B0,B0,B0]"

lemma binary_to_nat_trim:
  "binary_to_nat (trim l) = binary_to_nat l"
by (induct l, auto)

lemma nat_to_binary_inv: "nat_to_binary (binary_to_nat l) = trim l"
proof (induct l)
  case Nil
  thus ?case by auto
next
  case (Cons b l)
  hence *: "nat_to_binary (binary_to_nat l) = trim l" by auto
  thus ?case
  proof (cases b)
    case True
    have "nat_to_binary (1 + 2 * binary_to_nat l) = trim (B1 # l)" using * by auto
    with True show ?thesis by auto
  next
    case False
    have "nat_to_binary (2 * binary_to_nat l) = trim (B0 # l)" using *
      by (smt (z3) binary_to_nat.simps(1) binary_to_nat_trim dvd_triv_left 
          mult_0_right nat_to_binary.simps nonzero_mult_div_cancel_left 
          trim.simps(2) zero_neq_numeral)
    with False show ?thesis by auto
  qed    
qed

lemma binary_to_nat_inv: "binary_to_nat (nat_to_binary n) = n"
proof - (* using complete induction *)
  have "\<forall>m. m < n \<longrightarrow> binary_to_nat (nat_to_binary m) = m" by (induct n, auto)
  thus ?thesis by simp
qed

(* Addition on two bitvectors is just defined "semantically" *)
definition bv_add :: "bit list \<Rightarrow> bit list \<Rightarrow> bit list" (infixr "+B" 51)
where
  "l1 +B l2 = nat_to_binary (binary_to_nat l1 + binary_to_nat l2)"

fun zeroes :: "nat \<Rightarrow> bit list"
where
  "zeroes 0 = []"
| "zeroes (Suc n) = B0 # zeroes n"

fun prefix :: "nat \<Rightarrow> bit list \<Rightarrow> bit list"
where
  "prefix n [] = []"
| "prefix n (x # xs) = (if n = 0 then [] else x # prefix (n - 1) xs)"

value "prefix 3 [B0,B0,B1,B0,B1]"
value "prefix 4 [B0,B0,B1,B1]"
value "prefix 5 [B0,B0,B1]"

(* Forces a bitvector to have a given width, either by 
   trimming MSBs or by adding leading zeroes *)
definition setwidth :: "nat \<Rightarrow> bit list \<Rightarrow> bit list" ("\<^sub>_ _" [51, 52] 52)
where
  "\<^sub>n l = prefix n (l @ zeroes (n - length l))"

value "\<^sub>4 [B0,B1,B0]"
value "\<^sub>3 [B0,B1,B0]"
value "\<^sub>2 [B0,B1,B0]"

(* A simple "add associativity" lemma (without bitwidths) *)
lemma bv_add_assoc_simple: 
  "(a +B b) +B c = a +B (b +B c)"
  by (metis add.assoc binary_to_nat_inv bv_add_def)

(* Now incorporating bitwidths. Trying to see if Sam's sideconditions
  are necessary. The counterexample indicates that they're not. *)
lemma bv_add_assoc_necessary:
  assumes "\<^sub>t (\<^sub>u (\<^sub>p a +B \<^sub>r b) +B \<^sub>s c) = \<^sub>t (\<^sub>p a +B \<^sub>q (\<^sub>r b +B \<^sub>s c))"
  and "a \<noteq> []" and "b \<noteq> []" and "c \<noteq> []"
  and "p > 0" and "q > 0" and "r > 0" and "s > 0" and "t > 0"
  shows "(q \<ge> t \<or> r + s \<le> q) \<and> (u \<ge> t \<or> p + r \<le> u)"
  try
(*
Nitpick found a counterexample:
    a = [B0, B0]
    b = [B0, B0]
    c = [B0]
    p = 1
    q = 2
    r = 1
    s = 2
    t = 2
    u = 1
*)
  oops

end