Session Boolean_Expression_Checkers

Theory Boolean_Expression_Checkers

(*
  Boolean Expression Checkers Based on Binary Decision Trees
  Author: Tobias Nipkow
*)

theory Boolean_Expression_Checkers
  imports Main "HOL-Library.Mapping"
begin

section ‹Tautology (etc) Checking via Binary Decision Trees›

subsection ‹Binary Decision Trees›

datatype 'a ifex = Trueif | Falseif | IF 'a "'a ifex" "'a ifex"

fun val_ifex :: "'a ifex  ('a  bool)  bool" 
where
  "val_ifex Trueif s = True"
| "val_ifex Falseif s = False"
| "val_ifex (IF n t1 t2) s = (if s n then val_ifex t1 s else val_ifex t2 s)"

subsubsection ‹Environment›

text ‹Environments are substitutions of values for variables:›

type_synonym 'a env_bool = "('a, bool) mapping"

definition agree :: "('a  bool)  'a env_bool  bool"
where
  "agree s env = (x b. Mapping.lookup env x = Some b  s x = b)"

lemma agree_Nil: 
  "agree s Mapping.empty"
  by (simp add: agree_def lookup_empty)

lemma lookup_update_unfold: 
  "Mapping.lookup (Mapping.update k v m) k' = (if k = k' then Some v else Mapping.lookup m k')"
  using lookup_update lookup_update_neq by metis

lemma agree_Cons: 
  "x  Mapping.keys env  agree s (Mapping.update x b env) = ((if b then s x else ¬ s x)  agree s env)"
  by (simp add: agree_def lookup_update_unfold; unfold keys_is_none_rep lookup_update_unfold Option.is_none_def; blast)

lemma agreeDT:
  "agree s env  Mapping.lookup env x = Some True  s x"
  by (simp add: agree_def)

lemma agreeDF:
  "agree s env  Mapping.lookup env x = Some False  ¬s x"
  by (auto simp add: agree_def)

subsection ‹Recursive Tautology Checker›

text ‹Provided for completeness. However, it is recommend to use the checkers based on reduced trees.›

fun taut_test_rec :: "'a ifex  'a env_bool  bool" 
where
  "taut_test_rec Trueif env = True" 
| "taut_test_rec Falseif env = False" 
| "taut_test_rec (IF x t1 t2) env = (case Mapping.lookup env x of
  Some b  taut_test_rec (if b then t1 else t2) env |
  None  taut_test_rec t1 (Mapping.update x True env)  taut_test_rec t2 (Mapping.update x False env))"

lemma taut_test_rec: 
  "taut_test_rec t env = (s. agree s env  val_ifex t s)"
proof (induction t arbitrary: env)
  case Falseif
    have "agree (λx. the (Mapping.lookup env x)) env" 
      by (auto simp: agree_def)
    thus ?case 
      by auto
next
  case (IF x t1 t2) 
    thus ?case
    proof (cases "Mapping.lookup env x")
      case None 
        with IF show ?thesis 
          by simp (metis is_none_simps(1) agree_Cons keys_is_none_rep)
    qed (simp add: agree_def)
qed simp

definition taut_test_ifex :: "'a ifex  bool" 
where
  "taut_test_ifex t = taut_test_rec t Mapping.empty"

corollary taut_test_ifex: 
  "taut_test_ifex t = (s. val_ifex t s)"
  by (auto simp: taut_test_ifex_def taut_test_rec agree_Nil)

subsection ‹Reduced Binary Decision Trees›

subsubsection ‹Normalisation›

text ‹A normalisation avoiding duplicate variables and collapsing @{term "If x t t"} to t›.›

definition mkIF :: "'a  'a ifex  'a ifex  'a ifex" 
where
  "mkIF x t1 t2 = (if t1=t2 then t1 else IF x t1 t2)"

fun reduce :: "'a env_bool  'a ifex  'a ifex"
where
  "reduce env (IF x t1 t2) = (case Mapping.lookup env x of
     None  mkIF x (reduce (Mapping.update x True env) t1) (reduce (Mapping.update x False env) t2) |
     Some b  reduce env (if b then t1 else t2))" 
| "reduce _ t = t"

primrec normif :: "'a env_bool  'a ifex  'a ifex  'a ifex  'a ifex" 
where
  "normif env Trueif t1 t2 = reduce env t1" 
| "normif env Falseif t1 t2 = reduce env t2" 
| "normif env (IF x t1 t2) t3 t4 =
    (case Mapping.lookup env x of
       None  mkIF x (normif (Mapping.update x True env) t1 t3 t4) (normif (Mapping.update x False env) t2 t3 t4) |
       Some b  if b then normif env t1 t3 t4 else normif env t2 t3 t4)"

subsubsection ‹Functional Correctness Proof›

lemma val_mkIF: 
  "val_ifex (mkIF x t1 t2) s = val_ifex (IF x t1 t2) s"
  by (auto simp: mkIF_def Let_def)

theorem val_reduce: 
  "agree s env  val_ifex (reduce env t) s = val_ifex t s"
  by (induction t arbitrary: s env)
     (auto simp: map_of_eq_None_iff val_mkIF agree_Cons Let_def keys_is_none_rep
           dest: agreeDT agreeDF split: option.splits) 

lemma val_normif: 
  "agree s env  val_ifex (normif env t t1 t2) s = val_ifex (if val_ifex t s then t1 else t2) s"
  by (induct t arbitrary: t1 t2 s env)
     (auto simp: val_reduce val_mkIF agree_Cons map_of_eq_None_iff keys_is_none_rep
           dest: agreeDT agreeDF split: option.splits)   

subsubsection ‹Reduced If-Expressions›

text ‹An expression reduced iff no variable appears twice on any branch and there is no subexpression @{term "IF x t t"}.›

fun reduced :: "'a ifex  'a set  bool" where
"reduced (IF x t1 t2) X =
  (x  X  t1  t2  reduced t1 (insert x X)  reduced t2 (insert x X))" |
"reduced _ _ = True"

lemma reduced_antimono: 
  "X  Y  reduced t Y  reduced t X"
  by (induction t arbitrary: X Y)
     (auto, (metis insert_mono)+)

lemma reduced_mkIF: 
  "x  X  reduced t1 (insert x X)  reduced t2 (insert x X)  reduced (mkIF x t1 t2) X"
  by (auto simp: mkIF_def intro:reduced_antimono)

lemma reduced_reduce:
  "reduced (reduce env t) (Mapping.keys env)"
proof(induction t arbitrary: env)
  case (IF x t1 t2)
    thus ?case 
      using IF.IH(1) IF.IH(2)
      apply (auto simp: map_of_eq_None_iff image_iff reduced_mkIF split: option.split) 
      by (metis is_none_code(1) keys_is_none_rep keys_update reduced_mkIF)
qed auto

lemma reduced_normif:
  "reduced (normif env t t1 t2) (Mapping.keys env)"
proof(induction t arbitrary: t1 t2 env)
  case (IF x s1 s2)
  thus ?case using IF.IH
    apply (auto simp: reduced_mkIF map_of_eq_None_iff split: option.split) 
    by (metis is_none_code(1) keys_is_none_rep keys_update reduced_mkIF)
qed (auto simp: reduced_reduce)

subsubsection ‹Checkers Based on Reduced Binary Decision Trees›

text ‹The checkers are parameterized over the translation function to binary decision trees. 
  They rely on the fact that @{term ifex_of} produces reduced trees›

definition taut_test :: "('a  'b ifex)  'a  bool" 
where
  "taut_test ifex_of b = (ifex_of b = Trueif)"

definition sat_test :: "('a  'b ifex)  'a  bool" 
where
  "sat_test ifex_of b = (ifex_of b  Falseif)"

definition impl_test :: "('a  'b ifex)  'a  'a  bool" 
where
  "impl_test ifex_of b1 b2 = (normif Mapping.empty (ifex_of b1) (ifex_of b2) Trueif = Trueif)"

definition equiv_test :: "('a  'b ifex)  'a  'a  bool" 
where
  "equiv_test ifex_of b1 b2 = (let t1 = ifex_of b1; t2 = ifex_of b2 
    in Trueif = normif Mapping.empty t1 t2 (normif Mapping.empty t2 Falseif Trueif))"

locale reduced_bdt_checkers = 
  fixes
    ifex_of :: "'b  'a ifex"
  fixes
    val :: "'b  ('a  bool)  bool"
  assumes
    val_ifex: "val_ifex (ifex_of b) s = val b s"
  assumes 
    reduced_ifex: "reduced (ifex_of b) {}"
begin

text ‹Proof that reduced if-expressions are @{const Trueif}, @{const Falseif}
or can evaluate to both @{const True} and @{const False}.›

lemma same_val_if_reduced:
  "reduced t X  x. x  X  s1 x = s2 x  val_ifex t s1 = val_ifex t s2"
  by (induction t arbitrary: X) auto

lemma reduced_IF_depends: 
  " reduced t X; t  Trueif; t  Falseif   s1 s2. val_ifex t s1  val_ifex t s2"
proof(induction t arbitrary: X)
  case (IF x t1 t2)
  let ?t = "IF x t1 t2"
  have 1: "reduced t1 (insert x X)" using IF.prems(1) by simp
  have 2: "reduced t2 (insert x X)" using IF.prems(1) by simp
  show ?case
  proof(cases t1)
    case [simp]: Trueif
    show ?thesis
    proof (cases t2)
      case Trueif thus ?thesis using IF.prems(1) by simp
    next
      case Falseif
      hence "val_ifex ?t (λ_. True)  val_ifex ?t (λ_. False)" by simp
      thus ?thesis by blast
    next
      case IF
      then obtain s1 s2 where "val_ifex t2 s1  val_ifex t2 s2"
        using IF.IH(2)[OF 2] IF.prems(1) by auto
      hence "val_ifex ?t (s1(x:=False))  val_ifex ?t (s2(x:=False))"
        using same_val_if_reduced[OF 2, of "s1(x:=False)" s1]
          same_val_if_reduced[OF 2, of "s2(x:=False)" s2] by simp
      thus ?thesis by blast
    qed
  next
    case [simp]: Falseif
    show ?thesis
    proof (cases t2)
      case Falseif thus ?thesis using IF.prems(1) by simp
    next
      case Trueif
      hence "val_ifex ?t (λ_. True)  val_ifex ?t (λ_. False)" by simp
      thus ?thesis by blast
    next
      case IF
      then obtain s1 s2 where "val_ifex t2 s1  val_ifex t2 s2"
        using IF.IH(2)[OF 2] IF.prems(1) by auto
      hence "val_ifex ?t (s1(x:=False))  val_ifex ?t (s2(x:=False))"
        using same_val_if_reduced[OF 2, of "s1(x:=False)" s1]
          same_val_if_reduced[OF 2, of "s2(x:=False)" s2] by simp
      thus ?thesis by blast
    qed
  next
    case IF
    then obtain s1 s2 where "val_ifex t1 s1  val_ifex t1 s2"
      using IF.IH(1)[OF 1] IF.prems(1) by auto
    hence "val_ifex ?t (s1(x:=True))  val_ifex ?t (s2(x:=True))"
      using same_val_if_reduced[OF 1, of "s1(x:=True)" s1]
          same_val_if_reduced[OF 1, of "s2(x:=True)" s2] by simp
    thus ?thesis by blast
  qed
qed auto

corollary taut_test: 
  "taut_test ifex_of b = (s. val b s)"    
  by (metis taut_test_def reduced_IF_depends[OF reduced_ifex] val_ifex val_ifex.simps(1,2))

corollary sat_test: 
  "sat_test ifex_of b = (s. val b s)"
  by (metis sat_test_def reduced_IF_depends[OF reduced_ifex] val_ifex val_ifex.simps(1,2))

corollary impl_test: 
  "impl_test ifex_of b1 b2 = (s. val b1 s  val b2 s)"
proof -
  have "impl_test ifex_of b1 b2 = (s. val_ifex (normif Mapping.empty (ifex_of b1) (ifex_of b2) Trueif) s)"
    using reduced_IF_depends[OF reduced_normif] by (fastforce  simp: impl_test_def)
  also
  have "(s. val_ifex (normif Mapping.empty (ifex_of b1) (ifex_of b2) Trueif) s)  (s. val b1 s  val b2 s)"
    using reduced_IF_depends[OF reduced_ifex] val_ifex unfolding val_normif[OF agree_Nil] by simp
  finally
  show ?thesis .
qed

corollary equiv_test: 
  "equiv_test ifex_of b1 b2 = (s. val b1 s = val b2 s)"
proof -
  have "equiv_test ifex_of b1 b2 = (s. val_ifex (let t1 = ifex_of b1; t2 = ifex_of b2 in normif Mapping.empty t1 t2 (normif Mapping.empty t2 Falseif Trueif)) s)"
    by (simp add: equiv_test_def Let_def; insert reduced_IF_depends[OF reduced_normif]; force)
  moreover
  {
    fix s
    have "val_ifex (let t1 = ifex_of b1; t2 = ifex_of b2 in normif Mapping.empty t1 t2 (normif Mapping.empty t2 Falseif Trueif)) s
      = (val b1 s = val b2 s)"
      using val_ifex by (simp add: Let_def val_normif[OF agree_Nil]) 
  }
  ultimately
  show ?thesis 
    by blast
qed

end

subsection ‹Boolean Expressions›

text ‹This is the simplified interface to the tautology checker. If you have your own type of Boolean 
expressions you can either define your own translation to reduced binary decision trees or you can just 
translate into this type.›

datatype 'a bool_expr =
  Const_bool_expr bool |
  Atom_bool_expr 'a |
  Neg_bool_expr "'a bool_expr" |
  And_bool_expr "'a bool_expr" "'a bool_expr" |
  Or_bool_expr "'a bool_expr" "'a bool_expr" |
  Imp_bool_expr "'a bool_expr" "'a bool_expr" |
  Iff_bool_expr "'a bool_expr" "'a bool_expr"

primrec val_bool_expr :: "'a bool_expr  ('a  bool)  bool" where
"val_bool_expr (Const_bool_expr b) s = b" |
"val_bool_expr (Atom_bool_expr x) s = s x" |
"val_bool_expr (Neg_bool_expr b) s = (¬ val_bool_expr b s)" |
"val_bool_expr (And_bool_expr b1 b2) s = (val_bool_expr b1 s  val_bool_expr b2 s)" |
"val_bool_expr (Or_bool_expr b1 b2) s = (val_bool_expr b1 s  val_bool_expr b2 s)" |
"val_bool_expr (Imp_bool_expr b1 b2) s = (val_bool_expr b1 s  val_bool_expr b2 s)" |
"val_bool_expr (Iff_bool_expr b1 b2) s = (val_bool_expr b1 s = val_bool_expr b2 s)"

fun ifex_of :: "'a bool_expr  'a ifex" where
"ifex_of (Const_bool_expr b) = (if b then Trueif else Falseif)" |
"ifex_of (Atom_bool_expr x)   = IF x Trueif Falseif" |
"ifex_of (Neg_bool_expr b)   = normif Mapping.empty (ifex_of b) Falseif Trueif" |
"ifex_of (And_bool_expr b1 b2) = normif Mapping.empty (ifex_of b1) (ifex_of b2) Falseif" |
"ifex_of (Or_bool_expr b1 b2) = normif Mapping.empty (ifex_of b1) Trueif (ifex_of b2)" |
"ifex_of (Imp_bool_expr b1 b2) = normif Mapping.empty (ifex_of b1) (ifex_of b2) Trueif" |
"ifex_of (Iff_bool_expr b1 b2) = (let t1 = ifex_of b1; t2 = ifex_of b2 in
   normif Mapping.empty t1 t2 (normif Mapping.empty t2 Falseif Trueif))"

theorem val_ifex:
  "val_ifex (ifex_of b) s = val_bool_expr b s"
  by (induct_tac b) (auto simp: val_normif agree_Nil Let_def)

theorem reduced_ifex: 
  "reduced (ifex_of b) {}"
  by (induction b) (simp add: Let_def; metis keys_empty reduced_normif)+

definition "bool_taut_test  taut_test ifex_of"
definition "bool_sat_test  sat_test ifex_of"
definition "bool_impl_test  impl_test ifex_of"
definition "bool_equiv_test  equiv_test ifex_of"

lemma bool_tests:
  "bool_taut_test b = (s. val_bool_expr b s)" (is ?t1)
  "bool_sat_test b = (s. val_bool_expr b s)" (is ?t2)
  "bool_impl_test b1 b2 = (s. val_bool_expr b1 s  val_bool_expr b2 s)" (is ?t3)
  "bool_equiv_test b1 b2 = (s. val_bool_expr b1 s  val_bool_expr b2 s)" (is ?t4)
proof -
  interpret reduced_bdt_checkers ifex_of val_bool_expr
    by (unfold_locales; insert val_ifex reduced_ifex; blast)
  show ?t1 ?t2 ?t3 ?t4
    by (simp_all add: bool_taut_test_def bool_sat_test_def bool_impl_test_def bool_equiv_test_def taut_test sat_test impl_test equiv_test) 
qed

end

Theory Boolean_Expression_Checkers_AList_Mapping

(*
  Boolean Expression Checkers Based on Binary Decision Trees
  Author: Tobias Nipkow
*)

theory Boolean_Expression_Checkers_AList_Mapping
  imports Main "HOL-Library.AList_Mapping" Boolean_Expression_Checkers
begin

section‹Tweaks for @{const AList_Mapping.Mapping}
                                                       
― ‹If mappings are implemented by @{const AList_Mapping.Mapping}, the functions @{const reduce} and @{const normif} 
    search for x twice. The following code equations remove this redundant operation›

lemma AList_Mapping_update: 
  "map_of m k = None  Mapping.update k v (AList_Mapping.Mapping xs) = AList_Mapping.Mapping ((k,v)#xs)"
  by (metis Mapping.abs_eq map_of.simps(2) prod.sel(1) prod.sel(2) update_Mapping update_conv')

fun reduce_alist :: "('a * bool) list  'a ifex  'a ifex"
where
  "reduce_alist xs (IF x t1 t2) = (case map_of xs x of
     None  mkIF x (reduce_alist ((x, True)#xs) t1) (reduce_alist ((x, False)#xs) t2) |
     Some b  reduce_alist xs (if b then t1 else t2))" 
| "reduce_alist _ t = t"

primrec normif_alist :: "('a * bool) list  'a ifex  'a ifex  'a ifex  'a ifex" 
where
  "normif_alist xs Trueif t1 t2 = reduce_alist xs t1" 
| "normif_alist xs Falseif t1 t2 = reduce_alist xs t2" 
| "normif_alist xs (IF x t1 t2) t3 t4 = (case map_of xs x of
    None  mkIF x (normif_alist ((x, True)#xs) t1 t3 t4) (normif_alist ((x, False)#xs) t2 t3 t4) |
    Some b  if b then normif_alist xs t1 t3 t4 else normif_alist xs t2 t3 t4)"
   
lemma reduce_alist_code [code, code_unfold]:
  "reduce (AList_Mapping.Mapping xs) t = reduce_alist xs t"
  by (induction t arbitrary: xs)
     (auto simp: AList_Mapping_update split: option.split)  

lemma normif_alist_code [code, code_unfold]:
  "normif (AList_Mapping.Mapping xs) t = normif_alist xs t"
  by (induction t arbitrary: xs)
     (fastforce simp: AList_Mapping_update reduce_alist_code split: option.split)+

lemmas empty_Mapping [code_unfold]

end

Theory Boolean_Expression_Example

theory Boolean_Expression_Example
  imports Boolean_Expression_Checkers Boolean_Expression_Checkers_AList_Mapping
begin

section ‹Example›

text ‹Example usage of checkers. We have our own type of Boolean expressions with its own evaluation function:›

datatype 'a bexp =
  Const bool |
  Atom 'a |
  Neg "'a bexp" |
  And "'a bexp" "'a bexp"

fun bval where
"bval (Const b) s = b" |
"bval (Atom a) s = s a" |
"bval (Neg b) s = (¬ bval b s)" |
"bval (And b1 b2) s = (bval b1 s  bval b2 s)"

subsection ‹Indirect Translation using the Boolean Expression Interface› 

text ‹Now we translate into @{datatype bool_expr} provided by the checkers interface and show that the 
  semantics remains the same:›

fun bool_expr_of_bexp :: "'a bexp  'a bool_expr" 
where
  "bool_expr_of_bexp (Const b) = Const_bool_expr b" 
| "bool_expr_of_bexp (Atom a) = Atom_bool_expr a" 
| "bool_expr_of_bexp (Neg b) = Neg_bool_expr(bool_expr_of_bexp b)" 
| "bool_expr_of_bexp (And b1 b2) = And_bool_expr (bool_expr_of_bexp b1) (bool_expr_of_bexp b2)"

lemma val_preservation: 
  "val_bool_expr (bool_expr_of_bexp b) s = bval b s"
  by (induction b) auto 

definition "my_taut_test_bool = bool_taut_test o bool_expr_of_bexp"

corollary my_taut_test: 
  "my_taut_test_bool b = (s. bval b s)"
  by (simp add: my_taut_test_bool_def val_preservation bool_tests)

subsection ‹Direct Translation into Reduced Binary Decision Trees› 

text ‹Now we translate into a reduced binary decision tree, show that the semantics remains the same and 
  the tree is reduced:›

fun ifex_of :: "'a bexp  'a ifex" 
where
  "ifex_of (Const b) = (if b then Trueif else Falseif)" 
| "ifex_of (Atom a) = IF a Trueif Falseif" 
| "ifex_of (Neg b)   = normif Mapping.empty (ifex_of b) Falseif Trueif" 
| "ifex_of (And b1 b2) = normif Mapping.empty (ifex_of b1) (ifex_of b2) Falseif"

lemma val_ifex: 
  "val_ifex (ifex_of b) s = bval b s"
  by (induction b) (simp_all add: agree_Nil val_normif)

theorem reduced_ifex: 
  "reduced (ifex_of b) {}"
  by (induction b) (simp; metis keys_empty reduced_normif)+

definition "my_taut_test_ifex = taut_test ifex_of"

corollary my_taut_test_ifex: 
  "my_taut_test_ifex b = (s. bval b s)"
proof -
  interpret reduced_bdt_checkers ifex_of bval
    by (unfold_locales; insert val_ifex reduced_ifex; blast)
  show ?thesis
    by (simp add: my_taut_test_ifex_def taut_test)
qed

subsection ‹Test: Pigeonhole Formulas›

definition "Or b1 b2 == Neg (And (Neg b1) (Neg b2))"
definition "ors = foldl Or (Const False)"
definition "ands = foldl And (Const True)"

definition "pc n = ands[ors[Atom(i,j). j <- [1..<n+1]]. i <- [1..<n+2]]"
definition "nc n = ands[Or (Neg(Atom(i,k))) (Neg(Atom(j,k))). k <- [1..<n+1], i <- [1..<n+1], j <- [i+1..<n+2]]"

definition "php n = Neg(And (pc n) (nc n))"

text ‹Takes about 5 secs each; with 7 instead of 6 it takes about 4 mins (2015).›

lemma "my_taut_test_bool (php 6)"
  by eval

lemma "my_taut_test_ifex (php 6)"
  by eval 

end