section \Solutions for Session 11\ theory Solutions11 imports Main begin text \ Read and formalize @{doc locales} at least up to and including lemma \join_distr\ on page 5. \ locale partial_order = fixes le :: "'a \ 'a \ bool" (infixl "\" 50) assumes refl [intro, simp]: "x \ x" and anti_sym [intro]: "x \ y \ y \ x \ x = y" and trans [trans]: "x \ y \ y \ z \ x \ z" definition (in partial_order) less :: "'a \ 'a \ bool" (infix "\" 50) where "x \ y \ x \ y \ x \ y" lemma (in partial_order) less_le_trans [trans]: "x \ y \ y \ z \ x \ z" unfolding less_def by (blast intro: trans) context partial_order begin definition "is_inf x y i \ i \ x \ i \ y \ (\z. z \ x \ z \ y \ z \ i)" definition "is_sup x y s \ x \ s \ y \ s \ (\z. x \ z \ y \ z \ s \ 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: "\i. is_inf x y i" and ex_sup: "\s. is_sup x y s" begin definition meet (infix "\" 70) where "x \ y = (THE i. is_inf x y i)" definition join (infix "\" 65) where "x \ y = (THE s. is_sup x y s)" lemma is_inf_meet: "is_inf x y (x \ 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 \ 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 \ y \ x" using is_inf_meet [of x y] by (simp add: is_inf_def) lemma meet_right: "x \ y \ y" using is_inf_meet [of x y] by (simp add: is_inf_def) lemma join_left: "x \ x \ y" using is_sup_join [of x y] by (simp add: is_sup_def) lemma join_right: "y \ x \ y" using is_sup_join [of x y] by (simp add: is_sup_def) lemma le_meetI: "z \ x \ z \ y \ z \ x \ y" using is_inf_meet [of x y] by (auto simp: is_inf_def) lemma meet_leI: "x \ z \ y \ z \ x \ y \ z" using is_inf_meet [of x y] by (auto simp: is_inf_def dest: trans) lemma join_leI: "x \ z \ y \ z \ x \ y \ z" using is_sup_join [of x y] by (auto simp: is_sup_def) lemma join_mono: assumes "x \ u" and "y \ v" shows "x \ y \ u \ v" using assms by (auto dest: trans intro: join_leI join_left join_right) lemma meet_mono: assumes "x \ u" and "y \ v" shows "x \ y \ u \ v" using assms by (auto intro: le_meetI trans meet_left meet_right) lemma meet_commute [ac_simps]: "x \ y = y \ x" using is_inf_meet by (auto simp: is_inf_def) end locale total_order = partial_order + assumes total: "x \ y \ y \ x" lemma (in total_order) less_total: "x \ y \ x = y \ y \ x" using total unfolding less_def by blast locale distrib_lattice = lattice + assumes meet_distr: "x \ (y \ z) = (x \ y) \ (x \ z)" lemma (in distrib_lattice) meet_distr2: "(x \ y) \ z = (x \ z) \ (y \ z)" by (simp add: meet_commute meet_distr) lemma (in distrib_lattice) join_distrib: "x \ (y \ z) = (x \ y) \ (x \ z)" proof (intro anti_sym) have "x \ y \ z \ x \ y" by (auto intro: meet_left join_mono) moreover have "x \ y \ z \ x \ z" by (auto intro: meet_right join_mono) ultimately show "x \ y \ z \ (x \ y) \ (x \ z)" by (intro le_meetI) show "(x \ y) \ (x \ z) \ x \ y \ 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