section \<open>Solutions for Session 11\<close>

theory Solutions11
  imports Main
begin

text \<open>
Read and formalize @{doc locales} at least up to and including
lemma \<open>join_distr\<close> on page 5.
\<close>

locale partial_order =
  fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
  assumes refl [intro, simp]: "x \<sqsubseteq> x"
    and anti_sym [intro]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
    and trans [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"

definition (in partial_order) less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubset>" 50)
  where
    "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"

lemma (in partial_order) less_le_trans [trans]:
  "x \<sqsubset> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubset> z"
  unfolding less_def by (blast intro: trans)

context partial_order
begin

definition "is_inf x y i \<longleftrightarrow> i \<sqsubseteq> x \<and> i \<sqsubseteq> y \<and> (\<forall>z. z \<sqsubseteq> x \<and> z \<sqsubseteq> y \<longrightarrow> z \<sqsubseteq> i)"

definition "is_sup x y s \<longleftrightarrow> x \<sqsubseteq> s \<and> y \<sqsubseteq> s \<and> (\<forall>z. x \<sqsubseteq> z \<and> y \<sqsubseteq> z \<longrightarrow> s \<sqsubseteq> z)"

lemma is_inf_uniq:
  assumes "is_inf x y i" and "is_inf x y j"
  shows "i = j"
  using assms by (auto simp: is_inf_def)

lemma is_sup_uniq:
  assumes "is_sup x y s" and "is_sup x y t"
  shows "s = t"
  using assms by (auto simp: is_sup_def)

end

locale lattice = partial_order +
  assumes ex_inf: "\<exists>i. is_inf x y i"
    and ex_sup: "\<exists>s. is_sup x y s"
begin

definition meet (infix "\<sqinter>" 70)
  where
    "x \<sqinter> y = (THE i. is_inf x y i)"

definition join (infix "\<squnion>" 65)
  where
    "x \<squnion> y = (THE s. is_sup x y s)"

lemma is_inf_meet: "is_inf x y (x \<sqinter> y)"
proof -
  from ex_inf obtain i where "is_inf x y i" ..
  then show ?thesis by (auto simp: meet_def intro: theI is_inf_uniq)
qed

lemma is_sup_join: "is_sup x y (x \<squnion> y)"
proof -
  from ex_sup obtain s where "is_sup x y s" ..
  then show ?thesis by (auto simp: join_def intro: theI is_sup_uniq)
qed

lemma meet_left: "x \<sqinter> y \<sqsubseteq> x"
  using is_inf_meet [of x y] by (simp add: is_inf_def)

lemma meet_right: "x \<sqinter> y \<sqsubseteq> y"
  using is_inf_meet [of x y] by (simp add: is_inf_def)

lemma join_left: "x \<sqsubseteq> x \<squnion> y"
  using is_sup_join [of x y] by (simp add: is_sup_def)

lemma join_right: "y \<sqsubseteq> x \<squnion> y"
  using is_sup_join [of x y] by (simp add: is_sup_def)

lemma le_meetI:
  "z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y"
  using is_inf_meet [of x y] by (auto simp: is_inf_def)

lemma meet_leI:
  "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqinter> y \<sqsubseteq> z"
  using is_inf_meet [of x y]
  by (auto simp: is_inf_def dest: trans)

lemma join_leI:
  "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
  using is_sup_join [of x y] by (auto simp: is_sup_def)

lemma join_mono:
  assumes "x \<sqsubseteq> u" and "y \<sqsubseteq> v"
  shows "x \<squnion> y \<sqsubseteq> u \<squnion> v"
  using assms by (auto dest: trans intro: join_leI join_left join_right)

lemma meet_mono:
  assumes "x \<sqsubseteq> u" and "y \<sqsubseteq> v"
  shows "x \<sqinter> y \<sqsubseteq> u \<sqinter> v"
  using assms by (auto intro: le_meetI trans meet_left meet_right)

lemma meet_commute [ac_simps]:
  "x \<sqinter> y = y \<sqinter> x"
  using is_inf_meet by (auto simp: is_inf_def)

end

locale total_order = partial_order +
  assumes total: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"

lemma (in total_order) less_total: "x \<sqsubset> y \<or> x = y \<or> y \<sqsubset> x"
  using total unfolding less_def by blast

locale distrib_lattice = lattice +
  assumes meet_distr: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"

lemma (in distrib_lattice) meet_distr2: "(x \<squnion> y) \<sqinter> z = (x \<sqinter> z) \<squnion> (y \<sqinter> z)"
  by (simp add: meet_commute meet_distr)

lemma (in distrib_lattice) join_distrib: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
proof (intro anti_sym)
  have "x \<squnion> y \<sqinter> z \<sqsubseteq> x \<squnion> y"
    by (auto intro: meet_left join_mono)
  moreover have "x \<squnion> y \<sqinter> z \<sqsubseteq> x \<squnion> z"
    by (auto intro: meet_right join_mono)
  ultimately show "x \<squnion> y \<sqinter> z \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    by (intro le_meetI)
  show "(x \<squnion> y) \<sqinter> (x \<squnion> z) \<sqsubseteq> x \<squnion> y \<sqinter> z"
    unfolding meet_distr
    by (intro join_leI)
      (auto intro: join_left meet_right trans simp: join_mono meet_left meet_distr2 [of x y z])
qed

end