Theory Boolean_Inequalities

(*
 * Copyright 2023, Proofcraft Pty Ltd
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory Boolean_Inequalities
  imports Word_EqI
begin

section ‹All inequalities between binary Boolean operations on @{typ "'a word"}›

text ‹
  Enumerates all binary functions resulting from Boolean operations on @{typ "'a word"}
  and derives all inequalities of the form @{term "f x y ≤ g x y"} between them.
  We leave out the trivial @{term "0 ≤ g x y"}, @{term "f x y ≤ -1"}, and
  @{term "f x y ≤ f x y"}, because these are already readily available to the simplifier and
  other methods.

  This leaves 36 inequalities. Some of these are subsumed by each other, but we generate
  the full list to avoid too much manual processing.

  All inequalities produced here are in simp normal form.›

context
  includes bit_operations_syntax
begin

(* The following are all 16 binary Boolean operations (on bool):
   all_bool_funs ≡ [
     λx y. False,
     λx y. x ∧ y,
     λx y. x ∧ ¬y,
     λx y. x,
     λx y. ¬x ∧ y,
     λx y. y,
     λx y. x ≠ y,
     λx y. x ∨ y,
     λx y. ¬(x ∨ y),
     λx y. x = y,
     λx y. ¬y,
     λx y. x ∨ ¬y,
     λx y. ¬x,
     λx y. ¬x ∨ y,
     λx y. ¬(x ∧ y),
     λx y. True
   ]

  We can define the same for word operations:
*)
definition all_bool_word_funs :: "('a::len word ⇒ 'a word ⇒ 'a word) list" where
  "all_bool_word_funs ≡ [
     λx y. 0,
     λx y. x AND y,
     λx y. x AND NOT y,
     λx y. x,
     λx y. NOT x AND y,
     λx y. y,
     λx y. x XOR y,
     λx y. x OR y,
     λx y. NOT (x OR y),
     λx y. NOT (x XOR y),
     λx y. NOT y,
     λx y. x OR NOT y,
     λx y. NOT x,
     λx y. NOT x OR y,
     λx y. NOT (x AND y),
     λx y. -1
   ]"


text ‹
  The inequalities on @{typ "'a word"} follow directly from implications on propositional
  Boolean logic, which @{method simp} can solve automatically. This means, we can simply
  enumerate all combinations, reduce from @{typ "'a word"} to @{typ bool}, and attempt to
  solve by @{method simp} to get the complete list.›
local_setup ‹
let
  (* derived from Numeral.mk_num, but returns a term, not syntax. *)
  fun mk_num n =
    if n > 0 then
      (case Integer.quot_rem n 2 of
        (0, 1) => \<^const>‹Num.One›
      | (n, 0) => \<^const>‹Num.Bit0› $ mk_num n
      | (n, 1) => \<^const>‹Num.Bit1› $ mk_num n)
    else raise Match

  (* derived from Numeral.mk_number, but returns a term, not syntax. *)
  fun mk_number n =
    if n = 0 then \<^term>‹0::nat›
    else if n = 1 then \<^term>‹1::nat›
    else \<^term>‹numeral::num ⇒ nat› $ mk_num n;

  (* generic form of the goal statement *)
  val goal = @{term "λn m. (all_bool_word_funs!n) x y ≤ (all_bool_word_funs!m) x y"}
  (* instance of the goal statement for a pair (i,j) of Boolean functions *)
  fun stmt (i,j) = HOLogic.Trueprop $ (goal $ mk_number i $ mk_number j)

  (* attempt to prove an inequality between functions i and j *)
  fun le_thm ctxt (i,j) = Goal.prove ctxt ["x", "y"] [] (stmt (i,j)) (fn _ =>
    (asm_full_simp_tac (ctxt addsimps [@{thm all_bool_word_funs_def}])
     THEN_ALL_NEW resolve_tac ctxt @{thms word_leI}
     THEN_ALL_NEW asm_full_simp_tac (ctxt addsimps @{thms word_eqI_simps bit_simps})) 1)

  (* generate all combinations for (i,j), collect successful inequality theorems,
     unfold all_bool_word_funs, and put into simp normal form. We leave out 0 (bottom)
     and 15 (top), as well as reflexive thms to remove trivial lemmas from the list.*)
  fun thms ctxt =
    map_product (fn x => fn y => (x,y)) (1 upto 14) (1 upto 14)
    |> filter (fn (x,y) => x <> y)
    |> map_filter (try (le_thm ctxt))
    |> map (Simplifier.simplify ctxt o Local_Defs.unfold ctxt @{thms all_bool_word_funs_def})
in
  fn ctxt =>
    Local_Theory.notes [((Binding.name "word_bool_le_funs", []), [(thms ctxt, [])])] ctxt |> #2
end
›

(* Sanity checks: *)
lemma
  "x AND y ≤ x" for x :: "'a::len word"
  by (rule word_bool_le_funs(1))

lemma
  "NOT x ≤ NOT x OR NOT y" for x :: "'a::len word"
  by (rule word_bool_le_funs(36))

lemma
  "x XOR y ≤ NOT x OR NOT y" for x :: "'a::len word"
  by (rule word_bool_le_funs)

(* Example use when the goal is not in simp normal form: *)
lemma word_xor_le_nand:
  "x XOR y ≤ NOT (x AND y)" for x :: "'a::len word"
  by (simp add: word_bool_le_funs)

end

end