Theory Relation_Algebra_Tests
section ‹Tests›
theory Relation_Algebra_Tests
imports Relation_Algebra
begin
subsection ‹Tests›
text ‹Tests or subidentities provide another way of modelling sets. Once more
we prove the basic properties, most of which stem from Maddux's book.›
context relation_algebra
begin
definition is_test :: "'a ⇒ bool"
where "is_test x ≡ x ≤ 1'"
lemma test_conv: "is_test x ⟹ is_test (x⇧⌣)"
by (metis conv_e conv_iso is_test_def)
lemma test_conv_var: "is_test x ⟹ x⇧⌣ ≤ 1'"
by (metis test_conv is_test_def)
lemma test_eq_conv [simp]: "is_test x ⟹ x⇧⌣ = x"
proof (rule order.antisym)
assume hyp: "is_test x"
hence "x ≤ x ; (1' ⋅ x⇧⌣ ; 1')"
by (metis inf.commute inf_absorb2 inf_le2 modular_1' mult.right_neutral is_test_def)
thus "x ≤ x⇧⌣"
by (metis comp_unitr conv_contrav conv_invol order.eq_iff hyp inf_absorb2 mult_subdistl test_conv_var)
thus "x⇧⌣ ≤ x"
by (metis conv_invol conv_times le_iff_inf)
qed
lemma test_sum: "⟦is_test x; is_test y⟧ ⟹ is_test (x + y)"
by (simp add: is_test_def)
lemma test_prod: "⟦is_test x; is_test y⟧ ⟹ is_test (x ⋅ y)"
by (metis le_infI2 is_test_def)
lemma test_comp: "⟦is_test x; is_test y⟧ ⟹ is_test (x ; y)"
by (metis mult_isol comp_unitr order_trans is_test_def)
lemma test_comp_eq_mult:
assumes "is_test x"
and "is_test y"
shows "x ; y = x ⋅ y"
proof (rule order.antisym)
show "x ; y ≤ x ⋅ y"
by (metis assms comp_unitr inf_absorb2 le_inf_iff mult_onel mult_subdistl mult_subdistr is_test_def)
next
have "x ⋅ y ≤ x ; (1' ⋅ x⇧⌣ ; y)"
by (metis comp_unitr modular_1_var)
thus "x ⋅ y ≤ x ; y"
by (metis assms(1) inf_absorb2 le_infI2 mult.left_neutral mult_isol mult_subdistr order_trans test_eq_conv is_test_def)
qed
lemma test_1 [simp]: "is_test x ⟹ x ; 1 ⋅ y = x ; y"
by (metis inf.commute inf.idem inf_absorb2 mult.left_neutral one_conv ra_1 test_comp_eq_mult test_eq_conv is_test_def)
lemma maddux_32 [simp]: "is_test x ⟹ -(x ; 1) ⋅ 1' = -x ⋅ 1'"
proof (rule order.antisym)
assume "is_test x"
show "-(x ; 1) ⋅ 1' ≤ -x ⋅ 1'"
by (metis maddux_20 comp_anti inf.commute meet_isor)
next
assume "is_test x"
have one: "x ; 1 ⋅ (-x ⋅ 1') ≤ x ; x⇧⌣ ; (-x ⋅ 1')"
by (metis maddux_16 inf_top_left mult.assoc)
hence two: "x ; 1 ⋅ (-x ⋅ 1') ≤ -x"
by (metis inf.commute inf_le1 le_infE)
hence "x ; 1 ⋅ (-x ⋅ 1') ≤ x"
by (metis one inf.commute le_infE meet_iso one_conv ‹is_test x› order.eq_iff test_1 test_eq_conv)
hence "x ; 1 ⋅ (-x ⋅ 1') = 0"
by (metis two galois_aux2 le_iff_inf)
thus "-x ⋅ 1' ≤ -(x ; 1) ⋅ 1'"
by (metis double_compl galois_aux2 inf.commute inf_le1 le_inf_iff)
qed
lemma test_distr_1 :
assumes "is_test x"
and "is_test y"
shows "x ; z ⋅ y ; z = (x ⋅ y) ; z"
proof (rule order.antisym)
have "x ; z ⋅ y ; z ≤ x ; 1 ⋅ y ; z"
by (metis inf_top_left meet_iso mult_subdistl)
also have "… = x ; y ; z"
by (metis assms(1) mult.assoc test_1)
finally show "x ; z ⋅ y ; z ≤ (x ⋅ y) ; z"
by (metis assms test_comp_eq_mult)
next
show "(x ⋅ y) ; z ≤ x ; z ⋅ y ; z"
by (metis mult_subdistr_var)
qed
lemma maddux_35: "is_test x ⟹ x ; y ⋅ -z = x ; y ⋅ -(x ; z)"
proof (rule order.antisym)
assume "is_test x"
show "x ; y ⋅ -z ≤ x ; y ⋅ -(x ; z)"
by (metis ‹is_test x› comp_anti mult_isor mult_onel is_test_def inf.commute inf_le2 le_infI le_infI1)
have one: "x ; y ⋅ -(x ; z) ≤ x ; (y ⋅ -z)"
by (metis order.eq_iff le_infE maddux_23)
hence two: "x ; y ⋅ -(x ; z) ≤ x ; y"
by (metis inf_le1)
have "x ; y ⋅ -(x ; z) ≤ x ; -z"
using one
by (metis galois_1 le_iff_sup distrib_left sup_compl_top sup_top_right)
hence "x ; y ⋅ -(x ; z) ≤ -z"
by (metis ‹is_test x› mult_isor mult_onel is_test_def order_trans)
thus "x ; y ⋅ -(x ; z) ≤ x ; y ⋅ -z"
using two
by (metis le_inf_iff)
qed
subsection ‹Test Complements›
text ‹Text complements are complements of elements that are ``pushed below''
the multiplicative unit.›
definition tc :: "'a ⇒ 'a"
where "tc x = 1' ⋅ -x"
lemma test_compl_1 [simp]: "is_test x ⟹ x + tc x = 1'"
by (metis is_test_def local.aux4 local.inf.absorb_iff1 local.inf_commute tc_def)
lemma test_compl_2 [simp]: "is_test x ⟹ x ⋅ tc x = 0"
by (metis galois_aux inf.commute inf_le2 tc_def)
lemma test_test_compl: "is_test x ⟹ is_test (tc x)"
by (simp add: is_test_def tc_def)
lemma test_compl_de_morgan_1: "tc (x + y) = tc x ⋅ tc y"
by (metis compl_sup inf.left_commute inf.left_idem meet_assoc tc_def)
lemma test_compl_de_morgan_2: "tc (x ⋅ y) = tc x + tc y"
by (metis compl_inf inf_sup_distrib1 tc_def)
lemma test_compl_three [simp]: "tc (tc (tc x)) = tc x"
by (metis aux4 aux6 de_morgan_3 inf.commute inf_sup_absorb tc_def)
lemma test_compl_double [simp]: "is_test x ⟹ tc (tc x) = x"
by (metis aux6_var compl_inf double_compl inf.commute le_iff_inf tc_def is_test_def)
end
end