# Theory Regular_Algebra_Models

```(* Title:      Regular Algebras
Author:     Simon Foster, Georg Struth
Maintainer: Simon Foster <s.foster at york.ac.uk>
Georg Struth <g.struth at sheffield.ac.uk>
*)

section ‹Models of Regular Algebra›

theory Regular_Algebra_Models
imports Regular_Algebras Kleene_Algebra.Kleene_Algebra_Models
begin

subsection ‹Language Model of Salomaa Algebra›

abbreviation w_length :: "'a list ⇒ nat" ( "|_|")
where "|x| ≡ length x"

definition l_ewp :: "'a lan ⇒ bool" where
"l_ewp X ⟷ {[]} ⊆ X"

interpretation lan_kozen: K2_algebra "(+)" "(⋅)" "1 :: 'a lan" 0 "(⊆)" "(⊂)" "star" ..

interpretation lan_boffa: B1_algebra "(+)" "(⋅)" "1 :: 'a lan" 0 "(⊆)" "(⊂)" "star" ..

lemma length_lang_pow_lb:
assumes "∀x∈X. |x| ≥ k" "x ∈ X^n"
shows "|x| ≥ k*n"
using assms proof (induct n arbitrary: x)
case 0 thus ?case by auto
next
case (Suc n)
note hyp = this
thus ?case
proof -
have "x ∈ X⇗Suc n⇖ ⟷ (∃ y z. x = y@z ∧ y ∈ X ∧ z ∈ X⇗n⇖)"
also from hyp have "... ⟶ (∃ y z. x = y@z ∧ |y| ≥ k ∧ |z| ≥ k*n)"
by auto
also have "... ⟷ (∃ y z. x = y@z ∧ |y| ≥ k ∧ |z| ≥ k*n ∧ ( |x| = |y| + |z| ))"
by force
also have "... ⟷ (∃ y z. x = y@z ∧ |y| ≥ k ∧ |z| ≥ k*n ∧ ( |x| ≥ (n + 1) * k ))"
by (auto, metis add_mono mult.commute, force)
finally show ?thesis
by (metis Suc_eq_plus1 hyp(3) mult.commute)
qed
qed

lemma l_prod_elim: "w∈X ⋅ Y ⟷ (∃u v. w = u@v ∧ u∈X ∧ v∈Y)"

lemma power_minor_var:
assumes "∀w∈X. k≤|w|"
shows "∀w∈X⇗Suc n⇖. n*k≤|w|"
using assms

lemma power_lb: "(∀w∈X. k≤|w| ) ⟶ (∀w. w∈X⇗Suc n⇖ ⟶ n*k≤|w| )"
by (metis power_minor_var)

lemma prod_lb:
"⟦ (∀w∈X. m ≤ length w); (∀w∈Y. n ≤ length w) ⟧ ⟹ (∀w∈(X⋅Y). (m+n) ≤ length w)"

lemma suicide_aux_l:
"⟦ (∀w∈Y. 0≤length w); (∀w∈X⇗Suc n⇖. n ≤ length w) ⟧ ⟹ (∀w∈X⇗Suc n ⇖⋅ Y. n ≤ length w)"
apply (auto simp: l_prod_elim)
apply (drule_tac x="ua @ va" in bspec)
done

lemma suicide_aux_r:
"⟦ (∀w∈Y. 0≤length w); (∀w∈X⇗Suc n⇖. n ≤ length w) ⟧ ⟹ (∀w∈Y ⋅ X⇗Suc n⇖. n ≤ length w)"
by (auto, metis (full_types) le0 plus_nat.add_0 prod_lb)

lemma word_suicide_l:
assumes "¬ l_ewp X" "Y ≠ {}"
shows "(∀w∈Y. ∃n. w∉X⇗Suc n ⇖⋅ Y)"
proof -
have  "∀v∈Y. 0≤length v"
by (metis le0)
from assms have "∀v∈X. 1≤length v"
by (simp add: l_ewp_def, metis le_0_eq length_0_conv not_less_eq_eq)
hence "∀w∈Y. ∃n. w∉X⇗Suc n ⇖⋅ Y"
by (metis nat_mult_1_right power_lb suicide_aux_l le0 Suc_n_not_le_n)
thus ?thesis by metis
qed

lemma word_suicide_r:
assumes "¬ l_ewp X" "Y ≠ {}"
shows "(∀w∈Y. ∃n. w∉Y ⋅ X⇗Suc n⇖)"
proof -
have  "∀v∈Y. 0≤length v"
by (metis le0)
from assms have "∀v∈X. 1≤length v"
by (simp add: l_ewp_def, metis le_0_eq length_0_conv not_less_eq_eq)
hence "∀w∈Y. ∃n. w∉Y ⋅ X⇗Suc n ⇖"
by (metis nat_mult_1_right power_lb suicide_aux_r le0 Suc_n_not_le_n)
thus ?thesis by metis
qed

lemma word_suicide_lang_l: "⟦ ¬ l_ewp X; Y ≠ {} ⟧ ⟹ ∃ n. ¬ (Y ≤ X⇗Suc n ⇖⋅ Y)"
by (metis Set.set_eqI empty_iff in_mono word_suicide_l)

lemma word_suicide_lang_r: "⟦ ¬ l_ewp X; Y ≠ {} ⟧ ⟹ ∃ n. ¬ (Y ≤ Y ⋅ X⇗Suc n⇖)"
by (metis Set.set_eqI empty_iff in_mono word_suicide_r)

text ‹These duality results cannot be relocated easily›

context K1_algebra
begin

lemma power_dual_transfer [simp]:
"power.power (1::'a) (⊙) x n = x⇗n⇖"
by (induct n, simp_all, metis opp_mult_def power_commutes)

lemma aarden_aux_l:
"y ≤ x ⋅ y + z ⟹ y ≤  x⇗Suc n⇖ ⋅ y + x⇧⋆ ⋅ z"
using dual.aarden_aux[of "y" "x" "z" "n"]

end

lemma arden_l:
assumes "¬ l_ewp y" "x = y⋅x + z"
shows "x = y⇧⋆ ⋅ z"
proof (rule antisym)
show one: "y⇧⋆ ⋅ z ≤ x"
show "x ≤ y⇧⋆ ⋅ z"
proof (cases "x = 0")
show "x = 0 ⟹ x ≤ y⇧⋆⋅z"
by simp
assume assms': "x ≠ 0"
have "⋀ n. x ≤ y⇗Suc n ⇖⋅ x + y⇧⋆ ⋅ z"
by (metis assms(2) kleene_algebra_class.aarden_aux_l subsetI)
moreover then have "⋀ w n. w ∈ x ⟹ w ∈ y⇗Suc n ⇖⋅ x ∨ w ∈ y⇧⋆ ⋅ z"
by (force simp: plus_set_def)
ultimately show "x ≤ y⇧⋆ ⋅ z"
by (metis (full_types) all_not_in_conv assms(1) subsetI word_suicide_l)
qed
qed

lemma arden_r:
assumes "¬ l_ewp y" "x = x ⋅ y + z"
shows "x = z ⋅ y⇧⋆"
proof (rule antisym)
show one: "z ⋅ y⇧⋆ ≤ x"
by (metis assms(2) join.sup_commute kleene_algebra_class.star_inductr_var order_refl)
show "x ≤ z ⋅ y⇧⋆"
proof (cases "x = 0")
show "x = 0 ⟹ x ≤ z ⋅ y⇧⋆"
by simp
assume assms': "x ≠ 0"
have "⋀ n. x ≤ x ⋅ y⇗Suc n⇖ + z ⋅ y⇧⋆"
by (metis assms(2) kleene_algebra_class.aarden_aux subsetI)
moreover then have "⋀ w n. w ∈ x ⟹ w ∈ x ⋅ y⇗Suc n⇖ ∨ w ∈ z ⋅ y⇧⋆"
by (force simp: plus_set_def)
ultimately show "x ≤ z ⋅ y⇧⋆"
by (metis (full_types) all_not_in_conv assms(1) subsetI word_suicide_r)
qed
qed

text ‹The following two facts provide counterexamples to Arden's rule if the empty word property is not considered.›

lemma arden_l_counter: "∃ (x::'a lan) (y::'a lan) (z::'a lan). x = y ⋅ x + z ∧ x ≠ y⇧⋆ ⋅ z"
proof -
have one: "(0::'a lan) + 1 ⋅ 1 = 1"
have two: "(1::'a lan) ≠ 1⇧⋆ ⋅ 0"
proof -
have "∃x⇩1. (0::'a list set) ≠ x⇩1"
by auto
hence "(1::'a list set) ≠ 0"
by (metis kleene_algebra_class.dual.annir kleene_algebra_class.dual.mult.right_neutral)
thus "(1::'a list set) ≠ 1⇧⋆ ⋅ 0"
by simp
qed
show ?thesis using one and two
qed

lemma arden_r_counter: "∃ (x::'a lan) (y::'a lan) (z::'a lan). x = x ⋅ y + z ∧ x ≠ z ⋅ y⇧⋆"
proof -
have one: "(0::'a lan) + 1 ⋅ 1 = 1"
have two: "(1::'a lan) ≠ 0 ⋅ 1⇧⋆"
proof -
have "∃x⇩1. (0::'a list set) ≠ x⇩1"
by auto
hence "(1::'a list set) ≠ 0"
by (metis kleene_algebra_class.dual.annir kleene_algebra_class.dual.mult.right_neutral)
thus "(1::'a list set) ≠ 0 ⋅ 1⇧⋆"
by simp
qed
show ?thesis using one and two
qed

interpretation lan_salomaa_l: Sl_algebra "(+)" "(⋅)" "1 :: 'a lan" 0 "(⊆)" "(⊂)" "star" "l_ewp"
proof
fix x y z :: "'a lan"
show "(1 + x)⇧⋆ = x⇧⋆"
by (metis kleene_algebra_class.dual.star2)
show "l_ewp x = (∃y. x = 1 + y ∧ ¬ l_ewp y)"
by (simp add:l_ewp_def one_set_def one_list_def plus_set_def, metis insertCI mk_disjoint_insert)
show "1 + x ⋅ x⇧⋆ = x⇧⋆"
by (metis kleene_algebra_class.star_unfoldl_eq)
show "¬ l_ewp y ⟹ x = y ⋅ x + z ⟹ x = y⇧⋆ ⋅ z"
by (metis arden_l)
qed

interpretation lan_salomaa_r: Sr_algebra "(+)" "(⋅)" "1 :: 'a lan" 0 "(⊆)" "(⊂)" "star" "l_ewp"
proof
fix x y z :: "'a lan"
show "1 + x⇧⋆ ⋅ x = x⇧⋆"
by (metis kleene_algebra_class.star_unfoldr_eq)
show "¬ l_ewp y ⟹ x = x ⋅ y + z ⟹ x = z ⋅ y⇧⋆"
by (metis arden_r)
qed

subsection ‹Regular Language Model of Salomaa Algebra›

notation
Atom ("⟨_⟩") and
Plus (infixl "+⇩r" 65) and
Times (infixl "⋅⇩r" 70) and
Star ("_⇧⋆⇩r" [101] 100) and
Zero ("0⇩r") and
One ("1⇩r")

fun rexp_ewp :: "'a rexp ⇒ bool" where
"rexp_ewp 0⇩r = False" |
"rexp_ewp 1⇩r = True" |
"rexp_ewp ⟨a⟩ = False" |
"rexp_ewp (s +⇩r t) = (rexp_ewp s ∨ rexp_ewp t)" |
"rexp_ewp (s ⋅⇩r t) = (rexp_ewp s ∧ rexp_ewp t)" |
"rexp_ewp (s⇧⋆⇩r) = True"

abbreviation "ro(s) ≡ (if (rexp_ewp s) then 1⇩r else 0⇩r)"

lift_definition r_ewp :: "'a reg_lan ⇒ bool" is "l_ewp" .

lift_definition r_lang :: "'a rexp ⇒ 'a reg_lan"  is "lang"
by (simp)

abbreviation r_sim :: "'a rexp ⇒ 'a rexp ⇒ bool" (infix "∼" 50) where
"p ∼ q ≡ r_lang p = r_lang q"

declare Rep_reg_lan [simp]
declare Rep_reg_lan_inverse [simp]
declare Abs_reg_lan_inverse [simp]

lemma rexp_ewp_l_ewp: "l_ewp (lang x) = rexp_ewp x"
proof (induct x)
case (Star x) thus ?case
by (simp, metis lan_salomaa_l.EWP left_near_kleene_algebra_class.star_plus_one)
qed (simp_all add:l_ewp_def zero_set_def one_set_def one_list_def plus_set_def c_prod_def times_list_def)

theorem regexp_ewp:
defines P_def: "P(t) ≡ ∃ t'. t ∼ ro(t) +⇩r t' ∧ ro(t') = 0⇩r"
shows "P t"
proof (induct t)
show "P(0⇩r)"
by (simp add:P_def r_lang_def, rule_tac x="0⇩r" in exI, simp)
next
fix a
show "P(⟨a⟩)"
by (simp add:P_def r_lang_def, rule_tac x="⟨a⟩" in exI, simp)
next
show "P(1⇩r)"
by (simp add:P_def r_lang_def, rule_tac x="0⇩r" in exI, simp)
next
fix t1 t2
assume "P(t1)" "P(t2)"
then obtain t1' t2'
where "t1 ∼ ro(t1) +⇩r t1'" "ro(t1') = 0⇩r"
"t2 ∼ ro(t2) +⇩r t2'" "ro(t2') = 0⇩r"
by (metis assms rexp.distinct(1))
thus "P(t1 +⇩r t2)"
apply (subst P_def, transfer)
apply (rule_tac x="t1' +⇩r t2'" in exI)
apply clarsimp
by (metis (no_types, lifting) add.left_commute join.sup_assoc join.sup_left_idem rexp.distinct(2))
next
fix t1 t2
assume "P(t1)" "P(t2)"
then obtain t1' t2'
where t1: "t1 ∼ ro(t1) +⇩r t1'" "ro(t1') = 0⇩r" and
t2: "t2 ∼ ro(t2) +⇩r t2'" "ro(t2') = 0⇩r"
by (metis assms rexp.distinct(1))
thus "P(t1 ⋅⇩r t2)"
proof -
let ?t' = "ro(t1) ⋅⇩r t2' +⇩r t1' ⋅⇩r ro(t2) +⇩r t1' ⋅⇩r t2'"
from t1 t2 have r1: "ro(?t') = 0⇩r"
by (auto)
from t1 t2 have "t1 ⋅⇩r t2 ∼ (ro(t1) +⇩r t1') ⋅⇩r (ro(t2) +⇩r t2')" (is "?l ∼ ?r")
by (transfer, simp)
also have "?r ∼ ro(t1) ⋅⇩r ro(t2) +⇩r ro(t1) ⋅⇩r t2' +⇩r t1' ⋅⇩r ro(t2) +⇩r t1' ⋅⇩r t2'" (is "?l ∼ ?r")
apply (transfer, unfold lang.simps)
apply (simp only: distrib_right' semiring_class.distrib_left)
apply (metis (opaque_lifting, no_types) join_semilattice_class.add_comm semiring_class.combine_common_factor)
done
also have "?r ∼ ro(t1 ⋅⇩r t2) +⇩r ro(t1) ⋅⇩r t2' +⇩r t1' ⋅⇩r ro(t2) +⇩r t1' ⋅⇩r t2'" (is "?l ∼ ?r")
by (transfer, simp)
also have "?r ∼ ro(t1 ⋅⇩r t2) +⇩r ?t'"
apply (transfer, unfold lang.simps)
done
finally show ?thesis using r1
apply (unfold P_def)
apply (rule_tac x="?t'" in exI, simp)
done
qed
next
fix s
assume assm:"P s"
then obtain s' where r1: "s ∼ ro(s) +⇩r s'" "ro(s') = 0⇩r"
by (metis assms rexp.distinct(1))
thus "P (s⇧⋆⇩r)"
proof -
let ?t' = "s' ⋅⇩r (s')⇧⋆⇩r"
have r2: "ro(?t') = 0⇩r"
by (metis r1(2) rexp.distinct(1) rexp_ewp.simps(5))
from assm r1 have "(ro(s) +⇩r s')⇧⋆⇩r ∼ (s')⇧⋆⇩r" (is "?l ∼ ?r")
by (transfer, auto)
also have "?r ∼ 1⇩r +⇩r s' ⋅⇩r (s')⇧⋆⇩r" (is "?l ∼ ?r")
by (transfer, auto)
also have "?r ∼ ro(s⇧⋆⇩r) +⇩r ?t'"
by (metis (full_types) rexp_ewp.simps(6))
finally show ?thesis
by (metis assms lang.simps(6) r1(1) r2 r_lang.abs_eq r_lang.rep_eq)
qed
qed

instantiation reg_lan :: (type) Sr_algebra
begin

lift_definition ewp_reg_lan :: "'a reg_lan ⇒ bool" is "l_ewp" .

instance proof
fix x :: "'a reg_lan"
show "(1 + x)⇧⋆ = x⇧⋆"
by (metis kleene_algebra_class.dual.star2)
next
fix x :: "'a reg_lan"
show "1 + x⇧⋆ ⋅ x = x⇧⋆"
by (metis kleene_algebra_class.star_unfoldr_eq)
next
fix x :: "'a reg_lan"
show "ewp x = (∃y. x = 1 + y ∧ ¬ ewp y)"
proof -
obtain t where "r_lang t = x"
by (transfer, auto)
moreover obtain t' where "t ∼ ro(t) +⇩r t'" "ro(t') = 0⇩r"
by (metis regexp_ewp)
ultimately show ?thesis
apply (transfer, auto)
apply (metis (full_types) lang.simps(2) rexp.distinct(1) rexp_ewp_l_ewp)
apply (metis lan_salomaa_l.EWP)
done
qed
next
fix x y z :: "'a reg_lan"
show "⟦ ¬ ewp y; x = x ⋅ y + z ⟧ ⟹ x = z ⋅ y⇧⋆"
by (transfer, metis lan_salomaa_r.Ar)
qed
end

instantiation reg_lan :: (type) Sl_algebra
begin

instance proof
fix x :: "'a reg_lan"
show "1 + x ⋅ x⇧⋆ = x⇧⋆"
by (metis left_pre_kleene_algebra_class.star_unfoldl_eq)
next
fix x y z :: "'a reg_lan"
show "⟦ ¬ ewp y; x = y ⋅ x + z ⟧ ⟹ x = y⇧⋆ ⋅ z"
by (transfer, metis lan_salomaa_l.Al)
qed
end

instance reg_lan :: (type) S_algebra ..

theorem arden_regexp_l:
assumes "ro(y) = 0⇩r" "x ∼ y ⋅⇩r x +⇩r z"
shows "x ∼ y⇧⋆⇩r ⋅⇩r z"
using assms
by (transfer, metis arden_l lang.simps(4) lang.simps(5) lang.simps(6) rexp.distinct(1) rexp_ewp_l_ewp)

theorem arden_regexp_r:
assumes "ro(y) = 0⇩r" "x ∼ x ⋅⇩r y +⇩r z"
shows "x ∼ z ⋅⇩r y⇧⋆⇩r"
using assms
by transfer (metis lan_salomaa_r.Ar lang.simps(4) lang.simps(5) lang.simps(6) rexp.distinct(1) rexp_ewp_l_ewp)

end
```