theory CadeInsa imports Main "Relation_Algebra/Relation_Algebra" "Relation_Algebra/Relation_Algebra_Functions" "Relation_Algebra/Relation_Algebra_Models" begin context relation_algebra begin (* definitions/predicates *) definition symmetric :: "'a \ bool" where "symmetric x \ x=x\<^sup>\" definition reflexive :: "'a \ bool" where "reflexive x \ 1' \ x" definition irreflexive :: "'a \ bool" where "irreflexive x \ x \ -(1')" (* the used libraries use different notation. We adapted the notions to fit our paper in case the definitions are slightly different, we show equivalence *) definition univalent :: "'a \ bool" where "univalent x \ x\<^sup>\;x \ 1'" lemma "univalent x = is_p_fun x" by(simp add: univalent_def is_p_fun_def) definition total :: "'a \ bool" where "total x \ x;1=1" lemma total_is_total: "total x = is_total x" by (simp add: total_def total_def_var_1) definition is_function :: "'a \ bool" where "is_function x \ univalent x \ total x" lemma "is_function x = is_map x" by (simp add: is_function_def is_map_def is_p_fun_def total_def_var_1 total_def univalent_def) definition injective :: "'a \ bool" where "injective x \ univalent (x\<^sup>\)" lemma "injective x = is_inj x" unfolding injective_def is_inj_def univalent_def by(simp) definition surjective :: "'a \ bool" where "surjective x \ total (x\<^sup>\)" lemma "surjective x = is_sur x" by(simp add: surjective_def total_is_total is_total_def is_sur_def) definition coloringProperty where "coloringProperty x e \ x;x\<^sup>\ \ -e" lemmas unfold_defs = symmetric_def reflexive_def irreflexive_def univalent_def total_def is_function_def injective_def surjective_def coloringProperty_def is_p_fun_def is_point_def is_vector_def is_inj_def (* end definitions *) (* logical equivalences in the model of relations *) lemma rel_subset: "(\ x y. (x,y) \ r \ (x,y) \ s) = (r \ s)" by(auto) lemma rel_reflexive: "(\ x. (x,x) \ r) = (Id \ r)" by(simp add: subset_iff) lemma rel_irreflexive: "(\ x y. (x,y) \ r \ x \ y) = (r \ -Id)" by(auto) lemma rel_transitive: "(\ x y z. ((x,y) \ r \ (y,z) \ r) \ (x,z) \ r) = (r O r \ r)" by(auto) lemma rel_symmetric: "(\ x y. (x,y) \ r \ (y,x) \ r) = (r = r\)" by(auto simp add: subset_iff) lemma rel_antisymmetric: "(\ x y. (x,y) \ r \ (y,x) \ r \ x=y) = (r \ r\ \ Id)" by(simp add: subset_iff) lemma rel_asymmetric: "(\ x y. (x,y) \ r \ (y,x) \ r) = (r \ r\ = {})" by(auto simp add: subset_iff) lemma rel_total: "(\ x y. (x,y) \ r \ (y,x) \ r) = (UNIV = r \ r\)" by(auto simp add: subset_iff) (*end logical equivalences in the model of relations *) (* main lemmata of the paper *) lemma lemma31: "univalent 0 \ coloringProperty 0 e" by(simp add: univalent_def coloringProperty_def) lemma lemma32: assumes "univalent x" and "is_point p" and "is_point q" and "p \ -(x;1)" shows "univalent(x + p;q\<^sup>\)" proof (simp add: unfold_defs distrib_left distrib_right, safe) (* after unfolding sledgehammer is impressive *) from assms(1) show "x\<^sup>\ ; x \ 1'" by(unfold univalent_def) from assms(4) show goal2: "q ; p\<^sup>\ ; x \ 1'" by (metis compl_bot_eq compl_le_swap1 conv_galois_1 conv_galois_2 conv_one double_compl inf.boundedE inf_compl_bot mult_assoc) from goal2 show "x\<^sup>\ ; (p ; q\<^sup>\) \ 1'" by (metis conv_contrav conv_invol conv_iso mult_oner) from assms(3) and assms(4) show "q;p\<^sup>\;(p;q\<^sup>\) \ 1'" unfolding unfold_defs by (metis dual_order.trans mult_isol mult_isor top_greatest mult_assoc) qed lemma lemma33: assumes "symmetric e" and "irreflexive e" and "is_point p" and "is_point q" and "coloringProperty x e" and "q \ -(x\<^sup>\ ; e ; p)" shows "coloringProperty (x + p;q\<^sup>\) e" proof (simp add: unfold_defs distrib_left distrib_right, safe) show goal1: "x ; x\<^sup>\ \ -e" by (metis assms(5) coloringProperty_def) from assms(1) and assms(6) show goal3: "p ; q\<^sup>\ ; x\<^sup>\ \ - e" by (metis symmetric_def comp_anti conv_galois_1 conv_galois_2 double_compl mult_assoc) from goal3 show "x ; (q ; p\<^sup>\) \ - e" by (metis assms(6) conv_galois_1 conv_galois_2 conv_invol double_compl) from assms(2) and assms(3) and assms(4) show "p ; q\<^sup>\ ; (q ; p\<^sup>\) \ -e" unfolding unfold_defs by (metis dual_order.trans mult_isol mult_isor top_greatest mult_assoc compl_le_swap1) qed lemma lemma21: "\ is_point p ; is_point q ; (\ x. (x\0 \ 1 ; x ; 1 = 1)) \ \ p\0 \ p;q\<^sup>\ \ 0" unfolding unfold_defs by (metis mult_assoc sur_def_var1 sur_total total_1) lemma lemma34: assumes "is_point p" and "is_point q" and "x;1\1" and "p \ -(x;1)" and "\ x. (x\0 \ 1 ; x ; 1 = 1)" shows "x \ x + p;q\<^sup>\ \ x \ x + p;q\<^sup>\ " proof show "x \ x + p;q\<^sup>\" by simp from assms have temp: "p;q\<^sup>\ \ -x" unfolding is_point_def is_vector_def is_inj_def by (metis comp_anti comp_res_aux compl_bot_eq conv_galois_1 conv_galois_2 double_compl le_iff_inf order_trans top_greatest) { assume "x = x + p;q\<^sup>\" (* proof by contradiction *) with assms(1) and assms(2) and assms(5) have "False" by (metis aux6 inf.orderE inf_compl_bot temp lemma21) } then show "x \ x + p;q\<^sup>\" by blast qed end end