Theory KAT_and_DRA.Conway_Tests
section ‹Pre-Conway Algebra with Tests›
theory Conway_Tests
imports Kleene_Algebra.Conway Test_Dioid
begin
class near_conway_zerol_tests = near_conway_zerol + test_near_semiring_zerol_distrib
begin
lemma n_preserve1_var: "n x ⋅ y ≤ n x ⋅ y ⋅ n x ⟹ n x ⋅ (n x ⋅ y + t x ⋅ z)⇧† ≤ (n x ⋅ y)⇧† ⋅ n x"
proof -
assume a: "n x ⋅ y ≤ n x ⋅ y ⋅ n x"
have "n x ⋅ (n x ⋅ y + t x ⋅ z) = n x ⋅ y"
by (metis (no_types) local.add_zeror local.annil local.n_left_distrib local.n_mult_idem local.test_mult_comp mult_assoc)
hence "n x ⋅ (n x ⋅ y + t x ⋅ z) ≤ n x ⋅ y ⋅ n x"
by (simp add: a)
thus " n x ⋅ (n x ⋅ y + t x ⋅ z)⇧† ≤ (n x ⋅ y)⇧† ⋅ n x"
by (simp add: local.dagger_simr)
qed
lemma test_preserve1_var: "test p ⟹ p ⋅ x ≤ p ⋅ x ⋅ p ⟹ p ⋅ (p ⋅ x + !p ⋅ y)⇧† ≤ (p ⋅ x)⇧† ⋅ p"
by (metis local.test_double_comp_var n_preserve1_var)
end
class test_pre_conway = pre_conway + test_pre_dioid_zerol
begin
subclass near_conway_zerol_tests
by (unfold_locales)
lemma test_preserve: "test p ⟹ p ⋅ x ≤ p ⋅ x ⋅ p ⟹ p ⋅ x⇧† = (p ⋅ x)⇧† ⋅ p"
using local.preservation1_eq local.test_restrictr by auto
lemma test_preserve1: "test p ⟹ p ⋅ x ≤ p ⋅ x ⋅ p ⟹ p ⋅ (p ⋅ x + !p ⋅ y)⇧† = (p ⋅ x)⇧† ⋅ p"
proof (rule order.antisym)
assume a: "test p"
and b: "p ⋅ x ≤ p ⋅ x ⋅ p"
hence "p ⋅ (p ⋅ x + !p ⋅ y) ≤ (p ⋅ x) ⋅ p"
by (metis local.add_0_right local.annil local.n_left_distrib_var local.test_comp_mult2 local.test_mult_idem_var mult_assoc)
thus "p ⋅ (p ⋅ x + !p ⋅ y)⇧† ≤ (p ⋅ x)⇧† ⋅ p"
using local.dagger_simr by blast
next
assume a: "test p"
and b: "p ⋅ x ≤ p ⋅ x ⋅ p"
hence "(p ⋅ x)⇧† ⋅ p = p ⋅ (p ⋅ x ⋅ p)⇧†"
by (metis dagger_slide local.test_mult_idem_var mult_assoc)
also have "... = p ⋅ (p ⋅ x)⇧†"
by (metis a b local.order.antisym local.test_restrictr)
finally show "(p ⋅ x)⇧† ⋅ p ≤ p ⋅ (p ⋅ x + !p ⋅ y)⇧†"
by (simp add: a local.dagger_iso local.test_mult_isol)
qed
lemma test_preserve2: "test p ⟹ p ⋅ x ⋅ p = p ⋅ x ⟹ p ⋅ (p ⋅ x + !p ⋅ y)⇧† ≤ x⇧†"
by (metis (no_types) local.eq_refl local.test_restrictl test_preserve test_preserve1)
end
end