Theory HOL.Alethe_Boolean_Rewrites_Lemmas

(*  Title:      HOL/Alethe_Boolean_Rewrites_Lemmas.thy
    Author:     Hanna Lachnitt, Stanford University
*)
theory Alethe_Boolean_Rewrites_Lemmas
  imports Alethe_Rare_Nary_Ops
begin

lemma bool_or_taut_lemma:
  "w ∨ a ∨ foldr (∨) yss (¬ w)"
  "a ∨ foldr (∨) xss (w ∨ aa ∨ foldr (∨) yss (¬ w))"
  "foldr (∨) xss (w ∨ foldr (∨) yss (w ⟶ a ∨ foldr (∨) zss False))"
    apply force
   apply (metis (mono_tags, opaque_lifting) foldr_or_neutral)
  by (metis(full_types) foldr_or_neutral)

lemma bool_and_conf_lemma:
  "¬ foldr (∧) xss (w ∧ aa ∧ foldr (∧) yss (¬ w))"
  "¬ foldr (∧) xss (w ∧ foldr (∧) yss (¬ w ∧ a ∧ foldr (∧) zss True))"
  apply (metis (mono_tags, opaque_lifting) foldr_and_neutral)
  by (metis(full_types) foldr_and_neutral)

lemma bool_and_conf2_lemma:
  "¬ foldr (∧) xss ((¬ w) ∧ aa ∧ foldr (∧) yss w)"
  "¬ foldr (∧) xss ((¬ w) ∧ foldr (∧) yss (w ∧ a ∧ foldr (∧) zss True))"
  apply (metis (mono_tags, opaque_lifting) foldr_and_neutral)
  by (metis(full_types) foldr_and_neutral)

lemma bool_and_dup_lemma:
  "(b ∧ a ∧ foldr (∧) yss b) = (b ∧ a ∧ foldr (∧) yss True)"
  "(a ∧ foldr (∧) xss (b ∧ aa ∧ foldr (∧) yss b)) = (a ∧ foldr (∧) xss (b ∧ aa ∧ foldr (∧) yss True))"
  "foldr (∧) xss (b ∧ foldr (∧) yss (b ∧ a ∧ foldr (∧) zss True)) = foldr (∧) xss (b ∧ foldr (∧) yss (a ∧ foldr (∧) zss True))"
   apply auto[1]
   apply (metis(full_types))
  by (metis(full_types))

lemma bool_and_flatten_lemma:
  "(b ∧ a ∧ foldr (∧) yss True ∧ aa ∧ foldr (∧) zss True) = (b ∧ a ∧ foldr (∧) yss (aa ∧ foldr (∧) zss True))"
  by (metis(full_types) foldr_and_neutral)

lemma bool_or_dup_lemma:
  "(b ∨ a ∨ foldr (∨) yss b) = (b ∨ a ∨ foldr (∨) yss False)"
  "(a ∨ foldr (∨) xss (b ∨ aa ∨ foldr (∨) yss b)) = (a ∨ foldr (∨) xss (b ∨ aa ∨ foldr (∨) yss False))"
  "foldr (∨) xss (b ∨ foldr (∨) yss (b ∨ a ∨ foldr (∨) zss False)) = foldr (∨) xss (b ∨ foldr (∨) yss (a ∨ foldr (∨) zss False))"
    apply auto[1]
   apply (metis(full_types))
  by (metis(full_types))

lemma bool_or_flatten_lemma:
  "(b ∨ a ∨ foldr (∨) yss False ∨ aa ∨ foldr (∨) zss False) = (b ∨ a ∨ foldr (∨) yss (aa ∨ foldr (∨) zss False))"
  "(a ∨ foldr (∨) xss (b ∨ aa ∨ foldr (∨) yss False ∨ aaa ∨ foldr (∨) zss False)) =
  (a ∨ foldr (∨) xss (b ∨ aa ∨ foldr (∨) yss (aaa ∨ foldr (∨) zss False)))"
   apply (metis(full_types) foldr_or_neutral)
  by (metis(full_types) foldr_or_neutral)

lemma bool_or_and_distrib_lemma:
  shows "zs = ListVar zss ⟹
    ys = ListVar yss ⟹
    (y1 ∧ y2 ∧ foldr (∧) yss True ∨ z1 ∨ foldr (∨) zss False) =
    ((y1 ∨ z1 ∨ foldr (∨) zss False) ∧ (y2 ∧ foldr (∧) yss True ∨ z1 ∨ foldr (∨) zss False))"
  using disj_conj_distribR by simp

end