Theory DPN

(*  Title:       Dynamic pushdown networks
    ID:
    Author:      Peter Lammich <peter.lammich@uni-muenster.de>
    Maintainer:  Peter Lammich <peter.lammich@uni-muenster.de>
*)

section ‹ Dynamic pushdown networks ›
theory DPN
imports DPN_Setup SRS FSM NDET
begin

text ‹
  Dynamic pushdown networks (DPNs) are a model for parallel, context free processes where processes can create new processes.

  They have been introduced in \cite{BMT05}. In this theory we formalize DPNs and the automata based algorithm for calculating a representation of the (regular) set of backward reachable configurations, starting at
  a regular set of configurations. 

  We describe the algorithm nondeterministically, and prove its termination and correctness.
›

subsection ‹ Dynamic pushdown networks ›

subsubsection ‹ Definition ›
record ('c,'l) DPN_rec =
  csyms :: "'c set"
  ssyms :: "'c set"
  sep :: "'c"
  labels :: "'l set"
  rules :: "('c,'l) SRS"

text ‹
  A dynamic pushdown network consists of a finite set of control symbols, a finite set of stack symbols, a separator symbol\footnote{In the final version of \cite{BMT05}, 
  no separator symbols are used. We use them here because we think it simplifies formalization of the proofs.}, a finite set of labels and a finite set of labelled string rewrite rules.

  The set of control and stack symbols are disjoint, and both do not contain the separator. A string rewrite rule is either of the form @{text "[p,γ] ↪a p1#w1"} or @{text "[p,γ] ↪a p1#w1@♯#p2#w2"} where
  @{text "p,p1,p2"} are control symbols, @{text "w1,w2"} are sequences of stack symbols, @{text a} is a label and @{text "♯"} is the separator.
›

locale DPN = 
  fixes M
  fixes separator ("♯")
  defines sep_def: "♯ == sep M"
  assumes sym_finite: "finite (csyms M)" "finite (ssyms M)"
  assumes sym_disjoint: "csyms M ∩ ssyms M = {}" "♯ ∉ csyms M ∪ ssyms M"
  assumes lab_finite: "finite (labels M)"
  assumes rules_finite: "finite (rules M)"
  assumes rule_fmt: "r ∈ rules M ⟹ 
     (∃p γ a p' w. p∈csyms M ∧ γ∈ssyms M ∧ p'∈csyms M ∧ w∈lists (ssyms M) ∧ a∈labels M ∧ r=p#[γ] ↪⇘a⇙ p'#w) 
  ∨  (∃p γ a p1 w1 p2 w2.  p∈csyms M ∧ γ∈ssyms M ∧ p1∈csyms M ∧ w1∈lists (ssyms M) ∧ p2∈csyms M ∧ w2∈lists (ssyms M) ∧ a∈labels M ∧ r=p#[γ] ↪⇘a⇙ p1#w1@♯#p2#w2)"

lemma (in DPN) sep_fold: "sep M == ♯" by (simp add: sep_def)

lemma (in DPN) sym_disjoint': "sep M ∉ csyms M ∪ ssyms M" using sym_disjoint by (simp add: sep_def) 

subsubsection ‹ Basic properties ›
lemma (in DPN) syms_part: "x∈csyms M ⟹ x∉ssyms M" "x∈ssyms M ⟹ x∉csyms M" using sym_disjoint by auto
lemma (in DPN) syms_sep: "♯∉csyms M" "♯∉ssyms M" using sym_disjoint by auto
lemma (in DPN) syms_sep': "sep M∉csyms M" "sep M∉ssyms M" using syms_sep by (auto simp add: sep_def)

lemma (in DPN) rule_cases[consumes 1, case_names no_spawn spawn]: 
  assumes A: "r∈rules M"
  assumes NOSPAWN: "!! p γ a p' w. ⟦p∈csyms M; γ∈ssyms M; p'∈csyms M; w∈lists (ssyms M); a∈labels M; r=p#[γ] ↪⇘a⇙ p'#w⟧ ⟹ P"
  assumes SPAWN: "!! p γ a p1 w1 p2 w2. ⟦p∈csyms M; γ∈ssyms M; p1∈csyms M; w1∈lists (ssyms M); p2∈csyms M; w2∈lists (ssyms M); a∈labels M; r=p#[γ] ↪⇘a⇙ p1#w1@♯#p2#w2⟧ ⟹ P"
  shows P
  using A NOSPAWN SPAWN
  by (blast dest!: rule_fmt)

lemma (in DPN) rule_cases': 
  "⟦r∈rules M; 
    !! p γ a p' w. ⟦p∈csyms M; γ∈ssyms M; p'∈csyms M; w∈lists (ssyms M); a∈labels M; r=p#[γ] ↪⇘a⇙ p'#w⟧ ⟹ P; 
    !! p γ a p1 w1 p2 w2. ⟦p∈csyms M; γ∈ssyms M; p1∈csyms M; w1∈lists (ssyms M); p2∈csyms M; w2∈lists (ssyms M); a∈labels M; r=p#[γ] ↪⇘a⇙ p1#w1@(sep M)#p2#w2⟧ ⟹ P⟧ 
  ⟹ P" by (unfold sep_fold) (blast elim!: rule_cases)

lemma (in DPN) rule_prem_fmt: "r∈rules M ⟹ ∃ p γ a c'. p∈csyms M ∧ γ∈ssyms M ∧ a∈labels M ∧ set c' ⊆ csyms M ∪ ssyms M ∪ {♯} ∧ r=(p#[γ] ↪⇘a ⇙ c')" 
  apply (erule rule_cases)
  by (auto)

lemma (in DPN) rule_prem_fmt': "r∈rules M ⟹ ∃ p γ a c'. p∈csyms M ∧ γ∈ssyms M ∧ a∈labels M ∧ set c' ⊆ csyms M ∪ ssyms M ∪ {sep M} ∧ r=(p#[γ] ↪⇘a ⇙ c')" by (unfold sep_fold, rule rule_prem_fmt) 
  
lemma (in DPN) rule_prem_fmt2: "[p,γ]↪⇘a⇙ c' ∈ rules M ⟹ p∈csyms M ∧ γ∈ssyms M ∧ a∈labels M ∧ set c' ⊆ csyms M ∪ ssyms M ∪ {♯}" by (fast dest: rule_prem_fmt)
lemma (in DPN) rule_prem_fmt2': "[p,γ]↪⇘a⇙ c' ∈ rules M ⟹ p∈csyms M ∧ γ∈ssyms M ∧ a∈labels M ∧ set c' ⊆ csyms M ∪ ssyms M ∪ {sep M}" by (unfold sep_fold, rule rule_prem_fmt2)

lemma (in DPN) rule_fmt_fs: "[p,γ]↪⇘a⇙ p'#c' ∈ rules M ⟹ p∈csyms M ∧ γ∈ssyms M ∧ a∈labels M ∧ p'∈csyms M ∧ set c' ⊆ csyms M ∪ ssyms M ∪ {♯}"
  apply (erule rule_cases)
  by (auto)

  
subsubsection ‹Building DPNs›

text ‹Sanity check: we can create valid DPNs by adding rules to an empty DPN›

definition "dpn_empty C S s ≡ ⦇
  csyms = C,
  ssyms = S,
  sep = s,
  labels = {},
  rules = {}
⦈"

definition "dpn_add_local_rule p γ a p1 w1 D ≡ D⦇ labels := insert a (labels D), rules := insert ([p,γ],a,p1#w1) (rules D) ⦈"
definition "dpn_add_spawn_rule p γ a p1 w1 p2 w2 D ≡ D⦇ labels := insert a (labels D), rules := insert ([p,γ],a,p1#w1@sep D#p2#w2) (rules D) ⦈"

lemma dpn_empty_invar[simp]: "⟦finite C; finite S; C∩S={}; s∉C∪S⟧ ⟹ DPN (dpn_empty C S s)"
  apply unfold_locales unfolding dpn_empty_def by auto

lemma dpn_add_local_rule_invar[simp]: 
  assumes A: "{p,p1} ⊆ csyms D" "insert γ (set w1) ⊆ ssyms D" and "DPN D"   
  shows "DPN (dpn_add_local_rule p γ a p1 w1 D)"
proof -
  interpret DPN D "sep D" by fact  
  show ?thesis
    unfolding dpn_add_local_rule_def
    apply unfold_locales
    using sym_finite sym_disjoint lab_finite rules_finite
    apply simp_all
    apply (erule disjE)
    subgoal for r using A by auto
    subgoal for r using rule_fmt[of r] by metis
    done
qed  
  

lemma dpn_add_spawn_rule_invar[simp]: 
  assumes A: "{p,p1,p2} ⊆ csyms D" "insert γ (set w1 ∪ set w2) ⊆ ssyms D" and "DPN D"   
  shows "DPN (dpn_add_spawn_rule p γ a p1 w1 p2 w2 D)"
proof -
  interpret DPN D "sep D" by fact  
  show ?thesis
    unfolding dpn_add_spawn_rule_def
    apply unfold_locales
    using sym_finite sym_disjoint lab_finite rules_finite
    apply (simp_all)
    apply (erule disjE)
    subgoal for r apply (rule disjI2) using A apply clarsimp by (metis in_listsI subset_eq)
    subgoal for r using rule_fmt[of r]  by metis
    done
qed  


subsection ‹ M-automata ›
text ‹
  We are interested in calculating the predecessor sets of regular sets of configurations. For this purpose, the regular sets of configurations are represented as finite state machines, that
  conform to certain constraints, depending on the underlying DPN. These FSMs are called M-automata.
›


subsubsection ‹ Definition ›
record ('s,'c) MFSM_rec = "('s,'c) FSM_rec" +
  sstates :: "'s set"
  cstates :: "'s set"
  sp :: "'s ⇒ 'c ⇒ 's"


text ‹
  M-automata are FSMs whose states are partioned into control and stack states. For each control state $s$ and control symbol $p$, there is a unique and distinguished stack state @{text "sp A s p"}, and a transition
  @{text "(s,p,sp A s p)∈δ"}. The initial state is a control state, and the final states are all stack states.
  Moreover, the transitions are restricted: The only incoming transitions of control states are separator transitions from stack states. 
  The only outgoing transitions are the @{text "(s,p,sp A s p)∈δ"} transitions mentioned above. The @{text "sp A s p"}-states have no other incoming transitions.
›
locale MFSM = DPN M + FSM A 
  for M A +
  
  assumes alpha_cons: "Σ A = csyms M ∪ ssyms M ∪ {♯}"
  assumes states_part: "sstates A ∩ cstates A = {}" "Q A = sstates A ∪ cstates A"
  assumes uniqueSp: "⟦s∈cstates A; p∈csyms M⟧ ⟹ sp A s p ∈ sstates A" "⟦p∈csyms M; p'∈csyms M; s∈cstates A; s'∈cstates A; sp A s p = sp A s' p'⟧ ⟹ s=s' ∧ p=p'"
  assumes delta_fmt: "δ A ⊆ (sstates A × ssyms M × (sstates A - {sp A s p | s p . s∈cstates A ∧ p∈csyms M})) ∪ (sstates A × {♯} × cstates A) ∪ {(s,p,sp A s p) | s p . s∈cstates A ∧ p∈csyms M}"
                     "δ A ⊇ {(s,p,sp A s p) | s p . s∈cstates A ∧ p∈csyms M}"
  assumes s0_fmt: "s0 A ∈ cstates A"
  assumes F_fmt: "F A⊆sstates A" ― ‹ This deviates slightly from \cite{BMT05}, as we cannot represent the empty configuration here. However, this restriction is harmless, since the only predecessor
    of the empty configuration is the empty configuration itself. ›
  constrains M::"('c,'l,'e1) DPN_rec_scheme" 
  constrains A::"('s,'c,'e2) MFSM_rec_scheme"

(* TODO: Some sanity-check that M-automata exist. Ideally, that they exist for every regular language over valid configurations *)
  

lemma (in MFSM) alpha_cons': "Σ A = csyms M ∪ ssyms M ∪ {sep M}" by (unfold sep_fold, rule alpha_cons)
lemma (in MFSM) delta_fmt': "δ A ⊆ (sstates A × ssyms M × (sstates A - {sp A s p | s p . s∈cstates A ∧ p∈csyms M})) ∪ (sstates A × {sep M} × cstates A) ∪ {(s,p,sp A s p) | s p . s∈cstates A ∧ p∈csyms M}"
                     "δ A ⊇ {(s,p,sp A s p) | s p . s∈cstates A ∧ p∈csyms M}" by (unfold sep_fold, (rule delta_fmt)+)


subsubsection ‹ Basic properties ›
lemma (in MFSM) finite_cs_states: "finite (sstates A)" "finite (cstates A)"
proof -
  have "sstates A ⊆ Q A ∧ cstates A ⊆ Q A" by (auto simp add: states_part)
  then show "finite (sstates A)" "finite (cstates A)" by (auto dest: finite_subset intro: finite_states)
qed

lemma (in MFSM) sep_out_syms: "x∈csyms M ⟹ x ≠ ♯" "x∈ssyms M ⟹ x ≠ ♯" by (auto iff add: syms_sep)
lemma (in MFSM) sepI: "⟦x∈Σ A;x∉csyms M; x∉ssyms M⟧ ⟹ x=♯" using alpha_cons by auto
lemma (in MFSM) sep_out_syms': "x∈csyms M ⟹ x ≠ sep M" "x∈ssyms M ⟹ x ≠ sep M" by (unfold sep_fold, (fast dest: sep_out_syms) +)
lemma (in MFSM) sepI': "⟦x∈Σ A;x∉csyms M; x∉ssyms M⟧ ⟹ x=sep M" using alpha_cons' by auto

lemma (in MFSM) states_partI1: "x∈sstates A ⟹ ¬x∈cstates A" using states_part by (auto)
lemma (in MFSM) states_partI2: "x∈cstates A ⟹ ¬x∈sstates A" using states_part by (auto)
lemma (in MFSM) states_part_elim[elim]: "⟦q∈Q A; q∈sstates A ⟹ P; q∈cstates A ⟹ P⟧ ⟹ P" using states_part by (auto)

lemmas (in MFSM) mfsm_cons = sep_out_syms sepI sep_out_syms' sepI' states_partI1 states_partI2 syms_part syms_sep uniqueSp
lemmas (in MFSM) mfsm_cons' = sep_out_syms sepI sep_out_syms' sepI' states_partI1 states_partI2 syms_part uniqueSp

lemma (in MFSM) delta_cases: "⟦(q,p,q')∈δ A; q∈sstates A ∧ p∈ssyms M ∧ q'∈sstates A ∧ q'∉{sp A s p | s p . s∈cstates A ∧ p∈csyms M} ⟹ P; 
                                             q∈sstates A ∧ p=♯ ∧ q'∈cstates A ⟹ P;
                                             q∈cstates A ∧ p∈csyms M ∧ q'=sp A q p ⟹ P⟧ ⟹ P"
  using delta_fmt by auto

lemma (in MFSM) delta_elems: "(q,p,q')∈δ A ⟹ q∈sstates A ∧ ((p∈ssyms M ∧ q'∈sstates A ∧ (q'∉{sp A s p | s p . s∈cstates A ∧ p∈csyms M})) ∨ (p=♯ ∧ q'∈cstates A)) ∨ (q∈cstates A ∧ p∈csyms M ∧ q'=sp A q p)"
  using delta_fmt by auto

lemma (in MFSM) delta_cases': "⟦(q,p,q')∈δ A; q∈sstates A ∧ p∈ssyms M ∧ q'∈sstates A ∧ q'∉{sp A s p | s p . s∈cstates A ∧ p∈csyms M} ⟹ P; 
                                             q∈sstates A ∧ p=sep M ∧ q'∈cstates A ⟹ P;
                                             q∈cstates A ∧ p∈csyms M ∧ q'=sp A q p ⟹ P⟧ ⟹ P"
  using delta_fmt' by auto

lemma (in MFSM) delta_elems': "(q,p,q')∈δ A ⟹ q∈sstates A ∧ ((p∈ssyms M ∧ q'∈sstates A ∧ (q'∉{sp A s p | s p . s∈cstates A ∧ p∈csyms M})) ∨ (p=sep M ∧ q'∈cstates A)) ∨ (q∈cstates A ∧ p∈csyms M ∧ q'=sp A q p)"
  using delta_fmt' by auto


subsubsection ‹ Some implications of the M-automata conditions ›
text ‹ This list of properties is taken almost literally from \cite{BMT05}. ›
text ‹ Each control state @{term s} has @{term "sp A s p"} as its unique @{term p}-successor ›
lemma (in MFSM) cstate_succ_ex: "⟦p∈csyms M; s∈cstates A⟧ ⟹ (s,p,sp A s p) ∈ δ A"
  using delta_fmt by (auto)

lemma (in MFSM) cstate_succ_ex': "⟦p∈csyms M; s∈cstates A; δ A ⊆ D⟧ ⟹ (s,p,sp A s p) ∈ D" using cstate_succ_ex by auto

lemma (in MFSM) cstate_succ_unique: "⟦s∈cstates A; (s,p,x)∈δ A⟧ ⟹ p∈csyms M ∧ x=sp A s p" by (auto elim: delta_cases dest: mfsm_cons')

text ‹ Transitions labeled with control symbols only leave from control states ›
lemma (in MFSM) csym_from_cstate: "⟦(s,p,s')∈δ A; p∈csyms M⟧ ⟹ s∈cstates A" by (auto elim: delta_cases dest: mfsm_cons')


text ‹ @{term s} is the only predecessor of @{term "sp A s p"} ›
lemma (in MFSM) sp_pred_ex: "⟦s∈cstates A; p∈csyms M⟧ ⟹ (s,p,sp A s p)∈δ A" using delta_fmt by auto
lemma (in MFSM) sp_pred_unique: "⟦s∈cstates A; p∈csyms M; (s',p',sp A s p)∈δ A⟧ ⟹ s'=s ∧ p'=p ∧ s'∈cstates A ∧ p'∈csyms M" by (erule delta_cases) (auto dest: mfsm_cons')

text ‹ Only separators lead from stack states to control states ›
lemma (in MFSM) sep_in_between: "⟦s∈sstates A; s'∈cstates A; (s,p,s')∈δ A⟧ ⟹ p=♯" by (auto elim: delta_cases dest: mfsm_cons') 
lemma (in MFSM) sep_to_cstate: "⟦(s,♯,s')∈δ A⟧ ⟹ s∈sstates A ∧ s'∈cstates A" by (auto elim: delta_cases dest: mfsm_cons')


text ‹ Stack states do not have successors labelled with control symbols ›
lemma (in MFSM) sstate_succ: "⟦s∈sstates A; (s,γ,s')∈δ A⟧ ⟹ γ ∉ csyms M" by (auto elim: delta_cases dest: mfsm_cons') 
lemma (in MFSM) sstate_succ2: "⟦s∈sstates A; (s,γ,s')∈δ A; γ≠♯⟧ ⟹ γ∈ssyms M ∧ s'∈sstates A" by (auto elim: delta_cases dest: mfsm_cons')

text ‹ M-automata do not accept the empty word ›
lemma (in MFSM) not_empty[iff]: "[]∉lang A"
  apply (unfold lang_def langs_def)
  apply (clarsimp)
  apply (insert s0_fmt F_fmt)
  apply (subgoal_tac "s0 A = f")
  apply (auto dest: mfsm_cons')
done


text ‹ The paths through an M-automata have a very special form: Paths starting at a stack state are either labelled entirely with stack symbols, or have a prefix labelled with stack symbols followed by a separator ›
lemma (in MFSM) path_from_sstate: "!!s . ⟦s∈sstates A; (s,w,f)∈trclA A⟧ ⟹ (f∈sstates A ∧ w∈lists (ssyms M)) ∨ (∃w1 w2 t. w=w1@♯#w2 ∧ w1∈lists (ssyms M) ∧ t∈sstates A ∧ (s,w1,t)∈trclA A ∧ (t,♯#w2,f)∈trclA A)"
proof (induct w)
  case Nil thus ?case by (subgoal_tac "s=f") auto
next
  case (Cons e w)
  note IHP[rule_format]=this
  then obtain s' where STEP: "(s,e,s')∈(δ A) ∧ s∈Q A ∧ e∈Σ A ∧ (s',w,f)∈trclA A" by (fast dest: trclAD_uncons)
  show ?case proof (cases "e=♯")
    assume "e=♯"
    with IHP have "e#w=[]@♯#w ∧ []∈lists (ssyms M) ∧ s∈sstates A ∧ (s,[],s)∈trclA A ∧ (s,e#w,f)∈trclA A" using states_part by (auto)
    thus ?case by force
  next
    assume "e≠♯"
    with IHP STEP sstate_succ2 have EC: "e∈ssyms M ∧ s'∈sstates A" by blast
    with IHP STEP have "(f ∈ sstates A ∧ w ∈ lists (ssyms M)) ∨ (∃w1 w2 t. w = w1 @ ♯ # w2 ∧ w1 ∈ lists (ssyms M) ∧ t∈sstates A ∧ (s',w1,t)∈trclA A ∧ (t,♯#w2,f)∈trclA A)" (is "?C1∨?C2") by auto
    moreover {
      assume ?C1
      with EC have "f∈sstates A ∧ e#w ∈ lists (ssyms M)" by auto
    } moreover {
      assume ?C2
      then obtain w1 w2 t where CASE: "w = w1 @ ♯ # w2 ∧ w1 ∈ lists (ssyms M) ∧ t∈sstates A ∧ (s',w1,t)∈trclA A ∧ (t,♯#w2,f)∈trclA A" by (fast)
      with EC have "e#w = (e#w1) @ ♯ # w2 ∧ e#w1 ∈ lists (ssyms M)" by auto
      moreover from CASE STEP IHP  have "(s,e#w1,t)∈trclA A" using states_part by auto
      moreover note CASE
      ultimately have "∃w1 w2 t. e#w = w1 @ ♯ # w2 ∧ w1 ∈ lists (ssyms M) ∧ t∈sstates A ∧ (s,w1,t)∈trclA A ∧ (t,♯#w2,f)∈trclA A" by fast
    } ultimately show ?case by blast
  qed
qed

text ‹ Using @{thm [source] MFSM.path_from_sstate}, we can describe the format of paths from control states, too.
  A path from a control state @{term s} to some final state starts with a transition @{term "(s,p,sp A s p)"} for some control symbol @{term p}. It then continues with a sequence of transitions labelled by stack symbols.
  It then either ends or continues with a separator transition, bringing it to a control state again, and some further transitions from there on. 
›
lemma (in MFSM) path_from_cstate: 
  assumes A: "s∈cstates A" "(s,c,f)∈trclA A" "f∈sstates A"
  assumes SINGLE: "!! p w . ⟦c=p#w; p∈csyms M; w∈lists (ssyms M); (s,p,sp A s p)∈δ A; (sp A s p,w,f)∈trclA A⟧ ⟹ P"
  assumes CONC: "!! p w cr t s' . ⟦c=p#w@♯#cr; p∈csyms M; w∈lists (ssyms M); t∈sstates A; s'∈cstates A; (s,p,sp A s p)∈δ A; (sp A s p,w,t)∈trclA A; (t,♯,s')∈δ A; (s',cr,f)∈trclA A⟧ ⟹ P"
  shows "P"
proof (cases c)
  case Nil thus P using A by (subgoal_tac "s=f", auto dest: mfsm_cons')
next
  case (Cons p w) note CFMT=this
  with cstate_succ_unique A have SPLIT: "p∈csyms M ∧ (s,p,sp A s p)∈δ A ∧ (sp A s p,w,f)∈trclA A" by (blast dest: trclAD_uncons)
  with path_from_sstate A CFMT uniqueSp have CASES: "(f∈sstates A ∧ w∈lists (ssyms M)) ∨ (∃w1 w2 t. w=w1@♯#w2 ∧ w1∈lists (ssyms M) ∧ t∈sstates A ∧ (sp A s p,w1,t)∈trclA A ∧ (t,♯#w2,f)∈trclA A)" (is "?C1 ∨ ?C2") by blast
  moreover {
    assume CASE: ?C1
    with SPLIT SINGLE A CFMT have P by fast
  } moreover {
    assume CASE: ?C2
    then obtain w1 w2 t where WFMT: "w=w1@♯#w2 ∧ w1∈lists (ssyms M) ∧ t∈sstates A ∧ (sp A s p,w1,t)∈trclA A ∧ (t,♯#w2,f)∈trclA A" by fast
    with sep_to_cstate obtain s' where "s'∈cstates A ∧ (t,♯,s')∈δ A ∧ (s',w2,f)∈trclA A" by (fast dest: trclAD_uncons)
    with SPLIT CASE WFMT have "p#w=p#w1@♯#w2 ∧ p∈csyms M ∧ w1∈lists (ssyms M) ∧ t∈sstates A ∧ s'∈cstates A ∧ (s,p,sp A s p)∈δ A ∧ (sp A s p,w1,t)∈trclA A ∧ (t,♯,s')∈δ A ∧ (s',w2,f)∈trclA A" by auto
    with CFMT CONC have P by (fast)
  } ultimately show P by blast
qed


subsection ‹ $pre^*$-sets of regular sets of configurations ›
text ‹ Given a regular set @{term L} of configurations and a set @{term "Δ"} of string rewrite rules, @{text "pre* Δ L"} is the set of configurations that can be rewritten to some configuration in @{term L}, using rules from
  @{term "Δ"} arbitrarily often.

  We first define this set inductively based on rewrite steps, and then provide the characterization described above as a lemma.
 ›

inductive_set "pre_star" :: "('c,'l) SRS ⇒ ('s,'c,'e) FSM_rec_scheme ⇒ 'c list set" ("pre*") 
  for Δ L
where
  pre_refl: "c∈lang L ⟹ c∈pre* Δ L" |
  pre_step: "⟦c'∈pre* Δ L; (c,a,c')∈tr Δ⟧ ⟹ c∈pre* Δ L"

text ‹ Alternative characterization of @{term "pre* Δ L"} › (* FIXME: Proof is not nice *)
lemma pre_star_alt: "pre* Δ L = {c . ∃c'∈lang L . ∃as . (c,as,c')∈trcl (tr Δ)}"
proof - 
  {
    fix x c' as
    have "⟦x ↪⇘as⇙ c' ∈ trcl (tr Δ); c' ∈ lang L⟧ ⟹ x ∈ pre* Δ L"
      by (induct rule: trcl.induct) (auto intro: pre_step pre_refl)
  }  
  then show ?thesis
    by (auto elim!: pre_star.induct intro: trcl.intros)
  
qed

lemma pre_star_altI: "⟦c'∈lang L; c↪⇘as⇙ c'∈trcl (tr Δ)⟧ ⟹ c∈pre* Δ L" by (unfold pre_star_alt, auto)
lemma pre_star_altE: "⟦c∈pre* Δ L; !!c' as. ⟦c'∈lang L; c↪⇘as⇙ c'∈trcl (tr Δ)⟧ ⟹ P⟧ ⟹ P" by (unfold pre_star_alt, auto)


subsection ‹ Nondeterministic algorithm for pre$^*$›
text ‹
  In this section, we formalize the saturation algorithm for computing @{term "pre* Δ L"} from \cite{BMT05}.
  Roughly, the algorithm works as follows: 
  \begin{enumerate}
    \item Set @{term "D=δ A"}
    \item Choose a rule @{term "[p,γ]↪⇘a⇙ c' ∈ rules M"} and states @{text "q,q'∈Q A"}, such that @{term D} can read the configuration @{term "c'"} from state @{term "q"} and end in state @{term "q'"} 
      (i.e. @{term "(q,c',q')∈trclAD A D"}) and such that @{term "(sp A q p,γ,q')∉D"}. If this is not possible, terminate.
    \item Add the transition @{term "(sp A q p,γ,q')∉D"} to @{term D} and continue with step 2
  \end{enumerate}

  Intuitively, the behaviour of this algorithm can be explained as follows: 
    If there is a configuration @{term "c1@c'@c2 ∈ pre* Δ L"}, and a rule @{term "p#γ ↪⇘a⇙ c' ∈ Δ"}, then we also have @{term "c1@p#γ@c2∈pre* Δ L"}. The effect of step 3 is exactly adding
    these configurations @{term "c1@p#γ@c22"} to the regular set of configurations.

  We describe the algorithm nondeterministically by its step relation @{text "ps_R"}. Each step describes the addition of one transition.
›

text ‹
  In this approach, we directly restrict the domain of the step-relation to transition relations below some upper bound @{text "ps_upper"}.
  We will later show, that the initial transition relation of an M-automata is below this upper bound, and that the step-relation preserves the property of being below this upper bound.  
  
  We define  @{term "ps_upper M A"} as a finite set, and show that the initial transition relation @{term "δ A"} of an M-automata is below @{term "ps_upper M A"}, 
  and that @{term "ps_R M A"} preserves the property of being below the finite set @{term "ps_upper M A"}.
  Note that we use the more fine-grained @{term "ps_upper M A"} as upper bound for the termination proof rather than @{term "Q A × Σ A × Q A"}, as @{text "sp A q p"} is only specified
  for control states @{text "q"} and control symbols @{text "p"}. Hence we need the finer structure of @{term "ps_upper M A"} to guarantee that @{text "sp"} is only applied
  to arguments it is specified for. Anyway, the fine-grained @{term "ps_upper M A"} bound is also needed for the correctness proof.
›
definition ps_upper :: "('c,'l,'e1) DPN_rec_scheme ⇒ ('s,'c,'e2) MFSM_rec_scheme ⇒ ('s,'c) LTS" where
  "ps_upper M A == (sstates A × ssyms M × sstates A) ∪ (sstates A × {sep M} × cstates A) ∪ {(s,p,sp A s p) | s p . s∈cstates A ∧ p∈csyms M}"

inductive_set ps_R :: "('c,'l,'e1) DPN_rec_scheme ⇒ ('s,'c,'e2) MFSM_rec_scheme ⇒ (('s,'c) LTS * ('s,'c) LTS) set" for M A 
where
  "⟦[p,γ]↪⇘a⇙ c' ∈ rules M; (q,c',q')∈trclAD A D; (sp A q p,γ,q')∉D; D⊆ps_upper M A⟧ ⟹ (D,insert (sp A q p,γ,q') D)∈ps_R M A"

lemma ps_R_dom_below: "(D,D')∈ps_R M A ⟹ D⊆ps_upper M A" by (auto elim: ps_R.cases)

subsubsection ‹ Termination ›

text ‹
  Termination of our algorithm is equivalent to well-foundedness of its (converse) step relation, that is, we have to show @{term "wf ((ps_R M A)¯)"}.
  
  In the following, we also establich some properties of transition relations below @{term "ps_upper M A"}, that will be used later in the correctness proof.
›

lemma (in MFSM) ps_upper_cases: "⟦(s,e,s')∈ps_upper M A;
  ⟦s∈sstates A; e∈ssyms M; s'∈sstates A⟧ ⟹ P;
  ⟦s∈sstates A; e=♯; s'∈cstates A⟧ ⟹ P;
  ⟦s∈cstates A; e∈csyms M; s'=sp A s e⟧ ⟹ P
⟧ ⟹ P" 
  by (unfold ps_upper_def sep_def, auto)

lemma (in MFSM) ps_upper_cases': "⟦(s,e,s')∈ps_upper M A;
  ⟦s∈sstates A; e∈ssyms M; s'∈sstates A⟧ ⟹ P;
  ⟦s∈sstates A; e=sep M; s'∈cstates A⟧ ⟹ P;
  ⟦s∈cstates A; e∈csyms M; s'=sp A s e⟧ ⟹ P
⟧ ⟹ P" 
  apply (rule ps_upper_cases)
  by (unfold sep_def) auto

lemma (in MFSM) ps_upper_below_trivial: "ps_upper M A ⊆ Q A × Σ A × Q A" by (unfold ps_upper_def, auto simp add: states_part alpha_cons uniqueSp sep_def)

lemma (in MFSM) ps_upper_finite: "finite (ps_upper M A)" using ps_upper_below_trivial finite_delta_dom by (auto simp add: finite_subset)

text ‹ The initial transition relation of the M-automaton is below @{term "ps_upper M A"} ›
lemma (in MFSM) initial_delta_below: "δ A ⊆ ps_upper M A" using delta_fmt by (unfold ps_upper_def sep_def) auto


text ‹ Some lemmas about structure of transition relations below @{term "ps_upper M A"} ›
lemma (in MFSM) cstate_succ_unique': "⟦s∈cstates A; (s,p,x)∈D; D⊆ps_upper M A⟧ ⟹ p∈csyms M ∧ x=sp A s p" by (auto elim: ps_upper_cases dest: mfsm_cons')
lemma (in MFSM) csym_from_cstate': "⟦(s,p,s')∈D; D⊆ps_upper M A; p∈csyms M⟧ ⟹ s∈cstates A" by (auto elim: ps_upper_cases dest: mfsm_cons')

text ‹ The only way to end up in a control state is after executing a separator. ›
lemma (in MFSM) ctrl_after_sep: assumes BELOW: "D ⊆ ps_upper M A"
  assumes A: "(q,c',q')∈trclAD A D"    "c'≠[]"
  shows "q'∈cstates A = (last c' = ♯)"
proof -
  from A have "(q,butlast c' @ [last c'],q')∈trclAD A D" by auto
  with A obtain qh where "(qh,[last c'],q')∈trclAD A D" by (blast dest: trclAD_unconcat)
  hence "(qh,last c',q')∈ D" by (fast dest: trclAD_single)
  with BELOW have IS: "(qh,last c',q')∈ps_upper M A" by fast
  thus ?thesis by (erule_tac ps_upper_cases) (auto dest: mfsm_cons' simp add: sep_out_syms) (* This proof behaves somewhat odd, perhaps there's something in simp/dest that makes problems. *)
qed  

text ‹ When applying a rules right hand side to a control state, we will get to a stack state ›
lemma (in MFSM) ctrl_rule: assumes BELOW: "D ⊆ ps_upper M A"
  assumes A: "([p,γ],a,c')∈rules M" and B: "q∈cstates A" "(q,c',q')∈trclAD A D"
  shows "q'∈sstates A"
proof -
  from A show ?thesis
  proof (cases rule: rule_cases)
    case (no_spawn p γ a p' w)
    hence C: "q ↪⇘p' # w⇙ q' ∈ trclAD A D" "∀x∈set w. x ∈ ssyms M" "p' ∈ csyms M" using B by auto
    hence "last (p'#w) ≠ ♯ ∧ q'∈Q A" by (unfold sep_def) (auto dest: mfsm_cons' trclAD_elems)
    with C BELOW ctrl_after_sep[of D q "p'#w" q'] show "(q' ∈ sstates A)" by (fast dest: mfsm_cons')
  next
    case (spawn p γ a p1 w1 p2 w2)
    hence C: "q ↪⇘p1 # w1 @ ♯ # p2 # w2⇙ q' ∈ trclAD A D" "∀x∈set w2. x ∈ ssyms M" "p2 ∈ csyms M" using B by auto
    hence "last (p1 # w1 @ ♯ # p2 # w2) ≠ sep M ∧ q'∈Q A" by (auto dest: mfsm_cons' trclAD_elems)
    with C BELOW ctrl_after_sep[of D q "p1 # w1 @ ♯ # p2 # w2" q'] show "(q' ∈ sstates A)" by (unfold sep_def, fast dest: mfsm_cons')
  qed
qed


text ‹ @{term "ps_R M A"} preserves the property of being below @{term "ps_upper M A"}, and the transition relation becomes strictly greater in each step ›
lemma (in MFSM) ps_R_below: assumes E: "(D,D')∈ps_R M A" 
  shows "D⊂D' ∧ D' ⊆ ps_upper M A"
proof -
  from E have BELOW: "D⊆ps_upper M A" by (simp add: ps_R_dom_below)

  {
    fix p γ a c' q q'
    assume A: "[p, γ] ↪⇘a⇙ c' ∈ rules M" "q ↪⇘c'⇙ q' ∈ trclAD A D"
    obtain p' cr' where CSPLIT: "p∈csyms M ∧ p'∈csyms M ∧ c'=p'#cr' ∧ γ∈ssyms M" by (insert A) (erule rule_cases, fast+)
    with BELOW A obtain qh where SPLIT: "(q,p',qh)∈D" "(q,p',qh)∈ps_upper M A" by (fast dest: trclAD_uncons)
    with CSPLIT have QC: "q∈cstates A ∧ qh=sp A q p'" by (auto elim: ps_upper_cases dest: syms_part iff add: syms_sep)
    with BELOW A ctrl_rule[of D p γ a c' q q'] have Q'S: "q'∈sstates A" by simp
    from QC CSPLIT have "sp A q p ∈ sstates A" by (simp add: uniqueSp)
    with Q'S CSPLIT have "sp A q p ↪⇘γ⇙ q' ∈ ps_upper M A" by (unfold ps_upper_def, simp)
  }
  with E show ?thesis by (auto elim!: ps_R.cases)
qed

text ‹ As a result of this section, we get the well-foundedness of @{term "ps_R M A"}, 
  and that the transition relations that occur during the saturation algorithm stay above the initial transition relation @{term "δ A"} and below @{term "ps_upper M A"}›
theorem (in MFSM) ps_R_wf: "wf ((ps_R M A)¯)" using ps_upper_finite sat_wf[where α=id, simplified] ps_R_below by (blast)

theorem (in MFSM) ps_R_above_inv: "is_inv (ps_R M A) (δ A) (λD. δ A ⊆ D)" by (auto intro: invI elim: ps_R.cases)

theorem (in MFSM) ps_R_below_inv: "is_inv (ps_R M A) (δ A) (λD. D⊆ps_upper M A)" by (rule invI) (auto simp add: initial_delta_below ps_R_below) 

text ‹ We can also show that the algorithm is defined for every possible initial automata ›
theorem (in MFSM) total: "∃D. (δ A, D)∈ndet_algo(ps_R M A)" using ps_R_wf ndet_algo_total by blast

subsubsection ‹ Soundness ›
text ‹
  The soundness (over-approximation) proof works by induction over the definition of @{text "pre*"}. 
  
  In the reflexive case, a configuration from the original language is also in the saturated language, because no transitions are killed
  during saturation.

  In the step case, we assume that a configuration @{text "c'"} is in the saturated language, and show for a rewriting step @{text "c↪ac'"} that also @{text c} is in the saturated language. 
›
theorem (in MFSM) sound: "⟦c∈pre_star (rules M) A; (δ A,s')∈ndet_algo (ps_R M A)⟧ ⟹ c∈lang (A⦇ δ:=s' ⦈)" (*is "⟦_;_⟧⟹_ ∈ lang ?A'"*)
proof -
  let ?A' = "A⦇ δ:=s' ⦈"
  assume A:"(δ A,s')∈ndet_algo (ps_R M A)"
  ― ‹Some little helpers›
  from A ps_R_above_inv have SUBSET: "δ A ⊆ s'" by (unfold ndet_algo_def) (auto dest: inv)
  have TREQ: "!!D . trclAD A D = trclAD ?A' D" by (rule trclAD_eq, simp_all)
  from A ps_R_below_inv have SATSETU: "δ ?A' ⊆ ps_upper M A" by (erule_tac ndet_algoE) (auto dest: inv iff add: initial_delta_below) 

  assume "c∈pre_star (rules M) A"
  ― ‹ Make an induction over the definition of @{term "pre*"} ›
  thus ?thesis proof (induct c rule: pre_star.induct)
    fix c assume "c∈lang A" (*case (pre_refl c)*) ― ‹Reflexive case: The configuration comes from the original regular language›
    then obtain f where F: "f∈F A ∧ (s0 A,c,f)∈trclA A" by (unfold lang_def langs_def, fast) ― ‹ That is, @{term c} can bring the initial automata from its start state to some final state @{term f} ›
    with SUBSET trclAD_mono_adv[of "δ A" "s'" A ?A'] have "(s0 A,c,f)∈trclA ?A'" by (auto) ― ‹ Because the original transition relation @{term "δ A"} is a subset of the saturated one @{term "s'"} (@{thm [source] SUBSET}) and 
      the transitive closure is monotonous, @{term "(s0 A,c,f)"} is also in the transitive closure of the saturated transition relation ›
    with F show "c∈lang ?A'" by (unfold lang_def langs_def) auto ― ‹ and thus in the language of the saturated automaton ›
  next
    ― ‹Step case: ›
    fix a c c' 
    assume IHP: "c' ∈ pre* (rules M) A" "(c, a, c') ∈ tr (rules M)" ― ‹ We take some configurations @{term "c"} and @{term "c' ∈ pre* (rules M) A"} and assume that @{term "c"} can be rewritten to @{term "c'"} in one step ›
      "c' ∈ lang ?A'" ― ‹ We further assume that @{term "c'"} is in the saturated language, and we have to show that also @{term c} is in that language ›

    from IHP obtain f where F: "f∈F ?A' ∧ (s0 ?A',c',f) ∈ trclA ?A'" by (unfold lang_def langs_def, fast) ― ‹ Unfolding the definition of @{term "lang"} ›
    from IHP obtain w1 w2 r r' where CREW: "c=w1@(r@w2) ∧ c'=w1@(r'@w2) ∧ (r,a,r')∈rules M" by (auto elim!: tr.cases) ― ‹ Get the rewrite rule that rewrites @{term c} to @{term "c'"} ›
    then obtain p γ p' w' where RFMT: "p∈csyms M ∧ p'∈csyms M ∧ γ∈ssyms M ∧ r=[p,γ] ∧ r'=p'#w'" by (auto elim!: rule_cases) ― ‹ This rewrite rule rewrites some control symbol @{term p} followed by a stack symbol @{term "γ"} to 
      another control symbol @{term "p'"} and a sequence of further symbols @{term "w'"} ›
    with F CREW obtain q qh q' where SPLIT: "(s0 ?A',w1,q)∈trclA ?A' ∧ (q,p'#w',q')∈trclA ?A' ∧ (q',w2,f)∈trclA ?A' ∧ (q,p',qh)∈δ ?A'" 
      by (blast dest: trclAD_unconcat trclAD_uncons) ― ‹ Get the states in the transition relation generated by the algorithm, that correspond to the splitting of @{term "c'"} as established in @{thm [source] CREW} ›


    have SHORTCUT: "(q,[p,γ],q')∈trclA ?A'" ― ‹ In the transition relation generated by our algorithm, we can get from @{term q} to @{term "q'"} also by @{term "[p,γ]"} ›
    proof -
      have S1: "(q,p,sp A q p)∈δ ?A'" and QINC: "q∈cstates A" ― ‹ The first transition, from @{term q} with @{term p} to @{term "sp A q p"} is already contained in the initial M-automata. 
        We also need to know for further proofs, that @{term q} is a control state. ›
      proof -
        from SPLIT SATSETU have "(q,p',qh)∈ps_upper M A" by auto
        with RFMT show "q∈cstates A" by (auto elim!: ps_upper_cases dest: mfsm_cons' simp add: sep_def)
        with RFMT have "(q,p,sp A q p)∈δ A" by (fast intro: cstate_succ_ex)
        with SUBSET show "(q,p,sp A q p)∈δ ?A'" by auto
      qed
      moreover
      have S2: "(sp A q p,γ,q')∈δ ?A'" ― ‹ The second transition, from @{term "sp A q p"} with @{term "γ"} to @{term "q'"} has been added during the algorithm's execution ›
      proof -
        from A have "s'∉Domain (ps_R M A)" by (blast dest: termstate_ndet_algo)
        moreover from CREW RFMT SPLIT TREQ SATSETU have "(sp A q p,γ,q')∉s' ⟹ (s',insert (sp A q p,γ,q') s') ∈ (ps_R M A)" by (auto intro: ps_R.intros)
        ultimately show ?thesis by auto
      qed
      moreover
      have "sp A q p ∈ Q ?A' ∧ q'∈Q ?A' ∧ q∈Q ?A' ∧ p∈Σ ?A' ∧ γ∈Σ ?A'" ― ‹The intermediate states and labels have also the correct types›        
      proof -
        from S2 SATSETU have "(sp A q p,γ,q')∈ps_upper M A" by auto
        with QINC RFMT show ?thesis by (auto elim: ps_upper_cases dest: mfsm_cons' simp add: states_part alpha_cons)
      qed
      ultimately show ?thesis by simp
    qed

    have "(s0 ?A',w1@(([p,γ])@w2),f)∈trclA ?A'" ― ‹ Now we put the pieces together and construct a path from @{term "s0 A"} with @{term "w1"} to @{term q}, from there 
      with @{term "[p,γ]"} to @{term q'} and then with @{term w2} to the final state @{term f} ›    
    proof -
      from SHORTCUT SPLIT have "(q,([p,γ])@w2,f)∈trclA ?A'" by (fast dest: trclAD_concat)
      with SPLIT show ?thesis by (fast dest: trclAD_concat)
    qed
    with CREW RFMT have "(s0 ?A',c,f)∈trclA ?A'" by auto ― ‹ this is because @{term "c = w1@[p,γ]@w2"} ›
    with F show "c∈lang ?A'" by (unfold lang_def langs_def, fast) ― ‹ And thus @{term c} is in the language of the saturated automaton ›
  qed
qed

subsubsection ‹ Precision ›

text ‹
  In this section we show the precision of the algorithm, that is we show that the saturated language is below the backwards reachable set.
›

text ‹ 
  The following induction scheme makes an induction over the number of occurences of a certain transition in words accepted by a FSM: 

  To prove a proposition for all words from state @{term "qs"} to state @{term "qf"} in FSM @{term A} that has a transition rule @{term "(s,a,s')∈δ A"}, we have to show the following:
  \begin{itemize}
    \item Show, that the proposition is valid for words that do not use the transition rule @{term "(s,a,s')∈δ A"} at all
    \item Assuming that there is a prefix @{term "wp"} from @{term "qs"} to @{term "s"} and a suffix @{term "ws"} from @{term "s'"} to @{term "qf"}, and that @{term "wp"} does not use the new rule,
       and further assuming that for all prefixes @{term "wh"} from @{term "qs"} to @{term "s'"}, the proposition holds for @{term "wh@ws"}, show that the proposition also holds for
       @{term "wp@a#ws"}.
  \end{itemize}

  We actually do use @{term D} here instead of @{term "δ A"}, for use with @{term "trclAD"}.
›
lemma ins_trans_induct[consumes 1, case_names base step]:
  fixes qs and qf
  assumes A: "(qs,w,qf)∈trclAD A (insert (s,a,s') D)"
  assumes BASE_CASE: "!! w . (qs,w,qf)∈trclAD A D ⟹ P w"
  assumes STEP_CASE: "!! wp ws . ⟦(qs,wp,s)∈trclAD A D; (s',ws,qf)∈trclAD A (insert (s,a,s') D); !! wh . (qs,wh,s')∈trclAD A D ⟹ P (wh@ws)⟧ ⟹ P (wp@a#ws)"
  shows "P w"
proof -
  ― ‹ Essentially, the proof works by induction over the suffix @{term "ws"} ›
  {
    fix ws
    have "!!qh wp. ⟦(qs,wp,qh)∈trclAD A D; (qh,ws,qf)∈trclAD A (insert (s,a,s') D)⟧ ⟹ P (wp@ws)" proof (induct ws)
      case (Nil qh wp) with BASE_CASE show ?case by (subgoal_tac "qh=qf", auto)
    next
      case (Cons e w qh wp) note IHP=this
      then obtain qhh where SPLIT: "(qh,e,qhh)∈(insert (s ↪⇘a⇙ s') D) ∧ (qhh,w,qf)∈trclAD A (insert (s ↪⇘a⇙ s') D) ∧ qh∈Q A ∧ e∈Σ A" by (fast dest: trclAD_uncons)
      show ?case proof (cases "(qh,e,qhh) = (s,a,s')")
        case False 
        with SPLIT have "(qh,[e],qhh)∈trclAD A D" by (auto intro: trclAD_one_elem dest: trclAD_elems)
        with IHP have "(qs,wp@[e],qhh)∈trclAD A D" by (fast intro: trclAD_concat)
        with IHP SPLIT have "P ((wp@[e])@w)" by fast
        thus ?thesis by simp
      next
        case True note CASE=this
        with SPLIT IHP have "(qs,wp,s) ∈ trclAD A D ∧ s' ↪⇘w⇙ qf ∈ trclAD A (insert (s ↪⇘a⇙ s') D)" "!!wh. (qs,wh,s')∈trclAD A D ⟹ P (wh@w)" by simp_all
        with STEP_CASE CASE show ?thesis by simp
      qed
    qed
  } note C=this
  from A C[of "[]" qs w] show ?thesis by (auto dest: trclAD_elems)
qed


text ‹ 
  The following lemma is a stronger elimination rule than @{thm [source] ps_R.cases}. It makes a more fine-grained distinction.
  In words: A step of the algorithm adds a transition  @{term "(sp A q p,γ,s')"}, if there is a rule @{term "[p,γ]↪⇘a⇙ p'#c'"}, and a transition sequence @{term "(q,p'#c',s')∈trclAD A D"}. That is, if we have 
  @{term "(sp A q p',c',s')∈trclAD A D"}.
 ›

lemma (in MFSM) ps_R_elims_adv: 
  assumes "(D,D')∈ps_R M A"
  obtains γ s' a p' c' p q where 
    "D'=insert (sp A q p,γ,s') D" "(sp A q p,γ,s')∉D" "[p,γ]↪⇘a⇙ p'#c' ∈ rules M" "(q,p'#c',s')∈trclAD A D"
    "p∈csyms M" "γ∈ssyms M" "q∈cstates A" "p'∈csyms M" "a∈labels M" "(q,p',sp A q p')∈D" "(sp A q p',c',s')∈trclAD A D"
  using assms  
proof (cases rule: ps_R.cases)
  case A: (1 p γ a c' q q')
  then obtain p' cc' where RFMT: "p∈csyms M ∧ c'=p'#cc' ∧ p'∈csyms M ∧ γ∈ssyms M ∧ a∈labels M" by (auto elim!: rule_cases)
  with A obtain qh where SPLIT: "(q,p',qh)∈D ∧ (qh,cc',q')∈ trclAD A D" by (fast dest: trclAD_uncons)
  with A RFMT have "q∈cstates A ∧ qh=sp A q p'" by (subgoal_tac "(q,p',qh)∈ps_upper M A") (auto elim!: ps_upper_cases dest: syms_part sep_out_syms)
  then show ?thesis using A RFMT SPLIT that by blast
qed

text ‹ Now follows a helper lemma to establish the precision result. In the original paper \cite{BMT05} it is called the {\em crucial point} of the precision proof.

  It states that for transition relations that occur during the execution of the algorithm, for each word @{term w} that leads from the start state to a state @{term "sp A q p"}, there is a word
  @{term "ws@[p]"} that leads to @{term "sp A q p"} in the initial automaton and @{term w} can be rewritten to @{term "ws@[p]"}.

  In the initial transition relation, a state of the form @{term "sp A q p"} has only one incoming edge labelled @{term "p"} (@{thm [source] MFSM.sp_pred_ex MFSM.sp_pred_unique}).
  Intuitively, this lemma explains why it is correct to add further incoming edges to @{term "sp A q p"}: All words using such edges can be rewritten to a word using the original edge.  
›

lemma (in MFSM) sp_property:
  shows "is_inv (ps_R M A) (δ A) (λD. 
     (∀ w . ∀p∈csyms M. ∀q∈cstates A. (s0 A,w,sp A q p)∈trclAD A D ⟶ (∃ws as. (s0 A,ws,q)∈trclA A ∧ (w,as,ws@[p])∈trcl (tr (rules M)))) ∧ 
     (∀P'. is_inv (ps_R M A) (δ A) P' ⟶ P' D))"
  ― ‹We show the thesis by proving that it is an invariant of the saturation procedure›
proof (rule inv_useI; intro allI ballI impI conjI)  
  ― ‹Base case, show the thesis for the initial automata ›
  fix w p q
  assume A: "p ∈ csyms M" "q ∈ cstates A" "s0 A ↪⇘w⇙ sp A q p ∈ trclA A"
  show "∃ws as. s0 A ↪⇘ws⇙ q ∈ trclA A ∧ (w,as,ws@[p])∈trcl (tr (rules M))" 
  proof (cases w rule: rev_cases) ― ‹ Make a case distinction wether @{term w} is empty ›
    case Nil ― ‹ @{term w} cannot be empty, because @{term "s0"} is a control state, and @{term "sp"} is a stack state, and by definition of M-automata, these cannot be equal ›
    with A have "s0 A = sp A q p" by (auto)
    with A s0_fmt uniqueSp have False by (auto dest: mfsm_cons')
    thus ?thesis ..
  next
    case (snoc ws p') note CASE=this 
    with A obtain qh where "(s0 A,ws,qh)∈trclA A ∧ (qh,[p'],sp A q p)∈trclA A ∧ (qh,p',sp A q p)∈δ A" by (fast dest: trclAD_unconcat trclAD_single) ― ‹ Get the last state @{term "qh"} and 
      symbol @{term "p'"} before reaching @{term "sp"} ›
    moreover with A have "p=p' ∧ qh=q" by (blast dest: sp_pred_unique) ― ‹ This symbol is @{term p}, because the @{term p}-edge from @{term q} is the only edge to @{term "sp A q p"} in an M-automata ›
    moreover with CASE have "(w,[],ws@[p]) ∈ trcl (tr (rules M))" by (fast intro: trcl.empty)
    ultimately show ?thesis by (blast)
  qed
next
  ― ‹ Step case ›
  fix D1 D2 w p q
  assume 
    IH: "∀w. ∀p∈csyms M. ∀q∈cstates A. s0 A ↪⇘w⇙ sp A q p ∈ trclAD A D1 
      ⟶ (∃ws as. s0 A ↪⇘ws⇙ q ∈ trclAD A (δ A) ∧ (w ↪⇘as⇙ ws @ [p] ∈ trcl (tr (rules M))))" ― ‹ By induction hypothesis, our proposition is valid for @{term "D1"} ›
    and SUCC: "(D1,D2)∈ps_R M A" ― ‹ We have to show the proposition for some @{term "D2"}, that is a successor state of @{term "D1"} w.r.t. @{term "ps_R M A"} ›
    and P1: "p ∈ csyms M" "q ∈ cstates A" and P2: "s0 A ↪⇘w⇙ sp A q p ∈ trclAD A D2" ― ‹ Premise of our proposition: We reach some state @{term "sp A q p"} › 
    and USE_INV: "⋀P'. is_inv (ps_R M A) (δ A) P' ⟹ P' D1" ― ‹ We can use known invariants ›

  from SUCC have SS: "D1 ⊆ ps_upper M A" by (blast dest: ps_R_dom_below)
  from USE_INV have A2: "δ A ⊆ D1" by (blast intro: ps_R_above_inv)

  from SUCC obtain γ s' pp aa cc' qq where ADD: "insert (sp A qq pp,γ,s') D1 = D2 ∧ (sp A qq pp,γ,s')∉D1" and 
                                           RCONS: "([pp,γ],aa,cc')∈rules M ∧ (qq,cc',s')∈trclAD A D1 ∧ qq∈cstates A ∧ pp∈csyms M ∧ aa∈labels M"
    by (blast elim!: ps_R_elims_adv) ― ‹ Because of @{thm [source] SUCC}, we obtain @{term "D2"} by adding a (new) transition @{term "(sp A qq pp,γ,s')"} to @{term "D1"}, such that there is a rule 
    @{term "[pp,γ]↪⇘aa⇙ cc' ∈ rules M"} and the former transition relation can do @{term "(qq,cc',s')∈trclAD A D1"} ›
  from P2 ADD have P2': "s0 A ↪⇘w⇙ sp A q p ∈ trclAD A (insert (sp A qq pp ↪⇘γ⇙ s') D1)" by simp
      
  show "∃ws as. s0 A ↪⇘ws⇙ q ∈ trclA A ∧ w ↪⇘as⇙ ws @ [p] ∈ trcl (tr (rules M))" using P2' 
    ― ‹ We show the proposition by induction on how often the new rule was used. For this, we regard a prefix until the first usage of the added rule, and a suffix that may use the added rule arbitrarily often ›
  proof (induction rule: ins_trans_induct)
    case (base) ― ‹ Base case, the added rule is not used at all. The proof is straighforward using the induction hypothesis of the outer (invariant) induction ›
    thus ?case using IH P1 by simp
  next
    fix wpre wsfx ― ‹ Step case: We have a prefix that does not use the added rule, then a usage of the added rule and a suffix. 
      We know that our proposition holds for all prefixes that do not use the added rule. ›
    assume IP1: "(s0 A,wpre, sp A qq pp) ∈ trclAD A D1" and IP2: "(s', wsfx, sp A q p) ∈ trclAD A (insert (sp A qq pp, γ, s') D1)"
    assume IIH: "!!wh. (s0 A, wh, s') ∈ trclAD A D1 ⟹ ∃ws as. (s0 A, ws, q) ∈ trclAD A (δ A) ∧ ((wh @ wsfx, as, ws @ [p]) ∈ trcl (tr (rules M)))"
    from IP1 IH RCONS obtain wps aps where C1: "(s0 A,wps,qq) ∈ trclAD A (δ A) ∧ wpre ↪⇘aps⇙ wps @ [pp] ∈ trcl (tr (rules M))" by fast ― ‹ This is an instance of a configuration reaching a sp-state, 
      thus by induction hypothesis of the outer (invariant) induction, we find a successor configuration @{term "wps@[pp]"} that reaches this state using @{term "pp"} as last edge in @{term "δ A"} ›
    with A2 have "(s0 A,wps,qq) ∈ trclAD A D1" by (blast dest: trclAD_mono) ― ‹ And because @{thm "A2"}, we can do the transitions also in @{term "D1"} ›
    with RCONS have "(s0 A,wps@cc', s') ∈ trclAD A D1" by (blast intro: trclAD_concat) ― ‹ From above (@{thm [source] RCONS}) we know @{term "(qq,cc',s')∈trclAD A D1"}, and we can concatenate these transition sequences ›
    then obtain ws as where C2: "(s0 A,ws,q) ∈ trclAD A (δ A) ∧ (wps@cc') @ wsfx ↪⇘as⇙ ws @ [p] ∈ trcl (tr (rules M))" by (fast dest: IIH) ― ‹ This concatenation is a prefix to a usage of the added transition, 
      that does not use the added transition itself. (The whole configuration bringing us to @{term "sp A q p"} is @{term "wps@cc'@wsfx"}). 
      For those prefixes, we can apply the induction hypothesis of the inner induction and obtain a configuration @{term "ws@[p]"} that is a successor configuration of @{term "wps@cc'@wsfx"}, and with which 
      we can reach @{term "sp A q p"} using @{term p} as last edge ›

    have "∃as. wpre @ γ # wsfx ↪⇘as⇙ ws @ [p] ∈ trcl (tr (rules M))" ― ‹ Now we obtained some configuration @{term "ws@[p]"}, that reaches @{term "sp A q p"} using @{term p} as last edge in @{term "δ A"}. 
      Now we show that this is indeed a successor configuration of @{term "wpre@γ#wsfx"}. ›
    proof -
      ― ‹ This is done by putting together the transitions and using the extensibility of string rewrite systems, i.e. that we can still do a rewrite step if we add context ›
      from C1 have "wpre@(γ#wsfx) ↪⇘aps⇙ (wps@[pp])@(γ#wsfx) ∈ trcl (tr (rules M))" by (fast intro: srs_ext)
      hence "wpre@γ#wsfx ↪⇘aps⇙ wps@([pp,γ])@wsfx ∈ trcl (tr (rules M))" by simp
      moreover from RCONS have "wps@([pp,γ])@wsfx ↪⇘[aa]⇙ wps@cc'@wsfx ∈ trcl (tr (rules M))" by (fast intro: tr.rewrite trcl_one_elem)
      hence "wps@([pp,γ])@wsfx ↪⇘[aa]⇙ (wps@cc')@wsfx ∈ trcl (tr (rules M))" by simp
      moreover note C2
      ultimately have "wpre@γ#wsfx ↪⇘aps@[aa]@as⇙ ws@[p] ∈ trcl (tr (rules M))" by (fast intro: trcl_concat)
      thus ?thesis by fast
    qed
    with C2 show "∃ws as. s0 A ↪⇘ws⇙ q ∈ trclA A ∧ wpre @ γ # wsfx ↪⇘as⇙ ws @ [p] ∈ trcl (tr (rules M))" by fast ― ‹ Finally, we have the proposition for the configuration @{term "wpre@γ#wsfx"}, 
      that contains the added rule @{term "s↪⇘γ⇙s'"} one time more ›
  qed
qed  
  





text ‹ Helper lemma to clarify some subgoal in the precision proof: ›
lemma trclAD_delta_update_inv: "trclAD (A⦇δ:=X⦈) D = trclAD A D" by (simp add: trclAD_by_trcl')

text ‹ The precision is proved as an invariant of the saturation algorithm: ›
theorem (in MFSM) precise_inv: 
  shows "is_inv (ps_R M A) (δ A) (λD. (lang (A⦇δ:=D⦈) ⊆ pre* (rules M) A) ∧ (∀P'. is_inv (ps_R M A) (δ A) P' ⟶ P' D))"
proof -  

  {
    fix D1 D2 w f
    assume IH: "{w. ∃f∈F A. s0 A ↪⇘w⇙ f ∈ trclAD A D1} ⊆ pre* (rules M) A" ― ‹ By induction hypothesis, we know @{term "lang (A⦇δ:=D1⦈)⊆pre* (rules M) A"} ›
    assume SUCC: "(D1,D2)∈ps_R M A" ― ‹ We regard a successor @{term "D2"} of @{term "D1"} w.r.t. @{term "ps_R M A"} ›
    assume P1: "f∈F A" and P2: "s0 A ↪⇘w⇙ f ∈ trclAD A D2" ― ‹ And a word @{term "w∈lang (A⦇δ:=D2⦈)"} ›
    assume USE_INV: "⋀P'. is_inv (ps_R M A) (δ A) P' ⟹ P' D1" ― ‹ For the proof, we can use any known invariants ›
  
    from SUCC obtain γ s' p a c' q where ADD: "insert (sp A q p,γ,s') D1 = D2 ∧ (sp A q p,γ,s')∉D1" and 
                                             RCONS: "([p,γ],a,c')∈rules M ∧ (q,c',s')∈trclAD A D1 ∧ q∈cstates A ∧ p∈csyms M ∧ a∈labels M ∧ γ∈ssyms M"
      by (blast elim!: ps_R_elims_adv) ― ‹ Because of @{thm SUCC}, we obtain @{term "D2"} by adding a (new) transition @{term "(sp A q p,γ,s')"} to @{term "D1"}, 
        such that there is a rule @{term "[p,γ]↪⇘a⇙ c'"} and we have @{term "(q,c',s')∈trclAD A D1"} ›
    from P2 ADD have P2': "s0 A ↪⇘w⇙ f ∈ trclAD A (insert (sp A q p ↪⇘γ⇙ s') D1)" by simp
    from SUCC have SS: "D1 ⊆ ps_upper M A" by (blast dest: ps_R_dom_below) ― ‹We know, that the intermediate value is below the upper saturation bound›
    from USE_INV have A2: "δ A ⊆ D1" by (blast intro: ps_R_above_inv) ― ‹... and above the start value›
    from SS USE_INV sp_property have SP_PROP: "(∀ w . ∀p∈csyms M. ∀q∈cstates A. (s0 A,w,sp A q p)∈trclAD A D1 ⟶ (∃ws as. (s0 A,ws,q)∈trclA A ∧ (w,as,ws@[p])∈trcl (tr (rules M))))" 
      by blast ― ‹ And we have just shown @{thm [source] sp_property}, that tells us that each configuration @{term w} that leads to a state @{term "sp A q p"}, 
        can be rewritten to a configuration in the initial automaton, that uses @{term p} as its last transition ›
  
    have "w ∈ pre* (rules M) A" using P2' ― ‹ We have to show that the word @{term w} from the new automaton is also in @{term "pre* (rules M) A"}. 
      We show this by induction on how often the new transition is used by @{term w} ›
    proof (rule ins_trans_induct)
      fix wa assume "(s0 A, wa, f) ∈ trclAD A D1" ― ‹ Base case: @{term w} does not use the new transition at all ›
      with IH P1 show "wa ∈ pre* (rules M) A" by (fast) ― ‹ The proposition follows directly from the outer (invariant) induction and can be solved automatically ›
    next
      fix wpre wsfx ― ‹Step case›
      assume IP1: "(s0 A, wpre, sp A q p) ∈ trclAD A D1" ― ‹ We assume that we have a prefix @{term wpre} leading to the start state @{term s} of the new transition and not using the new transition ›
      assume IP2: "(s', wsfx, f) ∈ trclAD A (insert (sp A q p, γ, s') D1)" ― ‹ We also have a suffix from the end state @{term s'} to @{term f} ›
      assume IIH: "!!wh. (s0 A, wh, s') ∈ trclAD A D1 ⟹ wh @ wsfx ∈ pre* (rules M) A" ― ‹ And we assume that our proposition is valid for prefixes @{term wh} that do not use the new transition ›
      ― ‹ We have to show that the proposition is valid for @{term "wpre@γ#wsfx"} ›
      from IP1 SP_PROP RCONS obtain wpres apres where SPP: "(s0 A,wpres,q)∈trclA A ∧ wpre ↪⇘apres⇙ wpres@[p] ∈ trcl (tr (rules M))" by (blast) ― ‹ We can apply @{thm [source] SP_PROP}, 
        to find a successor @{term "wpres@[p]"} of @{term "wpre"} in the initial automata ›
      with A2 have "s0 A ↪⇘wpres⇙ q ∈ trclAD A D1" by (blast dest: trclAD_mono) ― ‹ @{term "wpres"} can also be read by D1 because of @{thm A2} ›
      with RCONS have "s0 A ↪⇘wpres@c'⇙ s' ∈ trclAD A D1" by (fast intro: trclAD_concat) ― ‹ Altogether we get a prefix @{term "wpres@c'"} that leads to @{term "s'"}, without using the added transition ›
      with IIH have "(wpres@c')@wsfx ∈pre_star (rules M) A" by fast ― ‹ We can apply the induction hypothesis ›
      then obtain as wo where C1: "wpres@c'@wsfx ↪⇘as⇙ wo ∈ trcl (tr (rules M)) ∧ wo∈lang A" by (auto elim!: pre_star_altE) ― ‹ And find that there is a @{term "wo"} in the original automata, 
        that is a successor of @{term "wpres@c'@wsfx"} ›
      moreover have "∃as. wpre@γ#wsfx ↪⇘as⇙ wo ∈ trcl (tr (rules M))" ― ‹ Next we show that @{term "wo"} is a successor of @{term "wpre@γ#wsfx"} ›
      proof -
        from SPP have "wpre@γ#wsfx ↪⇘apres⇙ (wpres@[p])@γ#wsfx ∈ trcl (tr (rules M))" by (fast intro: srs_ext)
        hence "wpre@γ#wsfx ↪⇘apres⇙ wpres@([p,γ])@wsfx ∈ trcl (tr (rules M))" by simp
        moreover from RCONS have "wpres@([p,γ])@wsfx ↪⇘[a]⇙ wpres@c'@wsfx ∈ trcl (tr (rules M))" by (fast intro: tr.rewrite trcl_one_elem)
        moreover note C1
        ultimately show ?thesis by (fast intro: trcl_concat)
      qed
      ultimately show "wpre @ γ # wsfx ∈ pre* (rules M) A" by (fast intro: pre_star_altI) ― ‹ And altogether we have @{term "wpre@γ#wsfx ∈ pre* (rules M) A"} ›
    qed
  } note A=this

  show ?thesis  
    apply (rule inv_useI)
    subgoal by (auto intro: pre_refl) ― ‹ The base case is solved automatically, it follows from the reflexivity of @{term "pre*"}. ›
    subgoal for D s'
      unfolding lang_def langs_def
      using A by (fastforce simp add: trclAD_delta_update_inv) 
    done      
qed

text ‹ As precision is an invariant of the saturation algorithm, and is trivial for the case of an already saturated initial automata, the result of the saturation algorithm is precise ›
corollary (in MFSM) precise: "⟦(δ A,D)∈ndet_algo (ps_R M A); x∈lang (A⦇ δ:=D ⦈)⟧ ⟹ x∈pre_star (rules M) A"
  by (auto elim!: ndet_algoE dest: inv intro: precise_inv pre_refl)

text ‹ And finally we get correctness of the algorithm, with no restrictions on valid states ›
theorem (in MFSM) correct: "⟦(δ A,D)∈ndet_algo (ps_R M A)⟧ ⟹ lang (A⦇ δ:=D ⦈) = pre_star (rules M) A" by (auto intro: precise sound)

text ‹
  So the main results of this theory are, that the algorithm is defined for every possible initial automata 
    
    @{thm MFSM.total} 

  and returns the correct result
  
    @{thm MFSM.correct}

›

text ‹ We could also prove determination, i.e. the terminating state is uniquely determined by the initial state (though there may be many ways to get there). This is not really needed here, because for correctness, we do not
  look at the structure of the final automaton, but just at its language. The language of the final automaton is determined, as implied by @{thm [source] MFSM.correct}. ›

end