Theory Reg_Lang_Exp_Eqns
section ‹Context free grammars and systems of equations›
theory Reg_Lang_Exp_Eqns
imports
"Parikh_Img"
"Context_Free_Grammar.Context_Free_Language"
begin
text ‹In this section, we will first introduce two types of systems of
equations. Then we will show that to each CFG corresponds a system of equations of the first type
and that the language defined by the CFG is a minimal solution of this systems. Lastly we prove
some relations between the two types of systems of equations.›
subsection ‹Introduction of systems of equations›
text ‹For the first type of systems, each equation is of the form
\[X_i \supseteq r_i\]
For the second type of systems, each equation is of the form
\[\Psi \; X_i \supseteq \Psi \; r_i\]
i.e.\ the Parikh image is applied on both sides of each equation.
In both cases, we represent the whole system by a list of regular language expressions where each
of the variables ‹X⇩0, X⇩1, …› is identified by its integer, i.e.\ \<^term>‹Var i› denotes the variable
‹X⇩i›. The ‹i›-th item of the list then represents the right-hand side ‹r⇩i› of the ‹i›-th equation:›
type_synonym 'a eq_sys = "'a rlexp list"
text ‹Now we can define what it means for a valuation ‹v› to solve a system of equations of the
first type, i.e.\ a system without Parikh images. Afterwards we characterize minimal solutions of
such a system.›
definition solves_ineq_sys :: "'a eq_sys ⇒ 'a valuation ⇒ bool" where
"solves_ineq_sys sys v ≡ ∀i < length sys. eval (sys ! i) v ⊆ v i"
definition min_sol_ineq_sys :: "'a eq_sys ⇒ 'a valuation ⇒ bool" where
"min_sol_ineq_sys sys sol ≡
solves_ineq_sys sys sol ∧ (∀sol'. solves_ineq_sys sys sol' ⟶ (∀x. sol x ⊆ sol' x))"
text ‹The previous definitions can easily be extended to the second type of systems of equations
where the Parikh image is applied on both sides of each equation:›
definition solves_ineq_comm :: "nat ⇒ 'a rlexp ⇒ 'a valuation ⇒ bool" where
"solves_ineq_comm x eq v ≡ Ψ (eval eq v) ⊆ Ψ (v x)"
definition solves_ineq_sys_comm :: "'a eq_sys ⇒ 'a valuation ⇒ bool" where
"solves_ineq_sys_comm sys v ≡ ∀i < length sys. solves_ineq_comm i (sys ! i) v"
definition min_sol_ineq_sys_comm :: "'a eq_sys ⇒ 'a valuation ⇒ bool" where
"min_sol_ineq_sys_comm sys sol ≡
solves_ineq_sys_comm sys sol ∧
(∀sol'. solves_ineq_sys_comm sys sol' ⟶ (∀x. Ψ (sol x) ⊆ Ψ (sol' x)))"
text ‹Substitution into each equation of a system:›
definition subst_sys :: "(nat ⇒ 'a rlexp) ⇒ 'a eq_sys ⇒ 'a eq_sys" where
"subst_sys ≡ map ∘ subst"
lemma subst_sys_subst:
assumes "i < length sys"
shows "(subst_sys s sys) ! i = subst s (sys ! i)"
unfolding subst_sys_def by (simp add: assms)
subsection ‹Partial solutions of systems of equations›
text ‹We introduce partial solutions, i.e.\ solutions which might depend on one or multiple
variables. They are therefore not represented as languages, but as regular language expressions.
‹sol› is a partial solution of the ‹x›-th equation if and only if it solves the equation
independently on the values of the other variables:›
definition partial_sol_ineq :: "nat ⇒ 'a rlexp ⇒ 'a rlexp ⇒ bool" where
"partial_sol_ineq x eq sol ≡ ∀v. v x = eval sol v ⟶ solves_ineq_comm x eq v"
text ‹We generalize the previous definition to partial solutions of whole systems of equations:
‹sols› maps each variable ‹i› to a regular language expression representing the partial solution
of the ‹i›-th equation. ‹sols› is then a partial solution of the whole system if it satisfies the
following predicate:›
definition solution_ineq_sys :: "'a eq_sys ⇒ (nat ⇒ 'a rlexp) ⇒ bool" where
"solution_ineq_sys sys sols ≡ ∀v. (∀x. v x = eval (sols x) v) ⟶ solves_ineq_sys_comm sys v"
text ‹Given the ‹x›-th equation ‹eq›, ‹sol› is a minimal partial solution of this equation if and
only if
\begin{enumerate}
\item ‹sol› is a partial solution of ‹eq›
\item ‹sol› is a proper partial solution (i.e.\ it does not depend on ‹x›) and only
depends on variables occurring in the equation ‹eq›
\item no partial solution of the equation ‹eq› is smaller than ‹sol›
\end{enumerate}
›
definition partial_min_sol_one_ineq :: "nat ⇒ 'a rlexp ⇒ 'a rlexp ⇒ bool" where
"partial_min_sol_one_ineq x eq sol ≡
partial_sol_ineq x eq sol ∧
vars sol ⊆ vars eq - {x} ∧
(∀sol' v'. solves_ineq_comm x eq v' ∧ v' x = eval sol' v'
⟶ Ψ (eval sol v') ⊆ Ψ (v' x))"
text ‹Given a whole system of equations ‹sys›, we can generalize the previous definition such that
‹sols› is a minimal solution (possibly dependent on the variables $X_n, X_{n+1}, \dots$) of
the first ‹n› equations. Besides the three conditions described above, we introduce a forth
condition: ‹sols i = Var i› for ‹i ≥ n›, i.e.\ ‹sols› assigns only spurious solutions to the
equations which are not yet solved:›
definition partial_min_sol_ineq_sys :: "nat ⇒ 'a eq_sys ⇒ (nat ⇒ 'a rlexp) ⇒ bool" where
"partial_min_sol_ineq_sys n sys sols ≡
solution_ineq_sys (take n sys) sols ∧
(∀i ≥ n. sols i = Var i) ∧
(∀i < n. ∀x ∈ vars (sols i). x ≥ n ∧ x < length sys) ∧
(∀sols' v'. (∀x. v' x = eval (sols' x) v')
∧ solves_ineq_sys_comm (take n sys) v'
⟶ (∀i. Ψ (eval (sols i) v') ⊆ Ψ (v' i)))"
text ‹If the Parikh image of two equations ‹f› and ‹g› is identical on all valuations, then their
minimal partial solutions are identical, too:›
lemma same_min_sol_if_same_parikh_img:
assumes same_parikh_img: "∀v. Ψ (eval f v) = Ψ (eval g v)"
and same_vars: "vars f - {x} = vars g - {x}"
and minimal_sol: "partial_min_sol_one_ineq x f sol"
shows "partial_min_sol_one_ineq x g sol"
proof -
from minimal_sol have "vars sol ⊆ vars g - {x}"
unfolding partial_min_sol_one_ineq_def using same_vars by blast
moreover from same_parikh_img minimal_sol have "partial_sol_ineq x g sol"
unfolding partial_min_sol_one_ineq_def partial_sol_ineq_def solves_ineq_comm_def by simp
moreover from same_parikh_img minimal_sol have "∀sol' v'. solves_ineq_comm x g v' ∧ v' x = eval sol' v'
⟶ Ψ (eval sol v') ⊆ Ψ (v' x)"
unfolding partial_min_sol_one_ineq_def solves_ineq_comm_def by blast
ultimately show ?thesis unfolding partial_min_sol_one_ineq_def by fast
qed
subsection ‹CFLs as minimal solutions to systems of equations›
text ‹\label{sec:cfl_as_eqns_sys}›
text ‹We show that each CFG induces a system of equations of the first type, i.e.\ without Parikh images,
such that each equation is \<^const>‹reg_eval› and the CFG's language is the minimal solution of the system.
First, we describe how to derive the system of equations from a CFG. This requires us to fix some
bijection between the variables in the system and the non-terminals occurring in the CFG:›
definition bij_Nt_Var :: "'n set ⇒ (nat ⇒ 'n) ⇒ ('n ⇒ nat) ⇒ bool" where
"bij_Nt_Var A γ γ' ≡ bij_betw γ {..< card A} A ∧ bij_betw γ' A {..< card A}
∧ (∀x ∈ {..< card A}. γ' (γ x) = x) ∧ (∀y ∈ A. γ (γ' y) = y)"
lemma exists_bij_Nt_Var:
assumes "finite A"
shows "∃γ γ'. bij_Nt_Var A γ γ'"
proof -
from assms have "∃γ. bij_betw γ {..< card A} A" by (simp add: bij_betw_iff_card)
then obtain γ where 1: "bij_betw γ {..< card A} A" by blast
let ?γ' = "the_inv_into {..< card A} γ"
from the_inv_into_f_f 1 have 2: "∀x ∈ {..< card A}. ?γ' (γ x) = x" unfolding bij_betw_def by fast
from bij_betw_the_inv_into[OF 1] have 3: "bij_betw ?γ' A {..< card A}" by blast
with 1 f_the_inv_into_f_bij_betw have 4: "∀y ∈ A. γ (?γ' y) = y" by metis
from 1 2 3 4 show ?thesis unfolding bij_Nt_Var_def by blast
qed
locale CFG_eq_sys =
fixes P :: "('n,'a) Prods"
fixes S :: 'n
fixes γ :: "nat ⇒ 'n"
fixes γ' :: "'n ⇒ nat"
assumes finite_P: "finite P"
assumes bij_γ_γ': "bij_Nt_Var (Nts P) γ γ'"
begin
text ‹The following definitions construct a regular language expression for a single production. This
happens step by step, i.e.\ starting with a single symbol (terminal or non-terminal) and then extending
this to a single production. The definitions closely follow the definitions \<^term>‹inst_sym›,
\<^term>‹concats› and \<^term>‹inst_syms› in \<^theory>‹Context_Free_Grammar.Context_Free_Language›.›
definition rlexp_sym :: "('n, 'a) sym ⇒ 'a rlexp" where
"rlexp_sym s = (case s of Tm a ⇒ Const {[a]} | Nt A ⇒ Var (γ' A))"
definition rlexp_concats :: "'a rlexp list ⇒ 'a rlexp" where
"rlexp_concats fs = foldr Concat fs (Const {[]})"
definition rlexp_syms :: "('n, 'a) syms ⇒ 'a rlexp" where
"rlexp_syms w = rlexp_concats (map rlexp_sym w)"
text ‹Now it is shown that the regular language expression constructed for a single production
is \<^const>‹reg_eval›. Again, this happens step by step:›
lemma rlexp_sym_reg: "reg_eval (rlexp_sym s)"
unfolding rlexp_sym_def proof (induction s)
case (Tm x)
have "regular_lang {[x]}" by (meson lang.simps(3))
then show ?case by auto
qed auto
lemma rlexp_concats_reg:
assumes "∀f ∈ set fs. reg_eval f"
shows "reg_eval (rlexp_concats fs)"
using assms unfolding rlexp_concats_def by (induction fs) (use epsilon_regular in auto)
lemma rlexp_syms_reg: "reg_eval (rlexp_syms w)"
proof -
from rlexp_sym_reg have "∀s ∈ set w. reg_eval (rlexp_sym s)" by blast
with rlexp_concats_reg show ?thesis unfolding rlexp_syms_def
by (metis (no_types, lifting) image_iff list.set_map)
qed
text ‹The subsequent lemmas prove that all variables appearing in the regular language
expression of a single production correspond to non-terminals appearing in the production:›
lemma rlexp_sym_vars_Nt:
assumes "s (γ' A) = L A"
shows "vars (rlexp_sym (Nt A)) = {γ' A}"
using assms unfolding rlexp_sym_def by simp
lemma rlexp_sym_vars_Tm: "vars (rlexp_sym (Tm x)) = {}"
unfolding rlexp_sym_def by simp
lemma rlexp_concats_vars: "vars (rlexp_concats fs) = ⋃(vars ` set fs)"
unfolding rlexp_concats_def by (induction fs) simp_all
lemma insts'_vars: "vars (rlexp_syms w) ⊆ γ' ` nts_syms w"
proof
fix x
assume "x ∈ vars (rlexp_syms w)"
with rlexp_concats_vars have "x ∈ ⋃(vars ` set (map rlexp_sym w))"
unfolding rlexp_syms_def by blast
then obtain f where *: "f ∈ set (map rlexp_sym w) ∧ x ∈ vars f" by blast
then obtain s where **: "s ∈ set w ∧ rlexp_sym s = f" by auto
with * rlexp_sym_vars_Tm obtain A where ***: "s = Nt A" by (metis empty_iff sym.exhaust)
with ** have ****: "A ∈ nts_syms w" unfolding nts_syms_def by blast
with rlexp_sym_vars_Nt have "vars (rlexp_sym (Nt A)) = {γ' A}" by blast
with * ** *** **** show "x ∈ γ' ` nts_syms w" by blast
qed
text ‹Evaluating the regular language expression of a single production under a valuation
corresponds to instantiating the non-terminals in the production according to the valuation:›
lemma rlexp_sym_inst_Nt:
assumes "v (γ' A) = L A"
shows "eval (rlexp_sym (Nt A)) v = inst_sym L (Nt A)"
using assms unfolding rlexp_sym_def inst_sym_def by force
lemma rlexp_sym_inst_Tm: "eval (rlexp_sym (Tm a)) v = inst_sym L (Tm a)"
unfolding rlexp_sym_def inst_sym_def by force
lemma rlexp_concats_concats:
assumes "length fs = length Ls"
and "∀i < length fs. eval (fs ! i) v = Ls ! i"
shows "eval (rlexp_concats fs) v = concats Ls"
using assms proof (induction fs arbitrary: Ls)
case Nil
then show ?case unfolding rlexp_concats_def concats_def by simp
next
case (Cons f1 fs)
then obtain L1 Lr where *: "Ls = L1#Lr" by (metis length_Suc_conv)
with Cons have "eval (rlexp_concats fs) v = concats Lr" by fastforce
moreover from Cons.prems * have "eval f1 v = L1" by force
ultimately show ?case unfolding rlexp_concats_def concats_def by (simp add: "*")
qed
lemma rlexp_syms_insts:
assumes "∀A ∈ nts_syms w. v (γ' A) = L A"
shows "eval (rlexp_syms w) v = inst_syms L w"
proof -
have "∀i < length w. eval (rlexp_sym (w!i)) v = inst_sym L (w!i)"
proof (rule allI, rule impI)
fix i
assume "i < length w"
then show "eval (rlexp_sym (w ! i)) v = inst_sym L (w ! i)"
proof (induction "w!i")
case (Nt A)
with assms have "v (γ' A) = L A" unfolding nts_syms_def by force
with rlexp_sym_inst_Nt Nt show ?case by metis
next
case (Tm x)
with rlexp_sym_inst_Tm show ?case by metis
qed
qed
then show ?thesis unfolding rlexp_syms_def inst_syms_def using rlexp_concats_concats
by (metis (mono_tags, lifting) length_map nth_map)
qed
text ‹Each non-terminal of the CFG induces some \<^const>‹reg_eval› equation. We do not directly construct
the equation but only prove its existence:›
lemma subst_lang_rlexp:
"∃eq. reg_eval eq ∧ vars eq ⊆ γ' ` Nts P
∧ (∀v L. (∀A ∈ Nts P. v (γ' A) = L A) ⟶ eval eq v = subst_lang P L A)"
proof -
let ?Insts = "rlexp_syms ` (Rhss P A)"
from finite_Rhss[OF finite_P] have "finite ?Insts" by simp
moreover from rlexp_syms_reg have "∀f ∈ ?Insts. reg_eval f" by blast
ultimately obtain eq where *: "reg_eval eq ∧ ⋃(vars ` ?Insts) = vars eq
∧ (∀v. (⋃f ∈ ?Insts. eval f v) = eval eq v)"
using finite_Union_regular by metis
moreover have "vars eq ⊆ γ' ` Nts P"
proof
fix x
assume "x ∈ vars eq"
with * obtain f where **: "f ∈ ?Insts ∧ x ∈ vars f" by blast
then obtain w where ***: "w ∈ Rhss P A ∧ f = rlexp_syms w" by blast
with ** insts'_vars have "x ∈ γ' ` nts_syms w" by auto
with *** show "x ∈ γ' ` Nts P" unfolding Nts_def Rhss_def by blast
qed
moreover have "∀v L. (∀A ∈ Nts P. v (γ' A) = L A) ⟶ eval eq v = subst_lang P L A"
proof (rule allI | rule impI)+
fix v :: "nat ⇒ 'a lang" and L :: "'n ⇒ 'a lang"
assume state_L: "∀A ∈ Nts P. v (γ' A) = L A"
have "∀w ∈ Rhss P A. eval (rlexp_syms w) v = inst_syms L w"
proof
fix w
assume "w ∈ Rhss P A"
with state_L Nts_nts_syms have "∀A ∈ nts_syms w. v (γ' A) = L A" by fast
from rlexp_syms_insts[OF this] show "eval (rlexp_syms w) v = inst_syms L w" by blast
qed
then have "subst_lang P L A = (⋃f ∈ ?Insts. eval f v)" unfolding subst_lang_def by auto
with * show "eval eq v = subst_lang P L A" by auto
qed
ultimately show ?thesis by auto
qed
text ‹The whole CFG induces a system of \<^const>‹reg_eval› equations. We first define which conditions
this system should fulfill and show its existence in the second step:›
abbreviation "CFG_sys sys ≡
length sys = card (Nts P) ∧
(∀i < card (Nts P). reg_eval (sys ! i) ∧ (∀x ∈ vars (sys ! i). x < card (Nts P))
∧ (∀s L. (∀A ∈ Nts P. s (γ' A) = L A)
⟶ eval (sys ! i) s = subst_lang P L (γ i)))"
lemma CFG_as_eq_sys: "∃sys. CFG_sys sys"
proof -
from bij_γ_γ' have *: "⋀eq. vars eq ⊆ γ' ` Nts P ⟹ ∀x ∈ vars eq. x < card (Nts P)"
unfolding bij_Nt_Var_def bij_betw_def by auto
from subst_lang_rlexp have "∀A. ∃eq. reg_eval eq ∧ vars eq ⊆ γ' ` Nts P ∧
(∀s L. (∀A ∈ Nts P. s (γ' A) = L A) ⟶ eval eq s = subst_lang P L A)"
by blast
with bij_γ_γ' * have "∀i < card (Nts P). ∃eq. reg_eval eq ∧ (∀x ∈ vars eq. x < card (Nts P))
∧ (∀s L. (∀A ∈ Nts P. s (γ' A) = L A) ⟶ eval eq s = subst_lang P L (γ i))"
unfolding bij_Nt_Var_def by metis
with Skolem_list_nth[where P="λi eq. reg_eval eq ∧ (∀x ∈ vars eq. x < card (Nts P))
∧ (∀s L. (∀A ∈ Nts P. s (γ' A) = L A) ⟶ eval eq s = subst_lang P L (γ i))"]
show ?thesis by blast
qed
text ‹As we have proved that each CFG induces a system of \<^const>‹reg_eval› equations, it remains to
show that the CFG's language is a minimal solution of this system. The first lemma proves that
the CFG's language is a solution and the next two lemmas prove that it is minimal:›
abbreviation "sol ≡ λi. if i < card (Nts P) then Lang_lfp P (γ i) else {}"
lemma CFG_sys_CFL_is_sol:
assumes "CFG_sys sys"
shows "solves_ineq_sys sys sol"
unfolding solves_ineq_sys_def proof (rule allI, rule impI)
fix i
assume "i < length sys"
with assms have "i < card (Nts P)" by argo
from bij_γ_γ' have *: "∀A ∈ Nts P. sol (γ' A) = Lang_lfp P A"
unfolding bij_Nt_Var_def bij_betw_def by force
with ‹i < card (Nts P)› assms have "eval (sys ! i) sol = subst_lang P (Lang_lfp P) (γ i)"
by presburger
with lfp_fixpoint[OF mono_if_omega_cont[OF omega_cont_Lang_lfp]] have 1: "eval (sys ! i) sol = Lang_lfp P (γ i)"
unfolding Lang_lfp_def by metis
from ‹i < card (Nts P)› bij_γ_γ' have "γ i ∈ Nts P"
unfolding bij_Nt_Var_def using bij_betwE by blast
with * have "Lang_lfp P (γ i) = sol (γ' (γ i))" by auto
also have "… = sol i" using bij_γ_γ' ‹i < card (Nts P)› unfolding bij_Nt_Var_def by auto
finally show "eval (sys ! i) sol ⊆ sol i" using 1 by blast
qed
lemma CFG_sys_CFL_is_min_aux:
assumes "CFG_sys sys"
and "solves_ineq_sys sys sol'"
shows "Lang_lfp P ≤ (λA. sol' (γ' A))" (is "_ ≤ ?L'")
proof -
have "subst_lang P ?L' A ⊆ ?L' A" for A
proof (cases "A ∈ Nts P")
case True
with assms(1) bij_γ_γ' have "γ' A < length sys"
unfolding bij_Nt_Var_def bij_betw_def by fastforce
with assms(1) bij_γ_γ' True have "subst_lang P ?L' A = eval (sys ! γ' A) sol'"
unfolding bij_Nt_Var_def by metis
also from True assms(2) ‹γ' A < length sys› bij_γ_γ' have "… ⊆ ?L' A"
unfolding solves_ineq_sys_def bij_Nt_Var_def by blast
finally show ?thesis .
next
case False
then have "Rhss P A = {}" unfolding Nts_def Rhss_def by blast
with False show ?thesis unfolding subst_lang_def by simp
qed
then have "subst_lang P ?L' ≤ ?L'" by (simp add: le_funI)
from lfp_lowerbound[of "subst_lang P", OF this] Lang_lfp_def show ?thesis by metis
qed
lemma CFG_sys_CFL_is_min:
assumes "CFG_sys sys"
and "solves_ineq_sys sys sol'"
shows "sol x ⊆ sol' x"
proof (cases "x < card (Nts P)")
case True
then have "sol x = Lang_lfp P (γ x)" by argo
also from CFG_sys_CFL_is_min_aux[OF assms] have "… ⊆ sol' (γ' (γ x))" by (simp add: le_fun_def)
finally show ?thesis using True bij_γ_γ' unfolding bij_Nt_Var_def by auto
next
case False
then show ?thesis by auto
qed
text ‹Lastly we combine all of the previous lemmas into the desired result of this section, namely
that each CFG induces a system of \<^const>‹reg_eval› equations such that the CFG's language is a
minimal solution of the system:›
lemma CFL_is_min_sol:
"∃sys. (∀eq ∈ set sys. reg_eval eq) ∧ (∀eq ∈ set sys. ∀x ∈ vars eq. x < length sys)
∧ min_sol_ineq_sys sys sol"
proof -
from CFG_as_eq_sys obtain sys where *: "CFG_sys sys" by blast
then have "length sys = card (Nts P)" by blast
moreover from * have "∀eq ∈ set sys. reg_eval eq" by (simp add: all_set_conv_all_nth)
moreover from * ‹length sys = card (Nts P)› have "∀eq ∈ set sys. ∀x ∈ vars eq. x < length sys"
by (simp add: all_set_conv_all_nth)
moreover from CFG_sys_CFL_is_sol[OF *] CFG_sys_CFL_is_min[OF *]
have "min_sol_ineq_sys sys sol" unfolding min_sol_ineq_sys_def by blast
ultimately show ?thesis by blast
qed
end
subsection ‹Relation between the two types of systems of equations›
text ‹\label{sec:eqns_sys_relations}›
text ‹One can simply convert a system ‹sys› of equations of the second type (i.e.\ with Parikh
images) into a system of equations of the first type by dropping the Parikh images on both sides of
each equation. The following lemmas describe how the two systems are related to each other.
First of all, to any solution ‹sol› of ‹sys› exists a valuation whose Parikh image is
identical to that of ‹sol› and which is a solution of the other system (i.e.\ the system obtained
by dropping all Parikh images in ‹sys›). The following proof explicitly gives such a solution,
namely \<^term>‹λx. ⋃(parikh_img_eq_class (sol x))›, benefiting from the results of section \ref{sec:parikh_eq_class}:›
lemma sol_comm_sol:
assumes sol_is_sol_comm: "solves_ineq_sys_comm sys sol"
shows "∃sol'. (∀x. Ψ (sol x) = Ψ (sol' x)) ∧ solves_ineq_sys sys sol'"
proof
let ?sol' = "λx. ⋃(parikh_img_eq_class (sol x))"
have sol'_sol: "∀x. Ψ (?sol' x) = Ψ (sol x)"
using parikh_img_Union_class by metis
moreover have "solves_ineq_sys sys ?sol'"
unfolding solves_ineq_sys_def proof (rule allI, rule impI)
fix i
assume "i < length sys"
with sol_is_sol_comm have "Ψ (eval (sys ! i) sol) ⊆ Ψ (sol i)"
unfolding solves_ineq_sys_comm_def solves_ineq_comm_def by blast
moreover from sol'_sol have "Ψ (eval (sys ! i) ?sol') = Ψ (eval (sys ! i) sol)"
using rlexp_mono_parikh_eq by meson
ultimately have "Ψ (eval (sys ! i) ?sol') ⊆ Ψ (sol i)" by simp
then show "eval (sys ! i) ?sol' ⊆ ?sol' i" using subseteq_comm_subseteq by metis
qed
ultimately show "(∀x. Ψ (sol x) = Ψ (?sol' x)) ∧ solves_ineq_sys sys ?sol'"
by simp
qed
text ‹The converse works similarly: Given a minimal solution ‹sol› of the system ‹sys› of the first type,
then ‹sol› is also a minimal solution to the system obtained by converting ‹sys› into a system of the second
type (which can be achieved by applying the Parikh image on both sides of each equation):›
lemma min_sol_min_sol_comm:
assumes "min_sol_ineq_sys sys sol"
shows "min_sol_ineq_sys_comm sys sol"
unfolding min_sol_ineq_sys_comm_def proof
from assms show "solves_ineq_sys_comm sys sol"
unfolding min_sol_ineq_sys_def min_sol_ineq_sys_comm_def solves_ineq_sys_def
solves_ineq_sys_comm_def solves_ineq_comm_def by (simp add: parikh_img_mono)
show " ∀sol'. solves_ineq_sys_comm sys sol' ⟶ (∀x. Ψ (sol x) ⊆ Ψ (sol' x))"
proof (rule allI, rule impI)
fix sol'
assume "solves_ineq_sys_comm sys sol'"
with sol_comm_sol obtain sol'' where sol''_intro:
"(∀x. Ψ (sol' x) = Ψ (sol'' x)) ∧ solves_ineq_sys sys sol''" by meson
with assms have "∀x. sol x ⊆ sol'' x" unfolding min_sol_ineq_sys_def by auto
with sol''_intro show "∀x. Ψ (sol x) ⊆ Ψ (sol' x)"
using parikh_img_mono by metis
qed
qed
text ‹All minimal solutions of a system of the second type have the same Parikh image:›
lemma min_sol_comm_unique:
assumes sol1_is_min_sol: "min_sol_ineq_sys_comm sys sol1"
and sol2_is_min_sol: "min_sol_ineq_sys_comm sys sol2"
shows "Ψ (sol1 x) = Ψ (sol2 x)"
proof -
from sol1_is_min_sol sol2_is_min_sol have "Ψ (sol1 x) ⊆ Ψ (sol2 x)"
unfolding min_sol_ineq_sys_comm_def by simp
moreover from sol1_is_min_sol sol2_is_min_sol have "Ψ (sol2 x) ⊆ Ψ (sol1 x)"
unfolding min_sol_ineq_sys_comm_def by simp
ultimately show ?thesis by blast
qed
end