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"
  by(simp add:wf_def)


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'"
    by(simp add:wf_def) blast
  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)
  apply (simp add:wf_def well_formed_def)
  done

lemma wf_wf_prog:
  fixes wfp
  shows "Rep_wf_prog wfp = (prog,procs) ⟹ wf prog procs"
using Rep_wf_prog[of wfp] by(simp add:wf_prog_def)


lemma wfp_Seq1:
  fixes wfp
  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:
  fixes wfp
  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:
  fixes wfp
  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:
  fixes wfp
  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:
  fixes wfp
  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:
  fixes wfp
  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