diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-03-03 19:27:16 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-03 19:27:16 +0000 |
| commit | c41ecea1938a16d10cef797ce2e0cdbb38f15a1b (patch) | |
| tree | 9d4850ba9fa7cf32a593c06802f342497bb78460 | |
| parent | 3304cda3345bd13544d74b6976b6f19532ce4d72 (diff) | |
| download | biteq-c41ecea1938a16d10cef797ce2e0cdbb38f15a1b.tar.gz biteq-c41ecea1938a16d10cef797ce2e0cdbb38f15a1b.zip | |
Add john's solution
| -rw-r--r-- | resources/eggman.thy | 119 |
1 files changed, 119 insertions, 0 deletions
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 |