Theory LiftingIntra

section ‹Framework Graph Lifting for Noninterference›

theory LiftingIntra 
  imports NonInterferenceIntra Slicing.CDepInstantiations 
begin

text ‹In this section, we show how a valid CFG from the slicing framework in
\<^cite>‹"Wasserrab:08"› can be lifted to fulfil all properties of the 
‹NonInterferenceIntraGraph› locale. Basically, we redefine the
hitherto existing ‹Entry› and ‹Exit› nodes as new
‹High› and ‹Low› nodes, and introduce two new nodes
‹NewEntry› and ‹NewExit›. Then, we have to lift all functions
to operate on this new graph.›

subsection ‹Liftings›

subsubsection ‹The datatypes›

datatype 'node LDCFG_node = Node 'node
  | NewEntry
  | NewExit


type_synonym ('edge,'node,'state) LDCFG_edge = 
  "'node LDCFG_node × ('state edge_kind) × 'node LDCFG_node"


subsubsection ‹Lifting @{term valid_edge}›

inductive lift_valid_edge :: "('edge ⇒ bool) ⇒ ('edge ⇒ 'node) ⇒ ('edge ⇒ 'node) ⇒
  ('edge ⇒ 'state edge_kind) ⇒ 'node ⇒ 'node ⇒ ('edge,'node,'state) LDCFG_edge ⇒ 
  bool"
for valid_edge::"'edge ⇒ bool" and src::"'edge ⇒ 'node" and trg::"'edge ⇒ 'node" 
  and knd::"'edge ⇒ 'state edge_kind" and E::'node and X::'node

where lve_edge:
  "⟦valid_edge a; src a ≠ E ∨ trg a ≠ X; 
    e = (Node (src a),knd a,Node (trg a))⟧
  ⟹ lift_valid_edge valid_edge src trg knd E X e"

  | lve_Entry_edge:
  "e = (NewEntry,(λs. True)⇩√,Node E) 
  ⟹ lift_valid_edge valid_edge src trg knd E X e"

  | lve_Exit_edge:
  "e = (Node X,(λs. True)⇩√,NewExit) 
  ⟹ lift_valid_edge valid_edge src trg knd E X e"

  | lve_Entry_Exit_edge:
  "e = (NewEntry,(λs. False)⇩√,NewExit) 
  ⟹ lift_valid_edge valid_edge src trg knd E X e"


lemma [simp]:"¬ lift_valid_edge valid_edge src trg knd E X (Node E,et,Node X)"
by(auto elim:lift_valid_edge.cases)


subsubsection ‹Lifting @{term Def} and @{term Use} sets›

inductive_set lift_Def_set :: "('node ⇒ 'var set) ⇒ 'node ⇒ 'node ⇒ 
                       'var set ⇒ 'var set ⇒ ('node LDCFG_node × 'var) set"
for Def::"('node ⇒ 'var set)" and E::'node and X::'node 
  and H::"'var set" and L::"'var set"

where lift_Def_node: 
  "V ∈ Def n ⟹ (Node n,V) ∈ lift_Def_set Def E X H L"

  | lift_Def_High:
  "V ∈ H ⟹ (Node E,V) ∈ lift_Def_set Def E X H L"

abbreviation lift_Def :: "('node ⇒ 'var set) ⇒ 'node ⇒ 'node ⇒ 
                       'var set ⇒ 'var set ⇒ 'node LDCFG_node ⇒ 'var set"
  where "lift_Def Def E X H L n ≡ {V. (n,V) ∈ lift_Def_set Def E X H L}"


inductive_set lift_Use_set :: "('node ⇒ 'var set) ⇒ 'node ⇒ 'node ⇒ 
                       'var set ⇒ 'var set ⇒ ('node LDCFG_node × 'var) set"
for Use::"'node ⇒ 'var set" and E::'node and X::'node 
  and H::"'var set" and L::"'var set"

where 
  lift_Use_node: 
  "V ∈ Use n ⟹ (Node n,V) ∈ lift_Use_set Use E X H L"

  | lift_Use_High:
  "V ∈ H ⟹ (Node E,V) ∈ lift_Use_set Use E X H L"

  | lift_Use_Low:
  "V ∈ L ⟹ (Node X,V) ∈ lift_Use_set Use E X H L"


abbreviation lift_Use :: "('node ⇒ 'var set) ⇒ 'node ⇒ 'node ⇒ 
                       'var set ⇒ 'var set ⇒ 'node LDCFG_node ⇒ 'var set"
  where "lift_Use Use E X H L n ≡ {V. (n,V) ∈ lift_Use_set Use E X H L}"



subsection ‹The lifting lemmas›

subsubsection ‹Lifting the basic locales›


abbreviation src :: "('edge,'node,'state) LDCFG_edge ⇒ 'node LDCFG_node"
  where "src a ≡ fst a"

abbreviation trg :: "('edge,'node,'state) LDCFG_edge ⇒ 'node LDCFG_node"
  where "trg a ≡ snd(snd a)"

definition knd :: "('edge,'node,'state) LDCFG_edge ⇒ 'state edge_kind"
  where "knd a ≡ fst(snd a)"


lemma lift_CFG:
  assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
                         state_val Exit"
  shows "CFG src trg
    (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry"
proof -
  interpret CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
                       state_val Exit
    by(rule wf)
  show ?thesis 
  proof
    fix a assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "trg a = NewEntry"
    thus False by(fastforce elim:lift_valid_edge.cases)
  next
    fix a a' 
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'"
      and "src a = src a'" and "trg a = trg a'"
    thus "a = a'"
    proof(induct rule:lift_valid_edge.induct)
      case lve_edge thus ?case by -(erule lift_valid_edge.cases,auto dest:edge_det)
    qed(auto elim:lift_valid_edge.cases)
  qed
qed


lemma lift_CFG_wf:
  assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
                         state_val Exit"
  shows "CFG_wf src trg knd 
         (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
         (lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L) state_val"
proof -
  interpret CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
                       state_val Exit
    by(rule wf)
  interpret CFG:CFG src trg knd
    "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit" NewEntry
    by(fastforce intro:lift_CFG wf)
  show ?thesis
  proof
    show "lift_Def Def Entry Exit H L NewEntry = {} ∧
          lift_Use Use Entry Exit H L NewEntry = {}"
      by(fastforce elim:lift_Use_set.cases lift_Def_set.cases)
  next
    fix a V s 
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "V ∉ lift_Def Def Entry Exit H L (src a)" and "pred (knd a) s"
    thus "state_val (transfer (knd a) s) V = state_val s V"
    proof(induct rule:lift_valid_edge.induct)
      case lve_edge
      thus ?case by(fastforce intro:CFG_edge_no_Def_equal dest:lift_Def_node[of _ Def]
        simp:knd_def)
    qed(auto simp:knd_def)
  next
    fix a s s'
    assume assms:"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      "∀V∈lift_Use Use Entry Exit H L (src a). state_val s V = state_val s' V"
      "pred (knd a) s" "pred (knd a) s'"
    show "∀V∈lift_Def Def Entry Exit H L (src a).
             state_val (transfer (knd a) s) V = state_val (transfer (knd a) s') V"
    proof
      fix V assume "V ∈ lift_Def Def Entry Exit H L (src a)"
      with assms
      show "state_val (transfer (knd a) s) V = state_val (transfer (knd a) s') V"
      proof(induct rule:lift_valid_edge.induct)
        case (lve_edge a e)
        show ?case
        proof (cases "Node (sourcenode a) = Node Entry")
          case True
          hence "sourcenode a = Entry" by simp
          from Entry_Exit_edge obtain a' where "valid_edge a'"
            and "sourcenode a' = Entry" and "targetnode a' = Exit"
            and "kind a' = (λs. False)⇩√" by blast
          have "∃Q. kind a = (Q)⇩√"
          proof(cases "targetnode a = Exit")
            case True
            with ‹valid_edge a› ‹valid_edge a'› ‹sourcenode a = Entry›
              ‹sourcenode a' = Entry› ‹targetnode a' = Exit›
            have "a = a'" by(fastforce dest:edge_det)
            with ‹kind a' = (λs. False)⇩√› show ?thesis by simp
          next
            case False
            with ‹valid_edge a› ‹valid_edge a'› ‹sourcenode a = Entry›
              ‹sourcenode a' = Entry› ‹targetnode a' = Exit›
            show ?thesis by(auto dest:deterministic)
          qed
          from True ‹V ∈ lift_Def Def Entry Exit H L (src e)› Entry_empty
            ‹e = (Node (sourcenode a), kind a, Node (targetnode a))›
          have "V ∈ H" by(fastforce elim:lift_Def_set.cases)
          from True ‹e = (Node (sourcenode a), kind a, Node (targetnode a))›
            ‹sourcenode a ≠ Entry ∨ targetnode a ≠ Exit›
          have "∀V∈H. V ∈ lift_Use Use Entry Exit H L (src e)"
            by(fastforce intro:lift_Use_High)
          with ‹∀V∈lift_Use Use Entry Exit H L (src e). 
                            state_val s V = state_val s' V› ‹V ∈ H›
          have "state_val s V = state_val s' V" by simp
          with ‹e = (Node (sourcenode a), kind a, Node (targetnode a))› 
            ‹∃Q. kind a = (Q)⇩√›
          show ?thesis by(fastforce simp:knd_def)
        next
          case False
          { fix V' assume "V' ∈ Use (sourcenode a)"
            with ‹e = (Node (sourcenode a), kind a, Node (targetnode a))›
            have "V' ∈ lift_Use Use Entry Exit H L (src e)"
              by(fastforce intro:lift_Use_node)
          }
          with ‹∀V∈lift_Use Use Entry Exit H L (src e). 
                            state_val s V = state_val s' V›
          have "∀V∈Use (sourcenode a). state_val s V = state_val s' V"
            by fastforce
          from ‹valid_edge a› this ‹pred (knd e) s› ‹pred (knd e) s'›
            ‹e = (Node (sourcenode a), kind a, Node (targetnode a))›
          have "∀V ∈ Def (sourcenode a). state_val (transfer (kind a) s) V =
            state_val (transfer (kind a) s') V"
            by -(erule CFG_edge_transfer_uses_only_Use,auto simp:knd_def)
          from ‹V ∈ lift_Def Def Entry Exit H L (src e)› False
            ‹e = (Node (sourcenode a), kind a, Node (targetnode a))›
          have "V ∈ Def (sourcenode a)" by(fastforce elim:lift_Def_set.cases)
          with ‹∀V ∈ Def (sourcenode a). state_val (transfer (kind a) s) V =
            state_val (transfer (kind a) s') V›
            ‹e = (Node (sourcenode a), kind a, Node (targetnode a))›
          show ?thesis by(simp add:knd_def)
        qed
      next
        case (lve_Entry_edge e)
        from ‹V ∈ lift_Def Def Entry Exit H L (src e)› 
          ‹e = (NewEntry, (λs. True)⇩√, Node Entry)›
        have False by(fastforce elim:lift_Def_set.cases)
        thus ?case by simp
      next
        case (lve_Exit_edge e)
        from ‹V ∈ lift_Def Def Entry Exit H L (src e)› 
          ‹e = (Node Exit, (λs. True)⇩√, NewExit)›
        have False
          by(fastforce elim:lift_Def_set.cases intro!:Entry_noteq_Exit simp:Exit_empty)
        thus ?case  by simp
      qed(simp add:knd_def)
    qed
  next
    fix a s s'
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "pred (knd a) s" 
      and "∀V∈lift_Use Use Entry Exit H L (src a). state_val s V = state_val s' V"
    thus "pred (knd a) s'"
      by(induct rule:lift_valid_edge.induct,
         auto elim!:CFG_edge_Uses_pred_equal dest:lift_Use_node simp:knd_def)
  next
    fix a a'
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'"
      and "src a = src a'" and "trg a ≠ trg a'"
    thus "∃Q Q'. knd a = (Q)⇩√ ∧ knd a' = (Q')⇩√ ∧ 
                 (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))"
    proof(induct rule:lift_valid_edge.induct)
      case (lve_edge a e)
      from ‹lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'›
        ‹valid_edge a› ‹e = (Node (sourcenode a), kind a, Node (targetnode a))›
        ‹src e = src a'› ‹trg e ≠ trg a'›
      show ?case
      proof(induct rule:lift_valid_edge.induct)
        case lve_edge thus ?case by(auto dest:deterministic simp:knd_def)
      next
        case (lve_Exit_edge e')
        from ‹e = (Node (sourcenode a), kind a, Node (targetnode a))›
          ‹e' = (Node Exit, (λs. True)⇩√, NewExit)› ‹src e = src e'›
        have "sourcenode a = Exit" by simp
        with ‹valid_edge a› have False by(rule Exit_source)
        thus ?case by simp
      qed auto
    qed (fastforce elim:lift_valid_edge.cases simp:knd_def)+
  qed
qed


lemma lift_CFGExit:
  assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
                         state_val Exit"
  shows "CFGExit src trg knd 
         (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) 
         NewEntry NewExit"
proof -
  interpret CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
                       state_val Exit
    by(rule wf)
  interpret CFG:CFG src trg knd
    "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit" NewEntry
    by(fastforce intro:lift_CFG wf)
  show ?thesis
  proof
    fix a assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "src a = NewExit"
    thus False by(fastforce elim:lift_valid_edge.cases)
  next
    from lve_Entry_Exit_edge
    show "∃a. lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a ∧
              src a = NewEntry ∧ trg a = NewExit ∧ knd a = (λs. False)⇩√"
      by(fastforce simp:knd_def)
  qed
qed


lemma lift_CFGExit_wf:
  assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
                         state_val Exit"
  shows "CFGExit_wf src trg knd 
        (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
        (lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L) state_val NewExit"
proof -
  interpret CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
                       state_val Exit
    by(rule wf)
  interpret CFGExit:CFGExit src trg knd
    "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit" 
    NewEntry NewExit
    by(fastforce intro:lift_CFGExit wf)
  interpret CFG_wf:CFG_wf src trg knd
    "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit" 
    NewEntry "lift_Def Def Entry Exit H L" "lift_Use Use Entry Exit H L" state_val
    by(fastforce intro:lift_CFG_wf wf)
  show ?thesis
  proof
    show "lift_Def Def Entry Exit H L NewExit = {} ∧
          lift_Use Use Entry Exit H L NewExit = {}"
      by(fastforce elim:lift_Use_set.cases lift_Def_set.cases)
  qed
qed



subsubsection ‹Lifting @{term wod_backward_slice}›

lemma lift_wod_backward_slice:
  fixes valid_edge and sourcenode and targetnode and kind and Entry and Exit
  and Def and Use and H and L
  defines lve:"lve ≡ lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit"
  and lDef:"lDef ≡ lift_Def Def Entry Exit H L" 
  and lUse:"lUse ≡ lift_Use Use Entry Exit H L"
  assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
                         state_val Exit"
  and "H ∩ L = {}" and "H ∪ L = UNIV"
  shows "NonInterferenceIntraGraph src trg knd lve NewEntry lDef lUse state_val 
         (CFG_wf.wod_backward_slice src trg lve lDef lUse)
         NewExit H L (Node Entry) (Node Exit)"
proof -
  interpret CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
                       state_val Exit
    by(rule wf)
  interpret CFGExit_wf:
    CFGExit_wf src trg knd lve NewEntry lDef lUse state_val NewExit
    by(fastforce intro:lift_CFGExit_wf wf simp:lve lDef lUse)
  from wf lve have CFG:"CFG src trg lve NewEntry"
    by(fastforce intro:lift_CFG)
  from wf lve lDef lUse have CFG_wf:"CFG_wf src trg knd lve NewEntry
    lDef lUse state_val"
    by(fastforce intro:lift_CFG_wf)
  show ?thesis
  proof
    fix n S
    assume "n ∈ CFG_wf.wod_backward_slice src trg lve lDef lUse S"
    with CFG_wf show "CFG.valid_node src trg lve n"
      by -(rule CFG_wf.wod_backward_slice_valid_node)
  next
    fix n S assume "CFG.valid_node src trg lve n" and "n ∈ S"
    with CFG_wf show "n ∈ CFG_wf.wod_backward_slice src trg lve lDef lUse S"
      by -(rule CFG_wf.refl)
  next
    fix n' S n V
    assume "n' ∈ CFG_wf.wod_backward_slice src trg lve lDef lUse S"
      and "CFG_wf.data_dependence src trg lve lDef lUse n V n'"
    with CFG_wf show "n ∈ CFG_wf.wod_backward_slice src trg lve lDef lUse S"
      by -(rule CFG_wf.dd_closed)
  next
    fix n S
    from CFG_wf 
    have "(∃m. (CFG.obs src trg lve n
        (CFG_wf.wod_backward_slice src trg lve lDef lUse S)) = {m}) ∨
      CFG.obs src trg lve n (CFG_wf.wod_backward_slice src trg lve lDef lUse S) = {}"
      by(rule CFG_wf.obs_singleton)
    thus "finite 
      (CFG.obs src trg lve n (CFG_wf.wod_backward_slice src trg lve lDef lUse S))"
      by fastforce
  next
    fix n S
    from CFG_wf 
    have "(∃m. (CFG.obs src trg lve n
        (CFG_wf.wod_backward_slice src trg lve lDef lUse S)) = {m}) ∨
      CFG.obs src trg lve n (CFG_wf.wod_backward_slice src trg lve lDef lUse S) = {}"
      by(rule CFG_wf.obs_singleton)
    thus "card (CFG.obs src trg lve n
                        (CFG_wf.wod_backward_slice src trg lve lDef lUse S)) ≤ 1"
      by fastforce
  next
    fix a assume "lve a" and "src a = NewEntry"
    with lve show "trg a = NewExit ∨ trg a = Node Entry"
      by(fastforce elim:lift_valid_edge.cases)
  next
    from lve_Entry_edge lve
    show "∃a. lve a ∧ src a = NewEntry ∧ trg a = Node Entry ∧ knd a = (λs. True)⇩√"
      by(fastforce simp:knd_def)
  next
    fix a assume "lve a" and "trg a = Node Entry"
    with lve show "src a = NewEntry" by(fastforce elim:lift_valid_edge.cases)
  next
    fix a assume "lve a" and "trg a = NewExit"
    with lve show "src a = NewEntry ∨ src a = Node Exit"
      by(fastforce elim:lift_valid_edge.cases)
  next
    from lve_Exit_edge lve
    show "∃a. lve a ∧ src a = Node Exit ∧ trg a = NewExit ∧ knd a = (λs. True)⇩√"
      by(fastforce simp:knd_def)
  next
    fix a assume "lve a" and "src a = Node Exit"
    with lve show "trg a = NewExit" by(fastforce elim:lift_valid_edge.cases)
  next
    from lDef show "lDef (Node Entry) = H"
      by(fastforce elim:lift_Def_set.cases intro:lift_Def_High)
  next
    from Entry_noteq_Exit lUse show "lUse (Node Entry) = H"
      by(fastforce elim:lift_Use_set.cases intro:lift_Use_High)
  next
    from Entry_noteq_Exit lUse show "lUse (Node Exit) = L"
      by(fastforce elim:lift_Use_set.cases intro:lift_Use_Low)
  next
    from ‹H ∩ L = {}› show "H ∩ L = {}" .
  next
    from ‹H ∪ L = UNIV› show "H ∪ L = UNIV" .
  qed
qed


subsubsection ‹Lifting ‹PDG_BS› with ‹standard_control_dependence››

lemma lift_Postdomination:
  assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
                         state_val Exit"
  and pd:"Postdomination sourcenode targetnode kind valid_edge Entry Exit"
  and inner:"CFGExit.inner_node sourcenode targetnode valid_edge Entry Exit nx"
  shows "Postdomination src trg knd
  (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry NewExit"
proof -
  interpret Postdomination sourcenode targetnode kind valid_edge Entry Exit
    by(rule pd)
  interpret CFGExit_wf:CFGExit_wf src trg knd
    "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit" NewEntry
    "lift_Def Def Entry Exit H L" "lift_Use Use Entry Exit H L" state_val NewExit
    by(fastforce intro:lift_CFGExit_wf wf)
  from wf have CFG:"CFG src trg
    (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry"
    by(rule lift_CFG)
  show ?thesis
  proof
    fix n assume "CFG.valid_node src trg
      (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) n"
    show "∃as. CFG.path src trg
      (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
      NewEntry as n"
    proof(cases n)
      case NewEntry
      have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
        (NewEntry,(λs. False)⇩√,NewExit)" by(fastforce intro:lve_Entry_Exit_edge)
      with NewEntry have "CFG.path src trg
        (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
        NewEntry [] n"
        by(fastforce intro:CFG.empty_path[OF CFG] simp:CFG.valid_node_def[OF CFG])
      thus ?thesis by blast
    next
      case NewExit
      have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
        (NewEntry,(λs. False)⇩√,NewExit)" by(fastforce intro:lve_Entry_Exit_edge)
      with NewExit have "CFG.path src trg
        (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
        NewEntry [(NewEntry,(λs. False)⇩√,NewExit)] n"
        by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
                     simp:CFG.valid_node_def[OF CFG])
      thus ?thesis by blast
    next
      case (Node m)
      with Entry_Exit_edge ‹CFG.valid_node src trg
        (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) n›
      have "valid_node m" 
        by(auto elim:lift_valid_edge.cases 
                simp:CFG.valid_node_def[OF CFG] valid_node_def)
      thus ?thesis
      proof(cases m rule:valid_node_cases)
        case Entry
        have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
          (NewEntry,(λs. True)⇩√,Node Entry)" by(fastforce intro:lve_Entry_edge)
        with Entry Node have "CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          NewEntry [(NewEntry,(λs. True)⇩√,Node Entry)] n"
          by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
                       simp:CFG.valid_node_def[OF CFG])
        thus ?thesis by blast
      next
        case Exit
        from inner obtain ax where "valid_edge ax" and "inner_node (sourcenode ax)"
          and "targetnode ax = Exit" by(erule inner_node_Exit_edge)
        hence "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
          (Node (sourcenode ax),kind ax,Node Exit)"
          by(auto intro:lift_valid_edge.lve_edge simp:inner_node_def)
        hence path:"CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          (Node (sourcenode ax)) [(Node (sourcenode ax),kind ax,Node Exit)] 
          (Node Exit)"
          by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
                       simp:CFG.valid_node_def[OF CFG])
        have edge:"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
          (NewEntry,(λs. True)⇩√,Node Entry)" by(fastforce intro:lve_Entry_edge)
        from ‹inner_node (sourcenode ax)› have "valid_node (sourcenode ax)"
          by(rule inner_is_valid)
        then obtain asx where "Entry -asx→* sourcenode ax"
          by(fastforce dest:Entry_path)
        from this ‹valid_edge ax› have "∃es. CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          (Node Entry) es (Node (sourcenode ax))"
        proof(induct asx arbitrary:ax rule:rev_induct)
          case Nil
          from ‹Entry -[]→* sourcenode ax› have "sourcenode ax = Entry" by fastforce
          hence "CFG.path src trg
            (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
            (Node Entry) [] (Node (sourcenode ax))"
            apply simp apply(rule CFG.empty_path[OF CFG])
            by(auto intro:lve_Entry_edge simp:CFG.valid_node_def[OF CFG])
          thus ?case by blast
        next
          case (snoc x xs)
          note IH = ‹⋀ax. ⟦Entry -xs→* sourcenode ax; valid_edge ax⟧ ⟹
            ∃es. CFG.path src trg
            (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
            (Node Entry) es (Node (sourcenode ax))›
          from ‹Entry -xs@[x]→* sourcenode ax›
          have "Entry -xs→* sourcenode x" and "valid_edge x"
            and "targetnode x = sourcenode ax" by(auto elim:path_split_snoc)
          { assume "targetnode x = Exit"
            with ‹valid_edge ax› ‹targetnode x = sourcenode ax›
            have False by -(rule Exit_source,simp+) }
          hence "targetnode x ≠ Exit" by clarsimp
          with ‹valid_edge x› ‹targetnode x = sourcenode ax›[THEN sym]
          have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
            (Node (sourcenode x),kind x,Node (sourcenode ax))"
            by(fastforce intro:lift_valid_edge.lve_edge)
          hence path:"CFG.path src trg
            (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
            (Node (sourcenode x)) [(Node (sourcenode x),kind x,Node (sourcenode ax))] 
            (Node (sourcenode ax))"
            by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
                         simp:CFG.valid_node_def[OF CFG])
          from IH[OF ‹Entry -xs→* sourcenode x› ‹valid_edge x›] obtain es
            where "CFG.path src trg
            (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
            (Node Entry) es (Node (sourcenode x))" by blast
          with path have "CFG.path src trg
            (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
            (Node Entry) (es@[(Node (sourcenode x),kind x,Node (sourcenode ax))])
            (Node (sourcenode ax))"
            by -(rule CFG.path_Append[OF CFG])
          thus ?case by blast
        qed
        then obtain es where "CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          (Node Entry) es (Node (sourcenode ax))" by blast
        with path have "CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          (Node Entry) (es@ [(Node (sourcenode ax),kind ax,Node Exit)]) (Node Exit)"
          by -(rule CFG.path_Append[OF CFG])
        with edge have "CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          NewEntry ((NewEntry,(λs. True)⇩√,Node Entry)#
                      (es@ [(Node (sourcenode ax),kind ax,Node Exit)])) (Node Exit)"
          by(fastforce intro:CFG.Cons_path[OF CFG])
        with Node Exit show ?thesis by fastforce
      next
        case inner
        from ‹valid_node m› obtain as where "Entry -as→* m"
          by(fastforce dest:Entry_path)
        with inner have "∃es. CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          (Node Entry) es (Node m)"
        proof(induct arbitrary:m rule:rev_induct)
          case Nil
          from ‹Entry -[]→* m›
          have "m = Entry" by fastforce
          with lve_Entry_edge have "CFG.path src trg
            (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
            (Node Entry) [] (Node m)"
            by(fastforce intro:CFG.empty_path[OF CFG] simp:CFG.valid_node_def[OF CFG])
          thus ?case by blast
        next
          case (snoc x xs)
          note IH = ‹⋀m. ⟦inner_node m; Entry -xs→* m⟧
            ⟹ ∃es. CFG.path src trg
            (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
            (Node Entry) es (Node m)›
          from ‹Entry -xs@[x]→* m› have "Entry -xs→* sourcenode x"
            and "valid_edge x" and "m = targetnode x" by(auto elim:path_split_snoc)
          with ‹inner_node m›
          have edge:"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
            (Node (sourcenode x),kind x,Node m)"
            by(fastforce intro:lve_edge simp:inner_node_def)
          hence path:"CFG.path src trg
            (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
            (Node (sourcenode x)) [(Node (sourcenode x),kind x,Node m)] (Node m)"
            by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
                         simp:CFG.valid_node_def[OF CFG])
          from ‹valid_edge x› have "valid_node (sourcenode x)" by simp
          thus ?case
          proof(cases "sourcenode x" rule:valid_node_cases)
            case Entry
            with edge have "CFG.path src trg
              (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
              (Node Entry) [(Node Entry,kind x,Node m)] (Node m)"
              apply - apply(rule CFG.Cons_path[OF CFG])
              apply(rule CFG.empty_path[OF CFG]) 
              by(auto simp:CFG.valid_node_def[OF CFG])
            thus ?thesis by blast
          next
            case Exit
            with ‹valid_edge x› have False by(rule Exit_source)
            thus ?thesis by simp
          next
            case inner
            from IH[OF this ‹Entry -xs→* sourcenode x›] obtain es 
              where "CFG.path src trg
              (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
              (Node Entry) es (Node (sourcenode x))" by blast
            with path have "CFG.path src trg
              (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
              (Node Entry) (es@[(Node (sourcenode x),kind x,Node m)]) (Node m)"
              by -(rule CFG.path_Append[OF CFG])
            thus ?thesis by blast
          qed
        qed
        then obtain es where path:"CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          (Node Entry) es (Node m)" by blast
        have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
          (NewEntry,(λs. True)⇩√,Node Entry)" by(fastforce intro:lve_Entry_edge)
        from this path Node have "CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          NewEntry ((NewEntry,(λs. True)⇩√,Node Entry)#es) n"
          by(fastforce intro:CFG.Cons_path[OF CFG])
        thus ?thesis by blast
      qed
    qed
  next
    fix n assume "CFG.valid_node src trg
      (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) n"
    show "∃as. CFG.path src trg
      (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
      n as NewExit"
    proof(cases n)
      case NewEntry
      have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
        (NewEntry,(λs. False)⇩√,NewExit)" by(fastforce intro:lve_Entry_Exit_edge)
      with NewEntry have "CFG.path src trg
        (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
        n [(NewEntry,(λs. False)⇩√,NewExit)] NewExit"
        by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
                     simp:CFG.valid_node_def[OF CFG])
      thus ?thesis by blast
    next
      case NewExit
      have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
        (NewEntry,(λs. False)⇩√,NewExit)" by(fastforce intro:lve_Entry_Exit_edge)
      with NewExit have "CFG.path src trg
        (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
        n [] NewExit"
        by(fastforce intro:CFG.empty_path[OF CFG] simp:CFG.valid_node_def[OF CFG])
      thus ?thesis by blast
    next
      case (Node m)
      with Entry_Exit_edge ‹CFG.valid_node src trg
        (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) n›
      have "valid_node m" 
        by(auto elim:lift_valid_edge.cases 
                simp:CFG.valid_node_def[OF CFG] valid_node_def)
      thus ?thesis
      proof(cases m rule:valid_node_cases)
        case Entry
        from inner obtain ax where "valid_edge ax" and "inner_node (targetnode ax)"
          and "sourcenode ax = Entry" by(erule inner_node_Entry_edge)
        hence edge:"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
          (Node Entry,kind ax,Node (targetnode ax))"
          by(auto intro:lift_valid_edge.lve_edge simp:inner_node_def)
        have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
          (Node Exit,(λs. True)⇩√,NewExit)" by(fastforce intro:lve_Exit_edge)
        hence path:"CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          (Node Exit) [(Node Exit,(λs. True)⇩√,NewExit)] (NewExit)"
          by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
                       simp:CFG.valid_node_def[OF CFG])
        from ‹inner_node (targetnode ax)› have "valid_node (targetnode ax)"
          by(rule inner_is_valid)
        then obtain asx where "targetnode ax -asx→* Exit" by(fastforce dest:Exit_path)
        from this ‹valid_edge ax› have "∃es. CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          (Node (targetnode ax)) es (Node Exit)"
        proof(induct asx arbitrary:ax)
          case Nil
          from ‹targetnode ax -[]→* Exit› have "targetnode ax = Exit" by fastforce
          hence "CFG.path src trg
            (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
            (Node (targetnode ax)) [] (Node Exit)"
            apply simp apply(rule CFG.empty_path[OF CFG])
            by(auto intro:lve_Exit_edge simp:CFG.valid_node_def[OF CFG])
          thus ?case by blast
        next
          case (Cons x xs)
          note IH = ‹⋀ax. ⟦targetnode ax -xs→* Exit; valid_edge ax⟧ ⟹
            ∃es. CFG.path src trg
            (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
            (Node (targetnode ax)) es (Node Exit)›
          from ‹targetnode ax -x#xs→* Exit›
          have "targetnode x -xs→* Exit" and "valid_edge x"
            and "sourcenode x = targetnode ax" by(auto elim:path_split_Cons)
          { assume "sourcenode x = Entry"
            with ‹valid_edge ax› ‹sourcenode x = targetnode ax›
            have False by -(rule Entry_target,simp+) }
          hence "sourcenode x ≠ Entry" by clarsimp
          with ‹valid_edge x› ‹sourcenode x = targetnode ax›[THEN sym]
          have edge:"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
            (Node (targetnode ax),kind x,Node (targetnode x))"
            by(fastforce intro:lift_valid_edge.lve_edge)
          from IH[OF ‹targetnode x -xs→* Exit› ‹valid_edge x›] obtain es
            where "CFG.path src trg
            (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
            (Node (targetnode x)) es (Node Exit)" by blast
          with edge have "CFG.path src trg
            (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
            (Node (targetnode ax)) 
            ((Node (targetnode ax),kind x,Node (targetnode x))#es) (Node Exit)"
            by(fastforce intro:CFG.Cons_path[OF CFG])
          thus ?case by blast
        qed
        then obtain es where "CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          (Node (targetnode ax)) es (Node Exit)" by blast
        with edge have "CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          (Node Entry) ((Node Entry, kind ax, Node (targetnode ax))#es) (Node Exit)"
          by(fastforce intro:CFG.Cons_path[OF CFG])
        with path have "CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          (Node Entry) (((Node Entry,kind ax,Node (targetnode ax))#es)@
                        [(Node Exit, (λs. True)⇩√, NewExit)]) NewExit"
          by -(rule CFG.path_Append[OF CFG])
        with Node Entry show ?thesis by fastforce
      next
        case Exit
        have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
          (Node Exit,(λs. True)⇩√,NewExit)" by(fastforce intro:lve_Exit_edge)
        with Exit Node have "CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          n [(Node Exit,(λs. True)⇩√,NewExit)] NewExit"
          by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
                       simp:CFG.valid_node_def[OF CFG])
        thus ?thesis by blast
      next
        case inner
        from ‹valid_node m› obtain as where "m -as→* Exit"
          by(fastforce dest:Exit_path)
        with inner have "∃es. CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          (Node m) es (Node Exit)"
        proof(induct as arbitrary:m)
          case Nil
          from ‹m -[]→* Exit›
          have "m = Exit" by fastforce
          with lve_Exit_edge have "CFG.path src trg
            (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
            (Node m) [] (Node Exit)"
            by(fastforce intro:CFG.empty_path[OF CFG] simp:CFG.valid_node_def[OF CFG])
          thus ?case by blast
        next
          case (Cons x xs)
          note IH = ‹⋀m. ⟦inner_node m; m -xs→* Exit⟧
            ⟹ ∃es. CFG.path src trg
            (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
            (Node m) es (Node Exit)›
          from ‹m -x#xs→* Exit› have "targetnode x -xs→* Exit"
            and "valid_edge x" and "m = sourcenode x" by(auto elim:path_split_Cons)
          with ‹inner_node m›
          have edge:"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
            (Node m,kind x,Node (targetnode x))"
            by(fastforce intro:lve_edge simp:inner_node_def)
          from ‹valid_edge x› have "valid_node (targetnode x)" by simp
          thus ?case
          proof(cases "targetnode x" rule:valid_node_cases)
            case Entry
            with ‹valid_edge x› have False by(rule Entry_target)
            thus ?thesis by simp
          next
            case Exit
            with edge have "CFG.path src trg
              (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
              (Node m) [(Node m,kind x,Node Exit)] (Node Exit)"
              apply - apply(rule CFG.Cons_path[OF CFG])
              apply(rule CFG.empty_path[OF CFG]) 
              by(auto simp:CFG.valid_node_def[OF CFG])
            thus ?thesis by blast
          next
            case inner
            from IH[OF this ‹targetnode x -xs→* Exit›] obtain es 
              where "CFG.path src trg
              (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
              (Node (targetnode x)) es (Node Exit)" by blast
            with edge have "CFG.path src trg
              (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
              (Node m) ((Node m,kind x,Node (targetnode x))#es) (Node Exit)"
              by(fastforce intro:CFG.Cons_path[OF CFG])
            thus ?thesis by blast
          qed
        qed
        then obtain es where path:"CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          (Node m) es (Node Exit)" by blast
        have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
          (Node Exit,(λs. True)⇩√,NewExit)" by(fastforce intro:lve_Exit_edge)
        hence "CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          (Node Exit) [(Node Exit,(λs. True)⇩√,NewExit)] NewExit"
          by(fastforce intro:CFG.Cons_path[OF CFG] CFG.empty_path[OF CFG]
                       simp:CFG.valid_node_def[OF CFG])
        with path Node have "CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          n (es@[(Node Exit, (λs. True)⇩√, NewExit)]) NewExit"
          by(fastforce intro:CFG.path_Append[OF CFG])
        thus ?thesis by blast
      qed
    qed
  qed
qed


lemma lift_PDG_scd:
  assumes PDG:"PDG sourcenode targetnode kind valid_edge Entry Def Use state_val Exit 
  (Postdomination.standard_control_dependence sourcenode targetnode valid_edge Exit)"
  and pd:"Postdomination sourcenode targetnode kind valid_edge Entry Exit"
  and inner:"CFGExit.inner_node sourcenode targetnode valid_edge Entry Exit nx"
  shows "PDG src trg knd 
  (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
  (lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L) state_val NewExit
  (Postdomination.standard_control_dependence src trg 
    (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewExit)"
proof -
  interpret PDG sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
    "Postdomination.standard_control_dependence sourcenode targetnode 
                                                           valid_edge Exit"
    by(rule PDG)
  have wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
                            state_val Exit" by(unfold_locales)
  from wf pd inner have pd':"Postdomination src trg knd
    (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) 
    NewEntry NewExit"
    by(rule lift_Postdomination)
  from wf have CFG:"CFG src trg
    (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry"
    by(rule lift_CFG)
  from wf have CFG_wf:"CFG_wf src trg knd
    (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
    (lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L) state_val"
    by(rule lift_CFG_wf)
  from wf have CFGExit:"CFGExit src trg knd 
    (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) 
    NewEntry NewExit"
    by(rule lift_CFGExit)
  from wf have CFGExit_wf:"CFGExit_wf src trg knd 
    (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
    (lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L) state_val NewExit"
    by(rule lift_CFGExit_wf)
  show ?thesis
  proof
    fix a assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "trg a = NewEntry"
    with CFG show False by(rule CFG.Entry_target)
  next
    fix a a' 
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'"
      and "src a = src a'" and "trg a = trg a'"
    with CFG show "a = a'" by(rule CFG.edge_det)
  next
    from CFG_wf
    show "lift_Def Def Entry Exit H L NewEntry = {} ∧
          lift_Use Use Entry Exit H L NewEntry = {}"
      by(rule CFG_wf.Entry_empty)
  next
    fix a V s 
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "V ∉ lift_Def Def Entry Exit H L (src a)" and "pred (knd a) s"
    with CFG_wf show "state_val (transfer (knd a) s) V = state_val s V"
      by(rule CFG_wf.CFG_edge_no_Def_equal)
  next
    fix a s s'
    assume assms:"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      "∀V∈lift_Use Use Entry Exit H L (src a). state_val s V = state_val s' V"
      "pred (knd a) s" "pred (knd a) s'"
    with CFG_wf show "∀V∈lift_Def Def Entry Exit H L (src a).
             state_val (transfer (knd a) s) V = state_val (transfer (knd a) s') V"
      by(rule CFG_wf.CFG_edge_transfer_uses_only_Use)
  next
    fix a s s'
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "pred (knd a) s" 
      and "∀V∈lift_Use Use Entry Exit H L (src a). state_val s V = state_val s' V"
    with CFG_wf show "pred (knd a) s'" by(rule CFG_wf.CFG_edge_Uses_pred_equal)
  next
    fix a a'
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'"
      and "src a = src a'" and "trg a ≠ trg a'"
    with CFG_wf show "∃Q Q'. knd a = (Q)⇩√ ∧ knd a' = (Q')⇩√ ∧ 
                             (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))"
      by(rule CFG_wf.deterministic)
  next
    fix a assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "src a = NewExit"
    with CFGExit show False by(rule CFGExit.Exit_source)
  next
    from CFGExit
    show "∃a. lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a ∧
              src a = NewEntry ∧ trg a = NewExit ∧ knd a = (λs. False)⇩√"
      by(rule CFGExit.Entry_Exit_edge)
  next
    from CFGExit_wf
    show "lift_Def Def Entry Exit H L NewExit = {} ∧
          lift_Use Use Entry Exit H L NewExit = {}"
      by(rule CFGExit_wf.Exit_empty)
  next
    fix n n'
    assume scd:"Postdomination.standard_control_dependence src trg
      (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewExit n n'"
    show "n' ≠ NewExit"
    proof(rule ccontr)
      assume "¬ n' ≠ NewExit"
      hence "n' = NewExit" by simp
      with scd pd' show False 
        by(fastforce intro:Postdomination.Exit_not_standard_control_dependent)
    qed
  next
    fix n n'
    assume "Postdomination.standard_control_dependence src trg
      (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewExit n n'"
    thus "∃as. CFG.path src trg
               (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
               n as n' ∧ as ≠ []"
      by(fastforce simp:Postdomination.standard_control_dependence_def[OF pd'])
  qed
qed




lemma lift_PDG_standard_backward_slice:
  fixes valid_edge and sourcenode and targetnode and kind and Entry and Exit
  and Def and Use and H and L
  defines lve:"lve ≡ lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit"
  and lDef:"lDef ≡ lift_Def Def Entry Exit H L" 
  and lUse:"lUse ≡ lift_Use Use Entry Exit H L"
  assumes PDG:"PDG sourcenode targetnode kind valid_edge Entry Def Use state_val Exit 
  (Postdomination.standard_control_dependence sourcenode targetnode valid_edge Exit)"
  and pd:"Postdomination sourcenode targetnode kind valid_edge Entry Exit"
  and inner:"CFGExit.inner_node sourcenode targetnode valid_edge Entry Exit nx"
  and "H ∩ L = {}" and "H ∪ L = UNIV"
  shows "NonInterferenceIntraGraph src trg knd lve NewEntry lDef lUse state_val 
         (PDG.PDG_BS src trg lve lDef lUse
           (Postdomination.standard_control_dependence src trg lve NewExit))
         NewExit H L (Node Entry) (Node Exit)"
proof -
  interpret PDG sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
    "Postdomination.standard_control_dependence sourcenode targetnode 
                                                           valid_edge Exit"
    by(rule PDG)
  have wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
                            state_val Exit" by(unfold_locales)
  interpret wf':CFGExit_wf src trg knd lve NewEntry lDef lUse state_val NewExit
    by(fastforce intro:lift_CFGExit_wf wf simp:lve lDef lUse)
  from PDG pd inner lve lDef lUse have PDG':"PDG src trg knd 
    lve NewEntry lDef lUse state_val NewExit
    (Postdomination.standard_control_dependence src trg lve NewExit)"
    by(fastforce intro:lift_PDG_scd)
  from wf pd inner have pd':"Postdomination src trg knd
    (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) 
    NewEntry NewExit"
    by(rule lift_Postdomination)
  from wf lve have CFG:"CFG src trg lve NewEntry"
    by(fastforce intro:lift_CFG)
  from wf lve lDef lUse 
  have CFG_wf:"CFG_wf src trg knd lve NewEntry lDef lUse state_val"
    by(fastforce intro:lift_CFG_wf)
  from wf lve have CFGExit:"CFGExit src trg knd lve NewEntry NewExit"
    by(fastforce intro:lift_CFGExit)
  from wf lve lDef lUse 
  have CFGExit_wf:"CFGExit_wf src trg knd lve NewEntry lDef lUse state_val NewExit"
    by(fastforce intro:lift_CFGExit_wf)
  show ?thesis
  proof
    fix n S
    assume "n ∈ PDG.PDG_BS src trg lve lDef lUse
      (Postdomination.standard_control_dependence src trg lve NewExit) S"
    with PDG' show "CFG.valid_node src trg lve n"
      by(rule PDG.PDG_BS_valid_node)
  next
    fix n S assume "CFG.valid_node src trg lve n" and "n ∈ S"
    thus "n ∈ PDG.PDG_BS src trg lve lDef lUse
      (Postdomination.standard_control_dependence src trg lve NewExit) S"
      by(fastforce intro:PDG.PDG_path_Nil[OF PDG'] simp:PDG.PDG_BS_def[OF PDG'])
  next
    fix n' S n V
    assume "n' ∈ PDG.PDG_BS src trg lve lDef lUse
      (Postdomination.standard_control_dependence src trg lve NewExit) S"
      and "CFG_wf.data_dependence src trg lve lDef lUse n V n'"
    thus "n ∈ PDG.PDG_BS src trg lve lDef lUse
      (Postdomination.standard_control_dependence src trg lve NewExit) S"
      by(fastforce intro:PDG.PDG_path_Append[OF PDG'] PDG.PDG_path_ddep[OF PDG']
                        PDG.PDG_ddep_edge[OF PDG'] simp:PDG.PDG_BS_def[OF PDG']
                  split:if_split_asm)
  next
    fix n S
    interpret PDGx:PDG src trg knd lve NewEntry lDef lUse state_val NewExit
      "Postdomination.standard_control_dependence src trg lve NewExit"
      by(rule PDG')
    interpret pdx:Postdomination src trg knd lve NewEntry NewExit
      by(fastforce intro:pd' simp:lve)
    have scd:"StandardControlDependencePDG src trg knd lve NewEntry
      lDef lUse state_val NewExit" by(unfold_locales)
    from StandardControlDependencePDG.obs_singleton[OF scd]
    have "(∃m. CFG.obs src trg lve n
      (PDG.PDG_BS src trg lve lDef lUse
        (Postdomination.standard_control_dependence src trg lve NewExit) S) = {m}) ∨
      CFG.obs src trg lve n
      (PDG.PDG_BS src trg lve lDef lUse
        (Postdomination.standard_control_dependence src trg lve NewExit) S) = {}"
      by(fastforce simp:StandardControlDependencePDG.PDG_BS_s_def[OF scd])
    thus "finite (CFG.obs src trg lve n
        (PDG.PDG_BS src trg lve lDef lUse
          (Postdomination.standard_control_dependence src trg lve NewExit) S))"
      by fastforce
  next
    fix n S
    interpret PDGx:PDG src trg knd lve NewEntry lDef lUse state_val NewExit
      "Postdomination.standard_control_dependence src trg lve NewExit"
      by(rule PDG')
    interpret pdx:Postdomination src trg knd lve NewEntry NewExit
      by(fastforce intro:pd' simp:lve)
    have scd:"StandardControlDependencePDG src trg knd lve NewEntry
      lDef lUse state_val NewExit" by(unfold_locales)
    from StandardControlDependencePDG.obs_singleton[OF scd]
    have "(∃m. CFG.obs src trg lve n
      (PDG.PDG_BS src trg lve lDef lUse
        (Postdomination.standard_control_dependence src trg lve NewExit) S) = {m}) ∨
      CFG.obs src trg lve n
      (PDG.PDG_BS src trg lve lDef lUse
        (Postdomination.standard_control_dependence src trg lve NewExit) S) = {}"
      by(fastforce simp:StandardControlDependencePDG.PDG_BS_s_def[OF scd])
    thus "card (CFG.obs src trg lve n
      (PDG.PDG_BS src trg lve lDef lUse
        (Postdomination.standard_control_dependence src trg lve NewExit) S)) ≤ 1"
      by fastforce
  next
    fix a assume "lve a" and "src a = NewEntry"
    with lve show "trg a = NewExit ∨ trg a = Node Entry"
      by(fastforce elim:lift_valid_edge.cases)
  next
    from lve_Entry_edge lve
    show "∃a. lve a ∧ src a = NewEntry ∧ trg a = Node Entry ∧ knd a = (λs. True)⇩√"
      by(fastforce simp:knd_def)
  next
    fix a assume "lve a" and "trg a = Node Entry"
    with lve show "src a = NewEntry" by(fastforce elim:lift_valid_edge.cases)
  next
    fix a assume "lve a" and "trg a = NewExit"
    with lve show "src a = NewEntry ∨ src a = Node Exit"
      by(fastforce elim:lift_valid_edge.cases)
  next
    from lve_Exit_edge lve
    show "∃a. lve a ∧ src a = Node Exit ∧ trg a = NewExit ∧ knd a = (λs. True)⇩√"
      by(fastforce simp:knd_def)
  next
    fix a assume "lve a" and "src a = Node Exit"
    with lve show "trg a = NewExit" by(fastforce elim:lift_valid_edge.cases)
  next
    from lDef show "lDef (Node Entry) = H"
      by(fastforce elim:lift_Def_set.cases intro:lift_Def_High)
  next
    from Entry_noteq_Exit lUse show "lUse (Node Entry) = H"
      by(fastforce elim:lift_Use_set.cases intro:lift_Use_High)
  next
    from Entry_noteq_Exit lUse show "lUse (Node Exit) = L"
      by(fastforce elim:lift_Use_set.cases intro:lift_Use_Low)
  next
    from ‹H ∩ L = {}› show "H ∩ L = {}" .
  next
    from ‹H ∪ L = UNIV› show "H ∪ L = UNIV" .
  qed
qed



subsubsection ‹Lifting ‹PDG_BS› with ‹weak_control_dependence››

lemma lift_StrongPostdomination:
  assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
                         state_val Exit"
  and spd:"StrongPostdomination sourcenode targetnode kind valid_edge Entry Exit"
  and inner:"CFGExit.inner_node sourcenode targetnode valid_edge Entry Exit nx"
  shows "StrongPostdomination src trg knd
  (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry NewExit"
proof -
  interpret StrongPostdomination sourcenode targetnode kind valid_edge Entry Exit
    by(rule spd)
  have pd:"Postdomination sourcenode targetnode kind valid_edge Entry Exit"
    by(unfold_locales)
  interpret pd':Postdomination src trg knd
    "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit"
    NewEntry NewExit
    by(fastforce intro:wf inner lift_Postdomination pd)
  interpret CFGExit_wf:CFGExit_wf src trg knd
    "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit" NewEntry
    "lift_Def Def Entry Exit H L" "lift_Use Use Entry Exit H L" state_val NewExit
    by(fastforce intro:lift_CFGExit_wf wf)
  from wf have CFG:"CFG src trg
    (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry"
    by(rule lift_CFG)
  show ?thesis
  proof
    fix n assume "CFG.valid_node src trg
      (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) n"
    show "finite
      {n'. ∃a'. lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a' ∧
                src a' = n ∧ trg a' = n'}"
    proof(cases n)
      case NewEntry
      hence "{n'. ∃a'. lift_valid_edge valid_edge sourcenode targetnode kind 
                     Entry Exit a' ∧ src a' = n ∧ trg a' = n'} = {NewExit,Node Entry}"
        by(auto elim:lift_valid_edge.cases intro:lift_valid_edge.intros)
      thus ?thesis by simp
    next
      case NewExit
      hence "{n'. ∃a'. lift_valid_edge valid_edge sourcenode targetnode kind 
                     Entry Exit a' ∧ src a' = n ∧ trg a' = n'} = {}"
        by fastforce
      thus ?thesis by simp
    next
      case (Node m)
      with Entry_Exit_edge ‹CFG.valid_node src trg
        (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) n›
      have "valid_node m" 
        by(auto elim:lift_valid_edge.cases 
                simp:CFG.valid_node_def[OF CFG] valid_node_def)
      hence "finite {m'. ∃a'. valid_edge a' ∧ sourcenode a' = m ∧ targetnode a' = m'}"
        by(rule successor_set_finite)
      have "{m'. ∃a'. lift_valid_edge valid_edge sourcenode targetnode kind 
                      Entry Exit a' ∧ src a' = Node m ∧ trg a' = Node m'} ⊆ 
            {m'. ∃a'. valid_edge a' ∧ sourcenode a' = m ∧ targetnode a' = m'}"
        by(fastforce elim:lift_valid_edge.cases)
      with ‹finite {m'. ∃a'. valid_edge a' ∧ sourcenode a' = m ∧ targetnode a' = m'}›
      have "finite {m'. ∃a'. lift_valid_edge valid_edge sourcenode targetnode kind 
                             Entry Exit a' ∧ src a' = Node m ∧ trg a' = Node m'}"
        by -(rule finite_subset)
      hence "finite (Node ` {m'. ∃a'. lift_valid_edge valid_edge sourcenode 
        targetnode kind Entry Exit a' ∧ src a' = Node m ∧ trg a' = Node m'})"
        by fastforce
      hence fin:"finite ((Node ` {m'. ∃a'. lift_valid_edge valid_edge sourcenode 
        targetnode kind Entry Exit a' ∧ src a' = Node m ∧ trg a' = Node m'}) ∪
        {NewEntry,NewExit})" by fastforce
      with Node have "{n'. ∃a'. lift_valid_edge valid_edge sourcenode targetnode kind 
        Entry Exit a' ∧ src a' = n ∧ trg a' = n'} ⊆
        (Node ` {m'. ∃a'. lift_valid_edge valid_edge sourcenode 
        targetnode kind Entry Exit a' ∧ src a' = Node m ∧ trg a' = Node m'}) ∪
        {NewEntry,NewExit}" by auto (case_tac x,auto)
      with fin show ?thesis by -(rule finite_subset)
    qed
  qed
qed





lemma lift_PDG_wcd:
  assumes PDG:"PDG sourcenode targetnode kind valid_edge Entry Def Use state_val Exit 
  (StrongPostdomination.weak_control_dependence sourcenode targetnode 
  valid_edge Exit)"
  and spd:"StrongPostdomination sourcenode targetnode kind valid_edge Entry Exit"
  and inner:"CFGExit.inner_node sourcenode targetnode valid_edge Entry Exit nx"
  shows "PDG src trg knd 
  (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
  (lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L) state_val NewExit
  (StrongPostdomination.weak_control_dependence src trg 
    (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewExit)"
proof -
  interpret PDG sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
    "StrongPostdomination.weak_control_dependence sourcenode targetnode 
                                                           valid_edge Exit"
    by(rule PDG)
  have wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
                            state_val Exit" by(unfold_locales)
  from wf spd inner have spd':"StrongPostdomination src trg knd
    (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) 
    NewEntry NewExit"
    by(rule lift_StrongPostdomination)
  from wf have CFG:"CFG src trg
    (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry"
    by(rule lift_CFG)
  from wf have CFG_wf:"CFG_wf src trg knd
    (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
    (lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L) state_val"
    by(rule lift_CFG_wf)
  from wf have CFGExit:"CFGExit src trg knd 
    (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) 
    NewEntry NewExit"
    by(rule lift_CFGExit)
  from wf have CFGExit_wf:"CFGExit_wf src trg knd 
    (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
    (lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L) state_val NewExit"
    by(rule lift_CFGExit_wf)
  show ?thesis
  proof
    fix a assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "trg a = NewEntry"
    with CFG show False by(rule CFG.Entry_target)
  next
    fix a a' 
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'"
      and "src a = src a'" and "trg a = trg a'"
    with CFG show "a = a'" by(rule CFG.edge_det)
  next
    from CFG_wf
    show "lift_Def Def Entry Exit H L NewEntry = {} ∧
          lift_Use Use Entry Exit H L NewEntry = {}"
      by(rule CFG_wf.Entry_empty)
  next
    fix a V s 
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "V ∉ lift_Def Def Entry Exit H L (src a)" and "pred (knd a) s"
    with CFG_wf show "state_val (transfer (knd a) s) V = state_val s V"
      by(rule CFG_wf.CFG_edge_no_Def_equal)
  next
    fix a s s'
    assume assms:"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      "∀V∈lift_Use Use Entry Exit H L (src a). state_val s V = state_val s' V"
      "pred (knd a) s" "pred (knd a) s'"
    with CFG_wf show "∀V∈lift_Def Def Entry Exit H L (src a).
             state_val (transfer (knd a) s) V = state_val (transfer (knd a) s') V"
      by(rule CFG_wf.CFG_edge_transfer_uses_only_Use)
  next
    fix a s s'
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "pred (knd a) s" 
      and "∀V∈lift_Use Use Entry Exit H L (src a). state_val s V = state_val s' V"
    with CFG_wf show "pred (knd a) s'" by(rule CFG_wf.CFG_edge_Uses_pred_equal)
  next
    fix a a'
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'"
      and "src a = src a'" and "trg a ≠ trg a'"
    with CFG_wf show "∃Q Q'. knd a = (Q)⇩√ ∧ knd a' = (Q')⇩√ ∧ 
                             (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))"
      by(rule CFG_wf.deterministic)
  next
    fix a assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "src a = NewExit"
    with CFGExit show False by(rule CFGExit.Exit_source)
  next
    from CFGExit
    show "∃a. lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a ∧
              src a = NewEntry ∧ trg a = NewExit ∧ knd a = (λs. False)⇩√"
      by(rule CFGExit.Entry_Exit_edge)
  next
    from CFGExit_wf
    show "lift_Def Def Entry Exit H L NewExit = {} ∧
          lift_Use Use Entry Exit H L NewExit = {}"
      by(rule CFGExit_wf.Exit_empty)
  next
    fix n n'
    assume wcd:"StrongPostdomination.weak_control_dependence src trg
      (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewExit n n'"
    show "n' ≠ NewExit"
    proof(rule ccontr)
      assume "¬ n' ≠ NewExit"
      hence "n' = NewExit" by simp
      with wcd spd' show False 
        by(fastforce intro:StrongPostdomination.Exit_not_weak_control_dependent)
    qed
  next
    fix n n'
    assume "StrongPostdomination.weak_control_dependence src trg
      (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewExit n n'"
    thus "∃as. CFG.path src trg
               (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
               n as n' ∧ as ≠ []"
      by(fastforce simp:StrongPostdomination.weak_control_dependence_def[OF spd'])
  qed
qed




lemma lift_PDG_weak_backward_slice:
  fixes valid_edge and sourcenode and targetnode and kind and Entry and Exit
  and Def and Use and H and L
  defines lve:"lve ≡ lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit"
  and lDef:"lDef ≡ lift_Def Def Entry Exit H L" 
  and lUse:"lUse ≡ lift_Use Use Entry Exit H L"
  assumes PDG:"PDG sourcenode targetnode kind valid_edge Entry Def Use state_val Exit 
  (StrongPostdomination.weak_control_dependence sourcenode targetnode 
  valid_edge Exit)"
  and spd:"StrongPostdomination sourcenode targetnode kind valid_edge Entry Exit"
  and inner:"CFGExit.inner_node sourcenode targetnode valid_edge Entry Exit nx"
  and "H ∩ L = {}" and "H ∪ L = UNIV"
  shows "NonInterferenceIntraGraph src trg knd lve NewEntry lDef lUse state_val 
         (PDG.PDG_BS src trg lve lDef lUse
           (StrongPostdomination.weak_control_dependence src trg lve NewExit))
         NewExit H L (Node Entry) (Node Exit)"
proof -
  interpret PDG sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
    "StrongPostdomination.weak_control_dependence sourcenode targetnode 
                                                           valid_edge Exit"
    by(rule PDG)
  have wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use
                            state_val Exit" by(unfold_locales)
  interpret wf':CFGExit_wf src trg knd lve NewEntry lDef lUse state_val NewExit
    by(fastforce intro:lift_CFGExit_wf wf simp:lve lDef lUse)
  from PDG spd inner lve lDef lUse have PDG':"PDG src trg knd 
    lve NewEntry lDef lUse state_val NewExit
    (StrongPostdomination.weak_control_dependence src trg lve NewExit)"
    by(fastforce intro:lift_PDG_wcd)
  from wf spd inner have spd':"StrongPostdomination src trg knd
    (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) 
    NewEntry NewExit"
    by(rule lift_StrongPostdomination)
  from wf lve have CFG:"CFG src trg lve NewEntry"
    by(fastforce intro:lift_CFG)
  from wf lve lDef lUse 
  have CFG_wf:"CFG_wf src trg knd lve NewEntry lDef lUse state_val"
    by(fastforce intro:lift_CFG_wf)
  from wf lve have CFGExit:"CFGExit src trg knd lve NewEntry NewExit"
    by(fastforce intro:lift_CFGExit)
  from wf lve lDef lUse 
  have CFGExit_wf:"CFGExit_wf src trg knd lve NewEntry lDef lUse state_val NewExit"
    by(fastforce intro:lift_CFGExit_wf)
  show ?thesis
  proof
    fix n S
    assume "n ∈ PDG.PDG_BS src trg lve lDef lUse
      (StrongPostdomination.weak_control_dependence src trg lve NewExit) S"
    with PDG' show "CFG.valid_node src trg lve n"
      by(rule PDG.PDG_BS_valid_node)
  next
    fix n S assume "CFG.valid_node src trg lve n" and "n ∈ S"
    thus "n ∈ PDG.PDG_BS src trg lve lDef lUse
      (StrongPostdomination.weak_control_dependence src trg lve NewExit) S"
      by(fastforce intro:PDG.PDG_path_Nil[OF PDG'] simp:PDG.PDG_BS_def[OF PDG'])
  next
    fix n' S n V
    assume "n' ∈ PDG.PDG_BS src trg lve lDef lUse
      (StrongPostdomination.weak_control_dependence src trg lve NewExit) S"
      and "CFG_wf.data_dependence src trg lve lDef lUse n V n'"
    thus "n ∈ PDG.PDG_BS src trg lve lDef lUse
      (StrongPostdomination.weak_control_dependence src trg lve NewExit) S"
      by(fastforce intro:PDG.PDG_path_Append[OF PDG'] PDG.PDG_path_ddep[OF PDG']
                        PDG.PDG_ddep_edge[OF PDG'] simp:PDG.PDG_BS_def[OF PDG']
                  split:if_split_asm)
  next
    fix n S
    interpret PDGx:PDG src trg knd lve NewEntry lDef lUse state_val NewExit
      "StrongPostdomination.weak_control_dependence src trg lve NewExit"
      by(rule PDG')
    interpret spdx:StrongPostdomination src trg knd lve NewEntry NewExit
      by(fastforce intro:spd' simp:lve)
    have wcd:"WeakControlDependencePDG src trg knd lve NewEntry
      lDef lUse state_val NewExit" by(unfold_locales)
    from WeakControlDependencePDG.obs_singleton[OF wcd]
    have "(∃m. CFG.obs src trg lve n
      (PDG.PDG_BS src trg lve lDef lUse
       (StrongPostdomination.weak_control_dependence src trg lve NewExit) S) = {m}) ∨
      CFG.obs src trg lve n
      (PDG.PDG_BS src trg lve lDef lUse
        (StrongPostdomination.weak_control_dependence src trg lve NewExit) S) = {}"
      by(fastforce simp:WeakControlDependencePDG.PDG_BS_w_def[OF wcd])
    thus "finite (CFG.obs src trg lve n
        (PDG.PDG_BS src trg lve lDef lUse
          (StrongPostdomination.weak_control_dependence src trg lve NewExit) S))"
      by fastforce
  next
    fix n S
    interpret PDGx:PDG src trg knd lve NewEntry lDef lUse state_val NewExit
      "StrongPostdomination.weak_control_dependence src trg lve NewExit"
      by(rule PDG')
    interpret spdx:StrongPostdomination src trg knd lve NewEntry NewExit
      by(fastforce intro:spd' simp:lve)
    have wcd:"WeakControlDependencePDG src trg knd lve NewEntry
      lDef lUse state_val NewExit" by(unfold_locales)
    from WeakControlDependencePDG.obs_singleton[OF wcd]
    have "(∃m. CFG.obs src trg lve n
      (PDG.PDG_BS src trg lve lDef lUse
       (StrongPostdomination.weak_control_dependence src trg lve NewExit) S) = {m}) ∨
      CFG.obs src trg lve n
      (PDG.PDG_BS src trg lve lDef lUse
        (StrongPostdomination.weak_control_dependence src trg lve NewExit) S) = {}"
      by(fastforce simp:WeakControlDependencePDG.PDG_BS_w_def[OF wcd])
    thus "card (CFG.obs src trg lve n
      (PDG.PDG_BS src trg lve lDef lUse
        (StrongPostdomination.weak_control_dependence src trg lve NewExit) S)) ≤ 1"
      by fastforce
  next
    fix a assume "lve a" and "src a = NewEntry"
    with lve show "trg a = NewExit ∨ trg a = Node Entry"
      by(fastforce elim:lift_valid_edge.cases)
  next
    from lve_Entry_edge lve
    show "∃a. lve a ∧ src a = NewEntry ∧ trg a = Node Entry ∧ knd a = (λs. True)⇩√"
      by(fastforce simp:knd_def)
  next
    fix a assume "lve a" and "trg a = Node Entry"
    with lve show "src a = NewEntry" by(fastforce elim:lift_valid_edge.cases)
  next
    fix a assume "lve a" and "trg a = NewExit"
    with lve show "src a = NewEntry ∨ src a = Node Exit"
      by(fastforce elim:lift_valid_edge.cases)
  next
    from lve_Exit_edge lve
    show "∃a. lve a ∧ src a = Node Exit ∧ trg a = NewExit ∧ knd a = (λs. True)⇩√"
      by(fastforce simp:knd_def)
  next
    fix a assume "lve a" and "src a = Node Exit"
    with lve show "trg a = NewExit" by(fastforce elim:lift_valid_edge.cases)
  next
    from lDef show "lDef (Node Entry) = H"
      by(fastforce elim:lift_Def_set.cases intro:lift_Def_High)
  next
    from Entry_noteq_Exit lUse show "lUse (Node Entry) = H"
      by(fastforce elim:lift_Use_set.cases intro:lift_Use_High)
  next
    from Entry_noteq_Exit lUse show "lUse (Node Exit) = L"
      by(fastforce elim:lift_Use_set.cases intro:lift_Use_Low)
  next
    from ‹H ∩ L = {}› show "H ∩ L = {}" .
  next
    from ‹H ∪ L = UNIV› show "H ∪ L = UNIV" .
  qed
qed


end