Theory Regular_Algebra_Models
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⇖)"
by (simp add:c_prod_def times_list_def)
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)"
by (simp add: c_prod_def times_list_def)
lemma power_minor_var:
assumes "∀w∈X. k≤|w|"
shows "∀w∈X⇗Suc n⇖. n*k≤|w|"
using assms
apply (auto simp add: l_prod_elim)
using length_lang_pow_lb trans_le_add2
by (simp add: length_lang_pow_lb trans_le_add2 mult.commute)
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)"
by (metis l_prod_elim add_le_mono length_append)
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)
apply (auto simp add: l_prod_elim)
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"]
by (auto simp add:opp_mult_def)
end
lemma arden_l:
assumes "¬ l_ewp y" "x = y⋅x + z"
shows "x = y⇧⋆ ⋅ z"
proof (rule antisym)
show one: "y⇧⋆ ⋅ z ≤ x"
by (metis assms(2) join_semilattice_class.add_comm left_near_kleene_algebra_class.star_inductl_eq)
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"
by (metis ab_near_semiring_one_class.mult_onel kleene_algebra_class.dual.add_zerol)
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
by (metis kleene_algebra_class.dual.add_zerol kleene_algebra_class.dual.add_zeror)
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"
by (metis ab_near_semiring_one_class.mult_onel kleene_algebra_class.dual.add_zerol)
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
by (metis kleene_algebra_class.dual.add_zerol kleene_algebra_class.dual.add_zeror)
qed