Quelle  Pilling.thy

(* Authors: Fabian Lehr *)

section ‹Pilling's proof of Parikh's theorem›

theory Pilling
  imports 
    "Reg_Lang_Exp_Eqns"
begin


text ‹We prove Parikh's theorem, closely following Pilling's proof cite‹Pilling›. The rough
  is as follows: As seen in section \ref{sec:cfl_as_eqns_sys}, each CFG can be interpreted as a
  of const‹reg_eval› equations of the first type and we can easily convert it into a system
  the second type by applying the Parikh image on both sides of each equation. Pilling now shows
  there is a regular solution to the latter system and that this solution is furthermore minimal.
  the relations explored in section \ref{sec:eqns_sys_relations} we prove that the CFG's
  is a minimal solution of the same sytem and hence that the Parikh image of the CFG's
  and of the regular solution must be identical; this finishes the proof of Parikh's theorem.

 , while in cite‹Pilling› Pilling proves an auxiliary lemma first and applies this lemma in
  proof of the main theorem, we were able to complete the whole proof without using the lemma.›


subsection ‹Special representation of regular language expressions›

text ‹To each const‹reg_eval› regular language expression and variable ‹x› corresponds a second
  language expression with the same Parikh image and of the form depicted in equation (3) in
 cite‹Pilling›. We call regular language expressions of this form "bipartite regular language
 " since they decompose into two subexpressions where one of them contains the variable
 ‹x› and the other one does not:›
definition bipart_rlexp :: "nat ==> 'a rlexp ==> bool" where
  "bipart_rlexp x f = (∃p q. reg_eval p ∧ reg_eval q ∧
    f = Union p (Concat q (Var x)) ∧ x ∉ vars p)"


text ‹All bipartite regular language expressions evaluate to regular languages. Additionally,
  each const‹reg_eval› regular language expression and variable ‹x›, there exists a bipartite
  language expression with identical Parikh image and almost identical set of variables.
  the first proof is simple, the second one is more complex and needs the results of the
  \ref{sec:parikh_img_star} and \ref{sec:parikh_img_star2}:›
lemma "bipart_rlexp x f ==> reg_eval f"
  unfolding bipart_rlexp_def by fastforce


lemma reg_eval_bipart_rlexp_Variable: "∃f'. bipart_rlexp x f' ∧ vars f' = vars (Var y) ∪ {x}
                                        ∧ (∀v. Ψ (eval (Var y) v) = Ψ (eval f' v))"
proof (cases "x = y")
let ?f' = "Union (Const {}) (Concat (Const {[]}) (Var x))"
  case True
  then have "bipart_rlexp x ?f'"
    unfolding bipart_rlexp_def using emptyset_regular epsilon_regular by fastforce
  moreover have "eval ?f' v = eval (Var y) v" for v :: "'a valuation" using True by simp
  moreover have "vars ?f' = vars (Var y) ∪ {x}" using True by simp
  ultimately show ?thesis by metis
next
  let ?f' = "Union (Var y) (Concat (Const {}) (Var x))"
  case False
  then have "bipart_rlexp x ?f'"
    unfolding bipart_rlexp_def using emptyset_regular epsilon_regular by fastforce
  moreover have "eval ?f' v = eval (Var y) v" for v :: "'a valuation" using False by simp
  moreover have "vars ?f' = vars (Var y) ∪ {x}" by simp
  ultimately show ?thesis by metis
qed

lemma reg_eval_bipart_rlexp_Const:
  assumes "regular_lang l"
    shows "∃f'. bipart_rlexp x f' ∧ vars f' = vars (Const l) ∪ {x}
                ∧ (∀v. Ψ (eval (Const l) v) = Ψ (eval f' v))"
proof -
  let ?f' = "Union (Const l) (Concat (Const {}) (Var x))"
  have "bipart_rlexp x ?f'"
    unfolding bipart_rlexp_def using assms emptyset_regular by simp
  moreover have "eval ?f' v = eval (Const l) v" for v :: "'a valuation" by simp
  moreover have "vars ?f' = vars (Const l) ∪ {x}" by simp 
  ultimately show ?thesis by metis
qed

lemma reg_eval_bipart_rlexp_Union:
  assumes "∃f'. bipart_rlexp x f' ∧ vars f' = vars f1 ∪ {x} ∧
                (∀v. Ψ (eval f1 v) = Ψ (eval f' v))"
          "∃f'. bipart_rlexp x f' ∧ vars f' = vars f2 ∪ {x} ∧
                (∀v. Ψ (eval f2 v) = Ψ (eval f' v))"
    shows "∃f'. bipart_rlexp x f' ∧ vars f' = vars (Union f1 f2) ∪ {x} ∧
                (∀v. Ψ (eval (Union f1 f2) v) = Ψ (eval f' v))"
proof -
  from assms obtain f1' f2' where f1'_intro: "bipart_rlexp x f1' ∧ vars f1' = vars f1 ∪ {x} ∧
      (∀v. Ψ (eval f1 v) = Ψ (eval f1' v))"
    and f2'_intro: "bipart_rlexp x f2' ∧ vars f2' = vars f2 ∪ {x} ∧
      (∀v. Ψ (eval f2 v) = Ψ (eval f2' v))"
    by auto
  then obtain p1 q1 p2 q2 where p1_q1_intro: "reg_eval p1 ∧ reg_eval q1 ∧
    f1' = Union p1 (Concat q1 (Var x)) ∧ (∀y ∈ vars p1. y ≠ x)"
    and p2_q2_intro: "reg_eval p2 ∧ reg_eval q2 ∧ f2' = Union p2 (Concat q2 (Var x)) ∧
    (∀y ∈ vars p2. y ≠ x)" unfolding bipart_rlexp_def by auto
  let ?f' = "Union (Union p1 p2) (Concat (Union q1 q2) (Var x))"
  have "bipart_rlexp x ?f'" unfolding bipart_rlexp_def using p1_q1_intro p2_q2_intro by auto
  moreover have "Ψ (eval ?f' v) = Ψ (eval (Union f1 f2) v)" for v
    using p1_q1_intro p2_q2_intro f1'_intro f2'_intro
    by (simp add: conc_Un_distrib(2) sup_assoc sup_left_commute)
  moreover from f1'_intro f2'_intro p1_q1_intro p2_q2_intro
    have "vars ?f' = vars (Union f1 f2) ∪ {x}" by auto
  ultimately show ?thesis by metis
qed

lemma reg_eval_bipart_rlexp_Concat:
  assumes "∃f'. bipart_rlexp x f' ∧ vars f' = vars f1 ∪ {x} ∧
                (∀v. Ψ (eval f1 v) = Ψ (eval f' v))"
          "∃f'. bipart_rlexp x f' ∧ vars f' = vars f2 ∪ {x} ∧
                (∀v. Ψ (eval f2 v) = Ψ (eval f' v))"
    shows "∃f'. bipart_rlexp x f' ∧ vars f' = vars (Concat f1 f2) ∪ {x} ∧
                (∀v. Ψ (eval (Concat f1 f2) v) = Ψ (eval f' v))"
proof -
  from assms obtain f1' f2' where f1'_intro: "bipart_rlexp x f1' ∧ vars f1' = vars f1 ∪ {x} ∧
      (∀v. Ψ (eval f1 v) = Ψ (eval f1' v))"
    and f2'_intro: "bipart_rlexp x f2' ∧ vars f2' = vars f2 ∪ {x} ∧
      (∀v. Ψ (eval f2 v) = Ψ (eval f2' v))"
    by auto
  then obtain p1 q1 p2 q2 where p1_q1_intro: "reg_eval p1 ∧ reg_eval q1 ∧
    f1' = Union p1 (Concat q1 (Var x)) ∧ (∀y ∈ vars p1. y ≠ x)"
    and p2_q2_intro: "reg_eval p2 ∧ reg_eval q2 ∧ f2' = Union p2 (Concat q2 (Var x)) ∧
    (∀y ∈ vars p2. y ≠ x)" unfolding bipart_rlexp_def by auto
  let ?q' = "Union (Concat q1 (Concat (Var x) q2)) (Union (Concat p1 q2) (Concat q1 p2))"
  let ?f' = "Union (Concat p1 p2) (Concat ?q' (Var x))"
  have "∀v. (Ψ (eval (Concat f1 f2) v) = Ψ (eval ?f' v))"
  proof (rule allI)
    fix v
    have f2_subst: "Ψ (eval f2 v) = Ψ (eval p2 v ∪ eval q2 v @@ v x)"
      using p2_q2_intro f2'_intro by auto
    have "Ψ (eval (Concat f1 f2) v) = Ψ ((eval p1 v ∪ eval q1 v @@ v x) @@ eval f2 v)"
      using p1_q1_intro f1'_intro
      by (metis eval.simps(1) eval.simps(3) eval.simps(4) parikh_conc_right)
    also have "… = Ψ (eval p1 v @@ eval f2 v ∪ eval q1 v @@ v x @@ eval f2 v)"
      by (simp add: conc_Un_distrib(2) conc_assoc)
    also have "… = Ψ (eval p1 v @@ (eval p2 v ∪ eval q2 v @@ v x)
        ∪ eval q1 v @@ v x @@ (eval p2 v ∪ eval q2 v @@ v x))"
      using f2_subst by (smt (verit, ccfv_threshold) parikh_conc_right parikh_img_Un parikh_img_commut)
    also have "… = Ψ (eval p1 v @@ eval p2 v ∪ (eval p1 v @@ eval q2 v @@ v x ∪
        eval q1 v @@ eval p2 v @@ v x ∪ eval q1 v @@ v x @@ eval q2 v @@ v x))"
      using parikh_img_commut by (smt (z3) conc_Un_distrib(1) parikh_conc_right parikh_img_Un sup_assoc)
    also have "… = Ψ (eval p1 v @@ eval p2 v ∪ (eval p1 v @@ eval q2 v ∪
        eval q1 v @@ eval p2 v ∪ eval q1 v @@ v x @@ eval q2 v) @@ v x)"
      by (simp add: conc_Un_distrib(2) conc_assoc)
    also have "… = Ψ (eval ?f' v)"
      by (simp add: Un_commute)
    finally show "Ψ (eval (Concat f1 f2) v) = Ψ (eval ?f' v)" .
  qed
  moreover have "bipart_rlexp x ?f'" unfolding bipart_rlexp_def using p1_q1_intro p2_q2_intro by auto
  moreover from f1'_intro f2'_intro p1_q1_intro p2_q2_intro
    have "vars ?f' = vars (Concat f1 f2) ∪ {x}" by auto
  ultimately show ?thesis by metis
qed

lemma reg_eval_bipart_rlexp_Star:
  assumes "∃f'. bipart_rlexp x f' ∧ vars f' = vars f ∪ {x}
                ∧ (∀v. Ψ (eval f v) = Ψ (eval f' v))"
  shows "∃f'. bipart_rlexp x f' ∧ vars f' = vars (Star f) ∪ {x}
                ∧ (∀v. Ψ (eval (Star f) v) = Ψ (eval f' v))"
proof -
  from assms obtain f' where f'_intro: "bipart_rlexp x f' ∧ vars f' = vars f ∪ {x} ∧
      (∀v. Ψ (eval f v) = Ψ (eval f' v))" by auto
  then obtain p q where p_q_intro: "reg_eval p ∧ reg_eval q ∧
    f' = Union p (Concat q (Var x)) ∧ (∀y ∈ vars p. y ≠ x)" unfolding bipart_rlexp_def by auto
  let ?q_new = "Concat (Star p) (Concat (Star (Concat q (Var x))) (Concat (Star (Concat q (Var x))) q))"
  let ?f_new = "Union (Star p) (Concat ?q_new (Var x))"
  have "∀v. (Ψ (eval (Star f) v) = Ψ (eval ?f_new v))"
  proof (rule allI)
    fix v
    have "Ψ (eval (Star f) v) = Ψ (star (eval p v ∪ eval q v @@ v x))"
      using f'_intro parikh_star_mono_eq p_q_intro
      by (metis eval.simps(1) eval.simps(3) eval.simps(4) eval.simps(5))
    also have "… = Ψ (star (eval p v) @@ star (eval q v @@ v x))"
      using parikh_img_star by blast
    also have "… = Ψ (star (eval p v) @@
        star ({[]} ∪ star (eval q v @@ v x) @@ eval q v @@ v x))"
      by (metis Un_commute conc_star_comm star_idemp star_unfold_left)
    also have "… = Ψ (star (eval p v) @@ star (star (eval q v @@ v x) @@ eval q v @@ v x))"
      by auto
    also have "… = Ψ (star (eval p v) @@ ({[]} ∪ star (eval q v @@ v x)
        @@ star (eval q v @@ v x) @@ eval q v @@ v x))"
      using parikh_img_star2 parikh_conc_left by blast
    also have "… = Ψ (star (eval p v) @@ {[]} ∪ star (eval p v) @@ star (eval q v @@ v x)
        @@ star (eval q v @@ v x) @@ eval q v @@ v x)" by (metis conc_Un_distrib(1))
    also have "… = Ψ (eval ?f_new v)" by (simp add: conc_assoc)
    finally show "Ψ (eval (Star f) v) = Ψ (eval ?f_new v)" .
  qed
  moreover have "bipart_rlexp x ?f_new" unfolding bipart_rlexp_def using p_q_intro by fastforce
  moreover from f'_intro p_q_intro have "vars ?f_new = vars (Star f) ∪ {x}" by auto
  ultimately show ?thesis by metis
qed

lemma reg_eval_bipart_rlexp: "reg_eval f ==>
    ∃f'. bipart_rlexp x f' ∧ vars f' = vars f ∪ {x} ∧
         (∀s. Ψ (eval f s) = Ψ (eval f' s))"
proof (induction f rule: reg_eval.induct)
  case (1 uu)
  from reg_eval_bipart_rlexp_Variable show ?case by blast
next
  case (2 l)
  then have "regular_lang l" by simp
  from reg_eval_bipart_rlexp_Const[OF this] show ?case by blast
next
  case (3 f g)
  then have "∃f'. bipart_rlexp x f' ∧ vars f' = vars f ∪ {x} ∧ (∀v. Ψ (eval f v) = Ψ (eval f' v))"
            "∃f'. bipart_rlexp x f' ∧ vars f' = vars g ∪ {x} ∧ (∀v. Ψ (eval g v) = Ψ (eval f' v))"
    by auto
  from reg_eval_bipart_rlexp_Union[OF this] show ?case by blast
next
  case (4 f g)
  then have "∃f'. bipart_rlexp x f' ∧ vars f' = vars f ∪ {x} ∧ (∀v. Ψ (eval f v) = Ψ (eval f' v))"
            "∃f'. bipart_rlexp x f' ∧ vars f' = vars g ∪ {x} ∧ (∀v. Ψ (eval g v) = Ψ (eval f' v))"
    by auto
  from reg_eval_bipart_rlexp_Concat[OF this] show ?case by blast
next
  case (5 f)
  then have "∃f'. bipart_rlexp x f' ∧ vars f' = vars f ∪ {x} ∧ (∀v. Ψ (eval f v) = Ψ (eval f' v))"
    by auto
  from reg_eval_bipart_rlexp_Star[OF this] show ?case by blast
qed


subsection ‹Minimal solution for a single equation›

text ‹The aim is to prove that every system of const‹reg_eval› equations of the second type
  some minimal solution which is const‹reg_eval›. In this section, we prove this property
  for the case of a single equation. First we assume that the equation is bipartite but later
  this section we will abandon this assumption.›

locale single_bipartite_eq =
  fixes x :: "nat"
  fixes p :: "'a rlexp"
  fixes q :: "'a rlexp"
  assumes p_reg:      "reg_eval p"
  assumes q_reg:      "reg_eval q"
  assumes x_not_in_p: "x ∉ vars p"
begin

text ‹The equation and the minimal solution look as follows. Here, ‹x› describes the variable whose
  is to be determined. In the subsequent lemmas, we prove that the solution is const‹reg_eval›
  fulfills each of the three conditions of the predicate const‹partial_min_sol_one_ineq›.
  particular, we will use the lemmas of the sections \ref{sec:rlexp_homogeneous} and
 ref{sec:parikh_arden} here:›
abbreviation "eq ≡ Union p (Concat q (Var x))"
abbreviation "sol ≡ Concat (Star (subst (Var(x := p)) q)) p"

lemma sol_is_reg: "reg_eval sol"
proof -
  from p_reg q_reg have r_reg: "reg_eval (subst (Var(x := p)) q)"
    using subst_reg_eval_update by auto
  with p_reg show "reg_eval sol" by auto
qed

lemma sol_vars: "vars sol ⊆ vars eq - {x}"
proof -
  let ?upd = "Var(x := p)"
  let ?subst_q = "subst ?upd q"
  from x_not_in_p have vars_p: "vars p ⊆ vars eq - {x}" by fastforce
  moreover have "vars p ∪ vars q ⊆ vars eq" by auto
  ultimately have "vars ?subst_q ⊆ vars eq - {x}" using vars_subst_upd_upper by blast
  with x_not_in_p show ?thesis by auto
qed

lemma sol_is_sol_ineq: "partial_sol_ineq x eq sol"
unfolding partial_sol_ineq_def proof (rule allI, rule impI)
  fix v
  assume x_is_sol: "v x = eval sol v"
  let ?r = "subst (Var (x := p)) q"
  let ?upd = "Var(x := sol)"
  let ?q_subst = "subst ?upd q"
  let ?eq_subst = "subst ?upd eq"
  have homogeneous_app: "Ψ (eval ?q_subst v) ⊆ Ψ (eval (Concat (Star ?r) ?r) v)"
    using rlexp_homogeneous by blast
  from x_not_in_p have "eval (subst ?upd p) v = eval p v" using eval_vars_subst[of p] by simp
  then have "Ψ (eval ?eq_subst v) = Ψ (eval p v ∪ eval ?q_subst v @@ eval sol v)"
    by simp
  also have "… ⊆ Ψ (eval p v ∪ eval (Concat (Star ?r) ?r) v @@ eval sol v)"
    using homogeneous_app by (metis dual_order.refl parikh_conc_right_subset parikh_img_Un sup.mono)
  also have "… = Ψ (eval p v) ∪
      Ψ (star (eval ?r v) @@ eval ?r v @@ star (eval ?r v) @@ eval p v)"
    by (simp add: conc_assoc)
  also have "… = Ψ (eval p v) ∪
      Ψ (eval ?r v @@ star (eval ?r v) @@ eval p v)"
    using parikh_img_commut conc_star_star by (smt (verit, best) conc_assoc conc_star_comm)
  also have "… = Ψ (star (eval ?r v) @@ eval p v)"
    using star_unfold_left
    by (smt (verit) conc_Un_distrib(2) conc_assoc conc_epsilon(1) parikh_img_Un sup_commute)
  finally have *: "Ψ (eval ?eq_subst v) ⊆ Ψ (v x)" using x_is_sol by simp
  from x_is_sol have "v = v(x := eval sol v)" using fun_upd_triv by metis
  then have "eval eq v = eval (subst (Var(x := sol)) eq) v"
    using substitution_lemma_upd[where f=eq] by presburger
  with * show "solves_ineq_comm x eq v" unfolding solves_ineq_comm_def by argo
qed

lemma sol_is_minimal:
  assumes is_sol:    "solves_ineq_comm x eq v"
      and sol'_s:    "v x = eval sol' v"
    shows            "Ψ (eval sol v) ⊆ Ψ (v x)"
proof -
  from is_sol sol'_s have is_sol': "Ψ (eval q v @@ v x ∪ eval p v) ⊆ Ψ (v x)"
    unfolding solves_ineq_comm_def by simp
  then have 1: "Ψ (eval (Concat (Star q) p) v) ⊆ Ψ (v x)"
    using parikh_img_arden by auto
  from is_sol' have "Ψ (eval p v) ⊆ Ψ (eval (Var x) v)" by auto
  then have "Ψ (eval (subst (Var(x := p)) q) v) ⊆ Ψ (eval q v)"
    using parikh_img_subst_mono_upd by (metis fun_upd_triv subst_id)
  then have "Ψ (eval (Star (subst (Var(x := p)) q)) v) ⊆ Ψ (eval (Star q) v)"
    using parikh_star_mono by auto
  then have "Ψ (eval sol v) ⊆ Ψ (eval (Concat (Star q) p) v)"
    using parikh_conc_right_subset by (metis eval.simps(4))
  with 1 show ?thesis by fast
qed

text ‹In summary, ‹sol› is a minimal partial solution and it is const‹reg_eval›:›
lemma sol_is_minimal_reg_sol:
  "reg_eval sol ∧ partial_min_sol_one_ineq x eq sol"
  unfolding partial_min_sol_one_ineq_def
  using sol_is_reg sol_vars sol_is_sol_ineq sol_is_minimal
  by blast

end


text ‹As announced at the beginning of this section, we now extend the previous result to arbitrary
 , i.e.\ we show that each const‹reg_eval› equation has some minimal partial solution which is
 const‹reg_eval›:›
lemma exists_minimal_reg_sol:
  assumes eq_reg: "reg_eval eq"
  shows "∃sol. reg_eval sol ∧ partial_min_sol_one_ineq x eq sol"
proof -
  from reg_eval_bipart_rlexp[OF eq_reg] obtain eq'
    where eq'_intro: "bipart_rlexp x eq' ∧ vars eq' = vars eq ∪ {x} ∧
                    (∀v. Ψ (eval eq v) = Ψ (eval eq' v))" by blast
  then obtain p q
    where p_q_intro: "reg_eval p ∧ reg_eval q ∧ eq' = Union p (Concat q (Var x)) ∧ x ∉ vars p"
    unfolding bipart_rlexp_def by blast
  let ?sol = "Concat (Star (subst (Var(x := p)) q)) p"
  from p_q_intro have sol_prop: "reg_eval ?sol ∧ partial_min_sol_one_ineq x eq' ?sol"
    using single_bipartite_eq.sol_is_minimal_reg_sol unfolding single_bipartite_eq_def by blast
  with eq'_intro have "partial_min_sol_one_ineq x eq ?sol"
    using same_min_sol_if_same_parikh_img by blast
  with sol_prop show ?thesis by blast
qed


subsection ‹Minimal solution of the whole system of equations›

text ‹In this section we will extend the last section's result to whole systems of const‹reg_eval›
 . For this purpose, we will show by induction on ‹r› that the first ‹r› equations have
  minimal partial solution which is const‹reg_eval›.

  start with the centerpiece of the induction step: If a const‹reg_eval› and minimal partial solution
 ‹sols› exists for the first ‹r› equations and furthermore a const‹reg_eval› and minimal partial solution
 ‹sol_r› exists for the ‹r›-th equation, then there exists a const‹reg_eval› and minimal partial solution
  the first ‹Suc r› equations as well.›

locale min_sol_induction_step =
  fixes r :: nat
    and sys :: "'a eq_sys"
    and sols :: "nat ==> 'a rlexp"
    and sol_r :: "'a rlexp"
  assumes eqs_reg:      "∀eq ∈ set sys. reg_eval eq"
      and sys_valid:    "∀eq ∈ set sys. ∀x ∈ vars eq. x < length sys"
      and r_valid:      "r < length sys"
      and sols_is_sol:  "partial_min_sol_ineq_sys r sys sols"
      and sols_reg:     "∀i. reg_eval (sols i)"
      and sol_r_is_sol: "partial_min_sol_one_ineq r (subst_sys sols sys ! r) sol_r"
      and sol_r_reg:    "reg_eval sol_r"
begin

text ‹Throughout the proof, a modified system of equations will be occasionally used to simplify
  proof; this modified system is obtained by substituting the partial solutions of
  first ‹r› equations into the original system. Additionally
  retrieve a partial solution for the first ‹Suc r› equations - named ‹sols'› - by substituting the partial
  of the ‹r›-th equation into the partial solutions of each of the first ‹r› equations:›
abbreviation "sys' ≡ subst_sys sols sys"
abbreviation "sols' ≡ λi. subst (Var(r := sol_r)) (sols i)"

lemma sols'_r: "sols' r = sol_r"
  using sols_is_sol unfolding partial_min_sol_ineq_sys_def by simp


text ‹The next lemmas show that const‹sols'› is still const‹reg_eval› and that it complies with
  of the four conditions defined by the predicate const‹partial_min_sol_ineq_sys›:›
lemma sols'_reg: "∀i. reg_eval (sols' i)"
  using sols_reg sol_r_reg using subst_reg_eval_update by blast

lemma sols'_is_sol: "solution_ineq_sys (take (Suc r) sys) sols'"
unfolding solution_ineq_sys_def proof (rule allI, rule impI)
  fix v
  assume s_sols': "∀x. v x = eval (sols' x) v"
  from sols'_r s_sols' have s_r_sol_r: "v r = eval sol_r v" by simp
  with s_sols' have s_sols: "v x = eval (sols x) v" for x
    using substitution_lemma_upd[where f="sols x"] by (auto simp add: fun_upd_idem)
  with sols_is_sol have solves_r_sys: "solves_ineq_sys_comm (take r sys) v"
    unfolding partial_min_sol_ineq_sys_def solution_ineq_sys_def by meson
  have "eval (sys ! r) (λy. eval (sols y) v) = eval (sys' ! r) v"
    using substitution_lemma[of "λy. eval (sols y) v"]
    by (simp add: r_valid Suc_le_lessD subst_sys_subst)
  with s_sols have "eval (sys ! r) v = eval (sys' ! r) v"
    by (metis (mono_tags, lifting) eval_vars)
  with sol_r_is_sol s_r_sol_r have "Ψ (eval (sys ! r) v) ⊆ Ψ (v r)"
    unfolding partial_min_sol_one_ineq_def partial_sol_ineq_def solves_ineq_comm_def by simp
  with solves_r_sys show "solves_ineq_sys_comm (take (Suc r) sys) v"
    unfolding solves_ineq_sys_comm_def solves_ineq_comm_def by (auto simp add: less_Suc_eq)
qed

lemma sols'_min: "∀sols2 v2. (∀x. v2 x = eval (sols2 x) v2)
                   ∧ solves_ineq_sys_comm (take (Suc r) sys) v2
                   ⟶ (∀i. Ψ (eval (sols' i) v2) ⊆ Ψ (v2 i))"
proof (rule allI | rule impI)+
  fix sols2 v2 i
  assume as: "(∀x. v2 x = eval (sols2 x) v2) ∧ solves_ineq_sys_comm (take (Suc r) sys) v2"
  then have "solves_ineq_sys_comm (take r sys) v2" unfolding solves_ineq_sys_comm_def by fastforce
  with as sols_is_sol have sols_s2: "Ψ (eval (sols i) v2) ⊆ Ψ (v2 i)" for i
    unfolding partial_min_sol_ineq_sys_def by auto
  have "eval (sys' ! r) v2 = eval (sys ! r) (λi. eval (sols i) v2)"
    unfolding subst_sys_def using substitution_lemma[where f="sys ! r"]
    by (simp add: r_valid Suc_le_lessD)
  with sols_s2 have "Ψ (eval (sys' ! r) v2) ⊆ Ψ (eval (sys ! r) v2)"
    using rlexp_mono_parikh[of "sys ! r"] by auto
  with as have "solves_ineq_comm r (sys' ! r) v2"
    unfolding solves_ineq_sys_comm_def solves_ineq_comm_def using r_valid by force
  with as sol_r_is_sol have sol_r_min: "Ψ (eval sol_r v2) ⊆ Ψ (v2 r)"
    unfolding partial_min_sol_one_ineq_def by blast
  let ?v' = "v2(r := eval sol_r v2)"
  from sol_r_min have "Ψ (?v' i) ⊆ Ψ (v2 i)" for i by simp
  with sols_s2 show "Ψ (eval (sols' i) v2) ⊆ Ψ (v2 i)"
    using substitution_lemma_upd[where f="sols i"] rlexp_mono_parikh[of "sols i" ?v' v2] by force
qed

lemma sols'_vars_gt_r: "∀i ≥ Suc r. sols' i = Var i"
  using sols_is_sol unfolding partial_min_sol_ineq_sys_def by auto

lemma sols'_vars_leq_r: "∀i < Suc r. ∀x ∈ vars (sols' i). x ≥ Suc r ∧ x < length sys"
proof -
  from sols_is_sol have "∀i < r. ∀x ∈ vars (sols i). x ≥ r ∧ x < length sys"
    unfolding partial_min_sol_ineq_sys_def by simp
  with sols_is_sol have vars_sols: "∀i < length sys. ∀x ∈ vars (sols i). x ≥ r ∧ x < length sys"
    unfolding partial_min_sol_ineq_sys_def by (metis empty_iff insert_iff leI vars.simps(1))
  with sys_valid have "∀x ∈ vars (subst sols (sys ! i)). x ≥ r ∧ x < length sys" if "i < length sys" for i
    using vars_subst[of sols "sys ! i"] that by (metis UN_E nth_mem)
  then have "∀x ∈ vars (sys' ! i). x ≥ r ∧ x < length sys" if "i < length sys" for i
    unfolding subst_sys_def using r_valid that by auto
  moreover from sol_r_is_sol have "vars (sol_r) ⊆ vars (sys' ! r) - {r}"
    unfolding partial_min_sol_one_ineq_def by simp
  ultimately have vars_sol_r: "∀x ∈ vars sol_r. x > r ∧ x < length sys"
    unfolding partial_min_sol_one_ineq_def using r_valid
    by (metis DiffE insertCI nat_less_le subsetD)
  moreover have "vars (sols' i) ⊆ vars (sols i) - {r} ∪ vars sol_r" if "i < length sys" for i
    using vars_subst_upd_upper by meson
  ultimately have "∀x ∈ vars (sols' i). x > r ∧ x < length sys" if "i < length sys" for i
    using vars_sols that by fastforce
  then show ?thesis by (meson r_valid Suc_le_eq dual_order.strict_trans1)
qed


text ‹In summary, const‹sols'› is a minimal partial solution of the first ‹Suc r› equations. This
  us to prove the centerpiece of the induction step in the next lemma, namely that there exists
  const‹reg_eval› and minimal partial solution for the first ‹Suc r› equations:›
lemma sols'_is_min_sol: "partial_min_sol_ineq_sys (Suc r) sys sols'"
  unfolding partial_min_sol_ineq_sys_def
  using sols'_is_sol sols'_min sols'_vars_gt_r sols'_vars_leq_r
  by blast

lemma exists_min_sol_Suc_r:
  "∃sols'. partial_min_sol_ineq_sys (Suc r) sys sols' ∧ (∀i. reg_eval (sols' i))"
  using sols'_reg sols'_is_min_sol by blast

end


text ‹Now follows the actual induction proof: For every ‹r›, there exists a const‹reg_eval› and minimal partial
  of the first ‹r› equations. This then implies that there exists a regular and minimal (non-partial)
  of the whole system:›
lemma exists_minimal_reg_sol_sys_aux:
  assumes eqs_reg:   "∀eq ∈ set sys. reg_eval eq"
      and sys_valid: "∀eq ∈ set sys. ∀x ∈ vars eq. x < length sys"
      and r_valid:   "r ≤ length sys"   
    shows            "∃sols. partial_min_sol_ineq_sys r sys sols ∧ (∀i. reg_eval (sols i))"
using r_valid proof (induction r)
  case 0
  have "solution_ineq_sys (take 0 sys) Var"
    unfolding solution_ineq_sys_def solves_ineq_sys_comm_def by simp
  then show ?case unfolding partial_min_sol_ineq_sys_def by auto
next
  case (Suc r)
  then obtain sols where sols_intro: "partial_min_sol_ineq_sys r sys sols ∧ (∀i. reg_eval (sols i))"
    by auto
  let ?sys' = "subst_sys sols sys"
  from eqs_reg Suc.prems have "reg_eval (sys ! r)" by simp
  with sols_intro Suc.prems have sys_r_reg: "reg_eval (?sys' ! r)"
    using subst_reg_eval[of "sys ! r"] subst_sys_subst[of r sys] by simp
  then obtain sol_r where sol_r_intro:
    "reg_eval sol_r ∧ partial_min_sol_one_ineq r (?sys' ! r) sol_r"
    using exists_minimal_reg_sol by blast
  with Suc sols_intro sys_valid eqs_reg have "min_sol_induction_step r sys sols sol_r"
    unfolding min_sol_induction_step_def by force
  from min_sol_induction_step.exists_min_sol_Suc_r[OF this] show ?case by blast
qed

lemma exists_minimal_reg_sol_sys:
  assumes eqs_reg:   "∀eq ∈ set sys. reg_eval eq"
      and sys_valid: "∀eq ∈ set sys. ∀x ∈ vars eq. x < length sys"
    shows            "∃sols. min_sol_ineq_sys_comm sys sols ∧ (∀i. regular_lang (sols i))"
proof -
  from eqs_reg sys_valid have
    "∃sols. partial_min_sol_ineq_sys (length sys) sys sols ∧ (∀i. reg_eval (sols i))"
    using exists_minimal_reg_sol_sys_aux by blast
  then obtain sols where
    sols_intro: "partial_min_sol_ineq_sys (length sys) sys sols ∧ (∀i. reg_eval (sols i))"
    by blast
  then have "const_rlexp (sols i)" if "i < length sys" for i
    using that unfolding partial_min_sol_ineq_sys_def by (meson equals0I leD)
  with sols_intro have "∃l. regular_lang l ∧ (∀v. eval (sols i) v = l)" if "i < length sys" for i
    using that const_rlexp_regular_lang by metis
  then obtain ls where ls_intro: "∀i < length sys. regular_lang (ls i) ∧ (∀v. eval (sols i) v = ls i)"
    by metis
  let ?ls' = "λi. if i < length sys then ls i else {}"
  from ls_intro have ls'_intro:
    "(∀i < length sys. regular_lang (?ls' i) ∧ (∀v. eval (sols i) v = ?ls' i))
     ∧ (∀i ≥ length sys. ?ls' i = {})" by force
  then have ls'_regular: "regular_lang (?ls' i)" for i by (meson lang.simps(1))
  from ls'_intro sols_intro have "solves_ineq_sys_comm sys ?ls'"
    unfolding partial_min_sol_ineq_sys_def solution_ineq_sys_def
    by (smt (verit) eval.simps(1) linorder_not_less nless_le take_all_iff)
  moreover have "∀sol'. solves_ineq_sys_comm sys sol' ⟶ (∀x. Ψ (?ls' x) ⊆ Ψ (sol' x))"
  proof (rule allI, rule impI)
    fix sol' x
    assume as: "solves_ineq_sys_comm sys sol'"
    let ?sol_rlexps = "λi. Const (sol' i)"
    from as have "solves_ineq_sys_comm (take (length sys) sys) sol'" by simp
    moreover have "sol' x = eval (?sol_rlexps x) sol'" for x by simp
    ultimately show "∀x. Ψ (?ls' x) ⊆ Ψ (sol' x)"
      using sols_intro unfolding partial_min_sol_ineq_sys_def
      by (smt (verit) empty_subsetI eval.simps(1) ls'_intro parikh_img_mono)
  qed
  ultimately have "min_sol_ineq_sys_comm sys ?ls'" unfolding min_sol_ineq_sys_comm_def by blast
  with ls'_regular show ?thesis by blast
qed



subsection ‹Parikh's theorem›

text ‹Finally we are able to prove Parikh's theorem, i.e.\ that to each context free language exists
  regular language with identical Parikh image:›
theorem Parikh:
  assumes "CFL (TYPE('n)) L"
  shows   "∃L'. regular_lang L' ∧ Ψ L = Ψ L'"
proof -
  from assms obtain P and S::'n where *: "L = Lang P S ∧ finite P" unfolding CFL_def by blast
  show ?thesis
  proof (cases "S ∈ Nts P")
    case True
    from * finite_Nts exists_bij_Nt_Var obtain γ γ' where **: "bij_Nt_Var (Nts P) γ γ'" by metis
    let ?sol = "λi. if i < card (Nts P) then Lang_lfp P (γ i) else {}"
    from ** True have "γ' S < card (Nts P)" "γ (γ' S) = S"
      unfolding bij_Nt_Var_def bij_betw_def by auto
    with Lang_lfp_eq_Lang have ***: "Lang P S = ?sol (γ' S)" by metis
    from * ** CFG_eq_sys.CFL_is_min_sol obtain sys
      where sys_intro: "(∀eq ∈ set sys. reg_eval eq) ∧ (∀eq ∈ set sys. ∀x ∈ vars eq. x < length sys)
                        ∧ min_sol_ineq_sys sys ?sol"
      unfolding CFG_eq_sys_def by blast
    with min_sol_min_sol_comm have sol_is_min_sol: "min_sol_ineq_sys_comm sys ?sol" by fast
    from sys_intro exists_minimal_reg_sol_sys obtain sol' where
      sol'_intro: "min_sol_ineq_sys_comm sys sol' ∧ regular_lang (sol' (γ' S))" by fastforce
    with sol_is_min_sol min_sol_comm_unique have "Ψ (?sol (γ' S)) = Ψ (sol' (γ' S))"
      by blast
    with * *** sol'_intro show ?thesis by auto
  next
    case False
    with Nts_Lhss_Rhs_Nts have "S ∉ Lhss P" by fast
    from Lang_empty_if_notin_Lhss[OF this] * show ?thesis by (metis lang.simps(1))
  qed
qed

text ‹Corollary: Every context-free language over a single letter is regular.›

corollary CFL_1_Tm_regular:
  assumes "CFL (TYPE('n)) L" and "∀w ∈ L. set w ⊆ {a}"
  shows "regular_lang L"
proof -
  obtain L' where "regular_lang L'" "Ψ L = Ψ L'"
    using Parikh[OF assms(1)] by blast
  have "L = L'"
    by (metis ‹Ψ L = Ψ L'› ‹∀w∈L. set w ⊆ {a}› parikh_img_def singleton_set_mset_eq)
  with ‹regular_lang L'› show ?thesis by blast
qed

corollary CFG_1_Tm_regular:
  assumes "finite P" "Tms P = {a}"
  shows "regular_lang (Lang P A)"
proof -
  let ?L = "Lang P A"
  have "∀w ∈ ?L. set w ⊆ {a}"
    using derives_Tms_syms_subset[of P "[Nt A]" "map Tm _"] assms(2)
    unfolding Lang_def Tms_syms_def by auto
  thus ?thesis
    by (meson CFL_1_Tm_regular CFL_def assms(1))
qed

no_notation parikh_img ("Ψ")

end