Theory Reaching_Definitions

theory Reaching_Definitions imports Bit_Vector_Framework begin

― ‹We encode the Reaching Definitions analysis into Datalog. First we define the analysis, then
    we encode the analysis directly into Datalog and prove the encoding correct. Hereafter we
    encode it into Datalog again, but this time using our Bit-Vector Framework locale. We also prove 
    this encoding correct. This latter encoding is described in our SAC 2024 paper. ›


section ‹Reaching Definitions›

type_synonym ('n,'v) def = "'v * 'n option * 'n"

type_synonym ('n,'v) analysis_assignment = "'n ⇒ ('n,'v) def set"


subsection ‹What is defined on a path›

fun def_action :: "'v action ⇒ 'v set" where
  "def_action (x ::= a) = {x}"
| "def_action (Bool b) = {}"
| "def_action Skip = {}"

abbreviation def_edge :: "('n,'v action) edge ⇒ 'v set" where
  "def_edge == λ(q1, α, q2). def_action α"

definition def_of :: "'v ⇒ ('n,'v action) edge ⇒ ('n,'v) def" where
  "def_of == (λx (q1, α, q2). (x, Some q1, q2))"

definition def_var :: "('n,'v action) edge list ⇒ 'v ⇒ 'n ⇒ ('n,'v) def" where
  "def_var π x start = (if (∃e ∈ set π. x ∈ def_edge e)
                        then (def_of x (last (filter (λe. x ∈ def_edge e) π)))
                        else (x, None, start))"

definition def_path :: "('n list × 'v action list) ⇒ 'n ⇒ ('n,'v) def set" where
  "def_path π start = ((λx. def_var (LTS.transition_list π) x start) ` UNIV)"


subsection ‹Reaching Definitions in Datalog›

― ‹Direct encoding of Reaching Definitions into Datalog.›

datatype ('n,'v) RD_elem =
  RD_Node 'n
  | RD_Var 'v
  | Questionmark

datatype RD_var =
  the_𝗎
  | the_𝗏
  | the_𝗐

datatype RD_pred =
  the_RD
  | the_VAR

abbreviation CstRDN :: "'n ⇒ (RD_var, ('n, 'v) RD_elem) id" where
  "CstRDN q == Cst (RD_Node q)"

fun CstRDN_Q :: "'n option ⇒ (RD_var, ('n, 'v) RD_elem) id" where
  "CstRDN_Q (Some q) = Cst (RD_Node q)"
| "CstRDN_Q None = Cst Questionmark"

abbreviation CstRDV :: "'v ⇒ (RD_var, ('n, 'v) RD_elem) id" where
  "CstRDV v == Cst (RD_Var v)"

abbreviation RD_Cls :: "(RD_var, ('n, 'v) RD_elem) id list ⇒ (RD_pred, RD_var, ('n, 'v) RD_elem) rh list ⇒ (RD_pred, RD_var, ('n, 'v) RD_elem) clause" ("RD⟨_⟩ :- _ .") where 
  "RD⟨args⟩ :- ls. ≡ Cls the_RD args ls"

abbreviation VAR_Cls :: "'v ⇒ (RD_pred, RD_var, ('n, 'v) RD_elem) clause" ("VAR⟨_⟩ :-.") where
  "VAR⟨x⟩ :-. == Cls the_VAR [CstRDV x] []"

abbreviation RD_lh :: "(RD_var, ('n, 'v) RD_elem) id list ⇒ (RD_pred, RD_var, ('n, 'v) RD_elem) lh" ("RD⟨_⟩.") where 
  "RD⟨args⟩. ≡ (the_RD, args)"

abbreviation VAR_lh :: "'v ⇒ (RD_pred, RD_var, ('n, 'v) RD_elem) lh" ("VAR⟨_⟩.") where 
  "VAR⟨x⟩. ≡ (the_VAR, [CstRDV x])"


abbreviation "RD == PosLit the_RD"
abbreviation "VAR == PosLit the_VAR"

abbreviation 𝗎 :: "(RD_var, 'aa) id" where
  "𝗎 == Var the_𝗎"

abbreviation 𝗏 :: "(RD_var, 'aa) id" where
  "𝗏 == Var the_𝗏"

abbreviation 𝗐 :: "(RD_var, 'aa) id" where
  "𝗐 == Var the_𝗐"

fun ana_edge :: "('n, 'v action) edge ⇒ (RD_pred, RD_var, ('n,'v) RD_elem) clause set" where
  "ana_edge (qo, x ::= a, qs) =
     {
        RD⟨[CstRDN qs, 𝗎, 𝗏, 𝗐]⟩ :-
          [
            RD[CstRDN qo, 𝗎, 𝗏, 𝗐],
            𝗎 ≠ (CstRDV x)
          ].
        ,
        RD⟨[CstRDN qs, CstRDV x, CstRDN qo, CstRDN qs]⟩ :- [].
     }"
| "ana_edge (qo, Bool b, qs) =
     {
       RD⟨[CstRDN qs, 𝗎, 𝗏, 𝗐]⟩ :-
         [
           RD[CstRDN qo, 𝗎, 𝗏, 𝗐]
         ].
     }"
| "ana_edge (qo, Skip, qs) =
     {
       RD⟨[CstRDN qs, 𝗎, 𝗏, 𝗐]⟩ :-
         [
           RD[CstRDN qo, 𝗎, 𝗏, 𝗐]
         ].
     }"

definition ana_entry_node :: "'n ⇒ (RD_pred, RD_var, ('n,'v) RD_elem) clause set" where
  "ana_entry_node start = 
     {
       RD⟨[CstRDN start, 𝗎, Cst Questionmark, CstRDN start]⟩ :-
         [
           VAR[𝗎]
         ].
     }"


fun ana_RD :: "('n, 'v action) program_graph ⇒ (RD_pred, RD_var, ('n,'v) RD_elem) clause set" where
  "ana_RD (es,start,end) = ⋃(ana_edge ` es) ∪ ana_entry_node start"

definition var_contraints :: "(RD_pred, RD_var, ('n,'v) RD_elem) clause set" where
  "var_contraints = VAR_Cls ` UNIV"

type_synonym ('n,'v) quadruple = "'n *'v * 'n option * 'n"

fun summarizes_RD :: "(RD_pred,('n,'v) RD_elem) pred_val ⇒ ('n,'v action) program_graph ⇒ bool" where
  "summarizes_RD ρ (es, start, end) =
    (∀π x q1 q2.
       π ∈ LTS.path_with_word_from es start ⟶
       (x, q1, q2) ∈ def_path π start ⟶ 
       ρ ⊨lh RD⟨[CstRDN (LTS.end_of π), CstRDV x, CstRDN_Q q1, CstRDN q2]⟩.)"

lemma def_var_x: "fst (def_var ts x start) = x"
  unfolding def_var_def by (simp add: case_prod_beta def_of_def)

lemma last_def_transition:
  assumes "length ss = length w"
  assumes "x ∈ def_action α"
  assumes "(x, q1, q2) ∈ def_path (ss @ [s, s'], w @ [α]) start"
  shows "Some s = q1 ∧ s' = q2"
proof -
  obtain y where y_p: "(x, q1, q2) = def_var (transition_list (ss @ [s], w) @ [(s, α, s')]) y start"
    by (metis (no_types, lifting) assms(1) assms(3) def_path_def imageE transition_list_reversed_simp)
  show ?thesis
  proof (cases "y = x")
    case True
    then show ?thesis 
      using assms y_p unfolding def_var_def def_of_def by auto
  next
    case False
    then show ?thesis
      by (metis y_p def_var_x fst_conv)
  qed
qed

lemma not_last_def_transition:
  assumes "length ss = length w"
  assumes "x ∉ def_action α"
  assumes "(x, q1, q2) ∈ def_path (ss @ [s, s'], w @ [α]) start"
  shows "(x, q1, q2) ∈ def_path (ss @ [s], w) start"
proof -
  obtain y where y_p: "(x, q1, q2) = def_var (transition_list (ss @ [s], w) @ [(s, α, s')]) y start"
    by (metis (no_types, lifting) assms(1) assms(3) def_path_def imageE transition_list_reversed_simp)
  have "(x, q1, q2) ∈ range (λx. def_var (transition_list (ss @ [s], w)) x start)"
  proof (cases "y = x")
    case True
    then show ?thesis 
      using assms y_p unfolding def_var_def def_of_def by auto
  next
    case False
    then show ?thesis
      by (metis y_p def_var_x fst_conv)
  qed
  then show ?thesis
    by (simp add: def_path_def)
qed

theorem RD_sound': 
  assumes "(ss,w) ∈ LTS.path_with_word_from es start"
  assumes "(x,q1,q2) ∈ def_path (ss,w) start"
  assumes "ρ ⊨dl (var_contraints ∪ ana_RD (es, start, end))"
  shows "ρ ⊨lh RD⟨[CstRDN (LTS.end_of (ss, w)), CstRDV x, CstRDN_Q q1, CstRDN q2]⟩."
  using assms 
proof (induction rule: LTS.path_with_word_from_induct_reverse[OF assms(1)])
  case (1 s)
  have "VAR⟨x⟩ :-. ∈ var_contraints"
    unfolding var_contraints_def by auto
  from assms(3) this have "ρ ⊨cls VAR⟨x⟩ :-."
    unfolding solves_program_def by auto  
  then have "∀y. ⟦(VAR⟨x⟩ :-.)⟧cls ρ y"
    unfolding solves_cls_def by auto
  then have x_sat: "[RD_Var x] ∈ ρ the_VAR"
    by auto

  have "RD⟨[CstRDN start, 𝗎, Cst Questionmark, CstRDN start]⟩ :-
         [
           VAR[𝗎]
         ]. ∈ ana_RD (es, start, end)"
    by (simp add: ana_entry_node_def)
  then have "ρ ⊨cls RD⟨[CstRDN start, 𝗎, Cst Questionmark, CstRDN start]⟩ :- [VAR [𝗎]] ."
    using assms(3) unfolding solves_program_def by auto 
  then have "∀σ. ⟦RD⟨[CstRDN start, 𝗎, Cst Questionmark, CstRDN start]⟩ :- [VAR [𝗎]] .⟧cls ρ σ"
    unfolding solves_cls_def by metis
  then have "⟦RD⟨[CstRDN start, 𝗎, Cst Questionmark, CstRDN start]⟩ :- [VAR [𝗎]] .⟧cls ρ (λv. RD_Var x)"
    by presburger
  then have "[RD_Var x] ∈ ρ the_VAR ⟶ [RD_Node start, RD_Var x, Questionmark, RD_Node start] ∈ ρ the_RD"
    by simp
  then have "[RD_Node start, RD_Var x, Questionmark, RD_Node start] ∈ ρ the_RD"
    using x_sat by auto

  from this 1 show ?case
    unfolding LTS.LTS.end_of_def def_path_def def_var_def LTS.start_of_def by auto
next
  case (2 ss s w α s')
  from 2(1) have len: "length ss = length w"
    using LTS.path_with_word_length by force
  show ?case 
  proof(cases "x ∈ def_action α")
    case True
    then have sq: "Some s = q1 ∧ s' = q2" using 2(5)
      using last_def_transition[of ss w x α q1 q2 s s'] len by auto
    from True have "∃e. (s,x ::= e,s') ∈ es"
      using "2.hyps"(2) by (cases α) auto
    then have "RD⟨[CstRDN q2, CstRDV x, CstRDN_Q q1, CstRDN q2]⟩ :- []. ∈ ana_RD (es, start, end)"
      using True ana_RD.simps sq by fastforce
    then have "ρ ⊨cls RD⟨[CstRDN q2, CstRDV x, CstRDN_Q q1, CstRDN q2]⟩ :- [] ."
      using 2(6) unfolding solves_program_def by auto
    then have "ρ ⊨lh RD⟨[CstRDN q2, CstRDV x, CstRDN_Q q1, CstRDN q2]⟩."
      using solves_lh_lh by metis 
    then show ?thesis
      by (simp add: LTS.end_of_def sq)
  next
    case False
    then have x_is_def: "(x, q1, q2) ∈ def_path (ss @ [s], w) start" using 2(5)
      using not_last_def_transition len by force
    then have "ρ ⊨lh RD⟨[CstRDN (LTS.end_of (ss @ [s], w)), CstRDV x, CstRDN_Q q1, CstRDN q2]⟩."
    proof -
      have "(ss @ [s], w) ∈ LTS.path_with_word es"
        using 2(1) by auto
      moreover
      have "ρ ⊨dl (var_contraints ∪ ana_RD (es, start, end))"
        using 2(6) by auto
      moreover
      have "LTS.start_of (ss @ [s], w) = start"
        using "2.hyps"(1) by auto
      moreover
      have "(x, q1, q2) ∈ def_path (ss @ [s], w) start"
        using x_is_def by auto
      ultimately
      show "ρ ⊨lh RD⟨[CstRDN (LTS.end_of (ss @ [s], w)), CstRDV x, CstRDN_Q q1, CstRDN q2]⟩."
        using 2(3) by auto
    qed
    then have ind: "ρ ⊨lh RD⟨[CstRDN s, CstRDV x, CstRDN_Q q1, CstRDN q2]⟩."
      by (simp add: LTS.end_of_def)
    define μ where "μ = undefined(the_𝗎 := CstRDV x, the_𝗏 := CstRDN_Q q1, the_𝗐 := CstRDN q2)"
    show ?thesis
    proof (cases α)
      case (Asg y e)
      have xy: "x ≠ y"
        using False Asg by auto
      then have xy': "ρ ⊨rh (CstRDV x ≠ CstRDV y)"
        by auto
      have "(s, y ::= e, s') ∈ es"
        using "2.hyps"(2) Asg by auto
      then have "RD⟨[CstRDN s', 𝗎, 𝗏, 𝗐]⟩ :-
          [
            RD[CstRDN s, 𝗎, 𝗏, 𝗐],
            𝗎 ≠ (CstRDV y)
          ]. ∈ ana_RD (es,start,end)"
        unfolding ana_RD.simps by force
      from this False have "ρ ⊨cls RD⟨[CstRDN s', 𝗎, 𝗏, 𝗐]⟩ :- [RD [CstRDN s, 𝗎, 𝗏, 𝗐], 𝗎 ≠ CstRDV y] ."
        by (meson "2.prems"(3) UnCI solves_program_def)
      moreover have 
        "(RD⟨[CstRDN s', 𝗎, 𝗏, 𝗐]⟩ :-
          [
            RD[CstRDN s, 𝗎, 𝗏, 𝗐],
            𝗎 ≠ (CstRDV y)
          ].) ⋅cls μ = 
          RD⟨[CstRDN s', CstRDV x, CstRDN_Q q1, CstRDN q2]⟩ :-
          [
            RD [CstRDN s,  CstRDV x, CstRDN_Q q1, CstRDN q2], 
            CstRDV x ≠ CstRDV y] ."
        unfolding μ_def by auto
      ultimately
      have "ρ ⊨cls RD⟨[CstRDN s', CstRDV x, CstRDN_Q q1, CstRDN q2]⟩
                    :- [RD [CstRDN s, CstRDV x, CstRDN_Q q1, CstRDN q2], CstRDV x ≠ CstRDV y] ."
        unfolding solves_cls_def by (metis substitution_lemma_cls)
      then have "ρ ⊨cls RD⟨[CstRDN s', CstRDV x, CstRDN_Q q1, CstRDN q2]⟩ 
                         :- [RD [CstRDN s, CstRDV x, CstRDN_Q q1, CstRDN q2]] ."
        using xy' by (simp add: prop_inf_last_from_cls_rh_to_cls)
      then have "ρ ⊨cls RD⟨[CstRDN s', CstRDV x, CstRDN_Q q1, CstRDN q2]⟩ :- [] ."
        using ind by (metis meaning_cls.simps modus_ponens_rh solves_cls_def solves_lh.simps)
      then have "ρ ⊨lh RD⟨[CstRDN s', CstRDV x, CstRDN_Q q1, CstRDN q2]⟩."
        using solves_lh_lh by metis
      then show ?thesis
        by (simp add: LTS.end_of_def)
    next
      case (Bool b)
      have "(s, Bool b, s') ∈ es"
        using "2.hyps"(2) Bool by auto
      then have "RD⟨[CstRDN s', 𝗎, 𝗏, 𝗐]⟩ :-
         [
           RD[CstRDN s, 𝗎, 𝗏, 𝗐]
         ]. ∈ ana_RD (es,start,end)"
        unfolding ana_RD.simps by force
      then have "ρ ⊨cls RD⟨[CstRDN s', 𝗎, 𝗏, 𝗐]⟩ :- [RD [CstRDN s, 𝗎, 𝗏, 𝗐]] ."
        by (meson "2.prems"(3) UnCI solves_program_def)
      moreover 
      have "(RD⟨[CstRDN s', 𝗎, 𝗏, 𝗐]⟩ :- [RD[CstRDN s, 𝗎, 𝗏, 𝗐]].) ⋅cls μ =
            RD⟨[CstRDN s', CstRDV x, CstRDN_Q q1, CstRDN q2]⟩ :- 
              [RD[CstRDN s, CstRDV x, CstRDN_Q q1, CstRDN q2]]."
        unfolding μ_def by auto
      ultimately have "ρ ⊨cls RD⟨[CstRDN s', CstRDV x, CstRDN_Q q1, CstRDN q2]⟩ 
                               :- [RD [CstRDN s, CstRDV x, CstRDN_Q q1, CstRDN q2]] ."
        by (metis substitution_lemma)
      then have "ρ ⊨lh RD⟨[CstRDN s', CstRDV x, CstRDN_Q q1, CstRDN q2]⟩."
        using ind
        by (meson prop_inf_only)
      then show ?thesis
        by (simp add: LTS.end_of_def)
    next
      case Skip
      have "(s, Skip, s') ∈ es"
        using "2.hyps"(2) Skip by auto
      then have "RD⟨[CstRDN s', 𝗎, 𝗏, 𝗐]⟩ :-
         [
           RD[CstRDN s, 𝗎, 𝗏, 𝗐]
         ]. ∈ ana_RD (es,start,end)"
        unfolding ana_RD.simps by force
      then have "ρ ⊨cls RD⟨[CstRDN s', 𝗎, 𝗏, 𝗐]⟩ :- [RD [CstRDN s, 𝗎, 𝗏, 𝗐]] ."
        by (meson "2.prems"(3) UnCI solves_program_def)
      moreover
      have "(RD⟨[CstRDN s', 𝗎, 𝗏, 𝗐]⟩ :- [RD [CstRDN s, 𝗎, 𝗏, 𝗐]] .) ⋅cls μ =
            RD⟨[CstRDN s', CstRDV x, CstRDN_Q q1, CstRDN q2]⟩ :-
              [RD [CstRDN s, CstRDV x, CstRDN_Q q1, CstRDN q2]]."
        unfolding μ_def by auto
      ultimately 
      have "ρ ⊨cls RD⟨[CstRDN s', CstRDV x, CstRDN_Q q1, CstRDN q2]⟩ 
                    :- [RD [CstRDN s, CstRDV x, CstRDN_Q q1, CstRDN q2]] ."
        by (metis substitution_lemma)
      from modus_ponens_rh[OF this ind] have "ρ ⊨lh RD⟨[CstRDN s', CstRDV x, CstRDN_Q q1, CstRDN q2]⟩."
        .
      then show ?thesis
        by (simp add: LTS.end_of_def)
    qed
  qed
qed

theorem RD_sound:
  assumes "ρ ⊨dl (var_contraints ∪ ana_RD pg)"
  shows "summarizes_RD ρ pg"
  using assms RD_sound' by (cases pg) force


subsection ‹Reaching Definitions as Bit-Vector Framework analysis›

― ‹Encoding of Reaching Definitions into Datalog using the Bit-Vector Framework.›

locale analysis_RD = finite_program_graph pg
  for pg :: "('n::finite,'v::finite action) program_graph" +
  assumes "finite edges"
begin

interpretation LTS edges .

definition analysis_dom_RD :: "('n,'v) def set" where
  "analysis_dom_RD = UNIV × UNIV × UNIV"

fun kill_set_RD :: "('n,'v action) edge ⇒ ('n,'v) def set" where
  "kill_set_RD (qo, x ::= a, qs) = {x} × UNIV × UNIV"
| "kill_set_RD (qo, Bool b, qs) = {}"
| "kill_set_RD (v, Skip, vc) = {}"

fun gen_set_RD :: "('n,'v action) edge ⇒ ('n,'v) def set" where
  "gen_set_RD (qo, x ::= a, qs) = {x} × {Some qo} × {qs}"
| "gen_set_RD (qo, Bool b, qs) = {}"
| "gen_set_RD (v, Skip, vc) = {} "

definition d_init_RD :: " ('n,'v) def set" where
  "d_init_RD = (UNIV × {None} × {start})"


lemma finite_analysis_dom_RD: "finite analysis_dom_RD"
  by auto

lemma d_init_RD_subset_analysis_dom_RD:
  "d_init_RD ⊆ analysis_dom_RD"
  unfolding d_init_RD_def analysis_dom_RD_def by auto

lemma gen_RD_subset_analysis_dom: "gen_set_RD e ⊆ analysis_dom_RD"
  unfolding analysis_dom_RD_def by auto

lemma kill_RD_subset_analysis_dom: "kill_set_RD e ⊆ analysis_dom_RD"
  unfolding analysis_dom_RD_def by auto

interpretation fw_may: analysis_BV_forward_may pg analysis_dom_RD kill_set_RD gen_set_RD d_init_RD 
  using analysis_BV_forward_may_def analysis_RD_axioms analysis_RD_def
    d_init_RD_subset_analysis_dom_RD finite_analysis_dom_RD gen_RD_subset_analysis_dom 
    kill_RD_subset_analysis_dom analysis_BV_forward_may_axioms.intro by metis

lemma def_var_def_edge_S_hat:
  assumes "def_var π x start ∈ R"
  assumes "x ∉ def_edge t"
  shows "def_var π x start ∈ fw_may.S_hat t R"
proof -
  define q1 where "q1 = fst t"
  define α where "α = fst (snd t)"
  define q2 where "q2 = snd (snd t)"
  have t_def: "t = (q1, α, q2)"
    by (simp add: α_def q1_def q2_def)

  from assms(2) have x_not_def: "x ∉ def_edge (q1, α, q2)"
    unfolding t_def by auto

  have "def_var π x start ∈ fw_may.S_hat (q1, α, q2) R"
  proof (cases α)
    case (Asg y exp)
    then show ?thesis
      by (metis (no_types, lifting) DiffI Un_iff assms(1) x_not_def def_action.simps(1) def_var_x fw_may.S_hat_def kill_set_RD.simps(1) mem_Sigma_iff old.prod.case prod.collapse)
  next
    case (Bool b)
    then show ?thesis
      by (simp add: fw_may.S_hat_def assms(1))
  next
    case Skip
    then show ?thesis
      by (simp add: fw_may.S_hat_def assms(1))
  qed
  then show ?thesis
    unfolding t_def by auto
qed

lemma def_var_S_hat_edge_list: "(def_var π) x start ∈ fw_may.S_hat_edge_list π d_init_RD"
proof (induction π rule: rev_induct)
  case Nil
  then show ?case
    unfolding def_var_def d_init_RD_def by auto
next
  case (snoc t π)
  then show ?case
  proof (cases "x ∈ def_edge t")
    case True
    then have "def_var (π @[t]) x start = def_var [t] x start"
      by (simp add: def_var_def)
    moreover
    have "fw_may.S_hat_edge_list (π @ [t]) d_init_RD = fw_may.S_hat t (fw_may.S_hat_edge_list π d_init_RD)"
      unfolding fw_may.S_hat_edge_list_def2 by simp
    moreover
    obtain q1 α q2 where t_split: "t = (q1, α, q2)"
      using prod_cases3 by blast
    moreover
    have "def_var [t] x start ∈ fw_may.S_hat t (fw_may.S_hat_edge_list π d_init_RD)"
      unfolding fw_may.S_hat_def def_var_def def_of_def using True t_split by (cases α) auto
    ultimately
    show ?thesis by auto
  next
    case False
    obtain q1 α q2 where t_split: "t = (q1, α, q2)"
      using prod_cases3 by blast
    from False have "def_var (π @ [t]) x start = def_var π x start"
      by (simp add: def_var_def)
    moreover
    from snoc.IH have "def_var π x start ∈ fw_may.S_hat t (fw_may.S_hat_edge_list π d_init_RD)"
      by (simp add: False def_var_def_edge_S_hat)
    then have "def_var π x start ∈ fw_may.S_hat_edge_list (π @ [t]) d_init_RD"
      unfolding fw_may.S_hat_edge_list_def2 by simp
    ultimately
    show ?thesis
      using snoc by auto
  qed
qed

lemma last_overwrites:
  "def_var (π @ [(q1, x ::= exp, q2)]) x start = (x, Some q1, q2)"
proof -
  have "x ∈ def_edge (q1, x ::= exp, q2)"
    by auto
  then have "∃e∈set (π @ [(q1, x ::= exp, q2)]). x ∈ def_edge e"
    by auto
  have "def_var (π @ [(q1, x ::= exp, q2)]) x start = def_of x (last (filter (λe. x ∈ def_edge e) (π @ [(q1, x ::= exp, q2)])))"
    unfolding def_var_def by auto
  also
  have "... = def_of x (q1, x ::= exp, q2)"
    by auto
  also
  have "... = (x, Some q1, q2)"
    unfolding def_of_def by auto
  finally
  show ?thesis
    .
qed

lemma S_hat_edge_list_last: "fw_may.S_hat_edge_list (π @ [e]) d_init_RD = fw_may.S_hat e (fw_may.S_hat_edge_list π d_init_RD)"
  using fw_may.S_hat_edge_list_def2 foldl_conv_foldr by simp

lemma def_var_if_S_hat:
  assumes "(x,q1,q2) ∈ fw_may.S_hat_edge_list π d_init_RD"
  shows "(x,q1,q2) = (def_var π) x start"
  using assms
proof (induction π rule: rev_induct)
  case Nil
  then show ?case
    by (metis append_is_Nil_conv d_init_RD_def def_var_def in_set_conv_decomp fw_may.S_hat_edge_list.simps(1) list.distinct(1) mem_Sigma_iff singletonD)
next
  case (snoc e π)

  from snoc(2) have "(x, q1, q2) ∈ fw_may.S_hat e (fw_may.S_hat_edge_list π d_init_RD)"
    using S_hat_edge_list_last by blast     

  then have "(x, q1, q2) ∈ fw_may.S_hat_edge_list π d_init_RD - kill_set_RD e ∨ (x, q1, q2) ∈ gen_set_RD e"
    unfolding fw_may.S_hat_def by auto
  then show ?case
  proof
    assume a: "(x, q1, q2) ∈ fw_may.S_hat_edge_list π d_init_RD - kill_set_RD e"
    then have "(x, q1, q2) = def_var π x start"
      using snoc by auto
    moreover
    from a have "(x, q1, q2) ∉ kill_set_RD e"
      by auto
    then have "def_var (π @ [e]) x start = def_var π x start"
    proof -
      assume def_not_kill: "(x, q1, q2) ∉ kill_set_RD e"
      obtain q q' α where "e = (q, α, q')"
        by (cases e) auto
      then have "x ∉ def_edge e"
        using def_not_kill by (cases α) auto
      then show ?thesis
        by (simp add: def_var_def)
    qed
    ultimately
    show ?case
      by auto
  next
    assume a: "(x, q1, q2) ∈ gen_set_RD e"
    obtain q q' α where "e = (q, α, q')"
      by (cases e) auto
    then have "∃exp theq1. e = (theq1, x ::= exp, q2) ∧ q1 = Some theq1"
      using a by (cases α) auto
    then obtain exp theq1 where exp_theq1_p: "e = (theq1, x ::= exp, q2) ∧ q1 = Some theq1"
      by auto
    then have "(x, q1, q2) = def_var (π @ [(theq1, x ::= exp, q2)]) x start"
      using last_overwrites[of π theq1 x exp q2] by auto
    then show ?case
      using exp_theq1_p by auto
  qed
qed

lemma def_var_UNIV_S_hat_edge_list: "(λx. def_var π x start) ` UNIV = fw_may.S_hat_edge_list π d_init_RD"
proof (rule; rule)
  fix x
  assume "x ∈ range (λx. def_var π x start)"
  then show "x ∈ fw_may.S_hat_edge_list π d_init_RD"
    using def_var_S_hat_edge_list by blast
next
  fix x
  assume "x ∈ fw_may.S_hat_edge_list π d_init_RD"
  then show "x ∈ range (λx. def_var π x start)"
    by (metis def_var_if_S_hat prod.collapse range_eqI)
qed

lemma def_path_S_hat_path: "def_path π start = fw_may.S_hat_path π d_init_RD"
  using fw_may.S_hat_path_def def_path_def def_var_UNIV_S_hat_edge_list by metis

definition summarizes_RD :: "(pred, ('n,'v action,('n,'v) def) cst) pred_val ⇒ bool" where
  "summarizes_RD ρ ⟷ (∀π d. π ∈ path_with_word_from start ⟶ d ∈ def_path π start ⟶ 
                        ρ ⊨lh may⟨[CstN (end_of π), CstE d]⟩.)"

theorem RD_sound: 
  assumes "ρ ⊨lst fw_may.ana_pg_fw_may s_BV"
  shows "summarizes_RD ρ"
  using assms def_path_S_hat_path fw_may.sound_ana_pg_fw_may unfolding fw_may.summarizes_fw_may_def summarizes_RD.simps
  using edges_def in_mono edges_def start_def start_def summarizes_RD_def by fastforce 

end

end