Theory Free_Boolean_Algebra

(*  Title:      Free_Boolean_Algebra.thy
    Author:     Brian Huffman, Portland State University
*)

section ‹Free Boolean algebras›

theory Free_Boolean_Algebra
imports Main
begin

(*<*)
notation
  bot ("⊥") and
  top ("⊤") and
  inf  (infixl "⊓" 70) and
  sup  (infixl "⊔" 65)

lemma sup_conv_inf:
  fixes x y :: "'a::boolean_algebra"
  shows "x ⊔ y = - (- x ⊓ - y)"
by simp
(*>*)

subsection ‹Free boolean algebra as a set›

text ‹
  We start by defining the free boolean algebra over type @{typ 'a} as
  an inductive set.  Here ‹i :: 'a› represents a variable;
  ‹A :: 'a set› represents a valuation, assigning a truth
  value to each variable; and ‹S :: 'a set set› represents a
  formula, as the set of valuations that make the formula true.  The
  set ‹fba› contains representatives of formulas built from
  finite combinations of variables with negation and conjunction.
›

inductive_set
  fba :: "'a set set set"
where
  var: "{A. i ∈ A} ∈ fba"
| Compl: "S ∈ fba ⟹ - S ∈ fba"
| inter: "S ∈ fba ⟹ T ∈ fba ⟹ S ∩ T ∈ fba"

lemma fba_Diff: "S ∈ fba ⟹ T ∈ fba ⟹ S - T ∈ fba"
unfolding Diff_eq by (intro fba.inter fba.Compl)

lemma fba_union: "S ∈ fba ⟹ T ∈ fba ⟹ S ∪ T ∈ fba"
proof -
  assume "S ∈ fba" and "T ∈ fba"
  hence "- (- S ∩ - T) ∈ fba" by (intro fba.intros)
  thus "S ∪ T ∈ fba" by simp
qed

lemma fba_empty: "({} :: 'a set set) ∈ fba"
proof -
  obtain S :: "'a set set" where "S ∈ fba"
    by (fast intro: fba.var)
  hence "S ∩ - S ∈ fba"
    by (intro fba.intros)
  thus ?thesis by simp
qed

lemma fba_UNIV: "(UNIV :: 'a set set) ∈ fba"
proof -
  have "- {} ∈ fba" using fba_empty by (rule fba.Compl)
  thus "UNIV ∈ fba" by simp
qed


subsection ‹Free boolean algebra as a type›

text ‹
  The next step is to use ‹typedef› to define a type isomorphic
  to the set @{const fba}.  We also define a constructor ‹var›
  that corresponds with the similarly-named introduction rule for
  @{const fba}.
›

typedef 'a formula = "fba :: 'a set set set"
  by (auto intro: fba_empty)

definition var :: "'a ⇒ 'a formula"
where "var i = Abs_formula {A. i ∈ A}"

lemma Rep_formula_var: "Rep_formula (var i) = {A. i ∈ A}"
unfolding var_def using fba.var by (rule Abs_formula_inverse)

text ‹
  \medskip
  Now we make type @{typ "'a formula"} into a Boolean algebra.  This
  involves defining the various operations (ordering relations, binary
  infimum and supremum, complement, difference, top and bottom
  elements) and proving that they satisfy the appropriate laws.
›

instantiation formula :: (type) boolean_algebra
begin

definition
  "x ⊓ y = Abs_formula (Rep_formula x ∩ Rep_formula y)"

definition
  "x ⊔ y = Abs_formula (Rep_formula x ∪ Rep_formula y)"

definition
  "⊤ = Abs_formula UNIV"

definition
  "⊥ = Abs_formula {}"

definition
  "x ≤ y ⟷ Rep_formula x ⊆ Rep_formula y"

definition
  "x < y ⟷ Rep_formula x ⊂ Rep_formula y"

definition
  "- x = Abs_formula (- Rep_formula x)"

definition
  "x - y = Abs_formula (Rep_formula x - Rep_formula y)"

lemma Rep_formula_inf:
  "Rep_formula (x ⊓ y) = Rep_formula x ∩ Rep_formula y"
unfolding inf_formula_def
by (intro Abs_formula_inverse fba.inter Rep_formula)

lemma Rep_formula_sup:
  "Rep_formula (x ⊔ y) = Rep_formula x ∪ Rep_formula y"
unfolding sup_formula_def
by (intro Abs_formula_inverse fba_union Rep_formula)

lemma Rep_formula_top: "Rep_formula ⊤ = UNIV"
unfolding top_formula_def by (intro Abs_formula_inverse fba_UNIV)

lemma Rep_formula_bot: "Rep_formula ⊥ = {}"
unfolding bot_formula_def by (intro Abs_formula_inverse fba_empty)

lemma Rep_formula_compl: "Rep_formula (- x) = - Rep_formula x"
unfolding uminus_formula_def
by (intro Abs_formula_inverse fba.Compl Rep_formula)

lemma Rep_formula_diff:
  "Rep_formula (x - y) = Rep_formula x - Rep_formula y"
unfolding minus_formula_def
by (intro Abs_formula_inverse fba_Diff Rep_formula)

lemmas eq_formula_iff = Rep_formula_inject [symmetric]

lemmas Rep_formula_simps =
  less_eq_formula_def less_formula_def eq_formula_iff
  Rep_formula_sup Rep_formula_inf Rep_formula_top Rep_formula_bot
  Rep_formula_compl Rep_formula_diff Rep_formula_var

instance proof
qed (unfold Rep_formula_simps, auto)

end

text ‹
  \medskip
  The laws of a Boolean algebra do not require the top and bottom
  elements to be distinct, so the following rules must be proved
  separately:
›

lemma bot_neq_top_formula [simp]: "(⊥ :: 'a formula) ≠ ⊤"
unfolding Rep_formula_simps by auto

lemma top_neq_bot_formula [simp]: "(⊤ :: 'a formula) ≠ ⊥"
unfolding Rep_formula_simps by auto

text ‹
  \medskip
  Here we prove an essential property of a free Boolean algebra:
  all generators are independent.
›

lemma var_le_var_simps [simp]:
  "var i ≤ var j ⟷ i = j"
  "¬ var i ≤ - var j"
  "¬ - var i ≤ var j"
unfolding Rep_formula_simps by fast+

lemma var_eq_var_simps [simp]:
  "var i = var j ⟷ i = j"
  "var i ≠ - var j"
  "- var i ≠ var j"
unfolding Rep_formula_simps set_eq_subset by fast+

text ‹
  \medskip
  We conclude this section by proving an induction principle for
  formulas.  It mirrors the definition of the inductive set ‹fba›, with cases for variables, complements, and conjunction.
›

lemma formula_induct [case_names var compl inf, induct type: formula]:
  fixes P :: "'a formula ⇒ bool"
  assumes 1: "⋀i. P (var i)"
  assumes 2: "⋀x. P x ⟹ P (- x)"
  assumes 3: "⋀x y. P x ⟹ P y ⟹ P (x ⊓ y)"
  shows "P x"
proof (induct x rule: Abs_formula_induct)
  fix y :: "'a set set"
  assume "y ∈ fba" thus "P (Abs_formula y)"
  proof (induct rule: fba.induct)
    case (var i)
    have "P (var i)" by (rule 1)
    thus ?case unfolding var_def .
  next
    case (Compl S)
    from ‹P (Abs_formula S)› have "P (- Abs_formula S)" by (rule 2)
    with ‹S ∈ fba› show ?case
      unfolding uminus_formula_def by (simp add: Abs_formula_inverse)
  next
    case (inter S T)
    from ‹P (Abs_formula S)› and ‹P (Abs_formula T)›
    have "P (Abs_formula S ⊓ Abs_formula T)" by (rule 3)
    with ‹S ∈ fba› and ‹T ∈ fba› show ?case
      unfolding inf_formula_def by (simp add: Abs_formula_inverse)
  qed
qed


subsection ‹If-then-else for Boolean algebras›

text ‹
  This is a generic if-then-else operator for arbitrary Boolean
  algebras.
›

definition
  ifte :: "'a::boolean_algebra ⇒ 'a ⇒ 'a ⇒ 'a"
where
  "ifte a x y = (a ⊓ x) ⊔ (- a ⊓ y)"

lemma ifte_top [simp]: "ifte ⊤ x y = x"
unfolding ifte_def by simp

lemma ifte_bot [simp]: "ifte ⊥ x y = y"
unfolding ifte_def by simp

lemma ifte_same: "ifte a x x = x"
unfolding ifte_def
by (simp add: inf_sup_distrib2 [symmetric] sup_compl_top)

lemma compl_ifte: "- ifte a x y = ifte a (- x) (- y)"
unfolding ifte_def
apply (rule order_antisym)
apply (simp add: inf_sup_distrib1 inf_sup_distrib2 compl_inf_bot)
apply (simp add: sup_inf_distrib1 sup_inf_distrib2 sup_compl_top)
apply (simp add: le_infI1 le_infI2 le_supI1 le_supI2)
apply (simp add: le_infI1 le_infI2 le_supI1 le_supI2)
done

lemma inf_ifte_distrib:
  "ifte x a b ⊓ ifte x c d = ifte x (a ⊓ c) (b ⊓ d)"
unfolding ifte_def
apply (simp add: inf_sup_distrib1 inf_sup_distrib2)
apply (simp add: inf_sup_aci inf_compl_bot)
done

lemma ifte_ifte_distrib:
  "ifte x (ifte y a b) (ifte y c d) = ifte y (ifte x a c) (ifte x b d)"
unfolding ifte_def [of x] sup_conv_inf
by (simp only: compl_ifte [symmetric] inf_ifte_distrib [symmetric] ifte_same)


subsection ‹Formulas over a set of generators›

text ‹
  The set ‹formulas S› consists of those formulas that only
  depend on variables in the set ‹S›.  It is analogous to the
  @{const lists} operator for the list datatype.
›

definition
  formulas :: "'a set ⇒ 'a formula set"
where
  "formulas S =
    {x. ∀A B. (∀i∈S. i ∈ A ⟷ i ∈ B) ⟶
      A ∈ Rep_formula x ⟷ B ∈ Rep_formula x}"

lemma formulasI:
  assumes "⋀A B. ∀i∈S. i ∈ A ⟷ i ∈ B
    ⟹ A ∈ Rep_formula x ⟷ B ∈ Rep_formula x"
  shows "x ∈ formulas S"
using assms unfolding formulas_def by simp

lemma formulasD:
  assumes "x ∈ formulas S"
  assumes "∀i∈S. i ∈ A ⟷ i ∈ B"
  shows "A ∈ Rep_formula x ⟷ B ∈ Rep_formula x"
using assms unfolding formulas_def by simp

lemma formulas_mono: "S ⊆ T ⟹ formulas S ⊆ formulas T"
by (fast intro!: formulasI elim!: formulasD)

lemma formulas_insert: "x ∈ formulas S ⟹ x ∈ formulas (insert a S)"
unfolding formulas_def by simp

lemma formulas_var: "i ∈ S ⟹ var i ∈ formulas S"
unfolding formulas_def by (simp add: Rep_formula_simps)

lemma formulas_var_iff: "var i ∈ formulas S ⟷ i ∈ S"
unfolding formulas_def by (simp add: Rep_formula_simps, fast)

lemma formulas_bot: "⊥ ∈ formulas S"
unfolding formulas_def by (simp add: Rep_formula_simps)

lemma formulas_top: "⊤ ∈ formulas S"
unfolding formulas_def by (simp add: Rep_formula_simps)

lemma formulas_compl: "x ∈ formulas S ⟹ - x ∈ formulas S"
unfolding formulas_def by (simp add: Rep_formula_simps)

lemma formulas_inf:
  "x ∈ formulas S ⟹ y ∈ formulas S ⟹ x ⊓ y ∈ formulas S"
unfolding formulas_def by (auto simp add: Rep_formula_simps)

lemma formulas_sup:
  "x ∈ formulas S ⟹ y ∈ formulas S ⟹ x ⊔ y ∈ formulas S"
unfolding formulas_def by (auto simp add: Rep_formula_simps)

lemma formulas_diff:
  "x ∈ formulas S ⟹ y ∈ formulas S ⟹ x - y ∈ formulas S"
unfolding formulas_def by (auto simp add: Rep_formula_simps)

lemma formulas_ifte:
  "a ∈ formulas S ⟹ x ∈ formulas S ⟹ y ∈ formulas S ⟹
    ifte a x y ∈ formulas S"
unfolding ifte_def
by (intro formulas_sup formulas_inf formulas_compl)

lemmas formulas_intros =
  formulas_var formulas_bot formulas_top formulas_compl
  formulas_inf formulas_sup formulas_diff formulas_ifte


subsection ‹Injectivity of if-then-else›

text ‹
  The if-then-else operator is injective in some limited
  circumstances: when the scrutinee is a variable that is not
  mentioned in either branch.
›

lemma ifte_inject:
  assumes "ifte (var i) x y = ifte (var i) x' y'" 
  assumes "i ∉ S"
  assumes "x ∈ formulas S" and "x' ∈ formulas S"
  assumes "y ∈ formulas S" and "y' ∈ formulas S"
  shows "x = x' ∧ y = y'"
proof
  have 1: "⋀A. i ∈ A ⟹ A ∈ Rep_formula x ⟷ A ∈ Rep_formula x'"
    using assms(1)
    by (simp add: Rep_formula_simps ifte_def set_eq_iff, fast)
  have 2: "⋀A. i ∉ A ⟹ A ∈ Rep_formula y ⟷ A ∈ Rep_formula y'"
    using assms(1)
    by (simp add: Rep_formula_simps ifte_def set_eq_iff, fast)

  show "x = x'"
  unfolding Rep_formula_simps
  proof (rule set_eqI)
    fix A
    have "A ∈ Rep_formula x ⟷ insert i A ∈ Rep_formula x"
      using ‹x ∈ formulas S› by (rule formulasD, force simp add: ‹i ∉ S›)
    also have "… ⟷ insert i A ∈ Rep_formula x'"
      by (rule 1, simp)
    also have "… ⟷ A ∈ Rep_formula x'"
      using ‹x' ∈ formulas S› by (rule formulasD, force simp add: ‹i ∉ S›)
    finally show "A ∈ Rep_formula x ⟷ A ∈ Rep_formula x'" .
  qed
  show  "y = y'"
  unfolding Rep_formula_simps
  proof (rule set_eqI)
    fix A
    have "A ∈ Rep_formula y ⟷ A - {i} ∈ Rep_formula y"
      using ‹y ∈ formulas S› by (rule formulasD, force simp add: ‹i ∉ S›)
    also have "… ⟷ A - {i} ∈ Rep_formula y'"
      by (rule 2, simp)
    also have "… ⟷ A ∈ Rep_formula y'"
      using ‹y' ∈ formulas S› by (rule formulasD, force simp add: ‹i ∉ S›)
    finally show "A ∈ Rep_formula y ⟷ A ∈ Rep_formula y'" .
  qed
qed


subsection ‹Specification of homomorphism operator›

text ‹
  Our goal is to define a homomorphism operator ‹hom› such that
  for any function ‹f›, ‹hom f› is the unique Boolean
  algebra homomorphism satisfying ‹hom f (var i) = f i›
  for all ‹i›.

  Instead of defining ‹hom› directly, we will follow the
  approach used to define Isabelle's ‹fold› operator for finite
  sets.  First we define the graph of the ‹hom› function as a
  relation; later we will define the ‹hom› function itself using
  definite choice.

  The ‹hom_graph› relation is defined inductively, with
  introduction rules based on the if-then-else normal form of Boolean
  formulas.  The relation is also indexed by an extra set parameter
  ‹S›, to ensure that branches of each if-then-else do not use
  the same variable again.
›

inductive
  hom_graph ::
    "('a ⇒ 'b::boolean_algebra) ⇒ 'a set ⇒ 'a formula ⇒ 'b ⇒ bool"
  for f :: "'a ⇒ 'b::boolean_algebra"
where
  bot: "hom_graph f {} bot bot"
| top: "hom_graph f {} top top"
| ifte: "i ∉ S ⟹ hom_graph f S x a ⟹ hom_graph f S y b ⟹
  hom_graph f (insert i S) (ifte (var i) x y) (ifte (f i) a b)"

text ‹
  \medskip
  The next two lemmas establish a stronger elimination rule for
  assumptions of the form @{term "hom_graph f (insert i S) x a"}.
  Essentially, they say that we can arrange the top-level if-then-else
  to use the variable of our choice.  The proof makes use of the
  distributive properties of if-then-else.
›

lemma hom_graph_dest:
  "hom_graph f S x a ⟹ k ∈ S ⟹ ∃y z b c.
    x = ifte (var k) y z ∧ a = ifte (f k) b c ∧
    hom_graph f (S - {k}) y b ∧ hom_graph f (S - {k}) z c"
proof (induct set: hom_graph)
  case (ifte i S x a y b) show ?case
  proof (cases "i = k")
    assume "i = k" with ifte(1,2,4) show ?case by auto
  next
    assume "i ≠ k"
    with ‹k ∈ insert i S› have k: "k ∈ S" by simp
    have *: "insert i S - {k} = insert i (S - {k})"
      using ‹i ≠ k› by (simp add: insert_Diff_if)
    have **: "i ∉ S - {k}" using ‹i ∉ S› by simp
    from ifte(1) ifte(3) [OF k] ifte(5) [OF k]
    show ?case
      unfolding *
      apply clarify
      apply (simp only: ifte_ifte_distrib [of "var i"])
      apply (simp only: ifte_ifte_distrib [of "f i"])
      apply (fast intro: hom_graph.ifte [OF **])
      done
  qed
qed simp_all

lemma hom_graph_insert_elim:
  assumes "hom_graph f (insert i S) x a" and "i ∉ S"
  obtains y z b c
  where "x = ifte (var i) y z"
    and "a = ifte (f i) b c"
    and "hom_graph f S y b"
    and "hom_graph f S z c"
using hom_graph_dest [OF assms(1) insertI1]
by (clarify, simp add: assms(2))

text ‹
  \medskip
  Now we prove the first uniqueness property of the @{const hom_graph}
  relation.  This version of uniqueness says that for any particular
  value of ‹S›, the relation @{term "hom_graph f S"} maps each
  ‹x› to at most one ‹a›.  The proof uses the
  injectiveness of if-then-else, which we proved earlier.
›

lemma hom_graph_imp_formulas:
  "hom_graph f S x a ⟹ x ∈ formulas S"
by (induct set: hom_graph, simp_all add: formulas_intros formulas_insert)

lemma hom_graph_unique:
  "hom_graph f S x a ⟹ hom_graph f S x a' ⟹ a = a'"
proof (induct arbitrary: a' set: hom_graph)
  case (ifte i S y b z c a')
  from ifte(6,1) obtain y' z' b' c'
    where 1: "ifte (var i) y z = ifte (var i) y' z'"
      and 2: "a' = ifte (f i) b' c'"
      and 3: "hom_graph f S y' b'"
      and 4: "hom_graph f S z' c'"
    by (rule hom_graph_insert_elim)
  from 1 3 4 ifte(1,2,4) have "y = y' ∧ z = z'"
    by (intro ifte_inject hom_graph_imp_formulas)
  with 2 3 4 ifte(3,5) show "ifte (f i) b c = a'"
    by simp
qed (erule hom_graph.cases, simp_all)+

text ‹
  \medskip
  The next few lemmas will help to establish a stronger version of the
  uniqueness property of @{const hom_graph}.  They show that the @{const
  hom_graph} relation is preserved if we replace ‹S› with a
  larger finite set.
›

lemma hom_graph_insert:
  assumes "hom_graph f S x a"
  shows "hom_graph f (insert i S) x a"
proof (cases "i ∈ S")
  assume "i ∈ S" with assms show ?thesis by (simp add: insert_absorb)
next
  assume "i ∉ S"
  hence "hom_graph f (insert i S) (ifte (var i) x x) (ifte (f i) a a)"
    by (intro hom_graph.ifte assms)
  thus "hom_graph f (insert i S) x a"
    by (simp only: ifte_same)
qed

lemma hom_graph_finite_superset:
  assumes "hom_graph f S x a" and "finite T" and "S ⊆ T"
  shows "hom_graph f T x a"
proof -
  from ‹finite T› have "hom_graph f (S ∪ T) x a"
    by (induct set: finite, simp add: assms, simp add: hom_graph_insert)
  with ‹S ⊆ T› show "hom_graph f T x a"
    by (simp only: subset_Un_eq)
qed

lemma hom_graph_imp_finite:
  "hom_graph f S x a ⟹ finite S"
by (induct set: hom_graph) simp_all

text ‹
  \medskip
  This stronger uniqueness property says that @{term "hom_graph f"}
  maps each ‹x› to at most one ‹a›, even for
  \emph{different} values of the set parameter.
›

lemma hom_graph_unique':
  assumes "hom_graph f S x a" and "hom_graph f T x a'"
  shows "a = a'"
proof (rule hom_graph_unique)
  have fin: "finite (S ∪ T)"
    using assms by (intro finite_UnI hom_graph_imp_finite)
  show "hom_graph f (S ∪ T) x a"
    using assms(1) fin Un_upper1 by (rule hom_graph_finite_superset)
  show "hom_graph f (S ∪ T) x a'"
    using assms(2) fin Un_upper2 by (rule hom_graph_finite_superset)
qed

text ‹
  \medskip
  Finally, these last few lemmas establish that the @{term "hom_graph
  f"} relation is total: every ‹x› is mapped to some ‹a›.
›

lemma hom_graph_var: "hom_graph f {i} (var i) (f i)"
proof -
  have "hom_graph f {i} (ifte (var i) top bot) (ifte (f i) top bot)"
    by (simp add: hom_graph.intros)
  thus "hom_graph f {i} (var i) (f i)"
    unfolding ifte_def by simp
qed

lemma hom_graph_compl:
  "hom_graph f S x a ⟹ hom_graph f S (- x) (- a)"
by (induct set: hom_graph, simp_all add: hom_graph.intros compl_ifte)

lemma hom_graph_inf:
  "hom_graph f S x a ⟹ hom_graph f S y b ⟹
   hom_graph f S (x ⊓ y) (a ⊓ b)"
 apply (induct arbitrary: y b set: hom_graph)
   apply (simp add: hom_graph.bot)
  apply simp
 apply (erule (1) hom_graph_insert_elim)
 apply (auto simp add: inf_ifte_distrib hom_graph.ifte)
done

lemma hom_graph_union_inf:
  assumes "hom_graph f S x a" and "hom_graph f T y b"
  shows "hom_graph f (S ∪ T) (x ⊓ y) (a ⊓ b)"
proof (rule hom_graph_inf)
  have fin: "finite (S ∪ T)"
    using assms by (intro finite_UnI hom_graph_imp_finite)
  show "hom_graph f (S ∪ T) x a"
    using assms(1) fin Un_upper1 by (rule hom_graph_finite_superset)
  show "hom_graph f (S ∪ T) y b"
    using assms(2) fin Un_upper2 by (rule hom_graph_finite_superset)
qed

lemma hom_graph_exists: "∃a S. hom_graph f S x a"
by (induct x)
   (auto intro: hom_graph_var hom_graph_compl hom_graph_union_inf)


subsection ‹Homomorphisms into other boolean algebras›

text ‹
  Now that we have proved the necessary existence and uniqueness
  properties of @{const hom_graph}, we can define the function ‹hom› using definite choice.
›

definition
  hom :: "('a ⇒ 'b::boolean_algebra) ⇒ 'a formula ⇒ 'b"
where
  "hom f x = (THE a. ∃S. hom_graph f S x a)"

lemma hom_graph_hom: "∃S. hom_graph f S x (hom f x)"
unfolding hom_def
apply (rule theI')
apply (rule ex_ex1I)
apply (rule hom_graph_exists)
apply (fast elim: hom_graph_unique')
done

lemma hom_equality:
  "hom_graph f S x a ⟹ hom f x = a"
unfolding hom_def
apply (rule the_equality)
apply (erule exI)
apply (erule exE)
apply (erule (1) hom_graph_unique')
done

text ‹
  \medskip
  The @{const hom} function correctly implements its specification:
›

lemma hom_var [simp]: "hom f (var i) = f i"
by (rule hom_equality, rule hom_graph_var)

lemma hom_bot [simp]: "hom f ⊥ = ⊥"
by (rule hom_equality, rule hom_graph.bot)

lemma hom_top [simp]: "hom f ⊤ = ⊤"
by (rule hom_equality, rule hom_graph.top)

lemma hom_compl [simp]: "hom f (- x) = - hom f x"
proof -
  obtain S where "hom_graph f S x (hom f x)"
    using hom_graph_hom ..
  hence "hom_graph f S (- x) (- hom f x)"
    by (rule hom_graph_compl)
  thus "hom f (- x) = - hom f x"
    by (rule hom_equality)
qed

lemma hom_inf [simp]: "hom f (x ⊓ y) = hom f x ⊓ hom f y"
proof -
  obtain S where S: "hom_graph f S x (hom f x)"
    using hom_graph_hom ..
  obtain T where T: "hom_graph f T y (hom f y)"
    using hom_graph_hom ..
  have "hom_graph f (S ∪ T) (x ⊓ y) (hom f x ⊓ hom f y)"
    using S T by (rule hom_graph_union_inf)
  thus ?thesis by (rule hom_equality)
qed

lemma hom_sup [simp]: "hom f (x ⊔ y) = hom f x ⊔ hom f y"
unfolding sup_conv_inf by (simp only: hom_compl hom_inf)

lemma hom_diff [simp]: "hom f (x - y) = hom f x - hom f y"
unfolding diff_eq by (simp only: hom_compl hom_inf)

lemma hom_ifte [simp]:
  "hom f (ifte x y z) = ifte (hom f x) (hom f y) (hom f z)"
unfolding ifte_def by (simp only: hom_compl hom_inf hom_sup)

lemmas hom_simps =
  hom_var hom_bot hom_top hom_compl
  hom_inf hom_sup hom_diff hom_ifte

text ‹
  \medskip
  The type @{typ "'a formula"} can be viewed as a monad, with @{const
  var} as the unit, and @{const hom} as the bind operator.  We can
  prove the standard monad laws with simple proofs by induction.
›

lemma hom_var_eq_id: "hom var x = x"
by (induct x) simp_all

lemma hom_hom: "hom f (hom g x) = hom (λi. hom f (g i)) x"
by (induct x) simp_all


subsection ‹Map operation on Boolean formulas›

text ‹
  We can define a map functional in terms of @{const hom} and @{const
  var}.  The properties of ‹fmap› follow directly from the
  lemmas we have already proved about @{const hom}.
›

definition
  fmap :: "('a ⇒ 'b) ⇒ 'a formula ⇒ 'b formula"
where
  "fmap f = hom (λi. var (f i))"

lemma fmap_var [simp]: "fmap f (var i) = var (f i)"
unfolding fmap_def by simp

lemma fmap_bot [simp]: "fmap f ⊥ = ⊥"
unfolding fmap_def by simp

lemma fmap_top [simp]: "fmap f ⊤ = ⊤"
unfolding fmap_def by simp

lemma fmap_compl [simp]: "fmap f (- x) = - fmap f x"
unfolding fmap_def by simp

lemma fmap_inf [simp]: "fmap f (x ⊓ y) = fmap f x ⊓ fmap f y"
unfolding fmap_def by simp

lemma fmap_sup [simp]: "fmap f (x ⊔ y) = fmap f x ⊔ fmap f y"
unfolding fmap_def by simp

lemma fmap_diff [simp]: "fmap f (x - y) = fmap f x - fmap f y"
unfolding fmap_def by simp

lemma fmap_ifte [simp]:
  "fmap f (ifte x y z) = ifte (fmap f x) (fmap f y) (fmap f z)"
unfolding fmap_def by simp

lemmas fmap_simps =
  fmap_var fmap_bot fmap_top fmap_compl
  fmap_inf fmap_sup fmap_diff fmap_ifte

text ‹
  \medskip
  The map functional satisfies the functor laws: it preserves identity
  and function composition.
›

lemma fmap_ident: "fmap (λi. i) x = x"
by (induct x) simp_all

lemma fmap_fmap: "fmap f (fmap g x) = fmap (f ∘ g) x"
by (induct x) simp_all


subsection ‹Hiding lattice syntax›

text ‹
  The following command hides the lattice syntax, to avoid potential
  conflicts with other theories that import this one.  To re-enable
  the syntax, users should unbundle ‹lattice_syntax›.
›

unbundle no_lattice_syntax

end