# 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

definition

definition

definition

definition

definition

definition

definition

lemma Rep_formula_inf:

unfolding inf_formula_def
by (intro Abs_formula_inverse fba.inter Rep_formula)

lemma Rep_formula_sup:

unfolding sup_formula_def
by (intro Abs_formula_inverse fba_union Rep_formula)

lemma Rep_formula_top:
unfolding top_formula_def by (intro Abs_formula_inverse fba_UNIV)

lemma Rep_formula_bot:
unfolding bot_formula_def by (intro Abs_formula_inverse fba_empty)

lemma Rep_formula_compl:
unfolding uminus_formula_def
by (intro Abs_formula_inverse fba.Compl Rep_formula)

lemma Rep_formula_diff:

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
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. (iS. i  A  i  B)
A  Rep_formula x  B  Rep_formula x}"

lemma formulasI:
assumes "A B. iS. 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 "iS. i  A  i  B"
shows
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
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›.

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]

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"
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)"
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
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
›

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