Theory Relation_Algebra_Functions
section ‹Functions›
theory Relation_Algebra_Functions
imports Relation_Algebra_Vectors Relation_Algebra_Tests
begin
subsection ‹Functions›
text ‹This section collects the most important properties of functions. Most
of them can be found in the books by Maddux and by Schmidt and Str\"ohlein. The
main material is on partial and total functions, injections, surjections,
bijections.›
context relation_algebra
begin
definition is_p_fun :: "'a ⇒ bool"
where "is_p_fun x ≡ x⇧⌣ ; x ≤ 1'"
definition is_total :: "'a ⇒ bool"
where "is_total x ≡ 1' ≤ x ; x⇧⌣"
definition is_map :: "'a ⇒ bool"
where "is_map x ≡ is_p_fun x ∧ is_total x"
definition is_inj :: "'a ⇒ bool"
where "is_inj x ≡ x ; x⇧⌣ ≤ 1'"
definition is_sur :: "'a ⇒ bool"
where "is_sur x ≡ 1' ≤ x⇧⌣ ; x"
text ‹We distinguish between partial and total bijections. As usual we call
the latter just bijections.›
definition is_p_bij :: "'a ⇒ bool"
where "is_p_bij x ≡ is_p_fun x ∧ is_inj x ∧ is_sur x"
definition is_bij :: "'a ⇒ bool"
where "is_bij x ≡ is_map x ∧ is_inj x ∧ is_sur x"
text ‹Our first set of lemmas relates the various concepts.›
lemma inj_p_fun: "is_inj x ⟷ is_p_fun (x⇧⌣)"
by (metis conv_invol is_inj_def is_p_fun_def)
lemma p_fun_inj: "is_p_fun x ⟷ is_inj (x⇧⌣)"
by (metis conv_invol inj_p_fun)
lemma sur_total: "is_sur x ⟷ is_total (x⇧⌣)"
by (metis conv_invol is_sur_def is_total_def)
lemma total_sur: "is_total x ⟷ is_sur (x⇧⌣)"
by (metis conv_invol sur_total)
lemma bij_conv: "is_bij x ⟷ is_bij (x⇧⌣)"
by (metis is_bij_def inj_p_fun is_map_def p_fun_inj sur_total total_sur)
text ‹Next we show that tests are partial injections.›
lemma test_is_inj_fun: "is_test x ⟹ (is_p_fun x ∧ is_inj x)"
by (metis is_inj_def p_fun_inj test_comp test_eq_conv is_test_def)
text ‹Next we show composition properties.›
lemma p_fun_comp:
assumes "is_p_fun x" and "is_p_fun y"
shows "is_p_fun (x ; y)"
proof (unfold is_p_fun_def)
have "(x ; y)⇧⌣ ; x ; y = y⇧⌣ ; x⇧⌣ ; x ; y"
by (metis conv_contrav mult.assoc)
also have "... ≤ y⇧⌣ ; y"
by (metis assms(1) is_p_fun_def mult_double_iso mult.right_neutral mult.assoc)
finally show "(x ; y)⇧⌣ ; (x ; y) ≤ 1'"
by (metis assms(2) order_trans is_p_fun_def mult.assoc)
qed
lemma p_fun_mult_var: "x⇧⌣ ; x ≤ 1' ⟹ (x ⋅ y)⇧⌣ ; (x ⋅ y) ≤ 1'"
by (metis conv_times inf_le1 mult_isol_var order_trans)
lemma inj_compose:
assumes "is_inj x" and "is_inj y"
shows "is_inj (x ; y)"
by (metis assms conv_contrav inj_p_fun p_fun_comp)
lemma inj_mult_var: "x⇧⌣ ; x ≤ 1' ⟹ (x ⋅ y)⇧⌣ ; (x ⋅ y) ≤ 1'"
by (metis p_fun_mult_var)
lemma total_comp:
assumes "is_total x" and "is_total y"
shows "is_total (x ; y)"
by (metis assms inf_top_left le_iff_inf mult.assoc mult.right_neutral one_conv ra_2 is_total_def)
lemma total_add_var: "1' ≤ x⇧⌣ ; x ⟹ 1' ≤ (x + y)⇧⌣ ; (x + y)"
by (metis local.conv_add local.inf.absorb2 local.inf.coboundedI1 local.join_interchange local.le_sup_iff)
lemma sur_comp:
assumes "is_sur x" and "is_sur y"
shows "is_sur (x ; y)"
by (metis assms conv_contrav sur_total total_comp)
lemma sur_sum_var: "1' ≤ x⇧⌣ ; x ⟹ 1' ≤ (x + y)⇧⌣ ; (x + y)"
by (metis total_add_var)
lemma map_comp:
assumes "is_map x" and "is_map y"
shows "is_map (x ; y)"
by (metis assms is_map_def p_fun_comp total_comp)
lemma bij_comp:
assumes "is_bij x" and "is_bij y"
shows "is_bij (x ; y)"
by (metis assms is_bij_def inj_compose map_comp sur_comp)
text ‹We now show that (partial) functions, unlike relations, distribute over
meets from the left.›
lemma p_fun_distl: "is_p_fun x ⟹ x ; (y ⋅ z) = x ; y ⋅ x ; z"
proof -
assume "is_p_fun x"
hence "x ; (z ⋅ ((x⇧⌣ ; x) ; y)) ≤ x ; (z ⋅ y)"
by (metis is_p_fun_def inf_le1 le_infI le_infI2 mult_isol mult_isor mult_onel)
hence "x ; y ⋅ x ; z ≤ x ; (z ⋅ y)"
by (metis inf.commute mult.assoc order_trans modular_1_var)
thus "x ; (y ⋅ z) = x ; y ⋅ x ; z"
by (metis order.eq_iff inf.commute le_infI mult_subdistl)
qed
lemma map_distl: "is_map x ⟹ x ; (y ⋅ z) = x ; y ⋅ x ; z"
by (metis is_map_def p_fun_distl)
text ‹Next we prove simple properties of functions which arise in equivalent
definitions of those concepts.›
lemma p_fun_zero: "is_p_fun x ⟹ x ; y ⋅ x ; -y = 0"
by (metis annir inf_compl_bot p_fun_distl)
lemma total_one: "is_total x ⟹ x ; 1 = 1"
by (metis conv_invol conv_one inf_top_left le_iff_inf mult.right_neutral one_conv ra_2 is_total_def)
lemma total_1: "is_total x ⟹ (∀y. y ; x = 0 ⟶ y = 0)"
by (metis conv_invol conv_zero inf_bot_left inf_top_left peirce total_one)
lemma surj_one: "is_sur x ⟹ 1 ; x = 1"
by (metis conv_contrav conv_invol conv_one sur_total total_one)
lemma surj_1: "is_sur x ⟹ (∀y. x ; y = 0 ⟶ y = 0)"
by (metis comp_res_aux compl_bot_eq conv_contrav conv_one inf.commute inf_top_right surj_one)
lemma bij_is_maprop:
assumes "is_bij x" and "is_map x"
shows "x⇧⌣ ; x = 1' ∧ x ; x⇧⌣ = 1'"
by (metis assms is_bij_def order.eq_iff is_inj_def is_map_def is_p_fun_def is_sur_def is_total_def)
text‹We now provide alternative definitions for functions. These can be found
in Schmidt and Str\"ohlein's book.›
lemma p_fun_def_var: "is_p_fun x ⟷ x ; -(1') ≤ -x"
by (metis conv_galois_1 double_compl galois_aux inf.commute is_p_fun_def)
lemma total_def_var_1: "is_total x ⟷ x ; 1 = 1"
by (metis inf_top_right le_iff_inf one_conv total_one is_total_def)
lemma total_def_var_2: "is_total x ⟷ -x ≤ x ; -(1')"
by (metis total_def_var_1 distrib_left sup_compl_top mult.right_neutral galois_aux3)
lemma sur_def_var1: "is_sur x ⟷ 1 ; x = 1"
by (metis conv_contrav conv_one sur_total surj_one total_def_var_1)
lemma sur_def_var2: "is_sur x ⟷ -x ≤ -(1') ; x"
by (metis sur_total total_def_var_2 conv_compl conv_contrav conv_e conv_iso)
lemma inj_def_var1: "is_inj x ⟷ -(1') ; x ≤ -x"
by (metis conv_galois_2 double_compl galois_aux inf.commute is_inj_def)
lemma is_maprop: "is_map x ⟷ x ; -(1') = -x"
by (metis order.eq_iff is_map_def p_fun_def_var total_def_var_2)
text ‹Finally we prove miscellaneous properties of functions.›
lemma ss_422iii: "is_p_fun y ⟹ (x ⋅ z ; y⇧⌣) ; y = x ; y ⋅ z"
proof (rule order.antisym)
assume "is_p_fun y"
show "x ; y ⋅ z ≤ (x ⋅ z ; y⇧⌣) ; y"
by (metis maddux_17)
have "(x ⋅ z ; y⇧⌣) ; y ≤ x ; y ⋅ (z ; (y⇧⌣ ; y))"
by (metis mult_subdistr_var mult.assoc)
also have "… ≤ x ; y ⋅ z ; 1'"
by (metis ‹is_p_fun y› inf_absorb2 inf_le1 le_infI le_infI2 mult_subdistl is_p_fun_def)
finally show "(x ⋅ z ; y⇧⌣) ; y ≤ x ; y ⋅ z"
by (metis mult.right_neutral)
qed
lemma p_fun_compl: "is_p_fun x ⟹ x ; -y ≤ -(x; y)"
by (metis annir galois_aux inf.commute inf_compl_bot p_fun_distl)
lemma ss_422v: "is_p_fun x ⟹ x ; -y = x ; 1 ⋅ -(x ; y)"
by (metis inf.commute inf_absorb2 inf_top_left maddux_23 p_fun_compl)
text ‹The next property is a Galois connection.›
lemma ss43iii: "is_map x ⟷ (∀y. x ; -y = -(x ; y))"
by standard (metis inf_top_left is_map_def ss_422v total_one, metis is_maprop mult.right_neutral)
text ‹Next we prove a lemma from Schmidt and Str\"ohlein's book and some of
its consequences. We show the proof in detail since the textbook proof uses
Tarski's rule which we omit.›
lemma ss423: "is_map x ⟹ y ; x ≤ z ⟷ y ≤ z ; x⇧⌣"
proof
assume "is_map x" and "y ; x ≤ z"
hence "y ≤ y ; x ; x⇧⌣"
by (metis is_map_def mult_1_right mult.assoc mult_isol is_total_def)
thus "y ≤ z ; x⇧⌣"
by (metis ‹y ; x ≤ z› mult_isor order_trans)
next
assume "is_map x" and "y ≤ z ; x⇧⌣"
hence "y ; x ≤ z ; x⇧⌣ ; x"
by (metis mult_isor)
also have "… ≤ z ; 1'"
by (metis ‹is_map x› is_map_def mult.assoc mult_isol is_p_fun_def)
finally show "y ; x ≤ z"
by (metis mult_1_right)
qed
lemma ss424i: "is_total x ⟷ (∀y. -(x ; y) ≤ x ; -y)"
by (metis galois_aux3 distrib_left sup_compl_top total_def_var_1)
lemma ss434ii: "is_p_fun x ⟷ (∀y. x ; -y ≤ -(x ; y))"
by (metis mult.right_neutral p_fun_compl p_fun_def_var)
lemma is_maprop1: "is_map x ⟹ (y ≤ x ; z ; x⇧⌣ ⟷ y ; x ≤ x ; z)"
by (metis ss423)
lemma is_maprop2: "is_map x ⟹ (y ; x ≤ x ; z ⟷ x⇧⌣ ; y; x ≤ z)"
by standard (metis galois_aux2 inf_commute mult.assoc schroeder_1 ss43iii, metis conv_contrav conv_invol conv_iso mult.assoc ss423)
lemma is_maprop3: "is_map x ⟹ (x⇧⌣ ; y; x ≤ z ⟷ x⇧⌣ ; y ≤ z ; x⇧⌣)"
by (metis ss423)
lemma p_fun_sur_id [simp]:
assumes "is_p_fun x" and "is_sur x"
shows "x⇧⌣ ; x = 1'"
by (metis assms order.eq_iff is_p_fun_def is_sur_def)
lemma total_inj_id [simp]:
assumes "is_total x" and "is_inj x"
shows "x ; x⇧⌣ = 1'"
by (metis assms conv_invol inj_p_fun p_fun_sur_id sur_total)
lemma bij_inv_1 [simp]: "is_bij x ⟹ x ; x⇧⌣ = 1'"
by (metis bij_is_maprop is_bij_def)
lemma bij_inv_2 [simp]: "is_bij x ⟹ x⇧⌣ ; x = 1'"
by (metis bij_is_maprop is_bij_def)
lemma bij_inv_comm: "is_bij x ⟹ x ; x⇧⌣ = x⇧⌣ ; x"
by (metis bij_inv_1 bij_inv_2)
lemma is_bijrop: "is_bij x ⟹ (y = x ; z ⟷ z = x⇧⌣ ; y)"
by (metis bij_inv_1 bij_inv_2 mult.assoc mult.left_neutral)
lemma inj_map_monomorph: "⟦is_inj x; is_map x⟧ ⟹ (∀y z. y ; x = z ; x ⟶ y = z)"
by (metis is_map_def mult.assoc mult.right_neutral total_inj_id)
lemma sur_map_epimorph: "⟦is_sur x; is_map x⟧ ⟹ (∀y z. x ; y = x ; z ⟶ y = z)"
by (metis order.eq_iff mult.assoc mult.left_neutral ss423 is_sur_def)
subsection ‹Points and Rectangles›
text ‹Finally here is a section on points and rectangles. This is only a
beginning.›
definition is_point :: "'a ⇒ bool"
where "is_point x ≡ is_vector x ∧ is_inj x ∧ x ≠ 0"
definition is_rectangle :: "'a ⇒ bool"
where "is_rectangle x ≡ x ; 1 ; x ≤ x"
lemma rectangle_eq [simp]: "is_rectangle x ⟷ x ; 1 ; x = x"
by (metis conv_one dedekind order.eq_iff inf_top_left mult.assoc one_idem_mult is_rectangle_def)
subsection ‹Antidomain›
text‹This section needs to be linked with domain semirings. We essentially
prove the antidomain semiring axioms. Then we have the abstract properties at
our disposition.›
definition antidom :: "'a ⇒ 'a" (‹a›)
where "a x = 1' ⋅ (-(x ; 1))"
definition dom :: "'a ⇒ 'a" (‹d›)
where "d x = a (a x)"
lemma antidom_test_comp [simp]: "a x = tc (x ; 1)"
by (metis antidom_def tc_def)
lemma dom_def_aux: "d x = 1' ⋅ x ; 1"
by (metis antidom_test_comp dom_def double_compl inf_top_left mult.left_neutral one_compl ra_1 tc_def)
lemma dom_def_aux_var: "d x = 1' ⋅ x ; x⇧⌣"
by (metis dom_def_aux one_conv)
lemma antidom_dom [simp]: "a (d x) = a x"
by (metis antidom_test_comp dom_def_aux inf_top_left mult.left_neutral ra_1)
lemma dom_antidom [simp]: "d (a x) = a x"
by (metis antidom_dom dom_def)
lemma dom_verystrict: "d x = 0 ⟷ x = 0"
using dom_def_aux_var local.schroeder_2 by force
lemma a_1 [simp]: "a x ; x = 0"
by (metis antidom_test_comp galois_aux2 maddux_20 mult.left_neutral one_compl ra_1 tc_def)
lemma a_2: "a (x ; y) = a (x ; d y)"
by (metis antidom_test_comp dom_def_aux inf_top_left mult.assoc mult.left_neutral ra_1)
lemma a_3 [simp]: "a x + d x = 1'"
by (metis antidom_def aux4 dom_def_aux double_compl)
lemma test_domain: "x = d x ⟷ x ≤ 1'"
apply standard
apply (metis dom_def_aux inf_le1)
apply (metis dom_def_aux inf.commute mult.right_neutral test_1 is_test_def)
done
text ‹At this point we have all the necessary ingredients to prove that
relation algebras form Boolean domain semirings. However, we omit a formal
proof since we haven't formalized the latter.›
lemma dom_one: "x ; 1 = d x ; 1"
by (metis dom_def_aux inf_top_left mult.left_neutral ra_1)
lemma test_dom: "is_test (d x)"
by (metis dom_def_aux inf_le1 is_test_def)
lemma p_fun_dom: "is_p_fun (d x)"
by (metis test_dom test_is_inj_fun)
lemma inj_dom: "is_inj (d x)"
by (metis test_dom test_is_inj_fun)
lemma total_alt_def: "is_total x ⟷ (d x) = 1'"
by (metis dom_def_aux_var le_iff_inf is_total_def)
end
end