Theory Domain_Semiring
section ‹Domain Semirings›
theory Domain_Semiring
imports Kleene_Algebra.Kleene_Algebra
begin
subsection ‹Domain Semigroups and Domain Monoids›
class domain_op =
fixes domain_op :: "'a ⇒ 'a" (‹d›)
text ‹First we define the class of domain semigroups. Axioms are taken from~\<^cite>‹"DesharnaisJipsenStruth"›.›
class domain_semigroup = semigroup_mult + domain_op +
assumes dsg1 [simp]: "d x ⋅ x = x"
and dsg2 [simp]: "d (x ⋅ d y) = d (x ⋅ y)"
and dsg3 [simp]: "d (d x ⋅ y) = d x ⋅ d y"
and dsg4: "d x ⋅ d y = d y ⋅ d x"
begin
lemma domain_invol [simp]: "d (d x) = d x"
proof -
have "d (d x) = d (d (d x ⋅ x))"
by simp
also have "... = d (d x ⋅ d x)"
using dsg3 by presburger
also have "... = d (d x ⋅ x)"
by simp
finally show ?thesis
by simp
qed
text ‹The next lemmas show that domain elements form semilattices.›
lemma dom_el_idem [simp]: "d x ⋅ d x = d x"
proof -
have "d x ⋅ d x = d (d x ⋅ x)"
using dsg3 by presburger
thus ?thesis
by simp
qed
lemma dom_mult_closed [simp]: "d (d x ⋅ d y) = d x ⋅ d y"
by simp
lemma dom_lc3 [simp]: "d x ⋅ d (x ⋅ y) = d (x ⋅ y)"
proof -
have "d x ⋅ d (x ⋅ y) = d (d x ⋅ x ⋅ y)"
using dsg3 mult_assoc by presburger
thus ?thesis
by simp
qed
lemma d_fixpoint: "(∃y. x = d y) ⟷ x = d x"
by auto
lemma d_type: "∀P. (∀x. x = d x ⟶ P x) ⟷ (∀x. P (d x))"
by (metis domain_invol)
text ‹We define the semilattice ordering on domain semigroups and explore the semilattice of domain elements from the order point of view.›
definition ds_ord :: "'a ⇒ 'a ⇒ bool" (infix ‹⊑› 50) where
"x ⊑ y ⟷ x = d x ⋅ y"
lemma ds_ord_refl: "x ⊑ x"
by (simp add: ds_ord_def)
lemma ds_ord_trans: "x ⊑ y ⟹ y ⊑ z ⟹ x ⊑ z"
proof -
assume "x ⊑ y" and a: "y ⊑ z"
hence b: "x = d x ⋅ y"
using ds_ord_def by blast
hence "x = d x ⋅ d y ⋅ z"
using a ds_ord_def mult_assoc by force
also have "... = d (d x ⋅ y) ⋅ z"
by simp
also have "... = d x ⋅ z"
using b by auto
finally show ?thesis
using ds_ord_def by blast
qed
lemma ds_ord_antisym: "x ⊑ y ⟹ y ⊑ x ⟹ x = y"
proof -
assume a: "x ⊑ y" and "y ⊑ x"
hence b: "y = d y ⋅ x"
using ds_ord_def by auto
have "x = d x ⋅ d y ⋅ x"
using a b ds_ord_def mult_assoc by force
also have "... = d y ⋅ x"
by (metis (full_types) b dsg3 dsg4)
thus ?thesis
using b calculation by presburger
qed
text ‹This relation is indeed an order.›
sublocale ds: ordering ‹(⊑)› ‹λx y. x ⊑ y ∧ x ≠ y›
proof
show ‹x ⊑ y ∧ x ≠ y ⟷ x ⊑ y ∧ x ≠ y› for x y
by (rule refl)
show "x ⊑ x" for x
by (rule ds_ord_refl)
show "x ⊑ y ⟹ y ⊑ z ⟹ x ⊑ z" for x y z
by (rule ds_ord_trans)
show "x ⊑ y ⟹ y ⊑ x ⟹ x = y" for x y
by (rule ds_ord_antisym)
qed
declare ds.refl [simp]
lemma ds_ord_eq: "x ⊑ d x ⟷ x = d x"
by (simp add: ds_ord_def)
lemma "x ⊑ y ⟹ z ⋅ x ⊑ z ⋅ y"
oops
lemma ds_ord_iso_right: "x ⊑ y ⟹ x ⋅ z ⊑ y ⋅ z"
proof -
assume "x ⊑ y"
hence a: "x = d x ⋅ y"
by (simp add: ds_ord_def)
hence "x ⋅ z = d x ⋅ y ⋅ z"
by auto
also have "... = d (d x ⋅ y ⋅ z) ⋅ d x ⋅ y ⋅ z"
using dsg1 mult_assoc by presburger
also have "... = d (x ⋅ z) ⋅ d x ⋅ y ⋅ z"
using a by presburger
finally show ?thesis
using ds_ord_def dsg4 mult_assoc by auto
qed
text ‹The order on domain elements could as well be defined based on multiplication/meet.›
lemma ds_ord_sl_ord: "d x ⊑ d y ⟷ d x ⋅ d y = d x"
using ds_ord_def by auto
lemma ds_ord_1: "d (x ⋅ y) ⊑ d x"
by (simp add: ds_ord_sl_ord dsg4)
lemma ds_subid_aux: "d x ⋅ y ⊑ y"
by (simp add: ds_ord_def mult_assoc)
lemma "y ⋅ d x ⊑ y"
oops
lemma ds_dom_iso: "x ⊑ y ⟹ d x ⊑ d y"
proof -
assume "x ⊑ y"
hence "x = d x ⋅ y"
by (simp add: ds_ord_def)
hence "d x = d (d x ⋅ y)"
by presburger
also have "... = d x ⋅ d y"
by simp
finally show ?thesis
using ds_ord_sl_ord by auto
qed
lemma ds_dom_llp: "x ⊑ d y ⋅ x ⟷ d x ⊑ d y"
proof
assume "x ⊑ d y ⋅ x"
hence "x = d y ⋅ x"
by (simp add: ds_subid_aux ds.antisym)
hence "d x = d (d y ⋅ x)"
by presburger
thus "d x ⊑ d y"
using ds_ord_sl_ord dsg4 by force
next
assume "d x ⊑ d y"
thus "x ⊑ d y ⋅ x"
by (metis (no_types) ds_ord_iso_right dsg1)
qed
lemma ds_dom_llp_strong: "x = d y ⋅ x ⟷ d x ⊑ d y"
using ds.eq_iff
by (simp add: ds_dom_llp ds.eq_iff ds_subid_aux)
definition refines :: "'a ⇒ 'a ⇒ bool"
where "refines x y ≡ d y ⊑ d x ∧ (d y) ⋅ x ⊑ y"
lemma refines_refl: "refines x x"
using refines_def by simp
lemma refines_trans: "refines x y ⟹ refines y z ⟹ refines x z"
unfolding refines_def
by (metis domain_invol ds.trans dsg1 dsg3 ds_ord_def)
lemma refines_antisym: "refines x y ⟹ refines y x ⟹ x = y"
apply (rule ds.antisym)
apply (simp_all add: refines_def)
apply (metis ds_dom_llp_strong)
apply (metis ds_dom_llp_strong)
done
sublocale ref: ordering "refines" "λx y. (refines x y ∧ x ≠ y)"
proof
show "⋀x y. refines x y ∧ x ≠ y ⟷ refines x y ∧ x ≠ y"
..
show "⋀x. refines x x"
by (rule refines_refl)
show "⋀x y z. refines x y ⟹ refines y z ⟹ refines x z"
by (rule refines_trans)
show "⋀x y. refines x y ⟹ refines y x ⟹ x = y"
by (rule refines_antisym)
qed
end
text ‹We expand domain semigroups to domain monoids.›
class domain_monoid = monoid_mult + domain_semigroup
begin
lemma dom_one [simp]: "d 1 = 1"
proof -
have "1 = d 1 ⋅ 1"
using dsg1 by presburger
thus ?thesis
by simp
qed
lemma ds_subid_eq: "x ⊑ 1 ⟷ x = d x"
by (simp add: ds_ord_def)
end
subsection ‹Domain Near-Semirings›
text ‹The axioms for domain near-semirings are taken from~\<^cite>‹"DesharnaisStruthAMAST"›.›
class domain_near_semiring = ab_near_semiring + plus_ord + domain_op +
assumes dns1 [simp]: "d x ⋅ x = x"
and dns2 [simp]: "d (x ⋅ d y) = d(x ⋅ y)"
and dns3 [simp]: "d (x + y) = d x + d y"
and dns4: "d x ⋅ d y = d y ⋅ d x"
and dns5 [simp]: "d x ⋅ (d x + d y) = d x"
begin
text ‹Domain near-semirings are automatically dioids; addition is idempotent.›
subclass near_dioid
proof
show "⋀x. x + x = x"
proof -
fix x
have a: "d x = d x ⋅ d (x + x)"
using dns3 dns5 by presburger
have "d (x + x) = d (x + x + (x + x)) ⋅ d (x + x)"
by (metis (no_types) dns3 dns4 dns5)
hence "d (x + x) = d (x + x) + d (x + x)"
by simp
thus "x + x = x"
by (metis a dns1 dns4 distrib_right')
qed
qed
text ‹Next we prepare to show that domain near-semirings are domain semigroups.›
lemma dom_iso: "x ≤ y ⟹ d x ≤ d y"
using order_prop by auto
lemma dom_add_closed [simp]: "d (d x + d y) = d x + d y"
proof -
have "d (d x + d y) = d (d x) + d (d y)"
by simp
thus ?thesis
by (metis dns1 dns2 dns3 dns4)
qed
lemma dom_absorp_2 [simp]: "d x + d x ⋅ d y = d x"
proof -
have "d x + d x ⋅ d y = d x ⋅ d x + d x ⋅ d y"
by (metis add_idem' dns5)
also have "... = (d x + d y) ⋅ d x"
by (simp add: dns4)
also have "... = d x ⋅ (d x + d y)"
by (metis dom_add_closed dns4)
finally show ?thesis
by simp
qed
lemma dom_1: "d (x ⋅ y) ≤ d x"
proof -
have "d (x ⋅ y) = d (d x ⋅ d (x ⋅ y))"
by (metis dns1 dns2 mult_assoc)
also have "... ≤ d (d x) + d (d x ⋅ d (x ⋅ y))"
by simp
also have "... = d (d x + d x ⋅ d (x ⋅ y))"
using dns3 by presburger
also have "... = d (d x)"
by simp
finally show ?thesis
by (metis dom_add_closed add_idem')
qed
lemma dom_subid_aux2: "d x ⋅ y ≤ y"
proof -
have "d x ⋅ y ≤ d (x + d y) ⋅ y"
by (simp add: mult_isor)
also have "... = (d x + d (d y)) ⋅ d y ⋅ y"
using dns1 dns3 mult_assoc by presburger
also have "... = (d y + d y ⋅ d x) ⋅ y"
by (simp add: dns4 add_commute)
finally show ?thesis
by simp
qed
lemma dom_glb: "d x ≤ d y ⟹ d x ≤ d z ⟹ d x ≤ d y ⋅ d z"
by (metis dns5 less_eq_def mult_isor)
lemma dom_glb_eq: "d x ≤ d y ⋅ d z ⟷ d x ≤ d y ∧ d x ≤ d z"
proof -
have "d x ≤ d z ⟶ d x ≤ d z"
by meson
then show ?thesis
by (metis (no_types) dom_absorp_2 dom_glb dom_subid_aux2 local.dual_order.trans local.join.sup.coboundedI2)
qed
lemma dom_ord: "d x ≤ d y ⟷ d x ⋅ d y = d x"
proof
assume "d x ≤ d y"
hence "d x + d y = d y"
by (simp add: less_eq_def)
thus "d x ⋅ d y = d x"
by (metis dns5)
next
assume "d x ⋅ d y = d x"
thus "d x ≤ d y"
by (metis dom_subid_aux2)
qed
lemma dom_export [simp]: "d (d x ⋅ y) = d x ⋅ d y"
proof (rule order.antisym)
have "d (d x ⋅ y) = d (d (d x ⋅ y)) ⋅ d (d x ⋅ y)"
using dns1 by presburger
also have "... = d (d x ⋅ d y) ⋅ d (d x ⋅ y)"
by (metis dns1 dns2 mult_assoc)
finally show a: "d (d x ⋅ y) ≤ d x ⋅ d y"
by (metis (no_types) dom_add_closed dom_glb dom_1 add_idem' dns2 dns4)
have "d (d x ⋅ y) = d (d x ⋅ y) ⋅ d x"
using a dom_glb_eq dom_ord by force
hence "d x ⋅ d y = d (d x ⋅ y) ⋅ d y"
by (metis dns1 dns2 mult_assoc)
thus "d x ⋅ d y ≤ d (d x ⋅ y)"
using a dom_glb_eq dom_ord by auto
qed
subclass domain_semigroup
by (unfold_locales, auto simp: dns4)
text ‹We compare the domain semigroup ordering with that of the dioid.›
lemma d_two_orders: "d x ⊑ d y ⟷ d x ≤ d y"
by (simp add: dom_ord ds_ord_sl_ord)
lemma two_orders: "x ⊑ y ⟹ x ≤ y"
by (metis dom_subid_aux2 ds_ord_def)
lemma "x ≤ y ⟹ x ⊑ y"
oops
text ‹Next we prove additional properties.›
lemma dom_subdist: "d x ≤ d (x + y)"
by simp
lemma dom_distrib: "d x + d y ⋅ d z = (d x + d y) ⋅ (d x + d z)"
proof -
have "(d x + d y) ⋅ (d x + d z) = d x ⋅ (d x + d z) + d y ⋅ (d x + d z)"
using distrib_right' by blast
also have "... = d x + (d x + d z) ⋅ d y"
by (metis (no_types) dns3 dns5 dsg4)
also have "... = d x + d x ⋅ d y + d z ⋅ d y"
using add_assoc' distrib_right' by presburger
finally show ?thesis
by (simp add: dsg4)
qed
lemma dom_llp1: "x ≤ d y ⋅ x ⟹ d x ≤ d y"
proof -
assume "x ≤ d y ⋅ x"
hence "d x ≤ d (d y ⋅ x)"
using dom_iso by blast
also have "... = d y ⋅ d x"
by simp
finally show "d x ≤ d y"
by (simp add: dom_glb_eq)
qed
lemma dom_llp2: "d x ≤ d y ⟹ x ≤ d y ⋅ x"
using d_two_orders local.ds_dom_llp two_orders by blast
lemma dom_llp: "x ≤ d y ⋅ x ⟷ d x ≤ d y"
using dom_llp1 dom_llp2 by blast
end
text ‹We expand domain near-semirings by an additive unit, using slightly different axioms.›
class domain_near_semiring_one = ab_near_semiring_one + plus_ord + domain_op +
assumes dnso1 [simp]: "x + d x ⋅ x = d x ⋅ x"
and dnso2 [simp]: "d (x ⋅ d y) = d (x ⋅ y)"
and dnso3 [simp]: "d x + 1 = 1"
and dnso4 [simp]: "d (x + y) = d x + d y"
and dnso5: "d x ⋅ d y = d y ⋅ d x"
begin
text ‹The previous axioms are derivable.›
subclass domain_near_semiring
proof
show a: "⋀x. d x ⋅ x = x"
by (metis add_commute local.dnso3 local.distrib_right' local.dnso1 local.mult_onel)
show "⋀x y. d (x ⋅ d y) = d (x ⋅ y)"
by simp
show "⋀x y. d (x + y) = d x + d y"
by simp
show "⋀x y. d x ⋅ d y = d y ⋅ d x"
by (simp add: dnso5)
show "⋀x y. d x ⋅ (d x + d y) = d x"
proof -
fix x y
have "⋀x. 1 + d x = 1"
using add_commute dnso3 by presburger
thus "d x ⋅ (d x + d y) = d x"
by (metis (no_types) a dnso2 dnso4 dnso5 distrib_right' mult_onel)
qed
qed
subclass domain_monoid ..
lemma dom_subid: "d x ≤ 1"
by (simp add: less_eq_def)
end
text ‹We add a left unit of multiplication.›
class domain_near_semiring_one_zerol = ab_near_semiring_one_zerol + domain_near_semiring_one +
assumes dnso6 [simp]: "d 0 = 0"
begin
lemma domain_very_strict: "d x = 0 ⟷ x = 0"
by (metis annil dns1 dnso6)
lemma dom_weakly_local: "x ⋅ y = 0 ⟷ x ⋅ d y = 0"
proof -
have "x ⋅ y = 0 ⟷ d (x ⋅ y) = 0"
by (simp add: domain_very_strict)
also have "... ⟷ d (x ⋅ d y) = 0"
by simp
finally show ?thesis
using domain_very_strict by blast
qed
end
subsection ‹Domain Pre-Dioids›
text ‹
Pre-semirings with one and a left zero are automatically dioids.
Hence there is no point defining domain pre-semirings separately from domain dioids. The axioms
are once again from~\<^cite>‹"DesharnaisStruthAMAST"›.
›
class domain_pre_dioid_one = pre_dioid_one + domain_op +
assumes dpd1 : "x ≤ d x ⋅ x"
and dpd2 [simp]: "d (x ⋅ d y) = d (x ⋅ y)"
and dpd3 [simp]: "d x ≤ 1"
and dpd4 [simp]: "d (x + y) = d x + d y"
begin
text ‹We prepare to show that every domain pre-dioid with one is a domain near-dioid with one.›
lemma dns1'' [simp]: "d x ⋅ x = x"
proof (rule order.antisym)
show "d x ⋅ x ≤ x"
using dpd3 mult_isor by fastforce
show "x ≤ d x ⋅ x "
by (simp add: dpd1)
qed
lemma d_iso: "x ≤ y ⟹ d x ≤ d y"
by (metis dpd4 less_eq_def)
lemma domain_1'': "d (x ⋅ y) ≤ d x"
proof -
have "d (x ⋅ y) = d (x ⋅ d y)"
by simp
also have "... ≤ d (x ⋅ 1)"
by (meson d_iso dpd3 mult_isol)
finally show ?thesis
by simp
qed
lemma domain_export'' [simp]: "d (d x ⋅ y) = d x ⋅ d y"
proof (rule order.antisym)
have one: "d (d x ⋅ y) ≤ d x"
by (metis dpd2 domain_1'' mult_onel)
have two: "d (d x ⋅ y) ≤ d y"
using d_iso dpd3 mult_isor by fastforce
have "d (d x ⋅ y) = d (d (d x ⋅ y)) ⋅ d (d x ⋅ y)"
by simp
also have "... = d (d x ⋅ y) ⋅ d (d x ⋅ y)"
by (metis dns1'' dpd2 mult_assoc)
thus "d (d x ⋅ y) ≤ d x ⋅ d y"
using mult_isol_var one two by force
next
have "d x ⋅ d y ≤ 1"
by (metis dpd3 mult_1_right mult_isol order.trans)
thus "d x ⋅ d y ≤ d (d x ⋅ y)"
by (metis dns1'' dpd2 mult_isol mult_oner)
qed
lemma dom_subid_aux1'': "d x ⋅ y ≤ y"
proof -
have "d x ⋅ y ≤ 1 ⋅ y"
using dpd3 mult_isor by blast
thus ?thesis
by simp
qed
lemma dom_subid_aux2'': "x ⋅ d y ≤ x"
using dpd3 mult_isol by fastforce
lemma d_comm: "d x ⋅ d y = d y ⋅ d x"
proof (rule order.antisym)
have "d x ⋅ d y = (d x ⋅ d y) ⋅ (d x ⋅ d y)"
by (metis dns1'' domain_export'')
thus "d x ⋅ d y ≤ d y ⋅ d x"
by (metis dom_subid_aux1'' dom_subid_aux2'' mult_isol_var)
next
have "d y ⋅ d x = (d y ⋅ d x) ⋅ (d y ⋅ d x)"
by (metis dns1'' domain_export'')
thus "d y ⋅ d x ≤ d x ⋅ d y"
by (metis dom_subid_aux1'' dom_subid_aux2'' mult_isol_var)
qed
subclass domain_near_semiring_one
by (unfold_locales, auto simp: d_comm local.join.sup.absorb2)
lemma domain_subid: "x ≤ 1 ⟹ x ≤ d x"
by (metis dns1 mult_isol mult_oner)
lemma d_preserves_equation: "d y ⋅ x ≤ x ⋅ d z ⟷ d y ⋅ x = d y ⋅ x ⋅ d z"
by (metis dom_subid_aux2'' order.antisym local.dom_el_idem local.dom_subid_aux2 local.order_prop local.subdistl mult_assoc)
lemma d_restrict_iff: "(x ≤ y) ⟷ (x ≤ d x ⋅ y)"
by (metis dom_subid_aux2 dsg1 less_eq_def order_trans subdistl)
lemma d_restrict_iff_1: "(d x ⋅ y ≤ z) ⟷ (d x ⋅ y ≤ d x ⋅ z)"
by (metis dom_subid_aux2 domain_1'' domain_invol dsg1 mult_isol_var order_trans)
end
text ‹We add once more a left unit of multiplication.›
class domain_pre_dioid_one_zerol = domain_pre_dioid_one + pre_dioid_one_zerol +
assumes dpd5 [simp]: "d 0 = 0"
begin
subclass domain_near_semiring_one_zerol
by (unfold_locales, simp)
end
subsection ‹Domain Semirings›
text ‹We do not consider domain semirings without units separately at the moment. The axioms are taken from from~\<^cite>‹"DesharnaisStruthSCP"››
class domain_semiringl = semiring_one_zerol + plus_ord + domain_op +
assumes dsr1 [simp]: "x + d x ⋅ x = d x ⋅ x"
and dsr2 [simp]: "d (x ⋅ d y) = d (x ⋅ y)"
and dsr3 [simp]: "d x + 1 = 1"
and dsr4 [simp]: "d 0 = 0"
and dsr5 [simp]: "d (x + y) = d x + d y"
begin
text ‹Every domain semiring is automatically a domain pre-dioid with one and left zero.›
subclass dioid_one_zerol
by (standard, metis add_commute dsr1 dsr3 distrib_left mult_oner)
subclass domain_pre_dioid_one_zerol
by (standard, auto simp: less_eq_def)
end
class domain_semiring = domain_semiringl + semiring_one_zero
subsection ‹The Algebra of Domain Elements›
text ‹We show that the domain elements of a domain semiring form a distributive lattice. Unfortunately we cannot prove this within the type class of domain semirings.›
typedef (overloaded) 'a d_element = "{x :: 'a :: domain_semiring. x = d x}"
by (rule_tac x = 1 in exI, simp add: domain_subid ds.eq_iff)
setup_lifting type_definition_d_element
instantiation d_element :: (domain_semiring) bounded_lattice
begin
lift_definition less_eq_d_element :: "'a d_element ⇒ 'a d_element ⇒ bool" is "(≤)" .
lift_definition less_d_element :: "'a d_element ⇒ 'a d_element ⇒ bool" is "(<)" .
lift_definition bot_d_element :: "'a d_element" is 0
by simp
lift_definition top_d_element :: "'a d_element" is 1
by simp
lift_definition inf_d_element :: "'a d_element ⇒ 'a d_element ⇒ 'a d_element" is "(⋅)"
by (metis dsg3)
lift_definition sup_d_element :: "'a d_element ⇒ 'a d_element ⇒ 'a d_element" is "(+)"
by simp
instance
apply (standard; transfer)
apply (simp add: less_le_not_le)+
apply (metis dom_subid_aux2'')
apply (metis dom_subid_aux2)
apply (metis dom_glb)
apply simp+
by (metis dom_subid)
end
instance d_element :: (domain_semiring) distrib_lattice
by (standard, transfer, metis dom_distrib)
subsection ‹Domain Semirings with a Greatest Element›
text ‹If there is a greatest element in the semiring, then we have another equality.›
class domain_semiring_top = domain_semiring + order_top
begin
notation top (‹⊤›)
lemma kat_equivalence_greatest: "d x ≤ d y ⟷ x ≤ d y ⋅ ⊤"
proof
assume "d x ≤ d y"
thus "x ≤ d y ⋅ ⊤"
by (metis dsg1 mult_isol_var top_greatest)
next
assume "x ≤ d y ⋅ ⊤"
thus "d x ≤ d y"
using dom_glb_eq dom_iso by fastforce
qed
end
subsection ‹Forward Diamond Operators›
context domain_semiringl
begin
text ‹We define a forward diamond operator over a domain semiring. A more modular consideration is not given at the moment.›
definition fd :: "'a ⇒ 'a ⇒ 'a" (‹( |_⟩ _)› [61,81] 82) where
"|x⟩ y = d (x ⋅ y)"
lemma fdia_d_simp [simp]: "|x⟩ d y = |x⟩ y"
by (simp add: fd_def)
lemma fdia_dom [simp]: "|x⟩ 1 = d x"
by (simp add: fd_def)
lemma fdia_add1: "|x⟩ (y + z) = |x⟩ y + |x⟩ z"
by (simp add: fd_def distrib_left)
lemma fdia_add2: "|x + y⟩ z = |x⟩ z + |y⟩ z"
by (simp add: fd_def distrib_right)
lemma fdia_mult: "|x ⋅ y⟩ z = |x⟩ |y⟩ z"
by (simp add: fd_def mult_assoc)
lemma fdia_one [simp]: "|1⟩ x = d x"
by (simp add: fd_def)
lemma fdemodalisation1: "d z ⋅ |x⟩ y = 0 ⟷ d z ⋅ x ⋅ d y = 0"
proof -
have "d z ⋅ |x⟩ y = 0 ⟷ d z ⋅ d (x ⋅ y) = 0"
by (simp add: fd_def)
also have "... ⟷ d z ⋅ x ⋅ y = 0"
by (metis annil dnso6 dsg1 dsg3 mult_assoc)
finally show ?thesis
using dom_weakly_local by auto
qed
lemma fdemodalisation2: "|x⟩ y ≤ d z ⟷ x ⋅ d y ≤ d z ⋅ x"
proof
assume "|x⟩ y ≤ d z"
hence a: "d (x ⋅ d y) ≤ d z"
by (simp add: fd_def)
have "x ⋅ d y = d (x ⋅ d y) ⋅ x ⋅ d y"
using dsg1 mult_assoc by presburger
also have "... ≤ d z ⋅ x ⋅ d y"
using a calculation dom_llp2 mult_assoc by auto
finally show "x ⋅ d y ≤ d z ⋅ x"
using dom_subid_aux2'' order_trans by blast
next
assume "x ⋅ d y ≤ d z ⋅ x"
hence "d (x ⋅ d y) ≤ d (d z ⋅ d x)"
using dom_iso by fastforce
also have "... ≤ d (d z)"
using domain_1'' by blast
finally show "|x⟩ y ≤ d z"
by (simp add: fd_def)
qed
lemma fd_iso1: "d x ≤ d y ⟹ |z⟩ x ≤ |z⟩ y"
using fd_def local.dom_iso local.mult_isol by fastforce
lemma fd_iso2: "x ≤ y ⟹ |x⟩ z ≤ |y⟩ z"
by (simp add: fd_def dom_iso mult_isor)
lemma fd_zero_var [simp]: "|0⟩ x = 0"
by (simp add: fd_def)
lemma fd_subdist_1: "|x⟩ y ≤ |x⟩ (y + z)"
by (simp add: fd_iso1)
lemma fd_subdist_2: "|x⟩ (d y ⋅ d z) ≤ |x⟩ y"
by (simp add: fd_iso1 dom_subid_aux2'')
lemma fd_subdist: "|x⟩ (d y ⋅ d z) ≤ |x⟩ y ⋅ |x⟩ z"
using fd_def fd_iso1 fd_subdist_2 dom_glb dom_subid_aux2 by auto
lemma fdia_export_1: "d y ⋅ |x⟩ z = |d y ⋅ x⟩ z"
by (simp add: fd_def mult_assoc)
end
context domain_semiring
begin
lemma fdia_zero [simp]: "|x⟩ 0 = 0"
by (simp add: fd_def)
end
subsection ‹Domain Kleene Algebras›
text ‹We add the Kleene star to our considerations. Special domain axioms are not needed.›
class domain_left_kleene_algebra = left_kleene_algebra_zerol + domain_semiringl
begin
lemma dom_star [simp]: "d (x⇧⋆) = 1"
proof -
have "d (x⇧⋆) = d (1 + x ⋅ x⇧⋆)"
by simp
also have "... = d 1 + d (x ⋅ x⇧⋆)"
using dns3 by blast
finally show ?thesis
using add_commute local.dsr3 by auto
qed
lemma fdia_star_unfold [simp]: "|1⟩ y + |x⟩ |x⇧⋆⟩ y = |x⇧⋆⟩ y"
proof -
have "|1⟩ y + |x⟩ |x⇧⋆⟩ y = |1 + x ⋅ x⇧⋆⟩ y"
using local.fdia_add2 local.fdia_mult by presburger
thus ?thesis
by simp
qed
lemma fdia_star_unfoldr [simp]: "|1⟩ y + |x⇧⋆⟩ |x⟩ y = |x⇧⋆⟩ y"
proof -
have "|1⟩ y + |x⇧⋆⟩ |x⟩ y = |1 + x⇧⋆ ⋅ x⟩ y"
using fdia_add2 fdia_mult by presburger
thus ?thesis
by simp
qed
lemma fdia_star_unfold_var [simp]: "d y + |x⟩ |x⇧⋆⟩ y = |x⇧⋆⟩ y"
proof -
have "d y + |x⟩ |x⇧⋆⟩ y = |1⟩ y + |x⟩ |x⇧⋆⟩ y"
by simp
also have "... = |1 + x ⋅ x⇧⋆⟩ y"
using fdia_add2 fdia_mult by presburger
finally show ?thesis
by simp
qed
lemma fdia_star_unfoldr_var [simp]: "d y + |x⇧⋆⟩ |x⟩ y = |x⇧⋆⟩ y"
proof -
have "d y + |x⇧⋆⟩ |x⟩ y = |1⟩ y + |x⇧⋆⟩ |x⟩ y"
by simp
also have "... = |1 + x⇧⋆ ⋅ x⟩ y"
using fdia_add2 fdia_mult by presburger
finally show ?thesis
by simp
qed
lemma fdia_star_induct_var: "|x⟩ y ≤ d y ⟹ |x⇧⋆⟩ y ≤ d y"
proof -
assume a1: "|x⟩ y ≤ d y"
hence "x ⋅ d y ≤ d y ⋅ x"
by (simp add: fdemodalisation2)
hence "x⇧⋆ ⋅ d y ≤ d y ⋅ x⇧⋆"
by (simp add: star_sim1)
thus ?thesis
by (simp add: fdemodalisation2)
qed
lemma fdia_star_induct: "d z + |x⟩ y ≤ d y ⟹ |x⇧⋆⟩ z ≤ d y"
proof -
assume a: "d z + |x⟩ y ≤ d y"
hence b: "d z ≤ d y" and c: "|x⟩ y ≤ d y"
apply (simp add: local.join.le_supE)
using a by auto
hence d: "|x⇧⋆⟩ z ≤ |x⇧⋆⟩ y"
using fd_def fd_iso1 by auto
have "|x⇧⋆⟩ y ≤ d y"
using c fdia_star_induct_var by blast
thus ?thesis
using d by fastforce
qed
lemma fdia_star_induct_eq: "d z + |x⟩ y = d y ⟹ |x⇧⋆⟩ z ≤ d y"
by (simp add: fdia_star_induct)
end
class domain_kleene_algebra = kleene_algebra + domain_semiring
begin
subclass domain_left_kleene_algebra ..
end
end