[STATEMENT]
lemma regular_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_p_algebra.regular f \<longleftrightarrow> (\<forall>e . f e = bot \<or> f e = top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_p_algebra.regular f = (\<forall>e. f e = bot \<or> f e = top)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_p_algebra.regular f = (\<forall>e. f e = bot \<or> f e = top)
[PROOF STEP]
have "matrix_p_algebra.regular f \<longleftrightarrow> (\<ominus>\<ominus>f = f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_p_algebra.regular f = (\<ominus> \<ominus> f = f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_p_algebra.regular f = (\<ominus> \<ominus> f = f)

goal (1 subgoal):
 1. matrix_p_algebra.regular f = (\<forall>e. f e = bot \<or> f e = top)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
matrix_p_algebra.regular f = (\<ominus> \<ominus> f = f)

goal (1 subgoal):
 1. matrix_p_algebra.regular f = (\<forall>e. f e = bot \<or> f e = top)
[PROOF STEP]
have "... \<longleftrightarrow> (\<forall>e . --f e = f e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<ominus> \<ominus> f = f) = (\<forall>e. - - f e = f e)
[PROOF STEP]
by (metis uminus_matrix_def ext)
[PROOF STATE]
proof (state)
this:
(\<ominus> \<ominus> f = f) = (\<forall>e. - - f e = f e)

goal (1 subgoal):
 1. matrix_p_algebra.regular f = (\<forall>e. f e = bot \<or> f e = top)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<ominus> \<ominus> f = f) = (\<forall>e. - - f e = f e)

goal (1 subgoal):
 1. matrix_p_algebra.regular f = (\<forall>e. f e = bot \<or> f e = top)
[PROOF STEP]
have "... \<longleftrightarrow> (\<forall>e . f e = bot \<or> f e = top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>e. - - f e = f e) = (\<forall>e. f e = bot \<or> f e = top)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<forall>e. - - f e = f e) = (\<forall>e. f e = bot \<or> f e = top)

goal (1 subgoal):
 1. matrix_p_algebra.regular f = (\<forall>e. f e = bot \<or> f e = top)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
matrix_p_algebra.regular f = (\<forall>e. f e = bot \<or> f e = top)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
matrix_p_algebra.regular f = (\<forall>e. f e = bot \<or> f e = top)

goal (1 subgoal):
 1. matrix_p_algebra.regular f = (\<forall>e. f e = bot \<or> f e = top)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
matrix_p_algebra.regular f = (\<forall>e. f e = bot \<or> f e = top)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vector_linorder_matrix_0:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_bounded_idempotent_semiring.vector f"
    shows "f (i,j) = (\<Squnion>\<^sub>k f (i,k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (i, j) = sup_monoid.sum (\<lambda>k. f (i, k)) {k. True}
[PROOF STEP]
by (metis assms comp_top_linorder_matrix)


[STATEMENT]
lemma vector_linorder_matrix_1:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_bounded_idempotent_semiring.vector f"
    shows "f (i,j) = f (i,k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (i, j) = f (i, k)
[PROOF STEP]
by (metis assms vector_linorder_matrix_0)


[STATEMENT]
lemma vector_linorder_matrix_2:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "\<forall>i j k . f (i,j) = f (i,k)"
    shows "matrix_bounded_idempotent_semiring.vector f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_bounded_idempotent_semiring.vector f
[PROOF STEP]
proof (rule ext, rule prod_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. (f \<odot> mtop) (a, b) = f (a, b)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. (f \<odot> mtop) (a, b) = f (a, b)
[PROOF STEP]
have "(f \<odot> mtop) (i,j) = (\<Squnion>\<^sub>k f (i,k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<odot> mtop) (i, j) = sup_monoid.sum (\<lambda>k. f (i, k)) {k. True}
[PROOF STEP]
by (simp add: comp_top_linorder_matrix)
[PROOF STATE]
proof (state)
this:
(f \<odot> mtop) (i, j) = sup_monoid.sum (\<lambda>k. f (i, k)) {k. True}

goal (1 subgoal):
 1. \<And>x a b. (f \<odot> mtop) (a, b) = f (a, b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f \<odot> mtop) (i, j) = sup_monoid.sum (\<lambda>k. f (i, k)) {k. True}

goal (1 subgoal):
 1. \<And>x a b. (f \<odot> mtop) (a, b) = f (a, b)
[PROOF STEP]
have "... = f (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} = f (i, j)
[PROOF STEP]
by (metis assms linorder_finite_sup_selective)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} = f (i, j)

goal (1 subgoal):
 1. \<And>x a b. (f \<odot> mtop) (a, b) = f (a, b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(f \<odot> mtop) (i, j) = f (i, j)
[PROOF STEP]
show "(f \<odot> mtop) (i,j) = f (i,j)"
[PROOF STATE]
proof (prove)
using this:
(f \<odot> mtop) (i, j) = f (i, j)

goal (1 subgoal):
 1. (f \<odot> mtop) (i, j) = f (i, j)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(f \<odot> mtop) (i, j) = f (i, j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vector_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_bounded_idempotent_semiring.vector f \<longleftrightarrow> (\<forall>i j k . f (i,j) = f (i,k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_bounded_idempotent_semiring.vector f = (\<forall>i j k. f (i, j) = f (i, k))
[PROOF STEP]
using vector_linorder_matrix_1 vector_linorder_matrix_2
[PROOF STATE]
proof (prove)
using this:
matrix_bounded_idempotent_semiring.vector ?f \<Longrightarrow> ?f (?i, ?j) = ?f (?i, ?k)
\<forall>i j k. ?f (i, j) = ?f (i, k) \<Longrightarrow> matrix_bounded_idempotent_semiring.vector ?f

goal (1 subgoal):
 1. matrix_bounded_idempotent_semiring.vector f = (\<forall>i j k. f (i, j) = f (i, k))
[PROOF STEP]
by auto


[STATEMENT]
lemma covector_linorder_matrix_0:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_bounded_idempotent_semiring.covector f"
    shows "f (i,j) = (\<Squnion>\<^sub>k f (k,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (i, j) = sup_monoid.sum (\<lambda>k. f (k, j)) {k. True}
[PROOF STEP]
by (metis assms top_comp_linorder_matrix)


[STATEMENT]
lemma covector_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_bounded_idempotent_semiring.covector f \<longleftrightarrow> (\<forall>i j k . f (i,j) = f (k,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_bounded_idempotent_semiring.covector f = (\<forall>i j k. f (i, j) = f (k, j))
[PROOF STEP]
by (unfold matrix_stone_relation_algebra.covector_conv_vector vector_linorder_matrix) (metis (no_types, lifting) case_prod_conv conv_matrix_def conv_def)


[STATEMENT]
lemma point_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.point f \<longleftrightarrow> (\<exists>i . \<forall>j . f (i,j) = top \<and> (\<forall>k . i \<noteq> k \<longrightarrow> f (k,j) = bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.point f = (\<exists>i. \<forall>j. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
apply (unfold vector_linorder_matrix bijective_linorder_matrix)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>i j k. f (i, j) = f (i, k)) \<and> (\<forall>j. \<exists>i. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))) = (\<exists>i. \<forall>j. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>i j k. f (i, j) = f (i, k)) \<and> (\<forall>j. \<exists>i. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot)) \<Longrightarrow> \<exists>i. \<forall>j. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot)
 2. \<exists>i. \<forall>j. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot) \<Longrightarrow> (\<forall>i j k. f (i, j) = f (i, k)) \<and> (\<forall>j. \<exists>i. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. \<forall>j. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot) \<Longrightarrow> (\<forall>i j k. f (i, j) = f (i, k)) \<and> (\<forall>j. \<exists>i. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
by metis


[STATEMENT]
lemma point_linorder_matrix_unique:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.point f \<longleftrightarrow> (\<exists>!i . \<forall>j . f (i,j) = top \<and> (\<forall>k . i \<noteq> k \<longrightarrow> f (k,j) = bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.point f = (\<exists>!i. \<forall>j. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
apply (unfold vector_linorder_matrix bijective_linorder_matrix)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>i j k. f (i, j) = f (i, k)) \<and> (\<forall>j. \<exists>i. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))) = (\<exists>!i. \<forall>j. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>i j k. f (i, j) = f (i, k)) \<and> (\<forall>j. \<exists>i. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot)) \<Longrightarrow> \<exists>!i. \<forall>j. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot)
 2. \<exists>!i. \<forall>j. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot) \<Longrightarrow> (\<forall>i j k. f (i, j) = f (i, k)) \<and> (\<forall>j. \<exists>i. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
apply (metis bot_not_top)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!i. \<forall>j. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot) \<Longrightarrow> (\<forall>i j k. f (i, j) = f (i, k)) \<and> (\<forall>j. \<exists>i. f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
by metis


[STATEMENT]
lemma pp_point_linorder_matrix:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.pp_point f \<longleftrightarrow> (\<exists>i . \<forall>j . f (i,j) \<noteq> bot \<and> (\<forall>k . f (i,j) = f (i,k)) \<and> (\<forall>k . i \<noteq> k \<longrightarrow> f (k,j) = bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.pp_point f = (\<exists>i. \<forall>j. f (i, j) \<noteq> bot \<and> (\<forall>k. f (i, j) = f (i, k)) \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
apply (unfold vector_linorder_matrix pp_bijective_linorder_matrix)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>i j k. f (i, j) = f (i, k)) \<and> (\<forall>j. \<exists>i. f (i, j) \<noteq> bot \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))) = (\<exists>i. \<forall>j. f (i, j) \<noteq> bot \<and> (\<forall>k. f (i, j) = f (i, k)) \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>i j k. f (i, j) = f (i, k)) \<and> (\<forall>j. \<exists>i. f (i, j) \<noteq> bot \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot)) \<Longrightarrow> \<exists>i. \<forall>j. f (i, j) \<noteq> bot \<and> (\<forall>k. f (i, j) = f (i, k)) \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot)
 2. \<exists>i. \<forall>j. f (i, j) \<noteq> bot \<and> (\<forall>k. f (i, j) = f (i, k)) \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot) \<Longrightarrow> (\<forall>i j k. f (i, j) = f (i, k)) \<and> (\<forall>j. \<exists>i. f (i, j) \<noteq> bot \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. \<forall>j. f (i, j) \<noteq> bot \<and> (\<forall>k. f (i, j) = f (i, k)) \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot) \<Longrightarrow> (\<forall>i j k. f (i, j) = f (i, k)) \<and> (\<forall>j. \<exists>i. f (i, j) \<noteq> bot \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
by metis


[STATEMENT]
lemma pp_point_linorder_matrix_unique:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.pp_point f \<longleftrightarrow> (\<exists>!i . \<forall>j . f (i,j) \<noteq> bot \<and> (\<forall>k . f (i,j) = f (i,k)) \<and> (\<forall>k . i \<noteq> k \<longrightarrow> f (k,j) = bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.pp_point f = (\<exists>!i. \<forall>j. f (i, j) \<noteq> bot \<and> (\<forall>k. f (i, j) = f (i, k)) \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
apply (unfold vector_linorder_matrix pp_bijective_linorder_matrix)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>i j k. f (i, j) = f (i, k)) \<and> (\<forall>j. \<exists>i. f (i, j) \<noteq> bot \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))) = (\<exists>!i. \<forall>j. f (i, j) \<noteq> bot \<and> (\<forall>k. f (i, j) = f (i, k)) \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<forall>i j k. f (i, j) = f (i, k)) \<and> (\<forall>j. \<exists>i. f (i, j) \<noteq> bot \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot)) \<Longrightarrow> \<exists>!i. \<forall>j. f (i, j) \<noteq> bot \<and> (\<forall>k. f (i, j) = f (i, k)) \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot)
 2. \<exists>!i. \<forall>j. f (i, j) \<noteq> bot \<and> (\<forall>k. f (i, j) = f (i, k)) \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot) \<Longrightarrow> (\<forall>i j k. f (i, j) = f (i, k)) \<and> (\<forall>j. \<exists>i. f (i, j) \<noteq> bot \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!i. \<forall>j. f (i, j) \<noteq> bot \<and> (\<forall>k. f (i, j) = f (i, k)) \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot) \<Longrightarrow> (\<forall>i j k. f (i, j) = f (i, k)) \<and> (\<forall>j. \<exists>i. f (i, j) \<noteq> bot \<and> (\<forall>k. i \<noteq> k \<longrightarrow> f (k, j) = bot))
[PROOF STEP]
by metis


[STATEMENT]
lemma arc_linorder_matrix_1:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_stone_relation_algebra.arc f"
    shows "\<exists>e . f e = top \<and> (\<forall>d . e \<noteq> d \<longrightarrow> f d = bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
have "matrix_stone_relation_algebra.point (f \<odot> mtop)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.point (f \<odot> mtop)
[PROOF STEP]
by (simp add: assms matrix_bounded_idempotent_semiring.vector_mult_closed)
[PROOF STATE]
proof (state)
this:
matrix_stone_relation_algebra.point (f \<odot> mtop)

goal (1 subgoal):
 1. \<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
matrix_stone_relation_algebra.point (f \<odot> mtop)
[PROOF STEP]
obtain i where 1: "\<forall>j . (f \<odot> mtop) (i,j) = top \<and> (\<forall>k . i \<noteq> k \<longrightarrow> (f \<odot> mtop) (k,j) = bot)"
[PROOF STATE]
proof (prove)
using this:
matrix_stone_relation_algebra.point (f \<odot> mtop)

goal (1 subgoal):
 1. (\<And>i. \<forall>j. (f \<odot> mtop) (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> (f \<odot> mtop) (k, j) = bot) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using point_linorder_matrix
[PROOF STATE]
proof (prove)
using this:
matrix_stone_relation_algebra.point (f \<odot> mtop)
matrix_stone_relation_algebra.point ?f = (\<exists>i. \<forall>j. ?f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> ?f (k, j) = bot))

goal (1 subgoal):
 1. (\<And>i. \<forall>j. (f \<odot> mtop) (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> (f \<odot> mtop) (k, j) = bot) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>j. (f \<odot> mtop) (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> (f \<odot> mtop) (k, j) = bot)

goal (1 subgoal):
 1. \<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
have "matrix_stone_relation_algebra.point (f\<^sup>t \<odot> mtop)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.point (f\<^sup>t \<odot> mtop)
[PROOF STEP]
by (simp add: assms matrix_bounded_idempotent_semiring.vector_mult_closed)
[PROOF STATE]
proof (state)
this:
matrix_stone_relation_algebra.point (f\<^sup>t \<odot> mtop)

goal (1 subgoal):
 1. \<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
matrix_stone_relation_algebra.point (f\<^sup>t \<odot> mtop)
[PROOF STEP]
obtain j where "\<forall>i . (f\<^sup>t \<odot> mtop) (j,i) = top \<and> (\<forall>k . j \<noteq> k \<longrightarrow> (f\<^sup>t \<odot> mtop) (k,i) = bot)"
[PROOF STATE]
proof (prove)
using this:
matrix_stone_relation_algebra.point (f\<^sup>t \<odot> mtop)

goal (1 subgoal):
 1. (\<And>j. \<forall>i. (f\<^sup>t \<odot> mtop) (j, i) = top \<and> (\<forall>k. j \<noteq> k \<longrightarrow> (f\<^sup>t \<odot> mtop) (k, i) = bot) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using point_linorder_matrix
[PROOF STATE]
proof (prove)
using this:
matrix_stone_relation_algebra.point (f\<^sup>t \<odot> mtop)
matrix_stone_relation_algebra.point ?f = (\<exists>i. \<forall>j. ?f (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> ?f (k, j) = bot))

goal (1 subgoal):
 1. (\<And>j. \<forall>i. (f\<^sup>t \<odot> mtop) (j, i) = top \<and> (\<forall>k. j \<noteq> k \<longrightarrow> (f\<^sup>t \<odot> mtop) (k, i) = bot) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i. (f\<^sup>t \<odot> mtop) (j, i) = top \<and> (\<forall>k. j \<noteq> k \<longrightarrow> (f\<^sup>t \<odot> mtop) (k, i) = bot)

goal (1 subgoal):
 1. \<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
hence 2: "\<forall>i . (mtop \<odot> f) (i,j) = top \<and> (\<forall>k . j \<noteq> k \<longrightarrow> (mtop \<odot> f) (i,k) = bot)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (f\<^sup>t \<odot> mtop) (j, i) = top \<and> (\<forall>k. j \<noteq> k \<longrightarrow> (f\<^sup>t \<odot> mtop) (k, i) = bot)

goal (1 subgoal):
 1. \<forall>i. (mtop \<odot> f) (i, j) = top \<and> (\<forall>k. j \<noteq> k \<longrightarrow> (mtop \<odot> f) (i, k) = bot)
[PROOF STEP]
by (metis (no_types) old.prod.case conv_matrix_def conv_def matrix_stone_relation_algebra.conv_dist_comp matrix_stone_relation_algebra.conv_top)
[PROOF STATE]
proof (state)
this:
\<forall>i. (mtop \<odot> f) (i, j) = top \<and> (\<forall>k. j \<noteq> k \<longrightarrow> (mtop \<odot> f) (i, k) = bot)

goal (1 subgoal):
 1. \<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
have 3: "\<forall>i k . j \<noteq> k \<longrightarrow> f (i,k) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i k. j \<noteq> k \<longrightarrow> f (i, k) = bot
[PROOF STEP]
proof (intro allI, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i k. j \<noteq> k \<Longrightarrow> f (i, k) = bot
[PROOF STEP]
fix i k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i k. j \<noteq> k \<Longrightarrow> f (i, k) = bot
[PROOF STEP]
assume "j \<noteq> k"
[PROOF STATE]
proof (state)
this:
j \<noteq> k

goal (1 subgoal):
 1. \<And>i k. j \<noteq> k \<Longrightarrow> f (i, k) = bot
[PROOF STEP]
hence "(\<Squnion>\<^sub>l f (l,k)) = bot"
[PROOF STATE]
proof (prove)
using this:
j \<noteq> k

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. f (l, k)) {l. True} = bot
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
j \<noteq> k
\<forall>i. (mtop \<odot> f) (i, j) = top \<and> (\<forall>k. j \<noteq> k \<longrightarrow> (mtop \<odot> f) (i, k) = bot)

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. f (l, k)) {l. True} = bot
[PROOF STEP]
by (simp add: top_comp_linorder_matrix)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. f (l, k)) {l. True} = bot

goal (1 subgoal):
 1. \<And>i k. j \<noteq> k \<Longrightarrow> f (i, k) = bot
[PROOF STEP]
thus "f (i,k) = bot"
[PROOF STATE]
proof (prove)
using this:
sup_monoid.sum (\<lambda>l. f (l, k)) {l. True} = bot

goal (1 subgoal):
 1. f (i, k) = bot
[PROOF STEP]
by (metis bot.extremum_uniqueI comp_inf.ub_sum)
[PROOF STATE]
proof (state)
this:
f (i, k) = bot

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i k. j \<noteq> k \<longrightarrow> f (i, k) = bot

goal (1 subgoal):
 1. \<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
have "(\<Squnion>\<^sub>k f (i,k)) = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} = top
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<forall>j. (f \<odot> mtop) (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> (f \<odot> mtop) (k, j) = bot)

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} = top
[PROOF STEP]
by (simp add: comp_top_linorder_matrix)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} = top

goal (1 subgoal):
 1. \<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
hence 4: "f (i,j) = top"
[PROOF STATE]
proof (prove)
using this:
sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} = top

goal (1 subgoal):
 1. f (i, j) = top
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} = top
\<forall>i k. j \<noteq> k \<longrightarrow> f (i, k) = bot

goal (1 subgoal):
 1. f (i, j) = top
[PROOF STEP]
by (metis bot_not_top linorder_finite_sup_selective)
[PROOF STATE]
proof (state)
this:
f (i, j) = top

goal (1 subgoal):
 1. \<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
have "\<forall>k l . k \<noteq> i \<or> l \<noteq> j \<longrightarrow> f (k,l) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k l. k \<noteq> i \<or> l \<noteq> j \<longrightarrow> f (k, l) = bot
[PROOF STEP]
proof (intro allI, unfold imp_disjL, rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k l. k \<noteq> i \<longrightarrow> f (k, l) = bot
 2. \<And>k l. l \<noteq> j \<longrightarrow> f (k, l) = bot
[PROOF STEP]
fix k l
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k l. k \<noteq> i \<longrightarrow> f (k, l) = bot
 2. \<And>k l. l \<noteq> j \<longrightarrow> f (k, l) = bot
[PROOF STEP]
show "k \<noteq> i \<longrightarrow> f (k,l) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<noteq> i \<longrightarrow> f (k, l) = bot
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> f (k, l) = bot
[PROOF STEP]
assume "k \<noteq> i"
[PROOF STATE]
proof (state)
this:
k \<noteq> i

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> f (k, l) = bot
[PROOF STEP]
hence "(\<Squnion>\<^sub>m f (k,m)) = bot"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> i

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>m. f (k, m)) {m. True} = bot
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
k \<noteq> i
\<forall>j. (f \<odot> mtop) (i, j) = top \<and> (\<forall>k. i \<noteq> k \<longrightarrow> (f \<odot> mtop) (k, j) = bot)

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>m. f (k, m)) {m. True} = bot
[PROOF STEP]
by (simp add: comp_top_linorder_matrix)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>m. f (k, m)) {m. True} = bot

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> f (k, l) = bot
[PROOF STEP]
thus "f (k,l) = bot"
[PROOF STATE]
proof (prove)
using this:
sup_monoid.sum (\<lambda>m. f (k, m)) {m. True} = bot

goal (1 subgoal):
 1. f (k, l) = bot
[PROOF STEP]
by (metis bot.extremum_uniqueI comp_inf.ub_sum)
[PROOF STATE]
proof (state)
this:
f (k, l) = bot

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k \<noteq> i \<longrightarrow> f (k, l) = bot

goal (1 subgoal):
 1. \<And>k l. l \<noteq> j \<longrightarrow> f (k, l) = bot
[PROOF STEP]
show "l \<noteq> j \<longrightarrow> f (k,l) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<noteq> j \<longrightarrow> f (k, l) = bot
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
\<forall>i k. j \<noteq> k \<longrightarrow> f (i, k) = bot

goal (1 subgoal):
 1. l \<noteq> j \<longrightarrow> f (k, l) = bot
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l \<noteq> j \<longrightarrow> f (k, l) = bot

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>k l. k \<noteq> i \<or> l \<noteq> j \<longrightarrow> f (k, l) = bot

goal (1 subgoal):
 1. \<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>k l. k \<noteq> i \<or> l \<noteq> j \<longrightarrow> f (k, l) = bot

goal (1 subgoal):
 1. \<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
\<forall>k l. k \<noteq> i \<or> l \<noteq> j \<longrightarrow> f (k, l) = bot
f (i, j) = top

goal (1 subgoal):
 1. \<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
by (metis old.prod.exhaust)
[PROOF STATE]
proof (state)
this:
\<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pp_arc_linorder_matrix_2:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "\<exists>e . f e \<noteq> bot \<and> (\<forall>d . e \<noteq> d \<longrightarrow> f d = bot)"
    shows "matrix_stone_relation_algebra.pp_arc f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.pp_arc f
[PROOF STEP]
proof (unfold matrix_stone_relation_algebra.pp_arc_expanded, intro conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. matrix_idempotent_semiring.coreflexive (f \<odot> mtop \<odot> f\<^sup>t)
 2. matrix_idempotent_semiring.coreflexive (f\<^sup>t \<odot> mtop \<odot> f)
 3. matrix_bounded_idempotent_semiring.total (mtop \<odot> \<ominus> \<ominus> f)
[PROOF STEP]
show "f \<odot> mtop \<odot> f\<^sup>t \<preceq> mone"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_idempotent_semiring.coreflexive (f \<odot> mtop \<odot> f\<^sup>t)
[PROOF STEP]
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e a b. (f \<odot> mtop \<odot> f\<^sup>t) (a, b) \<le> mone (a, b)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e a b. (f \<odot> mtop \<odot> f\<^sup>t) (a, b) \<le> mone (a, b)
[PROOF STEP]
show "(f \<odot> mtop \<odot> f\<^sup>t) (i,j) \<le> mone (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
proof (cases "i = j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = j \<Longrightarrow> (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
 2. i \<noteq> j \<Longrightarrow> (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
assume "i = j"
[PROOF STATE]
proof (state)
this:
i = j

goal (2 subgoals):
 1. i = j \<Longrightarrow> (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
 2. i \<noteq> j \<Longrightarrow> (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i = j

goal (1 subgoal):
 1. (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
by (simp add: one_matrix_def)
[PROOF STATE]
proof (state)
this:
(f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
assume "i \<noteq> j"
[PROOF STATE]
proof (state)
this:
i \<noteq> j

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
hence 1: "\<forall>k l . f (i,k) * f (j,l) = bot"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> j

goal (1 subgoal):
 1. \<forall>k l. f (i, k) * f (j, l) = bot
[PROOF STEP]
by (metis assms Pair_inject semiring.mult_not_zero)
[PROOF STATE]
proof (state)
this:
\<forall>k l. f (i, k) * f (j, l) = bot

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
have "(f \<odot> mtop \<odot> f\<^sup>t) (i,j) = (\<Squnion>\<^sub>l (f \<odot> mtop) (i,l) * (f\<^sup>t) (l,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<odot> mtop \<odot> f\<^sup>t) (i, j) = sup_monoid.sum (\<lambda>l. (f \<odot> mtop) (i, l) * (f\<^sup>t) (l, j)) {l. True}
[PROOF STEP]
by (simp add: times_matrix_def)
[PROOF STATE]
proof (state)
this:
(f \<odot> mtop \<odot> f\<^sup>t) (i, j) = sup_monoid.sum (\<lambda>l. (f \<odot> mtop) (i, l) * (f\<^sup>t) (l, j)) {l. True}

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f \<odot> mtop \<odot> f\<^sup>t) (i, j) = sup_monoid.sum (\<lambda>l. (f \<odot> mtop) (i, l) * (f\<^sup>t) (l, j)) {l. True}

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
have "... = (\<Squnion>\<^sub>l (f \<odot> mtop) (i,l) * f (j,l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. (f \<odot> mtop) (i, l) * (f\<^sup>t) (l, j)) {l. True} = sup_monoid.sum (\<lambda>l. (f \<odot> mtop) (i, l) * f (j, l)) {l. True}
[PROOF STEP]
by (simp add: conv_matrix_def)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. (f \<odot> mtop) (i, l) * (f\<^sup>t) (l, j)) {l. True} = sup_monoid.sum (\<lambda>l. (f \<odot> mtop) (i, l) * f (j, l)) {l. True}

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. (f \<odot> mtop) (i, l) * (f\<^sup>t) (l, j)) {l. True} = sup_monoid.sum (\<lambda>l. (f \<odot> mtop) (i, l) * f (j, l)) {l. True}

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
have "... = (\<Squnion>\<^sub>l (\<Squnion>\<^sub>k f (i,k)) * f (j,l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. (f \<odot> mtop) (i, l) * f (j, l)) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} * f (j, l)) {l. True}
[PROOF STEP]
by (simp add: comp_top_linorder_matrix)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. (f \<odot> mtop) (i, l) * f (j, l)) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} * f (j, l)) {l. True}

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. (f \<odot> mtop) (i, l) * f (j, l)) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} * f (j, l)) {l. True}

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
have "... = (\<Squnion>\<^sub>l \<Squnion>\<^sub>k f (i,k) * f (j,l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} * f (j, l)) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (i, k) * f (j, l)) {k. True}) {l. True}
[PROOF STEP]
by (metis comp_right_dist_sum)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} * f (j, l)) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (i, k) * f (j, l)) {k. True}) {l. True}

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} * f (j, l)) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (i, k) * f (j, l)) {k. True}) {l. True}

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
have "... = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (i, k) * f (j, l)) {k. True}) {l. True} = bot
[PROOF STEP]
using 1 linorder_finite_sup_selective
[PROOF STATE]
proof (prove)
using this:
\<forall>k l. f (i, k) * f (j, l) = bot
\<exists>i. sup_monoid.sum ?f {k. True} = ?f i

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (i, k) * f (j, l)) {k. True}) {l. True} = bot
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (i, k) * f (j, l)) {k. True}) {l. True} = bot

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(f \<odot> mtop \<odot> f\<^sup>t) (i, j) = bot
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(f \<odot> mtop \<odot> f\<^sup>t) (i, j) = bot

goal (1 subgoal):
 1. (f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(f \<odot> mtop \<odot> f\<^sup>t) (i, j) \<le> mone (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
matrix_idempotent_semiring.coreflexive (f \<odot> mtop \<odot> f\<^sup>t)

goal (2 subgoals):
 1. matrix_idempotent_semiring.coreflexive (f\<^sup>t \<odot> mtop \<odot> f)
 2. matrix_bounded_idempotent_semiring.total (mtop \<odot> \<ominus> \<ominus> f)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. matrix_idempotent_semiring.coreflexive (f\<^sup>t \<odot> mtop \<odot> f)
 2. matrix_bounded_idempotent_semiring.total (mtop \<odot> \<ominus> \<ominus> f)
[PROOF STEP]
show "f\<^sup>t \<odot> mtop \<odot> f \<preceq> mone"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_idempotent_semiring.coreflexive (f\<^sup>t \<odot> mtop \<odot> f)
[PROOF STEP]
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e a b. (f\<^sup>t \<odot> mtop \<odot> f) (a, b) \<le> mone (a, b)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e a b. (f\<^sup>t \<odot> mtop \<odot> f) (a, b) \<le> mone (a, b)
[PROOF STEP]
show "(f\<^sup>t \<odot> mtop \<odot> f) (i,j) \<le> mone (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
proof (cases "i = j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = j \<Longrightarrow> (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
 2. i \<noteq> j \<Longrightarrow> (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
assume "i = j"
[PROOF STATE]
proof (state)
this:
i = j

goal (2 subgoals):
 1. i = j \<Longrightarrow> (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
 2. i \<noteq> j \<Longrightarrow> (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i = j

goal (1 subgoal):
 1. (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
by (simp add: one_matrix_def)
[PROOF STATE]
proof (state)
this:
(f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
assume "i \<noteq> j"
[PROOF STATE]
proof (state)
this:
i \<noteq> j

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
hence 2: "\<forall>k l . f (k,i) * f (l,j) = bot"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> j

goal (1 subgoal):
 1. \<forall>k l. f (k, i) * f (l, j) = bot
[PROOF STEP]
by (metis assms Pair_inject semiring.mult_not_zero)
[PROOF STATE]
proof (state)
this:
\<forall>k l. f (k, i) * f (l, j) = bot

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
have "(f\<^sup>t \<odot> mtop \<odot> f) (i,j) = (\<Squnion>\<^sub>l (f\<^sup>t \<odot> mtop) (i,l) * f (l,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f\<^sup>t \<odot> mtop \<odot> f) (i, j) = sup_monoid.sum (\<lambda>l. (f\<^sup>t \<odot> mtop) (i, l) * f (l, j)) {l. True}
[PROOF STEP]
by (simp add: times_matrix_def)
[PROOF STATE]
proof (state)
this:
(f\<^sup>t \<odot> mtop \<odot> f) (i, j) = sup_monoid.sum (\<lambda>l. (f\<^sup>t \<odot> mtop) (i, l) * f (l, j)) {l. True}

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f\<^sup>t \<odot> mtop \<odot> f) (i, j) = sup_monoid.sum (\<lambda>l. (f\<^sup>t \<odot> mtop) (i, l) * f (l, j)) {l. True}

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
have "... = (\<Squnion>\<^sub>l (\<Squnion>\<^sub>k (f\<^sup>t) (i,k)) * f (l,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. (f\<^sup>t \<odot> mtop) (i, l) * f (l, j)) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. (f\<^sup>t) (i, k)) {k. True} * f (l, j)) {l. True}
[PROOF STEP]
by (simp add: comp_top_linorder_matrix)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. (f\<^sup>t \<odot> mtop) (i, l) * f (l, j)) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. (f\<^sup>t) (i, k)) {k. True} * f (l, j)) {l. True}

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. (f\<^sup>t \<odot> mtop) (i, l) * f (l, j)) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. (f\<^sup>t) (i, k)) {k. True} * f (l, j)) {l. True}

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
have "... = (\<Squnion>\<^sub>l (\<Squnion>\<^sub>k f (k,i)) * f (l,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. (f\<^sup>t) (i, k)) {k. True} * f (l, j)) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, i)) {k. True} * f (l, j)) {l. True}
[PROOF STEP]
by (simp add: conv_matrix_def)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. (f\<^sup>t) (i, k)) {k. True} * f (l, j)) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, i)) {k. True} * f (l, j)) {l. True}

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. (f\<^sup>t) (i, k)) {k. True} * f (l, j)) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, i)) {k. True} * f (l, j)) {l. True}

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
have "... = (\<Squnion>\<^sub>l \<Squnion>\<^sub>k f (k,i) * f (l,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, i)) {k. True} * f (l, j)) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, i) * f (l, j)) {k. True}) {l. True}
[PROOF STEP]
by (metis comp_right_dist_sum)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, i)) {k. True} * f (l, j)) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, i) * f (l, j)) {k. True}) {l. True}

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, i)) {k. True} * f (l, j)) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, i) * f (l, j)) {k. True}) {l. True}

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
have "... = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, i) * f (l, j)) {k. True}) {l. True} = bot
[PROOF STEP]
using 2 linorder_finite_sup_selective
[PROOF STATE]
proof (prove)
using this:
\<forall>k l. f (k, i) * f (l, j) = bot
\<exists>i. sup_monoid.sum ?f {k. True} = ?f i

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, i) * f (l, j)) {k. True}) {l. True} = bot
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, i) * f (l, j)) {k. True}) {l. True} = bot

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(f\<^sup>t \<odot> mtop \<odot> f) (i, j) = bot
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(f\<^sup>t \<odot> mtop \<odot> f) (i, j) = bot

goal (1 subgoal):
 1. (f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(f\<^sup>t \<odot> mtop \<odot> f) (i, j) \<le> mone (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
matrix_idempotent_semiring.coreflexive (f\<^sup>t \<odot> mtop \<odot> f)

goal (1 subgoal):
 1. matrix_bounded_idempotent_semiring.total (mtop \<odot> \<ominus> \<ominus> f)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_bounded_idempotent_semiring.total (mtop \<odot> \<ominus> \<ominus> f)
[PROOF STEP]
show "mtop \<odot> \<ominus>\<ominus>f \<odot> mtop = mtop"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_bounded_idempotent_semiring.total (mtop \<odot> \<ominus> \<ominus> f)
[PROOF STEP]
proof (rule ext, rule prod_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
obtain k l where "f (k,l) \<noteq> bot"
[PROOF STATE]
proof (prove)
using this:
\<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)

goal (1 subgoal):
 1. (\<And>k l. f (k, l) \<noteq> bot \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
\<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>k l. f (k, l) \<noteq> bot \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (k, l) \<noteq> bot

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
hence "top = --f (k,l)"
[PROOF STATE]
proof (prove)
using this:
f (k, l) \<noteq> bot

goal (1 subgoal):
 1. top = - - f (k, l)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
top = - - f (k, l)

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
top = - - f (k, l)

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
have "... \<le> (\<Squnion>\<^sub>k --f (k,l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - f (k, l) \<le> sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}
[PROOF STEP]
using comp_inf.ub_sum
[PROOF STATE]
proof (prove)
using this:
?f ?i \<le> sup_monoid.sum ?f {k. True}

goal (1 subgoal):
 1. - - f (k, l) \<le> sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
- - f (k, l) \<le> sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- - f (k, l) \<le> sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
have "... \<le> (\<Squnion>\<^sub>l \<Squnion>\<^sub>k --f (k,l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True} \<le> sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}) {l. True}
[PROOF STEP]
using comp_inf.ub_sum
[PROOF STATE]
proof (prove)
using this:
?f ?i \<le> sup_monoid.sum ?f {k. True}

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True} \<le> sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}) {l. True}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True} \<le> sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}) {l. True}

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
comp_inf.reflexive (sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}) {l. True})
[PROOF STEP]
have 3: "top \<le> (\<Squnion>\<^sub>l \<Squnion>\<^sub>k --f (k,l))"
[PROOF STATE]
proof (prove)
using this:
comp_inf.reflexive (sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}) {l. True})

goal (1 subgoal):
 1. comp_inf.reflexive (sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}) {l. True})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
comp_inf.reflexive (sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}) {l. True})

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
have "(mtop \<odot> \<ominus>\<ominus>f \<odot> mtop) (i,j) = (\<Squnion>\<^sub>l (\<Squnion>\<^sub>k top * --f (k,l)) * top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (i, j) = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. top * - - f (k, l)) {k. True} * top) {l. True}
[PROOF STEP]
by (simp add: times_matrix_def top_matrix_def uminus_matrix_def)
[PROOF STATE]
proof (state)
this:
(mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (i, j) = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. top * - - f (k, l)) {k. True} * top) {l. True}

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (i, j) = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. top * - - f (k, l)) {k. True} * top) {l. True}

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
have "... = (\<Squnion>\<^sub>l \<Squnion>\<^sub>k --f (k,l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. top * - - f (k, l)) {k. True} * top) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}) {l. True}
[PROOF STEP]
by (metis (no_types, lifting) sup_monoid.sum.cong comp_inf.mult_1_left times_inf comp_inf.mult_1_right)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. top * - - f (k, l)) {k. True} * top) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}) {l. True}

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. top * - - f (k, l)) {k. True} * top) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}) {l. True}

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
have "... = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}) {l. True} = top
[PROOF STEP]
using 3 top.extremum_unique
[PROOF STATE]
proof (prove)
using this:
comp_inf.reflexive (sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}) {l. True})
(top \<le> ?a) = (?a = top)

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}) {l. True} = top
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. - - f (k, l)) {k. True}) {l. True} = top

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (i, j) = top
[PROOF STEP]
show "(mtop \<odot> \<ominus>\<ominus>f \<odot> mtop) (i,j) = mtop (i,j)"
[PROOF STATE]
proof (prove)
using this:
(mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (i, j) = top

goal (1 subgoal):
 1. (mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (i, j) = mtop (i, j)
[PROOF STEP]
by (simp add: top_matrix_def)
[PROOF STATE]
proof (state)
this:
(mtop \<odot> \<ominus> \<ominus> f \<odot> mtop) (i, j) = mtop (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
matrix_bounded_idempotent_semiring.total (mtop \<odot> \<ominus> \<ominus> f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arc_linorder_matrix_2:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  assumes "\<exists>e . f e = top \<and> (\<forall>d . e \<noteq> d \<longrightarrow> f d = bot)"
    shows "matrix_stone_relation_algebra.arc f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.arc f
[PROOF STEP]
proof (unfold matrix_stone_relation_algebra.arc_expanded, intro conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. matrix_idempotent_semiring.coreflexive (f \<odot> mtop \<odot> f\<^sup>t)
 2. matrix_idempotent_semiring.coreflexive (f\<^sup>t \<odot> mtop \<odot> f)
 3. matrix_bounded_idempotent_semiring.total (mtop \<odot> f)
[PROOF STEP]
show "f \<odot> mtop \<odot> f\<^sup>t \<preceq> mone"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_idempotent_semiring.coreflexive (f \<odot> mtop \<odot> f\<^sup>t)
[PROOF STEP]
by (metis (no_types, lifting) assms bot_not_top matrix_stone_relation_algebra.pp_arc_expanded pp_arc_linorder_matrix_2)
[PROOF STATE]
proof (state)
this:
matrix_idempotent_semiring.coreflexive (f \<odot> mtop \<odot> f\<^sup>t)

goal (2 subgoals):
 1. matrix_idempotent_semiring.coreflexive (f\<^sup>t \<odot> mtop \<odot> f)
 2. matrix_bounded_idempotent_semiring.total (mtop \<odot> f)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. matrix_idempotent_semiring.coreflexive (f\<^sup>t \<odot> mtop \<odot> f)
 2. matrix_bounded_idempotent_semiring.total (mtop \<odot> f)
[PROOF STEP]
show "f\<^sup>t \<odot> mtop \<odot> f \<preceq> mone"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_idempotent_semiring.coreflexive (f\<^sup>t \<odot> mtop \<odot> f)
[PROOF STEP]
by (metis (no_types, lifting) assms bot_not_top matrix_stone_relation_algebra.pp_arc_expanded pp_arc_linorder_matrix_2)
[PROOF STATE]
proof (state)
this:
matrix_idempotent_semiring.coreflexive (f\<^sup>t \<odot> mtop \<odot> f)

goal (1 subgoal):
 1. matrix_bounded_idempotent_semiring.total (mtop \<odot> f)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_bounded_idempotent_semiring.total (mtop \<odot> f)
[PROOF STEP]
show "mtop \<odot> f \<odot> mtop = mtop"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_bounded_idempotent_semiring.total (mtop \<odot> f)
[PROOF STEP]
proof (rule ext, rule prod_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
obtain k l where "f (k,l) = top"
[PROOF STATE]
proof (prove)
using this:
\<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)

goal (1 subgoal):
 1. (\<And>k l. f (k, l) = top \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
\<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>k l. f (k, l) = top \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (k, l) = top

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
hence "(\<Squnion>\<^sub>k f (k,l)) = top"
[PROOF STATE]
proof (prove)
using this:
f (k, l) = top

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>k. f (k, l)) {k. True} = top
[PROOF STEP]
by (metis (mono_tags) comp_inf.ub_sum top_unique)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>k. f (k, l)) {k. True} = top

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
hence 3: "top \<le> (\<Squnion>\<^sub>l \<Squnion>\<^sub>k f (k,l))"
[PROOF STATE]
proof (prove)
using this:
sup_monoid.sum (\<lambda>k. f (k, l)) {k. True} = top

goal (1 subgoal):
 1. comp_inf.reflexive (sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, l)) {k. True}) {l. True})
[PROOF STEP]
by (metis (no_types) comp_inf.ub_sum)
[PROOF STATE]
proof (state)
this:
comp_inf.reflexive (sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, l)) {k. True}) {l. True})

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
have "(mtop \<odot> f \<odot> mtop) (i,j) = (\<Squnion>\<^sub>l (\<Squnion>\<^sub>k top * f (k,l)) * top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mtop \<odot> f \<odot> mtop) (i, j) = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. top * f (k, l)) {k. True} * top) {l. True}
[PROOF STEP]
by (simp add: times_matrix_def top_matrix_def)
[PROOF STATE]
proof (state)
this:
(mtop \<odot> f \<odot> mtop) (i, j) = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. top * f (k, l)) {k. True} * top) {l. True}

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(mtop \<odot> f \<odot> mtop) (i, j) = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. top * f (k, l)) {k. True} * top) {l. True}

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
have "... = (\<Squnion>\<^sub>l \<Squnion>\<^sub>k f (k,l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. top * f (k, l)) {k. True} * top) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, l)) {k. True}) {l. True}
[PROOF STEP]
by (metis (no_types, lifting) sup_monoid.sum.cong comp_inf.mult_1_left times_inf comp_inf.mult_1_right)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. top * f (k, l)) {k. True} * top) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, l)) {k. True}) {l. True}

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. top * f (k, l)) {k. True} * top) {l. True} = sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, l)) {k. True}) {l. True}

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
have "... = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, l)) {k. True}) {l. True} = top
[PROOF STEP]
using 3 top.extremum_unique
[PROOF STATE]
proof (prove)
using this:
comp_inf.reflexive (sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, l)) {k. True}) {l. True})
(top \<le> ?a) = (?a = top)

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, l)) {k. True}) {l. True} = top
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. sup_monoid.sum (\<lambda>k. f (k, l)) {k. True}) {l. True} = top

goal (1 subgoal):
 1. \<And>x a b. (mtop \<odot> f \<odot> mtop) (a, b) = mtop (a, b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(mtop \<odot> f \<odot> mtop) (i, j) = top
[PROOF STEP]
show "(mtop \<odot> f \<odot> mtop) (i,j) = mtop (i,j)"
[PROOF STATE]
proof (prove)
using this:
(mtop \<odot> f \<odot> mtop) (i, j) = top

goal (1 subgoal):
 1. (mtop \<odot> f \<odot> mtop) (i, j) = mtop (i, j)
[PROOF STEP]
by (simp add: top_matrix_def)
[PROOF STATE]
proof (state)
this:
(mtop \<odot> f \<odot> mtop) (i, j) = mtop (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
matrix_bounded_idempotent_semiring.total (mtop \<odot> f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arc_linorder_matrix:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.arc f \<longleftrightarrow> (\<exists>e . f e = top \<and> (\<forall>d . e \<noteq> d \<longrightarrow> f d = bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.arc f = (\<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot))
[PROOF STEP]
using arc_linorder_matrix_1 arc_linorder_matrix_2
[PROOF STATE]
proof (prove)
using this:
matrix_stone_relation_algebra.arc ?f \<Longrightarrow> \<exists>e. ?f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> ?f d = bot)
\<exists>e. ?f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> ?f d = bot) \<Longrightarrow> matrix_stone_relation_algebra.arc ?f

goal (1 subgoal):
 1. matrix_stone_relation_algebra.arc f = (\<exists>e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot))
[PROOF STEP]
by blast


[STATEMENT]
lemma arc_linorder_matrix_unique:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.arc f \<longleftrightarrow> (\<exists>!e . f e = top \<and> (\<forall>d . e \<noteq> d \<longrightarrow> f d = bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.arc f = (\<exists>!e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot))
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. matrix_stone_relation_algebra.arc f \<Longrightarrow> \<exists>!e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
 2. \<exists>!e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot) \<Longrightarrow> matrix_stone_relation_algebra.arc f
[PROOF STEP]
apply (metis (no_types, opaque_lifting) arc_linorder_matrix bot_not_top)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot) \<Longrightarrow> matrix_stone_relation_algebra.arc f
[PROOF STEP]
using arc_linorder_matrix
[PROOF STATE]
proof (prove)
using this:
matrix_stone_relation_algebra.arc ?f = (\<exists>e. ?f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> ?f d = bot))

goal (1 subgoal):
 1. \<exists>!e. f e = top \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot) \<Longrightarrow> matrix_stone_relation_algebra.arc f
[PROOF STEP]
by blast


[STATEMENT]
lemma pp_arc_linorder_matrix_1:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_stone_relation_algebra.pp_arc f"
    shows "\<exists>e . f e \<noteq> bot \<and> (\<forall>d . e \<noteq> d \<longrightarrow> f d = bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
have "matrix_stone_relation_algebra.pp_point (f \<odot> mtop)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.pp_point (f \<odot> mtop)
[PROOF STEP]
by (simp add: assms matrix_bounded_idempotent_semiring.vector_mult_closed)
[PROOF STATE]
proof (state)
this:
matrix_stone_relation_algebra.pp_point (f \<odot> mtop)

goal (1 subgoal):
 1. \<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
matrix_stone_relation_algebra.pp_point (f \<odot> mtop)
[PROOF STEP]
obtain i where 1: "\<forall>j . (f \<odot> mtop) (i,j) \<noteq> bot \<and> (\<forall>k . (f \<odot> mtop) (i,j) = (f \<odot> mtop) (i,k)) \<and> (\<forall>k . i \<noteq> k \<longrightarrow> (f \<odot> mtop) (k,j) = bot)"
[PROOF STATE]
proof (prove)
using this:
matrix_stone_relation_algebra.pp_point (f \<odot> mtop)

goal (1 subgoal):
 1. (\<And>i. \<forall>j. (f \<odot> mtop) (i, j) \<noteq> bot \<and> (\<forall>k. (f \<odot> mtop) (i, j) = (f \<odot> mtop) (i, k)) \<and> (\<forall>k. i \<noteq> k \<longrightarrow> (f \<odot> mtop) (k, j) = bot) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis pp_point_linorder_matrix)
[PROOF STATE]
proof (state)
this:
\<forall>j. (f \<odot> mtop) (i, j) \<noteq> bot \<and> (\<forall>k. (f \<odot> mtop) (i, j) = (f \<odot> mtop) (i, k)) \<and> (\<forall>k. i \<noteq> k \<longrightarrow> (f \<odot> mtop) (k, j) = bot)

goal (1 subgoal):
 1. \<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
have "matrix_stone_relation_algebra.pp_point (f\<^sup>t \<odot> mtop)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.pp_point (f\<^sup>t \<odot> mtop)
[PROOF STEP]
by (simp add: assms matrix_bounded_idempotent_semiring.vector_mult_closed)
[PROOF STATE]
proof (state)
this:
matrix_stone_relation_algebra.pp_point (f\<^sup>t \<odot> mtop)

goal (1 subgoal):
 1. \<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
matrix_stone_relation_algebra.pp_point (f\<^sup>t \<odot> mtop)
[PROOF STEP]
obtain j where "\<forall>i . (f\<^sup>t \<odot> mtop) (j,i) \<noteq> bot \<and> (\<forall>k . (f\<^sup>t \<odot> mtop) (j,i) = (f\<^sup>t \<odot> mtop) (j,k)) \<and> (\<forall>k . j \<noteq> k \<longrightarrow> (f\<^sup>t \<odot> mtop) (k,i) = bot)"
[PROOF STATE]
proof (prove)
using this:
matrix_stone_relation_algebra.pp_point (f\<^sup>t \<odot> mtop)

goal (1 subgoal):
 1. (\<And>j. \<forall>i. (f\<^sup>t \<odot> mtop) (j, i) \<noteq> bot \<and> (\<forall>k. (f\<^sup>t \<odot> mtop) (j, i) = (f\<^sup>t \<odot> mtop) (j, k)) \<and> (\<forall>k. j \<noteq> k \<longrightarrow> (f\<^sup>t \<odot> mtop) (k, i) = bot) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis pp_point_linorder_matrix)
[PROOF STATE]
proof (state)
this:
\<forall>i. (f\<^sup>t \<odot> mtop) (j, i) \<noteq> bot \<and> (\<forall>k. (f\<^sup>t \<odot> mtop) (j, i) = (f\<^sup>t \<odot> mtop) (j, k)) \<and> (\<forall>k. j \<noteq> k \<longrightarrow> (f\<^sup>t \<odot> mtop) (k, i) = bot)

goal (1 subgoal):
 1. \<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
hence 2: "\<forall>i . (mtop \<odot> f) (i,j) \<noteq> bot \<and> (\<forall>k . (mtop \<odot> f) (i,j) = (mtop \<odot> f) (k,j)) \<and> (\<forall>k . j \<noteq> k \<longrightarrow> (mtop \<odot> f) (i,k) = bot)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (f\<^sup>t \<odot> mtop) (j, i) \<noteq> bot \<and> (\<forall>k. (f\<^sup>t \<odot> mtop) (j, i) = (f\<^sup>t \<odot> mtop) (j, k)) \<and> (\<forall>k. j \<noteq> k \<longrightarrow> (f\<^sup>t \<odot> mtop) (k, i) = bot)

goal (1 subgoal):
 1. \<forall>i. (mtop \<odot> f) (i, j) \<noteq> bot \<and> (\<forall>k. (mtop \<odot> f) (i, j) = (mtop \<odot> f) (k, j)) \<and> (\<forall>k. j \<noteq> k \<longrightarrow> (mtop \<odot> f) (i, k) = bot)
[PROOF STEP]
by (metis (no_types) old.prod.case conv_matrix_def conv_def matrix_stone_relation_algebra.conv_dist_comp matrix_stone_relation_algebra.conv_top)
[PROOF STATE]
proof (state)
this:
\<forall>i. (mtop \<odot> f) (i, j) \<noteq> bot \<and> (\<forall>k. (mtop \<odot> f) (i, j) = (mtop \<odot> f) (k, j)) \<and> (\<forall>k. j \<noteq> k \<longrightarrow> (mtop \<odot> f) (i, k) = bot)

goal (1 subgoal):
 1. \<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
have 3: "\<forall>i k . j \<noteq> k \<longrightarrow> f (i,k) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i k. j \<noteq> k \<longrightarrow> f (i, k) = bot
[PROOF STEP]
proof (intro allI, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i k. j \<noteq> k \<Longrightarrow> f (i, k) = bot
[PROOF STEP]
fix i k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i k. j \<noteq> k \<Longrightarrow> f (i, k) = bot
[PROOF STEP]
assume "j \<noteq> k"
[PROOF STATE]
proof (state)
this:
j \<noteq> k

goal (1 subgoal):
 1. \<And>i k. j \<noteq> k \<Longrightarrow> f (i, k) = bot
[PROOF STEP]
hence "(\<Squnion>\<^sub>l f (l,k)) = bot"
[PROOF STATE]
proof (prove)
using this:
j \<noteq> k

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. f (l, k)) {l. True} = bot
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
j \<noteq> k
\<forall>i. (mtop \<odot> f) (i, j) \<noteq> bot \<and> (\<forall>k. (mtop \<odot> f) (i, j) = (mtop \<odot> f) (k, j)) \<and> (\<forall>k. j \<noteq> k \<longrightarrow> (mtop \<odot> f) (i, k) = bot)

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>l. f (l, k)) {l. True} = bot
[PROOF STEP]
by (simp add: top_comp_linorder_matrix)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>l. f (l, k)) {l. True} = bot

goal (1 subgoal):
 1. \<And>i k. j \<noteq> k \<Longrightarrow> f (i, k) = bot
[PROOF STEP]
thus "f (i,k) = bot"
[PROOF STATE]
proof (prove)
using this:
sup_monoid.sum (\<lambda>l. f (l, k)) {l. True} = bot

goal (1 subgoal):
 1. f (i, k) = bot
[PROOF STEP]
by (metis bot.extremum_uniqueI comp_inf.ub_sum)
[PROOF STATE]
proof (state)
this:
f (i, k) = bot

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i k. j \<noteq> k \<longrightarrow> f (i, k) = bot

goal (1 subgoal):
 1. \<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
have "(\<Squnion>\<^sub>k f (i,k)) \<noteq> bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} \<noteq> bot
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<forall>j. (f \<odot> mtop) (i, j) \<noteq> bot \<and> (\<forall>k. (f \<odot> mtop) (i, j) = (f \<odot> mtop) (i, k)) \<and> (\<forall>k. i \<noteq> k \<longrightarrow> (f \<odot> mtop) (k, j) = bot)

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} \<noteq> bot
[PROOF STEP]
by (simp add: comp_top_linorder_matrix)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} \<noteq> bot

goal (1 subgoal):
 1. \<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
hence 4: "f (i,j) \<noteq> bot"
[PROOF STATE]
proof (prove)
using this:
sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} \<noteq> bot

goal (1 subgoal):
 1. f (i, j) \<noteq> bot
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} \<noteq> bot
\<forall>i k. j \<noteq> k \<longrightarrow> f (i, k) = bot

goal (1 subgoal):
 1. f (i, j) \<noteq> bot
[PROOF STEP]
by (metis linorder_finite_sup_selective)
[PROOF STATE]
proof (state)
this:
f (i, j) \<noteq> bot

goal (1 subgoal):
 1. \<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
have "\<forall>k l . k \<noteq> i \<or> l \<noteq> j \<longrightarrow> f (k,l) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k l. k \<noteq> i \<or> l \<noteq> j \<longrightarrow> f (k, l) = bot
[PROOF STEP]
proof (intro allI, unfold imp_disjL, rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k l. k \<noteq> i \<longrightarrow> f (k, l) = bot
 2. \<And>k l. l \<noteq> j \<longrightarrow> f (k, l) = bot
[PROOF STEP]
fix k l
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k l. k \<noteq> i \<longrightarrow> f (k, l) = bot
 2. \<And>k l. l \<noteq> j \<longrightarrow> f (k, l) = bot
[PROOF STEP]
show "k \<noteq> i \<longrightarrow> f (k,l) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<noteq> i \<longrightarrow> f (k, l) = bot
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> f (k, l) = bot
[PROOF STEP]
assume "k \<noteq> i"
[PROOF STATE]
proof (state)
this:
k \<noteq> i

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> f (k, l) = bot
[PROOF STEP]
hence "(\<Squnion>\<^sub>m f (k,m)) = bot"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> i

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>m. f (k, m)) {m. True} = bot
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
k \<noteq> i
\<forall>j. (f \<odot> mtop) (i, j) \<noteq> bot \<and> (\<forall>k. (f \<odot> mtop) (i, j) = (f \<odot> mtop) (i, k)) \<and> (\<forall>k. i \<noteq> k \<longrightarrow> (f \<odot> mtop) (k, j) = bot)

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>m. f (k, m)) {m. True} = bot
[PROOF STEP]
by (simp add: comp_top_linorder_matrix)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>m. f (k, m)) {m. True} = bot

goal (1 subgoal):
 1. k \<noteq> i \<Longrightarrow> f (k, l) = bot
[PROOF STEP]
thus "f (k,l) = bot"
[PROOF STATE]
proof (prove)
using this:
sup_monoid.sum (\<lambda>m. f (k, m)) {m. True} = bot

goal (1 subgoal):
 1. f (k, l) = bot
[PROOF STEP]
by (metis bot.extremum_uniqueI comp_inf.ub_sum)
[PROOF STATE]
proof (state)
this:
f (k, l) = bot

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k \<noteq> i \<longrightarrow> f (k, l) = bot

goal (1 subgoal):
 1. \<And>k l. l \<noteq> j \<longrightarrow> f (k, l) = bot
[PROOF STEP]
show "l \<noteq> j \<longrightarrow> f (k,l) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<noteq> j \<longrightarrow> f (k, l) = bot
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
\<forall>i k. j \<noteq> k \<longrightarrow> f (i, k) = bot

goal (1 subgoal):
 1. l \<noteq> j \<longrightarrow> f (k, l) = bot
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l \<noteq> j \<longrightarrow> f (k, l) = bot

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>k l. k \<noteq> i \<or> l \<noteq> j \<longrightarrow> f (k, l) = bot

goal (1 subgoal):
 1. \<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>k l. k \<noteq> i \<or> l \<noteq> j \<longrightarrow> f (k, l) = bot

goal (1 subgoal):
 1. \<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
\<forall>k l. k \<noteq> i \<or> l \<noteq> j \<longrightarrow> f (k, l) = bot
f (i, j) \<noteq> bot

goal (1 subgoal):
 1. \<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
[PROOF STEP]
by (metis old.prod.exhaust)
[PROOF STATE]
proof (state)
this:
\<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pp_arc_linorder_matrix:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.pp_arc f \<longleftrightarrow> (\<exists>e . f e \<noteq> bot \<and> (\<forall>d . e \<noteq> d \<longrightarrow> f d = bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.pp_arc f = (\<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot))
[PROOF STEP]
using pp_arc_linorder_matrix_1 pp_arc_linorder_matrix_2
[PROOF STATE]
proof (prove)
using this:
matrix_stone_relation_algebra.pp_arc ?f \<Longrightarrow> \<exists>e. ?f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> ?f d = bot)
\<exists>e. ?f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> ?f d = bot) \<Longrightarrow> matrix_stone_relation_algebra.pp_arc ?f

goal (1 subgoal):
 1. matrix_stone_relation_algebra.pp_arc f = (\<exists>e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot))
[PROOF STEP]
by blast


[STATEMENT]
lemma pp_arc_linorder_matrix_unique:
  fixes f :: "('a::finite,'b::non_trivial_linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.pp_arc f \<longleftrightarrow> (\<exists>!e . f e \<noteq> bot \<and> (\<forall>d . e \<noteq> d \<longrightarrow> f d = bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.pp_arc f = (\<exists>!e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot))
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. matrix_stone_relation_algebra.pp_arc f \<Longrightarrow> \<exists>!e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot)
 2. \<exists>!e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot) \<Longrightarrow> matrix_stone_relation_algebra.pp_arc f
[PROOF STEP]
apply (metis (no_types, opaque_lifting) pp_arc_linorder_matrix)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot) \<Longrightarrow> matrix_stone_relation_algebra.pp_arc f
[PROOF STEP]
using pp_arc_linorder_matrix
[PROOF STATE]
proof (prove)
using this:
matrix_stone_relation_algebra.pp_arc ?f = (\<exists>e. ?f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> ?f d = bot))

goal (1 subgoal):
 1. \<exists>!e. f e \<noteq> bot \<and> (\<forall>d. e \<noteq> d \<longrightarrow> f d = bot) \<Longrightarrow> matrix_stone_relation_algebra.pp_arc f
[PROOF STEP]
by blast


[STATEMENT]
lemma reflexive_linorder_matrix_1:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_idempotent_semiring.reflexive f"
    shows "f (i,i) = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (i, i) = top
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (i, i) = top
[PROOF STEP]
have "(top::'b) = mone (i,i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. top = mone (i, i)
[PROOF STEP]
by (simp add: one_matrix_def)
[PROOF STATE]
proof (state)
this:
top = mone (i, i)

goal (1 subgoal):
 1. f (i, i) = top
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
top = mone (i, i)

goal (1 subgoal):
 1. f (i, i) = top
[PROOF STEP]
have "... \<le> f (i,i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mone (i, i) \<le> f (i, i)
[PROOF STEP]
using assms less_eq_matrix_def
[PROOF STATE]
proof (prove)
using this:
matrix_idempotent_semiring.reflexive f
(?f \<preceq> ?g) = (\<forall>e. ?f e \<le> ?g e)

goal (1 subgoal):
 1. mone (i, i) \<le> f (i, i)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mone (i, i) \<le> f (i, i)

goal (1 subgoal):
 1. f (i, i) = top
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
comp_inf.reflexive (f (i, i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
comp_inf.reflexive (f (i, i))

goal (1 subgoal):
 1. f (i, i) = top
[PROOF STEP]
by (simp add: top.extremum_unique)
[PROOF STATE]
proof (state)
this:
f (i, i) = top

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reflexive_linorder_matrix_2:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "\<forall>i . f (i,i) = top"
    shows "matrix_idempotent_semiring.reflexive f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_idempotent_semiring.reflexive f
[PROOF STEP]
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e a b. mone (a, b) \<le> f (a, b)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e a b. mone (a, b) \<le> f (a, b)
[PROOF STEP]
show "mone (i,j) \<le> f (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mone (i, j) \<le> f (i, j)
[PROOF STEP]
proof (cases "i = j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = j \<Longrightarrow> mone (i, j) \<le> f (i, j)
 2. i \<noteq> j \<Longrightarrow> mone (i, j) \<le> f (i, j)
[PROOF STEP]
assume "i = j"
[PROOF STATE]
proof (state)
this:
i = j

goal (2 subgoals):
 1. i = j \<Longrightarrow> mone (i, j) \<le> f (i, j)
 2. i \<noteq> j \<Longrightarrow> mone (i, j) \<le> f (i, j)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i = j

goal (1 subgoal):
 1. mone (i, j) \<le> f (i, j)
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
mone (i, j) \<le> f (i, j)

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> mone (i, j) \<le> f (i, j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> mone (i, j) \<le> f (i, j)
[PROOF STEP]
assume "i \<noteq> j"
[PROOF STATE]
proof (state)
this:
i \<noteq> j

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> mone (i, j) \<le> f (i, j)
[PROOF STEP]
hence "(bot::'b) = mone (i,j)"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> j

goal (1 subgoal):
 1. bot = mone (i, j)
[PROOF STEP]
by (simp add: one_matrix_def)
[PROOF STATE]
proof (state)
this:
bot = mone (i, j)

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> mone (i, j) \<le> f (i, j)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
bot = mone (i, j)

goal (1 subgoal):
 1. mone (i, j) \<le> f (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mone (i, j) \<le> f (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mone (i, j) \<le> f (i, j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reflexive_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_idempotent_semiring.reflexive f \<longleftrightarrow> (\<forall>i . f (i,i) = top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_idempotent_semiring.reflexive f = (\<forall>i. f (i, i) = top)
[PROOF STEP]
using reflexive_linorder_matrix_1 reflexive_linorder_matrix_2
[PROOF STATE]
proof (prove)
using this:
matrix_idempotent_semiring.reflexive ?f \<Longrightarrow> ?f (?i, ?i) = top
\<forall>i. ?f (i, i) = top \<Longrightarrow> matrix_idempotent_semiring.reflexive ?f

goal (1 subgoal):
 1. matrix_idempotent_semiring.reflexive f = (\<forall>i. f (i, i) = top)
[PROOF STEP]
by auto


[STATEMENT]
lemma coreflexive_linorder_matrix_1:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_idempotent_semiring.coreflexive f"
      and "i \<noteq> j"
    shows "f (i,j) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (i, j) = bot
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (i, j) = bot
[PROOF STEP]
have "f (i,j) \<le> mone (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (i, j) \<le> mone (i, j)
[PROOF STEP]
using assms less_eq_matrix_def
[PROOF STATE]
proof (prove)
using this:
matrix_idempotent_semiring.coreflexive f
i \<noteq> j
(?f \<preceq> ?g) = (\<forall>e. ?f e \<le> ?g e)

goal (1 subgoal):
 1. f (i, j) \<le> mone (i, j)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f (i, j) \<le> mone (i, j)

goal (1 subgoal):
 1. f (i, j) = bot
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (i, j) \<le> mone (i, j)

goal (1 subgoal):
 1. f (i, j) = bot
[PROOF STEP]
have "... = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mone (i, j) = bot
[PROOF STEP]
by (simp add: assms one_matrix_def)
[PROOF STATE]
proof (state)
this:
mone (i, j) = bot

goal (1 subgoal):
 1. f (i, j) = bot
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f (i, j) \<le> bot
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f (i, j) \<le> bot

goal (1 subgoal):
 1. f (i, j) = bot
[PROOF STEP]
by (simp add: bot.extremum_unique)
[PROOF STATE]
proof (state)
this:
f (i, j) = bot

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coreflexive_linorder_matrix_2:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "\<forall>i j . i \<noteq> j \<longrightarrow> f (i,j) = bot"
    shows "matrix_idempotent_semiring.coreflexive f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_idempotent_semiring.coreflexive f
[PROOF STEP]
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e a b. f (a, b) \<le> mone (a, b)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e a b. f (a, b) \<le> mone (a, b)
[PROOF STEP]
show "f (i,j) \<le> mone (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (i, j) \<le> mone (i, j)
[PROOF STEP]
proof (cases "i = j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = j \<Longrightarrow> f (i, j) \<le> mone (i, j)
 2. i \<noteq> j \<Longrightarrow> f (i, j) \<le> mone (i, j)
[PROOF STEP]
assume "i = j"
[PROOF STATE]
proof (state)
this:
i = j

goal (2 subgoals):
 1. i = j \<Longrightarrow> f (i, j) \<le> mone (i, j)
 2. i \<noteq> j \<Longrightarrow> f (i, j) \<le> mone (i, j)
[PROOF STEP]
hence "(top::'b) = mone (i,j)"
[PROOF STATE]
proof (prove)
using this:
i = j

goal (1 subgoal):
 1. top = mone (i, j)
[PROOF STEP]
by (simp add: one_matrix_def)
[PROOF STATE]
proof (state)
this:
top = mone (i, j)

goal (2 subgoals):
 1. i = j \<Longrightarrow> f (i, j) \<le> mone (i, j)
 2. i \<noteq> j \<Longrightarrow> f (i, j) \<le> mone (i, j)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
top = mone (i, j)

goal (1 subgoal):
 1. f (i, j) \<le> mone (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (i, j) \<le> mone (i, j)

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> f (i, j) \<le> mone (i, j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> f (i, j) \<le> mone (i, j)
[PROOF STEP]
assume "i \<noteq> j"
[PROOF STATE]
proof (state)
this:
i \<noteq> j

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> f (i, j) \<le> mone (i, j)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<noteq> j

goal (1 subgoal):
 1. f (i, j) \<le> mone (i, j)
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
f (i, j) \<le> mone (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (i, j) \<le> mone (i, j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coreflexive_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_idempotent_semiring.coreflexive f \<longleftrightarrow> (\<forall>i j . i \<noteq> j \<longrightarrow> f (i,j) = bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_idempotent_semiring.coreflexive f = (\<forall>i j. i \<noteq> j \<longrightarrow> f (i, j) = bot)
[PROOF STEP]
using coreflexive_linorder_matrix_1 coreflexive_linorder_matrix_2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>matrix_idempotent_semiring.coreflexive ?f; ?i \<noteq> ?j\<rbrakk> \<Longrightarrow> ?f (?i, ?j) = bot
\<forall>i j. i \<noteq> j \<longrightarrow> ?f (i, j) = bot \<Longrightarrow> matrix_idempotent_semiring.coreflexive ?f

goal (1 subgoal):
 1. matrix_idempotent_semiring.coreflexive f = (\<forall>i j. i \<noteq> j \<longrightarrow> f (i, j) = bot)
[PROOF STEP]
by auto


[STATEMENT]
lemma irreflexive_linorder_matrix_1:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_stone_relation_algebra.irreflexive f"
    shows "f (i,i) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (i, i) = bot
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (i, i) = bot
[PROOF STEP]
have "(top::'b) = mone (i,i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. top = mone (i, i)
[PROOF STEP]
by (simp add: one_matrix_def)
[PROOF STATE]
proof (state)
this:
top = mone (i, i)

goal (1 subgoal):
 1. f (i, i) = bot
[PROOF STEP]
hence "(bot::'b) = (\<ominus>mone) (i,i)"
[PROOF STATE]
proof (prove)
using this:
top = mone (i, i)

goal (1 subgoal):
 1. bot = (\<ominus> mone) (i, i)
[PROOF STEP]
by (simp add: uminus_matrix_def)
[PROOF STATE]
proof (state)
this:
bot = (\<ominus> mone) (i, i)

goal (1 subgoal):
 1. f (i, i) = bot
[PROOF STEP]
hence "f (i,i) \<le> bot"
[PROOF STATE]
proof (prove)
using this:
bot = (\<ominus> mone) (i, i)

goal (1 subgoal):
 1. f (i, i) \<le> bot
[PROOF STEP]
by (metis assms less_eq_matrix_def)
[PROOF STATE]
proof (state)
this:
f (i, i) \<le> bot

goal (1 subgoal):
 1. f (i, i) = bot
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f (i, i) \<le> bot

goal (1 subgoal):
 1. f (i, i) = bot
[PROOF STEP]
by (simp add: bot.extremum_unique)
[PROOF STATE]
proof (state)
this:
f (i, i) = bot

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma irreflexive_linorder_matrix_2:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "\<forall>i . f (i,i) = bot"
    shows "matrix_stone_relation_algebra.irreflexive f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.irreflexive f
[PROOF STEP]
proof (unfold less_eq_matrix_def, rule allI, rule prod_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e a b. f (a, b) \<le> (\<ominus> mone) (a, b)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e a b. f (a, b) \<le> (\<ominus> mone) (a, b)
[PROOF STEP]
show "f (i,j) \<le> (\<ominus>mone) (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (i, j) \<le> (\<ominus> mone) (i, j)
[PROOF STEP]
proof (cases "i = j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = j \<Longrightarrow> f (i, j) \<le> (\<ominus> mone) (i, j)
 2. i \<noteq> j \<Longrightarrow> f (i, j) \<le> (\<ominus> mone) (i, j)
[PROOF STEP]
assume "i = j"
[PROOF STATE]
proof (state)
this:
i = j

goal (2 subgoals):
 1. i = j \<Longrightarrow> f (i, j) \<le> (\<ominus> mone) (i, j)
 2. i \<noteq> j \<Longrightarrow> f (i, j) \<le> (\<ominus> mone) (i, j)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i = j

goal (1 subgoal):
 1. f (i, j) \<le> (\<ominus> mone) (i, j)
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
f (i, j) \<le> (\<ominus> mone) (i, j)

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> f (i, j) \<le> (\<ominus> mone) (i, j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> f (i, j) \<le> (\<ominus> mone) (i, j)
[PROOF STEP]
assume "i \<noteq> j"
[PROOF STATE]
proof (state)
this:
i \<noteq> j

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> f (i, j) \<le> (\<ominus> mone) (i, j)
[PROOF STEP]
hence "(bot::'b) = mone (i,j)"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> j

goal (1 subgoal):
 1. bot = mone (i, j)
[PROOF STEP]
by (simp add: one_matrix_def)
[PROOF STATE]
proof (state)
this:
bot = mone (i, j)

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> f (i, j) \<le> (\<ominus> mone) (i, j)
[PROOF STEP]
hence "(top::'b) = (\<ominus>mone) (i,j)"
[PROOF STATE]
proof (prove)
using this:
bot = mone (i, j)

goal (1 subgoal):
 1. top = (\<ominus> mone) (i, j)
[PROOF STEP]
by (simp add: uminus_matrix_def)
[PROOF STATE]
proof (state)
this:
top = (\<ominus> mone) (i, j)

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> f (i, j) \<le> (\<ominus> mone) (i, j)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
top = (\<ominus> mone) (i, j)

goal (1 subgoal):
 1. f (i, j) \<le> (\<ominus> mone) (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (i, j) \<le> (\<ominus> mone) (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (i, j) \<le> (\<ominus> mone) (i, j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma irreflexive_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.irreflexive f \<longleftrightarrow> (\<forall>i . f (i,i) = bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.irreflexive f = (\<forall>i. f (i, i) = bot)
[PROOF STEP]
using irreflexive_linorder_matrix_1 irreflexive_linorder_matrix_2
[PROOF STATE]
proof (prove)
using this:
matrix_stone_relation_algebra.irreflexive ?f \<Longrightarrow> ?f (?i, ?i) = bot
\<forall>i. ?f (i, i) = bot \<Longrightarrow> matrix_stone_relation_algebra.irreflexive ?f

goal (1 subgoal):
 1. matrix_stone_relation_algebra.irreflexive f = (\<forall>i. f (i, i) = bot)
[PROOF STEP]
by auto


[STATEMENT]
lemma symmetric_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.symmetric f \<longleftrightarrow> (\<forall>i j . f (i,j) = f (j,i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.symmetric f = (\<forall>i j. f (i, j) = f (j, i))
[PROOF STEP]
by (metis (mono_tags, lifting) case_prod_conv cond_case_prod_eta conv_matrix_def conv_def)


[STATEMENT]
lemma antisymmetric_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.antisymmetric f \<longleftrightarrow> (\<forall>i j . i \<noteq> j \<longrightarrow> f (i,j) = bot \<or> f (j,i) = bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.antisymmetric f = (\<forall>i j. i \<noteq> j \<longrightarrow> f (i, j) = bot \<or> f (j, i) = bot)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.antisymmetric f = (\<forall>i j. i \<noteq> j \<longrightarrow> f (i, j) = bot \<or> f (j, i) = bot)
[PROOF STEP]
have "matrix_stone_relation_algebra.antisymmetric f \<longleftrightarrow> (\<forall>i j . i \<noteq> j \<longrightarrow> f (i,j) \<sqinter> f (j,i) \<le> bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.antisymmetric f = (\<forall>i j. i \<noteq> j \<longrightarrow> f (i, j) \<sqinter> f (j, i) \<le> bot)
[PROOF STEP]
by (simp add: conv_matrix_def inf_matrix_def less_eq_matrix_def one_matrix_def)
[PROOF STATE]
proof (state)
this:
matrix_stone_relation_algebra.antisymmetric f = (\<forall>i j. i \<noteq> j \<longrightarrow> f (i, j) \<sqinter> f (j, i) \<le> bot)

goal (1 subgoal):
 1. matrix_stone_relation_algebra.antisymmetric f = (\<forall>i j. i \<noteq> j \<longrightarrow> f (i, j) = bot \<or> f (j, i) = bot)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
matrix_stone_relation_algebra.antisymmetric f = (\<forall>i j. i \<noteq> j \<longrightarrow> f (i, j) \<sqinter> f (j, i) \<le> bot)

goal (1 subgoal):
 1. matrix_stone_relation_algebra.antisymmetric f = (\<forall>i j. i \<noteq> j \<longrightarrow> f (i, j) = bot \<or> f (j, i) = bot)
[PROOF STEP]
by (metis (no_types, opaque_lifting) inf.absorb_iff1 inf.cobounded1 inf_bot_right inf_dense)
[PROOF STATE]
proof (state)
this:
matrix_stone_relation_algebra.antisymmetric f = (\<forall>i j. i \<noteq> j \<longrightarrow> f (i, j) = bot \<or> f (j, i) = bot)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma asymmetric_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_stone_relation_algebra.asymmetric f \<longleftrightarrow> (\<forall>i j . f (i,j) = bot \<or> f (j,i) = bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.asymmetric f = (\<forall>i j. f (i, j) = bot \<or> f (j, i) = bot)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.asymmetric f = (\<forall>i j. f (i, j) = bot \<or> f (j, i) = bot)
[PROOF STEP]
have "matrix_stone_relation_algebra.asymmetric f \<longleftrightarrow> (\<forall>i j . f (i,j) \<sqinter> f (j,i) \<le> bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_stone_relation_algebra.asymmetric f = (\<forall>i j. f (i, j) \<sqinter> f (j, i) \<le> bot)
[PROOF STEP]
apply (unfold conv_matrix_def inf_matrix_def conv_def id_def bot_matrix_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>e. f e \<sqinter> (case e of (i, j) \<Rightarrow> f (j, i))) = (\<lambda>e. bot)) = (\<forall>i j. f (i, j) \<sqinter> f (j, i) \<le> bot)
[PROOF STEP]
by (metis (mono_tags, lifting) bot.extremum bot.extremum_uniqueI case_prod_conv old.prod.exhaust)
[PROOF STATE]
proof (state)
this:
matrix_stone_relation_algebra.asymmetric f = (\<forall>i j. f (i, j) \<sqinter> f (j, i) \<le> bot)

goal (1 subgoal):
 1. matrix_stone_relation_algebra.asymmetric f = (\<forall>i j. f (i, j) = bot \<or> f (j, i) = bot)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
matrix_stone_relation_algebra.asymmetric f = (\<forall>i j. f (i, j) \<sqinter> f (j, i) \<le> bot)

goal (1 subgoal):
 1. matrix_stone_relation_algebra.asymmetric f = (\<forall>i j. f (i, j) = bot \<or> f (j, i) = bot)
[PROOF STEP]
by (metis (no_types, opaque_lifting) inf.absorb_iff1 inf.cobounded1 inf_bot_right inf_dense)
[PROOF STATE]
proof (state)
this:
matrix_stone_relation_algebra.asymmetric f = (\<forall>i j. f (i, j) = bot \<or> f (j, i) = bot)

goal:
No subgoals!
[PROOF STEP]
qed