Theory LiftingInter

section ‹Framework Graph Lifting for Noninterference›

theory LiftingInter 
imports NonInterferenceInter 
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,'var,'val,'ret,'pname) LDCFG_edge = 
  "'node LDCFG_node × (('var,'val,'ret,'pname) edge_kind) × 'node LDCFG_node"


subsubsection ‹Lifting basic definitions using @{typ 'edge} and @{typ 'node}

inductive lift_valid_edge :: "('edge  bool)  ('edge  'node)  ('edge  'node) 
  ('edge  ('var,'val,'ret,'pname) edge_kind)  'node  'node  
  ('edge,'node,'var,'val,'ret,'pname) LDCFG_edge  
  bool"
for valid_edge::"'edge  bool" and src::"'edge  'node" and trg::"'edge  'node" 
  and knd::"'edge  ('var,'val,'ret,'pname) 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)



fun lift_get_proc :: "('node  'pname)  'pname  'node LDCFG_node  'pname"
  where "lift_get_proc get_proc Main (Node n) = get_proc n"
  | "lift_get_proc get_proc Main NewEntry = Main"
  | "lift_get_proc get_proc Main NewExit = Main"


inductive_set lift_get_return_edges :: "('edge  'edge set)  ('edge  bool)  
  ('edge  'node)  ('edge  'node)  ('edge  ('var,'val,'ret,'pname) edge_kind) 
   ('edge,'node,'var,'val,'ret,'pname) LDCFG_edge 
   ('edge,'node,'var,'val,'ret,'pname) LDCFG_edge set"
for get_return_edges :: "'edge  'edge set" and valid_edge :: "'edge  bool"
  and src::"'edge  'node" and trg::"'edge  'node" 
  and knd::"'edge  ('var,'val,'ret,'pname) edge_kind" 
  and e::"('edge,'node,'var,'val,'ret,'pname) LDCFG_edge"
where lift_get_return_edgesI:
  "e = (Node (src a),knd a,Node (trg a)); valid_edge a; a'  get_return_edges a; 
  e' = (Node (src a'),knd a',Node (trg a'))
   e'  lift_get_return_edges get_return_edges valid_edge src trg knd e"


subsubsection ‹Lifting the Def and 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}"


fun lift_ParamUses :: "('node  'var set list)  'node LDCFG_node  'var set list"
  where "lift_ParamUses ParamUses (Node n) =  ParamUses n"
  | "lift_ParamUses ParamUses NewEntry = []"
  | "lift_ParamUses ParamUses NewExit = []"


fun lift_ParamDefs :: "('node  'var list)  'node LDCFG_node  'var list"
  where "lift_ParamDefs ParamDefs (Node n) =  ParamDefs n"
  | "lift_ParamDefs ParamDefs NewEntry = []"
  | "lift_ParamDefs ParamDefs NewExit = []"



subsection ‹The lifting lemmas›


subsubsection ‹Lifting the CFG locales›

abbreviation src :: "('edge,'node,'var,'val,'ret,'pname) LDCFG_edge  'node LDCFG_node"
  where "src a  fst a"

abbreviation trg :: "('edge,'node,'var,'val,'ret,'pname) LDCFG_edge  'node LDCFG_node"
  where "trg a  snd(snd a)"

abbreviation knd :: "('edge,'node,'var,'val,'ret,'pname) LDCFG_edge  
  ('var,'val,'ret,'pname) edge_kind"
  where "knd a  fst(snd a)"


lemma lift_CFG:
  assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry get_proc 
  get_return_edges procs Main Exit Def Use ParamDefs ParamUses"
  and pd:"Postdomination sourcenode targetnode kind valid_edge Entry get_proc 
  get_return_edges procs Main Exit"
  shows "CFG src trg knd
  (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
  (lift_get_proc get_proc Main) 
  (lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind) 
  procs Main"
proof -
  interpret CFGExit_wf sourcenode targetnode kind valid_edge Entry get_proc 
    get_return_edges procs Main Exit Def Use ParamDefs ParamUses
    by(rule wf)
  interpret Postdomination sourcenode targetnode kind valid_edge Entry get_proc 
    get_return_edges procs Main Exit
    by(rule pd)
  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
    show "lift_get_proc get_proc Main NewEntry = Main" by simp
  next
    fix a Q r p fs
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q:r↪⇘pfs" and "src 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)
  next
    fix a Q r f
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q:r↪⇘Mainf"
    thus False by(fastforce elim:lift_valid_edge.cases dest:Main_no_call_target)
  next
    fix a Q' f'
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q'↩⇘Mainf'"
    thus False by(fastforce elim:lift_valid_edge.cases dest:Main_no_return_source)
  next
    fix a Q r p fs
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q:r↪⇘pfs"
    thus "ins outs. (p, ins, outs)  set procs"
      by(fastforce elim:lift_valid_edge.cases intro:callee_in_procs)
  next
    fix a assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "intra_kind (knd a)"
    thus "lift_get_proc get_proc Main (src a) = lift_get_proc get_proc Main (trg a)"
      by(fastforce elim:lift_valid_edge.cases intro:get_proc_intra 
                  simp:get_proc_Entry get_proc_Exit)
  next
    fix a Q r p fs 
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q:r↪⇘pfs"
    thus "lift_get_proc get_proc Main (trg a) = p"
      by(fastforce elim:lift_valid_edge.cases intro:get_proc_call)
  next
    fix a Q' p f'
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q'↩⇘pf'"
    thus "lift_get_proc get_proc Main (src a) = p"
      by(fastforce elim:lift_valid_edge.cases intro:get_proc_return)
  next
    fix a Q r p fs
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q:r↪⇘pfs"
    then obtain ax where "valid_edge ax" and "kind ax = Q:r↪⇘pfs"
      and "sourcenode ax  Entry  targetnode ax  Exit"
      and "src a = Node (sourcenode ax)" and "trg a = Node (targetnode ax)"
      by(fastforce elim:lift_valid_edge.cases)
    from valid_edge ax kind ax = Q:r↪⇘pfs
    have all:"a'. valid_edge a'  targetnode a' = targetnode ax  
               (Qx rx fsx. kind a' = Qx:rx↪⇘pfsx)"
      by(auto dest:call_edges_only)
    { fix a' 
      assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'"
        and "trg a' = trg a"
      hence "Qx rx fsx. knd a' = Qx:rx↪⇘pfsx"
      proof(induct rule:lift_valid_edge.induct)
        case (lve_edge ax' e)
        note [simp] = e = (Node (sourcenode ax'), kind ax', Node (targetnode ax'))
        from trg e = trg a trg a = Node (targetnode ax)
        have "targetnode ax' = targetnode ax" by simp
        with valid_edge ax' all have "Qx rx fsx. kind ax' = Qx:rx↪⇘pfsx" by blast
        thus ?case by simp
      next
        case (lve_Entry_edge e)
        from e = (NewEntry, (λs. True), Node Entry) trg e = trg a
          trg a = Node (targetnode ax)
        have "targetnode ax = Entry" by simp
        with valid_edge ax have False by(rule Entry_target)
        thus ?case by simp
      next
        case (lve_Exit_edge e)
        from e = (Node Exit, (λs. True), NewExit) trg e = trg a
          trg a = Node (targetnode ax) have False by simp
        thus ?case by simp
      next
        case (lve_Entry_Exit_edge e)
        from e = (NewEntry,(λs. False),NewExit) trg e = trg a
          trg a = Node (targetnode ax) have False by simp
        thus ?case by simp
      qed }
    thus "a'. lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a' 
               trg a' = trg a  (Qx rx fsx. knd a' = Qx:rx↪⇘pfsx)" by simp
  next
    fix a Q' p f'
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q'↩⇘pf'"
    then obtain ax where "valid_edge ax" and "kind ax = Q'↩⇘pf'"
      and "sourcenode ax  Entry  targetnode ax  Exit"
      and "src a = Node (sourcenode ax)" and "trg a = Node (targetnode ax)"
      by(fastforce elim:lift_valid_edge.cases)
    from valid_edge ax kind ax = Q'↩⇘pf'
    have all:"a'. valid_edge a'  sourcenode a' = sourcenode ax  
            (Qx fx. kind a' = Qx↩⇘pfx)"
      by(auto dest:return_edges_only)
    { fix a' 
      assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'"
        and "src a' = src a"
      hence "Qx fx. knd a' = Qx↩⇘pfx"
      proof(induct rule:lift_valid_edge.induct)
        case (lve_edge ax' e)
        note [simp] = e = (Node (sourcenode ax'), kind ax', Node (targetnode ax'))
        from src e = src a src a = Node (sourcenode ax)
        have "sourcenode ax' = sourcenode ax" by simp
        with valid_edge ax' all have "Qx fx. kind ax' = Qx↩⇘pfx" by blast
        thus ?case by simp
      next
        case (lve_Entry_edge e)
        from e = (NewEntry, (λs. True), Node Entry) src e = src a
          src a = Node (sourcenode ax) have False by simp
        thus ?case by simp
      next
        case (lve_Exit_edge e)
        from e = (Node Exit, (λs. True), NewExit) src e = src a
          src a = Node (sourcenode ax) have "sourcenode ax = Exit" by simp
        with valid_edge ax have False by(rule Exit_source)
        thus ?case by simp
      next
        case (lve_Entry_Exit_edge e)
        from e = (NewEntry,(λs. False),NewExit) src e = src a
          src a = Node (sourcenode ax) have False by simp
        thus ?case by simp
      qed }
    thus "a'. lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a' 
               src a' = src a  (Qx fx. knd a' = Qx↩⇘pfx)" by simp
  next
    fix a Q r p fs
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q:r↪⇘pfs"
    thus "lift_get_return_edges get_return_edges valid_edge 
      sourcenode targetnode kind a  {}"
    proof(induct rule:lift_valid_edge.induct)
      case (lve_edge ax e)
      from e = (Node (sourcenode ax), kind ax, Node (targetnode ax)) 
        knd e = Q:r↪⇘pfs
      have "kind ax = Q:r↪⇘pfs" by simp
      with valid_edge ax have "get_return_edges ax  {}"
        by(rule get_return_edge_call)
      then obtain ax' where "ax'  get_return_edges ax" by blast
      with e = (Node (sourcenode ax), kind ax, Node (targetnode ax)) valid_edge ax
      have "(Node (sourcenode ax'),kind ax',Node (targetnode ax'))  
        lift_get_return_edges get_return_edges valid_edge 
        sourcenode targetnode kind e"
        by(fastforce intro:lift_get_return_edgesI)
      thus ?case by fastforce
    qed simp_all
  next
    fix a a'
    assume "a'  lift_get_return_edges get_return_edges valid_edge 
      sourcenode targetnode kind a"
      and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
    thus "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'"
    proof (induct rule:lift_get_return_edges.induct)
      case (lift_get_return_edgesI ax a' e')
      from valid_edge ax a'  get_return_edges ax have "valid_edge a'" 
        by(rule get_return_edges_valid)
      from valid_edge ax a'  get_return_edges ax obtain Q r p fs 
        where "kind ax = Q:r↪⇘pfs" by(fastforce dest!:only_call_get_return_edges)
      with valid_edge ax a'  get_return_edges ax obtain Q' f' 
        where "kind a' = Q'↩⇘pf'" by(fastforce dest!:call_return_edges)
      from valid_edge a' kind a' = Q'↩⇘pf' have "get_proc(sourcenode a') = p"
        by(rule get_proc_return)
      have "sourcenode a'  Entry"
      proof
        assume "sourcenode a' = Entry"
        with get_proc_Entry get_proc(sourcenode a') = p have "p = Main" by simp
        with kind a' = Q'↩⇘pf' have "kind a' = Q'↩⇘Mainf'" by simp
        with valid_edge a' show False by(rule Main_no_return_source)
      qed
      with e' = (Node (sourcenode a'), kind a', Node (targetnode a')) 
        valid_edge a'
      show ?case by(fastforce intro:lve_edge)
    qed
  next
    fix a a'
    assume "a'  lift_get_return_edges get_return_edges valid_edge sourcenode
      targetnode kind a"
      and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
    thus "Q r p fs. knd a = Q:r↪⇘pfs"
    proof (induct rule:lift_get_return_edges.induct)
      case (lift_get_return_edgesI ax a' e') 
      from valid_edge ax a'  get_return_edges ax 
      have "Q r p fs. kind ax = Q:r↪⇘pfs"
        by(rule only_call_get_return_edges)
      with a = (Node (sourcenode ax), kind ax, Node (targetnode ax))
      show ?case by simp
    qed
  next
    fix a Q r p fs a'
    assume "a'  lift_get_return_edges get_return_edges 
      valid_edge sourcenode targetnode kind a" and "knd a = Q:r↪⇘pfs"
      and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
    thus "Q' f'. knd a' = Q'↩⇘pf'"
    proof (induct rule:lift_get_return_edges.induct)
      case (lift_get_return_edgesI ax a' e')
      from a = (Node (sourcenode ax), kind ax, Node (targetnode ax))
        knd a = Q:r↪⇘pfs
      have "kind ax = Q:r↪⇘pfs" by simp
      with valid_edge ax a'  get_return_edges ax have "Q' f'. kind a' = Q'↩⇘pf'"
        by -(rule call_return_edges)
      with e' = (Node (sourcenode a'), kind a', Node (targetnode a'))
      show ?case by simp
    qed
  next
    fix a Q' p f'
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q'↩⇘pf'"
    thus "∃!a'. lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a' 
      (Q r fs. knd a' = Q:r↪⇘pfs)  a  lift_get_return_edges get_return_edges 
      valid_edge sourcenode targetnode kind a'"
    proof(induct rule:lift_valid_edge.induct)
      case (lve_edge a e)
      from e = (Node (sourcenode a), kind a, Node (targetnode a))
        knd e = Q'↩⇘pf' have "kind a = Q'↩⇘pf'" by simp
      with valid_edge a
      have "∃!a'. valid_edge a'  (Q r fs. kind a' = Q:r↪⇘pfs)  
        a  get_return_edges a'"
        by(rule return_needs_call)
      then obtain a' Q r fs where "valid_edge a'" and "kind a' = Q:r↪⇘pfs"
        and "a  get_return_edges a'"
        and imp:"x. valid_edge x  (Q r fs. kind x = Q:r↪⇘pfs)  
        a  get_return_edges x  x = a'"
        by(fastforce elim:ex1E)
      let ?e' = "(Node (sourcenode a'),kind a',Node (targetnode a'))"
      have "sourcenode a'  Entry"
      proof
        assume "sourcenode a' = Entry"
        with valid_edge a' kind a' = Q:r↪⇘pfs
        show False by(rule Entry_no_call_source)
      qed
      with valid_edge a'
      have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit ?e'"
        by(fastforce intro:lift_valid_edge.lve_edge)
      moreover
      from kind a' = Q:r↪⇘pfs have "knd ?e' = Q:r↪⇘pfs" by simp
      moreover
      from e = (Node (sourcenode a), kind a, Node (targetnode a)) 
        valid_edge a' a  get_return_edges a'
      have "e  lift_get_return_edges get_return_edges valid_edge
        sourcenode targetnode kind ?e'" by(fastforce intro:lift_get_return_edgesI)
      moreover
      { fix x
        assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit x"
          and "Q r fs. knd x = Q:r↪⇘pfs" 
          and "e  lift_get_return_edges get_return_edges valid_edge
          sourcenode targetnode kind x"
        from lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit x
          Q r fs. knd x = Q:r↪⇘pfs obtain y where "valid_edge y" 
          and "x = (Node (sourcenode y), kind y, Node (targetnode y))"
          by(fastforce elim:lift_valid_edge.cases)
        with e  lift_get_return_edges get_return_edges valid_edge
          sourcenode targetnode kind x valid_edge a
          e = (Node (sourcenode a), kind a, Node (targetnode a))
        have "x = ?e'"
        proof(induct rule:lift_get_return_edges.induct)
          case (lift_get_return_edgesI ax ax' e)
          from valid_edge ax ax'  get_return_edges ax have "valid_edge ax'"
            by(rule get_return_edges_valid)
          from e = (Node (sourcenode ax'), kind ax', Node (targetnode ax'))
            e = (Node (sourcenode a), kind a, Node (targetnode a))
          have "sourcenode a = sourcenode ax'" and "targetnode a = targetnode ax'"
            by simp_all
          with valid_edge a valid_edge ax' have [simp]:"a = ax'" by(rule edge_det)
          from x = (Node (sourcenode ax), kind ax, Node (targetnode ax))
            Q r fs. knd x = Q:r↪⇘pfs have "Q r fs. kind ax = Q:r↪⇘pfs" by simp
          with valid_edge ax ax'  get_return_edges ax imp
          have "ax = a'" by fastforce
          with x = (Node (sourcenode ax), kind ax, Node (targetnode ax)) 
          show ?thesis by simp
        qed }
      ultimately show ?case by(blast intro:ex1I)
    qed simp_all
  next
    fix a a'
    assume "a'  lift_get_return_edges get_return_edges valid_edge sourcenode
      targetnode kind a" 
      and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
    thus "a''. lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'' 
      src a'' = trg a  trg a'' = src a'  knd a'' = (λcf. False)"
    proof(induct rule:lift_get_return_edges.induct)
      case (lift_get_return_edgesI ax a' e')
      from valid_edge ax a'  get_return_edges ax
      obtain ax' where "valid_edge ax'" and "sourcenode ax' = targetnode ax"
        and "targetnode ax' = sourcenode a'" and "kind ax' = (λcf. False)"
        by(fastforce dest:intra_proc_additional_edge)
      let ?ex = "(Node (sourcenode ax'), kind ax', Node (targetnode ax'))"
      have "targetnode ax  Entry"
      proof
        assume "targetnode ax = Entry"
        with valid_edge ax show False by(rule Entry_target)
      qed
      with sourcenode ax' = targetnode ax have "sourcenode ax'  Entry" by simp
      with valid_edge ax' 
      have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit ?ex"
        by(fastforce intro:lve_edge)
      with e' = (Node (sourcenode a'), kind a', Node (targetnode a'))
        a = (Node (sourcenode ax), kind ax, Node (targetnode ax))
        e' = (Node (sourcenode a'), kind a', Node (targetnode a'))
        sourcenode ax' = targetnode ax targetnode ax' = sourcenode a'
        kind ax' = (λcf. False)
      show ?case by simp
    qed
  next
    fix a a'
    assume "a'  lift_get_return_edges get_return_edges valid_edge sourcenode
      targetnode kind a" 
      and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
    thus "a''. lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'' 
      src a'' = src a  trg a'' = trg a'  knd a'' = (λcf. False)"
    proof(induct rule:lift_get_return_edges.induct)
      case (lift_get_return_edgesI ax a' e')
      from valid_edge ax a'  get_return_edges ax
      obtain ax' where "valid_edge ax'" and "sourcenode ax' = sourcenode ax"
        and "targetnode ax' = targetnode a'" and "kind ax' = (λcf. False)"
        by(fastforce dest:call_return_node_edge)
      let ?ex = "(Node (sourcenode ax'), kind ax', Node (targetnode ax'))"
      from valid_edge ax a'  get_return_edges ax
      obtain Q r p fs where "kind ax = Q:r↪⇘pfs" 
        by(fastforce dest!:only_call_get_return_edges)
      have "sourcenode ax  Entry"
      proof
        assume "sourcenode ax = Entry"
        with valid_edge ax kind ax = Q:r↪⇘pfs show False
          by(rule Entry_no_call_source)
      qed
      with sourcenode ax' = sourcenode ax have "sourcenode ax'  Entry" by simp
      with valid_edge ax' 
      have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit ?ex"
        by(fastforce intro:lve_edge)
      with e' = (Node (sourcenode a'), kind a', Node (targetnode a'))
        a = (Node (sourcenode ax), kind ax, Node (targetnode ax))
        e' = (Node (sourcenode a'), kind a', Node (targetnode a'))
        sourcenode ax' = sourcenode ax targetnode ax' = targetnode a'
        kind ax' = (λcf. False)
      show ?case by simp
    qed
  next
    fix a Q r p fs
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q:r↪⇘pfs"
    thus "∃!a'. lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a' 
      src a' = src a  intra_kind (knd a')"
    proof(induct rule:lift_valid_edge.induct)
      case (lve_edge a e)
      from e = (Node (sourcenode a), kind a, Node (targetnode a)) knd e = Q:r↪⇘pfs
      have "kind a = Q:r↪⇘pfs" by simp
      with valid_edge a have "∃!a'. valid_edge a'  sourcenode a' = sourcenode a 
        intra_kind(kind a')" by(rule call_only_one_intra_edge)
      then obtain a' where "valid_edge a'" and "sourcenode a' = sourcenode a"
        and "intra_kind(kind a')" 
        and imp:"x. valid_edge x  sourcenode x = sourcenode a  intra_kind(kind x)
         x = a'" by(fastforce elim:ex1E)
      let ?e' = "(Node (sourcenode a'), kind a', Node (targetnode a'))"
      have "sourcenode a  Entry"
      proof
        assume "sourcenode a = Entry"
        with valid_edge a kind a = Q:r↪⇘pfs show False
          by(rule Entry_no_call_source)
      qed
      with sourcenode a' = sourcenode a have "sourcenode a'  Entry" by simp
      with valid_edge a' 
      have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit ?e'"
        by(fastforce intro:lift_valid_edge.lve_edge)
      moreover
      from e = (Node (sourcenode a), kind a, Node (targetnode a))
        sourcenode a' = sourcenode a
      have "src ?e' = src e" by simp
      moreover
      from intra_kind(kind a') have "intra_kind (knd ?e')" by simp
      moreover
      { fix x 
        assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit x"
          and "src x = src e" and "intra_kind (knd x)"
        from lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit x
        have "x = ?e'"
        proof(induct rule:lift_valid_edge.cases)
          case (lve_edge ax ex)
          from intra_kind (knd x) x = ex src x = src e
            ex = (Node (sourcenode ax), kind ax, Node (targetnode ax))
            e = (Node (sourcenode a), kind a, Node (targetnode a))
          have "intra_kind (kind ax)" and "sourcenode ax = sourcenode a" by simp_all
          with valid_edge ax imp have "ax = a'" by fastforce
          with x = ex ex = (Node (sourcenode ax), kind ax, Node (targetnode ax))
          show ?case by simp
        next
          case (lve_Entry_edge ex)
          with src x = src e 
            e = (Node (sourcenode a), kind a, Node (targetnode a))
          have False by simp
          thus ?case by simp
        next
          case (lve_Exit_edge ex)
          with src x = src e 
            e = (Node (sourcenode a), kind a, Node (targetnode a))
          have "sourcenode a = Exit" by simp
          with valid_edge a have False by(rule Exit_source)
          thus ?case by simp
        next
          case (lve_Entry_Exit_edge ex)
          with src x = src e 
            e = (Node (sourcenode a), kind a, Node (targetnode a))
          have False by simp
          thus ?case by simp
        qed }
      ultimately show ?case by(blast intro:ex1I)
    qed simp_all
  next
    fix a Q' p f'
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q'↩⇘pf'"
    thus "∃!a'. lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a' 
      trg a' = trg a  intra_kind (knd a')"
    proof(induct rule:lift_valid_edge.induct)
      case (lve_edge a e)
      from e = (Node (sourcenode a), kind a, Node (targetnode a)) knd e = Q'↩⇘pf'
      have "kind a = Q'↩⇘pf'" by simp
      with valid_edge a have "∃!a'. valid_edge a'  targetnode a' = targetnode a 
        intra_kind(kind a')" by(rule return_only_one_intra_edge)
      then obtain a' where "valid_edge a'" and "targetnode a' = targetnode a"
        and "intra_kind(kind a')" 
        and imp:"x. valid_edge x  targetnode x = targetnode a  intra_kind(kind x)
         x = a'" by(fastforce elim:ex1E)
      let ?e' = "(Node (sourcenode a'), kind a', Node (targetnode a'))"
      have "targetnode a  Exit"
      proof
        assume "targetnode a = Exit"
        with valid_edge a kind a = Q'↩⇘pf' show False
          by(rule Exit_no_return_target)
      qed
      with targetnode a' = targetnode a have "targetnode a'  Exit" by simp
      with valid_edge a' 
      have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit ?e'"
        by(fastforce intro:lift_valid_edge.lve_edge)
      moreover
      from e = (Node (sourcenode a), kind a, Node (targetnode a))
        targetnode a' = targetnode a
      have "trg ?e' = trg e" by simp
      moreover
      from intra_kind(kind a') have "intra_kind (knd ?e')" by simp
      moreover
      { fix x 
        assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit x"
          and "trg x = trg e" and "intra_kind (knd x)"
        from lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit x
        have "x = ?e'"
        proof(induct rule:lift_valid_edge.cases)
          case (lve_edge ax ex)
          from intra_kind (knd x) x = ex trg x = trg e
            ex = (Node (sourcenode ax), kind ax, Node (targetnode ax))
            e = (Node (sourcenode a), kind a, Node (targetnode a))
          have "intra_kind (kind ax)" and "targetnode ax = targetnode a" by simp_all
          with valid_edge ax imp have "ax = a'" by fastforce
          with x = ex ex = (Node (sourcenode ax), kind ax, Node (targetnode ax))
          show ?case by simp
        next
          case (lve_Entry_edge ex)
          with trg x = trg e 
            e = (Node (sourcenode a), kind a, Node (targetnode a))
          have "targetnode a = Entry" by simp
          with valid_edge a have False by(rule Entry_target)
          thus ?case by simp
        next
          case (lve_Exit_edge ex)
          with trg x = trg e 
            e = (Node (sourcenode a), kind a, Node (targetnode a))
          have False by simp
          thus ?case by simp
        next
          case (lve_Entry_Exit_edge ex)
          with trg x = trg e 
            e = (Node (sourcenode a), kind a, Node (targetnode a))
          have False by simp
          thus ?case by simp
        qed }
      ultimately show ?case by(blast intro:ex1I)
    qed simp_all
  next
    fix a a' Q1 r1 p fs1 Q2 r2 fs2
    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 "knd a = Q1:r1↪⇘pfs1" and "knd a' = Q2:r2↪⇘pfs2"
    then obtain x x' where "valid_edge x" 
      and a:"a = (Node (sourcenode x),kind x,Node (targetnode x))" and "valid_edge x'"
      and a':"a' = (Node (sourcenode x'),kind x',Node (targetnode x'))"
      by(auto elim!:lift_valid_edge.cases)
    with knd a = Q1:r1↪⇘pfs1 knd a' = Q2:r2↪⇘pfs2
    have "kind x = Q1:r1↪⇘pfs1" and "kind x' = Q2:r2↪⇘pfs2" by simp_all
    with valid_edge x valid_edge x' have "targetnode x = targetnode x'"
      by(rule same_proc_call_unique_target)
    with a a' show "trg a = trg a'" by simp
  next
    from unique_callers show "distinct_fst procs" .
  next
    fix p ins outs
    assume "(p, ins, outs)  set procs"
    from distinct_formal_ins[OF this] show "distinct ins" .
  next
    fix p ins outs
    assume "(p, ins, outs)  set procs"
    from distinct_formal_outs[OF this] show "distinct outs" .
  qed
qed


lemma lift_CFG_wf:
  assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry get_proc 
  get_return_edges procs Main Exit Def Use ParamDefs ParamUses"
  and pd:"Postdomination sourcenode targetnode kind valid_edge Entry get_proc 
  get_return_edges procs Main Exit"
  shows "CFG_wf src trg knd
  (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
  (lift_get_proc get_proc Main) 
  (lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind) 
  procs Main (lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L)
  (lift_ParamDefs ParamDefs) (lift_ParamUses ParamUses)"
proof -
  interpret CFGExit_wf sourcenode targetnode kind valid_edge Entry get_proc 
    get_return_edges procs Main Exit Def Use ParamDefs ParamUses
    by(rule wf)
  interpret Postdomination sourcenode targetnode kind valid_edge Entry get_proc 
    get_return_edges procs Main Exit
    by(rule pd)
  interpret CFG:CFG src trg knd
    "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit" NewEntry
    "lift_get_proc get_proc Main" 
    "lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind"
    procs Main
    by(fastforce intro:lift_CFG wf pd)
  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 Q r p fs ins outs
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q:r↪⇘pfs" and "(p, ins, outs)  set procs"
    thus "length (lift_ParamUses ParamUses (src a)) = length ins"
    proof(induct rule:lift_valid_edge.induct)
      case (lve_edge a e)
      from e = (Node (sourcenode a), kind a, Node (targetnode a)) knd e = Q:r↪⇘pfs
      have "kind a = Q:r↪⇘pfs" and "src e = Node (sourcenode a)" by simp_all
      with valid_edge a (p,ins,outs)  set procs
      have "length(ParamUses (sourcenode a)) = length ins"
        by -(rule ParamUses_call_source_length)
      with src e = Node (sourcenode a) show ?case by simp
    qed simp_all
  next
    fix a assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
    thus "distinct (lift_ParamDefs ParamDefs (trg a))"
    proof(induct rule:lift_valid_edge.induct)
      case (lve_edge a e)
      from valid_edge a have "distinct (ParamDefs (targetnode a))"
        by(rule distinct_ParamDefs)
      with e = (Node (sourcenode a), kind a, Node (targetnode a))
      show ?case by simp
    next
      case (lve_Entry_edge e)
      have "ParamDefs Entry = []"
      proof(rule ccontr)
        assume "ParamDefs Entry  []"
        then obtain V Vs where "ParamDefs Entry = V#Vs" 
          by(cases "ParamDefs Entry") auto
        hence "V  set (ParamDefs Entry)" by fastforce
        hence "V  Def Entry" by(fastforce intro:ParamDefs_in_Def)
        with Entry_empty show False by simp
      qed
      with e = (NewEntry, (λs. True), Node Entry) show ?case by simp
    qed simp_all
  next
    fix a Q' p f' ins outs
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q'↩⇘pf'" and "(p, ins, outs)  set procs"
    thus "length (lift_ParamDefs ParamDefs (trg a)) = length outs"
    proof(induct rule:lift_valid_edge.induct)
      case (lve_edge a e)
      from e = (Node (sourcenode a), kind a, Node (targetnode a))
        knd e = Q'↩⇘pf'
      have "kind a = Q'↩⇘pf'" and "trg e = Node (targetnode a)" by simp_all
      with valid_edge a (p,ins,outs)  set procs
      have "length(ParamDefs (targetnode a)) = length outs"
        by -(rule ParamDefs_return_target_length)
      with trg e = Node (targetnode a) show ?case by simp
    qed simp_all
  next
    fix n V
    assume "CFG.CFG.valid_node src trg 
      (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) n"
      and "V  set (lift_ParamDefs ParamDefs n)"
    hence "((n = NewEntry)  n = NewExit)  (m. n = Node m  valid_node m)"
      by(auto elim:lift_valid_edge.cases simp:CFG.valid_node_def)
    thus "V  lift_Def Def Entry Exit H L n" apply -
    proof(erule disjE)+
      assume "n = NewEntry"
      with V  set (lift_ParamDefs ParamDefs n) show ?thesis by simp
    next
       assume "n = NewExit"
      with V  set (lift_ParamDefs ParamDefs n) show ?thesis by simp
    next
      assume "m. n = Node m  valid_node m"
      then obtain m where "n = Node m" and "valid_node m" by blast
      from n = Node m V  set (lift_ParamDefs ParamDefs n)
      have "V  set (ParamDefs m)" by simp
      with valid_node m have "V  Def m" by(rule ParamDefs_in_Def)
      with n = Node m show ?thesis by(fastforce intro:lift_Def_node)
    qed
  next
    fix a Q r p fs ins outs V
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q:r↪⇘pfs" and "(p, ins, outs)  set procs" and "V  set ins"
    thus "V  lift_Def Def Entry Exit H L (trg a)"
    proof(induct rule:lift_valid_edge.induct)
      case (lve_edge a e)
      from e = (Node (sourcenode a), kind a, Node (targetnode a)) knd e = Q:r↪⇘pfs
      have "kind a = Q:r↪⇘pfs" by simp
      from valid_edge a kind a = Q:r↪⇘pfs (p, ins, outs)  set procs V  set ins
      have "V  Def (targetnode a)" by(rule ins_in_Def)
      from e = (Node (sourcenode a), kind a, Node (targetnode a))
      have "trg e = Node (targetnode a)" by simp
      with V  Def (targetnode a) show ?case by(fastforce intro:lift_Def_node)
    qed simp_all
  next
    fix a Q r p fs
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q:r↪⇘pfs"
    thus "lift_Def Def Entry Exit H L (src a) = {}"
    proof(induct rule:lift_valid_edge.induct)
      case (lve_edge a e)
      show ?case
      proof(rule ccontr)
        assume "lift_Def Def Entry Exit H L (src e)  {}"
        then obtain x where "x  lift_Def Def Entry Exit H L (src e)" by blast
        from e = (Node (sourcenode a), kind a, Node (targetnode a)) knd e = Q:r↪⇘pfs
        have "kind a = Q:r↪⇘pfs" by simp
        with valid_edge a have "Def (sourcenode a) = {}" 
          by(rule call_source_Def_empty)
        have "sourcenode a  Entry"
        proof
          assume "sourcenode a = Entry"
          with valid_edge a kind a = Q:r↪⇘pfs
          show False by(rule Entry_no_call_source)
        qed
        from e = (Node (sourcenode a), kind a, Node (targetnode a))
        have "src e = Node (sourcenode a)" by simp
        with Def (sourcenode a) = {} x  lift_Def Def Entry Exit H L (src e)
          sourcenode a  Entry
        show False by(fastforce elim:lift_Def_set.cases)
      qed 
    qed simp_all
  next
    fix n V
    assume "CFG.CFG.valid_node src trg 
      (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) n"
      and "V  (set (lift_ParamUses ParamUses n))"
    hence "((n = NewEntry)  n = NewExit)  (m. n = Node m  valid_node m)"
      by(auto elim:lift_valid_edge.cases simp:CFG.valid_node_def)
    thus "V  lift_Use Use Entry Exit H L n" apply -
    proof(erule disjE)+
      assume "n = NewEntry"
      with V  (set (lift_ParamUses ParamUses n)) show ?thesis by simp
    next
      assume "n = NewExit"
      with V  (set (lift_ParamUses ParamUses n)) show ?thesis by simp
    next
      assume "m. n = Node m  valid_node m"
      then obtain m where "n = Node m" and "valid_node m" by blast
      from V  (set (lift_ParamUses ParamUses n)) n = Node m
      have "V  (set (ParamUses m))" by simp
      with valid_node m have "V  Use m" by(rule ParamUses_in_Use)
      with n = Node m show ?thesis by(fastforce intro:lift_Use_node)
    qed
  next
    fix a Q p f ins outs V
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q↩⇘pf" and "(p, ins, outs)  set procs" and "V  set outs"
    thus "V  lift_Use Use Entry Exit H L (src a)"
    proof(induct rule:lift_valid_edge.induct)
      case (lve_edge a e)
      from e = (Node (sourcenode a), kind a, Node (targetnode a)) knd e = Q↩⇘pf
      have "kind a = Q↩⇘pf" by simp
      from valid_edge a kind a = Q↩⇘pf (p, ins, outs)  set procs V  set outs
      have "V  Use (sourcenode a)" by(rule outs_in_Use)
      from e = (Node (sourcenode a), kind a, Node (targetnode a))
      have "src e = Node (sourcenode a)" by simp
      with V  Use (sourcenode a) show ?case by(fastforce intro:lift_Use_node)
    qed simp_all
  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 "intra_kind (knd 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 a e)
      from e = (Node (sourcenode a), kind a, Node (targetnode a)) 
        intra_kind (knd e) pred (knd e) s
      have "intra_kind (kind a)" and "pred (kind a) s" 
        and "knd e = kind a" and "src e = Node (sourcenode a)" by simp_all
      from V  lift_Def Def Entry Exit H L (src e) src e = Node (sourcenode a)
      have "V  Def (sourcenode a)" by (auto dest: lift_Def_node)
      from valid_edge a V  Def (sourcenode a) intra_kind (kind a) 
        pred (kind a) s
      have "state_val (transfer (kind a) s) V = state_val s V" 
        by(rule CFG_intra_edge_no_Def_equal)
      with knd e = kind a show ?case by simp
    next
      case (lve_Entry_edge e)
      from e = (NewEntry, (λs. True), Node Entry) pred (knd e) s
      show ?case by(cases s) auto
    next
      case (lve_Exit_edge e)
      from e = (Node Exit, (λs. True), NewExit) pred (knd e) s
      show ?case by(cases s) auto
    next
      case (lve_Entry_Exit_edge e)
      from e = (NewEntry, (λs. False), NewExit) pred (knd e) s
      have False by(cases s) auto
      thus ?case by simp
    qed
  next
    fix a s s'
    assume assms:"lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      "Vlift_Use Use Entry Exit H L (src a). state_val s V = state_val s' V"
      "intra_kind (knd a)" "pred (knd a) s" "pred (knd a) s'"
    show "Vlift_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)
        from e = (Node (sourcenode a), kind a, Node (targetnode a))
          intra_kind (knd e) have "intra_kind (kind a)" by simp
        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
              intra_kind (kind a) kind a' = (λs. False)
            show ?thesis by(auto dest:deterministic simp:intra_kind_def)
          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 "VH. V  lift_Use Use Entry Exit H L (src e)"
            by(fastforce intro:lift_Use_High)
          with Vlift_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) pred (knd e) s pred (knd e) s'
          show ?thesis by(cases s,auto,cases s',auto)
        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 Vlift_Use Use Entry Exit H L (src e). 
            state_val s V = state_val s' V
          have "VUse (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))
            intra_kind (knd e)
          have "V  Def (sourcenode a). state_val (transfer (kind a) s) V =
            state_val (transfer (kind a) s') V"
            by -(erule CFG_intra_edge_transfer_uses_only_Use,auto)
          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
        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
      next
        case (lve_Entry_Exit_edge e)
        thus ?case by(cases s) auto
      qed
    qed
  next
    fix a s s'
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "pred (knd a) s" and "snd (hd s) = snd (hd s')"
      and "Vlift_Use Use Entry Exit H L (src a). state_val s V = state_val s' V"
      and "length s = length s'"
    thus "pred (knd a) s'"
    proof(induct rule:lift_valid_edge.induct)
      case (lve_edge a e)
      from e = (Node (sourcenode a), kind a, Node (targetnode a)) pred (knd e) s
      have "pred (kind a) s" and "src e = Node (sourcenode a)" by simp_all
      from src e = Node (sourcenode a) 
        Vlift_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(auto dest:lift_Use_node)
      from valid_edge a pred (kind a) s snd (hd s) = snd (hd s')
        this length s = length s'
      have "pred (kind a) s'" by(rule CFG_edge_Uses_pred_equal)
      with e = (Node (sourcenode a), kind a, Node (targetnode a))
      show ?case by simp
    next
      case (lve_Entry_edge e)
      thus ?case by(cases s') auto
    next
      case (lve_Exit_edge e)
      thus ?case by(cases s') auto
    next
      case (lve_Entry_Exit_edge e)
      thus ?case by(cases s) auto
    qed
  next
    fix a Q r p fs ins outs
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q:r↪⇘pfs" and "(p, ins, outs)  set procs"
    thus "length fs = length ins"
    proof(induct rule:lift_valid_edge.induct)
      case (lve_edge a e)
      from e = (Node (sourcenode a), kind a, Node (targetnode a)) knd e = Q:r↪⇘pfs
      have "kind a = Q:r↪⇘pfs" by simp
      from valid_edge a kind a = Q:r↪⇘pfs (p, ins, outs)  set procs
      show ?case by(rule CFG_call_edge_length)
    qed simp_all
  next
    fix a Q r p fs a' Q' r' p' fs' s s'
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q:r↪⇘pfs" and "knd a' = Q':r'↪⇘p'fs'"
      and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'"
      and "src a = src a'" and "pred (knd a) s" and "pred (knd a') s"
    from lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a
      knd a = Q:r↪⇘pfs pred (knd a) s
    obtain x where a:"a = (Node (sourcenode x),kind x,Node (targetnode x))" 
      and "valid_edge x" and "src a = Node (sourcenode x)" 
      and "kind x = Q:r↪⇘pfs" and "pred (kind x) s"
      by(fastforce elim:lift_valid_edge.cases)
    from lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'
      knd a' = Q':r'↪⇘p'fs' pred (knd a') s
    obtain x' where a':"a' = (Node (sourcenode x'),kind x',Node (targetnode x'))" 
      and "valid_edge x'" and "src a' = Node (sourcenode x')" 
      and "kind x' = Q':r'↪⇘p'fs'" and "pred (kind x') s"
      by(fastforce elim:lift_valid_edge.cases)
    from src a = Node (sourcenode x) src a' = Node (sourcenode x') 
      src a = src a'
    have "sourcenode x = sourcenode x'" by simp
    from valid_edge x kind x = Q:r↪⇘pfs valid_edge x' kind x' = Q':r'↪⇘p'fs'
      sourcenode x = sourcenode x' pred (kind x) s pred (kind x') s
    have "x = x'" by(rule CFG_call_determ)
    with a a' show "a = a'" by simp
  next
    fix a Q r p fs i ins outs s s'
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q:r↪⇘pfs" and "i < length ins" and "(p, ins, outs)  set procs"
      and "pred (knd a) s" and "pred (knd a) s'"
      and "Vlift_ParamUses ParamUses (src a) ! i. state_val s V = state_val s' V"
    thus "params fs (state_val s) ! i = CFG.params fs (state_val s') ! i"
    proof(induct rule:lift_valid_edge.induct)
      case (lve_edge a e)
      from e = (Node (sourcenode a), kind a, Node (targetnode a)) knd e = Q:r↪⇘pfs
        pred (knd e) s pred (knd e) s'
      have "kind a = Q:r↪⇘pfs" and "pred (kind a) s" and "pred (kind a) s'"
        and "src e = Node (sourcenode a)"
        by simp_all
      from Vlift_ParamUses ParamUses (src e) ! i. state_val s V = state_val s' V
        src e = Node (sourcenode a)
      have "V  (ParamUses (sourcenode a))!i. state_val s V = state_val s' V" by simp
      with valid_edge a kind a = Q:r↪⇘pfs i < length ins 
        (p, ins, outs)  set procs pred (kind a) s pred (kind a) s'
      show ?case by(rule CFG_call_edge_params)
    qed simp_all
  next
    fix a Q' p f' ins outs cf cf'
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q'↩⇘pf'" and "(p, ins, outs)  set procs"
    thus "f' cf cf' = cf'(lift_ParamDefs ParamDefs (trg a) [:=] map cf outs)"
    proof(induct rule:lift_valid_edge.induct)
      case (lve_edge a e)
      from e = (Node (sourcenode a), kind a, Node (targetnode a)) knd e = Q'↩⇘pf'
      have "kind a = Q'↩⇘pf'" and "trg e = Node (targetnode a)" by simp_all
      from valid_edge a kind a = Q'↩⇘pf' (p, ins, outs)  set procs
      have "f' cf cf' = cf'(ParamDefs (targetnode a) [:=] map cf outs)"
        by(rule CFG_return_edge_fun)
      with trg e = Node (targetnode a) show ?case by simp
    qed simp_all
  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'"
      and "intra_kind (knd a)" and "intra_kind (knd 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' intra_kind (knd e) intra_kind (knd a')
      show ?case
      proof(induct rule:lift_valid_edge.induct)
        case lve_edge thus ?case by(auto dest:deterministic)
      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)+
  qed
qed


lemma lift_CFGExit:
  assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry get_proc 
  get_return_edges procs Main Exit Def Use ParamDefs ParamUses"
  and pd:"Postdomination sourcenode targetnode kind valid_edge Entry get_proc 
  get_return_edges procs Main Exit"
  shows "CFGExit src trg knd
  (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
  (lift_get_proc get_proc Main) 
  (lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind) 
  procs Main NewExit"
proof -
  interpret CFGExit_wf sourcenode targetnode kind valid_edge Entry get_proc 
    get_return_edges procs Main Exit Def Use ParamDefs ParamUses
    by(rule wf)
  interpret Postdomination sourcenode targetnode kind valid_edge Entry get_proc 
    get_return_edges procs Main Exit
    by(rule pd)
  interpret CFG:CFG src trg knd
    "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit" NewEntry
    "lift_get_proc get_proc Main" 
    "lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind"
    procs Main
    by(fastforce intro:lift_CFG wf pd)
  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
    show "lift_get_proc get_proc Main NewExit = Main" by simp
  next
    fix a Q p f
    assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
      and "knd a = Q↩⇘pf" and "trg a = NewExit"
    thus False by(fastforce elim:lift_valid_edge.cases)
  next
    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 intro:lve_Entry_Exit_edge)
  qed
qed


lemma lift_CFGExit_wf:
  assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry get_proc 
  get_return_edges procs Main Exit Def Use ParamDefs ParamUses"
  and pd:"Postdomination sourcenode targetnode kind valid_edge Entry get_proc 
  get_return_edges procs Main Exit"
  shows "CFGExit_wf src trg knd
  (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewEntry
  (lift_get_proc get_proc Main) 
  (lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind) 
  procs Main NewExit (lift_Def Def Entry Exit H L) (lift_Use Use Entry Exit H L)
  (lift_ParamDefs ParamDefs) (lift_ParamUses ParamUses)"
proof -
  interpret CFGExit_wf sourcenode targetnode kind valid_edge Entry get_proc 
    get_return_edges procs Main Exit Def Use ParamDefs ParamUses
    by(rule wf)
  interpret Postdomination sourcenode targetnode kind valid_edge Entry get_proc 
    get_return_edges procs Main Exit
    by(rule pd)
  interpret CFG_wf:CFG_wf src trg knd
    "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit" NewEntry
    "lift_get_proc get_proc Main" 
    "lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind"
    procs Main "lift_Def Def Entry Exit H L" "lift_Use Use Entry Exit H L"
    "lift_ParamDefs ParamDefs" "lift_ParamUses ParamUses"
    by(fastforce intro:lift_CFG_wf wf pd)
  interpret CFGExit:CFGExit src trg knd
    "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit" NewEntry
    "lift_get_proc get_proc Main"
    "lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind"
    procs Main NewExit 
    by(fastforce intro:lift_CFGExit wf pd)
  show ?thesis
  proof
    show "lift_Def Def Entry Exit H L NewExit = {} 
      lift_Use Use Entry Exit H L NewExit = {}" 
      by(fastforce elim:lift_Def_set.cases lift_Use_set.cases)
  qed
qed


subsubsection ‹Lifting the SDG›



lemma lift_Postdomination:
  assumes wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry get_proc 
  get_return_edges procs Main Exit Def Use ParamDefs ParamUses"
  and pd:"Postdomination sourcenode targetnode kind valid_edge Entry get_proc 
  get_return_edges procs Main 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
  (lift_get_proc get_proc Main) 
  (lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind) 
  procs Main NewExit"
proof -
  interpret CFGExit_wf sourcenode targetnode kind valid_edge Entry get_proc 
    get_return_edges procs Main Exit Def Use ParamDefs ParamUses
    by(rule wf)
  interpret Postdomination sourcenode targetnode kind valid_edge Entry get_proc 
    get_return_edges procs Main Exit
    by(rule pd)
  interpret CFGExit:CFGExit src trg knd
    "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit" NewEntry
    "lift_get_proc get_proc Main"
    "lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind"
    procs Main NewExit 
    by(fastforce intro:lift_CFGExit wf pd)
  { fix m assume "valid_node m"
    then obtain a where "valid_edge a" and "m = sourcenode a  m = targetnode a"
      by(auto simp:valid_node_def)
    from m = sourcenode a  m = targetnode a
    have "CFG.CFG.valid_node src trg
      (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) (Node m)"
    proof
      assume "m = sourcenode a"
      show ?thesis
      proof(cases "m = Entry")
        case True
        have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
          (NewEntry,(λs. True),Node Entry)" by(fastforce intro:lve_Entry_edge)
        with m = Entry show ?thesis by(fastforce simp:CFGExit.valid_node_def)
      next
        case False
        with m = sourcenode a valid_edge a
        have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
          (Node (sourcenode a),kind a,Node(targetnode a))"
          by(fastforce intro:lve_edge)
        with m = sourcenode a show ?thesis by(fastforce simp:CFGExit.valid_node_def)
      qed
    next
      assume "m = targetnode a"
      show ?thesis
      proof(cases "m = Exit")
        case True
        have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
          (Node Exit,(λs. True),NewExit)" by(fastforce intro:lve_Exit_edge)
        with m = Exit show ?thesis by(fastforce simp:CFGExit.valid_node_def)
      next
        case False
        with m = targetnode a valid_edge a
        have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
          (Node (sourcenode a),kind a,Node(targetnode a))"
          by(fastforce intro:lve_edge)
        with m = targetnode a show ?thesis by(fastforce simp:CFGExit.valid_node_def)
      qed
    qed }
  note lift_valid_node = this
  { fix n as n' cs m m'
    assume "valid_path_aux cs as" and "m -as→* m'" and "c  set cs. valid_edge c"
      and "m  Entry  m'  Exit"
    hence "cs' es. CFG.CFG.valid_path_aux knd
      (lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind)
      cs' es  
      list_all2 (λc c'. c' = (Node (sourcenode c),kind c,Node (targetnode c))) cs cs' 
        CFG.CFG.path src trg
      (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
      (Node m) es (Node m')"
    proof(induct arbitrary:m rule:vpa_induct)
      case (vpa_empty cs)
      from m -[]→* m' have [simp]:"m = m'" by fastforce
      from m -[]→* m' have "valid_node m" by(rule path_valid_node)
      obtain cs' where "cs' = 
        map (λc. (Node (sourcenode c),kind c,Node (targetnode c))) cs" by simp
      hence "list_all2 
        (λc c'. c' = (Node (sourcenode c),kind c,Node (targetnode c))) cs cs'"
        by(simp add:list_all2_conv_all_nth)
      with valid_node m show ?case
        apply(rule_tac x="cs'" in exI)
        apply(rule_tac x="[]" in exI)
        by(fastforce intro:CFGExit.empty_path lift_valid_node)
    next
      case (vpa_intra cs a as)
      note IH = m. m -as→* m'; cset cs. valid_edge c; m  Entry  m'  Exit 
        cs' es. CFG.valid_path_aux knd
        (lift_get_return_edges get_return_edges valid_edge sourcenode
        targetnode kind) cs' es 
        list_all2 (λc c'. c' = (Node (sourcenode c), kind c, Node (targetnode c))) cs
        cs'  CFG.path src trg
        (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
        (Node m) es (Node m')
      from m -a # as→* m' have "m = sourcenode a" and "valid_edge a"
        and "targetnode a -as→* m'" by(auto elim:path_split_Cons)
      show ?case
      proof(cases "sourcenode a = Entry  targetnode a = Exit")
        case True
        with m = sourcenode a m  Entry  m'  Exit
        have "m'  Exit" by simp
        from True have "targetnode a = Exit" by simp
        with targetnode a -as→* m' have "m' = Exit"
          by -(drule path_Exit_source,auto)
        with m'  Exit have False by simp
        thus ?thesis by simp
      next
        case False
        let ?e = "(Node (sourcenode a),kind a,Node (targetnode a))"
        from False valid_edge a 
        have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit ?e"
          by(fastforce intro:lve_edge)
        have "targetnode a  Entry"
        proof
          assume "targetnode a = Entry"
          with valid_edge a show False by(rule Entry_target)
        qed
        hence "targetnode a  Entry  m'  Exit" by simp
        from IH[OF targetnode a -as→* m' cset cs. valid_edge c this] 
        obtain cs' es
          where valid_path:"CFG.valid_path_aux knd
          (lift_get_return_edges get_return_edges valid_edge sourcenode 
          targetnode kind) cs' es" 
          and list:"list_all2 
          (λc c'. c' = (Node (sourcenode c), kind c, Node (targetnode c))) cs cs'"
          and path:"CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          (Node (targetnode a)) es (Node m')" by blast
        from intra_kind (kind a) valid_path have "CFG.valid_path_aux knd
          (lift_get_return_edges get_return_edges valid_edge sourcenode 
          targetnode kind) cs' (?e#es)" by(fastforce simp:intra_kind_def)
        moreover
        from path m = sourcenode a 
          lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit ?e
        have "CFG.path src trg
          (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
          (Node m) (?e#es) (Node m')" by(fastforce intro:CFGExit.Cons_path)
        ultimately show ?thesis using list by blast
      qed
    next
      case (vpa_Call cs a as Q r p fs)
      note IH = m. m -as→* m'; cset (a # cs). valid_edge c; 
        m  Entry  m'  Exit 
        cs' es. CFG.valid_path_aux knd
        (lift_get_return_edges get_return_edges valid_edge sourcenode
        targetnode kind) cs' es 
        list_all2 (λc c'. c' = (Node (sourcenode c), kind c, Node (targetnode c))) 
        (a#cs) cs'  CFG.path src trg
        (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
        (Node m) es (Node m')
      from m -a # as→* m' have "m = sourcenode a" and "valid_edge a"
        and "targetnode a -as→* m'" by(auto elim:path_split_Cons)
      from cset cs. valid_edge c valid_edge a 
      have "cset (a # cs). valid_edge c" by simp
      let ?e = "(Node (sourcenode a),kind a,Node (targetnode a))"
      have "sourcenode a  Entry"
      proof
        assume "sourcenode a = Entry"
        with valid_edge a kind a = Q:r↪⇘pfs 
        show False by(rule Entry_no_call_source)
      qed
      with valid_edge a 
      have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit ?e"
        by(fastforce intro:lve_edge)
      have "targetnode a  Entry"
      proof
        assume "targetnode a = Entry"
        with valid_edge a show False by(rule Entry_target)
      qed
      hence "targetnode a  Entry  m'  Exit" by simp
      from IH[OF targetnode a -as→* m' cset (a # cs). valid_edge c this]
      obtain cs' es
        where valid_path:"CFG.valid_path_aux knd
        (lift_get_return_edges get_return_edges valid_edge sourcenode 
        targetnode kind) cs' es" 
        and list:"list_all2 
        (λc c'. c' = (Node (sourcenode c), kind c, Node (targetnode c))) (a#cs) cs'"
        and path:"CFG.path src trg
        (lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
        (Node (targetnode a)) es (Node m')" by blast
      from list obtain cx csx where "cs' = cx#csx"
        and cx:"cx = (Node (sourcenode a), kind a, Node (targetnode a))"
        and list':"list_all2 
        (λc c'. c' = (Node (sourcenode c), kind c, Node (targetnode c))) cs csx"
        by(fastforce simp:list_all2_Cons1)
      from valid_path cx cs' = cx#csx kind a = Q:r↪⇘pfs
      have "CFG.valid_path_aux knd
        (lift_get_return_edges get_return_edges valid_edge sourcenode 
        targetnode kind) csx (?e#es)" by simp
      moreover
      from path m = sourcenode a 
        lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit ?e
      have "CFG.path src trg