# Theory WellFormProgs

```section ‹Well-formedness of programs›

theory WellFormProgs imports PCFG begin

subsection ‹Well-formedness of procedure lists.›

definition wf_proc :: "proc ⇒ bool"
where "wf_proc x ≡ let (p,ins,outs,c) = x in
p ≠ Main ∧ distinct ins ∧ distinct outs"

definition well_formed :: "procs ⇒ bool"
where "well_formed procs ≡ distinct_fst procs ∧
(∀(p,ins,outs,c) ∈ set procs. wf_proc (p,ins,outs,c))"

lemma [dest]:"⟦well_formed procs; (Main,ins,outs,c) ∈ set procs⟧ ⟹ False"
by(fastforce simp:well_formed_def wf_proc_def)

lemma well_formed_same_procs [dest]:
"⟦well_formed procs; (p,ins,outs,c) ∈ set procs; (p,ins',outs',c') ∈ set procs⟧
⟹ ins = ins' ∧ outs = outs' ∧ c = c'"
apply(auto simp:well_formed_def distinct_fst_def distinct_map inj_on_def)
by(erule_tac x="(p,ins,outs,c)" in ballE,auto)+

lemma PCFG_sourcelabel_None_less_num_nodes:
"⟦prog,procs ⊢ (Main,Label l) -et→ n'; well_formed procs⟧ ⟹ l < #:prog"
proof(induct "(Main,Label l)" et n'
arbitrary:l rule:PCFG.induct)
case (Main et n')
from ‹prog ⊢ Label l -IEdge et→⇩p n'›
show ?case by(fastforce elim:Proc_CFG_sourcelabel_less_num_nodes)
next
case (MainCall l p es rets n' ins outs c)
from ‹prog ⊢ Label l -CEdge (p,es,rets)→⇩p n'›
show ?case by(fastforce elim:Proc_CFG_sourcelabel_less_num_nodes)
next
case (MainCallReturn p es rets n' l)
from ‹prog ⊢ Label l -CEdge (p, es, rets)→⇩p n'›
show ?case by(fastforce elim:Proc_CFG_sourcelabel_less_num_nodes)
qed auto

lemma Proc_CFG_sourcelabel_Some_less_num_nodes:
"⟦prog,procs ⊢ (p,Label l) -et→ n'; (p,ins,outs,c) ∈ set procs;
well_formed procs⟧ ⟹ l < #:c"
proof(induct "(p,Label l)" et n' arbitrary:l rule:PCFG.induct)
case (Proc ins' outs' c' et n')
from ‹c' ⊢ Label l -IEdge et→⇩p n'› have "l < #:c'"
by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
with ‹well_formed procs› ‹(p,ins,outs,c) ∈ set procs›
‹(p,ins',outs',c') ∈ set procs›
show ?case by fastforce
next
case (ProcCall ins' outs' c' l' p' es rets l'' ins'' outs'' c'' ps)
from ‹c' ⊢ Label l' -CEdge (p',es,rets)→⇩p Label l''› have "l' < #:c'"
by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
with ‹well_formed procs› ‹(p,ins,outs,c) ∈ set procs›
‹(p, ins', outs', c') ∈ set procs›
show ?case by fastforce
next
case (ProcCallReturn ins' outs' c' p' es rets n')
from ‹c' ⊢ Label l -CEdge (p', es, rets)→⇩p n'› have "l < #:c'"
by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
with ‹well_formed procs› ‹(p,ins,outs,c) ∈ set procs›
‹(p,ins',outs',c') ∈ set procs›
show ?case by fastforce
qed auto

lemma Proc_CFG_targetlabel_Main_less_num_nodes:
"⟦prog,procs ⊢ n -et→ (Main,Label l); well_formed procs⟧ ⟹ l < #:prog"
proof(induct n et "(Main,Label l)"
arbitrary:l rule:PCFG.induct)
case (Main n et)
from ‹prog ⊢ n -IEdge et→⇩p Label l›
show ?case by(fastforce elim:Proc_CFG_targetlabel_less_num_nodes)
next
case (MainReturn l' p es rets l'' ins outs c)
from ‹prog ⊢ Label l' -CEdge (p,es,rets)→⇩p Label l''›
show ?case by(fastforce elim:Proc_CFG_targetlabel_less_num_nodes)
next
case (MainCallReturn n p es rets)
from ‹prog ⊢ n -CEdge (p, es, rets)→⇩p Label l›
show ?case by(fastforce elim:Proc_CFG_targetlabel_less_num_nodes)
qed auto

lemma Proc_CFG_targetlabel_Some_less_num_nodes:
"⟦prog,procs ⊢ n -et→ (p,Label l); (p,ins,outs,c) ∈ set procs;
well_formed procs⟧ ⟹ l < #:c"
proof(induct n et "(p,Label l)" arbitrary:l rule:PCFG.induct)
case (Proc ins' outs' c' n et)
from ‹c' ⊢ n -IEdge et→⇩p Label l› have "l < #:c'"
by(fastforce intro:Proc_CFG_targetlabel_less_num_nodes)
with ‹well_formed procs› ‹(p,ins,outs,c) ∈ set procs›
‹(p,ins',outs',c') ∈ set procs›
show ?case by fastforce
next
case (ProcReturn ins' outs' c' l' p' es rets l ins'' outs'' c'' ps)
from ‹c' ⊢ Label l' -CEdge (p',es,rets)→⇩p Label l› have "l < #:c'"
by(fastforce intro:Proc_CFG_targetlabel_less_num_nodes)
with ‹well_formed procs› ‹(p,ins,outs,c) ∈ set procs›
‹(p, ins', outs', c') ∈ set procs›
show ?case by fastforce
next
case (ProcCallReturn ins' outs' c' n p'' es rets)
from ‹c' ⊢ n -CEdge (p'', es, rets)→⇩p Label l› have "l < #:c'"
by(fastforce intro:Proc_CFG_targetlabel_less_num_nodes)
with ‹well_formed procs› ‹(p,ins,outs,c) ∈ set procs›
‹(p,ins',outs',c') ∈ set procs›
show ?case by fastforce
qed auto

lemma Proc_CFG_edge_det:
"⟦prog,procs ⊢ n -et→ n'; prog,procs ⊢ n -et'→ n'; well_formed procs⟧
⟹ et = et'"
proof(induct rule:PCFG.induct)
case Main thus ?case by(auto elim:PCFG.cases dest:Proc_CFG_edge_det)
next
case Proc thus ?case by(auto elim:PCFG.cases dest:Proc_CFG_edge_det)
next
case (MainCall l p es rets n' ins outs c)
from ‹prog,procs ⊢ (Main,Label l) -et'→ (p,Entry)› ‹well_formed procs›
obtain es' rets' n'' ins' outs' c'
where "prog ⊢ Label l -CEdge (p,es',rets')→⇩p n''"
and "(p,ins',outs',c') ∈ set procs"
and "et' = (λs. True):(Main,n'')↪⇘p⇙map (λe cf. interpret e cf) es'"
by(auto elim:PCFG.cases)
from ‹(p,ins,outs,c) ∈ set procs› ‹(p,ins',outs',c') ∈ set procs›
‹well_formed procs›
have "ins = ins'" by fastforce
from ‹prog ⊢ Label l -CEdge (p,es,rets)→⇩p n'›
‹prog ⊢ Label l -CEdge (p,es',rets')→⇩p n''›
have "es = es'" and "n' = n''" by(auto dest:Proc_CFG_Call_nodes_eq)
with ‹et' = (λs. True):(Main,n'')↪⇘p⇙map (λe cf. interpret e cf) es'› ‹ins = ins'›
show ?case by simp
next
case (ProcCall p ins outs c l p' es' rets' l' ins' outs' c' ps)
from ‹prog,procs ⊢ (p,Label l) -et'→ (p',Entry)› ‹(p',ins',outs',c') ∈ set procs›
‹(p, ins, outs, c) ∈ set procs› ‹well_formed procs›
‹c ⊢ Label l -CEdge (p', es', rets')→⇩p Label l'›
show ?case
proof(induct "(p,Label l)" et' "(p',Entry)" rule:PCFG.induct)
case (ProcCall insx outsx cx es'x rets'x l'x ins'x outs'x c'x ps)
from ‹well_formed procs› ‹(p, insx, outsx, cx) ∈ set procs›
‹(p, ins, outs, c) ∈ set procs›
have [simp]:"cx = c" by auto
from ‹cx ⊢ Label l -CEdge (p', es'x, rets'x)→⇩p Label l'x›
‹c ⊢ Label l -CEdge (p', es', rets')→⇩p Label l'›
have [simp]:"es'x = es'" "l'x = l'" by(auto dest:Proc_CFG_Call_nodes_eq)
show ?case by simp
qed auto
next
case MainReturn
thus ?case by -(erule PCFG.cases,auto dest:Proc_CFG_Call_nodes_eq')
next
case (ProcReturn p ins outs c l p' es' rets' l' ins' outs' c' ps)
from ‹prog,procs ⊢ (p',Exit) -et'→ (p, Label l')›
‹(p, ins, outs, c) ∈ set procs› ‹(p', ins', outs', c') ∈ set procs›
‹c ⊢ Label l -CEdge (p', es', rets')→⇩p Label l'›
‹containsCall procs prog ps p› ‹well_formed procs›
show ?case
proof(induct "(p',Exit)" et' "(p,Label l')" rule:PCFG.induct)
case (ProcReturn insx outsx cx lx es'x rets'x ins'x outs'x c'x psx)
from ‹(p', ins'x, outs'x, c'x) ∈ set procs›
‹(p', ins', outs', c') ∈ set procs› ‹well_formed procs›
have [simp]:"outs'x = outs'" by fastforce
from ‹(p, insx, outsx, cx) ∈ set procs› ‹(p, ins, outs, c) ∈ set procs›
‹well_formed procs›
have [simp]:"cx = c" by auto
from ‹cx ⊢ Label lx -CEdge (p', es'x, rets'x)→⇩p Label l'›
‹c ⊢ Label l -CEdge (p', es', rets')→⇩p Label l'›
have [simp]:"rets'x = rets'" by(fastforce dest:Proc_CFG_Call_nodes_eq')
show ?case by simp
qed auto
next
case MainCallReturn thus ?case by(auto elim:PCFG.cases dest:Proc_CFG_edge_det)
next
case ProcCallReturn thus ?case by(auto elim:PCFG.cases dest:Proc_CFG_edge_det)
qed

lemma Proc_CFG_deterministic:
"⟦prog,procs ⊢ n⇩1 -et⇩1→ n⇩1'; prog,procs ⊢ n⇩2 -et⇩2→ n⇩2'; n⇩1 = n⇩2; n⇩1' ≠ n⇩2';
intra_kind et⇩1; intra_kind et⇩2; well_formed procs⟧
⟹ ∃Q Q'. et⇩1 = (Q)⇩√ ∧ et⇩2 = (Q')⇩√ ∧
(∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))"
proof(induct arbitrary:n⇩2 n⇩2' rule:PCFG.induct)
case (Main n et n')
from ‹prog,procs ⊢ n⇩2 -et⇩2→ n⇩2'› ‹(Main,n) = n⇩2›
‹intra_kind et⇩2› ‹well_formed procs›
obtain m m' where "(Main,m) = n⇩2" and "(Main,m') = n⇩2'"
and disj:"prog ⊢ m -IEdge et⇩2→⇩p m' ∨
(∃p es rets. prog ⊢ m -CEdge (p,es,rets)→⇩p m' ∧ et⇩2 = (λs. False)⇩√)"
by(induct rule:PCFG.induct)(fastforce simp:intra_kind_def)+
from disj show ?case
proof
assume "prog ⊢ m -IEdge et⇩2→⇩p m'"
with ‹(Main,m) = n⇩2› ‹(Main,m') = n⇩2'›
‹prog ⊢ n -IEdge et→⇩p n'› ‹(Main,n) = n⇩2› ‹(Main,n') ≠ n⇩2'›
show ?thesis by(auto dest:WCFG_deterministic)
next
assume "∃p es rets. prog ⊢ m -CEdge (p, es, rets)→⇩p m' ∧ et⇩2 = (λs. False)⇩√"
with ‹(Main,m) = n⇩2› ‹(Main,m') = n⇩2'›
‹prog ⊢ n -IEdge et→⇩p n'› ‹(Main,n) = n⇩2› ‹(Main,n') ≠ n⇩2'›
have False by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_source)
thus ?thesis by simp
qed
next
case (Proc p ins outs c n et n')
from ‹prog,procs ⊢ n⇩2 -et⇩2→ n⇩2'› ‹(p,n) = n⇩2› ‹intra_kind et⇩2›
‹(p,ins,outs,c) ∈ set procs› ‹well_formed procs›
obtain m m' where "(p,m) = n⇩2" and "(p,m') = n⇩2'"
and disj:"c ⊢ m -IEdge et⇩2→⇩p m' ∨
(∃p' es' rets'. c ⊢ m -CEdge (p',es',rets')→⇩p m' ∧ et⇩2 = (λs. False)⇩√)"
by(induct rule:PCFG.induct)(fastforce simp:intra_kind_def)+
from disj show ?case
proof
assume "c ⊢ m -IEdge et⇩2→⇩p m'"
with ‹(p,m) = n⇩2› ‹(p,m') = n⇩2'›
‹c ⊢ n -IEdge et→⇩p n'› ‹(p,n) = n⇩2› ‹(p,n') ≠ n⇩2'›
show ?thesis by(auto dest:WCFG_deterministic)
next
assume "∃p' es' rets'. c ⊢ m -CEdge (p', es', rets')→⇩p m' ∧ et⇩2 = (λs. False)⇩√"
with ‹(p,m) = n⇩2› ‹(p,m') = n⇩2'›
‹c ⊢ n -IEdge et→⇩p n'› ‹(p,n) = n⇩2› ‹(p,n') ≠ n⇩2'›
have False by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_source)
thus ?thesis by simp
qed
next
case (MainCallReturn n p es rets n' n⇩2 n⇩2')
from ‹prog,procs ⊢ n⇩2 -et⇩2→ n⇩2'› ‹(Main,n) = n⇩2›
‹intra_kind et⇩2› ‹well_formed procs›
obtain m m' where "(Main,m) = n⇩2" and "(Main,m') = n⇩2'"
and disj:"prog ⊢ m -IEdge et⇩2→⇩p m' ∨
(∃p es rets. prog ⊢ m -CEdge (p,es,rets)→⇩p m' ∧ et⇩2 = (λs. False)⇩√)"
by(induct rule:PCFG.induct)(fastforce simp:intra_kind_def)+
from disj show ?case
proof
assume "prog ⊢ m -IEdge et⇩2→⇩p m'"
with ‹(Main,m) = n⇩2› ‹(Main,m') = n⇩2'› ‹prog ⊢ n -CEdge (p, es, rets)→⇩p n'›
‹(Main, n) = n⇩2› ‹(Main, n') ≠ n⇩2'›
have False by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_source)
thus ?thesis by simp
next
assume "∃p es rets. prog ⊢ m -CEdge (p,es,rets)→⇩p m' ∧ et⇩2 = (λs. False)⇩√"
with ‹(Main,m) = n⇩2› ‹(Main,m') = n⇩2'› ‹prog ⊢ n -CEdge (p, es, rets)→⇩p n'›
‹(Main, n) = n⇩2› ‹(Main, n') ≠ n⇩2'›
show ?thesis by(fastforce dest:Proc_CFG_Call_nodes_eq)
qed
next
case (ProcCallReturn p ins outs c n p' es rets n' ps n⇩2 n⇩2')
from ‹prog,procs ⊢ n⇩2 -et⇩2→ n⇩2'› ‹(p,n) = n⇩2› ‹intra_kind et⇩2›
‹(p,ins,outs,c) ∈ set procs› ‹well_formed procs›
obtain m m' where "(p,m) = n⇩2" and "(p,m') = n⇩2'"
and disj:"c ⊢ m -IEdge et⇩2→⇩p m' ∨
(∃p' es' rets'. c ⊢ m -CEdge (p',es',rets')→⇩p m' ∧ et⇩2 = (λs. False)⇩√)"
by(induct rule:PCFG.induct)(fastforce simp:intra_kind_def)+
from disj show ?case
proof
assume "c ⊢ m -IEdge et⇩2→⇩p m'"
with ‹(p,m) = n⇩2› ‹(p,m') = n⇩2'›
‹c ⊢ n -CEdge (p', es, rets)→⇩p n'› ‹(p,n) = n⇩2› ‹(p,n') ≠ n⇩2'›
have False by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_source)
thus ?thesis by simp
next
assume "∃p' es' rets'. c ⊢ m -CEdge (p', es', rets')→⇩p m' ∧ et⇩2 = (λs. False)⇩√"
with ‹(p,m) = n⇩2› ‹(p,m') = n⇩2'›
‹c ⊢ n -CEdge (p', es, rets)→⇩p n'› ‹(p,n) = n⇩2› ‹(p,n') ≠ n⇩2'›
show ?thesis by(fastforce dest:Proc_CFG_Call_nodes_eq)
qed
qed(auto simp:intra_kind_def)

subsection ‹Well-formedness of programs in combination with a procedure list.›

definition wf :: "cmd ⇒ procs ⇒ bool"
where "wf prog procs ≡ well_formed procs ∧
(∀ps p. containsCall procs prog ps p ⟶ (∃ins outs c. (p,ins,outs,c) ∈ set procs ∧
(∀c' n n' es rets. c' ⊢ n -CEdge (p,es,rets)→⇩p n' ⟶
distinct rets ∧ length rets = length outs ∧ length es = length ins)))"

lemma wf_well_formed [intro]:"wf prog procs ⟹ well_formed procs"

lemma wf_distinct_rets [intro]:
"⟦wf prog procs; containsCall procs prog ps p; (p,ins,outs,c) ∈ set procs;
c' ⊢ n -CEdge (p,es,rets)→⇩p n'⟧ ⟹ distinct rets"
by(fastforce simp:wf_def)

lemma
assumes "wf prog procs" and "containsCall procs prog ps p"
and "(p,ins,outs,c) ∈ set procs" and "c' ⊢ n -CEdge (p,es,rets)→⇩p n'"
shows wf_length_retsI [intro]:"length rets = length outs"
and wf_length_esI [intro]:"length es = length ins"
proof -
from ‹wf prog procs› have "well_formed procs" by fastforce
from assms
obtain ins' outs' c' where "(p,ins',outs',c') ∈ set procs"
and lengths:"length rets = length outs'" "length es = length ins'"
from ‹(p,ins,outs,c) ∈ set procs› ‹(p,ins',outs',c') ∈ set procs›
‹well_formed procs›
have "ins' = ins" "outs' = outs" "c' = c" by auto
with lengths show "length rets = length outs" "length es = length ins"
by simp_all
qed

subsection ‹Type of well-formed programs›

definition "wf_prog = {(prog,procs). wf prog procs}"

typedef wf_prog = wf_prog
unfolding wf_prog_def
apply (rule_tac x="(Skip,[])" in exI)
done

lemma wf_wf_prog:"Rep_wf_prog wfp = (prog,procs) ⟹ wf prog procs"

lemma wfp_Seq1: assumes "Rep_wf_prog wfp = (c⇩1;; c⇩2, procs)"
obtains wfp' where "Rep_wf_prog wfp' = (c⇩1, procs)"
using ‹Rep_wf_prog wfp = (c⇩1;; c⇩2, procs)›
apply(cases wfp) apply(auto simp:Abs_wf_prog_inverse wf_prog_def wf_def)
apply(erule_tac x="Abs_wf_prog (c⇩1, procs)" in meta_allE)
by(auto elim:meta_mp simp:Abs_wf_prog_inverse wf_prog_def wf_def)

lemma wfp_Seq2: assumes "Rep_wf_prog wfp = (c⇩1;; c⇩2, procs)"
obtains wfp' where "Rep_wf_prog wfp' = (c⇩2, procs)"
using ‹Rep_wf_prog wfp = (c⇩1;; c⇩2, procs)›
apply(cases wfp) apply(auto simp:Abs_wf_prog_inverse wf_prog_def wf_def)
apply(erule_tac x="Abs_wf_prog (c⇩2, procs)" in meta_allE)
by(auto elim:meta_mp simp:Abs_wf_prog_inverse wf_prog_def wf_def)

lemma wfp_CondTrue: assumes "Rep_wf_prog wfp = (if (b) c⇩1 else c⇩2, procs)"
obtains wfp' where "Rep_wf_prog wfp' = (c⇩1, procs)"
using ‹Rep_wf_prog wfp = (if (b) c⇩1 else c⇩2, procs)›
apply(cases wfp) apply(auto simp:Abs_wf_prog_inverse wf_prog_def wf_def)
apply(erule_tac x="Abs_wf_prog (c⇩1, procs)" in meta_allE)
by(auto elim:meta_mp simp:Abs_wf_prog_inverse wf_prog_def wf_def)

lemma wfp_CondFalse: assumes "Rep_wf_prog wfp = (if (b) c⇩1 else c⇩2, procs)"
obtains wfp' where "Rep_wf_prog wfp' = (c⇩2, procs)"
using ‹Rep_wf_prog wfp = (if (b) c⇩1 else c⇩2, procs)›
apply(cases wfp) apply(auto simp:Abs_wf_prog_inverse wf_prog_def wf_def)
apply(erule_tac x="Abs_wf_prog (c⇩2, procs)" in meta_allE)
by(auto elim:meta_mp simp:Abs_wf_prog_inverse wf_prog_def wf_def)

lemma wfp_WhileBody: assumes "Rep_wf_prog wfp = (while (b) c', procs)"
obtains wfp' where "Rep_wf_prog wfp' = (c', procs)"
using ‹Rep_wf_prog wfp = (while (b) c', procs)›
apply(cases wfp) apply(auto simp:Abs_wf_prog_inverse wf_prog_def wf_def)
apply(erule_tac x="Abs_wf_prog (c', procs)" in meta_allE)
by(auto elim:meta_mp simp:Abs_wf_prog_inverse wf_prog_def wf_def)

lemma wfp_Call: assumes "Rep_wf_prog wfp = (prog,procs)"
and "(p,ins,outs,c) ∈ set procs" and "containsCall procs prog ps p"
obtains wfp' where "Rep_wf_prog wfp' = (c,procs)"
using assms
apply(cases wfp) apply(auto simp:Abs_wf_prog_inverse wf_prog_def wf_def)
apply(erule_tac x="Abs_wf_prog (c, procs)" in meta_allE)
apply(erule meta_mp) apply(rule Abs_wf_prog_inverse)
by(auto dest:containsCall_indirection simp:wf_prog_def wf_def)

end
```