Theory More_Relation_Algebra
section ‹(More) Relation Algebra›
text ‹
This theory presents fundamental properties of relation algebras, which are not present in the AFP entry on relation algebras but could be integrated there \<^cite>‹"ArmstrongFosterStruthWeber2014"›.
Many theorems concern vectors and points.
›
theory More_Relation_Algebra
imports Relation_Algebra.Relation_Algebra_RTC Relation_Algebra.Relation_Algebra_Functions
begin
no_notation
trancl ("(_⇧+)" [1000] 999)
context relation_algebra
begin
notation
converse ("(_⇧T)" [102] 101)
abbreviation bijective
where "bijective x ≡ is_inj x ∧ is_sur x"
abbreviation reflexive
where "reflexive R ≡ 1' ≤ R"
abbreviation symmetric
where "symmetric R ≡ R = R⇧T"
abbreviation transitive
where "transitive R ≡ R;R ≤ R"
text ‹General theorems›
lemma x_leq_triple_x:
"x ≤ x;x⇧T;x"
proof -
have "x = x;1' ⋅ 1"
by simp
also have "... ≤ (x ⋅ 1;1'⇧T);(1' ⋅ x⇧T;1)"
by (rule dedekind)
also have "... = x;(x⇧T;1 ⋅ 1')"
by (simp add: inf.commute)
also have "... ≤ x;(x⇧T ⋅ 1';1⇧T);(1 ⋅ (x⇧T)⇧T;1')"
by (metis comp_assoc dedekind mult_isol)
also have "... ≤ x;x⇧T;x"
by simp
finally show ?thesis .
qed
lemma inj_triple:
assumes "is_inj x"
shows "x = x;x⇧T;x"
by (metis assms order.eq_iff inf_absorb2 is_inj_def mult_1_left mult_subdistr x_leq_triple_x)
lemma p_fun_triple:
assumes "is_p_fun x"
shows "x = x;x⇧T;x"
by (metis assms comp_assoc order.eq_iff is_p_fun_def mult_isol mult_oner x_leq_triple_x)
lemma loop_backward_forward:
"x⇧T ≤ -(1') + x"
by (metis conv_e conv_times inf.cobounded2 test_dom test_domain test_eq_conv galois_2 inf.commute
sup.commute)
lemma inj_sur_semi_swap:
assumes "is_sur z"
and "is_inj x"
shows "z ≤ y;x ⟹ x ≤ y⇧T;z"
proof -
assume "z ≤ y;x"
hence "z;x⇧T ≤ y;(x;x⇧T)"
by (metis mult_isor mult_assoc)
hence "z;x⇧T ≤ y"
using ‹is_inj x› unfolding is_inj_def
by (metis mult_isol order.trans mult_1_right)
hence "(z⇧T;z);x⇧T ≤ z⇧T;y"
by (metis mult_isol mult_assoc)
hence "x⇧T ≤ z⇧T;y"
using ‹is_sur z› unfolding is_sur_def
by (metis mult_isor order.trans mult_1_left)
thus ?thesis
using conv_iso by fastforce
qed
lemma inj_sur_semi_swap_short:
assumes "is_sur z"
and "is_inj x"
shows "z ≤ y⇧T;x ⟹ x ≤ y;z"
proof -
assume as: "z ≤ y⇧T;x"
hence "z;x⇧T ≤ y⇧T"
using ‹z ≤ y⇧T;x› ‹is_inj x› unfolding is_inj_def
by (metis assms(2) conv_invol inf.orderI inf_absorb1 inj_p_fun ss_422iii)
hence "x⇧T ≤ z⇧T;y⇧T"
using ‹is_sur z› unfolding is_sur_def
by (metis as assms inj_sur_semi_swap conv_contrav conv_invol conv_iso)
thus "x ≤ y;z"
using conv_iso by fastforce
qed
lemma bij_swap:
assumes "bijective z"
and "bijective x"
shows "z ≤ y⇧T;x ⟷ x ≤ y;z"
by (metis assms inj_sur_semi_swap conv_invol)
text ‹The following result is \<^cite>‹‹Proposition 4.2.2(iv)› in "SchmidtStroehlein1993"›.›
lemma ss422iv:
assumes "is_p_fun y"
and "x ≤ y"
and "y;1 ≤ x;1"
shows "x = y"
proof -
have "y ≤ (x;1)⋅y"
using assms(3) le_infI maddux_20 order_trans by blast
also have "... ≤ x;x⇧T;y"
by (metis inf_top_left modular_1_var comp_assoc)
also have "... ≤ x;y⇧T;y"
using assms(2) conv_iso mult_double_iso by blast
also have "... ≤ x"
using assms(1) comp_assoc is_p_fun_def mult_isol mult_1_right
by fastforce
finally show ?thesis
by (simp add: assms(2) order.antisym)
qed
text ‹The following results are variants of \<^cite>‹‹Proposition 4.2.3› in "SchmidtStroehlein1993"›.›
lemma ss423conv:
assumes "bijective x"
shows "x ; y ≤ z ⟷ y ≤ x⇧T ; z"
by (metis assms conv_contrav conv_iso inj_p_fun is_map_def ss423 sur_total)
lemma ss423bij:
assumes "bijective x"
shows "y ; x⇧T ≤ z ⟷ y ≤ z ; x"
by (simp add: assms is_map_def p_fun_inj ss423 total_sur)
lemma inj_distr:
assumes "is_inj z"
shows "(x⋅y);z = (x;z)⋅(y;z)"
apply (rule order.antisym)
using mult_subdistr_var apply blast
using assms conv_iso inj_p_fun p_fun_distl by fastforce
lemma test_converse:
"x ⋅ 1' = x⇧T ⋅ 1'"
by (metis conv_e conv_times inf_le2 is_test_def test_eq_conv)
lemma injective_down_closed:
assumes "is_inj x"
and "y ≤ x"
shows "is_inj y"
by (meson assms conv_iso dual_order.trans is_inj_def mult_isol_var)
lemma injective_sup:
assumes "is_inj t"
and "e;t⇧T ≤ 1'"
and "is_inj e"
shows "is_inj (t + e)"
proof -
have 1: "t;e⇧T ≤ 1'"
using assms(2) conv_contrav conv_e conv_invol conv_iso by fastforce
have "(t + e);(t + e)⇧T = t;t⇧T + t;e⇧T + e;t⇧T + e;e⇧T"
by (metis conv_add distrib_left distrib_right' sup_assoc)
also have "... ≤ 1'"
using 1 assms by (simp add: is_inj_def le_supI)
finally show ?thesis
unfolding is_inj_def .
qed
text ‹Some (more) results about vectors›
lemma vector_meet_comp:
assumes "is_vector v"
and "is_vector w"
shows "v;w⇧T = v⋅w⇧T"
by (metis assms conv_contrav conv_one inf_top_right is_vector_def vector_1)
lemma vector_meet_comp':
assumes "is_vector v"
shows "v;v⇧T = v⋅v⇧T"
using assms vector_meet_comp by blast
lemma vector_meet_comp_x:
"x;1;x⇧T = x;1⋅1;x⇧T"
by (metis comp_assoc inf_top.right_neutral is_vector_def one_idem_mult vector_1)
lemma vector_meet_comp_x':
"x;1;x = x;1⋅1;x"
by (metis inf_commute inf_top.right_neutral ra_1)
lemma vector_prop1:
assumes "is_vector v"
shows "-v⇧T;v = 0"
by (metis assms compl_inf_bot inf_top.right_neutral one_compl one_idem_mult vector_2)
text ‹The following results and a number of others in this theory are from \<^cite>‹"Guttmann2017a"›.›
lemma ee:
assumes "is_vector v"
and "e ≤ v;-v⇧T"
shows "e;e = 0"
proof -
have "e;v ≤ 0"
by (metis assms annir mult_isor vector_prop1 comp_assoc)
thus ?thesis
by (metis assms(2) annil order.antisym bot_least comp_assoc mult_isol)
qed
lemma et:
assumes "is_vector v"
and "e ≤ v;-v⇧T"
and "t ≤ v;v⇧T"
shows "e;t = 0"
and "e;t⇧T = 0"
proof -
have "e;t ≤ v;-v⇧T;v;v⇧T"
by (metis assms(2-3) mult_isol_var comp_assoc)
thus "e;t = 0"
by (simp add: assms(1) comp_assoc le_bot vector_prop1)
next
have "t⇧T ≤ v;v⇧T"
using assms(3) conv_iso by fastforce
hence "e;t⇧T ≤ v;-v⇧T;v;v⇧T"
by (metis assms(2) mult_isol_var comp_assoc)
thus "e;t⇧T = 0"
by (simp add: assms(1) comp_assoc le_bot vector_prop1)
qed
text ‹Some (more) results about points›
definition point
where "point x ≡ is_vector x ∧ bijective x"
lemma point_swap:
assumes "point p"
and "point q"
shows "p ≤ x;q ⟷ q ≤ x⇧T;p"
by (metis assms conv_invol inj_sur_semi_swap point_def)
text ‹Some (more) results about singletons›
abbreviation singleton
where "singleton x ≡ bijective (x;1) ∧ bijective (x⇧T;1)"
lemma singleton_injective:
assumes "singleton x"
shows "is_inj x"
using assms injective_down_closed maddux_20 by blast
lemma injective_inv:
assumes "is_vector v"
and "singleton e"
and "e ≤ v;-v⇧T"
and "t ≤ v;v⇧T"
and "is_inj t"
shows "is_inj (t + e)"
by (metis assms singleton_injective injective_sup bot_least et(2))
lemma singleton_is_point:
assumes "singleton p"
shows "point (p;1)"
by (simp add: assms comp_assoc is_vector_def point_def)
lemma singleton_transp:
assumes "singleton p"
shows "singleton (p⇧T)"
by (simp add: assms)
lemma point_to_singleton:
assumes "singleton p"
shows "singleton (1'⋅p;p⇧T)"
using assms dom_def_aux_var dom_one is_vector_def point_def by fastforce
lemma singleton_singletonT:
assumes "singleton p"
shows "p;p⇧T ≤ 1'"
using assms singleton_injective is_inj_def by blast
text ‹Minimality›
abbreviation minimum
where "minimum x v ≡ v ⋅ -(x⇧T;v)"
text ‹Regressively finite›
abbreviation regressively_finite
where "regressively_finite x ≡ ∀v . is_vector v ∧ v ≤ x⇧T;v ⟶ v = 0"
lemma regressively_finite_minimum:
"regressively_finite R ⟹ is_vector v ⟹ v ≠ 0 ⟹ minimum R v ≠ 0"
using galois_aux2 by blast
lemma regressively_finite_irreflexive:
assumes "regressively_finite x"
shows "x ≤ -1'"
proof -
have 1: "is_vector ((x⇧T ⋅ 1');1)"
by (simp add: is_vector_def mult_assoc)
have "(x⇧T ⋅ 1');1 = (x⇧T ⋅ 1');(x⇧T ⋅ 1');1"
by (simp add: is_test_def test_comp_eq_mult)
with 1 have "(x⇧T ⋅ 1');1 = 0"
by (metis assms comp_assoc mult_subdistr)
thus ?thesis
by (metis conv_e conv_invol conv_times conv_zero galois_aux ss_p18)
qed
end
subsection ‹Relation algebras satisfying the Tarski rule›
class relation_algebra_tarski = relation_algebra +
assumes tarski: "x ≠ 0 ⟷ 1;x;1 = 1"
begin
text ‹Some (more) results about points›
lemma point_equations:
assumes "is_point p"
shows "p;1=p"
and "1;p=1"
and "p⇧T;1=1"
and "1;p⇧T=p⇧T"
apply (metis assms is_point_def is_vector_def)
using assms is_point_def is_vector_def tarski vector_comp apply fastforce
apply (metis assms conv_contrav conv_one conv_zero is_point_def is_vector_def tarski)
by (metis assms conv_contrav conv_one is_point_def is_vector_def)
text ‹The following result is \<^cite>‹‹Proposition 2.4.5(i)› in "SchmidtStroehlein1993"›.›
lemma point_singleton:
assumes "is_point p"
and "is_vector v"
and "v ≠ 0"
and "v ≤ p"
shows "v = p"
proof -
have "1;v = 1"
using assms(2,3) comp_assoc is_vector_def tarski by fastforce
hence "p = 1;v ⋅ p"
by simp
also have "... ≤ (1 ⋅ p;v⇧T);(v ⋅ 1⇧T;p)"
using dedekind by blast
also have "... ≤ p;v⇧T;v"
by (simp add: mult_subdistl)
also have "... ≤ p;p⇧T;v"
using assms(4) conv_iso mult_double_iso by blast
also have "... ≤ v"
by (metis assms(1) is_inj_def is_point_def mult_isor mult_onel)
finally show ?thesis
using assms(4) by simp
qed
lemma point_not_equal_aux:
assumes "is_point p"
and "is_point q"
shows "p≠q ⟷ p ⋅ -q ≠ 0"
proof
show "p ≠ q ⟹ p ⋅ - q ≠ 0"
proof (rule contrapos_nn)
assume "p ⋅ -q = 0"
thus "p = q"
using assms galois_aux2 is_point_def point_singleton by fastforce
qed
next
show "p ⋅ - q ≠ 0 ⟹ p ≠ q"
using inf_compl_bot by blast
qed
text ‹The following result is part of \<^cite>‹‹Proposition 2.4.5(ii)› in "SchmidtStroehlein1993"›.›
lemma point_not_equal:
assumes "is_point p"
and "is_point q"
shows "p≠q ⟷ p≤-q"
and "p≤-q ⟷ p;q⇧T ≤ -1'"
and "p;q⇧T ≤ -1' ⟷ p⇧T;q ≤ 0"
proof -
have "p ≠ q ⟹ p ≤ - q"
by (metis assms point_not_equal_aux is_point_def vector_compl vector_mult point_singleton
inf.orderI inf.cobounded1)
thus "p≠q ⟷ p≤-q"
by (metis assms(1) galois_aux inf.orderE is_point_def order.refl)
next
show "(p ≤ - q) = (p ; q⇧T ≤ - 1')"
by (simp add: conv_galois_2)
next
show "(p ; q⇧T ≤ - 1') = (p⇧T ; q ≤ 0)"
by (metis assms(2) compl_bot_eq conv_galois_2 galois_aux maddux_141 mult_1_right
point_equations(4))
qed
lemma point_is_point:
"point x ⟷ is_point x"
apply (rule iffI)
apply (simp add: is_point_def point_def surj_one tarski)
using is_point_def is_vector_def mult_assoc point_def sur_def_var1 tarski by fastforce
lemma point_in_vector_or_complement:
assumes "point p"
and "is_vector v"
shows "p ≤ v ∨ p ≤ -v"
proof (cases "p ≤ -v")
assume "p ≤ -v"
thus ?thesis
by simp
next
assume "¬(p ≤ -v)"
hence "p⋅v ≠ 0"
by (simp add: galois_aux)
hence "1;(p⋅v) = 1"
using assms comp_assoc is_vector_def point_def tarski vector_mult by fastforce
hence "p ≤ p;(p⋅v)⇧T;(p⋅v)"
by (metis inf_top.left_neutral modular_2_var)
also have "... ≤ p;p⇧T;v"
by (simp add: mult_isol_var)
also have "... ≤ v"
using assms(1) comp_assoc point_def ss423conv by fastforce
finally show ?thesis ..
qed
lemma point_in_vector_or_complement_iff:
assumes "point p"
and "is_vector v"
shows "p ≤ v ⟷ ¬(p ≤ -v)"
by (metis assms annir compl_top_eq galois_aux inf.orderE one_compl point_def ss423conv tarski
top_greatest point_in_vector_or_complement)
lemma different_points_consequences:
assumes "point p"
and "point q"
and "p≠q"
shows "p⇧T;-q=1"
and "-q⇧T;p=1"
and "-(p⇧T;-q)=0"
and "-(-q⇧T;p)=0"
proof -
have "p ≤ -q"
by (metis assms compl_le_swap1 inf.absorb1 inf.absorb2 point_def point_in_vector_or_complement)
thus 1: "p⇧T;-q=1"
using assms(1) by (metis is_vector_def point_def ss423conv top_le)
thus 2: "-q⇧T;p=1"
using conv_compl conv_one by force
from 1 show "-(p⇧T;-q)=0"
by simp
from 2 show "-(-q⇧T;p)=0"
by simp
qed
text ‹Some (more) results about singletons›
lemma singleton_pq:
assumes "point p"
and "point q"
shows "singleton (p;q⇧T)"
using assms comp_assoc point_def point_equations(1,3) point_is_point by fastforce
lemma singleton_equal_aux:
assumes "singleton p"
and "singleton q"
and "q≤p"
shows "p ≤ q;1"
proof -
have pLp: "p;1;p⇧T ≤1'"
by (simp add: assms(1) maddux_21 ss423conv)
have "p = 1;(q⇧T;q;1) ⋅ p"
using tarski
by (metis assms(2) annir singleton_injective inf.commute inf_top.right_neutral inj_triple
mult_assoc surj_one)
also have "... ≤ (1 ⋅ p;(q⇧T;q;1)⇧T);(q⇧T;q;1 ⋅ 1;p)"
using dedekind by (metis conv_one)
also have "... ≤ p;1;q⇧T;q;q⇧T;q;1"
by (simp add: comp_assoc mult_isol)
also have "... ≤ p;1;p⇧T;q;q⇧T;q;1"
using assms(3) by (metis comp_assoc conv_iso mult_double_iso)
also have "... ≤ 1';q;q⇧T;q;1"
using pLp using mult_isor by blast
also have "... ≤ q;1"
using assms(2) singleton_singletonT by (simp add: comp_assoc mult_isol)
finally show ?thesis .
qed
lemma singleton_equal:
assumes "singleton p"
and "singleton q"
and "q≤p"
shows "q=p"
proof -
have p1: "p ≤ q;1"
using assms by (rule singleton_equal_aux)
have "p⇧T ≤ q⇧T;1"
using assms singleton_equal_aux singleton_transp conv_iso by fastforce
hence p2: "p ≤ 1;q"
using conv_iso by force
have "p ≤ q;1 ⋅ 1;q"
using p1 p2 inf.boundedI by blast
also have "... ≤ (q ⋅ 1;q;1);(1 ⋅ q⇧T;1;q)"
using dedekind by (metis comp_assoc conv_one)
also have "... ≤ q;q⇧T;1;q"
by (simp add: mult_isor comp_assoc)
also have "... ≤ q;1'"
by (metis assms(2) conv_contrav conv_invol conv_one is_inj_def mult_assoc mult_isol
one_idem_mult)
also have "... ≤ q"
by simp
finally have "p ≤ q" .
thus "q=p"
using assms(3) by simp
qed
lemma singleton_nonsplit:
assumes "singleton p"
and "x≤p"
shows "x=0 ∨ x=p"
proof (cases "x=0")
assume "x=0"
thus ?thesis ..
next
assume 1: "x≠0"
have "singleton x"
proof (safe)
show "is_inj (x;1)"
using assms injective_down_closed mult_isor by blast
show "is_inj (x⇧T;1)"
using assms conv_iso injective_down_closed mult_isol_var by blast
show "is_sur (x;1)"
using 1 comp_assoc sur_def_var1 tarski by fastforce
thus "is_sur (x⇧T;1)"
by (metis conv_contrav conv_one mult.semigroup_axioms sur_def_var1 semigroup.assoc)
qed
thus ?thesis
using assms singleton_equal by blast
qed
lemma singleton_nonzero:
assumes "singleton p"
shows "p≠0"
proof
assume "p = 0"
hence "point 0"
using assms singleton_is_point by fastforce
thus False
by (simp add: is_point_def point_is_point)
qed
lemma singleton_sum:
assumes "singleton p"
shows "p ≤ x+y ⟷ (p≤x ∨ p≤y)"
proof
show "p ≤ x + y ⟹ p ≤ x ∨ p ≤ y"
proof -
assume as: "p ≤ x + y"
show "p ≤ x ∨ p ≤ y"
proof (cases "p≤x")
assume "p≤x"
thus ?thesis ..
next
assume a:"¬(p≤x)"
hence "p⋅x ≠ p"
using a inf.orderI by fastforce
hence "p ≤ -x"
using assms singleton_nonsplit galois_aux inf_le1 by blast
hence "p≤y"
using as by (metis galois_1 inf.orderE)
thus ?thesis
by simp
qed
qed
next
show "p ≤ x ∨ p ≤ y ⟹ p ≤ x + y"
using sup.coboundedI1 sup.coboundedI2 by blast
qed
lemma singleton_iff:
"singleton x ⟷ x ≠ 0 ∧ x⇧T;1;x + x;1;x⇧T ≤ 1'"
by (smt comp_assoc conv_contrav conv_invol conv_one is_inj_def le_sup_iff one_idem_mult
sur_def_var1 tarski)
lemma singleton_not_atom_in_relation_algebra_tarski:
assumes "p≠0"
and "∀x . x≤p ⟶ x=0 ∨ x=p"
shows "singleton p"
nitpick [expect=genuine] oops
end
subsection ‹Relation algebras satisfying the point axiom›
class relation_algebra_point = relation_algebra +
assumes point_axiom: "x ≠ 0 ⟶ (∃y z . point y ∧ point z ∧ y;z⇧T ≤ x)"
begin
text ‹Some (more) results about points›
lemma point_exists:
"∃x . point x"
by (metis (full_types) order.eq_iff is_inj_def is_sur_def is_vector_def point_axiom point_def)
lemma point_below_vector:
assumes "is_vector v"
and "v ≠ 0"
shows "∃x . point x ∧ x ≤ v"
proof -
from assms(2) obtain y and z where 1: "point y ∧ point z ∧ y;z⇧T ≤ v"
using point_axiom by blast
have "z⇧T;1 = (1;z)⇧T"
using conv_contrav conv_one by simp
hence "y;(1;z)⇧T ≤ v"
using 1 by (metis assms(1) comp_assoc is_vector_def mult_isor)
thus ?thesis
using 1 by (metis conv_one is_vector_def point_def sur_def_var1)
qed
end
class relation_algebra_tarski_point = relation_algebra_tarski + relation_algebra_point
begin
lemma atom_is_singleton:
assumes "p≠0"
and "∀x . x≤p ⟶ x=0 ∨ x=p"
shows "singleton p"
by (metis assms singleton_nonzero singleton_pq point_axiom)
lemma singleton_iff_atom:
"singleton p ⟷ p≠0 ∧ (∀x . x≤p ⟶ x=0 ∨ x=p)"
using singleton_nonsplit singleton_nonzero atom_is_singleton by blast
lemma maddux_tarski:
assumes "x≠0"
shows "∃y . y≠0 ∧ y≤x ∧ is_p_fun y"
proof -
obtain p q where 1: "point p ∧ point q ∧ p;q⇧T ≤ x"
using assms point_axiom by blast
hence 2: "p;q⇧T≠0"
by (simp add: singleton_nonzero singleton_pq)
have "is_p_fun (p;q⇧T)"
using 1 by (meson singleton_singletonT singleton_pq singleton_transp is_inj_def p_fun_inj)
thus ?thesis
using 1 2 by force
qed
text ‹Intermediate Point Theorem \<^cite>‹‹Proposition 2.4.8› in "SchmidtStroehlein1993"››
lemma intermediate_point_theorem:
assumes "point p"
and "point r"
shows "p ≤ x;y;r ⟷ (∃q . point q ∧ p ≤ x;q ∧ q ≤ y;r)"
proof
assume 1: "p ≤ x;y;r"
let ?v = "x⇧T;p ⋅ y;r"
have 2: "is_vector ?v"
using assms comp_assoc is_vector_def point_def vector_mult by fastforce
have "?v ≠ 0"
using 1 by (metis assms(1) inf.absorb2 is_point_def maddux_141 point_is_point mult.assoc)
hence "∃q . point q ∧ q ≤ ?v"
using 2 point_below_vector by blast
thus "∃q . point q ∧ p ≤ x;q ∧ q ≤ y;r"
using assms(1) point_swap by auto
next
assume "∃q . point q ∧ p ≤ x;q ∧ q ≤ y;r"
thus "p ≤ x;y;r"
using comp_assoc mult_isol order_trans by fastforce
qed
end
context relation_algebra
begin
lemma unfoldl_inductl_implies_unfoldr:
assumes "⋀x. 1' + x;(rtc x) ≤ rtc x"
and "⋀x y z. x+y;z ≤ z ⟹ rtc(y);x ≤ z"
shows "1' + rtc(x);x ≤ rtc x"
by (metis assms le_sup_iff mult_oner order.trans subdistl_eq sup_absorb2 sup_ge1)
lemma star_transpose_swap:
assumes "⋀x. 1' + x;(rtc x) ≤ rtc x"
and "⋀x y z. x+y;z ≤ z ⟹ rtc(y);x ≤ z"
shows "rtc(x⇧T) = (rtc x)⇧T"
apply(simp only: order.eq_iff; rule conjI)
apply (metis assms conv_add conv_contrav conv_e conv_iso mult_1_right
unfoldl_inductl_implies_unfoldr )
by (metis assms conv_add conv_contrav conv_e conv_invol conv_iso mult_1_right
unfoldl_inductl_implies_unfoldr)
lemma unfoldl_inductl_implies_inductr:
assumes "⋀x. 1' + x;(rtc x) ≤ rtc x"
and "⋀x y z. x+y;z ≤ z ⟹ rtc(y);x ≤ z"
shows "x+z;y ≤ z ⟹ x;rtc(y) ≤ z"
by (metis assms conv_add conv_contrav conv_iso star_transpose_swap)
end
context relation_algebra_rtc
begin
abbreviation tc ("(_⇧+)" [101] 100) where "tc x ≡ x;x⇧⋆"
abbreviation is_acyclic
where "is_acyclic x ≡ x⇧+ ≤ -1'"
text ‹General theorems›
lemma star_denest_10:
assumes "x;y=0"
shows "(x+y)⇧⋆ = y;y⇧⋆;x⇧⋆+x⇧⋆"
using assms bubble_sort sup.commute by auto
lemma star_star_plus:
"x⇧⋆ + y⇧⋆ = x⇧+ + y⇧⋆"
by (metis (full_types) sup.left_commute star_plus_one star_unfoldl_eq sup.commute)
text ‹The following two lemmas are from \<^cite>‹"Guttmann2018b"›.›
lemma cancel_separate:
assumes "x ; y ≤ 1'"
shows "x⇧⋆ ; y⇧⋆ ≤ x⇧⋆ + y⇧⋆"
proof -
have "x ; y⇧⋆ = x + x ; y ; y⇧⋆"
by (metis comp_assoc conway.dagger_unfoldl_distr distrib_left mult_oner)
also have "... ≤ x + y⇧⋆"
by (metis assms join_isol star_invol star_plus_one star_subdist_var_2 sup.absorb2 sup.assoc)
also have "... ≤ x⇧⋆ + y⇧⋆"
using join_iso by fastforce
finally have "x ; (x⇧⋆ + y⇧⋆) ≤ x⇧⋆ + y⇧⋆"
by (simp add: distrib_left le_supI1)
thus ?thesis
by (simp add: rtc_inductl)
qed
lemma cancel_separate_inj_converse:
assumes "is_inj x"
shows "x⇧⋆ ; x⇧T⇧⋆ = x⇧⋆ + x⇧T⇧⋆"
apply (rule order.antisym)
using assms cancel_separate is_inj_def apply blast
by (metis conway.dagger_unfoldl_distr le_supI mult_1_right mult_isol sup.cobounded1)
lemma cancel_separate_p_fun_converse:
assumes "is_p_fun x"
shows "x⇧T⇧⋆ ; x⇧⋆ = x⇧⋆ + x⇧T⇧⋆"
using sup_commute assms cancel_separate_inj_converse p_fun_inj by fastforce
lemma cancel_separate_converse_idempotent:
assumes "is_inj x"
and "is_p_fun x"
shows "(x⇧⋆ + x⇧T⇧⋆);(x⇧⋆ + x⇧T⇧⋆) = x⇧⋆ + x⇧T⇧⋆"
by (metis assms cancel_separate cancel_separate_p_fun_converse church_rosser_equiv is_inj_def
star_denest_var_6)
lemma triple_star:
assumes "is_inj x"
and "is_p_fun x"
shows "x⇧⋆;x⇧T⇧⋆;x⇧⋆ = x⇧⋆ + x⇧T⇧⋆"
by (simp add: assms cancel_separate_inj_converse cancel_separate_p_fun_converse)
lemma inj_xxts:
assumes "is_inj x"
shows "x;x⇧T⇧⋆ ≤ x⇧⋆ + x⇧T⇧⋆"
by (metis assms cancel_separate_inj_converse distrib_right less_eq_def star_ext)
lemma plus_top:
"x⇧+;1 = x;1"
by (metis comp_assoc conway.dagger_unfoldr_distr sup_top_left)
lemma top_plus:
"1;x⇧+ = 1;x"
by (metis comp_assoc conway.dagger_unfoldr_distr star_denest_var_2 star_ext star_slide_var
sup_top_left top_unique)
lemma plus_conv:
"(x⇧+)⇧T = x⇧T⇧+"
by (simp add: star_conv star_slide_var)
lemma inj_implies_step_forwards_backwards:
assumes "is_inj x"
shows "x⇧⋆;(x⇧+⋅1');1 ≤ x⇧T;1"
proof -
have "(x⇧+⋅1');1 ≤ (x⇧⋆⋅x⇧T);(x⋅(x⇧⋆)⇧T);1"
by (metis conv_contrav conv_e dedekind mult_1_right mult_isor star_slide_var)
also have "... ≤ (x⇧⋆⋅x⇧T);1"
by (simp add: comp_assoc mult_isol)
finally have 1: "(x⇧+⋅1');1 ≤ (x⇧⋆⋅x⇧T);1" .
have "x;(x⇧⋆⋅x⇧T);1 ≤ (x⇧+⋅x;x⇧T);1"
by (metis inf_idem meet_interchange mult_isor)
also have "... ≤ (x⇧+⋅1');1"
using assms is_inj_def meet_isor mult_isor by fastforce
finally have "x;(x⇧⋆⋅x⇧T);1 ≤ (x⇧⋆⋅x⇧T);1"
using 1 by fastforce
hence "x⇧⋆;(x⇧+⋅1');1 ≤ (x⇧⋆⋅x⇧T);1"
using 1 by (simp add: comp_assoc rtc_inductl)
thus "x⇧⋆;(x⇧+⋅1');1 ≤ x⇧T;1"
using inf.cobounded2 mult_isor order_trans by blast
qed
text ‹Acyclic relations›
text ‹The following result is from \<^cite>‹"Guttmann2017c"›.›
lemma acyclic_inv:
assumes "is_acyclic t"
and "is_vector v"
and "e ≤ v;-v⇧T"
and "t ≤ v;v⇧T"
shows "is_acyclic (t + e)"
proof -
have "t⇧+;e ≤ t⇧+;v;-v⇧T"
by (simp add: assms(3) mult_assoc mult_isol)
also have "... ≤ v;v⇧T;t⇧⋆;v;-v⇧T"
by (simp add: assms(4) mult_isor)
also have "... ≤ v;-v⇧T"
by (metis assms(2) mult_double_iso top_greatest is_vector_def mult_assoc)
also have "... ≤ -1'"
by (simp add: conv_galois_1)
finally have 1: "t⇧+;e ≤ -1'" .
have "e ≤ v;-v⇧T"
using assms(3) by simp
also have "... ≤ -1'"
by (simp add: conv_galois_1)
finally have 2: "t⇧+;e + e ≤ -1'"
using 1 by simp
have 3: "e;t⇧⋆ = e"
by (metis assms(2-4) et(1) independence2)
have 4: "e⇧⋆ = 1' + e"
using assms(2-3) ee boffa_var bot_least by blast
have "(t + e)⇧+ = (t + e);t⇧⋆;(e;t⇧⋆)⇧⋆"
by (simp add: comp_assoc)
also have "... = (t + e);t⇧⋆;(1' + e)"
using 3 4 by simp
also have "... = t⇧+;(1' + e) + e;t⇧⋆;(1' + e)"
by simp
also have "... = t⇧+;(1' + e) + e;(1' + e)"
using 3 by simp
also have "... = t⇧+;(1' + e) + e"
using 4 assms(2-3) ee independence2 by fastforce
also have "... = t⇧+ + t⇧+;e + e"
by (simp add: distrib_left)
also have "... ≤ -1'"
using assms(1) 2 by simp
finally show ?thesis .
qed
lemma acyclic_single_step:
assumes "is_acyclic x"
shows "x ≤ -1'"
by (metis assms dual_order.trans mult_isol mult_oner star_ref)
lemma acyclic_reachable_points:
assumes "is_point p"
and "is_point q"
and "p ≤ x;q"
and "is_acyclic x"
shows "p≠q"
proof
assume "p=q"
hence "p ≤ x;q ⋅ q"
by (simp add: assms(3) order.eq_iff inf.absorb2)
also have "... = (x ⋅ 1');q"
using assms(2) inj_distr is_point_def by simp
also have "... ≤ (-1' ⋅ 1');q"
using acyclic_single_step assms(4) by (metis abel_semigroup.commute inf.abel_semigroup_axioms
meet_isor mult_isor)
also have "... = 0"
by simp
finally have "p ≤ 0" .
thus False
using assms(1) bot_unique is_point_def by blast
qed
lemma acyclic_trans:
assumes "is_acyclic x"
shows "x ≤ -(x⇧T⇧+)"
proof -
have "∃c≥x. c ≤ - (x⇧+)⇧T"
by (metis assms compl_mono conv_galois_2 conv_iso double_compl mult_onel star_1l)
thus ?thesis
by (metis dual_order.trans plus_conv)
qed
lemma acyclic_trans':
assumes "is_acyclic x"
shows "x⇧⋆ ≤ -(x⇧T⇧+)"
proof -
have "x⇧⋆ ≤ - (- (- (x⇧T ; - (- 1'))) ; (x⇧⋆)⇧T)"
by (metis assms conv_galois_1 conv_galois_2 order_trans star_trans)
then show ?thesis
by (simp add: star_conv)
qed
text ‹Regressively finite›
lemma regressively_finite_acyclic:
assumes "regressively_finite x"
shows "is_acyclic x"
proof -
have 1: "is_vector ((x⇧+ ⋅ 1');1)"
by (simp add: is_vector_def mult_assoc)
have "(x⇧+ ⋅ 1');1 = (x⇧T⇧+ ⋅ 1');1"
by (metis plus_conv test_converse)
also have "... ≤ x⇧T;(1';x⇧T⇧⋆ ⋅ x);1"
by (metis conv_invol modular_1_var mult_isor mult_oner mult_onel)
also have "... ≤ x⇧T;(1' ⋅ x⇧+);x⇧T⇧⋆;1"
by (metis comp_assoc conv_invol modular_2_var mult_isol mult_isor star_conv)
also have "... = x⇧T;(x⇧+ ⋅ 1');1"
by (metis comp_assoc conway.dagger_unfoldr_distr inf.commute sup.cobounded1 top_le)
finally have "(x⇧+ ⋅ 1');1 = 0"
using 1 assms by (simp add: comp_assoc)
thus ?thesis
by (simp add: galois_aux ss_p18)
qed
notation power (infixr "↑" 80)
lemma power_suc_below_plus:
"x ↑ Suc n ≤ x⇧+"
apply (induct n)
using mult_isol star_ref apply fastforce
by (simp add: mult_isol_var order_trans)
end
class relation_algebra_rtc_tarski = relation_algebra_rtc + relation_algebra_tarski
begin
lemma point_loop_not_acyclic:
assumes "is_point p"
and "p ≤ x ↑ Suc n ; p"
shows "¬ is_acyclic x"
proof -
have "p ≤ x⇧+ ; p"
by (meson assms dual_order.trans point_def point_is_point ss423bij power_suc_below_plus)
hence "p ; p⇧T ≤ x⇧+"
using assms(1) point_def point_is_point ss423bij by blast
thus ?thesis
using assms(1) order.trans point_not_equal(1) point_not_equal(2) by blast
qed
end
class relation_algebra_rtc_point = relation_algebra_rtc + relation_algebra_point
class relation_algebra_rtc_tarski_point = relation_algebra_rtc_tarski + relation_algebra_rtc_point +
relation_algebra_tarski_point
text ‹
Finite graphs: the axiom says the algebra has finitely many elements.
This means the relations have a finite base set.
›
class relation_algebra_rtc_tarski_point_finite = relation_algebra_rtc_tarski_point + finite
begin
text ‹For a finite acyclic relation, the powers eventually vanish.›
lemma acyclic_power_vanishes:
assumes "is_acyclic x"
shows "∃n . x ↑ Suc n = 0"
proof -
let ?n = "card { p . is_point p }"
let ?p = "x ↑ ?n"
have "?p = 0"
proof (rule ccontr)
assume "?p ≠ 0"
from this obtain p q where 1: "point p ∧ point q ∧ p;q⇧T ≤ ?p"
using point_axiom by blast
hence 2: "p ≤ ?p;q"
using point_def ss423bij by blast
have "∀n≤?n . (∃f. ∀i≤n . is_point (f i) ∧ (∀j≤i . p ≤ x↑(?n-i) ; f i ∧ f i ≤ x↑(i-j) ; f j))"
proof
fix n
show "n≤?n ⟶ (∃f. ∀i≤n . is_point (f i) ∧ (∀j≤i . p ≤ x↑(?n-i) ; f i ∧ f i ≤ x↑(i-j) ; f j))"
proof (induct n)
case 0
thus ?case
using 1 2 point_is_point by fastforce
next
case (Suc n)
fix n
assume 3: "n≤?n ⟶ (∃f . ∀i≤n . is_point (f i) ∧ (∀j≤i . p ≤ x ↑ (?n-i) ; f i ∧ f i ≤ x ↑ (i-j) ; f j))"
show "Suc n≤?n ⟶ (∃f . ∀i≤Suc n . is_point (f i) ∧ (∀j≤i . p ≤ x ↑ (?n-i) ; f i ∧ f i ≤ x ↑ (i-j) ; f j))"
proof
assume 4: "Suc n≤?n"
from this obtain f where 5: "∀i≤n . is_point (f i) ∧ (∀j≤i . p ≤ x ↑ (?n-i) ; f i ∧ f i ≤ x ↑ (i-j) ; f j)"
using 3 by auto
have "p ≤ x ↑ (?n-n) ; f n"
using 5 by blast
also have "... = x ↑ (?n-n-one_class.one) ; x ; f n"
using 4 by (metis (no_types) Suc_diff_le diff_Suc_1 diff_Suc_Suc power_Suc2)
finally obtain r where 6: "point r ∧ p ≤ x ↑ (?n-Suc n) ; r ∧ r ≤ x ; f n"
using 1 5 intermediate_point_theorem point_is_point by fastforce
let ?g = "λm . if m = Suc n then r else f m"
have "∀i≤Suc n . is_point (?g i) ∧ (∀j≤i . p ≤ x ↑ (?n-i) ; ?g i ∧ ?g i ≤ x ↑ (i-j) ; ?g j)"
proof
fix i
show "i≤Suc n ⟶ is_point (?g i) ∧ (∀j≤i . p ≤ x ↑ (?n-i) ; ?g i ∧ ?g i ≤ x ↑ (i-j) ; ?g j)"
proof (cases "i≤n")
case True
thus ?thesis
using 5 by simp
next
case False
have "is_point (?g (Suc n)) ∧ (∀j≤Suc n . p ≤ x ↑ (?n-Suc n) ; ?g (Suc n) ∧ ?g (Suc n) ≤ x ↑ (Suc n-j) ; ?g j)"
proof
show "is_point (?g (Suc n))"
using 6 point_is_point by fastforce
next
show "∀j≤Suc n . p ≤ x ↑ (?n-Suc n) ; ?g (Suc n) ∧ ?g (Suc n) ≤ x ↑ (Suc n-j) ; ?g j"
proof
fix j
show "j≤Suc n ⟶ p ≤ x ↑ (?n-Suc n) ; ?g (Suc n) ∧ ?g (Suc n) ≤ x ↑ (Suc n-j) ; ?g j"
proof
assume 7: "j≤Suc n"
show "p ≤ x ↑ (?n-Suc n) ; ?g (Suc n) ∧ ?g (Suc n) ≤ x ↑ (Suc n-j) ; ?g j"
proof
show "p ≤ x ↑ (?n-Suc n) ; ?g (Suc n)"
using 6 by simp
next
show "?g (Suc n) ≤ x ↑ (Suc n-j) ; ?g j"
proof (cases "j = Suc n")
case True
thus ?thesis
by simp
next
case False
hence "f n ≤ x ↑ (n-j) ; f j"
using 5 7 by fastforce
hence "x ; f n ≤ x ↑ (Suc n-j) ; f j"
using 7 False Suc_diff_le comp_assoc mult_isol by fastforce
thus ?thesis
using 6 False by fastforce
qed
qed
qed
qed
qed
thus ?thesis
by (simp add: False le_Suc_eq)
qed
qed
thus "∃f . ∀i≤Suc n . is_point (f i) ∧ (∀j≤i . p ≤ x ↑ (?n-i) ; f i ∧ f i ≤ x ↑ (i-j) ; f j)"
by auto
qed
qed
qed
from this obtain f where 8: "∀i≤?n . is_point (f i) ∧ (∀j≤i . p ≤ x ↑ (?n-i) ; f i ∧ f i ≤ x ↑ (i-j) ; f j)"
by fastforce
let ?A = "{ k . k≤?n }"
have "f ` ?A ⊆ { p . is_point p }"
using 8 by blast
hence "card (f ` ?A) ≤ ?n"
by (simp add: card_mono)
hence "¬ inj_on f ?A"
by (simp add: pigeonhole)
from this obtain i j where 9: "i ≤ ?n ∧ j ≤ ?n ∧ i ≠ j ∧ f i = f j"
by (metis (no_types, lifting) inj_on_def mem_Collect_eq)
show False
apply (cases "i < j")
using 8 9 apply (metis Suc_diff_le Suc_leI assms diff_Suc_Suc order_less_imp_le
point_loop_not_acyclic)
using 8 9 by (metis assms neqE point_loop_not_acyclic Suc_diff_le Suc_leI assms diff_Suc_Suc
order_less_imp_le)
qed
thus ?thesis
by (metis annir power.simps(2))
qed
text ‹Hence finite acyclic relations are regressively finite.›
lemma acyclic_regressively_finite:
assumes "is_acyclic x"
shows "regressively_finite x"
proof
have "is_acyclic (x⇧T)"
using assms acyclic_trans' compl_le_swap1 order_trans star_ref by blast
from this obtain n where 1: "x⇧T ↑ Suc n = 0"
using acyclic_power_vanishes by fastforce
fix v
show "is_vector v ∧ v ≤ x⇧T;v ⟶ v = 0"
proof
assume 2: "is_vector v ∧ v ≤ x⇧T;v"
have "v ≤ x⇧T ↑ Suc n ; v"
proof (induct n)
case 0
thus ?case
using 2 by simp
next
case (Suc n)
hence "x⇧T ; v ≤ x⇧T ↑ Suc (Suc n) ; v"
by (simp add: comp_assoc mult_isol)
thus ?case
using 2 dual_order.trans by blast
qed
thus "v = 0"
using 1 by (simp add: le_bot)
qed
qed
lemma acyclic_is_regressively_finite:
"is_acyclic x ⟷ regressively_finite x"
using acyclic_regressively_finite regressively_finite_acyclic by blast
end
end