Theory WellFormed

section ‹Instantiate well-formedness locales with Proc CFG›

theory WellFormed imports Interpretation Labels "../StaticInter/CFGExit_wf" begin

subsection ‹Determining the first atomic command›

fun fst_cmd :: "cmd  cmd"
where "fst_cmd (c1;;c2) = fst_cmd c1"
  | "fst_cmd c = c"

lemma Proc_CFG_Call_target_fst_cmd_Skip:
  "labels prog l' c; prog  n -CEdge (p,es,rets)p Label l' 
   fst_cmd c = Skip"
proof(induct arbitrary:n rule:labels.induct) 
  case (Labels_Seq1 c1 l c c2)
  note IH = n. c1  n -CEdge (p, es, rets)p Label l  fst_cmd c = Skip
  from c1;; c2  n -CEdge (p, es, rets)p Label l labels c1 l c
  have "c1  n -CEdge (p, es, rets)p Label l"
    apply - apply(erule Proc_CFG.cases,auto dest:Proc_CFG_Call_Labels)
    by(case_tac n')(auto dest:label_less_num_inner_nodes)
  from IH[OF this] show ?case by simp
next
  case (Labels_Seq2 c2 l c c1)
  note IH = n. c2  n -CEdge (p, es, rets)p Label l  fst_cmd c = Skip
  from c1;; c2  n -CEdge (p, es, rets)p Label (l + #:c1) labels c2 l c
  obtain nx where "c2  nx -CEdge (p, es, rets)p Label l"
    apply - apply(erule Proc_CFG.cases)
    apply(auto dest:Proc_CFG_targetlabel_less_num_nodes Proc_CFG_Call_Labels)
    by(case_tac n') auto
  from IH[OF this] show ?case by simp
next
  case (Labels_CondTrue c1 l c b c2)
  note IH = n. c1  n -CEdge (p, es, rets)p Label l  fst_cmd c = Skip
  from if (b) c1 else c2  n -CEdge (p, es, rets)p Label (l + 1) labels c1 l c
  obtain nx where "c1  nx -CEdge (p, es, rets)p Label l"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(case_tac n') apply auto
    by(case_tac n')(auto dest:label_less_num_inner_nodes)
  from IH[OF this] show ?case by simp
next
  case (Labels_CondFalse c2 l c b c1)
  note IH = n. c2  n -CEdge (p, es, rets)p Label l  fst_cmd c = Skip
  from if (b) c1 else c2  n -CEdge (p, es, rets)p Label (l + #:c1 + 1) 
    labels c2 l c
  obtain nx where "c2  nx -CEdge (p, es, rets)p Label l"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(case_tac n') apply(auto dest:Proc_CFG_targetlabel_less_num_nodes)
    by(case_tac n') auto
  from IH[OF this] show ?case by simp
next
  case (Labels_WhileBody c' l c b)
  note IH = n. c'  n -CEdge (p, es, rets)p Label l  fst_cmd c = Skip
  from while (b) c'  n -CEdge (p, es, rets)p Label (l + 2) labels c' l c
  obtain nx where "c'  nx -CEdge (p, es, rets)p Label l"
    apply - apply(erule Proc_CFG.cases,auto)
    by(case_tac n') auto
  from IH[OF this] show ?case by simp
next
  case (Labels_Call px esx retsx)
  from Call px esx retsx  n -CEdge (p, es, rets)p Label 1
  show ?case by(fastforce elim:Proc_CFG.cases)
qed(auto dest:Proc_CFG_Call_Labels)


lemma Proc_CFG_Call_source_fst_cmd_Call:
  "labels prog l c; prog  Label l -CEdge (p,es,rets)p n' 
   p es rets. fst_cmd c = Call p es rets"
proof(induct arbitrary:n' rule:labels.induct)
  case (Labels_Base c n')
  from c  Label 0 -CEdge (p, es, rets)p n' show ?case
    by(induct c "Label 0" "CEdge (p, es, rets)" n' rule:Proc_CFG.induct) auto
next
  case (Labels_LAss V e n')
  from V:=e  Label 1 -CEdge (p, es, rets)p n' show ?case
    by(fastforce elim:Proc_CFG.cases)
next
  case (Labels_Seq1 c1 l c c2)
  note IH = n'. c1  Label l -CEdge (p, es, rets)p n' 
     p es rets. fst_cmd c = Call p es rets
  from c1;; c2  Label l -CEdge (p, es, rets)p n' labels c1 l c
  have "c1  Label l -CEdge (p, es, rets)p n'"
    apply - apply(erule Proc_CFG.cases,auto dest:Proc_CFG_Call_Labels)
    by(case_tac n)(auto dest:label_less_num_inner_nodes)
  from IH[OF this] show ?case by simp
next
  case (Labels_Seq2 c2 l c c1)
  note IH = n'. c2  Label l -CEdge (p, es, rets)p n'
     p es rets. fst_cmd c = Call p es rets
  from c1;; c2  Label (l + #:c1) -CEdge (p, es, rets)p n' labels c2 l c
  obtain nx where "c2  Label l -CEdge (p, es, rets)p nx"
    apply - apply(erule Proc_CFG.cases)
    apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes Proc_CFG_Call_Labels)
    by(case_tac n) auto
  from IH[OF this] show ?case by simp
next
  case (Labels_CondTrue c1 l c b c2)
  note IH = n'. c1  Label l -CEdge (p, es, rets)p n' 
     p es rets. fst_cmd c = Call p es rets
  from if (b) c1 else c2  Label (l + 1) -CEdge (p, es, rets)p n' labels c1 l c
  obtain nx where "c1  Label l -CEdge (p, es, rets)p nx"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(case_tac n) apply auto
    by(case_tac n)(auto dest:label_less_num_inner_nodes)
  from IH[OF this] show ?case by simp
next
  case (Labels_CondFalse c2 l c b c1)
  note IH = n'. c2  Label l -CEdge (p, es, rets)p n' 
     p es rets. fst_cmd c = Call p es rets
  from if (b) c1 else c2  Label  (l + #:c1 + 1)-CEdge (p, es, rets)p n' 
    labels c2 l c
  obtain nx where "c2  Label l -CEdge (p, es, rets)p nx"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(case_tac n) apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
    by(case_tac n) auto
  from IH[OF this] show ?case by simp
next
  case (Labels_WhileBody c' l c b)
  note IH = n'. c'  Label l -CEdge (p, es, rets)p n' 
     p es rets. fst_cmd c = Call p es rets
  from while (b) c'  Label (l + 2) -CEdge (p, es, rets)p n' labels c' l c
  obtain nx where "c'  Label l -CEdge (p, es, rets)p nx"
    apply - apply(erule Proc_CFG.cases,auto dest:Proc_CFG_Call_Labels)
    by(case_tac n) auto
  from IH[OF this] show ?case by simp
next
  case (Labels_WhileExit b c' n')
  have "while (b) c'  Label 1 -IEdge idp Exit" by(rule Proc_CFG_WhileFalseSkip)
  with while (b) c'  Label 1 -CEdge (p, es, rets)p n'
  have False by(rule Proc_CFG_Call_Intra_edge_not_same_source)
  thus ?case by simp
next
  case (Labels_Call px esx retsx)
  from Call px esx retsx  Label 1 -CEdge (p, es, rets)p n'
  show ?case by(fastforce elim:Proc_CFG.cases)
qed


subsection ‹Definition of Def› and Use› sets›

subsubsection ParamDefs›

lemma PCFG_CallEdge_THE_rets:
  "prog  n -CEdge (p,es,rets)p n'
 (THE rets'. p' es' n. prog  n -CEdge(p',es',rets')p n') = rets"
by(fastforce intro:the_equality dest:Proc_CFG_Call_nodes_eq')


definition ParamDefs_proc :: "cmd  label  vname list"
  where "ParamDefs_proc c n  
  if (n' p' es' rets'. c  n' -CEdge(p',es',rets')p n) then 
     (THE rets'. p' es' n'. c  n' -CEdge(p',es',rets')p n)
  else []"


lemma in_procs_THE_in_procs_cmd:
  "well_formed procs; (p,ins,outs,c)  set procs
   (THE c'. ins' outs'. (p,ins',outs',c')  set procs) = c"
  by(fastforce intro:the_equality)


definition ParamDefs :: "wf_prog  node  vname list"
  where "ParamDefs wfp n  let (prog,procs) = Rep_wf_prog wfp; (p,l) = n in
  (if (p = Main) then ParamDefs_proc prog l
   else (if (ins outs c. (p,ins,outs,c)  set procs)
         then ParamDefs_proc (THE c'. ins' outs'. (p,ins',outs',c')  set procs) l
         else []))"


lemma ParamDefs_Main_Return_target:
  "Rep_wf_prog wfp = (prog,procs); prog  n -CEdge(p',es,rets)p n'
   ParamDefs wfp (Main,n') = rets"
  by(fastforce dest:PCFG_CallEdge_THE_rets simp:ParamDefs_def ParamDefs_proc_def)

lemma ParamDefs_Proc_Return_target:
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c)  set procs" and "c  n -CEdge(p',es,rets)p n'"
  shows "ParamDefs wfp (p,n') = rets"
proof -
  from Rep_wf_prog wfp = (prog,procs) have "well_formed procs" 
    by(fastforce intro:wf_wf_prog)
  with (p,ins,outs,c)  set procs have "p  Main" by fastforce
  moreover
  from well_formed procs (p,ins,outs,c)  set procs
  have "(THE c'. ins' outs'. (p,ins',outs',c')  set procs) = c"
    by(rule in_procs_THE_in_procs_cmd)
  ultimately show ?thesis using assms
    by(fastforce dest:PCFG_CallEdge_THE_rets simp:ParamDefs_def ParamDefs_proc_def)
qed

lemma ParamDefs_Main_IEdge_Nil:
  "Rep_wf_prog wfp = (prog,procs); prog  n -IEdge etp n'
   ParamDefs wfp (Main,n') = []"
by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_target 
            simp:ParamDefs_def ParamDefs_proc_def)

lemma ParamDefs_Proc_IEdge_Nil:
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c)  set procs" and "c  n -IEdge etp n'"
  shows "ParamDefs wfp (p,n') = []"
proof -
  from Rep_wf_prog wfp = (prog,procs) have "well_formed procs" 
    by(fastforce intro:wf_wf_prog)
  with (p,ins,outs,c)  set procs have "p  Main" by fastforce  
  moreover
  from well_formed procs (p,ins,outs,c)  set procs
  have "(THE c'. ins' outs'. (p,ins',outs',c')  set procs) = c"
    by(rule in_procs_THE_in_procs_cmd)
  ultimately show ?thesis using assms
    by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_target 
                simp:ParamDefs_def ParamDefs_proc_def)
qed

lemma ParamDefs_Main_CEdge_Nil:
  "Rep_wf_prog wfp = (prog,procs); prog  n' -CEdge(p',es,rets)p n''
   ParamDefs wfp (Main,n') = []"
by(fastforce dest:Proc_CFG_Call_targetnode_no_Call_sourcenode
            simp:ParamDefs_def ParamDefs_proc_def)

lemma ParamDefs_Proc_CEdge_Nil:
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c)  set procs" and "c  n' -CEdge(p',es,rets)p n''"
  shows "ParamDefs wfp (p,n') = []"
proof -
  from Rep_wf_prog wfp = (prog,procs) have "well_formed procs" 
    by(fastforce intro:wf_wf_prog)
  with (p,ins,outs,c)  set procs have "p  Main" by fastforce  
  moreover
  from well_formed procs (p,ins,outs,c)  set procs
  have "(THE c'. ins' outs'. (p,ins',outs',c')  set procs) = c"
    by(rule in_procs_THE_in_procs_cmd)
  ultimately show ?thesis using assms
    by(fastforce dest:Proc_CFG_Call_targetnode_no_Call_sourcenode
                simp:ParamDefs_def ParamDefs_proc_def)
qed


lemma assumes "valid_edge wfp a" and "kind a = Q'↩⇘pf'"
  and "(p, ins, outs)  set (lift_procs wfp)"
  shows ParamDefs_length:"length (ParamDefs wfp (targetnode a)) = length outs"
  (is ?length)
  and Return_update:"f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)"
  (is ?update)
proof -
  from Rep_wf_prog[of wfp]
  obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)" 
    by(fastforce simp:wf_prog_def)
  hence "wf prog procs" by(rule wf_wf_prog)
  hence wf:"well_formed procs" by fastforce
  from assms have "prog,procs  sourcenode a -kind a targetnode a"
    by(simp add:valid_edge_def)
  from this kind a = Q'↩⇘pf' wf have "?length  ?update"
  proof(induct "sourcenode a" "kind a" "targetnode a" rule:PCFG.induct)
    case (MainReturn l p' es rets l' insx outsx cx)
    from λcf. snd cf = (Main, Label l')↩⇘p'λcf cf'. cf'(rets [:=] map cf outsx) =
      kind a kind a = Q'↩⇘pf' have "p' = p" 
      and f':"f' = (λcf cf'. cf'(rets [:=] map cf outsx))" by simp_all
    with well_formed procs (p', insx, outsx, cx)  set procs
      (p, ins, outs)  set (lift_procs wfp)
    have [simp]:"outsx = outs" by fastforce
    from prog  Label l -CEdge (p', es, rets)p Label l'
    have "containsCall procs prog [] p'" by(rule Proc_CFG_Call_containsCall)
    with wf prog procs (p', insx, outsx, cx)  set procs 
      prog  Label l -CEdge (p', es, rets)p Label l'
    have "length rets = length outs" by fastforce
    from prog  Label l -CEdge (p', es, rets)p Label l'
    have "ParamDefs wfp (Main,Label l') = rets"
      by(fastforce intro:ParamDefs_Main_Return_target)
    with (Main, Label l') = targetnode a f' length rets = length outs
    show ?thesis by simp
  next
    case (ProcReturn px insx outsx cx l p' es rets l' ins' outs' c' ps)
    from λcf. snd cf = (px, Label l')↩⇘p'λcf cf'. cf'(rets [:=] map cf outs') =
      kind a kind a = Q'↩⇘pf'
    have "p' = p" and f':"f' = (λcf cf'. cf'(rets [:=] map cf outs'))"
      by simp_all
    with well_formed procs (p', ins', outs', c')  set procs
      (p, ins, outs)  set (lift_procs wfp)
    have [simp]:"outs' = outs" by fastforce
    from cx  Label l -CEdge (p', es, rets)p Label l'
    have "containsCall procs cx [] p'" by(rule Proc_CFG_Call_containsCall)
    with containsCall procs prog ps px (px, insx, outsx, cx)  set procs
    have "containsCall procs prog (ps@[px]) p'" by(rule containsCall_in_proc)
    with wf prog procs (p', ins', outs', c')  set procs
      cx  Label l -CEdge (p', es, rets)p Label l'
    have "length rets = length outs" by fastforce
    from (px, insx, outsx, cx)  set procs
      cx  Label l -CEdge (p', es, rets)p Label l'
    have "ParamDefs wfp (px,Label l') = rets"
      by(fastforce intro:ParamDefs_Proc_Return_target simp:set_conv_nth)
    with (px, Label l') = targetnode a f' length rets = length outs
    show ?thesis by simp
  qed auto
  thus "?length" and "?update" by simp_all
qed


subsubsection ParamUses›

fun fv :: "expr  vname set"
where
  "fv (Val v)       = {}"
  | "fv (Var V)       = {V}"
  | "fv (e1 «bop» e2) = (fv e1  fv e2)"


lemma rhs_interpret_eq: 
  "state_check cf e v'; V  fv e. cf V = cf' V 
    state_check cf' e v'"
proof(induct e arbitrary:v')
  case (Val v)
  from state_check cf (Val v) v' have "v' = Some v" 
    by(fastforce elim:interpret.cases)
  thus ?case by simp
next
  case (Var V)
  hence "cf' (V) = v'" by(fastforce elim:interpret.cases)
  thus ?case by simp
next
  case (BinOp b1 bop b2)
  note IH1 = v'. state_check cf b1 v'; Vfv b1. cf V = cf' V
     state_check cf' b1 v'
  note IH2 = v'. state_check cf b2 v'; Vfv b2. cf V = cf' V
     state_check cf' b2 v'
  from V  fv (b1 «bop» b2). cf V = cf' V have "V  fv b1. cf V = cf' V"
    and "V  fv b2. cf V = cf' V" by simp_all
  from state_check cf (b1 «bop» b2) v'
  have "((state_check cf b1 None  v' = None)  
          (state_check cf b2 None  v' = None)) 
    (v1 v2. state_check cf b1 (Some v1)  state_check cf b2 (Some v2) 
    binop bop v1 v2 = v')"
    apply(cases "interpret b1 cf",simp)
    apply(cases "interpret b2 cf",simp)
    by(case_tac "binop bop a aa",simp+)
  thus ?case apply - 
  proof(erule disjE)+
    assume "state_check cf b1 None  v' = None"
    hence check:"state_check cf b1 None" and "v' = None" by simp_all
    from IH1[OF check V  fv b1. cf V = cf' V] have "state_check cf' b1 None" .
    with v' = None show ?case by simp
  next
    assume "state_check cf b2 None  v' = None"
    hence check:"state_check cf b2 None" and "v' = None" by simp_all
    from IH2[OF check V  fv b2. cf V = cf' V] have "state_check cf' b2 None" .
    with v' = None show ?case by(cases "interpret b1 cf'") simp+
  next
    assume "v1 v2. state_check cf b1 (Some v1) 
      state_check cf b2 (Some v2)  binop bop v1 v2 = v'"
    then obtain v1 v2 where "state_check cf b1 (Some v1)"
      and "state_check cf b2 (Some v2)" and "binop bop v1 v2 = v'" by blast
    from V  fv (b1 «bop» b2). cf V = cf' V have "V  fv b1. cf V = cf' V"
      by simp
    from IH1[OF state_check cf b1 (Some v1) this]
    have "interpret b1 cf' = Some v1" .
    from V  fv (b1 «bop» b2). cf V = cf' V have "V  fv b2. cf V = cf' V"
      by simp
    from IH2[OF state_check cf b2 (Some v2) this] 
    have "interpret b2 cf' = Some v2" .
    with interpret b1 cf' = Some v1 binop bop v1 v2 = v'
    show ?thesis by(cases v') simp+
  qed
qed



lemma PCFG_CallEdge_THE_es:
  "prog  n -CEdge(p,es,rets)p n'
 (THE es'. p' rets' n'. prog  n -CEdge(p',es',rets')p n') = es"
by(fastforce intro:the_equality dest:Proc_CFG_Call_nodes_eq)


definition ParamUses_proc :: "cmd  label  vname set list"
  where "ParamUses_proc c n 
  if (n' p' es' rets'. c  n -CEdge(p',es',rets')p n') then 
  (map fv (THE es'. p' rets' n'. c  n -CEdge(p',es',rets')p n'))
  else []"


definition ParamUses :: "wf_prog  node  vname set list"
  where "ParamUses wfp n  let (prog,procs) = Rep_wf_prog wfp; (p,l) = n in
  (if (p = Main) then ParamUses_proc prog l
   else (if (ins outs c. (p,ins,outs,c)  set procs)
         then ParamUses_proc (THE c'. ins' outs'. (p,ins',outs',c')  set procs) l
         else []))"


lemma ParamUses_Main_Return_target:
  "Rep_wf_prog wfp = (prog,procs); prog  n -CEdge(p',es,rets)p n' 
   ParamUses wfp (Main,n) = map fv es"
  by(fastforce dest:PCFG_CallEdge_THE_es simp:ParamUses_def ParamUses_proc_def)

lemma ParamUses_Proc_Return_target:
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c)  set procs" and "c  n -CEdge(p',es,rets)p n'"
  shows "ParamUses wfp (p,n) = map fv es"
proof -
  from Rep_wf_prog wfp = (prog,procs) have "well_formed procs" 
    by(fastforce intro:wf_wf_prog)
  with (p,ins,outs,c)  set procs have "p  Main" by fastforce  
  moreover
  from well_formed procs (p,ins,outs,c)  set procs
  have "(THE c'. ins' outs'. (p,ins',outs',c')  set procs) = c"
    by(rule in_procs_THE_in_procs_cmd)
  ultimately show ?thesis using assms
    by(fastforce dest:PCFG_CallEdge_THE_es simp:ParamUses_def ParamUses_proc_def)
qed

lemma ParamUses_Main_IEdge_Nil:
  "Rep_wf_prog wfp = (prog,procs); prog  n -IEdge etp n'
   ParamUses wfp (Main,n) = []"
by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_source
            simp:ParamUses_def ParamUses_proc_def)

lemma ParamUses_Proc_IEdge_Nil:
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c)  set procs" and "c  n -IEdge etp n'"
  shows "ParamUses wfp (p,n) = []"
proof -
  from Rep_wf_prog wfp = (prog,procs) have "well_formed procs" 
    by(fastforce intro:wf_wf_prog)
  with (p,ins,outs,c)  set procs have "p  Main" by fastforce  
  moreover
  from well_formed procs (p,ins,outs,c)  set procs
  have "(THE c'. ins' outs'. (p,ins',outs',c')  set procs) = c"
    by(rule in_procs_THE_in_procs_cmd)
  ultimately show ?thesis using assms
    by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_source
                simp:ParamUses_def ParamUses_proc_def)
qed

lemma ParamUses_Main_CEdge_Nil:
  "Rep_wf_prog wfp = (prog,procs); prog  n' -CEdge(p',es,rets)p n
   ParamUses wfp (Main,n) = []"
by(fastforce dest:Proc_CFG_Call_targetnode_no_Call_sourcenode
            simp:ParamUses_def ParamUses_proc_def)

lemma ParamUses_Proc_CEdge_Nil:
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c)  set procs" and "c  n' -CEdge(p',es,rets)p n"
  shows "ParamUses wfp (p,n) = []"
proof -
  from Rep_wf_prog wfp = (prog,procs) have "well_formed procs" 
    by(fastforce intro:wf_wf_prog)
  with (p,ins,outs,c)  set procs have "p  Main" by fastforce  
  moreover
  from well_formed procs 
    (p,ins,outs,c)  set procs
  have "(THE c'. ins' outs'. (p,ins',outs',c')  set procs) = c"
    by(rule in_procs_THE_in_procs_cmd)
  ultimately show ?thesis using assms
    by(fastforce dest:Proc_CFG_Call_targetnode_no_Call_sourcenode
                simp:ParamUses_def ParamUses_proc_def)
qed


subsubsection Def›

fun lhs :: "cmd  vname set"
where
  "lhs Skip                = {}"
  | "lhs (V:=e)              = {V}"
  | "lhs (c1;;c2)            = lhs c1"
  | "lhs (if (b) c1 else c2) = {}"
  | "lhs (while (b) c)       = {}"
  | "lhs (Call p es rets)    = {}"

lemma lhs_fst_cmd:"lhs (fst_cmd c) = lhs c" by(induct c) auto

lemma Proc_CFG_Call_source_empty_lhs:
  assumes "prog  Label l -CEdge (p,es,rets)p n'"
  shows "lhs (label prog l) = {}"
proof -
  from prog  Label l -CEdge (p,es,rets)p n' have "l < #:prog"
    by(rule Proc_CFG_sourcelabel_less_num_nodes)
  then obtain c' where "labels prog l c'"
    by(erule less_num_inner_nodes_label)
  hence "label prog l = c'" by(rule labels_label)
  from labels prog l c' prog  Label l -CEdge (p,es,rets)p n'
  have "p es rets. fst_cmd c' = Call p es rets" 
    by(rule Proc_CFG_Call_source_fst_cmd_Call)
  with lhs_fst_cmd[of c'] have "lhs c' = {}" by auto
  with label prog l = c' show ?thesis by simp
qed


lemma in_procs_THE_in_procs_ins:
  "well_formed procs; (p,ins,outs,c)  set procs
   (THE ins'. c' outs'. (p,ins',outs',c')  set procs) = ins"
  by(fastforce intro:the_equality)


definition Def :: "wf_prog  node  vname set"
  where "Def wfp n  (let (prog,procs) = Rep_wf_prog wfp; (p,l) = n in
  (case l of Label lx  
    (if p = Main then lhs (label prog lx)
     else (if (ins outs c. (p,ins,outs,c)  set procs)
           then 
  lhs (label (THE c'. ins' outs'. (p,ins',outs',c')  set procs) lx)
           else {}))
  | Entry  if (ins outs c. (p,ins,outs,c)  set procs)
            then (set 
      (THE ins'. c' outs'. (p,ins',outs',c')  set procs)) else {}
  | Exit  {}))
     set (ParamDefs wfp n)"

lemma Entry_Def_empty:"Def wfp (Main, Entry) = {}"
proof -
  obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
    by(cases "Rep_wf_prog wfp") auto
  hence "well_formed procs" by(fastforce intro:wf_wf_prog)
  thus ?thesis by(auto simp:Def_def ParamDefs_def ParamDefs_proc_def)
qed


lemma Exit_Def_empty:"Def wfp (Main, Exit) = {}"
  proof -
  obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
    by(cases "Rep_wf_prog wfp") auto
  hence "well_formed procs" by(fastforce intro:wf_wf_prog)
  thus ?thesis 
    by(auto dest:Proc_CFG_Call_Labels simp:Def_def ParamDefs_def ParamDefs_proc_def)
qed



subsubsection Use›

fun rhs :: "cmd  vname set"
where
  "rhs Skip                = {}"
  | "rhs (V:=e)              = fv e"
  | "rhs (c1;;c2)            = rhs c1"
  | "rhs (if (b) c1 else c2) = fv b"
  | "rhs (while (b) c)       = fv b"
  | "rhs (Call p es rets)    = {}"

lemma rhs_fst_cmd:"rhs (fst_cmd c) = rhs c" by(induct c) auto

lemma Proc_CFG_Call_target_empty_rhs:
  assumes "prog  n -CEdge (p,es,rets)p Label l'"
  shows "rhs (label prog l') = {}"
proof -
  from prog  n -CEdge (p,es,rets)p Label l' have "l' < #:prog"
    by(rule Proc_CFG_targetlabel_less_num_nodes)
  then obtain c' where "labels prog l' c'"
    by(erule less_num_inner_nodes_label)
  hence "label prog l' = c'" by(rule labels_label)
  from labels prog l' c' prog  n -CEdge (p,es,rets)p Label l'
  have "fst_cmd c' = Skip" by(rule Proc_CFG_Call_target_fst_cmd_Skip)
  with rhs_fst_cmd[of c'] have "rhs c' = {}" by simp
  with label prog l' = c' show ?thesis by simp
qed



lemma in_procs_THE_in_procs_outs:
  "well_formed procs; (p,ins,outs,c)  set procs
   (THE outs'. c' ins'. (p,ins',outs',c')  set procs) = outs"
  by(fastforce intro:the_equality)


definition Use :: "wf_prog  node  vname set"
  where "Use wfp n  (let (prog,procs) = Rep_wf_prog wfp; (p,l) = n in
  (case l of Label lx  
    (if p = Main then rhs (label prog lx) 
     else (if (ins outs c. (p,ins,outs,c)  set procs)
           then 
  rhs (label (THE c'. ins' outs'. (p,ins',outs',c')  set procs) lx)
           else {}))
  | Exit  if (ins outs c. (p,ins,outs,c)  set procs)
            then (set (THE outs'. c' ins'. (p,ins',outs',c')  set procs) )
            else {}
  | Entry  if (ins outs c. (p,ins,outs,c)  set procs)
      then (set (THE ins'. c' outs'. (p,ins',outs',c')  set procs))
      else {}))
   Union (set (ParamUses wfp n))  set (ParamDefs wfp n)"


lemma Entry_Use_empty:"Use wfp (Main, Entry) = {}"
proof -
  obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
    by(cases "Rep_wf_prog wfp") auto
  hence "well_formed procs" by(fastforce intro:wf_wf_prog)
  thus ?thesis by(auto dest:Proc_CFG_Call_Labels 
    simp:Use_def ParamUses_def ParamUses_proc_def ParamDefs_def ParamDefs_proc_def)
qed

lemma Exit_Use_empty:"Use wfp (Main, Exit) = {}"
proof -
  obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
    by(cases "Rep_wf_prog wfp") auto
  hence "well_formed procs" by(fastforce intro:wf_wf_prog)
  thus ?thesis by(auto dest:Proc_CFG_Call_Labels 
    simp:Use_def ParamUses_def ParamUses_proc_def ParamDefs_def ParamDefs_proc_def)
qed


subsection ‹Lemmas about edges and call frames›

lemmas transfers_simps = ProcCFG.transfer.simps[simplified]
declare transfers_simps [simp]

abbreviation state_val :: "(('var  'val) × 'ret) list  'var  'val"
  where "state_val s V  (fst (hd s)) V"

lemma Proc_CFG_edge_no_lhs_equal:
  assumes "prog  Label l -IEdge etp n'" and "V  lhs (label prog l)"
  shows "state_val (CFG.transfer (lift_procs wfp) et (cf#cfs)) V = fst cf V"
proof -
  from prog  Label l -IEdge etp n' 
  obtain x where "IEdge et = x" and "prog  Label l -xp n'" by simp_all
  from prog  Label l -xp n' IEdge et = x V  lhs (label prog l)
  show ?thesis
  proof(induct prog "Label l" x n' arbitrary:l rule:Proc_CFG.induct)
    case (Proc_CFG_LAss V' e)
    have "labels (V':=e) 0 (V':=e)" by(rule Labels_Base)
    hence "label (V':=e) 0 = (V':=e)" by(rule labels_label)
    have "V'  lhs (V':=e)" by simp
    with V  lhs (label (V':=e) 0)
      IEdge et = IEdge λcf. update cf V' e label (V':=e) 0 = (V':=e)
    show ?case by fastforce
  next
    case (Proc_CFG_SeqFirst c1 et' n' c2)
    note IH = IEdge et = et'; V  lhs (label c1 l)
       state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V
    from c1  Label l -et'p n' have "l < #:c1"
      by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c1 l c'" by(erule less_num_inner_nodes_label)
    hence "labels (c1;;c2) l (c';;c2)" by(rule Labels_Seq1)
    hence "label (c1;;c2) l = c';;c2" by(rule labels_label)
    with V  lhs (label (c1;; c2) l) labels c1 l c' 
    have "V  lhs (label c1 l)" by(fastforce dest:labels_label)
    with IEdge et = et' show ?case by (rule IH)
  next
    case (Proc_CFG_SeqConnect c1 et' c2)
    note IH = IEdge et = et'; V  lhs (label c1 l)
       state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V
    from c1  Label l -et'p Exit have "l < #:c1"
      by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c1 l c'" by(erule less_num_inner_nodes_label)
    hence "labels (c1;;c2) l (c';;c2)" by(rule Labels_Seq1)
    hence "label (c1;;c2) l = c';;c2" by(rule labels_label)
    with V  lhs (label (c1;; c2) l) labels c1 l c' 
    have "V  lhs (label c1 l)" by(fastforce dest:labels_label)
    with IEdge et = et' show ?case by (rule IH)
  next
    case (Proc_CFG_SeqSecond c2 n et' n' c1 l)
    note IH = l. n = Label l; IEdge et = et'; V  lhs (label c2 l)
       state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V
    from n  #:c1 = Label l obtain l' 
      where "n = Label l'" and "l = l' + #:c1" by(cases n) auto
    from n = Label l' c2  n -et'p n' have "l' < #:c2"
      by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c2 l' c'" by(erule less_num_inner_nodes_label)
    with l = l' + #:c1 have "labels (c1;;c2) l c'" 
      by(fastforce intro:Labels_Seq2)
    hence "label (c1;;c2) l = c'" by(rule labels_label)
    with V  lhs (label (c1;;c2) l) labels c2 l' c' l = l' + #:c1
    have "V  lhs (label c2 l')" by(fastforce dest:labels_label)
    with n = Label l' IEdge et = et' show ?case by (rule IH)
  next
    case (Proc_CFG_CondThen c1 n et' n' b c2 l)
    note IH = l. n = Label l; IEdge et = et'; V  lhs (label c1 l)
       state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V
    from n  1 = Label l obtain l' 
      where "n = Label l'" and "l = l' + 1" by(cases n) auto
    from n = Label l' c1  n -et'p n' have "l' < #:c1"
      by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c1 l' c'" by(erule less_num_inner_nodes_label)
    with l = l' + 1 have "labels (if (b) c1 else c2) l c'" 
      by(fastforce intro:Labels_CondTrue)
    hence "label (if (b) c1 else c2) l = c'" by(rule labels_label)
    with V  lhs (label (if (b) c1 else c2) l) labels c1 l' c' l = l' + 1
    have "V  lhs (label c1 l')" by(fastforce dest:labels_label)
    with n = Label l' IEdge et = et' show ?case by (rule IH)
  next
    case (Proc_CFG_CondElse c2 n et' n' b c1 l)
    note IH = l. n = Label l; IEdge et = et'; V  lhs (label c2 l)
       state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V
    from n  #:c1 + 1 = Label l obtain l' 
      where "n = Label l'" and "l = l' + #:c1 + 1" by(cases n) auto
    from n = Label l' c2  n -et'p n' have "l' < #:c2"
      by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c2 l' c'" by(erule less_num_inner_nodes_label)
    with l = l' + #:c1 + 1 have "labels (if (b) c1 else c2) l c'" 
      by(fastforce intro:Labels_CondFalse)
    hence "label (if (b) c1 else c2) l = c'" by(rule labels_label)
    with V  lhs (label (if (b) c1 else c2) l) labels c2 l' c' l = l' + #:c1 + 1
    have "V  lhs (label c2 l')" by(fastforce dest:labels_label)
    with n = Label l' IEdge et = et' show ?case by (rule IH)
  next
    case (Proc_CFG_WhileBody c' n et' n' b l)
    note IH = l. n = Label l; IEdge et = et'; V  lhs (label c' l)
       state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V
    from n  2 = Label l obtain l' 
      where "n = Label l'" and "l = l' + 2" by(cases n) auto
    from n = Label l' c'  n -et'p n' have "l' < #:c'"
      by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
    with l = l' + 2 have "labels (while (b) c') l (cx;;while (b) c')" 
      by(fastforce intro:Labels_WhileBody)
    hence "label (while (b) c') l = cx;;while (b) c'" by(rule labels_label)
    with V  lhs (label (while (b) c') l) labels c' l' cx l = l' + 2
    have "V  lhs (label c' l')" by(fastforce dest:labels_label)
    with n = Label l' IEdge et = et' show ?case by (rule IH)
  next
    case (Proc_CFG_WhileBodyExit c' n et' b l)
    note IH = l. n = Label l; IEdge et = et'; V  lhs (label c' l)
       state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V
    from n  2 = Label l obtain l' 
      where "n = Label l'" and "l = l' + 2" by(cases n) auto
    from n = Label l' c'  n -et'p Exit have "l' < #:c'"
      by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
    with l = l' + 2 have "labels (while (b) c') l (cx;;while (b) c')" 
      by(fastforce intro:Labels_WhileBody)
    hence "label (while (b) c') l = cx;;while (b) c'" by(rule labels_label)
    with V  lhs (label (while (b) c') l) labels c' l' cx l = l' + 2
    have "V  lhs (label c' l')" by(fastforce dest:labels_label)
    with n = Label l' IEdge et = et' show ?case by (rule IH)
  qed auto
qed



lemma Proc_CFG_edge_uses_only_rhs:
  assumes "prog  Label l -IEdge etp n'" and "CFG.pred et s"
  and "CFG.pred et s'" and "Vrhs (label prog l). state_val s V = state_val s' V"
  shows "Vlhs (label prog l). 
    state_val (CFG.transfer (lift_procs wfp) et s) V =
    state_val (CFG.transfer (lift_procs wfp) et s') V"
proof -
  from prog  Label l -IEdge etp n' 
  obtain x where "IEdge et = x" and "prog  Label l -xp n'" by simp_all
  from CFG.pred et s obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
  from CFG.pred et s' obtain cf' cfs' where [simp]:"s' = cf'#cfs'" 
    by(cases s') auto
  from prog  Label l -xp n' IEdge et = x
    Vrhs (label prog l). state_val s V = state_val s' V
  show ?thesis
  proof(induct prog "Label l" x n' arbitrary:l rule:Proc_CFG.induct)
    case Proc_CFG_Skip
    have "labels Skip 0 Skip" by(rule Labels_Base)
    hence "label Skip 0 = Skip" by(rule labels_label)
    hence "V. V  lhs (label Skip 0)" by simp
    then show ?case by fastforce
  next
    case (Proc_CFG_LAss V e)
    have "labels (V:=e) 0 (V:=e)" by(rule Labels_Base)
    hence "label (V:=e) 0 = V:=e" by(rule labels_label)
    then have "lhs (label (V:=e) 0) = {V}"
      and "rhs (label (V:=e) 0) = fv e" by auto
    with IEdge et = IEdge λcf. update cf V e 
      Vrhs (label (V:=e) 0). state_val s V = state_val s' V
    show ?case by(fastforce intro:rhs_interpret_eq)
  next
    case (Proc_CFG_LAssSkip V e)
    have "labels (V:=e) 1 Skip" by(rule Labels_LAss)
    hence "label (V:=e) 1 = Skip" by(rule labels_label)
    hence "V'. V'  lhs (label (V:=e) 1)" by simp
    then show ?case by fastforce
  next
    case (Proc_CFG_SeqFirst c1 et' n' c2)
    note IH = IEdge et = et'; 
      Vrhs (label c1 l). state_val s V = state_val s' V
       Vlhs (label c1 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
        state_val (CFG.transfer (lift_procs wfp) et s') V
    from c1  Label l -et'p n'
    have "l < #:c1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c1 l c'" by(erule less_num_inner_nodes_label)
    hence "labels (c1;;c2) l (c';;c2)" by(rule Labels_Seq1)
    with labels c1 l c' Vrhs (label (c1;; c2) l). state_val s V = state_val s' V
    have "Vrhs (label c1 l). state_val s V = state_val s' V"
      by(fastforce dest:labels_label)
    with IEdge et = et'
    have "Vlhs (label c1 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
      state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
    with labels c1 l c' labels (c1;;c2) l (c';;c2)
    show ?case by(fastforce dest:labels_label)
  next
    case (Proc_CFG_SeqConnect c1 et' c2)
    note IH = IEdge et = et'; 
      Vrhs (label c1 l). state_val s V = state_val s' V
       Vlhs (label c1 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
        state_val (CFG.transfer (lift_procs wfp) et s') V
    from c1  Label l -et'p Exit
    have "l < #:c1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c1 l c'" by(erule less_num_inner_nodes_label)
    hence "labels (c1;;c2) l (c';;c2)" by(rule Labels_Seq1)
    with labels c1 l c' Vrhs (label (c1;; c2) l). state_val s V = state_val s' V
    have "Vrhs (label c1 l). state_val s V = state_val s' V"
      by(fastforce dest:labels_label)
    with IEdge et = et'
    have "Vlhs (label c1 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
      state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
    with labels c1 l c' labels (c1;;c2) l (c';;c2)
    show ?case by(fastforce dest:labels_label)
  next
    case (Proc_CFG_SeqSecond c2 n et' n' c1)
    note IH = l. n = Label l; IEdge et = et'; 
      Vrhs (label c2 l). state_val s V = state_val s' V
       Vlhs (label c2 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
        state_val (CFG.transfer (lift_procs wfp) et s') V
    from n  #:c1 = Label l obtain l' where "n = Label l'" and "l = l' + #:c1"
      by(cases n) auto
    from c2  n -et'p n' n = Label l'
    have "l' < #:c2" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c2 l' c'" by(erule less_num_inner_nodes_label)
    with l = l' + #:c1 have "labels (c1;;c2) l c'" by(fastforce intro:Labels_Seq2)
    with labels c2 l' c' Vrhs (label (c1;;c2) l). state_val s V = state_val s' V
    have "Vrhs (label c2 l'). state_val s V = state_val s' V"
      by(fastforce dest:labels_label)
    with n = Label l' IEdge et = et'
    have "Vlhs (label c2 l'). state_val (CFG.transfer (lift_procs wfp) et s) V =
      state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
    with labels c2 l' c' labels (c1;;c2) l c'
    show ?case by(fastforce dest:labels_label)
  next
    case (Proc_CFG_CondTrue b c1 c2)
    have "labels (if (b) c1 else c2) 0 (if (b) c1 else c2)" by(rule Labels_Base)
    hence "label (if (b) c1 else c2) 0 = if (b) c1 else c2" by(rule labels_label)
    hence "V. V  lhs (label (if (b) c1 else c2) 0)" by simp
    then show ?case by fastforce
  next
    case (Proc_CFG_CondFalse b c1 c2)
    have "labels (if (b) c1 else c2) 0 (if (b) c1 else c2)" by(rule Labels_Base)
    hence "label (if (b) c1 else c2) 0 = if (b) c1 else c2" by(rule labels_label)
    hence "V. V  lhs (label (if (b) c1 else c2) 0)" by simp
    then show ?case by fastforce
  next
    case (Proc_CFG_CondThen c1 n et' n' b c2)
    note IH = l. n = Label l; IEdge et = et'; 
      Vrhs (label c1 l). state_val s V = state_val s' V
       Vlhs (label c1 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
        state_val (CFG.transfer (lift_procs wfp) et s') V
    from n  1 = Label l obtain l' where "n = Label l'" and "l = l' + 1"
      by(cases n) auto
    from c1  n -et'p n' n = Label l'
    have "l' < #:c1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c1 l' c'" by(erule less_num_inner_nodes_label)
    with l = l' + 1 have "labels (if (b) c1 else c2) l c'" 
      by(fastforce intro:Labels_CondTrue)
    with labels c1 l' c' Vrhs (label (if (b) c1 else c2) l). state_val s V = state_val s' V
    have "Vrhs (label c1 l'). state_val s V = state_val s' V"
      by(fastforce dest:labels_label)
    with n = Label l' IEdge et = et'
    have "Vlhs (label c1 l'). state_val (CFG.transfer (lift_procs wfp) et s) V =
      state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
    with labels c1 l' c' labels (if (b) c1 else c2) l c'
    show ?case by(fastforce dest:labels_label)
  next
    case (Proc_CFG_CondElse c2 n et' n' b c1)
    note IH = l. n = Label l; IEdge et = et';
      Vrhs (label c2 l). state_val s V = state_val s' V
       Vlhs (label c2 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
        state_val (CFG.transfer (lift_procs wfp) et s') V
    from n  #:c1 + 1= Label l obtain l' where "n = Label l'" and "l = l' + #:c1+1"
      by(cases n) auto
    from c2  n -et'p n' n = Label l'
    have "l' < #:c2" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c2 l' c'" by(erule less_num_inner_nodes_label)
    with l = l' + #:c1 + 1 have "labels (if (b) c1 else c2) l c'" 
      by(fastforce intro:Labels_CondFalse)
    with labels c2 l' c' Vrhs (label (if (b) c1 else c2) l). 
      state_val s V = state_val s' V
    have "Vrhs (label c2 l'). state_val s V = state_val s' V"
      by(fastforce dest:labels_label)
    with n = Label l' IEdge et = et'
    have "Vlhs (label c2 l'). state_val (CFG.transfer (lift_procs wfp) et s) V =
      state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
    with labels c2 l' c' labels (if (b) c1 else c2) l c'
    show ?case by(fastforce dest:labels_label)
  next
    case (Proc_CFG_WhileTrue b c')
    have "labels (while (b) c') 0 (while (b) c')" by(rule Labels_Base)
    hence "label (while (b) c') 0 = while (b) c'" by(rule labels_label)
    hence "V. V  lhs (label (while (b) c') 0)" by simp
    then show ?case by fastforce
  next
    case (Proc_CFG_WhileFalse b c')
    have "labels (while (b) c') 0 (while (b) c')" by(rule Labels_Base)
    hence "label (while (b) c') 0 = while (b) c'" by(rule labels_label)
    hence "V. V  lhs (label (while (b) c') 0)" by simp
    then show ?case by fastforce
  next
    case (Proc_CFG_WhileFalseSkip b c')
    have "labels (while (b) c') 1 Skip" by(rule Labels_WhileExit)
    hence "label (while (b) c') 1 = Skip" by(rule labels_label)
    hence "V. V  lhs (label (while (b) c') 1)" by simp
    then show ?case by fastforce
  next
    case (Proc_CFG_WhileBody c' n et' n' b)
    note IH = l. n = Label l; IEdge et = et';
      Vrhs (label c' l). state_val s V = state_val s' V
       Vlhs (label c' l). state_val (CFG.transfer (lift_procs wfp) et s) V =
        state_val (CFG.transfer (lift_procs wfp) et s') V
    from n  2 = Label l obtain l' where "n = Label l'" and "l = l' + 2"
      by(cases n) auto
    from c'  n -et'p n' n = Label l'
    have "l' < #:c'" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
    with l = l' + 2 have "labels (while (b) c') l (cx;;while (b) c')" 
      by(fastforce intro:Labels_WhileBody)
    with labels c' l' cx Vrhs (label (while (b) c') l). 
      state_val s V = state_val s' V
    have "Vrhs (label c' l'). state_val s V = state_val s' V"
      by(fastforce dest:labels_label)
    with n = Label l' IEdge et = et'
    have "Vlhs (label c' l'). state_val (CFG.transfer (lift_procs wfp) et s) V =
      state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
    with labels c' l' cx labels (while (b) c') l (cx;;while (b) c')
    show ?case by(fastforce dest:labels_label)
  next
    case (Proc_CFG_WhileBodyExit c' n et' b)
    note IH = l. n = Label l; IEdge et = et';
      Vrhs (label c' l). state_val s V = state_val s' V
       Vlhs (label c' l). state_val (CFG.transfer (lift_procs wfp) et s) V =
        state_val (CFG.transfer (lift_procs wfp) et s') V
    from n  2 = Label l obtain l' where "n = Label l'" and "l = l' + 2"
      by(cases n) auto
    from c'  n -et'p Exit n = Label l'
    have "l' < #:c'" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
    with l = l' + 2 have "labels (while (b) c') l (cx;;while (b) c')" 
      by(fastforce intro:Labels_WhileBody)
    with labels c' l' cx Vrhs (label (while (b) c') l).
      state_val s V = state_val s' V
    have "Vrhs (label c' l'). state_val s V = state_val s' V"
      by(fastforce dest:labels_label)
    with n = Label l' IEdge et = et'
    have "Vlhs (label c' l'). state_val (CFG.transfer (lift_procs wfp) et s) V =
      state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
    with labels c' l' cx labels (while (b) c') l (cx;;while (b) c')
    show ?case by(fastforce dest:labels_label)
  next
    case (Proc_CFG_CallSkip p es rets)
    have "labels (Call p es rets) 1 Skip" by(rule Labels_Call)
    hence "label (Call p es rets) 1 = Skip" by(rule labels_label)
    hence "V. V  lhs (label (Call p es rets) 1)" by simp
    then show ?case by fastforce
  qed auto
qed


lemma Proc_CFG_edge_rhs_pred_eq:
  assumes "prog  Label l -IEdge etp n'" and "CFG.pred et s"
  and "Vrhs (label prog l). state_val s V = state_val s' V"
  and "length s = length s'"
  shows "CFG.pred et s'"
proof -
  from prog  Label l -IEdge etp n' 
  obtain x where "IEdge et = x" and "prog  Label l -xp n'" by simp_all
  from CFG.pred et s obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
  from length s = length s' obtain cf' cfs' where [simp]:"s' = cf'#cfs'" 
    by(cases s') auto
  from prog  Label l -xp n' IEdge et = x 
    Vrhs (label prog l). state_val s V = state_val s' V
  show ?thesis
  proof(induct prog "Label l" x n' arbitrary:l rule:Proc_CFG.induct)
    case (Proc_CFG_SeqFirst c1 et' n' c2)
    note IH = IEdge et = et'; Vrhs (label c1 l). 
      state_val s V = state_val s' V  CFG.pred et s'
    from c1  Label l -et'p n'
    have "l < #:c1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c1 l c'" by(erule less_num_inner_nodes_label)
    hence "labels (c1;;c2) l (c';;c2)" by(rule Labels_Seq1)
    with labels c1 l c' Vrhs (label (c1;; c2) l). state_val s V = state_val s' V
    have "Vrhs (label c1 l). state_val s V = state_val s' V" 
      by(fastforce dest:labels_label)
    with IEdge et = et' show ?case by (rule IH)
  next
    case (Proc_CFG_SeqConnect c1 et' c2)
    note IH = IEdge et = et'; 
      Vrhs (label c1 l). state_val s V = state_val s' V
       CFG.pred et s'
    from c1  Label l -et'p Exit
    have "l < #:c1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c1 l c'" by(erule less_num_inner_nodes_label)
    hence "labels (c1;;c2) l (c';;c2)" by(rule Labels_Seq1)
    with labels c1 l c' Vrhs (label (c1;; c2) l). state_val s V = state_val s' V
    have "Vrhs (label c1 l). state_val s V = state_val s' V" 
      by(fastforce dest:labels_label)
    with IEdge et = et' show ?case by (rule IH)
  next
    case (Proc_CFG_SeqSecond c2 n et' n' c1)
    note IH = l. n = Label l; IEdge et = et';
      Vrhs (label c2 l). state_val s V = state_val s' V 
       CFG.pred et s'
    from n  #:c1 = Label l obtain l' where "n = Label l'" and "l = l' + #:c1"
      by(cases n) auto
    from c2  n -et'p n' n = Label l'
    have "l' < #:c2" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c2 l' c'" by(erule less_num_inner_nodes_label)
    with l = l' + #:c1 have "labels (c1;;c2) l c'" by(fastforce intro:Labels_Seq2)
    with labels c2 l' c' Vrhs (label (c1;;c2) l). state_val s V = state_val s' V
    have "Vrhs (label c2 l'). state_val s V = state_val s' V" 
      by(fastforce dest:labels_label)
    with n = Label l' IEdge et = et' show ?case by (rule IH)
  next
    case (Proc_CFG_CondTrue b c1 c2)
    from CFG.pred et s IEdge et = IEdge (λcf. state_check cf b (Some true))
    have "state_check (fst cf) b (Some true)" by simp
    moreover
    have "labels (if (b) c1 else c2) 0 (if (b) c1 else c2)" by(rule Labels_Base)
    hence "label (if (b) c1 else c2) 0 = if (b) c1 else c2" by(rule labels_label)
    with Vrhs (label (if (b) c1 else c2) 0). state_val s V = state_val s' V
    have "V fv b. state_val s V = state_val s' V" by fastforce
    ultimately have "state_check (fst cf') b (Some true)" 
      by simp(rule rhs_interpret_eq)
    with IEdge et = IEdge (λcf. state_check cf b (Some true))
    show ?case by simp
  next
    case (Proc_CFG_CondFalse b c1 c2)
    from CFG.pred et s 
      IEdge et = IEdge (λcf. state_check cf b (Some false))
    have "state_check (fst cf) b (Some false)" by simp
    moreover
    have "labels (if (b) c1 else c2) 0 (if (b) c1 else c2)" by(rule Labels_Base)
    hence "label (if (b) c1 else c2) 0 = if (b) c1 else c2" by(rule labels_label)
    with Vrhs (label (if (b) c1 else c2) 0). state_val s V = state_val s' V
    have "V fv b. state_val s V = state_val s' V" by fastforce
    ultimately have "state_check (fst cf') b (Some false)" 
      by simp(rule rhs_interpret_eq)
    with IEdge et = IEdge (λcf. state_check cf b (Some false)) 
    show ?case by simp
  next
    case (Proc_CFG_CondThen c1 n et' n' b c2)
    note IH = l. n = Label l; IEdge et = et';
      Vrhs (label c1 l). state_val s V = state_val s' V 
       CFG.pred et s'
    from n  1 = Label l obtain l' where "n = Label l'" and "l = l' + 1"
      by(cases n) auto
    from c1  n -et'p n' n = Label l'
    have "l' < #:c1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c1 l' c'" by(erule less_num_inner_nodes_label)
    with l = l' + 1 have "labels (if (b) c1 else c2) l c'" 
      by(fastforce intro:Labels_CondTrue)
    with labels c1 l' c' Vrhs (label (if (b) c1 else c2) l). 
      state_val s V = state_val s' V
    have "Vrhs (label c1 l'). state_val s V = state_val s' V"
      by(fastforce dest:labels_label)
    with n = Label l' IEdge et = et' show ?case by (rule IH)
  next
    case (Proc_CFG_CondElse c2 n et' n' b c1)
    note IH = l. n = Label l; IEdge et = et';
      Vrhs (label c2 l). state_val s V = state_val s' V 
       CFG.pred et s'
    from n  #:c1 + 1= Label l obtain l' where "n = Label l'" and "l = l' + #:c1+1"
      by(cases n) auto
    from c2  n -et'p n' n = Label l'
    have "l' < #:c2" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain c' where "labels c2 l' c'" by(erule less_num_inner_nodes_label)
    with l = l' + #:c1 + 1 have "labels (if (b) c1 else c2) l c'" 
      by(fastforce intro:Labels_CondFalse)
    with labels c2 l' c' Vrhs (label (if (b) c1 else c2) l). 
      state_val s V = state_val s' V
    have "Vrhs (label c2 l'). state_val s V = state_val s' V" 
      by(fastforce dest:labels_label)
    with n = Label l' IEdge et = et' show ?case by (rule IH)
  next
    case (Proc_CFG_WhileTrue b c')
    from CFG.pred et s IEdge et = IEdge (λcf. state_check cf b (Some true))
    have "state_check (fst cf) b (Some true)" by simp
    moreover
    have "labels (while (b) c') 0 (while (b) c')" by(rule Labels_Base)
    hence "label (while (b) c') 0 = while (b) c'" by(rule labels_label)
    with Vrhs (label (while (b) c') 0). state_val s V = state_val s' V 
    have "V fv b. state_val s V = state_val s' V" by fastforce
    ultimately have "state_check (fst cf') b (Some true)" 
      by simp(rule rhs_interpret_eq)
    with IEdge et = IEdge (λcf. state_check cf b (Some true))
    show ?case by simp
  next
    case (Proc_CFG_WhileFalse b c')
    from CFG.pred et s
      IEdge et = IEdge (λcf. state_check cf b (Some false))
    have "state_check (fst cf) b (Some false)" by simp
    moreover
    have "labels (while (b) c') 0 (while (b) c')" by(rule Labels_Base)
    hence "label (while (b) c') 0 = while (b) c'" by(rule labels_label)
    with Vrhs (label (while (b) c') 0). state_val s V = state_val s' V 
    have "V fv b. state_val s V = state_val s' V" by fastforce
    ultimately have "state_check (fst cf') b (Some false)" 
      by simp(rule rhs_interpret_eq)
    with IEdge et = IEdge (λcf. state_check cf b (Some false))
    show ?case by simp
  next
    case (Proc_CFG_WhileBody c' n et' n' b)
    note IH = l. n = Label l; IEdge et = et';
      Vrhs (label c' l). state_val s V = state_val s' V 
       CFG.pred et s'
    from n  2 = Label l obtain l' where "n = Label l'" and "l = l' + 2"
      by(cases n) auto
    from c'  n -et'p n' n = Label l'
    have "l' < #:c'" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
    with l = l' + 2 have "labels (while (b) c') l (cx;;while (b) c')" 
      by(fastforce intro:Labels_WhileBody)
    with labels c' l' cx Vrhs (label (while (b) c') l). 
      state_val s V = state_val s' V
    have "Vrhs (label c' l'). state_val s V = state_val s' V" 
      by(fastforce dest:labels_label)
    with n = Label l' IEdge et = et' show ?case by (rule IH)
  next
    case (Proc_CFG_WhileBodyExit c' n et' b)
    note IH = l. n = Label l; IEdge et = et';
      Vrhs (label c' l). state_val s V = state_val s' V 
       CFG.pred et s'
    from n  2 = Label l obtain l' where "n = Label l'" and "l = l' + 2"
      by(cases n) auto
    from c'  n -et'p Exit n = Label l'
    have "l' < #:c'" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
    then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
    with l = l' + 2 have "labels (while (b) c') l (cx;;while (b) c')" 
      by(fastforce intro:Labels_WhileBody)
    with labels c' l' cx Vrhs (label (while (b) c') l). 
      state_val s V = state_val s' V
    have "Vrhs (label c' l'). state_val s V = state_val s' V" 
      by(fastforce dest:labels_label)
    with n = Label l' IEdge et = et' show ?case by (rule