# Theory LiftingInter

theory LiftingInter
imports NonInterferenceInter
```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↪⇘p⇙fs" 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↪⇘Main⇙f"
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'↩⇘Main⇙f'"
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↪⇘p⇙fs"
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↪⇘p⇙fs"
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'↩⇘p⇙f'"
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↪⇘p⇙fs"
then obtain ax where "valid_edge ax" and "kind ax = Q:r↪⇘p⇙fs"
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↪⇘p⇙fs›
have all:"∀a'. valid_edge a' ∧ targetnode a' = targetnode ax ⟶
(∃Qx rx fsx. kind a' = Qx:rx↪⇘p⇙fsx)"
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↪⇘p⇙fsx"
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↪⇘p⇙fsx" 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↪⇘p⇙fsx)" by simp
next
fix a Q' p f'
assume "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "knd a = Q'↩⇘p⇙f'"
then obtain ax where "valid_edge ax" and "kind ax = Q'↩⇘p⇙f'"
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'↩⇘p⇙f'›
have all:"∀a'. valid_edge a' ∧ sourcenode a' = sourcenode ax ⟶
(∃Qx fx. kind a' = Qx↩⇘p⇙fx)"
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↩⇘p⇙fx"
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↩⇘p⇙fx" 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↩⇘p⇙fx)" 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↪⇘p⇙fs"
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↪⇘p⇙fs›
have "kind ax = Q:r↪⇘p⇙fs" 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↪⇘p⇙fs" by(fastforce dest!:only_call_get_return_edges)
with ‹valid_edge ax› ‹a' ∈ get_return_edges ax› obtain Q' f'
where "kind a' = Q'↩⇘p⇙f'" by(fastforce dest!:call_return_edges)
from ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'› 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'↩⇘p⇙f'› have "kind a' = Q'↩⇘Main⇙f'" 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↪⇘p⇙fs"
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↪⇘p⇙fs"
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↪⇘p⇙fs"
and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
thus "∃Q' f'. knd a' = Q'↩⇘p⇙f'"
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↪⇘p⇙fs›
have "kind ax = Q:r↪⇘p⇙fs" by simp
with ‹valid_edge ax› ‹a' ∈ get_return_edges ax› have "∃Q' f'. kind a' = Q'↩⇘p⇙f'"
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'↩⇘p⇙f'"
thus "∃!a'. lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a' ∧
(∃Q r fs. knd a' = Q:r↪⇘p⇙fs) ∧ 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'↩⇘p⇙f'› have "kind a = Q'↩⇘p⇙f'" by simp
with ‹valid_edge a›
have "∃!a'. valid_edge a' ∧ (∃Q r fs. kind a' = Q:r↪⇘p⇙fs) ∧
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↪⇘p⇙fs"
and "a ∈ get_return_edges a'"
and imp:"∀x. valid_edge x ∧ (∃Q r fs. kind x = Q:r↪⇘p⇙fs) ∧
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↪⇘p⇙fs›
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↪⇘p⇙fs› have "knd ?e' = Q:r↪⇘p⇙fs" 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↪⇘p⇙fs"
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↪⇘p⇙fs› 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↪⇘p⇙fs› have "∃Q r fs. kind ax = Q:r↪⇘p⇙fs" 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)⇩√"
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↪⇘p⇙fs"
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↪⇘p⇙fs› 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↪⇘p⇙fs"
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↪⇘p⇙fs›
have "kind a = Q:r↪⇘p⇙fs" 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↪⇘p⇙fs› 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'↩⇘p⇙f'"
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'↩⇘p⇙f'›
have "kind a = Q'↩⇘p⇙f'" 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'↩⇘p⇙f'› 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' Q⇩1 r⇩1 p fs⇩1 Q⇩2 r⇩2 fs⇩2
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 = Q⇩1:r⇩1↪⇘p⇙fs⇩1" and "knd a' = Q⇩2:r⇩2↪⇘p⇙fs⇩2"
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 = Q⇩1:r⇩1↪⇘p⇙fs⇩1› ‹knd a' = Q⇩2:r⇩2↪⇘p⇙fs⇩2›
have "kind x = Q⇩1:r⇩1↪⇘p⇙fs⇩1" and "kind x' = Q⇩2:r⇩2↪⇘p⇙fs⇩2" 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↪⇘p⇙fs" 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↪⇘p⇙fs›
have "kind a = Q:r↪⇘p⇙fs" 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'↩⇘p⇙f'" 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'↩⇘p⇙f'›
have "kind a = Q'↩⇘p⇙f'" 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↪⇘p⇙fs" 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↪⇘p⇙fs›
have "kind a = Q:r↪⇘p⇙fs" by simp
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹(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↪⇘p⇙fs"
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↪⇘p⇙fs›
have "kind a = Q:r↪⇘p⇙fs" 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↪⇘p⇙fs›
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↩⇘p⇙f" 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↩⇘p⇙f›
have "kind a = Q↩⇘p⇙f" by simp
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› ‹(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"
"∀V∈lift_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 "∀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)
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 "∀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)⇩√› ‹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 ‹∀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))›
‹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 "∀V∈lift_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)›
‹∀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(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↪⇘p⇙fs" 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↪⇘p⇙fs›
have "kind a = Q:r↪⇘p⇙fs" by simp
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹(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↪⇘p⇙fs" 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↪⇘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 ‹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↪⇘p⇙fs› ‹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↪⇘p⇙fs" and "i < length ins" and "(p, ins, outs) ∈ set procs"
and "pred (knd a) s" and "pred (knd a) s'"
and "∀V∈lift_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↪⇘p⇙fs›
‹pred (knd e) s› ‹pred (knd e) s'›
have "kind a = Q:r↪⇘p⇙fs" and "pred (kind a) s" and "pred (kind a) s'"
and "src e = Node (sourcenode a)"
by simp_all
from ‹∀V∈lift_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↪⇘p⇙fs› ‹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'↩⇘p⇙f'" 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'↩⇘p⇙f'›
have "kind a = Q'↩⇘p⇙f'" and "trg e = Node (targetnode a)" by simp_all
from ‹valid_edge a› ‹kind a = Q'↩⇘p⇙f'› ‹(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↩⇘p⇙f" 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'"
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'; ∀c∈set 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'› ‹∀c∈set 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'; ∀c∈set (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 ‹∀c∈set cs. valid_edge c› ‹valid_edge a›
have "∀c∈set (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↪⇘p⇙fs›
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'› ‹∀c∈set (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↪⇘p⇙fs›
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
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node m) (?e#es) (Node m')" by(fastforce intro:CFGExit.Cons_path)
ultimately show ?case using list' by blast
next
case (vpa_ReturnEmpty cs a as Q p f)
note IH = ‹⋀m. ⟦m -as→* m'; ∀c∈set []. 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' ∧ 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)
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↩⇘p⇙f› show False by(rule Exit_no_return_target)
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'› _ this] obtain es
where valid_path:"CFG.valid_path_aux knd
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind) [] es"
and path:"CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node (targetnode a)) es (Node m')" by auto
from valid_path ‹kind a = Q↩⇘p⇙f›
have "CFG.valid_path_aux knd
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind) [] (?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
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node m) (?e#es) (Node m')" by(fastforce intro:CFGExit.Cons_path)
ultimately show ?case using ‹cs = []› by blast
next
case (vpa_ReturnCons cs a as Q p f c' cs')
note IH = ‹⋀m. ⟦m -as→* m'; ∀c∈set cs'. valid_edge c; m ≠ Entry ∨ m' ≠ Exit⟧ ⟹
∃csx es. CFG.valid_path_aux knd
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind) csx es ∧
list_all2 (λc c'. c' = (Node (sourcenode c), kind c, Node (targetnode c)))
cs' csx ∧ 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 ‹∀c∈set cs. valid_edge c› ‹cs = c' # cs'›
have "valid_edge c'" and "∀c∈set cs'. valid_edge c" by simp_all
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↩⇘p⇙f› show False by(rule Exit_no_return_target)
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'› ‹∀c∈set cs'. valid_edge c› this]
obtain csx es
where valid_path:"CFG.valid_path_aux knd
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind) csx es"
and list:"list_all2
(λc c'. c' = (Node (sourcenode c), kind c, Node (targetnode c))) cs' csx"
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 ‹valid_edge c'› ‹a ∈ get_return_edges c'›
have "?e ∈ lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind (Node (sourcenode c'),kind c',Node (targetnode c'))"
by(fastforce intro:lift_get_return_edgesI)
with valid_path ‹kind a = Q↩⇘p⇙f›
have "CFG.valid_path_aux knd
(lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind)
((Node (sourcenode c'),kind c',Node (targetnode c'))#csx) (?e#es)"
by simp
moreover
from list ‹cs = c' # cs'›
have "list_all2
(λc c'. c' = (Node (sourcenode c), kind c, Node (targetnode c))) cs
((Node (sourcenode c'),kind c',Node (targetnode c'))#csx)"
by simp
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 ?case using ‹kind a = Q↩⇘p⇙f› by blast
qed }
hence lift_valid_path:"⋀m as m'. ⟦m -as→⇩√* m'; m ≠ Entry ∨ m' ≠ Exit⟧
⟹ ∃es. CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind)
(Node m) es (Node m')"
by(fastforce simp:vp_def valid_path_def CFGExit.vp_def CFGExit.valid_path_def)
show ?thesis
proof
fix n assume "CFG.CFG.valid_node src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) n"
hence "((n = NewEntry) ∨ n = NewExit) ∨ (∃m. n = Node m ∧ valid_node m)"
by(auto elim:lift_valid_edge.cases simp:CFGExit.valid_node_def)
thus "∃as. CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind)
NewEntry as n" apply -
proof(erule disjE)+
assume "n = NewEntry"
hence "CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind)
NewEntry [] n"
by(fastforce intro:CFGExit.empty_path
simp:CFGExit.vp_def CFGExit.valid_path_def)
thus ?thesis by blast
next
assume "n = NewExit"
have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(NewEntry,(λs. False)⇩√,NewExit)" by(fastforce intro:lve_Entry_Exit_edge)
hence "CFG.CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
NewEntry [(NewEntry,(λs. False)⇩√,NewExit)] NewExit"
by(fastforce dest:CFGExit.path_edge)
with ‹n = NewExit› have "CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind)
NewEntry [(NewEntry,(λs. False)⇩√,NewExit)] n"
by(fastforce simp:CFGExit.vp_def CFGExit.valid_path_def)
thus ?thesis by blast
next
assume "∃m. n = Node m ∧ valid_node m"
then obtain m where "n = Node m" and "valid_node m" by blast
from ‹valid_node m›
show ?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 ‹m = Entry› ‹n = Node m› have "CFG.CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
NewEntry [(NewEntry,(λs. True)⇩√,Node Entry)] n"
by(fastforce intro:CFGExit.Cons_path CFGExit.empty_path
simp:CFGExit.valid_node_def)
thus ?thesis by(fastforce simp:CFGExit.vp_def CFGExit.valid_path_def)
next
case Exit
from inner obtain ax where "valid_edge ax" and "intra_kind (kind 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 "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:CFGExit.Cons_path CFGExit.empty_path
simp:CFGExit.valid_node_def)
with ‹intra_kind (kind ax)›
have slp_edge:"CFG.CFG.same_level_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind)
(Node (sourcenode ax)) [(Node (sourcenode ax),kind ax,Node Exit)]
(Node Exit)"
by(fastforce simp:CFGExit.slp_def CFGExit.same_level_path_def
intra_kind_def)
have "sourcenode ax ≠ Exit"
proof
assume "sourcenode ax = Exit"
with ‹valid_edge ax› show False by(rule Exit_source)
qed
have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(NewEntry,(λs. True)⇩√,Node Entry)" by(fastforce intro:lve_Entry_edge)
hence "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(NewEntry) [(NewEntry,(λs. True)⇩√,Node Entry)] (Node Entry)"
by(fastforce intro:CFGExit.Cons_path CFGExit.empty_path
simp:CFGExit.valid_node_def)
hence slp_edge':"CFG.CFG.same_level_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind)
(NewEntry) [(NewEntry,(λs. True)⇩√,Node Entry)] (Node Entry)"
by(fastforce simp:CFGExit.slp_def CFGExit.same_level_path_def)
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)
with ‹sourcenode ax ≠ Exit›
have "∃es. CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind) (Node Entry) es (Node (sourcenode ax))"
by(fastforce intro:lift_valid_path)
then obtain es where "CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind) (Node Entry) es (Node (sourcenode ax))" by blast
with slp_edge have "CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind)
(Node Entry) (es@[(Node (sourcenode ax),kind ax,Node Exit)]) (Node Exit)"
by -(rule CFGExit.vp_slp_Append)
with slp_edge' have "CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind) NewEntry
([(NewEntry,(λs. True)⇩√,Node Entry)]@
(es@[(Node (sourcenode ax),kind ax,Node Exit)])) (Node Exit)"
by(rule CFGExit.slp_vp_Append)
with ‹m = Exit› ‹n = Node m› show ?thesis by simp blast
next
case inner
have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(NewEntry,(λs. True)⇩√,Node Entry)" by(fastforce intro:lve_Entry_edge)
hence "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(NewEntry) [(NewEntry,(λs. True)⇩√,Node Entry)] (Node Entry)"
by(fastforce intro:CFGExit.Cons_path CFGExit.empty_path
simp:CFGExit.valid_node_def)
hence slp_edge:"CFG.CFG.same_level_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind)
(NewEntry) [(NewEntry,(λs. True)⇩√,Node Entry)] (Node Entry)"
by(fastforce simp:CFGExit.slp_def CFGExit.same_level_path_def)
from ‹valid_node m› obtain as where "Entry -as→⇩√* m"
by(fastforce dest:Entry_path)
with ‹inner_node m›
have "∃es. CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind) (Node Entry) es (Node m)"
by(fastforce intro:lift_valid_path simp:inner_node_def)
then obtain es where "CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind) (Node Entry) es (Node m)" by blast
with slp_edge have "CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind) NewEntry ([(NewEntry,(λs. True)⇩√,Node Entry)]@es) (Node m)"
by(rule CFGExit.slp_vp_Append)
with ‹n = Node m› show ?thesis by simp blast
qed
qed
next
fix n assume "CFG.CFG.valid_node src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) n"
hence "((n = NewEntry) ∨ n = NewExit) ∨ (∃m. n = Node m ∧ valid_node m)"
by(auto elim:lift_valid_edge.cases simp:CFGExit.valid_node_def)
thus "∃as. CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind)
n as NewExit" apply -
proof(erule disjE)+
assume "n = NewEntry"
have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit
(NewEntry,(λs. False)⇩√,NewExit)" by(fastforce intro:lve_Entry_Exit_edge)
hence "CFG.CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
NewEntry [(NewEntry,(λs. False)⇩√,NewExit)] NewExit"
by(fastforce dest:CFGExit.path_edge)
with ‹n = NewEntry› have "CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind)
n [(NewEntry,(λs. False)⇩√,NewExit)] NewExit"
by(fastforce simp:CFGExit.vp_def CFGExit.valid_path_def)
thus ?thesis by blast
next
assume "n = NewExit"
hence "CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind)
n [] NewExit"
by(fastforce intro:CFGExit.empty_path
simp:CFGExit.vp_def CFGExit.valid_path_def)
thus ?thesis by blast
next
assume "∃m. n = Node m ∧ valid_node m"
then obtain m where "n = Node m" and "valid_node m" by blast
from ‹valid_node m›
show ?thesis
proof(cases m rule:valid_node_cases)
case Entry
from inner obtain ax where "valid_edge ax" and "intra_kind (kind ax)"
and "inner_node (targetnode ax)" and "sourcenode ax = Entry"
by(erule inner_node_Entry_edge)
hence "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)
hence "CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(Node Entry) [(Node Entry,kind ax,Node (targetnode ax))]
(Node (targetnode ax))"
by(fastforce intro:CFGExit.Cons_path CFGExit.empty_path
simp:CFGExit.valid_node_def)
with ‹intra_kind (kind ax)›
have slp_edge:"CFG.CFG.same_level_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind)
(Node Entry) [(Node Entry,kind ax,Node (targetnode ax))]
(Node (targetnode ax))"
by(fastforce simp:CFGExit.slp_def CFGExit.same_level_path_def
intra_kind_def)
have "targetnode ax ≠ Entry"
proof
assume "targetnode ax = Entry"
with ‹valid_edge ax› show False by(rule Entry_target)
qed
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:CFGExit.Cons_path CFGExit.empty_path
simp:CFGExit.valid_node_def)
hence slp_edge':"CFG.CFG.same_level_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind)
(Node Exit) [(Node Exit,(λs. True)⇩√,NewExit)] NewExit"
by(fastforce simp:CFGExit.slp_def CFGExit.same_level_path_def)
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)
with ‹targetnode ax ≠ Entry›
have "∃es. CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind) (Node (targetnode ax)) es (Node Exit)"
by(fastforce intro:lift_valid_path)
then obtain es where "CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind) (Node (targetnode ax)) es (Node Exit)" by blast
with slp_edge have "CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind)
(Node Entry) ([(Node Entry,kind ax,Node (targetnode ax))]@es) (Node Exit)"
by(rule CFGExit.slp_vp_Append)
with slp_edge' have "CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind) (Node Entry)
(([(Node Entry,kind ax,Node (targetnode ax))]@es)@
[(Node Exit,(λs. True)⇩√,NewExit)]) NewExit"
by -(rule CFGExit.vp_slp_Append)
with ‹m = Entry› ‹n = Node m› show ?thesis by simp blast
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 ‹m = Exit› ‹n = Node m› have "CFG.CFG.path src trg
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
n [(Node Exit,(λs. True)⇩√,NewExit)] NewExit"
by(fastforce intro:CFGExit.Cons_path CFGExit.empty_path
simp:CFGExit.valid_node_def)
thus ?thesis by(fastforce simp:CFGExit.vp_def CFGExit.valid_path_def)
next
case inner
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:CFGExit.Cons_path CFGExit.empty_path
simp:CFGExit.valid_node_def)
hence slp_edge:"CFG.CFG.same_level_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind)
(Node Exit) [(Node Exit,(λs. True)⇩√,NewExit)] NewExit"
by(fastforce simp:CFGExit.slp_def CFGExit.same_level_path_def)
from ‹valid_node m› obtain as where "m -as→⇩√* Exit"
by(fastforce dest:Exit_path)
with ‹inner_node m›
have "∃es. CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind) (Node m) es (Node Exit)"
by(fastforce intro:lift_valid_path simp:inner_node_def)
then obtain es where "CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind) (Node m) es (Node Exit)" by blast
with slp_edge have "CFG.CFG.valid_path' src trg knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit)
(lift_get_return_edges get_return_edges valid_edge sourcenode
targetnode kind) (Node m) (es@[(Node Exit,(λs. True)⇩√,NewExit)]) NewExit"
by -(rule CFGExit.vp_slp_Append)
with ‹n = Node m› show ?thesis by simp blast
qed
qed
next
fix n n'
assume method_exit1:"CFGExit.CFGExit.method_exit src knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewExit n"
and method_exit2:"CFGExit.CFGExit.method_exit src knd
(lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit) NewExit n'"
and lift_eq:"lift_get_proc get_proc Main n = lift_get_proc get_proc Main n'"
from method_exit1 show "n = n'"
proof(rule CFGExit.method_exit_cases)
assume "n = NewExit"
from method_exit2 show ?thesis
proof(rule CFGExit.method_exit_cases)
assume "n' = NewExit"
with ‹n = NewExit› show ?thesis by simp
next
fix a Q f p
assume "n' = src a"
and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "knd a = Q↩⇘p⇙f"
hence "lift_get_proc get_proc Main (src a) = p"
by -(rule CFGExit.get_proc_return)
with CFGExit.get_proc_Exit lift_eq ‹n' = src a› ‹n = NewExit›
have "p = Main" by simp
with ‹knd a = Q↩⇘p⇙f› have "knd a = Q↩⇘Main⇙f" by simp
with ‹lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a›
have False by(rule CFGExit.Main_no_return_source)
thus ?thesis by simp
qed
next
fix a Q f p
assume "n = src a"
and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
and "knd a = Q↩⇘p⇙f"
then obtain x where "valid_edge x" and "src a = Node (sourcenode x)"
and "kind x = Q↩⇘p⇙f"
by(fastforce elim:lift_valid_edge.cases)
hence "method_exit (sourcenode x)" by(fastforce simp:method_exit_def)
from method_exit2 show ?thesis
proof(rule CFGExit.method_exit_cases)
assume "n' = NewExit"
from ‹lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a›
‹knd a = Q↩⇘p⇙f›
have "lift_get_proc get_proc Main (src a) = p"
by -(rule CFGExit.get_proc_return)
with CFGExit.get_proc_Exit lift_eq ‹n = src a› ‹n' = NewExit›
have "p = Main" by simp
with ‹knd a = Q↩⇘p⇙f› have "knd a = Q↩⇘Main⇙f" by simp
with ‹lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a›
have False by(rule CFGExit.Main_no_return_source)
thus ?thesis by simp
next
fix a' Q' f' p'
assume "n' = src a'"
and "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a'"
and "knd a' = Q'↩⇘p'⇙f'"
then obtain x' where "valid_edge x'" and "src a' = Node (sourcenode x')"
and "kind x' = Q'↩⇘p'⇙f'"
by(fastforce elim:lift_valid_edge.cases)
hence "method_exit (sourcenode x')" by(fastforce simp:method_exit_def)
with ‹method_exit (sourcenode x)› lift_eq ‹n = src a› ‹n' = src a'›
‹src a = Node (sourcenode x)› ‹src a' = Node (sourcenode x')›
have "sourcenode x = sourcenode x'" by(fastforce intro:method_exit_unique)
with ‹src a = Node (sourcenode x)› ‹src a' = Node (sourcenode x')›
‹n = src a› ‹n' = src a'›
show ?thesis by simp
qed
qed
qed
qed

lemma lift_SDG:
assumes SDG:"SDG sourcenode targetnode kind valid_edge Entry get_proc
get_return_edges procs Main Exit Def Use ParamDefs ParamUses"
and inner:"CFGExit.inner_node sourcenode targetnode valid_edge Entry Exit nx"
shows "SDG 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 SDG sourcenode targetnode kind valid_edge Entry get_proc
get_return_edges procs Main Exit Def Use ParamDefs ParamUses
by(rule SDG)
have wf:"CFGExit_wf sourcenode targetnode kind valid_edge Entry get_proc
get_return_edges procs Main Exit Def Use ParamDefs ParamUses"
by(unfold_locales)
have pd:"Postdomination sourcenode targetnode kind valid_edge Entry get_proc
get_return_edges procs Main Exit"
by(unfold_locales)
interpret wf':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"
by(fastforce intro:lift_CFGExit_wf wf pd)
interpret pd':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
by(fastforce intro:lift_Postdomination wf pd inner)
show ?thesis by(unfold_locales)
qed

subsubsection ‹Low-deterministic security via the lifted graph›

lemma Lift_NonInterferenceGraph:
fixes valid_edge and sourcenode and targetnode and kind and Entry and Exit
and get_proc and get_return_edges and procs and Main
and Def and Use and ParamDefs and ParamUses and H and L
defines lve:"lve ≡ lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit"
and lget_proc:"lget_proc ≡ lift_get_proc get_proc Main"
and lget_return_edges:"lget_return_edges ≡
lift_get_return_edges get_return_edges valid_edge sourcenode targetnode kind"
and lDef:"lDef ≡ lift_Def Def Entry Exit H L"
and lUse:"lUse ≡ lift_Use Use Entry Exit H L"
and lParamDefs:"lParamDefs ≡ lift_ParamDefs ParamDefs"
and lParamUses:"lParamUses ≡ lift_ParamUses ParamUses"
assumes SDG:"SDG sourcenode targetnode kind valid_edge Entry get_proc
get_return_edges procs Main Exit Def Use ParamDefs ParamUses"
and inner:"CFGExit.inner_node sourcenode targetnode valid_edge Entry Exit nx"
and "H ∩ L = {}" and "H ∪ L = UNIV"
shows "NonInterferenceInterGraph src trg knd lve NewEntry lget_proc
lget_return_edges procs Main NewExit lDef lUse lParamDefs lParamUses H L
(Node Entry) (Node Exit)"
proof -
interpret SDG sourcenode targetnode kind valid_edge Entry get_proc
get_return_edges procs Main Exit Def Use ParamDefs ParamUses
by(rule SDG)
interpret SDG':SDG src trg knd lve NewEntry lget_proc lget_return_edges
procs Main NewExit lDef lUse lParamDefs lParamUses
by(fastforce intro:lift_SDG SDG inner simp:lve lget_proc lget_return_edges lDef
lUse lParamDefs lParamUses)
show ?thesis
proof
fix a assume "lve a" and "src a = NewEntry"
thus "trg a = NewExit ∨ trg a = Node Entry"
by(fastforce elim:lift_valid_edge.cases simp:lve)
next
show "∃a. lve a ∧ src a = NewEntry ∧ trg a = Node Entry ∧ knd a = (λs. True)⇩√"
by(fastforce intro:lve_Entry_edge simp:lve)
next
fix a assume "lve a" and "trg a = Node Entry"
from ‹lve a›
have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
from this ‹trg a = Node Entry›
show "src a = NewEntry"
proof(induct rule:lift_valid_edge.induct)
case (lve_edge a e)
from ‹e = (Node (sourcenode a), kind a, Node (targetnode a))›
‹trg e = Node Entry›
have "targetnode a = Entry" by simp
with ‹valid_edge a› have False by(rule Entry_target)
thus ?case by simp
qed simp_all
next
fix a assume "lve a" and "trg a = NewExit"
thus "src a = NewEntry ∨ src a = Node Exit"
by(fastforce elim:lift_valid_edge.cases simp:lve)
next
show "∃a. lve a ∧ src a = Node Exit ∧ trg a = NewExit ∧ knd a = (λs. True)⇩√"
by(fastforce intro:lve_Exit_edge simp:lve)
next
fix a assume "lve a" and "src a = Node Exit"
from ‹lve a›
have "lift_valid_edge valid_edge sourcenode targetnode kind Entry Exit a"
from this ‹src a = Node Exit›
show "trg a = NewExit"
proof(induct rule:lift_valid_edge.induct)
case (lve_edge a e)
from ‹e = (Node (sourcenode a), kind a, Node (targetnode a))›
‹src e = Node Exit›
have "sourcenode a = Exit" by simp
with ‹valid_edge a› have False by(rule Exit_source)
thus ?case by simp
qed simp_all
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

```