Theory WellFormProgs

Up to index of Isabelle/HOL/Jinja/HRB-Slicing

theory WellFormProgs
imports PCFG
header {* \isaheader{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 \<turnstile> (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 \<turnstile> 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 \<turnstile> 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 \<turnstile> 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 \<turnstile> (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' \<turnstile> 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' \<turnstile> 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' \<turnstile> 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 \<turnstile> 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 \<turnstile> 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 \<turnstile> 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 \<turnstile> 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 \<turnstile> 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' \<turnstile> 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' \<turnstile> 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' \<turnstile> 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 \<turnstile> n -et-> n'; prog,procs \<turnstile> 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 \<turnstile> (Main,Label l) -et'-> (p,Entry)` `well_formed procs`
  obtain es' rets' n'' ins' outs' c' 
    where "prog \<turnstile> Label l -CEdge (p,es',rets')->p n''" 
    and "(p,ins',outs',c') ∈ set procs" 
    and "et' = (λs. True):(Main,n'')\<hookrightarrow>pmap (λ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 \<turnstile> Label l -CEdge (p,es,rets)->p n'`
    `prog \<turnstile> 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'')\<hookrightarrow>pmap (λ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 \<turnstile> (p,Label l) -et'-> (p',Entry)` `(p',ins',outs',c') ∈ set procs` 
    `(p, ins, outs, c) ∈ set procs` `well_formed procs`
    `c \<turnstile> 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 \<turnstile> Label l -CEdge (p', es'x, rets'x)->p Label l'x`
      `c \<turnstile> 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 \<turnstile> (p',Exit) -et'-> (p, Label l')`
    `(p, ins, outs, c) ∈ set procs` `(p', ins', outs', c') ∈ set procs`
    `c \<turnstile> 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 \<turnstile> Label lx -CEdge (p', es'x, rets'x)->p Label l'`
      `c \<turnstile> 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 \<turnstile> n1 -et1-> n1'; prog,procs \<turnstile> n2 -et2-> n2'; n1 = n2; n1' ≠ n2'; 
   intra_kind et1; intra_kind et2; well_formed procs|]
  ==> ∃Q Q'. et1 = (Q)\<surd> ∧ et2 = (Q')\<surd> ∧ 
            (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))"
proof(induct arbitrary:n2 n2' rule:PCFG.induct)
  case (Main n et n')
  from `prog,procs \<turnstile> n2 -et2-> n2'` `(Main,n) = n2`
    `intra_kind et2` `well_formed procs`
  obtain m m' where "(Main,m) = n2" and "(Main,m') = n2'"
    and disj:"prog \<turnstile> m -IEdge et2->p m' ∨ 
    (∃p es rets. prog \<turnstile> m -CEdge (p,es,rets)->p m' ∧ et2 = (λs. False)\<surd>)"
    by(induct rule:PCFG.induct)(fastforce simp:intra_kind_def)+
  from disj show ?case
  proof
    assume "prog \<turnstile> m -IEdge et2->p m'"
    with `(Main,m) = n2` `(Main,m') = n2'` 
      `prog \<turnstile> n -IEdge et->p n'` `(Main,n) = n2` `(Main,n') ≠ n2'`
    show ?thesis by(auto dest:WCFG_deterministic)
  next
    assume "∃p es rets. prog \<turnstile> m -CEdge (p, es, rets)->p m' ∧ et2 = (λs. False)\<surd>"
    with `(Main,m) = n2` `(Main,m') = n2'` 
      `prog \<turnstile> n -IEdge et->p n'` `(Main,n) = n2` `(Main,n') ≠ n2'`
    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 \<turnstile> n2 -et2-> n2'` `(p,n) = n2` `intra_kind et2`
    `(p,ins,outs,c) ∈ set procs` `well_formed procs`
  obtain m m' where "(p,m) = n2" and "(p,m') = n2'"
    and disj:"c \<turnstile> m -IEdge et2->p m' ∨ 
    (∃p' es' rets'. c \<turnstile> m -CEdge (p',es',rets')->p m' ∧ et2 = (λs. False)\<surd>)"
    by(induct rule:PCFG.induct)(fastforce simp:intra_kind_def)+
  from disj show ?case
  proof
    assume "c \<turnstile> m -IEdge et2->p m'"
    with `(p,m) = n2` `(p,m') = n2'` 
      `c \<turnstile> n -IEdge et->p n'` `(p,n) = n2` `(p,n') ≠ n2'`
    show ?thesis by(auto dest:WCFG_deterministic)
  next
    assume "∃p' es' rets'. c \<turnstile> m -CEdge (p', es', rets')->p m' ∧ et2 = (λs. False)\<surd>"
    with `(p,m) = n2` `(p,m') = n2'` 
      `c \<turnstile> n -IEdge et->p n'` `(p,n) = n2` `(p,n') ≠ n2'`
    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' n2 n2')
  from `prog,procs \<turnstile> n2 -et2-> n2'` `(Main,n) = n2`
    `intra_kind et2` `well_formed procs`
  obtain m m' where "(Main,m) = n2" and "(Main,m') = n2'"
    and disj:"prog \<turnstile> m -IEdge et2->p m' ∨ 
    (∃p es rets. prog \<turnstile> m -CEdge (p,es,rets)->p m' ∧ et2 = (λs. False)\<surd>)"
    by(induct rule:PCFG.induct)(fastforce simp:intra_kind_def)+
  from disj show ?case
  proof
    assume "prog \<turnstile> m -IEdge et2->p m'"
    with `(Main,m) = n2` `(Main,m') = n2'` `prog \<turnstile> n -CEdge (p, es, rets)->p n'`
      `(Main, n) = n2` `(Main, n') ≠ n2'`
    have False by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_source)
    thus ?thesis by simp
  next
    assume "∃p es rets. prog \<turnstile> m -CEdge (p,es,rets)->p m' ∧ et2 = (λs. False)\<surd>"
    with `(Main,m) = n2` `(Main,m') = n2'` `prog \<turnstile> n -CEdge (p, es, rets)->p n'`
      `(Main, n) = n2` `(Main, n') ≠ n2'`
    show ?thesis by(fastforce dest:Proc_CFG_Call_nodes_eq)
  qed
next
  case (ProcCallReturn p ins outs c n p' es rets n' ps n2 n2')
  from `prog,procs \<turnstile> n2 -et2-> n2'` `(p,n) = n2` `intra_kind et2`
    `(p,ins,outs,c) ∈ set procs` `well_formed procs`
  obtain m m' where "(p,m) = n2" and "(p,m') = n2'"
    and disj:"c \<turnstile> m -IEdge et2->p m' ∨ 
    (∃p' es' rets'. c \<turnstile> m -CEdge (p',es',rets')->p m' ∧ et2 = (λs. False)\<surd>)"
    by(induct rule:PCFG.induct)(fastforce simp:intra_kind_def)+
  from disj show ?case
  proof
    assume "c \<turnstile> m -IEdge et2->p m'"
    with `(p,m) = n2` `(p,m') = n2'` 
      `c \<turnstile> n -CEdge (p', es, rets)->p n'` `(p,n) = n2` `(p,n') ≠ n2'`
    have False by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_source)
    thus ?thesis by simp
  next
    assume "∃p' es' rets'. c \<turnstile> m -CEdge (p', es', rets')->p m' ∧ et2 = (λs. False)\<surd>"
    with `(p,m) = n2` `(p,m') = n2'` 
      `c \<turnstile> n -CEdge (p', es, rets)->p n'` `(p,n) = n2` `(p,n') ≠ n2'`
    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' \<turnstile> 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' \<turnstile> 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' \<turnstile> 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:"Rep_wf_prog wfp = (prog,procs) ==> wf prog procs"
using Rep_wf_prog[of wfp] by(simp add:wf_prog_def)


lemma wfp_Seq1: assumes "Rep_wf_prog wfp = (c1;; c2, procs)"
  obtains wfp' where "Rep_wf_prog wfp' = (c1, procs)"
using `Rep_wf_prog wfp = (c1;; c2, procs)`
apply(cases wfp) apply(auto simp:Abs_wf_prog_inverse wf_prog_def wf_def)
apply(erule_tac x="Abs_wf_prog (c1, 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 = (c1;; c2, procs)"
  obtains wfp' where "Rep_wf_prog wfp' = (c2, procs)"
using `Rep_wf_prog wfp = (c1;; c2, procs)`
apply(cases wfp) apply(auto simp:Abs_wf_prog_inverse wf_prog_def wf_def)
apply(erule_tac x="Abs_wf_prog (c2, 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) c1 else c2, procs)"
  obtains wfp' where "Rep_wf_prog wfp' = (c1, procs)"
using `Rep_wf_prog wfp = (if (b) c1 else c2, procs)`
apply(cases wfp) apply(auto simp:Abs_wf_prog_inverse wf_prog_def wf_def)
apply(erule_tac x="Abs_wf_prog (c1, 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) c1 else c2, procs)"
  obtains wfp' where "Rep_wf_prog wfp' = (c2, procs)"
using `Rep_wf_prog wfp = (if (b) c1 else c2, procs)`
apply(cases wfp) apply(auto simp:Abs_wf_prog_inverse wf_prog_def wf_def)
apply(erule_tac x="Abs_wf_prog (c2, 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