Theory Bit_Vector_Framework

theory Bit_Vector_Framework imports Program_Graph begin

― ‹We encode the Bit Vector Framework into Datalog. ›

section ‹Bit-Vector Framework›

subsection ‹Definitions›

datatype pred =
  the_may
  | the_must
  | the_kill
  | the_gen
  | the_init
  | the_anadom

datatype var =
  the_𝔲

abbreviation "may == PosLit the_may"
abbreviation "must == PosLit the_must"
abbreviation NegLit_BV ("❙¬may") where
  "❙¬may ≡ NegLit the_may"
abbreviation "kill == PosLit the_kill"
abbreviation NegLit_kill ("❙¬kill") where
  "❙¬kill ≡ NegLit the_kill"
abbreviation "gen == PosLit the_gen"
abbreviation "init == PosLit the_init"
abbreviation "anadom == PosLit the_anadom"

fun s_BV :: "pred ⇒ nat" where 
  "s_BV the_kill = 0"
| "s_BV the_gen = 0"
| "s_BV the_init = 0"
| "s_BV the_anadom = 0"
| "s_BV the_may = 1"
| "s_BV the_must = 2"

datatype ('n,'a,'d) cst =
  is_Node: Node (the_Node: 'n)
  | is_Elem: Elem (the_Elem: 'd)
  | is_Action: Action (the_Action: "'a")

abbreviation may_Cls 
  :: "(var, ('n,'v,'d) cst) id list ⇒ 
      (pred, var, ('n,'v,'d) cst) rh list ⇒ 
      (pred, var, ('n,'v,'d) cst) clause" ("may⟨_⟩ :- _ .") where
   "may⟨ids⟩ :- ls. ≡ Cls the_may ids ls"

abbreviation must_Cls 
  :: "(var, ('n,'v,'d) cst) id list ⇒ 
      (pred, var, ('n,'v,'d) cst) rh list ⇒ 
      (pred, var, ('n,'v,'d) cst) clause" ("must⟨_⟩ :- _ .") where
  "must⟨ids⟩ :- ls. ≡ Cls the_must ids ls"

abbreviation init_Cls 
  :: "(var, ('n,'v,'d) cst) id list ⇒ 
      (pred, var, ('n,'v,'d) cst) rh list ⇒ 
      (pred, var, ('n,'v,'d) cst) clause" ("init⟨_⟩ :- _ .") where 
  "init⟨ids⟩ :- ls. ≡ Cls the_init ids ls"

abbreviation anadom_Cls 
  :: "(var, ('n,'v,'d) cst) id list ⇒ 
      (pred, var, ('n,'v,'d) cst) rh list ⇒ 
      (pred, var, ('n,'v,'d) cst) clause" ("anadom⟨_⟩ :- _ .") where 
  "anadom⟨ids⟩ :- ls. ≡ Cls the_anadom ids ls"

abbreviation kill_Cls 
  :: "(var, ('n,'v,'d) cst) id list ⇒ 
      (pred, var, ('n,'v,'d) cst) rh list ⇒ 
      (pred, var, ('n,'v,'d) cst) clause" ("kill⟨_⟩ :- _ .") where 
  "kill⟨ids⟩ :- ls. ≡ Cls the_kill ids ls"

abbreviation gen_Cls 
  :: "(var, ('n,'v,'d) cst) id list ⇒ 
      (pred, var, ('n,'v,'d) cst) rh list ⇒ 
      (pred, var, ('n,'v,'d) cst) clause" ("gen⟨_⟩ :- _ .") where 
  "gen⟨ids⟩ :- ls. ≡ Cls the_gen ids ls"

abbreviation BV_lh :: "(var, ('n,'v,'d) cst) id list ⇒ (pred, var, ('n,'v,'d) cst) lh" 
  ("may⟨_⟩.") where  
  "may⟨ids⟩. ≡ (the_may, ids)"

abbreviation must_lh :: "(var, ('n,'v,'d) cst) id list ⇒ (pred, var, ('n,'v,'d) cst) lh" 
  ("must⟨_⟩.") where 
  "must⟨ids⟩. ≡ (the_must, ids)"

abbreviation init_lh :: "(var, ('n,'v,'d) cst) id list ⇒ (pred, var, ('n,'v,'d) cst) lh" 
  ("init⟨_⟩.") where
  "init⟨ids⟩. ≡ (the_init, ids)"

abbreviation dom_lh :: "(var, ('n,'v,'d) cst) id list ⇒ (pred, var, ('n,'v,'d) cst) lh" 
  ("anadom⟨_⟩.") where
  "anadom⟨ids⟩. ≡ (the_anadom, ids)"

abbreviation 𝔲 :: "(var, 'a) id" where
  "𝔲 == Var the_𝔲"

abbreviation Cst⇩N :: "'n ⇒ (var, ('n, 'a, 'd) cst) id" where
  "Cst⇩N q == Cst (Node q)"

abbreviation Cst⇩E :: "'d ⇒ (var, ('n, 'a, 'd) cst) id" where
  "Cst⇩E e == Cst (Elem e)"

abbreviation Cst⇩A :: "'a ⇒ (var, ('n, 'a, 'd) cst) id" where
  "Cst⇩A α == Cst (Action α)"

abbreviation the_Node⇩i⇩d :: "(var, ('n, 'a, 'd) cst) id ⇒ 'n" where
  "the_Node⇩i⇩d ident == the_Node (the_Cst ident)"

abbreviation the_Elem⇩i⇩d :: "(var, ('n, 'a, 'd) cst) id ⇒ 'd" where
  "the_Elem⇩i⇩d ident == the_Elem (the_Cst ident)"

abbreviation the_Action⇩i⇩d :: "(var, ('n, 'a, 'd) cst) id ⇒ 'a" where
  "the_Action⇩i⇩d ident == the_Action (the_Cst ident)"

abbreviation is_Elem⇩i⇩d :: "(var, ('n, 'a, 'd) cst) id ⇒ bool" where
  "is_Elem⇩i⇩d ident == is_Cst ident ∧ is_Elem (the_Cst ident)"

abbreviation is_Node⇩i⇩d :: "(var, ('n, 'a, 'd) cst) id ⇒ bool" where
  "is_Node⇩i⇩d ident == is_Cst ident ∧ is_Node (the_Cst ident)"

abbreviation is_Action⇩i⇩d :: "(var, ('n, 'a, 'd) cst) id ⇒ bool" where
  "is_Action⇩i⇩d ident == is_Cst ident ∧ is_Action (the_Cst ident)"


subsection ‹Forward may-analysis›       

locale analysis_BV_forward_may = finite_program_graph pg 
  for pg :: "('n::finite,'a) program_graph" +
  fixes analysis_dom :: "'d set"
  fixes kill_set :: "('n,'a) edge ⇒ 'd set"
  fixes gen_set :: "('n,'a) edge ⇒ 'd set"
  fixes d_init :: "'d set"
  assumes "finite analysis_dom"
  assumes "d_init ⊆ analysis_dom"
  assumes "∀e. gen_set e ⊆ analysis_dom"
  assumes "∀e. kill_set e ⊆ analysis_dom"
begin

lemma finite_d_init: "finite d_init"
  by (meson analysis_BV_forward_may_axioms analysis_BV_forward_may_axioms_def 
      analysis_BV_forward_may_def rev_finite_subset)

interpretation LTS edges .

definition "S_hat" :: "('n,'a) edge ⇒ 'd set ⇒ 'd set" ("S^⇩E⟦_⟧ _") where
  "S^⇩E⟦e⟧ R = (R - kill_set e) ∪ gen_set e"

lemma S_hat_mono:
  assumes "d1 ⊆ d2"
  shows "S^⇩E⟦e⟧ d1 ⊆ S^⇩E⟦e⟧ d2"
  using assms unfolding S_hat_def by auto

fun S_hat_edge_list :: "('n,'a) edge list ⇒ 'd set ⇒ 'd set" ("S^⇩E⇩s⟦_⟧ _") where
  "S^⇩E⇩s⟦[]⟧ R = R" |
  "S^⇩E⇩s⟦e # π⟧ R = S^⇩E⇩s⟦π⟧ (S^⇩E⟦e⟧ R)"

lemma S_hat_edge_list_def2:
  "S^⇩E⇩s⟦π⟧ R = foldl (λa b. S^⇩E⟦b⟧ a) R π"
proof (induction π arbitrary: R)
  case Nil
  then show ?case
    by simp
next
  case (Cons a π)
  then show ?case
    by simp
qed

lemma S_hat_edge_list_append[simp]:
  "S^⇩E⇩s⟦xs @ ys⟧ R = S^⇩E⇩s⟦ys⟧ (S^⇩E⇩s⟦xs⟧ R)"
  unfolding S_hat_edge_list_def2 foldl_append by auto

lemma S_hat_edge_list_mono:
  assumes "R1 ⊆ R2"
  shows "S^⇩E⇩s⟦π⟧ R1 ⊆ S^⇩E⇩s⟦π⟧ R2"
proof(induction π rule: List.rev_induct)
  case Nil
  then show ?case
    using assms by auto
next
  case (snoc x xs)
  then show ?case
    using assms by (simp add: S_hat_mono)
qed

definition S_hat_path :: "('n list × 'a list) ⇒ 'd set ⇒ 'd set" ("S^⇩P⟦_⟧ _") where
  "S^⇩P⟦π⟧ R = S^⇩E⇩s⟦LTS.transition_list π⟧ R"

lemma S_hat_path_mono:
  assumes "R1 ⊆ R2"
  shows "S^⇩P⟦π⟧ R1 ⊆ S^⇩P⟦π⟧ R2"
  unfolding S_hat_path_def using assms S_hat_edge_list_mono by auto

fun ana_kill_edge_d :: "('n, 'a) edge ⇒ 'd ⇒ (pred, var, ('n, 'a, 'd) cst) clause" where
  "ana_kill_edge_d (q⇩o, α, q⇩s) d = kill⟨[Cst⇩N q⇩o, Cst⇩A α, Cst⇩N q⇩s, Cst⇩E d]⟩ :- []."

definition ana_kill_edge :: "('n, 'a) edge ⇒ (pred, var, ('n, 'a, 'd) cst) clause set" where
  "ana_kill_edge e = ana_kill_edge_d e ` (kill_set e)"

lemma kill_set_eq_kill_set_inter_analysis_dom: "kill_set e = kill_set e ∩ analysis_dom"
  by (meson analysis_BV_forward_may_axioms analysis_BV_forward_may_axioms_def 
      analysis_BV_forward_may_def inf.orderE)

fun ana_gen_edge_d :: "('n, 'a) edge ⇒ 'd ⇒ (pred, var, ('n, 'a, 'd) cst) clause" where
  "ana_gen_edge_d (q⇩o, α, q⇩s) d = gen⟨[Cst⇩N q⇩o, Cst⇩A α, Cst⇩N q⇩s, Cst⇩E d]⟩ :- []."

definition ana_gen_edge :: "('n, 'a) edge ⇒ (pred, var, ('n, 'a, 'd) cst) clause set" where
  "ana_gen_edge e = ana_gen_edge_d e ` (gen_set e)"

lemma gen_set_eq_gen_set_inter_analysis_dom: "gen_set e = gen_set e ∩ analysis_dom"
  by (meson analysis_BV_forward_may_axioms analysis_BV_forward_may_axioms_def 
      analysis_BV_forward_may_def inf.orderE)

definition ana_init :: "'d ⇒ (pred, var, ('n, 'a, 'd) cst) clause" where
  "ana_init d = init⟨[Cst⇩E d]⟩ :- []."

definition ana_anadom :: "'d ⇒ (pred, var, ('n, 'a, 'd) cst) clause" where
  "ana_anadom d = anadom⟨[Cst⇩E d]⟩ :- []."

definition ana_entry_node :: "(pred, var, ('n, 'a, 'd) cst) clause" where
  "ana_entry_node = may⟨[Cst⇩N start,𝔲]⟩ :- [init[𝔲]]."

fun ana_edge :: "('n, 'a) edge ⇒ (pred, var, ('n, 'a, 'd) cst) clause set" where
  "ana_edge (q⇩o, α, q⇩s) =
     {
        may⟨[Cst⇩N q⇩s, 𝔲]⟩ :-
          [
            may[Cst⇩N q⇩o, 𝔲],
            ❙¬kill[Cst⇩N q⇩o, Cst⇩A α, Cst⇩N q⇩s, 𝔲]
          ].
        ,
        may⟨[Cst⇩N q⇩s, 𝔲]⟩ :- [gen[Cst⇩N q⇩o, Cst⇩A α, Cst⇩N q⇩s, 𝔲]].
     }"

definition ana_must :: "'n ⇒ (pred, var, ('n, 'a, 'd) cst) clause" where
  "ana_must q = must⟨[Cst⇩N q,𝔲]⟩ :- [❙¬may[Cst⇩N q,𝔲], anadom[𝔲]]."

lemma ana_must_meta_var:
  assumes "ρ ⊨⇩c⇩l⇩s must⟨[Cst⇩N q,𝔲]⟩ :- [❙¬may[Cst⇩N q,𝔲], anadom[𝔲]]."
  shows "ρ ⊨⇩c⇩l⇩s must⟨[Cst⇩N q,v]⟩ :- [❙¬may[Cst⇩N q,v], anadom[v]]."
proof -
  define μ where "μ = Var(the_𝔲 := v)"
  have "ρ ⊨⇩c⇩l⇩s ((must⟨[Cst⇩N q,𝔲]⟩ :- [❙¬may[Cst⇩N q,𝔲], anadom[𝔲]].) ⋅⇩c⇩l⇩s μ)"
    using assms substitution_lemma by blast
  then show ?thesis
    unfolding μ_def by auto
qed

definition ana_pg_fw_may :: "(pred, var, ('n, 'a, 'd) cst) clause set" where
  "ana_pg_fw_may = ⋃(ana_edge ` edges)
               ∪ ana_init ` d_init
               ∪ ana_anadom ` analysis_dom
               ∪ ⋃(ana_kill_edge ` edges)
               ∪ ⋃(ana_gen_edge ` edges)
               ∪ ana_must ` UNIV
               ∪ {ana_entry_node}"

lemma ana_entry_node_meta_var:
  assumes "ρ ⊨⇩c⇩l⇩s may⟨[Cst⇩N start,𝔲]⟩ :- [init[𝔲]]."
  shows "ρ ⊨⇩c⇩l⇩s may⟨[Cst⇩N start,u]⟩ :- [init[u]]."
proof -
  define μ where "μ = Var(the_𝔲 := u)"
  have "ρ ⊨⇩c⇩l⇩s ((may⟨[Cst⇩N start,𝔲]⟩ :- [init[𝔲]].) ⋅⇩c⇩l⇩s μ)"
    using assms substitution_lemma by blast
  then show ?thesis
    unfolding μ_def by auto
qed

definition summarizes_fw_may :: "(pred, ('n, 'a, 'd) cst) pred_val ⇒ bool" where
  "summarizes_fw_may ρ ⟷ 
     (∀π d. π ∈ path_with_word_from start ⟶ d ∈ S^⇩P⟦π⟧ d_init ⟶ 
        ρ ⊨⇩l⇩h (may⟨[Cst⇩N (LTS.end_of π), Cst⇩E d]⟩.))"

lemma S_hat_path_append:
  assumes "length qs = length w"                               
  shows "S^⇩P⟦(qs @ [qnminus1, qn], w @ [α])⟧ d_init =
    S^⇩E⟦(qnminus1, α, qn)⟧ (S^⇩P⟦(qs @ [qnminus1], w)⟧ d_init)"
proof -
  have "S^⇩P⟦ (qs @ [qnminus1, qn], w @ [α])⟧ d_init = 
        S^⇩E⇩s⟦(transition_list (qs @ [qnminus1, qn], w @ [α]))⟧ d_init"
    unfolding S_hat_path_def by auto
  moreover
  have "S^⇩E⇩s⟦(transition_list (qs @ [qnminus1, qn], w @ [α]))⟧ d_init =
        S^⇩E⇩s⟦(transition_list (qs @ [qnminus1], w) @ [(qnminus1, α, qn)])⟧ d_init"
    using transition_list_reversed_simp[of qs w] assms
    by auto
  moreover
  have 
    "... = S^⇩E⇩s⟦[(qnminus1, α, qn)]⟧ (S_hat_edge_list (transition_list (qs @ [qnminus1], w)) d_init)"
    using S_hat_edge_list_append[of "transition_list (qs @ [qnminus1], w)" "[(qnminus1, α, qn)]" d_init]
    by auto
  moreover
  have "... = S^⇩E⟦(qnminus1, α, qn)⟧ (S^⇩P⟦ (qs @ [qnminus1], w)⟧ d_init)"
    unfolding S_hat_path_def by auto
  ultimately show ?thesis
    by blast
qed

lemma ana_pg_fw_may_stratified: "strat_wf s_BV ana_pg_fw_may"
  unfolding ana_pg_fw_may_def strat_wf_def ana_init_def ana_anadom_def ana_gen_edge_def 
    ana_must_def ana_entry_node_def  ana_kill_edge_def by auto

lemma finite_ana_edge_edgeset: "finite (⋃ (ana_edge ` edges))"
proof -
  have "finite edges"
    using finite_program_graph_axioms finite_program_graph_def by blast
  moreover
  have "∀e ∈ edges. finite (ana_edge e)"
    by force
  ultimately
  show ?thesis
    by blast
qed

lemma finite_ana_kill_edgeset: "finite (⋃ (ana_kill_edge ` edges))"
proof -
  have "finite edges"
    using finite_program_graph_axioms finite_program_graph_def by blast
  moreover
  have "∀e ∈ edges. finite (ana_kill_edge e)"
    by (metis ana_kill_edge_def analysis_BV_forward_may_axioms analysis_BV_forward_may_axioms_def 
        analysis_BV_forward_may_def finite_Int finite_imageI kill_set_eq_kill_set_inter_analysis_dom)
  ultimately
  show ?thesis
    by blast
qed

lemma finite_ana_gen_edgeset: "finite (⋃ (ana_gen_edge ` edges))"
proof -
  have "finite edges"
    using finite_program_graph_axioms finite_program_graph_def by blast
  moreover
  have "∀e ∈ edges. finite (ana_gen_edge e)"
    by (metis ana_gen_edge_def analysis_BV_forward_may_axioms analysis_BV_forward_may_axioms_def 
        analysis_BV_forward_may_def finite_imageI rev_finite_subset)
  ultimately
  show ?thesis
    by blast
qed

lemma finite_ana_anadom_edgeset: "finite (ana_anadom ` analysis_dom)"
  by (meson analysis_BV_forward_may_axioms analysis_BV_forward_may_axioms_def 
      analysis_BV_forward_may_def finite_imageI)

lemma ana_pg_fw_may_finite: "finite ana_pg_fw_may"
  unfolding ana_pg_fw_may_def using finite_ana_edge_edgeset finite_d_init
    finite_ana_anadom_edgeset finite_ana_kill_edgeset finite_ana_gen_edgeset by auto

fun vars_lh :: "('p,'x,'e) lh ⇒ 'x set" where
  "vars_lh (p,ids) = vars_ids ids"

lemma not_kill:
  fixes ρ :: "(pred, ('n, 'a, 'd) cst) pred_val"
  assumes "d ∉ kill_set(q⇩o, α, q⇩s)"
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_may s_BV"
  shows "ρ ⊨⇩r⇩h ❙¬kill[Cst⇩N q⇩o, Cst⇩A α, Cst⇩N q⇩s, Cst⇩E d]"
proof -
  have "finite ana_pg_fw_may"
    by (simp add: ana_pg_fw_may_finite)
  moreover
  have "ρ ⊨⇩l⇩s⇩t ana_pg_fw_may s_BV"
    using assms(2) by blast
  moreover
  have "strat_wf s_BV ana_pg_fw_may"
    by (simp add: ana_pg_fw_may_stratified)
  moreover
  have "∀c∈ana_pg_fw_may. 
           ∀σ'. 
             (the_lh c ⋅⇩v⇩l⇩h σ') = ((the_kill, [Cst⇩N q⇩o, Cst⇩A α, Cst⇩N q⇩s, Cst⇩E d])) 
               ⟶ ¬ ⟦the_rhs c⟧⇩r⇩h⇩s ρ σ'"
  proof (rule, rule, rule)
    fix c σ'
    assume c_dl: "c ∈ (ana_pg_fw_may)"
    assume "(the_lh c ⋅⇩v⇩l⇩h σ') = ((the_kill, [Cst⇩N q⇩o, Cst⇩A α, Cst⇩N q⇩s, Cst⇩E d]))"
    moreover
    from c_dl have "c ∈ (ana_pg_fw_may)"
      by auto
    ultimately
    show "¬ ⟦the_rhs c⟧⇩r⇩h⇩s ρ σ'"
      unfolding ana_pg_fw_may_def ana_init_def ana_anadom_def ana_kill_edge_def 
        ana_gen_edge_def ana_must_def ana_entry_node_def using assms(1) by fastforce
  qed
  then have "¬ (∃c∈ana_pg_fw_may.
                  lh_consequence ρ c (the_kill, [Cst⇩N q⇩o, Cst⇩A α, Cst⇩N q⇩s, Cst⇩E d]))"
    using lh_consequence_def by metis
  ultimately
  show "ρ ⊨⇩r⇩h ❙¬kill [Cst⇩N q⇩o, Cst⇩A α, Cst⇩N q⇩s, Cst⇩E d]"
    using solves_NegLit_least[of ana_pg_fw_may ρ s_BV "[Cst⇩N q⇩o, Cst⇩A α, Cst⇩N q⇩s, Cst⇩E d]" the_kill] 
    by auto
qed

lemma S_hat_edge_list_subset_analysis_dom:
  assumes "d ∈ S^⇩E⇩s⟦π⟧ d_init"
  shows "d ∈ analysis_dom"
  using assms
proof(induction π rule: List.rev_induct)
  case Nil
  then show ?case
    by (metis S_hat_edge_list.simps(1) analysis_BV_forward_may.axioms(2) 
        analysis_BV_forward_may_axioms analysis_BV_forward_may_axioms_def subsetD)

next
  case (snoc e π)
  have "gen_set e ∩ analysis_dom ⊆ analysis_dom"
    by fastforce
  then show ?case
    using S_hat_def gen_set_eq_gen_set_inter_analysis_dom snoc by auto
qed

lemma S_hat_path_subset_analysis_dom:
  assumes "d ∈ S^⇩P⟦(ss,w)⟧ d_init"
  shows "d ∈ analysis_dom"
  using assms S_hat_path_def S_hat_edge_list_subset_analysis_dom by auto

lemma S_hat_path_last:
  assumes "length qs = length w"
  shows "S^⇩P⟦(qs @ [qnminus1, qn], w @ [α])⟧ d_init =
         S^⇩E⟦(qnminus1, α, qn)⟧ (S^⇩P⟦(qs @ [qnminus1], w)⟧ d_init)"
  using assms transition_list_reversed_simp unfolding S_hat_path_def by force

lemma gen_sound:
  assumes "d ∈ gen_set (q, α, q')"
  assumes "(q, α, q') ∈ edges"
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_may s_BV"
  shows "ρ ⊨⇩c⇩l⇩s gen⟨[Cst⇩N q, Cst⇩A α, Cst⇩N q', Cst⇩E d]⟩ :- [] ."
proof -
  have "gen⟨[Cst⇩N q, Cst⇩A α, Cst⇩N q', Cst⇩E d]⟩ :- [] . ∈ ana_pg_fw_may"
    using assms(1,2) unfolding ana_pg_fw_may_def ana_gen_edge_def by fastforce
  then show "?thesis"
    using ‹gen⟨[Cst⇩N q, Cst⇩A α, Cst⇩N q', Cst⇩E d]⟩ :- [] . ∈ ana_pg_fw_may› assms(3) 
      least_solution_def solves_program_def by blast
qed

lemma sound_ana_pg_fw_may':
  assumes "(ss,w) ∈ path_with_word_from start"
  assumes "d ∈ S^⇩P⟦(ss,w)⟧ d_init"
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_may s_BV"
  shows "ρ ⊨⇩l⇩h may⟨[Cst⇩N (LTS.end_of (ss, w)), Cst⇩E d]⟩."
  using assms 
proof (induction rule: LTS.path_with_word_from_induct_reverse[OF assms(1)])
  case (1 s)
  have ρ_soultion: "ρ ⊨⇩d⇩l ana_pg_fw_may"
    using assms(3) unfolding least_solution_def by auto

  from 1(1) have start_end: "LTS.end_of ([s], []) = start"
    by (simp add: LTS.end_of_def LTS.start_of_def)

  from 1 have "S^⇩P⟦([s], [])⟧ d_init = d_init"
    unfolding S_hat_path_def by auto
  then have "d ∈ d_init"
    using 1(2) by auto
  then have "ρ ⊨⇩c⇩l⇩s init⟨[Cst⇩E d]⟩ :- [] ."
    using ρ_soultion unfolding ana_pg_fw_may_def ana_init_def solves_program_def by auto
  moreover
  have "ρ ⊨⇩c⇩l⇩s may⟨[Cst⇩N start, 𝔲]⟩ :- [init[𝔲]]."
    by (metis Un_insert_right ana_entry_node_def analysis_BV_forward_may.ana_pg_fw_may_def 
        analysis_BV_forward_may_axioms ρ_soultion insertI1 solves_program_def)
  then have "ρ ⊨⇩c⇩l⇩s may⟨[Cst⇩N start, Cst⇩E d]⟩ :- [init[Cst⇩E d]]."
    using ana_entry_node_meta_var by blast
  ultimately have "ρ ⊨⇩c⇩l⇩s may⟨[Cst⇩N start, Cst⇩E d]⟩ :- [] ."
    using prop_inf_only_from_cls_cls_to_cls by metis
  then show ?case
    using start_end solves_lh_lh by metis
next
  case (2 qs qnminus1 w α qn)
  then have len: "length qs = length w"
    using path_with_word_lengths by blast
  
  have "d ∈ S^⇩E⟦(qnminus1, α, qn)⟧ (S^⇩P⟦(qs @ [qnminus1], w)⟧ d_init)"
    using "2.prems"(2) S_hat_path_last len by blast
  then have "d ∈ (S^⇩P⟦(qs @ [qnminus1], w)⟧ d_init) - kill_set (qnminus1, α, qn) ∨
             d ∈ gen_set (qnminus1, α, qn)"
    unfolding S_hat_def by simp
  then show ?case
  proof 
    assume dSnotkill: "d ∈ (S^⇩P⟦(qs @ [qnminus1], w)⟧ d_init) - kill_set (qnminus1, α, qn)"
    then have "ρ ⊨⇩l⇩h may⟨[Cst⇩N qnminus1, Cst⇩E d]⟩."
      using 2(1,3,6) by (auto simp add: LTS.end_of_def)
    moreover
    from dSnotkill have "ρ ⊨⇩r⇩h ❙¬kill [Cst⇩N qnminus1, Cst⇩A α, Cst⇩N qn, Cst⇩E d]"
      using not_kill[of d qnminus1 α qn ρ] 2(6) by auto
    moreover
    have "ρ ⊨⇩c⇩l⇩s may⟨[Cst⇩N qn, 𝔲]⟩ :- [may [Cst⇩N qnminus1, 𝔲],
                                      ❙¬kill [Cst⇩N qnminus1, Cst⇩A α, Cst⇩N qn, 𝔲]]."
      using 2(6) "2.hyps"(2) 
      by (force simp add: ana_pg_fw_may_def solves_program_def least_solution_def)
    then have "ρ ⊨⇩c⇩l⇩s may⟨[Cst⇩N qn, Cst⇩E d]⟩ :- [may [Cst⇩N qnminus1, Cst⇩E d], 
                                               ❙¬kill [Cst⇩N qnminus1, Cst⇩A α, Cst⇩N qn, Cst⇩E d]]."
      using substitution_lemma[of ρ _ "λu. Cst⇩E d"] by force
    ultimately 
    have "ρ ⊨⇩l⇩h may⟨[Cst⇩N qn, Cst⇩E d]⟩."
      by (metis (no_types, lifting) Cons_eq_appendI prop_inf_last_from_cls_rh_to_cls modus_ponens_rh 
          self_append_conv2)
    then show "?case"
      by (auto simp add: LTS.end_of_def)
  next
    assume d_gen: "d ∈ gen_set (qnminus1, α, qn)"

    have "∀c∈ana_edge (qnminus1, α, qn). ρ ⊨⇩c⇩l⇩s c"
      using 2(6) "2.hyps"(2) unfolding ana_pg_fw_may_def solves_program_def least_solution_def 
      by blast
    then have "ρ ⊨⇩c⇩l⇩s may⟨[Cst⇩N qn, 𝔲]⟩ :- [gen [Cst⇩N qnminus1, Cst⇩A α, Cst⇩N qn, 𝔲]] ."
      by auto
    then have "ρ ⊨⇩c⇩l⇩s may⟨[Cst⇩N qn, Cst⇩E d]⟩ :- [gen [Cst⇩N qnminus1, Cst⇩A α, Cst⇩N qn, Cst⇩E d]] ."
      using substitution_lemma[of ρ _ "λu. Cst⇩E d" ]
      by force
    moreover
    have "ρ ⊨⇩c⇩l⇩s gen⟨[Cst⇩N qnminus1, Cst⇩A α, Cst⇩N qn, Cst⇩E d]⟩ :- [] ."
      using d_gen "2.hyps"(2) 2(6) gen_sound by auto
    ultimately
    have "ρ ⊨⇩l⇩h may⟨[Cst⇩N qn, Cst⇩E d]⟩."
      by (meson modus_ponens_rh solves_lh_lh)
    then show ?case
      by (auto simp add: LTS.end_of_def)
  qed
qed

theorem sound_ana_pg_fw_may:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_may s_BV"
  shows "summarizes_fw_may ρ"
  using sound_ana_pg_fw_may' assms unfolding summarizes_fw_may_def by (cases pg) fastforce

end


subsection ‹Backward may-analysis›

locale analysis_BV_backward_may = finite_program_graph pg
  for pg :: "('n::finite,'a) program_graph" +
  fixes analysis_dom :: "'d set"
  fixes kill_set :: "('n,'a) edge ⇒ 'd set"
  fixes gen_set :: "('n,'a) edge ⇒ 'd set"
  fixes d_init :: "'d set"
  assumes "finite edges"
  assumes "finite analysis_dom"
  assumes "d_init ⊆ analysis_dom"
  assumes "∀e. gen_set e ⊆ analysis_dom"
  assumes "∀e. kill_set e ⊆ analysis_dom"
begin



interpretation LTS edges .

definition S_hat :: "('n,'a) edge ⇒ 'd set ⇒ 'd set" ("S^⇩E⟦_⟧ _") where
  "S^⇩E⟦e⟧ R = (R - kill_set e) ∪ gen_set e"

lemma S_hat_mono:
  assumes "R1 ⊆ R2"
  shows "S^⇩E⟦e⟧ R1 ⊆ S^⇩E⟦e⟧ R2"
  using assms unfolding S_hat_def by auto

fun S_hat_edge_list :: "('n,'a) edge list ⇒ 'd set ⇒ 'd set" ("S^⇩E⇩s⟦_⟧ _") where
  "S^⇩E⇩s⟦[]⟧ R = R" |
  "S^⇩E⇩s⟦(e # π)⟧ R = S^⇩E⟦e⟧ (S^⇩E⇩s⟦π⟧ R)"

lemma S_hat_edge_list_def2:
  "S^⇩E⇩s⟦π⟧ R = foldr S_hat π R"
proof (induction π arbitrary: R)
  case Nil
  then show ?case
    by simp
next
  case (Cons a π)
  then show ?case
    by simp
qed

lemma S_hat_edge_list_append[simp]:
  "S^⇩E⇩s⟦(xs @ ys)⟧ R = S^⇩E⇩s⟦xs⟧ (S^⇩E⇩s⟦ys⟧ R)"
  unfolding S_hat_edge_list_def2 foldl_append by auto

lemma S_hat_edge_list_mono:
  assumes "d1 ⊆ d2"
  shows "S^⇩E⇩s⟦π⟧ d1 ⊆ S^⇩E⇩s⟦π⟧ d2"
proof(induction π)
  case Nil
  then show ?case
    using assms by auto
next
  case (Cons x xs)
  then show ?case
    using assms by (simp add: S_hat_mono)
qed

definition S_hat_path :: "('n list × 'a list) ⇒ 'd set ⇒ 'd set" ("S^⇩P⟦_⟧ _") where
  "S^⇩P⟦π⟧ R = S^⇩E⇩s⟦(transition_list π)⟧ R"

definition summarizes_bw_may :: "(pred, ('n, 'a, 'd) cst) pred_val ⇒ bool" where
  "summarizes_bw_may ρ ⟷ (∀π d. π ∈ path_with_word_to end ⟶ d ∈ S^⇩P⟦π⟧ d_init ⟶ 
                             ρ ⊨⇩l⇩h may⟨[Cst⇩N (start_of π), Cst⇩E d]⟩.)"

lemma kill_subs_analysis_dom: "(kill_set (rev_edge e)) ⊆ analysis_dom"
  by (meson analysis_BV_backward_may_axioms analysis_BV_backward_may_axioms_def 
      analysis_BV_backward_may_def)

lemma gen_subs_analysis_dom: "(gen_set (rev_edge e)) ⊆ analysis_dom"
  by (meson analysis_BV_backward_may.axioms(2) analysis_BV_backward_may_axioms 
      analysis_BV_backward_may_axioms_def)

interpretation fw_may: analysis_BV_forward_may 
  pg_rev analysis_dom "λe. (kill_set (rev_edge e))" "(λe. gen_set (rev_edge e))" d_init
  using analysis_BV_forward_may_def finite_pg_rev analysis_BV_backward_may_axioms 
    analysis_BV_backward_may_def
  by (metis (no_types, lifting) analysis_BV_backward_may_axioms_def 
      analysis_BV_forward_may_axioms_def finite_program_graph_def program_graph.edges_def)
 
abbreviation ana_pg_bw_may where
  "ana_pg_bw_may == fw_may.ana_pg_fw_may"

lemma rev_end_is_start:
  assumes "ss ≠ []"
  assumes "end_of (ss, w) = end"
  shows "start_of (rev ss, rev w) = fw_may.start"
  using assms
  unfolding end_of_def LTS.start_of_def fw_may.start_def pg_rev_def fw_may.start_def
  using hd_rev by (metis fw_may.start_def fst_conv pg_rev_def snd_conv) 

lemma S_hat_edge_list_forward_backward:
  "S^⇩E⇩s⟦ss⟧ d_init = fw_may.S_hat_edge_list (rev_edge_list ss) d_init"
proof (induction ss)
  case Nil
  then show ?case
    unfolding rev_edge_list_def by auto
next
  case (Cons e es)
  have "S^⇩E⇩s⟦e # es⟧ d_init = S^⇩E⟦e⟧ S^⇩E⇩s⟦es⟧ d_init"
    by simp
  also 
  have "... = fw_may.S_hat (rev_edge e) (foldr fw_may.S_hat (map rev_edge es) d_init)"
    unfolding foldr_conv_foldl fw_may.S_hat_edge_list_def2[symmetric]
    unfolding rev_edge_list_def[symmetric] fw_may.S_hat_def S_hat_def
    using Cons by simp
  also
  have "... = fw_may.S_hat_edge_list (rev_edge_list (e # es)) d_init"
    unfolding rev_edge_list_def fw_may.S_hat_edge_list_def2 foldl_conv_foldr
    by simp
  finally
  show ?case
    by metis
qed

lemma S_hat_path_forward_backward:
  assumes "(ss,w) ∈ path_with_word"
  shows "S^⇩P⟦(ss, w)⟧ d_init = fw_may.S_hat_path (rev ss, rev w) d_init"
  using S_hat_edge_list_forward_backward unfolding S_hat_path_def fw_may.S_hat_path_def
  by (metis transition_list_rev_edge_list assms)

lemma summarizes_bw_may_forward_backward':
  assumes "(ss,w) ∈ path_with_word"
  assumes "end_of (ss,w) = end"
  assumes "d ∈ S^⇩P⟦(ss,w)⟧ d_init"
  assumes "fw_may.summarizes_fw_may ρ"
  shows "ρ ⊨⇩l⇩h may⟨[Cst⇩N (start_of (ss, w)), Cst⇩E d]⟩."
proof -
  have rev_in_edges: "(rev ss, rev w) ∈ LTS.path_with_word fw_may.edges"
    using assms(1) rev_path_in_rev_pg[of ss w] fw_may.edges_def pg_rev_def by auto 
  moreover
  have "LTS.start_of (rev ss, rev w) = fw_may.start"
    using assms(1,2) rev_end_is_start by (metis LTS.path_with_word_not_empty)
  moreover
  have "d ∈ fw_may.S_hat_path (rev ss, rev w) d_init"
    using assms(3)
    using assms(1) S_hat_path_forward_backward by auto
  ultimately
  have "ρ ⊨⇩l⇩h may⟨[Cst⇩N (LTS.end_of (rev ss, rev w)), Cst⇩E d]⟩."
    using assms(4) fw_may.summarizes_fw_may_def by blast
  then show ?thesis
    by (metis LTS.end_of_def LTS.start_of_def fst_conv hd_rev rev_rev_ident)
qed

lemma summarizes_dl_BV_forward_backward:
  assumes "fw_may.summarizes_fw_may ρ"
  shows "summarizes_bw_may ρ"
  unfolding summarizes_bw_may_def
proof(rule; rule ; rule; rule)
  fix π d
  assume "π ∈ {π ∈ path_with_word. LTS.end_of π = end}"
  moreover
  assume "d ∈ S^⇩P⟦π⟧ d_init"
  ultimately
  show "ρ ⊨⇩l⇩h may⟨[Cst⇩N (LTS.start_of π), Cst⇩E d]⟩."
    using summarizes_bw_may_forward_backward'[of "fst π" "snd π" d ρ] using assms by auto
qed

theorem sound_ana_pg_bw_may:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_bw_may s_BV"
  shows "summarizes_bw_may ρ"
  using assms fw_may.sound_ana_pg_fw_may[of ρ] summarizes_dl_BV_forward_backward by metis

end


subsection ‹Forward must-analysis›
                                            
locale analysis_BV_forward_must = finite_program_graph pg
  for pg :: "('n::finite,'a) program_graph" +
  fixes analysis_dom :: "'d set"
  fixes kill_set :: "('n,'a) edge ⇒ 'd set"
  fixes gen_set :: "('n,'a) edge ⇒ 'd set"
  fixes d_init :: "'d set"
  assumes "finite analysis_dom"
  assumes "d_init ⊆ analysis_dom"
begin

lemma finite_d_init: "finite d_init"
  by (meson analysis_BV_forward_must.axioms(2) analysis_BV_forward_must_axioms 
      analysis_BV_forward_must_axioms_def rev_finite_subset)

interpretation LTS edges .

definition S_hat :: "('n,'a) edge ⇒ 'd set ⇒ 'd set" ("S^⇩E⟦_⟧ _") where
  "S^⇩E⟦e⟧ R = (R - kill_set e) ∪ gen_set e"

lemma S_hat_mono:
  assumes "R1 ⊆ R2"
  shows "S^⇩E⟦e⟧ R1 ⊆ S^⇩E⟦e⟧ R2"
  using assms unfolding S_hat_def by auto

fun S_hat_edge_list :: "('n,'a) edge list ⇒ 'd set ⇒ 'd set" ("S^⇩E⇩s⟦_⟧ _") where
  "S^⇩E⇩s⟦[]⟧ R = R" |
  "S^⇩E⇩s⟦(e # π)⟧ R = S^⇩E⇩s⟦π⟧ (S^⇩E⟦e⟧ R)"

lemma S_hat_edge_list_def2:
  "S^⇩E⇩s⟦π⟧ R = foldl (λa b. S^⇩E⟦b⟧ a) R π"
proof (induction π arbitrary: R)
  case Nil
  then show ?case
    by simp
next
  case (Cons a π)
  then show ?case
    by simp
qed

lemma S_hat_edge_list_append[simp]:
  "S^⇩E⇩s⟦(xs @ ys)⟧ R = S^⇩E⇩s⟦ys⟧ (S^⇩E⇩s⟦xs⟧ R)"
  unfolding S_hat_edge_list_def2 foldl_append by auto

lemma S_hat_edge_list_mono:
  assumes "R1 ⊆ R2"
  shows "S^⇩E⇩s⟦π⟧ R1 ⊆ S^⇩E⇩s⟦π⟧ R2"
proof(induction π rule: List.rev_induct)
  case Nil
  then show ?case
    using assms by auto
next
  case (snoc x xs)
  then show ?case
    using assms by (simp add: S_hat_mono)
qed

definition S_hat_path :: "('n list × 'a list) ⇒ 'd set ⇒ 'd set" ("S^⇩P⟦_⟧ _") where
  "S^⇩P⟦π⟧ R = S^⇩E⇩s⟦LTS.transition_list π⟧ R"

lemma S_hat_path_mono:
  assumes "R1 ⊆ R2"
  shows "S^⇩P⟦π⟧ R1 ⊆ S^⇩P⟦π⟧ R2"
  unfolding S_hat_path_def using assms S_hat_edge_list_mono by auto

definition summarizes_fw_must :: "(pred, ('n, 'a, 'd) cst) pred_val ⇒ bool" where
   "summarizes_fw_must ρ ⟷
     (∀q d.
         ρ ⊨⇩l⇩h must⟨[q, d]⟩. ⟶
           (∀π. π ∈ path_with_word ⟶
                start_of π = start ⟶
                end_of π = the_Node⇩i⇩d q ⟶
                (the_Elem⇩i⇩d d) ∈ S^⇩P⟦π⟧ d_init))"

interpretation fw_may: analysis_BV_forward_may 
  pg analysis_dom "λe. analysis_dom - (kill_set e)" "(λe. analysis_dom - gen_set e)" 
  "analysis_dom - d_init"
  using analysis_BV_forward_may.intro[of pg] analysis_BV_forward_must_def[of pg] 
    analysis_BV_forward_may_axioms_def analysis_BV_forward_must_axioms 
    analysis_BV_forward_must_axioms_def by (metis Diff_subset)
  
abbreviation ana_pg_fw_must where
  "ana_pg_fw_must == fw_may.ana_pg_fw_may"

lemma opposite_lemma:
  assumes "d ∈ analysis_dom"
  assumes "¬d ∈ fw_may.S_hat_edge_list π (analysis_dom - d_init)"
  shows "d ∈ S^⇩E⇩s⟦π⟧ d_init"
  using assms proof (induction π rule: List.rev_induct)
  case Nil
  then show ?case
    by auto
next
  case (snoc x xs)
  then show ?case
    unfolding fw_may.S_hat_edge_list_def2
    by (simp add: S_hat_def fw_may.S_hat_def)
qed

lemma opposite_lemma_path:
  assumes "d ∈ analysis_dom"
  assumes "¬d ∈ fw_may.S_hat_path π (analysis_dom - d_init)"
  shows "d ∈ S^⇩P⟦π⟧ d_init"
  using S_hat_path_def fw_may.S_hat_path_def assms opposite_lemma by metis

lemma the_must_only_ana_must: "the_must ∉ preds_dl (ana_pg_fw_must - (fw_may.ana_must ` UNIV))"
  unfolding fw_may.ana_pg_fw_may_def preds_dl_def preds_dl_def fw_may.ana_init_def
    preds_dl_def fw_may.ana_anadom_def preds_dl_def fw_may.ana_kill_edge_def preds_dl_def
    fw_may.ana_gen_edge_def fw_may.ana_entry_node_def by auto 

lemma agree_off_rh:
  assumes "∀p. p ≠ p' ⟶ ρ' p = ρ p"
  assumes "p' ∉ preds_rh rh"
  shows "⟦rh⟧⇩r⇩h ρ' σ ⟷ ⟦rh⟧⇩r⇩h ρ σ"
  using assms proof (cases rh)
  case (Eql a a')
  then show ?thesis
    by auto 
next
  case (Neql a a')
  then show ?thesis 
    by auto 
next
  case (PosLit p ids)
  then show ?thesis
    using assms by auto 
next
  case (NegLit p ids)
  then show ?thesis 
    using assms by auto 
qed

definition preds_rhs where
  "preds_rhs rhs = ⋃(preds_rh ` set rhs)"

lemma preds_cls_preds_rhs: "preds_cls (Cls p ids rhs) = {p} ∪ preds_rhs rhs"
  by (simp add: preds_rhs_def)

lemma agree_off_rhs:
  assumes "∀p. p ≠ p' ⟶ ρ' p = ρ p"
  assumes "p' ∉ preds_rhs rhs"
  shows "⟦rhs⟧⇩r⇩h⇩s ρ' σ ⟷ ⟦rhs⟧⇩r⇩h⇩s ρ σ"
  using assms agree_off_rh[of p' ρ' ρ _ σ] unfolding preds_rhs_def by auto

lemma agree_off_lh:
  assumes "∀p. p ≠ p' ⟶ ρ' p = ρ p"
  assumes "p' ∉ preds_lh lh"
  shows "⟦lh⟧⇩l⇩h ρ' σ ⟷ ⟦lh⟧⇩l⇩h ρ σ"
proof (cases lh)
  case (Pair p ids)
  then show ?thesis
    using assms by auto
qed

lemma agree_off_cls:
  assumes "∀p. p ≠ p' ⟶ ρ' p = ρ p"
  assumes "p' ∉ preds_cls c"
  shows "⟦c⟧⇩c⇩l⇩s ρ' σ ⟷ ⟦c⟧⇩c⇩l⇩s ρ σ"
proof (cases c)
  case (Cls p ids rhs)
  show ?thesis
  proof
    assume "⟦c⟧⇩c⇩l⇩s ρ' σ"
    show "⟦c⟧⇩c⇩l⇩s ρ σ"
      unfolding Cls meaning_cls.simps
    proof
      assume "⟦rhs⟧⇩r⇩h⇩s ρ σ"
      then have "⟦rhs⟧⇩r⇩h⇩s ρ' σ"
        using agree_off_rhs
        by (metis Cls assms(1) assms(2) clause.simps(6) insert_iff preds_rhs_def)
      then show"⟦(p, ids)⟧⇩l⇩h ρ σ"
        using Cls ‹⟦c⟧⇩c⇩l⇩s ρ' σ› assms(1) assms(2) by auto
    qed
  next
    assume "⟦c⟧⇩c⇩l⇩s ρ σ"
    show "⟦c⟧⇩c⇩l⇩s ρ' σ"
    unfolding Cls meaning_cls.simps
    proof
      assume "⟦rhs⟧⇩r⇩h⇩s ρ' σ"
      then have "⟦rhs⟧⇩r⇩h⇩s ρ σ"
        using agree_off_rhs
        by (metis Cls assms(1) assms(2) clause.simps(6) insert_iff preds_rhs_def)
      then show"⟦(p, ids)⟧⇩l⇩h ρ' σ"
        using Cls ‹⟦c⟧⇩c⇩l⇩s ρ σ› assms(1) assms(2) by auto
    qed
  qed
qed

lemma agree_off_solves_cls:
  assumes "∀p. p ≠ p' ⟶ ρ' p = ρ p"
  assumes "p' ∉ preds_cls c"
  shows "ρ' ⊨⇩c⇩l⇩s c ⟷ ρ ⊨⇩c⇩l⇩s c"
proof (cases c)
  case (Cls p ids rhs)
  then show ?thesis
    by (metis (mono_tags, opaque_lifting) agree_off_cls assms solves_cls_def)
qed

lemma agree_off_dl:
  assumes "∀p. p ≠ p' ⟶ ρ' p = ρ p"
  assumes "p' ∉ preds_dl dl"
  shows "ρ' ⊨⇩d⇩l dl ⟷ ρ ⊨⇩d⇩l dl"
proof 
  assume "ρ' ⊨⇩d⇩l dl"
  show "ρ ⊨⇩d⇩l dl"
    unfolding solves_program_def
  proof
    fix c
    assume "c ∈ dl"
    have "p' ∉ preds_cls c"
      using ‹c ∈ dl› assms(2) preds_dl_def by fastforce
    show "ρ ⊨⇩c⇩l⇩s c"
      by (metis ‹ρ' ⊨⇩d⇩l dl› ‹c ∈ dl› ‹p' ∉ preds_cls c› agree_off_solves_cls assms(1) 
          solves_program_def)
  qed
next 
  assume "ρ ⊨⇩d⇩l dl"
  show "ρ' ⊨⇩d⇩l dl"
    unfolding solves_program_def
  proof
    fix c
    assume "c ∈ dl"
    have "p' ∉ preds_cls c"
      using ‹c ∈ dl› assms(2) preds_dl_def by fastforce
    show "ρ' ⊨⇩c⇩l⇩s c"
      by (metis ‹ρ ⊨⇩d⇩l dl› ‹c ∈ dl› ‹p' ∉ preds_cls c› agree_off_solves_cls assms(1) 
          solves_program_def)
  qed
qed

lemma is_Cst_if_init:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h init⟨[d]⟩."
  shows "is_Cst d"
proof (rule ccontr)
  assume "¬ is_Cst d"
  then have du: "d = 𝔲"
    by (metis (full_types) id.disc(1) id.exhaust_disc id.expand var.exhaust)
  then have "⟦init⟨[d]⟩.⟧⇩l⇩h ρ (λx. Action undefined)" 
    using assms
    by auto
  then have "ρ ⊨⇩l⇩h init⟨[d ⋅⇩v⇩i⇩d (λx. Action undefined)]⟩."
    using solves_lh_substv_lh_if_meaning_lh[of "init⟨[d]⟩." ρ "(λx. Action undefined)"] du by auto
  moreover
  have "is_Cst (Cst⇩A undefined)"
    by auto
  moreover
  have "is_Cst (d ⋅⇩v⇩i⇩d (λx. Action undefined))"
    by (metis id.disc(4) substv_id.elims)
  ultimately
  have "∃c ∈ ana_pg_fw_must. lh_consequence ρ c (init⟨[Cst⇩A undefined]⟩.)"
    using solves_lh_least[of ana_pg_fw_must ρ s_BV] du
    by (simp add: assms(1) fw_may.ana_pg_fw_may_finite fw_may.ana_pg_fw_may_stratified)
  then show False
    unfolding fw_may.ana_pg_fw_may_def fw_may.ana_entry_node_def lh_consequence_def
      fw_may.ana_init_def fw_may.ana_anadom_def fw_may.ana_kill_edge_def fw_may.ana_gen_edge_def
      fw_may.ana_must_def by auto
qed

lemma is_Cst_if_anadom:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h anadom⟨[d]⟩."
  shows "is_Cst d"
proof (rule ccontr)
  assume "¬ is_Cst d"
  then have du: "d = 𝔲"
    by (metis (full_types) id.disc(1) id.exhaust_disc id.expand var.exhaust)
  then have "⟦anadom⟨[d]⟩.⟧⇩l⇩h ρ (λx. Action undefined)" 
    using assms
    by auto
  then have "ρ ⊨⇩l⇩h anadom⟨[d ⋅⇩v⇩i⇩d (λx. Action undefined)]⟩."
    using solves_lh_substv_lh_if_meaning_lh[of "anadom⟨[d]⟩." ρ "(λx. Action undefined)"] du by auto
  moreover
  have "is_Cst (Cst⇩A undefined)"
    by auto
  moreover
  have "is_Cst (d ⋅⇩v⇩i⇩d (λx. Action undefined))"
    by (metis id.disc(4) substv_id.elims)
  ultimately
  have "∃c ∈ ana_pg_fw_must. lh_consequence ρ c (anadom⟨[Cst⇩A undefined]⟩.)"
    using solves_lh_least[of ana_pg_fw_must ρ s_BV] du
    by (simp add: assms(1) fw_may.ana_pg_fw_may_finite fw_may.ana_pg_fw_may_stratified)
  then show False
    unfolding fw_may.ana_pg_fw_may_def fw_may.ana_entry_node_def lh_consequence_def
      fw_may.ana_init_def fw_may.ana_anadom_def fw_may.ana_kill_edge_def fw_may.ana_gen_edge_def
      fw_may.ana_must_def by auto
qed

lemma if_init:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h init⟨[d]⟩."
  shows "is_Elem⇩i⇩d d ∧ the_Elem⇩i⇩d d ∈ (analysis_dom - d_init)"
proof -
  have d_Cst: "is_Cst d"
    using assms(1) assms(2) is_Cst_if_init by blast

  from assms(1,2) d_Cst have "∃c ∈ ana_pg_fw_must. lh_consequence ρ c (init⟨[d]⟩.)"
    using solves_lh_least[of ana_pg_fw_must ρ s_BV "[d]"] fw_may.ana_pg_fw_may_finite
      fw_may.ana_pg_fw_may_stratified by fastforce

  then obtain c where 
    "c ∈ ana_pg_fw_must"
    "lh_consequence ρ c (init⟨[d]⟩.)"
    by auto
  from this have "∃d' ∈ (analysis_dom - d_init). c = init⟨[Cst⇩E d']⟩ :- []."
    unfolding fw_may.ana_pg_fw_may_def fw_may.ana_entry_node_def lh_consequence_def
      fw_may.ana_anadom_def fw_may.ana_kill_edge_def fw_may.ana_gen_edge_def
      fw_may.ana_must_def fw_may.ana_init_def by auto
  then obtain d' where "d' ∈ analysis_dom - d_init ∧ c = init⟨[Cst⇩E d']⟩ :- []."
    by auto
  have "lh_consequence ρ (init⟨[Cst⇩E d']⟩ :- [].) (init⟨[d]⟩.)"
    using ‹d' ∈ analysis_dom - d_init ∧ c = init⟨[Cst⇩E d']⟩ :- [] .›
      ‹lh_consequence ρ c init⟨[d]⟩.› by fastforce
  then have "∃σ. (init⟨[Cst⇩E d']⟩. ⋅⇩v⇩l⇩h σ) = init⟨[d]⟩."
    unfolding lh_consequence_def by auto
  then obtain σ where σ_p:
    "(init⟨[Cst⇩E d']⟩. ⋅⇩v⇩l⇩h σ) = init⟨[d]⟩."
    by auto
  then have "d = Cst⇩E d'"
    by auto
  then have "the_Elem⇩i⇩d d ∈ analysis_dom - d_init ∧ is_Elem⇩i⇩d d"
    using ‹d' ∈ analysis_dom - d_init ∧ c = init⟨[Cst⇩E d']⟩ :- [] .› by auto
  then show ?thesis
    by auto
qed

lemma if_anadom:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h anadom⟨[d]⟩."
  shows "is_Elem⇩i⇩d d ∧ the_Elem⇩i⇩d d ∈ analysis_dom"
proof -
  have d_Cst: "is_Cst d"
    using assms(1) assms(2) is_Cst_if_anadom by blast

  from assms(1,2) d_Cst have "∃c ∈ ana_pg_fw_must. lh_consequence ρ c (anadom⟨[d]⟩.)"
    using solves_lh_least[of ana_pg_fw_must ρ s_BV "[d]"] fw_may.ana_pg_fw_may_finite
      fw_may.ana_pg_fw_may_stratified by fastforce
  then obtain c where 
    "c ∈ ana_pg_fw_must"
    "lh_consequence ρ c (anadom⟨[d]⟩.)"
    by auto
  from this have "∃d' ∈ analysis_dom. c = anadom⟨[Cst⇩E d']⟩ :- []."
    unfolding fw_may.ana_pg_fw_may_def fw_may.ana_entry_node_def lh_consequence_def
      fw_may.ana_anadom_def fw_may.ana_kill_edge_def fw_may.ana_gen_edge_def
      fw_may.ana_must_def fw_may.ana_init_def by auto
  then obtain d' where "d' ∈ analysis_dom ∧ c = anadom⟨[Cst⇩E d']⟩ :- []."
    by auto
  have "lh_consequence ρ (anadom⟨[Cst⇩E d']⟩ :- [].) (anadom⟨[d]⟩.)"
    using ‹d' ∈ analysis_dom ∧ c = anadom⟨[Cst⇩E d']⟩ :- [] .›
      ‹lh_consequence ρ c anadom⟨[d]⟩.› by fastforce
  then have "∃σ. (anadom⟨[Cst⇩E d']⟩. ⋅⇩v⇩l⇩h σ) = anadom⟨[d]⟩."
    unfolding lh_consequence_def by auto
  then obtain σ where σ_p:
    "(anadom⟨[Cst⇩E d']⟩. ⋅⇩v⇩l⇩h σ) = anadom⟨[d]⟩."
    by auto
  then have "d = Cst⇩E d'"
    by auto
  then have "the_Elem⇩i⇩d d ∈ analysis_dom ∧ is_Elem⇩i⇩d d"
    using ‹d' ∈ analysis_dom ∧ c = anadom⟨[Cst⇩E d']⟩ :- [] .› by auto
  then show ?thesis
    by auto
qed

lemma is_elem_if_init:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h init⟨[Cst d]⟩."
  shows "is_Elem d"
  by (metis if_init assms id.sel(2))

lemma not_init_node:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  shows "¬ρ ⊨⇩l⇩h init⟨[Cst⇩N q]⟩."
  by (metis if_init assms cst.collapse(2) cst.disc(1) cst.disc(2) id.sel(2))

lemma not_init_action:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  shows "¬ρ ⊨⇩l⇩h init⟨[Cst⇩A q]⟩."
  by (metis assms cst.collapse(2) cst.simps(9) id.sel(2) if_init)

lemma in_analysis_dom_if_init':
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h init⟨[Cst⇩E d]⟩."
  shows "d ∈ analysis_dom"
  using assms if_init by force

lemma in_analysis_dom_if_init:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h init⟨[d]⟩."
  shows "the_Elem⇩i⇩d d ∈ analysis_dom"
  using assms if_init by force

lemma not_anadom_node:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  shows "¬ρ ⊨⇩l⇩h anadom⟨[Cst⇩N q]⟩."
  by (metis assms cst.collapse(2) cst.disc(1) cst.disc(2) id.sel(2) if_anadom)

lemma not_anadom_action:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  shows "¬ρ ⊨⇩l⇩h anadom⟨[Cst⇩A q]⟩."
  by (metis assms cst.collapse(2) cst.simps(9) id.sel(2) if_anadom)

lemma in_analysis_dom_if_anadom':
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h anadom⟨[Cst⇩E d]⟩."
  shows "d ∈ analysis_dom"
  using assms if_anadom by force

lemma in_analysis_dom_if_anadom:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h anadom⟨[d]⟩."
  shows "the_Elem⇩i⇩d d ∈ analysis_dom ∧ is_Elem⇩i⇩d d"
  using assms if_anadom by force

lemma must_fst_id_is_Cst:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h must⟨[q,d]⟩."
  shows "is_Cst q"
proof (rule ccontr)
  assume "¬ is_Cst q"
  then have qu: "q = 𝔲"
    by (metis (full_types) id.disc(1) id.exhaust_disc id.expand var.exhaust)
  then have "⟦must⟨[q,d]⟩.⟧⇩l⇩h ρ (λx. Action undefined)" 
    using assms
    by auto
  then have "ρ ⊨⇩l⇩h must⟨[Cst⇩A undefined, d ⋅⇩v⇩i⇩d (λx. Action undefined)]⟩."
    using solves_lh_substv_lh_if_meaning_lh[of "must⟨[q, d]⟩." ρ "(λx. Action undefined)"] qu by auto
  moreover
  have "is_Cst (Cst⇩A undefined)"
    by auto
  moreover
  have "is_Cst (d ⋅⇩v⇩i⇩d (λx. Action undefined))"
    by (metis id.disc(4) substv_id.elims)
  ultimately
  have "∃c ∈ ana_pg_fw_must. lh_consequence ρ c (must⟨[Cst⇩A undefined, d ⋅⇩v⇩i⇩d (λx. Action undefined)]⟩.)"
    using solves_lh_least[of ana_pg_fw_must ρ s_BV "[Cst⇩A undefined, d ⋅⇩v⇩i⇩d (λx. Action undefined)]"
        the_must]
    by (simp add: assms(1) fw_may.ana_pg_fw_may_finite fw_may.ana_pg_fw_may_stratified)
  then show False
    unfolding fw_may.ana_pg_fw_may_def fw_may.ana_entry_node_def lh_consequence_def
      fw_may.ana_init_def fw_may.ana_anadom_def fw_may.ana_kill_edge_def fw_may.ana_gen_edge_def
      fw_may.ana_must_def by auto
qed

lemma must_snd_id_is_Cst:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h must⟨[q,d]⟩."
  shows "is_Cst d"
proof (rule ccontr)
  assume "¬ is_Cst d"
  then have du: "d = 𝔲"
    by (metis (full_types) id.disc(1) id.exhaust_disc id.expand var.exhaust)
  then have "⟦must⟨[q,d]⟩.⟧⇩l⇩h ρ (λx. Action undefined)" 
    using assms
    by auto
  then have "ρ ⊨⇩l⇩h must⟨[q ⋅⇩v⇩i⇩d (λx. Action undefined), Cst⇩A undefined]⟩."
    using solves_lh_substv_lh_if_meaning_lh[of "must⟨[q, d]⟩." ρ "(λx. Action undefined)"] du by auto
  moreover
  have "is_Cst (Cst⇩A undefined)"
    by auto
  moreover
  have "is_Cst (q ⋅⇩v⇩i⇩d (λx. Action undefined))"
    by (metis id.disc(4) substv_id.elims)
  ultimately
  have "∃c ∈ ana_pg_fw_must. lh_consequence ρ c (must⟨[q ⋅⇩v⇩i⇩d (λx. Action undefined), Cst⇩A undefined]⟩.)"
    using solves_lh_least[of ana_pg_fw_must ρ s_BV "[q ⋅⇩v⇩i⇩d (λx. Action undefined), Cst⇩A undefined]"
        the_must]
    by (simp add: assms(1) fw_may.ana_pg_fw_may_finite fw_may.ana_pg_fw_may_stratified)
    then obtain c where c_p:
    "c ∈ ana_pg_fw_must"
    "lh_consequence ρ c (must⟨[q ⋅⇩v⇩i⇩d (λx. Action undefined), Cst⇩A undefined]⟩.)"
    by auto
  from this have "∃q'. c = must⟨[Cst⇩N q',𝔲]⟩ :- [❙¬may[Cst⇩N q',𝔲], anadom[𝔲]]."
    unfolding fw_may.ana_pg_fw_may_def fw_may.ana_entry_node_def lh_consequence_def
      fw_may.ana_init_def fw_may.ana_anadom_def fw_may.ana_kill_edge_def fw_may.ana_gen_edge_def
      fw_may.ana_must_def by auto
  then obtain q' where "c = must⟨[Cst⇩N q',𝔲]⟩ :- [❙¬may[Cst⇩N q',𝔲], anadom[𝔲]]."
    by auto
  then have "lh_consequence ρ (must⟨[Cst⇩N q',𝔲]⟩ :- [❙¬may[Cst⇩N q',𝔲], anadom[𝔲]].) 
                              (must⟨[q ⋅⇩v⇩i⇩d (λx. Action undefined), Cst⇩A undefined]⟩.)"
    using c_p(2) by auto
  then have "∃σ'. (must⟨[Cst⇩N q', 𝔲]⟩. ⋅⇩v⇩l⇩h σ') = must⟨[q ⋅⇩v⇩i⇩d (λx. Action undefined), Cst⇩A undefined]⟩.
                  ∧ ⟦[❙¬may[Cst⇩N q', 𝔲], anadom[𝔲]]⟧⇩r⇩h⇩s ρ σ'"
    unfolding lh_consequence_def using the_lh.simps clause.sel(3) by metis
  then obtain σ' where σ'_p:
    "(must⟨[Cst⇩N q', 𝔲]⟩. ⋅⇩v⇩l⇩h σ') = must⟨[q ⋅⇩v⇩i⇩d (λx. Action undefined), Cst⇩A undefined]⟩."
    "⟦[❙¬may[Cst⇩N q', 𝔲], anadom[𝔲]]⟧⇩r⇩h⇩s ρ σ'"
    by metis
  then have "σ' the_𝔲 = Action undefined"
    by auto
  then have "ρ ⊨⇩r⇩h anadom[(Cst⇩A undefined)]"
    using σ'_p(2) solves_rh_substv_rh_if_meaning_rh  by auto
  then show False
    using assms(1) not_anadom_action by auto
qed

lemma if_must:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h must⟨[q,d]⟩."
  shows 
    "ρ ⊨⇩r⇩h ❙¬may[q, d] ∧ ρ ⊨⇩l⇩h anadom⟨[d]⟩. ∧ is_Node⇩i⇩d q ∧is_Elem⇩i⇩d d ∧ the_Elem⇩i⇩d d ∈ analysis_dom"
proof -
  have Csts: "is_Cst q" "is_Cst d"
    using must_fst_id_is_Cst must_snd_id_is_Cst using assms by auto

  from assms(1,2) Csts have "∃c ∈ ana_pg_fw_must. lh_consequence ρ c (must⟨[q,d]⟩.)"
    using solves_lh_least[of ana_pg_fw_must ρ s_BV "[q,d]" the_must] fw_may.ana_pg_fw_may_finite
      fw_may.ana_pg_fw_may_stratified by fastforce

  then obtain c where 
    "c ∈ ana_pg_fw_must"
    "lh_consequence ρ c (must⟨[q,d]⟩.)"
    by auto
  from this have "∃q'. c = must⟨[Cst⇩N q',𝔲]⟩ :- [❙¬may[Cst⇩N q',𝔲], anadom[𝔲]]."
    unfolding fw_may.ana_pg_fw_may_def fw_may.ana_entry_node_def lh_consequence_def
      fw_may.ana_init_def fw_may.ana_anadom_def fw_may.ana_kill_edge_def fw_may.ana_gen_edge_def
      fw_may.ana_must_def by auto
    
  then obtain q' where "c = must⟨[Cst⇩N q',𝔲]⟩ :- [❙¬may[Cst⇩N q',𝔲], anadom[𝔲]]."
    by auto
  have "lh_consequence ρ (must⟨[Cst⇩N q',𝔲]⟩ :- [❙¬may[Cst⇩N q',𝔲], anadom[𝔲]].) (must⟨[q,d]⟩.)"
    using ‹c = must⟨[Cst⇩N q', 𝔲]⟩ :- [❙¬may [Cst⇩N q', 𝔲], anadom [𝔲]] .› 
      ‹lh_consequence ρ c must⟨[q, d]⟩.› by fastforce
  then have "∃σ. (must⟨[Cst⇩N q', 𝔲]⟩. ⋅⇩v⇩l⇩h σ) = must⟨[q, d]⟩. ∧ ⟦[❙¬may[Cst⇩N q', 𝔲], anadom[𝔲]]⟧⇩r⇩h⇩s ρ σ"
    unfolding lh_consequence_def by auto
  then obtain σ where σ_p:
    "(must⟨[Cst⇩N q', 𝔲]⟩. ⋅⇩v⇩l⇩h σ) = must⟨[q, d]⟩."
    "⟦[❙¬may[Cst⇩N q', 𝔲], anadom[𝔲]]⟧⇩r⇩h⇩s ρ σ"
    by auto
  then have "q = Cst⇩N q'"
    by auto
  from σ_p have "∃d'. σ the_𝔲 = d' ∧ d = Cst d'"
    by auto
  then obtain d' where 
    "σ the_𝔲 = d'"
    "d = Cst d'"
    by auto
  from σ_p(2) have "⟦❙¬may[Cst⇩N q', 𝔲]⟧⇩r⇩h ρ σ"
    by auto
  then have "ρ ⊨⇩r⇩h ❙¬may[q, d]"
    using solves_rh_substv_rh_if_meaning_rh ‹σ the_𝔲 = d'› ‹d = Cst d'› ‹q = Cst⇩N q'› by force 
  have "⟦anadom[𝔲]⟧⇩r⇩h ρ σ"
    using σ_p(2) by auto
  then have "ρ ⊨⇩r⇩h anadom[d]"
    using solves_rh_substv_rh_if_meaning_rh ‹σ the_𝔲 = d'› ‹d = Cst d'› ‹q = Cst⇩N q'› by force
  then have "the_Elem⇩i⇩d d ∈ analysis_dom ∧ is_Elem⇩i⇩d d"
    using in_analysis_dom_if_anadom[of ρ d] assms by fastforce
  show ?thesis 
    using ‹ρ ⊨⇩r⇩h ❙¬may [q, d]› ‹ρ ⊨⇩r⇩h anadom [d]› ‹q = Cst⇩N q'›
      ‹the_Elem⇩i⇩d d ∈ analysis_dom ∧ is_Elem⇩i⇩d d› by auto
qed

lemma not_must_and_may:
  assumes "[Node q, Elem d] ∈ ρ the_must"
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "[Node q, Elem d] ∈ ρ the_may"                  
  shows False
proof -
  have "ρ ⊨⇩l⇩h must⟨[Cst⇩N q, Cst⇩E d]⟩."
    using assms(1) by auto
  then have "ρ ⊨⇩r⇩h ❙¬may [Cst⇩N q, Cst⇩E d]"
    using if_must assms(2) by metis
  then show False
    using assms(3) by auto
qed

lemma not_solves_must_and_may:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h must⟨[Cst⇩N q, Cst⇩E d]⟩."
  assumes "ρ ⊨⇩l⇩h may⟨[Cst⇩N q, Cst⇩E d]⟩."
  shows "False"
proof -
  have "[Node q, Elem d] ∈ ρ the_must"
    using assms(2)
    unfolding solves_lh.simps
    unfolding meaning_lh.simps
    by auto
  moreover
  have "[Node q, Elem d] ∈ ρ the_may"
    using assms(3)
    unfolding solves_lh.simps
    unfolding meaning_lh.simps
    by auto
  ultimately
  show "False"
    using not_must_and_may[of q d ρ] assms(1) by auto
qed

lemma anadom_if_must:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h must⟨[q, d]⟩."
  shows "ρ ⊨⇩l⇩h anadom⟨[d]⟩."
  using assms(1) assms(2) if_must by blast

lemma not_must_action:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  shows "¬ρ ⊨⇩l⇩h must⟨[Cst⇩A q,d]⟩."
  by (metis assms cst.disc(3) id.sel(2) if_must)

lemma is_encode_elem_if_must_right_arg:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h must⟨[q, d]⟩."
  shows "∃d'. d = Cst⇩E d'"
  by (metis assms(1) assms(2) cst.collapse(2) id.collapse(2) if_must)

lemma not_must_element: 
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  shows "¬ρ ⊨⇩l⇩h must⟨[Cst⇩E q,d]⟩."
  by (metis assms cst.disc(2) id.sel(2) if_must)

lemma is_encode_node_if_must_left_arg:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h must⟨[q, d]⟩."
  shows "∃q'. q = Cst⇩N q'"
  by (metis assms(1) assms(2) cst.collapse(1) id.collapse(2) if_must)

lemma in_analysis_dom_if_must:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h must⟨[q, d]⟩."
  shows "the_Elem⇩i⇩d d ∈ analysis_dom"
  using assms(1) assms(2) if_must by blast

lemma sound_ana_pg_fw_must':
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  assumes "ρ ⊨⇩l⇩h must⟨[q, d]⟩."
  assumes "π ∈ path_with_word_from_to start (the_Node⇩i⇩d q)"
  shows "the_Elem⇩i⇩d d ∈ S^⇩P⟦π⟧ d_init"
proof -
  have d_ana: "the_Elem⇩i⇩d d ∈ analysis_dom"
    using assms(1) assms(2) in_analysis_dom_if_must by auto

  have πe: "q = Cst⇩N (end_of π)"
    using assms(1) assms(2) assms(3) is_encode_node_if_must_left_arg by fastforce

  have d_encdec: "d = Cst⇩E (the_Elem⇩i⇩d d)"
    by (metis cst.sel(2) assms(1) assms(2) id.sel(2) is_encode_elem_if_must_right_arg)

  have not_may: "¬ ρ ⊨⇩l⇩h may⟨[Cst⇩N (end_of π), d]⟩."
    using not_solves_must_and_may[OF assms(1), of "(end_of π)" "the_Elem⇩i⇩d d"] assms(2) πe d_encdec 
    by force
  have "¬the_Elem⇩i⇩d d ∈ fw_may.S_hat_path π (analysis_dom - d_init)"
    using fw_may.sound_ana_pg_fw_may assms(1)
    unfolding fw_may.summarizes_fw_may_def
     edges_def start_def assms(2) edges_def start_def
    using assms(3)  d_encdec edges_def not_may start_def by (metis (mono_tags) mem_Collect_eq) 
  then show "the_Elem⇩i⇩d d ∈ S^⇩P⟦π⟧ d_init"
    using opposite_lemma_path
    using assms(1)
    using d_ana by blast 
qed

theorem sound_ana_pg_fw_must:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_fw_must s_BV"
  shows "summarizes_fw_must ρ"
  using assms unfolding summarizes_fw_must_def using sound_ana_pg_fw_must' by auto

end


subsection ‹Backward must-analysis›

locale analysis_BV_backward_must = finite_program_graph pg
  for pg :: "('n::finite,'a) program_graph" +
  fixes analysis_dom :: "'d set"
  fixes kill_set :: "('n,'a) edge ⇒ 'd set"
  fixes gen_set :: "('n,'a) edge ⇒ 'd set"
  fixes d_init :: "'d set"
  assumes "finite analysis_dom"
  assumes "d_init ⊆ analysis_dom"
begin

lemma finite_d_init: "finite d_init"
  by (meson analysis_BV_backward_must.axioms(2) analysis_BV_backward_must_axioms 
      analysis_BV_backward_must_axioms_def rev_finite_subset)

interpretation LTS edges .

definition S_hat :: "('n,'a) edge ⇒ 'd set ⇒ 'd set" ("S^⇩E⟦_⟧ _") where
  "S^⇩E⟦e⟧ R = (R - kill_set e) ∪ gen_set e"

lemma S_hat_mono:
  assumes "R1 ⊆ R2"
  shows "S^⇩E⟦e⟧ R1 ⊆ S^⇩E⟦e⟧ R2"
  using assms unfolding S_hat_def by auto

fun S_hat_edge_list :: "('n,'a) edge list ⇒ 'd set ⇒ 'd set" ("S^⇩E⇩s⟦_⟧ _") where
  "S^⇩E⇩s⟦[]⟧ R = R" |
  "S^⇩E⇩s⟦(e # π)⟧ R = S^⇩E⟦e⟧ (S^⇩E⇩s⟦π⟧ R)"

lemma S_hat_edge_list_def2:
  "S^⇩E⇩s⟦π⟧ R = foldr S_hat π R"
proof (induction π arbitrary: R)
  case Nil
  then show ?case
    by simp
next
  case (Cons a π)
  then show ?case
    by simp
qed

lemma S_hat_edge_list_append[simp]:
  "S^⇩E⇩s⟦xs @ ys⟧ R = S^⇩E⇩s⟦xs⟧ (S^⇩E⇩s⟦ys⟧ R)"
  unfolding S_hat_edge_list_def2 foldl_append by auto

lemma S_hat_edge_list_mono:
  assumes "R1 ⊆ R2"
  shows "S^⇩E⇩s⟦π⟧ R1 ⊆ S^⇩E⇩s⟦π⟧ R2"
proof(induction π)
  case Nil
  then show ?case
    using assms by auto
next
  case (Cons x xs)
  then show ?case
    using assms by (simp add: S_hat_mono)
qed

definition S_hat_path :: "('n list × 'a list) ⇒ 'd set ⇒ 'd set" ("S^⇩P⟦_⟧ _") where
  "S^⇩P⟦π⟧ R = S^⇩E⇩s⟦LTS.transition_list π⟧ R"

definition summarizes_bw_must :: "(pred, ('n, 'v, 'd) cst) pred_val ⇒ bool" where
   "summarizes_bw_must ρ ⟷
     (∀q d.
         ρ ⊨⇩l⇩h must⟨[q, d]⟩. ⟶
          (∀π. π ∈ path_with_word_from_to (the_Node⇩i⇩d q) end ⟶ the_Elem⇩i⇩d d ∈ S^⇩P⟦π⟧ d_init))"

interpretation fw_must: analysis_BV_forward_must 
  pg_rev analysis_dom "λe. (kill_set (rev_edge e))" "(λe. gen_set (rev_edge e))" d_init
  using analysis_BV_forward_must_def finite_pg_rev analysis_BV_backward_must_axioms
    analysis_BV_backward_must_def analysis_BV_backward_must_axioms_def
    analysis_BV_forward_must_axioms.intro finite_program_graph.intro
    program_graph.edges_def by metis


abbreviation ana_pg_bw_must where
  "ana_pg_bw_must == fw_must.ana_pg_fw_must"

lemma rev_end_is_start:
  assumes "ss ≠ []"
  assumes "end_of (ss, w) = end"
  shows "start_of (rev ss, rev w) = fw_must.start"
  using assms
  unfolding LTS.end_of_def LTS.start_of_def fw_must.start_def pg_rev_def fw_must.start_def
  using hd_rev by (metis fw_must.start_def fst_conv pg_rev_def snd_conv) 

lemma S_hat_edge_list_forward_backward:
  "S^⇩E⇩s⟦ss⟧ d_init = fw_must.S_hat_edge_list (rev_edge_list ss) d_init"
proof (induction ss)
  case Nil
  then show ?case
    unfolding rev_edge_list_def by auto
next
  case (Cons a ss)
  have "S^⇩E⇩s⟦a # ss⟧ d_init = S^⇩E⟦a⟧ S^⇩E⇩s⟦ss⟧ d_init"
    by simp
  also
  have "... = (((S^⇩E⇩s⟦ss⟧ d_init) - kill_set a) ∪ gen_set a)"
    using S_hat_def by auto
  also
  have "... = fw_must.S_hat_edge_list (rev_edge_list ss) d_init - kill_set a ∪ gen_set a"
    using Cons by auto
  also
  have "... = fw_must.S_hat_edge_list (rev_edge_list ss) d_init - kill_set (rev_edge (rev_edge a)) 
                ∪ gen_set (rev_edge (rev_edge a))"
    by simp
  also
  have "... = fw_must.S_hat (rev_edge a) (fw_must.S_hat_edge_list (rev_edge_list ss) d_init)"
    using fw_must.S_hat_def by auto
  also
  have "... = fw_must.S_hat (rev_edge a) (fw_must.S_hat_edge_list (rev (map rev_edge ss)) d_init)"
    by (simp add: rev_edge_list_def)
  also
  have "... = fw_must.S_hat (rev_edge a) (foldl (λx y. fw_must.S_hat y x) d_init (rev (map rev_edge ss)))"
    using fw_must.S_hat_edge_list_def2 by force
  also
  have "... = fw_must.S_hat (rev_edge a) (foldr fw_must.S_hat (map rev_edge ss) d_init)"
    by (simp add: foldr_conv_foldl)
  also
  have "... = foldr fw_must.S_hat (rev (rev (map rev_edge (a # ss)))) d_init"
    by force
  also
  have "... = foldl (λa b. fw_must.S_hat b a) d_init (rev (map rev_edge (a # ss)))"
    by (simp add: foldr_conv_foldl)
  also
  have "... = fw_must.S_hat_edge_list (rev (map rev_edge (a # ss))) d_init"
    using fw_must.S_hat_edge_list_def2 by auto
  also
  have "... = fw_must.S_hat_edge_list (rev_edge_list (a # ss)) d_init"
    by (simp add: rev_edge_list_def)
  finally
  show ?case
    by auto
qed

lemma S_hat_path_forward_backward:
  assumes "(ss,w) ∈ path_with_word"
  shows "S^⇩P⟦(ss, w)⟧ d_init = fw_must.S_hat_path (rev ss, rev w) d_init"
  using S_hat_edge_list_forward_backward unfolding S_hat_path_def fw_must.S_hat_path_def
  by (metis transition_list_rev_edge_list assms)

lemma summarizes_fw_must_forward_backward':
  assumes "fw_must.summarizes_fw_must ρ"
  assumes "ρ ⊨⇩l⇩h must⟨[q, d]⟩."
  assumes "π ∈ path_with_word_from_to (the_Node⇩i⇩d q) end"
  shows "the_Elem⇩i⇩d d ∈ S^⇩P⟦π⟧ d_init"
proof -
  define rev_π where "rev_π = (rev (fst π), rev (snd π))"
  have rev_π_path: "rev_π ∈ LTS.path_with_word fw_must.edges"
    using rev_π_def assms(3) fw_must.edges_def pg_rev_def rev_path_in_rev_pg
    by (metis (no_types, lifting) fst_conv mem_Collect_eq  prod.collapse)
  have rev_π_start: "start_of rev_π = fw_must.start"
    using  rev_π_def analysis_BV_backward_must_axioms
      assms(3) pg_rev_def start_of_def edges_def end_of_def hd_rev  
      by (metis (mono_tags, lifting) fw_must.start_def mem_Collect_eq prod.sel)
  have rev_π_start_end: "end_of rev_π = the_Node⇩i⇩d q"
    using assms(3) rev_π_def end_of_def last_rev start_of_def
    by (metis (mono_tags, lifting) mem_Collect_eq prod.sel(1))
  have "the_Elem⇩i⇩d d ∈ fw_must.S_hat_path (rev (fst π), rev (snd π)) d_init"
    using rev_π_def rev_π_path rev_π_start_end rev_π_start assms(1) assms(2) 
      fw_must.summarizes_fw_must_def by blast
  then show ?thesis
    by (metis (no_types, lifting) S_hat_path_forward_backward assms(3) mem_Collect_eq prod.collapse)
qed
 

lemma summarizes_bw_must_forward_backward:
  assumes "fw_must.summarizes_fw_must ρ"
  shows "summarizes_bw_must ρ"
  unfolding summarizes_bw_must_def
  using assms summarizes_fw_must_forward_backward' by auto

theorem sound_ana_pg_bw_must:
  assumes "ρ ⊨⇩l⇩s⇩t ana_pg_bw_must s_BV"
  shows "summarizes_bw_must ρ"
  using assms fw_must.sound_ana_pg_fw_must[of ρ] summarizes_bw_must_forward_backward by metis

end

end