Theory Pre_Star

(* Authors: Tassilo Lemke, Tobias Nipkow *)

section ‹$Pre^*$›

theory Pre_Star
imports
  Context_Free_Grammar.Context_Free_Grammar
  LTS_Automata
  "HOL-Library.While_Combinator"
begin

(* Internal polishing: One could get rid of ‹reachable_from› and use ‹states_lts ⊆ Q› instead. *)

text‹This theory defines ‹pre⇧*(L)› (‹pre_star› below) and verifies a simple saturation algorithm
‹pre_star_auto› that computes ‹pre⇧*(M)› given an NFA ‹M› and a finite set of context-free productions.
Most of the work is on the level of finite LTS (via ‹pre_star_lts›).

A closely related formalization is ‹AFP/Pushdown_Systems›where ‹pre⇧*› is computed for pushdown systems instead of CFGs.
›

definition pre_star :: "('n,'t)Prods ⇒ ('n,'t) syms set ⇒ ('n,'t) syms set" where
"pre_star P L ≡ {α. ∃β ∈ L. P ⊢ α ⇒* β}"


subsection ‹Definition on LTS as Fixpoint›

text‹
  The algorithm works by repeatedly adding transitions to the LTS, such that at after every step,
  the LTS accepts the original language and its \textbf{direct} predecessors.

  Since no new states are added, the number of transitions that can be added is bounded,
  which allow to both prove termination and the property of a fixpoint:
  At some point, adding another layer of direct predecessors no-longer changes anything,
  i.e.\ the LTS is saturated and ‹pre⇧*› has been reached.›

definition pre_lts :: "('n,'t) Prods ⇒ 's set ⇒ ('s, ('n,'t) sym) lts ⇒ ('s, ('n,'t) sym) lts"
  where
"pre_lts P Q T =
  { (q, Nt A, q') | q q' A. q ∈ Q ∧ (∃β. (A, β) ∈ P ∧ q' ∈ steps_lts T β q)}"

lemma pre_lts_code[code]: "pre_lts P Q T =
   (⋃q ∈ Q. ⋃(A,β) ∈ P. ⋃q' ∈ steps_lts T β q. {(q, Nt A, q')})"
  unfolding pre_lts_def image_def by(auto)

definition pre_star_lts :: "('n, 't) Prods ⇒ 's set
    ⇒ ('s, ('n, 't) sym) lts ⇒ ('s, ('n, 't) sym) lts option" where
"pre_star_lts P Q ≡ while_option (λT. T ∪ pre_lts P Q T ≠ T) (λT. T ∪ pre_lts P Q T)"

lemma pre_star_lts_rule:
  assumes "⋀T. H T ⟹ T ∪ pre_lts P Q T ≠ T ⟹ H (T ∪ pre_lts P Q T)"
    and "pre_star_lts P Q T = Some T'" and "H T"
  shows "H T'"
  using assms unfolding pre_star_lts_def by (rule while_option_rule)

lemma pre_star_lts_fp: "pre_star_lts P Q T = Some T' ⟹ T' ∪ (pre_lts P Q T') = T'"
  unfolding pre_star_lts_def using while_option_stop by fast

lemma pre_star_lts_mono: "pre_star_lts P Q T = Some T' ⟹ T ⊆ T'"
  by (rule pre_star_lts_rule) blast+


subsection‹Propagation of Reachability›

text‹
  No new states are added. Expressing this fact within the ‹auto› model is to show that the
  set of reachable states from any given start state remains unaltered.
›

lemma pre_lts_reachable:
  "reachable_from T q = reachable_from (T ∪ pre_lts P Q T) q"
  unfolding pre_lts_def by (rule reachable_add_trans) blast

lemma pre_star_lts_reachable:
  assumes "pre_star_lts P Q T = Some T'"
  shows "reachable_from T q = reachable_from T' q"
  by (rule pre_star_lts_rule; use assms pre_lts_reachable in fast)

lemma states_pre_lts: assumes "states_lts T ⊆ Q" shows "states_lts (pre_lts P Q T) ⊆ Q"
using steps_states_lts[OF assms] unfolding pre_lts_def states_lts_def by auto

lemma states_pre_star_lts:
  assumes "pre_star_lts P Q T = Some T'" and "states_lts T ⊆ Q"
  shows "states_lts T' ⊆ Q"
apply (rule pre_star_lts_rule[OF _ assms(1)])
 apply (simp add: states_lts_Un states_pre_lts)
by(fact assms(2))


subsection‹Correctness›

lemma pre_lts_keeps:
  assumes "q' ∈ steps_lts T β q"
  shows "q' ∈ steps_lts (T ∪ pre_lts P Q T) β q"
  using assms steps_lts_mono by (metis insert_absorb insert_subset sup_ge1)

lemma pre_lts_prod:
  assumes "(A, β) ∈ P" and "q ∈ Q" and "q' ∈ Q" and "q' ∈ steps_lts T β q"
  shows "q' ∈ steps_lts (T ∪ pre_lts P Q T) [Nt A] q"
  using assms unfolding pre_lts_def Steps_lts_def Step_lts_def step_lts_def by force

lemma pre_lts_pre:
  assumes "P ⊢ w⇩α ⇒ w⇩β" and "reachable_from T q ⊆ Q" and "q' ∈ steps_lts T w⇩β q"
  shows "q' ∈ steps_lts (T ∪ pre_lts P Q T) w⇩α q"
proof -
  obtain w⇩p w⇩s A β where prod: "(A, β) ∈ P"
      and w⇩α_split: "w⇩α = w⇩p@[Nt A]@w⇩s"
      and w⇩β_split: "w⇩β = w⇩p@β@w⇩s"
    using assms(1) by (meson derive.cases)

  obtain q1 q2 where step_w⇩p: "q1 ∈ steps_lts T w⇩p q"
      and step_β: "q2 ∈ steps_lts T β q1"
      and step_w⇩s: "q' ∈ steps_lts T w⇩s q2"
    using Steps_lts_split3 assms(3)[unfolded w⇩β_split] by fast
  then have q1_reach: "q1 ∈ reachable_from T q" and "q2 ∈ reachable_from T q1"
    using assms(2) unfolding reachable_from_def by blast+
  then have q2_reach: "q2 ∈ reachable_from T q"
    using assms(2) reachable_from_trans by fast

  have "q2 ∈ steps_lts (T ∪ pre_lts P Q T) [Nt A] q1"
    by (rule pre_lts_prod; use q1_reach q2_reach assms(2) prod step_β in blast)
  moreover have "q1 ∈ steps_lts (T ∪ pre_lts P Q T) w⇩p q"
      and "q' ∈ steps_lts (T ∪ pre_lts P Q T) w⇩s q2"
    using step_w⇩p step_w⇩s pre_lts_keeps by fast+
  ultimately have "q' ∈ steps_lts (T ∪ pre_lts P Q T) w⇩α q"
    unfolding w⇩α_split using Steps_lts_join3 by fast
  then show ?thesis .
qed

lemma pre_lts_fp:
  assumes "P ⊢ w⇩α ⇒* w⇩β" and "reachable_from T q ⊆ Q" and "q' ∈ steps_lts T w⇩β q"
    and fp: "T ∪ pre_lts P Q T = T"
  shows "q' ∈ steps_lts T w⇩α q"
proof (insert assms, induction rule: converse_rtranclp_induct[where r="derive P"])
  case base thus ?case by simp
next
  case (step y z)
  then show ?case
    using pre_lts_pre by fastforce
qed

lemma pre_lts_while:
  assumes "P ⊢ w⇩α ⇒* w⇩β" and "reachable_from T q ⊆ Q" and "q' ∈ steps_lts T w⇩β q"
    and "pre_star_lts P Q T = Some T'"
  shows "q' ∈ steps_lts T' w⇩α q"
proof -
  have "T' ∪ pre_lts P Q T' = T'"
    using assms(4) by (rule pre_star_lts_fp)
  moreover have "reachable_from T' q ⊆ Q"
    using assms(2,4) pre_star_lts_reachable by fast
  moreover have "q' ∈ steps_lts T' w⇩β q"
    by (rule steps_lts_mono'[where T⇩1=T]; use assms(3,4) pre_star_lts_mono in blast)
  ultimately show ?thesis
    using assms(1) pre_lts_fp by fast
qed

lemma pre_lts_sub_aux:
  assumes "q' ∈ steps_lts (T ∪ pre_lts P Q T) w q"
  shows "∃w'. P ⊢ w ⇒* w' ∧ q' ∈ steps_lts T w' q"
proof (insert assms, induction w arbitrary: q)
  case Nil
  then show ?case
    by (simp add: Steps_lts_def)
next
  case (Cons c w)
  then obtain q1 where step_w: "q' ∈ steps_lts (T ∪ pre_lts P Q T) w q1"
      and step_c: "q1 ∈ steps_lts (T ∪ pre_lts P Q T) [c] q"
    using Steps_lts_split by (metis (no_types, lifting) append_Cons append_Nil)

  obtain w' where "q' ∈ steps_lts T w' q1" and "P ⊢ w ⇒* w'"
    using Cons step_w by blast

  have "∃c'. q1 ∈ steps_lts T c' q ∧ P ⊢ [c] ⇒* c'"
  proof (cases "q1 ∈ steps_lts T [c] q")
    case True
    then show ?thesis
      by blast
  next
    case False
    then have "q1 ∈ steps_lts (pre_lts P Q T) [c] q"
      using step_c unfolding Steps_lts_def Step_lts_def step_lts_def by force
    then have "(q, c, q1) ∈ pre_lts P Q T"
      by (auto simp: Steps_lts_def Step_lts_def step_lts_def)
    then obtain A β where "(A, β) ∈ P" and "c = Nt A" and "q1 ∈ steps_lts T β q"
      unfolding pre_lts_def by blast
    moreover have "P ⊢ [c] ⇒* β"
      using calculation by (simp add: derive_singleton r_into_rtranclp)
    ultimately show ?thesis
      by blast
  qed
  then obtain c' where "q1 ∈ steps_lts T c' q" and "P ⊢ [c] ⇒* c'"
    by blast

  have "q' ∈ steps_lts T (c'@w') q"
    using ‹q1 ∈ steps_lts T c' q› ‹q' ∈ steps_lts T w' q1› Steps_lts_join by fast
  moreover have "P ⊢ (c#w) ⇒* (c'@w')"
    using ‹P ⊢ [c] ⇒* c'› ‹P ⊢ w ⇒* w'›
    by (metis (no_types, opaque_lifting) Cons_eq_appendI derives_append_decomp self_append_conv2)
  ultimately show ?case
    by blast
qed

lemma pre_lts_sub:
  assumes "∀w. (q' ∈ steps_lts T' w q) ⟶ (∃w'. P ⊢ w ⇒* w' ∧ q' ∈ steps_lts T w' q)"
    and "q' ∈ steps_lts (T' ∪ pre_lts P Q T') w q"
  shows "∃w'. P ⊢ w ⇒* w' ∧ q' ∈ steps_lts T w' q"
proof -
  obtain w' where "P ⊢ w ⇒* w'" and "q' ∈ steps_lts T' w' q"
    using pre_lts_sub_aux assms by fast
  then obtain w'' where "P ⊢ w' ⇒* w''" and "q' ∈ steps_lts T w'' q"
    using assms(1) by blast
  moreover have "P ⊢ w ⇒* w''"
    using ‹P ⊢ w ⇒* w'› calculation(1) by simp
  ultimately show ?thesis
    by blast
qed

lemma pre_star_lts_sub:
  assumes "pre_star_lts P Q T = Some T'"
  shows "(q' ∈ steps_lts T' w q) ⟹ (∃w'. P ⊢ w ⇒* w' ∧ q' ∈ steps_lts T w' q)"
proof -
  let ?I = "λT'. ∀w. (q' ∈ steps_lts T' w q) ⟶ (∃w'. P ⊢ w ⇒* w' ∧ q' ∈ steps_lts T w' q)"
  have "⋀T'. ?I T' ⟹ ?I (T' ∪ pre_lts P Q T')"
    by (simp add: pre_lts_sub[where T=T])
  then have "?I T'"
    by (rule pre_star_lts_rule[where T=T and T'=T']; use assms in blast)
  then show "(q' ∈ steps_lts T' w q) ⟹ (∃w'. P ⊢ w ⇒* w' ∧ q' ∈ steps_lts T w' q)"
    by simp
qed

lemma pre_star_lts_correct:                 
  assumes "reachable_from T q⇩0 ⊆ Q" and "pre_star_lts P Q T = Some T'"
  shows "Lang_lts T' q⇩0 F = pre_star P (Lang_lts T q⇩0 F)"
proof (standard; standard)
  fix w
  assume "w ∈ Lang_lts T' q⇩0 F"
  then obtain q⇩f where "q⇩f ∈ steps_lts T' w q⇩0" and "q⇩f ∈ F"
    by blast
  then obtain w' where "P ⊢ w ⇒* w'" and "q⇩f ∈ steps_lts T w' q⇩0"
    using pre_star_lts_sub assms by fast
  moreover have "w' ∈ Lang_lts T q⇩0 F"
    using calculation ‹q⇩f ∈ F› by blast
  ultimately show "w ∈ pre_star P (Lang_lts T q⇩0 F)"
    unfolding pre_star_def by blast
next
  fix w
  assume "w ∈ pre_star P (Lang_lts T q⇩0 F)"
  then obtain w' where "P ⊢ w ⇒* w'" and "w' ∈ Lang_lts T q⇩0 F"
    unfolding pre_star_def by blast
  then obtain q⇩f where "q⇩f ∈ steps_lts T w' q⇩0" and "q⇩f ∈ F"
    by blast
  then have "q⇩f ∈ steps_lts T' w' q⇩0"
    using steps_lts_mono pre_star_lts_mono assms by (metis in_mono)
  moreover have "reachable_from T' q⇩0 ⊆ Q"
    using assms pre_star_lts_reachable by fast
  moreover have "T' ∪ pre_lts P Q T' = T'"
    by (rule pre_star_lts_fp; use assms(2) in simp)
  moreover note ‹P ⊢ w ⇒* w'›
  ultimately have "q⇩f ∈ steps_lts T' w q⇩0"
    by (elim pre_lts_fp) simp+
  with ‹q⇩f ∈ F› show "w ∈ Lang_lts T' q⇩0 F"
    by blast
qed


subsection‹Termination›

lemma while_option_finite_subset_Some':
  fixes C :: "'a set"
  assumes "mono f" and "⋀X. X ⊆ C ⟹ f X ⊆ C" and "finite C" and "S ⊆ C" and "⋀X. X ⊆ f X"
  shows "∃P. while_option (λA. f A ≠ A) f S = Some P"
proof (rule measure_while_option_Some[where
    f= "%A::'a set. card C - card A" and P= "%A. A ⊆ C ∧ A ⊆ f A" and s=S])
  fix A assume A: "A ⊆ C ∧ A ⊆ f A" "f A ≠ A"
  show "(f A ⊆ C ∧ f A ⊆ f (f A)) ∧ card C - card (f A) < card C - card A"
    (is "?L ∧ ?R")
  proof
    show ?L by (metis A(1) assms(2) monoD[OF ‹mono f›])
    show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset)
  qed
qed (simp add: assms)

lemma pre_star_lts_terminates:
  fixes P :: "('n, 't) Prods" and Q :: "'s set" and T⇩0 :: "('s, ('n, 't) sym) lts"
  assumes "finite P" and "finite Q" and "finite T⇩0" and "states_lts T⇩0 ⊆ Q"
  shows "∃T. pre_star_lts P Q T⇩0 = Some T"
proof -
  define b :: "('s, ('n, 't) sym) lts ⇒ bool" where
    [simp]: "b = (λT. T ∪ pre_lts P Q T ≠ T)"
  define f :: "('s, ('n, 't) sym) lts ⇒ ('s, ('n, 't) sym) lts" where
    [simp]: "f = (λT. T ∪ pre_lts P Q T)"
  then have "mono f"
    unfolding mono_def pre_lts_def
    by (smt (verit, ccfv_threshold) UnCI UnE in_mono mem_Collect_eq Steps_lts_mono2 subsetI)

  define U :: "('s, ('n, 't) sym) lts" where
    "U = { (q, Nt A, q') | q q' A. q ∈ Q ∧ (∃β. (A, β) ∈ P ∧ q' ∈ Q)} ∪ T⇩0"
  have "⋀p a q. (p,a,q) ∈ T⇩0 ⟹ p ∈ Q ∧ q ∈ Q"
    using assms(4) unfolding states_lts_def by auto
  then have "pre_lts P Q T ⊆ U" if asm: "T ⊆ U" for T
    using asm steps_states_lts[of T Q] unfolding U_def pre_lts_def states_lts_def
    by fastforce
  then have U_bounds: "⋀X. X ⊆ U ⟹ f X ⊆ U"
    by simp

  have "finite U"
  proof -
    define U' :: "('s, ('n, 't) sym) lts" where
      [simp]: "U' = Q × ((λ(A,_). Nt A) ` P) × Q"
    have "finite ((λ(A,_). Nt A) ` P)"
      using assms(1) by simp
    then have "finite U'"
      using assms(2) U'_def by blast

    define T' :: "('s, ('n, 't) sym) lts" where
      [simp]: "T' = { (q,Nt A,q') | q q' A. q ∈ Q ∧ (∃β. (A, β) ∈ P ∧ q' ∈ Q)}"
    then have "T' ⊆ U'"
      unfolding T'_def U'_def using assms(1) by fast
    moreover note ‹finite U'›
    ultimately have "finite T'"
      using rev_finite_subset[of U' T'] by blast
    then show "finite U"
      by (simp add: U_def assms)
  qed

  note criteria = ‹finite U› U_def f_def U_bounds ‹mono f›
  have "∃P. while_option (λA. f A ≠ A) f T⇩0 = Some P"
    by (rule while_option_finite_subset_Some'[where C=U]; use criteria in blast)
  then show ?thesis
    by (simp add: pre_star_lts_def)
qed

subsection ‹The Automaton Level›

definition pre_star_auto :: "('n, 't) Prods ⇒ ('s, ('n, 't) sym) auto ⇒ ('s, ('n, 't) sym) auto" where
  "pre_star_auto P M ≡ (
    let Q = {auto.start M} ∪ states_lts (auto.lts M) in
    case pre_star_lts P Q (auto.lts M) of
      Some T' ⇒ M ⦇ auto.lts := T' ⦈
  )"

lemma pre_star_auto_correct:
  assumes "finite P" and "finite (auto.lts M)"
  shows "Lang_auto (pre_star_auto P M) = pre_star P (Lang_auto M)"
proof -
  define T where "T ≡ auto.lts M"
  define Q where "Q ≡ {auto.start M} ∪ states_lts T"
  then have "finite Q"
    unfolding T_def states_lts_def using assms(2) by auto
  have MQ: "states_lts (auto.lts M) ⊆ Q" unfolding Q_def T_def by (force)
  have "reachable_from T (auto.start M) ⊆ Q"
    using reachable_from_computable unfolding Q_def states_lts_def by fastforce
  moreover obtain T' where T'_def: "pre_star_lts P Q T = Some T'"
    using pre_star_lts_terminates[OF assms(1) ‹finite Q› assms(2) MQ] T_def by blast
  ultimately have "Lang_lts T' (auto.start M) (auto.finals M)
    = pre_star P (Lang_lts T (auto.start M) (auto.finals M))"
    by (rule pre_star_lts_correct)
  then have "Lang_auto (M ⦇ auto.lts := T' ⦈) = pre_star P (Lang_auto M)"
    by (simp add: T_def)
  then show ?thesis
    unfolding pre_star_auto_def using Q_def T'_def T_def
    by(force)
qed

lemma pre_star_lts_refl:
  assumes "pre_star_lts P Q T = Some T'" and "(A, []) ∈ P" and "q ∈ Q"
  shows "(q, Nt A, q) ∈ T'"
proof -
  have "q ∈ steps_lts T' [] q"
    unfolding Steps_lts_def using assms by force
  then have "(q, Nt A, q) ∈ pre_lts P Q T'"
    unfolding pre_lts_def using assms by blast
  moreover have "T' = T' ∪ pre_lts P Q T'"
    using pre_star_lts_fp assms(1) by blast
  ultimately show ?thesis
    by blast
qed

lemma pre_star_lts_singleton:
  assumes "pre_star_lts P Q T = Some T'" and "(A, [B]) ∈ P"
    and "(q, B, q') ∈ T'" and "q ∈ Q" and "q' ∈ Q"
  shows "(q, Nt A, q') ∈ T'"
proof -
  have "q' ∈ steps_lts T' [B] q"
    unfolding steps_lts_defs using assms by force
  then have "(q, Nt A, q') ∈ pre_lts P Q T'"
    unfolding pre_lts_def using assms by blast
  moreover have "T' = T' ∪ (pre_lts P Q T')"
    using pre_star_lts_fp assms(1) by blast
  ultimately show ?thesis
    by blast
qed

lemma pre_star_lts_impl:
  assumes "pre_star_lts P Q T = Some T'" and "(A, [B, C]) ∈ P"
    and "(q, B, q') ∈ T'" and "(q', C, q'') ∈ T'"
    and "q ∈ Q" and "q' ∈ Q" and "q'' ∈ Q"
  shows "(q, Nt A, q'') ∈ T'"
proof -
  have "q'' ∈ steps_lts T' [B, C] q"
    unfolding steps_lts_defs using assms by force
  then have "(q, Nt A, q'') ∈ pre_lts P Q T'"
    unfolding pre_lts_def using assms by blast
  moreover have "T' = T' ∪ pre_lts P Q T'"
    using pre_star_lts_fp assms(1) by blast
  ultimately show ?thesis
    by blast
qed

end