# HG changeset patch
# User haftmann
# Date 1571771232 0
# Node ID b4564de51fa78c1786f5c067a3b7da4e970f0d56
# Parent  525853e4ec80cb08f3be45574b72f74b25749998
bit operations form an boolean algebra

diff -r 525853e4ec80 -r b4564de51fa7 src/HOL/ex/Bit_Lists.thy
--- a/src/HOL/ex/Bit_Lists.thy	Tue Oct 22 19:07:11 2019 +0000
+++ b/src/HOL/ex/Bit_Lists.thy	Tue Oct 22 19:07:12 2019 +0000
@@ -4,9 +4,21 @@
 section \<open>Proof(s) of concept for algebraically founded lists of bits\<close>
 
 theory Bit_Lists
-  imports Main
+  imports
+    Main
+    "HOL-Library.Boolean_Algebra"
+begin
+
+context ab_group_add
 begin
 
+lemma minus_diff_commute:
+  "- b - a = - a - b"
+  by (simp only: diff_conv_add_uminus add.commute)
+
+end
+
+
 subsection \<open>Bit representations\<close>
 
 subsubsection \<open>Mere syntactic bit representation\<close>
@@ -232,7 +244,7 @@
 subsection \<open>Syntactic bit operations\<close>
 
 class bit_operations = bit_representation +
-  fixes not :: "'a \<Rightarrow> 'a"  ("NOT _" [70] 71)
+  fixes not :: "'a \<Rightarrow> 'a"  ("NOT")
     and "and" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "AND" 64)
     and or :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "OR"  59)
     and xor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "XOR" 59)
@@ -529,6 +541,10 @@
   "complement (k * 2) div 2 = complement k"
   by simp
 
+lemma complement_div_2:
+  "complement (k div 2) = complement k div 2"
+  by linarith
+
 locale zip_int = single: abel_semigroup f
   for f :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixl "\<^bold>*" 70)
 begin
@@ -903,7 +919,7 @@
 
 lemma not_int_simps [simp]:
   "NOT 0 = (- 1 :: int)"
-  "NOT - 1 = (0 :: int)"
+  "NOT (- 1) = (0 :: int)"
   "k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int
   by (auto simp add: not_int_def elim: oddE)
 
@@ -911,6 +927,16 @@
   "NOT 1 = (- 2 :: int)"
   by simp
 
+lemma even_not_iff [simp]:
+  "even (NOT k) \<longleftrightarrow> odd k"
+  for k :: int
+  by (simp add: not_int_def)
+
+lemma not_div_2:
+  "NOT k div 2 = NOT (k div 2)"
+  for k :: int
+  by (simp add: complement_div_2 not_int_def)
+
 lemma one_and_int_eq [simp]:
   "1 AND k = k mod 2" for k :: int
   using and_int.rec [of 1] by (simp add: mod2_eq_if)
@@ -935,4 +961,86 @@
   "k XOR 1 = k + of_bool (even k) - of_bool (odd k)" for k :: int
   using one_xor_int_eq [of k] by (simp add: ac_simps)
 
+global_interpretation bit_int: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: int"
+  rewrites "bit_int.xor = ((XOR) :: int \<Rightarrow> _)"
+proof -
+  interpret bit_int: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: int"
+  proof
+    show "k AND (l OR r) = k AND l OR k AND r"
+      for k l r :: int
+    proof (induction k arbitrary: l r rule: int_bit_induct)
+      case zero
+      show ?case
+        by simp
+    next
+      case minus
+      show ?case
+        by simp
+    next
+      case (even k)
+      then show ?case by (simp add: and_int.rec [of "k * 2"]
+        or_int.rec [of "(k AND l div 2) * 2"] or_int.rec [of l])
+    next
+      case (odd k)
+      then show ?case by (simp add: and_int.rec [of "1 + k * 2"]
+        or_int.rec [of "(k AND l div 2) * 2"] or_int.rec [of "1 + (k AND l div 2) * 2"] or_int.rec [of l])
+    qed
+    show "k OR l AND r = (k OR l) AND (k OR r)"
+      for k l r :: int
+    proof (induction k arbitrary: l r rule: int_bit_induct)
+      case zero
+      then show ?case
+        by simp
+    next
+      case minus
+      then show ?case
+        by simp
+    next
+      case (even k)
+      then show ?case by (simp add: or_int.rec [of "k * 2"]
+        and_int.rec [of "(k OR l div 2) * 2"] and_int.rec [of "1 + (k OR l div 2) * 2"] and_int.rec [of l])
+    next
+      case (odd k)
+      then show ?case by (simp add: or_int.rec [of "1 + k * 2"]
+        and_int.rec [of "1 + (k OR l div 2) * 2"] and_int.rec [of l])
+    qed
+    show "k AND NOT k = 0" for k :: int
+      by (induction k rule: int_bit_induct)
+        (simp_all add: not_int_def complement_half minus_diff_commute [of 1])
+    show "k OR NOT k = - 1" for k :: int
+      by (induction k rule: int_bit_induct)
+        (simp_all add: not_int_def complement_half minus_diff_commute [of 1])
+  qed simp_all
+  show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: int)"
+    by (fact bit_int.boolean_algebra_axioms)
+  show "bit_int.xor = ((XOR) :: int \<Rightarrow> _)"
+  proof (rule ext)+
+    fix k l :: int
+    have "k XOR l = k AND NOT l OR NOT k AND l"
+    proof (induction k arbitrary: l rule: int_bit_induct)
+      case zero
+      show ?case
+        by simp
+    next
+      case minus
+      show ?case
+        by (simp add: not_int_def)
+    next
+      case (even k)
+      then show ?case
+        by (simp add: xor_int.rec [of "k * 2"] and_int.rec [of "k * 2"]
+          or_int.rec [of _ "1 + 2 * NOT k AND l"] not_div_2)
+          (simp add: and_int.rec [of _ l])
+    next
+      case (odd k)
+      then show ?case
+        by (simp add: xor_int.rec [of "1 + k * 2"] and_int.rec [of "1 + k * 2"]
+          or_int.rec [of _ "2 * NOT k AND l"] not_div_2)
+          (simp add: and_int.rec [of _ l])
+    qed
+    then show "bit_int.xor k l = k XOR l"
+      by (simp add: bit_int.xor_def)
+  qed
+qed
+
 end