From c41ecea1938a16d10cef797ce2e0cdbb38f15a1b Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 3 Mar 2022 19:27:16 +0000
Subject: Add john's solution

---
 resources/eggman.thy | 119 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 119 insertions(+)
 create mode 100644 resources/eggman.thy

diff --git a/resources/eggman.thy b/resources/eggman.thy
new file mode 100644
index 0000000..88c2dcc
--- /dev/null
+++ b/resources/eggman.thy
@@ -0,0 +1,119 @@
+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
\ No newline at end of file
-- 
cgit