Theory Quantales.Quantale_Star
section ‹Star and Fixpoints in Quantales›
theory Quantale_Star
imports Quantales
Kleene_Algebra.Kleene_Algebra
begin
text ‹This component formalises properties of the star in quantales. For pre-quantales these are modelled as
fixpoints. For weak quantales they are given by iteration.›
subsection ‹Star and Fixpoints in Pre-Quantales›
context unital_near_quantale
begin
definition "qiter_fun x y = (⊔) x ∘ (⋅) y"
definition "qiterl x y = lfp (qiter_fun x y)"
definition "qiterg x y = gfp (qiter_fun x y)"
abbreviation "qiterl_id ≡ qiterl 1"
abbreviation "qiterq_id ≡ qiterg 1"
definition "qstar x = (⨆i. x ^ i)"
lemma qiter_fun_exp: "qiter_fun x y z = x ⊔ y ⋅ z"
unfolding qiter_fun_def by simp
end
text ‹Many properties of fixpoints have been developed for Isabelle's monotone functions. These carry
two type parameters, and must therefore be used outside of contexts.›
lemma iso_qiter_fun: "mono (λz::'a::unital_pre_quantale. qiter_fun x y z)"
by (metis monoI proto_pre_quantale_class.mult_isol qiter_fun_exp sup.idem sup.mono sup.orderI)
text ‹I derive the left unfold and induction laws of Kleene algebra. I link with the Kleene algebra components
at the end of this section, to bring properties into scope.›
lemma qiterl_unfoldl [simp]: "x ⊔ y ⋅ qiterl x y = qiterl (x::'a::unital_pre_quantale) y"
by (metis iso_qiter_fun lfp_unfold qiter_fun_exp qiterl_def)
lemma qiterg_unfoldl [simp]: "x ⊔ y ⋅ qiterg x y = qiterg (x::'a::unital_pre_quantale) y"
by (metis gfp_fixpoint iso_qiter_fun qiter_fun_exp qiterg_def)
lemma qiterl_inductl: "x ⊔ y ⋅ z ≤ z ⟹ qiterl (x::'a::unital_near_quantale) y ≤ z"
by (simp add: lfp_lowerbound qiterl_def qiter_fun_def)
lemma qiterg_coinductl: "z ≤ x ⊔ y ⋅ z ⟹ z ≤ qiterg (x::'a::unital_near_quantale) y"
by (simp add: gfp_upperbound qiterg_def qiter_fun_def)
context unital_near_quantale
begin
lemma powers_distr: "qstar x ⋅ y = (⨆i. x ^ i ⋅ y)"
by (simp add: qstar_def Sup_distr image_comp)
lemma Sup_iter_unfold: "x ^ 0 ⊔ (⨆n. x ^ (Suc n)) = (⨆n. x ^ n)"
using fSup_unfold by presburger
lemma Sup_iter_unfold_var: "1 ⊔ (⨆n. x ⋅ x ^ n) = (⨆n. x ^ n)"
by (simp only: Sup_iter_unfold[symmetric]) auto
lemma power_inductr: "z ⊔ y ⋅ x ≤ y ⟹ z ⋅ x ^ i ≤ y"
by (induct i, simp_all, metis power_commutes order.eq_iff mult_isor order.trans mult_assoc power.power.power_Suc)
end
context unital_pre_quantale
begin
lemma powers_subdistl: "(⨆i. x ⋅ y ^ i) ≤ x ⋅ qstar y"
by (simp add: SUP_le_iff SUP_upper mult_isol qstar_def)
lemma qstar_subcomm: "qstar x ⋅ x ≤ x ⋅ qstar x"
by (simp add: powers_distr powers_subdistl power_commutes)
lemma power_inductl: "z ⊔ x ⋅ y ≤ y ⟹ x ^ i ⋅ z ≤ y"
by (induct i, simp_all, metis dual_order.trans mult_isol mult_assoc)
end
subsection ‹Star and Iteration in Weak Quantales›
context unital_weak_quantale
begin
text ‹In unital weak quantales one can derive the star axioms of Kleene algebra for iteration. This
generalises the language and relation models from our Kleene algebra components.›
lemma powers_distl: "x ⋅ qstar y = (⨆i. x ⋅ y ^ i)"
by (simp add: qstar_def weak_Sup_distl image_comp)
lemma qstar_unfoldl: "1 ⊔ x ⋅ qstar x ≤ qstar x"
by (simp only: powers_distl Sup_iter_unfold_var, simp add: qstar_def)
lemma qstar_comm: "x ⋅ qstar x = qstar x ⋅ x"
using power_commutes powers_distr powers_distl by auto
lemma qstar_unfoldr [simp]: "1 ⊔ qstar x ⋅ x = qstar x"
using qstar_comm qstar_unfoldl Sup_iter_unfold_var qstar_def powers_distl by auto
lemma qstar_inductl: "z ⊔ x ⋅ y ≤ y ⟹ qstar x ⋅ z ≤ y"
by (subst powers_distr, auto intro!: Sup_least power_inductl)
lemma qstar_inductr: "z ⊔ y ⋅ x ≤ y ⟹ z ⋅ qstar x ≤ y"
by (subst powers_distl, auto intro!: Sup_least power_inductr)
text ‹Hence in this setting one also obtains the right Kleene algebra axioms.›
end