Theory Representation

theory Representation

imports Stone_Relation_Algebras.Matrix_Relation_Algebras

begin

section ‹Representation of Stone Relation Algebras›

text ‹
We show that Stone relation algebras can be represented by matrices if we assume a point axiom.
The matrix indices and entries and the point axiom are based on the concepts of ideals and ideal-points.
We start with general results about sets and finite suprema.
›

lemma finite_ne_subset_induct' [consumes 3, case_names singleton insert]:
  assumes "finite F"
      and "F ≠ {}"
      and "F ⊆ S"
      and singleton: "⋀x . x ∈ S ⟹ P {x}"
      and insert: "⋀x F . finite F ⟹ F ≠ {} ⟹ F ⊆ S ⟹ x ∈ S ⟹ x ∉ F ⟹ P F ⟹ P (insert x F)"
    shows "P F"
  using assms(1-3)
  apply (induct rule: finite_ne_induct)
  apply (simp add: singleton)
  by (simp add: insert)

context order_bot
begin

abbreviation atom :: "'a ⇒ bool"
  where "atom x ≡ x ≠ bot ∧ (∀y . y ≠ bot ∧ y ≤ x ⟶ y = x)"

end

context semilattice_sup
begin

lemma nested_sup_fin:
  assumes "finite X"
      and "X ≠ {}"
      and "finite Y"
      and "Y ≠ {}"
    shows "Sup_fin { Sup_fin { f x y | x . x ∈ X } | y . y ∈ Y } = Sup_fin { f x y | x y . x ∈ X ∧ y ∈ Y }"
proof (rule order.antisym)
  have 1: "finite { f x y | x y . x ∈ X ∧ y ∈ Y }"
  proof -
    have "finite (X × Y)"
      by (simp add: assms(1,3))
    hence "finite { f (fst z) (snd z) | z . z ∈ X × Y }"
      by (metis (mono_tags) Collect_mem_eq finite_image_set)
    thus ?thesis
      by auto
  qed
  show "Sup_fin { Sup_fin { f x y | x . x ∈ X } | y . y ∈ Y } ≤ Sup_fin { f x y | x y . x ∈ X ∧ y ∈ Y }"
    apply (rule Sup_fin.boundedI)
    subgoal by (simp add: assms(3))
    subgoal using assms(4) by blast
    subgoal for a
    proof -
      assume "a ∈ { Sup_fin { f x y | x . x ∈ X } | y . y ∈ Y }"
      from this obtain y where 2: "y ∈ Y ∧ a = Sup_fin { f x y | x . x ∈ X }"
        by auto
      have "Sup_fin { f x y | x . x ∈ X } ≤ Sup_fin { f x y | x y . x ∈ X ∧ y ∈ Y }"
        apply (rule Sup_fin.boundedI)
        subgoal by (simp add: assms(1))
        subgoal using assms(2) by blast
        subgoal using Sup_fin.coboundedI 1 2 by blast
        done
      thus ?thesis
        using 2 by simp
    qed
    done
  show "Sup_fin { f x y | x y . x ∈ X ∧ y ∈ Y } ≤ Sup_fin { Sup_fin { f x y | x . x ∈ X } | y . y ∈ Y }"
    apply (rule Sup_fin.boundedI)
    subgoal using 1 by simp
    subgoal using assms(2,4) by blast
    subgoal for a
    proof -
      assume "a ∈ { f x y | x y . x ∈ X ∧ y ∈ Y }"
      from this obtain x y where 3: "x ∈ X ∧ y ∈ Y ∧ a = f x y"
        by auto
      have "a ≤ Sup_fin { f x y | x . x ∈ X }"
        apply (rule Sup_fin.coboundedI)
        apply (simp add: assms(1))
        using 3 by blast
      also have "... ≤ Sup_fin { Sup_fin { f x y | x . x ∈ X } | y . y ∈ Y }"
        apply (rule Sup_fin.coboundedI)
        apply (simp add: assms(3))
        using 3 by blast
      finally show "a ≤ Sup_fin { Sup_fin { f x y | x . x ∈ X } | y . y ∈ Y }"
        .
    qed
    done
qed

end

context bounded_semilattice_sup_bot
begin

lemma one_point_sup_fin:
  assumes "finite X"
      and "y ∈ X"
    shows "Sup_fin { (if x = y then f x else bot) | x . x ∈ X } = f y"
proof (rule order.antisym)
  show "Sup_fin { (if x = y then f x else bot) | x . x ∈ X } ≤ f y"
    apply (rule Sup_fin.boundedI)
    apply (simp add: assms(1))
    using assms(2) apply blast
    by auto
  show "f y ≤ Sup_fin { (if x = y then f x else bot) | x . x ∈ X }"
    apply (rule Sup_fin.coboundedI)
    using assms by auto
qed

end

subsection ‹Ideals and Ideal-Points›

text ‹
We study ideals in Stone relation algebras, which are elements that are both a vector and a covector.
We include general results about Stone relation algebras.
›

context times_top
begin

abbreviation ideal :: "'a ⇒ bool" where "ideal x ≡ vector x ∧ covector x"

end

context bounded_non_associative_left_semiring
begin

lemma ideal_fixpoint:
  "ideal x ⟷ top * x * top = x"
  by (metis order.antisym top_left_mult_increasing top_right_mult_increasing)

lemma ideal_top_closed:
  "ideal top"
  by simp

end

context bounded_idempotent_left_semiring
begin

lemma ideal_mult_closed:
  "ideal x ⟹ ideal y ⟹ ideal (x * y)"
  by (metis mult_assoc)

end

context bounded_idempotent_left_zero_semiring
begin

lemma ideal_sup_closed:
  "ideal x ⟹ ideal y ⟹ ideal (x ⊔ y)"
  by (simp add: covector_sup_closed vector_sup_closed)

end

context idempotent_semiring
begin

lemma sup_fin_sum:
  fixes f :: "'b::finite ⇒ 'a"
  shows "Sup_fin { f x | x . x ∈ UNIV } = (⨆⇩x f x)"
proof (rule order.antisym)
  show "Sup_fin { f x | x . x ∈ UNIV } ≤ (⨆⇩x f x)"
    apply (rule Sup_fin.boundedI)
    apply (metis (mono_tags) finite finite_image_set)
    apply blast
    using ub_sum by auto
next
  show "(⨆⇩x f x) ≤ Sup_fin { f x | x . x ∈ UNIV }"
    apply (rule lub_sum, rule allI)
    apply (rule Sup_fin.coboundedI)
    apply (metis (mono_tags) finite finite_image_set)
    by auto
qed

end

context stone_relation_algebra
begin

lemma dedekind_univalent:
  assumes "univalent y"
    shows "x * y ⊓ z = (x ⊓ z * y⇧T) * y"
proof (rule order.antisym)
  show "x * y ⊓ z ≤ (x ⊓ z * y⇧T) * y"
    by (simp add: dedekind_2)
next
  have "(x ⊓ z * y⇧T) * y ≤ x * y ⊓ z * y⇧T * y"
    using comp_left_subdist_inf by auto
  also have "... ≤ x * y ⊓ z"
    by (metis assms comp_associative comp_inf.mult_right_isotone comp_right_one mult_right_isotone)
  finally show "(x ⊓ z * y⇧T) * y ≤ x * y ⊓ z"
    .
qed

lemma dedekind_injective:
  assumes "injective x"
    shows "x * y ⊓ z = x * (y ⊓ x⇧T * z)"
proof (rule order.antisym)
  show "x * y ⊓ z ≤ x * (y ⊓ x⇧T * z)"
    by (simp add: dedekind_1)
next
  have "x * (y ⊓ x⇧T * z) ≤ x * y ⊓ x * x⇧T * z"
    using comp_associative comp_right_subdist_inf by auto
  also have "... ≤ x * y ⊓ z"
    by (metis assms coreflexive_comp_top_inf inf.boundedE inf.boundedI inf.cobounded2 inf_le1)
  finally show "x * (y ⊓ x⇧T * z) ≤ x * y ⊓ z"
    .
qed

lemma domain_vector_conv:
  "1 ⊓ x * top = 1 ⊓ x * x⇧T"
  by (metis comp_right_one dedekind_eq ex231a inf.sup_monoid.add_commute inf_top.right_neutral total_conv_surjective vector_conv_covector vector_top_closed)

lemma domain_vector_covector:
  "1 ⊓ x * top = 1 ⊓ top * x⇧T"
  by (metis conv_dist_comp one_inf_conv symmetric_top_closed)

lemma domain_covector_conv:
  "1 ⊓ top * x⇧T = 1 ⊓ x * x⇧T"
  using domain_vector_conv domain_vector_covector by auto

lemma ideal_bot_closed:
  "ideal bot"
  by simp

lemma ideal_inf_closed:
  "ideal x ⟹ ideal y ⟹ ideal (x ⊓ y)"
  by (simp add: covector_comp_inf vector_inf_comp)

lemma ideal_conv_closed:
  "ideal x ⟹ ideal (x⇧T)"
  using covector_conv_vector vector_conv_covector by blast

lemma ideal_complement_closed:
  "ideal x ⟹ ideal (-x)"
  by (simp add: covector_complement_closed vector_complement_closed)

lemma ideal_conv_id:
  "ideal x ⟹ x = x⇧T"
  by (metis covector_comp_inf_1 inf.sup_monoid.add_commute inf_top.right_neutral mult_left_one vector_inf_comp)

lemma ideal_mult_inf:
  "ideal x ⟹ ideal y ⟹ x * y = x ⊓ y"
  by (metis inf_top_right vector_inf_comp)

lemma ideal_mult_import:
  "ideal x ⟹ y * z ⊓ x = (y ⊓ x) * (z ⊓ x)"
  using covector_comp_inf inf.sup_monoid.add_commute vector_inf_comp by auto

lemma point_meet_one:
  "point x ⟹ x * x⇧T = x ⊓ 1"
  by (metis domain_vector_conv inf.absorb2 inf.sup_monoid.add_commute)

lemma below_point_eq_domain:
  "point x ⟹ y ≤ x ⟹ y = x * x⇧T * y"
  by (metis inf.absorb2 vector_export_comp_unit point_meet_one)

lemma covector_mult_vector_ideal:
  "vector x ⟹ vector z ⟹ ideal (x⇧T * y * z)"
  by (metis comp_associative vector_conv_covector)

abbreviation ideal_point :: "'a ⇒ bool" where "ideal_point x ≡ point x ∧ (∀y z . point y ∧ ideal z ∧ z ≠ bot ∧ y * z ≤ x ⟶ y ≤ x)"

lemma different_ideal_points_disjoint:
  assumes "ideal_point p"
      and "ideal_point q"
      and "p ≠ q"
    shows "p ⊓ q = bot"
proof (rule ccontr)
  let ?r = "p⇧T * (p ⊓ q)"
  assume 1: "p ⊓ q ≠ bot"
  have 2: "p ⊓ q = p * ?r"
    by (metis assms(1) comp_associative inf.left_idem vector_export_comp_unit point_meet_one)
  have "ideal ?r"
    by (meson assms(1,2) covector_mult_closed vector_conv_covector vector_inf_closed vector_mult_closed)
  hence "p ≤ q"
    using 1 2 by (metis assms(1,2) inf_le2 semiring.mult_not_zero)
  thus "False"
    by (metis assms dual_order.eq_iff epm_3)
qed

lemma points_disjoint_iff:
  assumes "vector x"
    shows "x ⊓ y = bot ⟷ x⇧T * y = bot"
  by (metis assms inf_top_right schroeder_1)

lemma different_ideal_points_disjoint_2:
  assumes "ideal_point p"
      and "ideal_point q"
      and "p ≠ q"
    shows "p⇧T * q = bot"
  using assms different_ideal_points_disjoint points_disjoint_iff by blast

lemma mult_right_dist_sup_fin:
  assumes "finite X"
      and "X ≠ {}"
    shows "Sup_fin { f x | x::'b . x ∈ X } * y = Sup_fin { f x * y | x . x ∈ X }"
proof (rule finite_ne_induct[where F="X"])
  show "finite X"
    using assms(1) by simp
  show "X ≠ {}"
    using assms(2) by simp
  show "⋀z . Sup_fin { f x | x . x ∈ {z} } * y = Sup_fin { f x * y | x . x ∈ {z} }"
    by auto
  fix z F
  assume 1: "finite F" "F ≠ {}" "z ∉ F" "Sup_fin { f x | x . x ∈ F } * y = Sup_fin { f x * y | x . x ∈ F }"
  have "{ f x | x . x ∈ insert z F } = insert (f z) { f x | x . x ∈ F }"
    by auto
  hence "Sup_fin { f x | x . x ∈ insert z F } * y = (f z ⊔ Sup_fin { f x | x . x ∈ F }) * y"
    using Sup_fin.insert 1 by auto
  also have "... = f z * y ⊔ Sup_fin { f x | x . x ∈ F } * y"
    using mult_right_dist_sup by blast
  also have "... = f z * y ⊔ Sup_fin { f x * y | x . x ∈ F }"
    using 1 by simp
  also have "... = Sup_fin (insert (f z * y) { f x * y | x . x ∈ F })"
    using 1 by auto
  also have "... = Sup_fin { f x * y | x . x ∈ insert z F }"
    by (rule arg_cong[where f = "Sup_fin"], auto)
  finally show "Sup_fin { f x | x . x ∈ insert z F } * y = Sup_fin { f x * y | x . x ∈ insert z F }"
    .
qed

lemma mult_left_dist_sup_fin:
  assumes "finite X"
      and "X ≠ {}"
    shows "y * Sup_fin { f x | x::'b . x ∈ X } = Sup_fin { y * f x | x . x ∈ X }"
proof (rule finite_ne_induct[where F="X"])
  show "finite X"
    using assms(1) by simp
  show "X ≠ {}"
    using assms(2) by simp
  show "⋀z . y * Sup_fin { f x | x . x ∈ {z} } = Sup_fin { y * f x | x . x ∈ {z} }"
    by auto
  fix z F
  assume 1: "finite F" "F ≠ {}" "z ∉ F" "y * Sup_fin { f x | x . x ∈ F } = Sup_fin { y * f x | x . x ∈ F }"
  have "{ f x | x . x ∈ insert z F } = insert (f z) { f x | x . x ∈ F }"
    by auto
  hence "y * Sup_fin { f x | x . x ∈ insert z F } = y * (f z ⊔ Sup_fin { f x | x . x ∈ F })"
    using Sup_fin.insert 1 by auto
  also have "... = y * f z ⊔ y * Sup_fin { f x | x . x ∈ F }"
    using mult_left_dist_sup by blast
  also have "... = y * f z ⊔ Sup_fin { y * f x | x . x ∈ F }"
    using 1 by simp
  also have "... = Sup_fin (insert (y * f z) { y * f x | x . x ∈ F })"
    using 1 by auto
  also have "... = Sup_fin { y * f x | x . x ∈ insert z F }"
    by (rule arg_cong[where f = "Sup_fin"], auto)
  finally show "y * Sup_fin { f x | x . x ∈ insert z F } = Sup_fin { y * f x | x . x ∈ insert z F }"
    .
qed

lemma inf_left_dist_sup_fin:
  assumes "finite X"
      and "X ≠ {}"
    shows "y ⊓ Sup_fin { f x | x::'b . x ∈ X } = Sup_fin { y ⊓ f x | x . x ∈ X }"
proof (rule finite_ne_induct[where F="X"])
  show "finite X"
    using assms(1) by simp
  show "X ≠ {}"
    using assms(2) by simp
  show "⋀z . y ⊓ Sup_fin { f x | x . x ∈ {z} } = Sup_fin { y ⊓ f x | x . x ∈ {z} }"
    by auto
  fix z F
  assume 1: "finite F" "F ≠ {}" "z ∉ F" "y ⊓ Sup_fin { f x | x . x ∈ F } = Sup_fin { y ⊓ f x | x . x ∈ F }"
  have "{ f x | x . x ∈ insert z F } = insert (f z) { f x | x . x ∈ F }"
    by auto
  hence "y ⊓ Sup_fin { f x | x . x ∈ insert z F } = y ⊓ (f z ⊔ Sup_fin { f x | x . x ∈ F })"
    using Sup_fin.insert 1 by auto
  also have "... = (y ⊓ f z) ⊔ (y ⊓ Sup_fin { f x | x . x ∈ F })"
    using inf_sup_distrib1 by auto
  also have "... = (y ⊓ f z) ⊔ Sup_fin { y ⊓ f x | x . x ∈ F }"
    using 1 by simp
  also have "... = Sup_fin (insert (y ⊓ f z) { y ⊓ f x | x . x ∈ F })"
    using 1 by auto
  also have "... = Sup_fin { y ⊓ f x | x . x ∈ insert z F }"
    by (rule arg_cong[where f = "Sup_fin"], auto)
  finally show "y ⊓ Sup_fin { f x | x . x ∈ insert z F } = Sup_fin { y ⊓ f x | x . x ∈ insert z F }"
    .
qed

lemma top_one_sup_fin_iff:
  assumes "finite P"
      and "P ≠ {}"
      and "∀p∈P . point p"
    shows "top = Sup_fin P ⟷ 1 = Sup_fin { p * p⇧T | p . p ∈ P }"
proof
  assume "top = Sup_fin P"
  hence "1 = 1 ⊓ Sup_fin P"
    using inf_top_right by auto
  also have "... = Sup_fin { 1 ⊓ p | p . p ∈ P }"
    using inf_Sup1_distrib assms(1,2) by simp
  also have "... = Sup_fin { p * p⇧T | p . p ∈ P }"
    by (metis (no_types, opaque_lifting) point_meet_one assms(3) inf.sup_monoid.add_commute)
  finally show "1 = Sup_fin { p * p⇧T | p . p ∈ P }"
    .
next
  assume "1 = Sup_fin { p * p⇧T | p . p ∈ P }"
  hence "top = Sup_fin { p * p⇧T | p . p ∈ P } * top"
    using total_one_closed by auto
  also have "... = Sup_fin { 1 ⊓ p | p . p ∈ P } * top"
    by (metis (no_types, opaque_lifting) point_meet_one assms(3) inf.sup_monoid.add_commute)
  also have "... = Sup_fin { (1 ⊓ p) * top | p . p ∈ P }"
    using mult_right_dist_sup_fin assms(1,2) by auto
  also have "... = Sup_fin { p | p . p ∈ P }"
    by (metis (no_types, opaque_lifting) assms(3) inf.sup_monoid.add_commute inf_top.right_neutral vector_inf_one_comp)
  finally show "top = Sup_fin P"
    by simp
qed

abbreviation ideals :: "'a set" where "ideals ≡ { x . ideal x }"
abbreviation ideal_points :: "'a set" where "ideal_points ≡ { x . ideal_point x }"

lemma surjective_vector_top:
  "surjective x ⟹ vector x ⟹ x⇧T * x = top"
  by (metis domain_vector_conv covector_inf_comp_3 ex231a inf.sup_monoid.add_commute inf_top.left_neutral vector_export_comp_unit)

lemma point_mult_top:
  "point x ⟹ x⇧T * x = top"
  using surjective_vector_top by blast

lemma point_below_equal:
  "point p ⟹ point q ⟹ p ≤ q ⟹ p = q"
  by (metis below_point_eq_domain comp_associative)

lemma ideal_point_without_ideal:
  "ideal_point p ⟷ (point p ∧ (∀q . point q ⟶ q ≤ p ∨ q ≤ -p))"
proof
  assume 1: "ideal_point p"
  have "∀q . point q ⟶ q ≤ p ∨ q ≤ -p"
  proof (rule allI, rule impI)
    fix q
    assume 2: "point q"
    hence 3: "ideal (q⇧T * p)"
      using 1 by (metis comp_associative vector_conv_covector)
    have "q * (q⇧T * p) ≤ p"
      using 2 shunt_mapping surjective_conv_total by force
    hence "q⇧T * p = bot ∨ q ≤ p"
      using 1 2 3 by blast
    thus "q ≤ p ∨ q ≤ -p"
      using 2 by (metis bot_least schroeder_3_p)
  qed
  thus "point p ∧ (∀q . point q ⟶ q ≤ p ∨ q ≤ -p)"
    using 1 by blast
next
  assume 4: "point p ∧ (∀q . point q ⟶ q ≤ p ∨ q ≤ -p)"
  have "∀y z . point y ∧ ideal z ∧ z ≠ bot ∧ y * z ≤ p ⟶ y ≤ p"
  proof (intro allI, rule impI)
    fix y z
    assume 5: "point y ∧ ideal z ∧ z ≠ bot ∧ y * z ≤ p"
    show "y ≤ p"
    proof (rule ccontr)
      assume "¬ y ≤ p"
      hence "y ≤ -p"
        using 4 5 by blast
      hence "y⇧T * p = bot"
        using 5 points_disjoint_iff pseudo_complement by blast
      thus False
        using 5 bot_unique shunt_mapping surjective_conv_total by force
    qed
  qed
  thus "ideal_point p"
    using 4 by blast
qed

lemma ideal_point_without_ideal_2:
  "ideal_point p ⟷ (point p ∧ (∀q . point q ⟶ q = p ∨ q ≤ -p))"
  by (smt (verit) ideal_point_without_ideal point_below_equal comp_associative mult_semi_associative)

lemma ideal_point_without_ideal_3:
  "ideal_point p ⟷ (point p ∧ (∀q . point q ∧ q ≠ p ⟶ q ≤ -p))"
  using ideal_point_without_ideal_2 by force

end

subsection ‹Point Axiom›

text ‹
The following class captures the point axiom for Stone relation algebras.
›

class stone_relation_algebra_pa = stone_relation_algebra +
  assumes finite_ideal_points: "finite ideal_points"
  assumes ne_ideal_points: "ideal_points ≠ {}"
  assumes top_sup_ideal_points: "top = Sup_fin ideal_points"
begin

lemma one_sup_ideal_points:
  "1 = Sup_fin { p * p⇧T | p . ideal_point p }"
proof -
  have "1 = Sup_fin { p * p⇧T | p . p ∈ ideal_points }"
    using top_one_sup_fin_iff finite_ideal_points ne_ideal_points top_sup_ideal_points by blast
  also have "... = Sup_fin { p * p⇧T | p . ideal_point p }"
    by simp
  finally show ?thesis
    .
qed

lemma ideal_point_rep_1:
  "x = Sup_fin { p * p⇧T * x * q * q⇧T | p q . ideal_point p ∧ ideal_point q }"
proof -
  let ?p = "{ p * p⇧T | p . p ∈ ideal_points }"
  have "x = Sup_fin ?p * (x * Sup_fin ?p)"
    using one_sup_ideal_points by auto
  also have "... = Sup_fin { p * p⇧T * (x * Sup_fin ?p) | p . p ∈ ideal_points }"
    apply (rule mult_right_dist_sup_fin)
    using finite_ideal_points ne_ideal_points by simp_all
  also have "... = Sup_fin { p * p⇧T * x * Sup_fin ?p | p . p ∈ ideal_points }"
    using mult_assoc by simp
  also have "... = Sup_fin { Sup_fin { p * p⇧T * x * q * q⇧T | q . q ∈ ideal_points } | p . p ∈ ideal_points }"
  proof -
    have "⋀p . p * p⇧T * x * Sup_fin ?p = Sup_fin { p * p⇧T * x * (q * q⇧T) | q . q ∈ ideal_points }"
      apply (rule mult_left_dist_sup_fin)
      using finite_ideal_points ne_ideal_points by simp_all
    thus ?thesis
      using mult_assoc by simp
  qed
  also have "... = Sup_fin { p * p⇧T * x * q * q⇧T | q p . q ∈ ideal_points ∧ p ∈ ideal_points }"
    apply (rule nested_sup_fin)
    using finite_ideal_points ne_ideal_points by simp_all
  also have "... = Sup_fin { p * p⇧T * x * q * q⇧T | p q . p ∈ ideal_points ∧ q ∈ ideal_points }"
    by meson
  also have "... = Sup_fin { p * p⇧T * x * q * q⇧T | p q . ideal_point p ∧ ideal_point q }"
    by auto
  finally show ?thesis
    .
qed

lemma atom_below_ideal_point:
  assumes "atom a"
    shows "∃p . ideal_point p ∧ a ≤ p"
proof -
  have "a = a ⊓ Sup_fin { p | p . p ∈ ideal_points }"
    using top_sup_ideal_points by auto
  also have "... = Sup_fin { a ⊓ p | p . p ∈ ideal_points }"
    apply (rule inf_left_dist_sup_fin)
    using finite_ideal_points apply blast
    using ne_ideal_points by blast
  finally have 1: "Sup_fin { a ⊓ p | p . p ∈ ideal_points } ≠ bot"
    using assms by auto
  have "∃p∈ideal_points . a ⊓ p ≠ bot"
  proof (rule ccontr)
    assume "¬ (∃p∈ideal_points . a ⊓ p ≠ bot)"
    hence "∀p∈ideal_points . a ⊓ p = bot"
      by auto
    hence "{ a ⊓ p | p . p ∈ ideal_points } = { bot | p . p ∈ ideal_points }"
      by auto
    hence "Sup_fin { a ⊓ p | p . p ∈ ideal_points } = Sup_fin { bot | p . p ∈ ideal_points }"
      by simp
    also have "... ≤ bot"
      apply (rule Sup_fin.boundedI)
      apply (simp add: finite_ideal_points)
      using ne_ideal_points apply simp
      by blast
    finally show "False"
      using 1 le_bot by blast
  qed
  from this obtain p where "p ∈ ideal_points ∧ a ⊓ p ≠ bot"
    by auto
  hence "ideal_point p ∧ a ≤ p"
    using assms inf.absorb_iff1 inf_le1 by blast
  thus ?thesis
    by auto
qed

lemma point_ideal_point_1:
  assumes "point a"
    shows "ideal_point a"
proof (cases "a = bot")
  case True
  thus ?thesis
    using assms by fastforce
next
  case False
  have "a = a ⊓ Sup_fin { p | p . p ∈ ideal_points }"
    using top_sup_ideal_points by auto
  also have "... = Sup_fin { a ⊓ p | p . p ∈ ideal_points }"
    apply (rule inf_left_dist_sup_fin)
    using finite_ideal_points apply blast
    using ne_ideal_points by blast
  finally have 1: "Sup_fin { a ⊓ p | p . p ∈ ideal_points } ≠ bot"
    using False by auto
  have "∃p∈ideal_points . a ⊓ p ≠ bot"
  proof (rule ccontr)
    assume "¬ (∃p∈ideal_points . a ⊓ p ≠ bot)"
    hence "∀p∈ideal_points . a ⊓ p = bot"
      by auto
    hence "{ a ⊓ p | p . p ∈ ideal_points } = { bot | p . p ∈ ideal_points }"
      by auto
    hence "Sup_fin { a ⊓ p | p . p ∈ ideal_points } = Sup_fin { bot | p . p ∈ ideal_points }"
      by simp
    also have "... ≤ bot"
      apply (rule Sup_fin.boundedI)
      apply (simp add: finite_ideal_points)
      using ne_ideal_points apply simp
      by blast
    finally show "False"
      using 1 le_bot by blast
  qed
  from this obtain p where 2: "p ∈ ideal_points ∧ a ⊓ p ≠ bot"
    by auto
  hence "a ≤ p ∨ a ≤ -p"
    using assms ideal_point_without_ideal by auto
  hence "a ≤ p"
    using 2 pseudo_complement by blast
  thus ?thesis
    using 2 assms point_below_equal by blast
qed

lemma point_ideal_point:
  "point x ⟷ ideal_point x"
  using point_ideal_point_1 by blast

end

subsection ‹Ideals, Ideal-Points and Matrices as Types›

text ‹
Stone relation algebras will be represented by matrices with ideal-points as entries and ideals as indices.
To define the type of such matrices, we first derive types for the set of ideals and ideal-points.
›

typedef (overloaded) 'a ideal = "ideals::'a::stone_relation_algebra_pa set"
  using surjective_top_closed by blast

setup_lifting type_definition_ideal

instantiation ideal :: (stone_relation_algebra_pa) stone_algebra
begin

lift_definition uminus_ideal :: "'a ideal ⇒ 'a ideal" is uminus
  using ideal_complement_closed by blast

lift_definition inf_ideal :: "'a ideal ⇒ 'a ideal ⇒ 'a ideal" is inf
  by (simp add: ideal_inf_closed)

lift_definition sup_ideal :: "'a ideal ⇒ 'a ideal ⇒ 'a ideal" is sup
  by (simp add: ideal_sup_closed)

lift_definition bot_ideal :: "'a ideal" is bot
  by (simp add: ideal_bot_closed)

lift_definition top_ideal :: "'a ideal" is top
  by simp

lift_definition less_eq_ideal :: "'a ideal ⇒ 'a ideal ⇒ bool" is less_eq .

lift_definition less_ideal :: "'a ideal ⇒ 'a ideal ⇒ bool" is less .

instance
  apply intro_classes
  subgoal apply transfer by (simp add: less_le_not_le)
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by (simp add: sup_inf_distrib1)
  subgoal apply transfer by (simp add: pseudo_complement)
  subgoal apply transfer by simp
  done

end

instantiation ideal :: (stone_relation_algebra_pa) stone_relation_algebra
begin

lift_definition conv_ideal :: "'a ideal ⇒ 'a ideal" is id
  by simp

lift_definition times_ideal :: "'a ideal ⇒ 'a ideal ⇒ 'a ideal" is inf
  by (simp add: ideal_inf_closed)

lift_definition one_ideal :: "'a ideal" is top
  by simp

instance
  apply intro_classes
  apply (metis comp_inf.comp_associative inf_ideal_def times_ideal_def)
  apply (metis inf_commute inf_ideal_def inf_sup_distrib1 times_ideal_def)
  apply (metis (mono_tags, lifting) comp_inf.mult_left_zero inf_ideal_def times_ideal_def)
  apply (metis (mono_tags, opaque_lifting) comp_inf.mult_1_left inf_ideal_def one_ideal.abs_eq times_ideal_def top_ideal.abs_eq)
  using Rep_ideal_inject conv_ideal.rep_eq apply fastforce
  apply (metis (mono_tags) Rep_ideal_inverse conv_ideal.rep_eq)
  apply (metis (mono_tags) Rep_ideal_inverse conv_ideal.rep_eq inf_commute inf_ideal_def times_ideal_def)
  apply (metis (mono_tags, opaque_lifting) Rep_ideal_inverse conv_ideal.rep_eq inf_ideal_def le_inf_iff order_refl times_ideal_def)
  apply (metis inf_ideal_def p_dist_inf p_dist_sup times_ideal_def)
  by (metis (mono_tags) one_ideal.abs_eq regular_closed_top top_ideal_def)

end

typedef (overloaded) 'a ideal_point = "ideal_points::'a::stone_relation_algebra_pa set"
  using ne_ideal_points by blast

instantiation ideal_point :: (stone_relation_algebra_pa) finite
begin

instance
proof
  have "Abs_ideal_point ` ideal_points = UNIV"
    using type_definition.Abs_image type_definition_ideal_point by blast
  thus "finite (UNIV::'a ideal_point set)"
    by (metis (mono_tags, lifting) finite_ideal_points finite_imageI)
qed

end

type_synonym 'a ideal_matrix = "('a ideal_point,'a ideal) square"

interpretation ideal_matrix_stone_relation_algebra: stone_relation_algebra where sup = sup_matrix and inf = inf_matrix and less_eq = less_eq_matrix and less = less_matrix and bot = "bot_matrix::'a::stone_relation_algebra_pa ideal_matrix" and top = top_matrix and uminus = uminus_matrix and one = one_matrix and times = times_matrix and conv = conv_matrix
  by (rule matrix_stone_relation_algebra.stone_relation_algebra_axioms)

lemma ideal_point_rep_2:
  assumes "x = Sup_fin { Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T | p q . True }"
    shows "f r s = Abs_ideal ((Rep_ideal_point r)⇧T * x * (Rep_ideal_point s))"
proof -
  let ?r = "Rep_ideal_point r"
  let ?s = "Rep_ideal_point s"
  have "?r⇧T * x * ?s = ?r⇧T * Sup_fin { Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T | p q . True } * ?s"
    using assms by simp
  also have "... = ?r⇧T * Sup_fin { Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T | p q . p ∈ UNIV ∧ q ∈ UNIV } * ?s"
    by simp
  also have "... = ?r⇧T * Sup_fin { Sup_fin { Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T | p . p ∈ UNIV } | q . q ∈ UNIV } * ?s"
  proof -
    have "Sup_fin { Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T | p q . p ∈ UNIV ∧ q ∈ UNIV } = Sup_fin { Sup_fin { Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T | p . p ∈ UNIV } | q . q ∈ UNIV }"
      by (rule nested_sup_fin[symmetric], simp_all)
    thus ?thesis
      by simp
  qed
  also have "... = Sup_fin { Sup_fin { ?r⇧T * Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T | p . p ∈ UNIV } | q . q ∈ UNIV } * ?s"
  proof -
    have 1: "?r⇧T * Sup_fin { Sup_fin { Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T | p . p ∈ UNIV } | q . q ∈ UNIV } = Sup_fin { ?r⇧T * Sup_fin { Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T | p . p ∈ UNIV } | q . q ∈ UNIV }"
      by (rule mult_left_dist_sup_fin, simp_all)
    have 2: "⋀q . ?r⇧T * Sup_fin { Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T | p . p ∈ UNIV } = Sup_fin { ?r⇧T * (Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T) | p . p ∈ UNIV }"
      by (rule mult_left_dist_sup_fin, simp_all)
    have "⋀p q . ?r⇧T * (Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T) = ?r⇧T * Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T"
      by (simp add: mult.assoc)
    thus ?thesis
      using 1 2 by simp
  qed
  also have "... = Sup_fin { Sup_fin { ?r⇧T * Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T * ?s | p . p ∈ UNIV } | q . q ∈ UNIV }"
  proof -
    have 3: "Sup_fin { Sup_fin { ?r⇧T * Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T | p . p ∈ UNIV } | q . q ∈ UNIV } * ?s = Sup_fin { Sup_fin { ?r⇧T * Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T | p . p ∈ UNIV } * ?s | q . q ∈ UNIV }"
      by (rule mult_right_dist_sup_fin, simp_all)
    have "⋀q . Sup_fin { ?r⇧T * Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T | p . p ∈ UNIV } * ?s = Sup_fin { ?r⇧T * Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T * ?s | p . p ∈ UNIV }"
      by (rule mult_right_dist_sup_fin, simp_all)
    thus ?thesis
      using 3 by simp
  qed
  also have "... = Sup_fin { Sup_fin { if p = r then ?r⇧T * Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T * ?s else bot | p . p ∈ UNIV } | q . q ∈ UNIV }"
  proof -
    have "⋀p . ?r⇧T * Rep_ideal_point p = (if p = r then ?r⇧T * Rep_ideal_point p else bot)"
    proof -
      fix p
      show "?r⇧T * Rep_ideal_point p = (if p = r then ?r⇧T * Rep_ideal_point p else bot)"
      proof (cases "p = r")
        case True
        thus ?thesis
          by auto
      next
        case False
        have "?r⇧T * Rep_ideal_point p = bot"
          apply (rule different_ideal_points_disjoint_2)
          using Rep_ideal_point apply blast
          using Rep_ideal_point apply blast
          using False by (simp add: Rep_ideal_point_inject)
        thus ?thesis
          using False by simp
      qed
    qed
    hence "⋀p q . ?r⇧T * Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T * ?s = (if p = r then ?r⇧T * Rep_ideal_point p * Rep_ideal (f p q) * (Rep_ideal_point q)⇧T * ?s else bot)"
      by (metis semiring.mult_zero_left)
    thus ?thesis
      by simp
  qed
  also have "... = Sup_fin { ?r⇧T * ?r * Rep_ideal (f r q) * (Rep_ideal_point q)⇧T * ?s | q . q ∈ UNIV }"
    by (subst one_point_sup_fin, simp_all)
  also have "... = Sup_fin { if q = s then ?r⇧T * ?r * Rep_ideal (f r q) * (Rep_ideal_point q)⇧T * ?s else bot | q . q ∈ UNIV }"
  proof -
    have "⋀q . (Rep_ideal_point q)⇧T * ?s = (if q = s then (Rep_ideal_point q)⇧T * ?s else bot)"
    proof -
      fix q
      show "(Rep_ideal_point q)⇧T * ?s = (if q = s then (Rep_ideal_point q)⇧T * ?s else bot)"
      proof (cases "q = s")
        case True
        thus ?thesis
          by auto
      next
        case False
        have "(Rep_ideal_point q)⇧T * ?s = bot"
          apply (rule different_ideal_points_disjoint_2)
          using Rep_ideal_point apply blast
          using Rep_ideal_point apply blast
          using False by (simp add: Rep_ideal_point_inject)
        thus ?thesis
          using False by simp
      qed
    qed
    hence "⋀q . ?r⇧T * ?r * Rep_ideal (f r q) * (Rep_ideal_point q)⇧T * ?s = (if q = s then ?r⇧T * ?r * Rep_ideal (f r q) * (Rep_ideal_point q)⇧T * ?s else bot)"
      by (metis comp_associative mult_right_zero)
    thus ?thesis
      by simp
  qed
  also have "... = ?r⇧T * ?r * Rep_ideal (f r s) * ?s⇧T * ?s"
    by (subst one_point_sup_fin, simp_all)
  also have "... = top * Rep_ideal (f r s) * top"
  proof -
    have "?r⇧T * ?r = top ∧ ?s⇧T * ?s = top"
      using point_mult_top Rep_ideal_point by blast
    thus ?thesis
      by (simp add: mult.assoc)
  qed
  also have "... = Rep_ideal (f r s)"
    by (metis (mono_tags, lifting) Rep_ideal mem_Collect_eq)
  finally show ?thesis
    by (simp add: Rep_ideal_inverse)
qed

subsection ‹Isomorphism›

text ‹
The following two functions comprise the isomorphism between Stone relation algebras and matrices.
We prove that they are inverses of each other and that the first one is a homomorphism.
›

definition sra_to_mat :: "'a::stone_relation_algebra_pa ⇒ 'a ideal_matrix"
  where "sra_to_mat x ≡ λ(p,q) . Abs_ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point q)"

definition mat_to_sra :: "'a::stone_relation_algebra_pa ideal_matrix ⇒ 'a"
  where "mat_to_sra f ≡ Sup_fin { Rep_ideal_point p * Rep_ideal (f (p,q)) * (Rep_ideal_point q)⇧T | p q . True }"

lemma sra_mat_sra:
  "mat_to_sra (sra_to_mat x) = x"
proof -
  have "mat_to_sra (sra_to_mat x) = Sup_fin { Rep_ideal_point p * Rep_ideal (Abs_ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point q)) * (Rep_ideal_point q)⇧T | p q . True }"
    by (unfold sra_to_mat_def mat_to_sra_def, simp)
  also have "... = Sup_fin { Rep_ideal_point p * (Rep_ideal_point p)⇧T * x * Rep_ideal_point q * (Rep_ideal_point q)⇧T | p q . True }"
  proof -
    have "⋀p q . ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point q)"
      using Rep_ideal_point covector_mult_vector_ideal by force
    hence "⋀p q . Rep_ideal (Abs_ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point q)) = (Rep_ideal_point p)⇧T * x * Rep_ideal_point q"
      using Abs_ideal_inverse by blast
    thus ?thesis
      by (simp add: mult.assoc)
  qed
  also have "... = Sup_fin { p * p⇧T * x * q * q⇧T | p q . ideal_point p ∧ ideal_point q }"
  proof -
    have "{ Rep_ideal_point p * (Rep_ideal_point p)⇧T * x * Rep_ideal_point q * (Rep_ideal_point q)⇧T | p q . True } = { p * p⇧T * x * q * q⇧T | p q . ideal_point p ∧ ideal_point q }"
    proof (rule set_eqI)
      fix z
      show "z ∈ { Rep_ideal_point p * (Rep_ideal_point p)⇧T * x * Rep_ideal_point q * (Rep_ideal_point q)⇧T | p q . True } ⟷ z ∈ { p * p⇧T * x * q * q⇧T | p q . ideal_point p ∧ ideal_point q }"
      proof
        assume "z ∈ { Rep_ideal_point p * (Rep_ideal_point p)⇧T * x * Rep_ideal_point q * (Rep_ideal_point q)⇧T | p q . True }"
        from this obtain p q where "z = Rep_ideal_point p * (Rep_ideal_point p)⇧T * x * Rep_ideal_point q * (Rep_ideal_point q)⇧T"
          by auto
        thus "z ∈ { p * p⇧T * x * q * q⇧T | p q . ideal_point p ∧ ideal_point q }"
          using Rep_ideal_point by blast
      next
        assume "z ∈ { p * p⇧T * x * q * q⇧T | p q . ideal_point p ∧ ideal_point q }"
        from this obtain p q where 1: "ideal_point p ∧ ideal_point q ∧ z = p * p⇧T * x * q * q⇧T"
          by auto
        hence "Rep_ideal_point (Abs_ideal_point p) = p ∧ Rep_ideal_point (Abs_ideal_point q) = q"
          using Abs_ideal_point_inverse by auto
        thus "z ∈ { Rep_ideal_point p * (Rep_ideal_point p)⇧T * x * Rep_ideal_point q * (Rep_ideal_point q)⇧T | p q . True }"
          using 1 by (metis (mono_tags, lifting) mem_Collect_eq)
      qed
    qed
    thus ?thesis
      by simp
  qed
  also have "... = x"
    by (rule ideal_point_rep_1[symmetric])
  finally show ?thesis
    .
qed

lemma mat_sra_mat:
  "sra_to_mat (mat_to_sra f) = f"
  by (unfold sra_to_mat_def mat_to_sra_def, simp add: ideal_point_rep_2[symmetric])

lemma sra_to_mat_sup_homomorphism:
  "sra_to_mat (x ⊔ y) = sra_to_mat x ⊔ sra_to_mat y"
proof (rule ext,unfold split_paired_all)
  fix p q
  have "sra_to_mat (x ⊔ y) (p,q) = Abs_ideal ((Rep_ideal_point p)⇧T * (x ⊔ y) * Rep_ideal_point q)"
    by (unfold sra_to_mat_def, simp)
  also have "... = Abs_ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point q ⊔ (Rep_ideal_point p)⇧T * y * Rep_ideal_point q)"
    by (simp add: comp_right_dist_sup idempotent_left_zero_semiring_class.semiring.distrib_left)
  also have "... = Abs_ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point q) ⊔ Abs_ideal ((Rep_ideal_point p)⇧T * y * Rep_ideal_point q)"
  proof (rule sup_ideal.abs_eq[symmetric])
    have 1: "⋀x . ideal_point (Rep_ideal_point x::'a)"
      using Rep_ideal_point by blast
    hence 2: "covector ((Rep_ideal_point p)⇧T)"
      using vector_conv_covector by blast
    thus "eq_onp ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point q) ((Rep_ideal_point p)⇧T * x * Rep_ideal_point q)"
      using 1 by (simp add: comp_associative covector_mult_closed eq_onp_same_args)
    show "eq_onp ideal ((Rep_ideal_point p)⇧T * y * Rep_ideal_point q) ((Rep_ideal_point p)⇧T * y * Rep_ideal_point q)"
      using 1 2 by (simp add: comp_associative covector_mult_closed eq_onp_same_args)
  qed
  also have "... = sra_to_mat x (p,q) ⊔ sra_to_mat y (p,q)"
    by (unfold sra_to_mat_def, simp)
  finally show "sra_to_mat (x ⊔ y) (p,q) = (sra_to_mat x ⊔ sra_to_mat y) (p,q)"
    by simp
qed

lemma sra_to_mat_inf_homomorphism:
  "sra_to_mat (x ⊓ y) = sra_to_mat x ⊓ sra_to_mat y"
proof (rule ext,unfold split_paired_all)
  fix p q
  have "sra_to_mat (x ⊓ y) (p,q) = Abs_ideal ((Rep_ideal_point p)⇧T * (x ⊓ y) * Rep_ideal_point q)"
    by (unfold sra_to_mat_def, simp)
  also have "... = Abs_ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point q ⊓ (Rep_ideal_point p)⇧T * y * Rep_ideal_point q)"
    by (metis (no_types, lifting) Rep_ideal_point conv_involutive injective_comp_right_dist_inf mem_Collect_eq univalent_comp_left_dist_inf)
  also have "... = Abs_ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point q) ⊓ Abs_ideal ((Rep_ideal_point p)⇧T * y * Rep_ideal_point q)"
  proof (rule inf_ideal.abs_eq[symmetric])
    have 1: "⋀x . ideal_point (Rep_ideal_point x::'a)"
      using Rep_ideal_point by blast
    hence 2: "covector ((Rep_ideal_point p)⇧T)"
      using vector_conv_covector by blast
    thus "eq_onp ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point q) ((Rep_ideal_point p)⇧T * x * Rep_ideal_point q)"
      using 1 by (simp add: comp_associative covector_mult_closed eq_onp_same_args)
    show "eq_onp ideal ((Rep_ideal_point p)⇧T * y * Rep_ideal_point q) ((Rep_ideal_point p)⇧T * y * Rep_ideal_point q)"
      using 1 2 by (simp add: comp_associative covector_mult_closed eq_onp_same_args)
  qed
  also have "... = sra_to_mat x (p,q) ⊓ sra_to_mat y (p,q)"
    by (unfold sra_to_mat_def, simp)
  finally show "sra_to_mat (x ⊓ y) (p,q) = (sra_to_mat x ⊓ sra_to_mat y) (p,q)"
    by simp
qed

lemma sra_to_mat_conv_homomorphism:
  "sra_to_mat (x⇧T) = (sra_to_mat x)⇧t"
proof (rule ext,unfold split_paired_all)
  fix p q
  have "sra_to_mat (x⇧T) (p,q) = Abs_ideal ((Rep_ideal_point p)⇧T * (x⇧T) * Rep_ideal_point q)"
    by (unfold sra_to_mat_def, simp)
  also have "... = Abs_ideal (((Rep_ideal_point q)⇧T * x * Rep_ideal_point p)⇧T)"
    by (simp add: conv_dist_comp mult.assoc)
  also have "... = Abs_ideal ((Rep_ideal_point q)⇧T * x * Rep_ideal_point p)"
  proof -
    have "ideal_point (Rep_ideal_point p) ∧ ideal_point (Rep_ideal_point q)"
      using Rep_ideal_point by blast
    thus ?thesis
      by (metis (full_types) covector_mult_vector_ideal ideal_conv_id)
  qed
  also have "... = (Abs_ideal ((Rep_ideal_point q)⇧T * x * Rep_ideal_point p))⇧T"
    by (metis Rep_ideal_inject conv_ideal.rep_eq)
  also have "... = (sra_to_mat x (q,p))⇧T"
    by (unfold sra_to_mat_def, simp)
  finally show "sra_to_mat (x⇧T) (p,q) = ((sra_to_mat x)⇧t) (p,q)"
    by (simp add: conv_matrix_def)
qed

lemma sra_to_mat_complement_homomorphism:
  "sra_to_mat (-x) = -(sra_to_mat x)"
proof (rule ext,unfold split_paired_all)
  fix p q
  have "sra_to_mat (-x) (p,q) = Abs_ideal ((Rep_ideal_point p)⇧T * -x * Rep_ideal_point q)"
    by (unfold sra_to_mat_def, simp)
  also have "... = Abs_ideal (-((Rep_ideal_point p)⇧T * x * Rep_ideal_point q))"
  proof -
    have 1: "(Rep_ideal_point p)⇧T * -x = -((Rep_ideal_point p)⇧T * x)"
      using Rep_ideal_point comp_mapping_complement surjective_conv_total by force
    have "-((Rep_ideal_point p)⇧T * x) * Rep_ideal_point q = -((Rep_ideal_point p)⇧T * x * Rep_ideal_point q)"
      using Rep_ideal_point comp_bijective_complement by blast
    thus ?thesis
      using 1 by simp
  qed
  also have "... = -Abs_ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point q)"
  proof (rule uminus_ideal.abs_eq[symmetric])
    have 1: "⋀x . ideal_point (Rep_ideal_point x::'a)"
      using Rep_ideal_point by blast
    hence "covector ((Rep_ideal_point p)⇧T)"
      using vector_conv_covector by blast
    thus "eq_onp ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point q) ((Rep_ideal_point p)⇧T * x * Rep_ideal_point q)"
      using 1 by (simp add: comp_associative covector_mult_closed eq_onp_same_args)
  qed
  also have "... = -sra_to_mat x (p,q)"
    by (unfold sra_to_mat_def, simp)
  finally show "sra_to_mat (-x) (p,q) = (-sra_to_mat x) (p,q)"
    by simp
qed

lemma sra_to_mat_bot_homomorphism:
  "sra_to_mat bot = bot"
proof (rule ext,unfold split_paired_all)
  fix p q :: "'a ideal_point"
  have "sra_to_mat bot (p,q) = Abs_ideal ((Rep_ideal_point p)⇧T * bot * Rep_ideal_point q)"
    by (unfold sra_to_mat_def, simp)
  also have "... = bot"
    by (simp add: bot_ideal.abs_eq)
  finally show "sra_to_mat bot (p,q) = bot (p,q)"
    by simp
qed

lemma sra_to_mat_top_homomorphism:
  "sra_to_mat top = top"
proof (rule ext,unfold split_paired_all)
  fix p q :: "'a ideal_point"
  have "sra_to_mat top (p,q) = Abs_ideal ((Rep_ideal_point p)⇧T * top * Rep_ideal_point q)"
    by (unfold sra_to_mat_def, simp)
  also have "... = top"
  proof -
    have "⋀x . ideal_point (Rep_ideal_point x::'a)"
      using Rep_ideal_point by blast
    thus ?thesis
      by (metis (full_types) conv_dist_comp symmetric_top_closed top_ideal.abs_eq)
  qed
  finally show "sra_to_mat top (p,q) = top (p,q)"
    by simp
qed

lemma sra_to_mat_one_homomorphism:
  "sra_to_mat 1 = one_matrix"
proof (rule ext,unfold split_paired_all)
  fix p q :: "'a ideal_point"
  have "sra_to_mat 1 (p,q) = Abs_ideal ((Rep_ideal_point p)⇧T * Rep_ideal_point q)"
    by (unfold sra_to_mat_def, simp)
  also have "... = one_matrix (p,q)"
  proof (cases "p = q")
    case True
    hence "(Rep_ideal_point p)⇧T * Rep_ideal_point q = top"
      using Rep_ideal_point point_mult_top by auto
    hence "Abs_ideal ((Rep_ideal_point p)⇧T * Rep_ideal_point q) = Abs_ideal top"
      by simp
    also have "... = one_matrix (p,q)"
      by (unfold one_matrix_def, simp add: True one_ideal_def)
    finally show ?thesis
      .
  next
    case False
    have "(Rep_ideal_point p)⇧T * Rep_ideal_point q = bot"
      apply (rule different_ideal_points_disjoint_2)
      using Rep_ideal_point apply blast
      using Rep_ideal_point apply blast
      by (simp add: False Rep_ideal_point_inject)
    also have "... = one_matrix (p,q)"
      by (unfold one_matrix_def, simp add: False)
    finally show ?thesis
      by (simp add: False bot_ideal_def one_matrix_def)
  qed
  finally show "sra_to_mat 1 (p,q) = one_matrix (p,q)"
    by simp
qed

lemma Abs_ideal_dist_sup_fin:
  assumes "finite X"
      and "X ≠ {}"
      and "∀x∈X . ideal (f x)"
    shows "Abs_ideal (Sup_fin { f x | x . x ∈ X }) = Sup_fin { Abs_ideal (f x) | x . x ∈ X }"
proof (rule finite_ne_subset_induct'[where F="X"])
  show "finite X"
    using assms(1) by simp
  show "X ≠ {}"
    using assms(2) by simp
  show "X ⊆ X"
    by simp
  fix y
  assume 1: "y ∈ X"
  thus "Abs_ideal (Sup_fin { f x | x . x ∈ {y} }) = Sup_fin { Abs_ideal (f x) | x . x ∈ {y} }"
    by auto
  fix F
  assume 2: "finite F" "F ≠ {}" "F ⊆ X" "y ∉ F" "Abs_ideal (Sup_fin { f x | x . x ∈ F }) = Sup_fin { Abs_ideal (f x) | x . x ∈ F }"
  have "Abs_ideal (Sup_fin { f x | x . x ∈ insert y F }) = Abs_ideal (f y ⊔ Sup_fin { f x | x . x ∈ F })"
  proof -
    have "Sup_fin { f x | x . x ∈ insert y F } = f y ⊔ Sup_fin { f x | x . x ∈ F }"
      apply (subst Sup_fin.insert[symmetric])
      using 2 apply simp
      using 2 apply simp
      by (auto intro: arg_cong[where f="Sup_fin"])
    thus ?thesis
      by simp
  qed
  also have "... = Abs_ideal (f y) ⊔ Abs_ideal (Sup_fin { f x | x . x ∈ F })"
  proof (rule sup_ideal.abs_eq[symmetric])
    show "eq_onp ideal (f y) (f y)"
      using 1 by (simp add: assms(3) eq_onp_same_args)
    have "top * Sup_fin { f x | x . x ∈ F } = Sup_fin { top * f x | x . x ∈ F }"
      using 2 mult_left_dist_sup_fin by fastforce
    hence "top * Sup_fin { f x | x . x ∈ F } * top = Sup_fin { top * f x | x . x ∈ F } * top"
      by simp
    also have "... = Sup_fin { top * f x * top | x . x ∈ F }"
      using 2 mult_right_dist_sup_fin by force
    also have "... = Sup_fin { f x | x . x ∈ F }"
      using 2 by (metis assms(3) subset_iff)
    finally have "top * Sup_fin { f x | x . x ∈ F } * top = Sup_fin { f x | x . x ∈ F }"
      .
    hence "ideal (Sup_fin { f x | x . x ∈ F })"
      using ideal_fixpoint by blast
    thus "eq_onp ideal (Sup_fin { f x | x . x ∈ F }) (Sup_fin { f x | x . x ∈ F })"
      by (simp add: eq_onp_def)
  qed
  also have "... = Abs_ideal (f y) ⊔ Sup_fin { Abs_ideal (f x) | x . x ∈ F }"
    using 2 by simp
  also have "... = Sup_fin { Abs_ideal (f x) | x . x ∈ insert y F }"
    apply (subst Sup_fin.insert[symmetric])
    using 2 apply simp
    using 2 apply simp
    by (auto intro: arg_cong[where f="Sup_fin"])
  finally show "Abs_ideal (Sup_fin { f x | x . x ∈ insert y F }) = Sup_fin { Abs_ideal (f x) | x . x ∈ insert y F }"
    .
qed

lemma sra_to_mat_mult_homomorphism:
  "sra_to_mat (x * y) = sra_to_mat x ⊙ sra_to_mat y"
proof (rule ext,unfold split_paired_all)
  fix p q
  have "sra_to_mat (x * y) (p,q) = Abs_ideal ((Rep_ideal_point p)⇧T * (x * y) * Rep_ideal_point q)"
    by (unfold sra_to_mat_def, simp)
  also have "... = Abs_ideal ((Rep_ideal_point p)⇧T * x * 1 * y * Rep_ideal_point q)"
    by (simp add: mult.assoc)
  also have "... = Abs_ideal ((Rep_ideal_point p)⇧T * x * Sup_fin { r * r⇧T | r . ideal_point r } * y * Rep_ideal_point q)"
    by (unfold one_sup_ideal_points[symmetric], simp)
  also have "... = Abs_ideal ((Rep_ideal_point p)⇧T * x * Sup_fin { Rep_ideal_point r * (Rep_ideal_point r)⇧T | r . r ∈ UNIV } * y * Rep_ideal_point q)"
  proof -
    have "{ r * r⇧T | r::'a . ideal_point r } = { Rep_ideal_point r * (Rep_ideal_point r)⇧T | r . r ∈ UNIV }"
    proof (rule set_eqI)
      fix x
      show "x ∈ { r * r⇧T | r::'a . ideal_point r } ⟷ x ∈ { Rep_ideal_point r * (Rep_ideal_point r)⇧T | r . r ∈ UNIV }"
      proof
        assume "x ∈ { r * r⇧T | r::'a . ideal_point r }"
        from this obtain r where 1: "ideal_point r ∧ x = r * r⇧T"
          by auto
        hence "Rep_ideal_point (Abs_ideal_point r) = r"
          using Abs_ideal_point_inverse by auto
        thus "x ∈ { Rep_ideal_point r * (Rep_ideal_point r)⇧T | r . r ∈ UNIV }"
          using 1 by (metis (mono_tags, lifting) UNIV_I mem_Collect_eq)
      next
        assume "x ∈ { Rep_ideal_point r * (Rep_ideal_point r)⇧T | r . r ∈ UNIV }"
        from this obtain r where "x = Rep_ideal_point r * (Rep_ideal_point r)⇧T"
          by auto
        thus "x ∈ { r * r⇧T | r::'a . ideal_point r }"
          using Rep_ideal_point by blast
      qed
    qed
    thus ?thesis
      by simp
  qed
  also have "... = Abs_ideal (Sup_fin { (Rep_ideal_point p)⇧T * x * Rep_ideal_point r * (Rep_ideal_point r)⇧T | r . r ∈ UNIV } * (y * Rep_ideal_point q))"
    by (subst mult_left_dist_sup_fin, simp_all add: mult.assoc)
  also have "... = Abs_ideal (Sup_fin { (Rep_ideal_point p)⇧T * x * Rep_ideal_point r * (Rep_ideal_point r)⇧T * y * Rep_ideal_point q | r . r ∈ UNIV })"
    by (subst mult_right_dist_sup_fin, simp_all add: mult.assoc)
  also have "... = Sup_fin { Abs_ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point r * (Rep_ideal_point r)⇧T * y * Rep_ideal_point q) | r . r ∈ UNIV }"
  proof -
    have 1: "⋀r . ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point r * (Rep_ideal_point r)⇧T * y * Rep_ideal_point q)"
    proof -
      fix r :: "'a ideal_point"
      have "⋀x . ideal_point (Rep_ideal_point x::'a)"
        using Rep_ideal_point by blast
      thus "ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point r * (Rep_ideal_point r)⇧T * y * Rep_ideal_point q)"
        by (simp add: covector_mult_closed vector_conv_covector vector_mult_closed)
    qed
    show ?thesis
      apply (rule Abs_ideal_dist_sup_fin)
      using 1 by simp_all
  qed
  also have "... = (⨆⇩r Abs_ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point r * (Rep_ideal_point r)⇧T * y * Rep_ideal_point q))"
    by (rule sup_fin_sum)
  also have "... = (⨆⇩r Abs_ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point r ⊓ (Rep_ideal_point r)⇧T * y * Rep_ideal_point q))"
  proof -
    have "⋀r . (Rep_ideal_point p)⇧T * x * Rep_ideal_point r * ((Rep_ideal_point r)⇧T * y * Rep_ideal_point q) = (Rep_ideal_point p)⇧T * x * Rep_ideal_point r ⊓ (Rep_ideal_point r)⇧T * y * Rep_ideal_point q"
    proof (rule ideal_mult_inf)
      fix r :: "'a ideal_point"
      have 2: "⋀x . ideal_point (Rep_ideal_point x::'a)"
        using Rep_ideal_point by blast
      thus "ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point r)"
        by (simp add: covector_mult_closed vector_conv_covector vector_mult_closed)
      show "ideal ((Rep_ideal_point r)⇧T * y * Rep_ideal_point q)"
        using 2 by (simp add: covector_mult_closed vector_conv_covector vector_mult_closed)
    qed
    thus ?thesis
      by (simp add: mult.assoc)
  qed
  also have "... = (⨆⇩r Abs_ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point r) * Abs_ideal ((Rep_ideal_point r)⇧T * y * Rep_ideal_point q))"
  proof -
    have "⋀r . Abs_ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point r ⊓ (Rep_ideal_point r)⇧T * y * Rep_ideal_point q) = Abs_ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point r) * Abs_ideal ((Rep_ideal_point r)⇧T * y * Rep_ideal_point q)"
    proof (rule times_ideal.abs_eq[symmetric])
      fix r :: "'a ideal_point"
      have 3: "⋀x . ideal_point (Rep_ideal_point x::'a)"
        using Rep_ideal_point by blast
      hence 4: "covector ((Rep_ideal_point p)⇧T) ∧ covector ((Rep_ideal_point r)⇧T)"
        using vector_conv_covector by blast
      thus "eq_onp ideal ((Rep_ideal_point p)⇧T * x * Rep_ideal_point r) ((Rep_ideal_point p)⇧T * x * Rep_ideal_point r)"
        using 3 by (simp add: comp_associative covector_mult_closed eq_onp_same_args)
      show "eq_onp ideal ((Rep_ideal_point r)⇧T * y * Rep_ideal_point q) ((Rep_ideal_point r)⇧T * y * Rep_ideal_point q)"
        using 3 4 by (simp add: comp_associative covector_mult_closed eq_onp_same_args)
    qed
    thus ?thesis
      by simp
  qed
  also have "... = (⨆⇩r sra_to_mat x (p,r) * sra_to_mat y (r,q))"
    by (unfold sra_to_mat_def, simp)
  finally show "sra_to_mat (x * y) (p,q) = (sra_to_mat x ⊙ sra_to_mat y) (p,q)"
    by (simp add: times_matrix_def)
qed

end