Theory Slicing.WellFormed

section ‹General well-formedness of While CFG›

theory WellFormed imports 
  Interpretation 
  Labels 
  "../Basic/CFGExit_wf" 
  "../StaticIntra/CDepInstantiations" 
begin

subsection ‹Definition of some functions›

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)       = {}"

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

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


lemma rhs_interpret_eq: 
  "interpret b s = Some v'; V  rhs_aux b. s V = s' V 
    interpret b s' = Some v'"
proof(induct b arbitrary:v')
  case (Val v)
  from interpret (Val v) s = Some v' have "v' = v" by(fastforce elim:interpret.cases)
  thus ?case by simp
next
  case (Var V)
  hence "s' V = Some v'" by(fastforce elim:interpret.cases)
  thus ?case by simp
next
  case (BinOp b1 bop b2)
  note IH1 = v'. interpret b1 s = Some v'; V  rhs_aux b1. s V = s' V 
              interpret b1 s' = Some v'
  note IH2 = v'. interpret b2 s = Some v'; V  rhs_aux b2. s V = s' V 
              interpret b2 s' = Some v'
  from interpret (b1 «bop» b2) s = Some v' 
  have "v1 v2. interpret b1 s = Some v1  interpret b2 s = Some v2 
                binop bop v1 v2 = Some v'"
    apply(cases "interpret b1 s",simp)
    apply(cases "interpret b2 s",simp)
    by(case_tac "binop bop a aa",simp+)
  then obtain v1 v2 where "interpret b1 s = Some v1"
    and "interpret b2 s = Some v2" and "binop bop v1 v2 = Some v'" by blast
  from V  rhs_aux (b1 «bop» b2). s V = s' V have "V  rhs_aux b1. s V = s' V"
    by simp
  from IH1[OF interpret b1 s = Some v1 this] have "interpret b1 s' = Some v1" .
  from V  rhs_aux (b1 «bop» b2). s V = s' V have "V  rhs_aux b2. s V = s' V"
    by simp
  from IH2[OF interpret b2 s = Some v2 this] have "interpret b2 s' = Some v2" .
  with interpret b1 s' = Some v1 binop bop v1 v2 = Some v' show ?case by simp
qed


fun Defs :: "cmd  w_node  vname set"
where "Defs prog n = {V. l c.  n = (_ l _)  labels prog l c  V  lhs c}"

fun Uses :: "cmd  w_node  vname set"
where "Uses prog n = {V. l c.  n = (_ l _)  labels prog l c  V  rhs c}"


subsection ‹Lemmas about @{term "prog  n -et n'"} to show well-formed 
  properties›

lemma WCFG_edge_no_Defs_equal:
  "prog  n -et n'; V  Defs prog n  (transfer et s) V = s V"
proof(induct rule:WCFG_induct)
  case (WCFG_LAss V' e)
  have label:"labels (V':=e) 0 (V':=e)" and lhs:"V'  lhs (V':=e)"
    by(auto intro:Labels_Base)
  hence "V'  Defs (V':=e) (_0_)" by fastforce
  with V  Defs (V':=e) (_0_) show ?case by auto
next
  case (WCFG_SeqFirst c1 n et n' c2)
  note IH = V  Defs c1 n  transfer et s V = s V
  have "V  Defs c1 n"
  proof
    assume "V  Defs c1 n"
    then obtain c l where [simp]:"n = (_ l _)" and "labels c1 l c"
      and "V  lhs c" by fastforce
    from labels c1 l c have "labels (c1;;c2) l (c;;c2)"
      by(fastforce intro:Labels_Seq1)
    from V  lhs c have "V  lhs (c;;c2)" by simp
    with labels (c1;;c2) l (c;;c2) have "V  Defs (c1;;c2) n" by fastforce
    with V  Defs (c1;;c2) n show False by fastforce
  qed
  from IH[OF this] show ?case .
next
  case (WCFG_SeqConnect c1 n et c2)
  note IH = V  Defs c1 n  transfer et s V = s V
  have "V  Defs c1 n"
  proof
    assume "V  Defs c1 n"
    then obtain c l where [simp]:"n = (_ l _)" and "labels c1 l c"
      and "V  lhs c" by fastforce
    from labels c1 l c have "labels (c1;;c2) l (c;;c2)"
      by(fastforce intro:Labels_Seq1)
    from V  lhs c have "V  lhs (c;;c2)" by simp
    with labels (c1;;c2) l (c;;c2) have "V  Defs (c1;;c2) n" by fastforce
    with V  Defs (c1;;c2) n show False by fastforce
  qed
  from IH[OF this] show ?case .
next
  case (WCFG_SeqSecond c2 n et n' c1)
  note IH = V  Defs c2 n  transfer et s V = s V
  have "V  Defs c2 n"
  proof
    assume "V  Defs c2 n"
    then obtain c l where [simp]:"n = (_ l _)" and "labels c2 l c"
      and "V  lhs c" by fastforce
    from labels c2 l c have "labels (c1;;c2) (l + #:c1) c"
      by(fastforce intro:Labels_Seq2)
    with V  lhs c have "V  Defs (c1;;c2) (n  #:c1)" by fastforce
    with V  Defs (c1;;c2) (n  #:c1) show False by fastforce
  qed
  from IH[OF this] show ?case .
next
  case (WCFG_CondThen c1 n et n' b c2)
  note IH = V  Defs c1 n  transfer et s V = s V
  have "V  Defs c1 n"
  proof
    assume "V  Defs c1 n"
    then obtain c l where [simp]:"n = (_ l _)" and "labels c1 l c"
      and "V  lhs c" by fastforce
    from labels c1 l c have "labels (if (b) c1 else c2) (l + 1) c"
      by(fastforce intro:Labels_CondTrue)
    with V  lhs c have "V  Defs (if (b) c1 else c2) (n  1)" by fastforce
    with V  Defs (if (b) c1 else c2) (n  1) show False by fastforce
  qed
  from IH[OF this] show ?case .
next
  case (WCFG_CondElse c2 n et n' b c1)
  note IH = V  Defs c2 n  transfer et s V = s V
  have "V  Defs c2 n"
  proof
    assume "V  Defs c2 n"
    then obtain c l where [simp]:"n = (_ l _)" and "labels c2 l c"
      and "V  lhs c" by fastforce
    from labels c2 l c have "labels (if (b) c1 else c2) (l + #:c1 + 1) c"
      by(fastforce intro:Labels_CondFalse)
    with V  lhs c have "V  Defs (if (b) c1 else c2) (n  #:c1 + 1)"
      by(fastforce simp:add.commute add.left_commute)
    with V  Defs (if (b) c1 else c2) (n  #:c1 + 1) show False by fastforce
  qed
  from IH[OF this] show ?case .
next
  case (WCFG_WhileBody c' n et n' b)
  note IH = V  Defs c' n  transfer et s V = s V
  have "V  Defs c' n"
  proof
    assume "V  Defs c' n"
    then obtain c l where [simp]:"n = (_ l _)" and "labels c' l c"
      and "V  lhs c" by fastforce
    from labels c' l c have "labels (while (b) c') (l + 2) (c;;while (b) c')"
      by(fastforce intro:Labels_WhileBody)
    from V  lhs c have "V  lhs (c;;while (b) c')" by fastforce
    with labels (while (b) c') (l + 2) (c;;while (b) c')
    have "V  Defs (while (b) c') (n  2)" by fastforce
    with V  Defs (while (b) c') (n  2) show False by fastforce
  qed
  from IH[OF this] show ?case .
next
  case (WCFG_WhileBodyExit c' n et b)
  note IH = V  Defs c' n  transfer et s V = s V
  have "V  Defs c' n"
  proof
    assume "V  Defs c' n"
    then obtain c l where [simp]:"n = (_ l _)" and "labels c' l c"
      and "V  lhs c" by fastforce
    from labels c' l c have "labels (while (b) c') (l + 2) (c;;while (b) c')"
      by(fastforce intro:Labels_WhileBody)
    from V  lhs c have "V  lhs (c;;while (b) c')" by fastforce
    with labels (while (b) c') (l + 2) (c;;while (b) c')
    have "V  Defs (while (b) c') (n  2)" by fastforce
    with V  Defs (while (b) c') (n  2) show False by fastforce
  qed
  from IH[OF this] show ?case .
qed auto


(*<*)declare One_nat_def [simp del](*>*)

lemma WCFG_edge_transfer_uses_only_Uses:
  "prog  n -et n'; V  Uses prog n. s V = s' V
   V  Defs prog n. (transfer et s) V = (transfer et s') V"
proof(induct rule:WCFG_induct)
  case (WCFG_LAss V e)
  have "Uses (V:=e) (_0_) = {V. V  rhs_aux e}"
    by(fastforce elim:labels.cases intro:Labels_Base)
  with V'Uses (V:=e) (_0_). s V' = s' V' 
  have "V'rhs_aux e. s V' = s' V'" by blast
  have "Defs (V:=e) (_0_) = {V}"
    by(fastforce elim:labels.cases intro:Labels_Base)
  have "transfer λs. s(V := interpret e s) s V =
        transfer λs. s(V := interpret e s) s' V"
  proof(cases "interpret e s")
    case None
    { fix v assume "interpret e s' = Some v"
      with V'rhs_aux e. s V' = s' V' have "interpret e s = Some v"
        by(fastforce intro:rhs_interpret_eq)
      with None have False by(fastforce split:if_split_asm) }
    with None show ?thesis by fastforce
  next
    case (Some v)
    hence "interpret e s = Some v" by(fastforce split:if_split_asm)
    with V'rhs_aux e. s V' = s' V'
    have "interpret e s' = Some v" by(fastforce intro:rhs_interpret_eq)
    with Some show ?thesis by simp
  qed
  with Defs (V:=e) (_0_) = {V} show ?case by simp
next
  case (WCFG_SeqFirst c1 n et n' c2)
  note IH = VUses c1 n. s V = s' V 
     VDefs c1 n. transfer et s V = transfer et s' V
  from VUses (c1;;c2) n. s V = s' V have "VUses c1 n. s V = s' V"
    by auto(drule Labels_Seq1[of _ _ _ c2],erule_tac x="V" in allE,auto)
  from IH[OF this] have "VDefs c1 n. transfer et s V = transfer et s' V" .
  with c1  n -et n' show ?case using Labels_Base 
    apply clarsimp 
    apply(erule labels.cases,auto dest:WCFG_sourcelabel_less_num_nodes)
    by(erule_tac x="V" in allE,fastforce)
next
  case (WCFG_SeqConnect c1 n et c2)
  note IH = VUses c1 n. s V = s' V 
     VDefs c1 n. transfer et s V = transfer et s' V
  from VUses (c1;;c2) n. s V = s' V have "VUses c1 n. s V = s' V"
    by auto(drule Labels_Seq1[of _ _ _ c2],erule_tac x="V" in allE,auto)
  from IH[OF this] have "VDefs c1 n. transfer et s V = transfer et s' V" .
  with c1  n -et (_Exit_) show ?case using Labels_Base 
    apply clarsimp 
    apply(erule labels.cases,auto dest:WCFG_sourcelabel_less_num_nodes)
    by(erule_tac x="V" in allE,fastforce)
next
  case (WCFG_SeqSecond c2 n et n' c1)
  note IH = VUses c2 n. s V = s' V 
     VDefs c2 n. transfer et s V = transfer et s' V
  from VUses (c1;;c2) (n  #:c1). s V = s' V have "VUses c2 n. s V = s' V"
    by(auto,blast dest:Labels_Seq2)
  from IH[OF this] have "VDefs c2 n. transfer et s V = transfer et s' V" .
  with num_inner_nodes_gr_0[of "c1"] show ?case
    apply clarsimp
    apply(erule labels.cases,auto)
    by(cases n,auto dest:label_less_num_inner_nodes)+
next
  case (WCFG_CondThen c1 n et n' b c2)
  note IH = VUses c1 n. s V = s' V 
     VDefs c1 n. transfer et s V = transfer et s' V
  from VUses (if (b) c1 else c2) (n  1). s V = s' V 
  have "VUses c1 n. s V = s' V" by(auto,blast dest:Labels_CondTrue)
  from IH[OF this] have "VDefs c1 n. transfer et s V = transfer et s' V" .
  with c1  n -et n' show ?case
    apply clarsimp 
    apply(erule labels.cases,auto)
    apply(cases n,auto dest:label_less_num_inner_nodes)
    by(cases n,auto dest:WCFG_sourcelabel_less_num_nodes)
next
  case (WCFG_CondElse c2 n et n' b c1)
  note IH = VUses c2 n. s V = s' V 
     VDefs c2 n. transfer et s V = transfer et s' V
  from VUses (if (b) c1 else c2) (n  #:c1 + 1). s V = s' V 
  have "VUses c2 n. s V = s' V"
    by auto(drule Labels_CondFalse[of _ _ _ b c1],erule_tac x="V" in allE,
       auto simp:add.assoc)
  from IH[OF this] have "VDefs c2 n. transfer et s V = transfer et s' V" .
  with c2  n -et n' show ?case
    apply clarsimp 
    apply(erule labels.cases,auto)
    apply(cases n,auto dest:label_less_num_inner_nodes)
    by(cases n,auto dest:WCFG_sourcelabel_less_num_nodes)
next
  case (WCFG_WhileBody c' n et n' b)
  note IH = VUses c' n. s V = s' V 
     VDefs c' n. transfer et s V = transfer et s' V
  from VUses (while (b) c') (n  2). s V = s' V have "VUses c' n. s V = s' V"
    by auto(drule Labels_WhileBody[of _ _ _ b],erule_tac x="V" in allE,auto)
  from IH[OF this] have "VDefs c' n. transfer et s V = transfer et s' V" .
  thus ?case
    apply clarsimp 
    apply(erule labels.cases,auto)
    by(cases n,auto dest:label_less_num_inner_nodes)
next
  case (WCFG_WhileBodyExit c' n et b)
  note IH = VUses c' n. s V = s' V 
     VDefs c' n. transfer et s V = transfer et s' V
  from VUses (while (b) c') (n  2). s V = s' V have "VUses c' n. s V = s' V"
    by auto(drule Labels_WhileBody[of _ _ _ b],erule_tac x="V" in allE,auto)
  from IH[OF this] have "VDefs c' n. transfer et s V = transfer et s' V" .
  thus ?case
    apply clarsimp 
    apply(erule labels.cases,auto)
    by(cases n,auto dest:label_less_num_inner_nodes)
qed (fastforce elim:labels.cases)+


lemma WCFG_edge_Uses_pred_eq:
  "prog  n -et n'; V  Uses prog n. s V = s' V; pred et s
     pred et s'"
proof(induct rule:WCFG_induct)
  case (WCFG_SeqFirst c1 n et n' c2)
  note IH = VUses c1 n. s V = s' V; pred et s  pred et s'
  from VUses (c1;; c2) n. s V = s' V have "VUses c1 n. s V = s' V"
    by auto(drule Labels_Seq1[of _ _ _ c2],erule_tac x="V" in allE,auto)
  from IH[OF this pred et s] show ?case .
next
  case (WCFG_SeqConnect c1 n et c2)
  note IH = VUses c1 n. s V = s' V; pred et s  pred et s'
  from VUses (c1;; c2) n. s V = s' V have "VUses c1 n. s V = s' V"
    by auto(drule Labels_Seq1[of _ _ _ c2],erule_tac x="V" in allE,auto)
  from IH[OF this pred et s] show ?case .
next
  case (WCFG_SeqSecond c2 n et n' c1)
  note IH = VUses c2 n. s V = s' V; pred et s  pred et s'
  from VUses (c1;; c2) (n  #:c1). s V = s' V
  have "VUses c2 n. s V = s' V" by(auto,blast dest:Labels_Seq2)
  from IH[OF this pred et s] show ?case .
next
  case (WCFG_CondTrue b c1 c2)
  from VUses (if (b) c1 else c2) (_0_). s V = s' V 
  have all:"V. labels (if (b) c1 else c2) 0 (if (b) c1 else c2)  
            V  rhs (if (b) c1 else c2)  (s V = s' V)"
    by fastforce
  obtain v' where [simp]:"v' = true" by simp
  with pred (λs. interpret b s = Some true) s
  have "interpret b s = Some v'" by simp
  have "labels (if (b) c1 else c2) 0 (if (b) c1 else c2)" by(rule Labels_Base)
  with all have "V  rhs_aux b. s V = s' V" by simp
  with interpret b s = Some v' have "interpret b s' = Some v'"
    by(rule rhs_interpret_eq)
  thus ?case by simp
next
  case (WCFG_CondFalse b c1 c2)
  from VUses (if (b) c1 else c2) (_0_). s V = s' V
  have all:"V. labels (if (b) c1 else c2) 0 (if (b) c1 else c2)  
              V  rhs (if (b) c1 else c2)  (s V = s' V)"
    by fastforce
  obtain v' where [simp]:"v' = false" by simp
  with pred (λs. interpret b s = Some false) s 
  have "interpret b s = Some v'" by simp
  have "labels (if (b) c1 else c2) 0 (if (b) c1 else c2)" by(rule Labels_Base)
  with all have "V  rhs_aux b. s V = s' V" by simp
  with interpret b s = Some v' have "interpret b s' = Some v'"
    by(rule rhs_interpret_eq)
  thus ?case by simp
next
  case (WCFG_CondThen c1 n et n' b c2)
  note IH = VUses c1 n. s V = s' V; pred et s  pred et s'
  from VUses (if (b) c1 else c2) (n  1). s V = s' V
  have "VUses c1 n. s V = s' V" by(auto,blast dest:Labels_CondTrue)
  from IH[OF this pred et s] show ?case .
next
  case (WCFG_CondElse c2 n et n' b c1)
  note IH = VUses c2 n. s V = s' V; pred et s  pred et s'
  from VUses (if (b) c1 else c2) (n  #:c1 + 1). s V = s' V
  have "VUses c2 n. s V = s' V"
    by auto(drule Labels_CondFalse[of _ _ _ b c1],erule_tac x="V" in allE,
       auto simp:add.assoc)
  from IH[OF this pred et s] show ?case .
next
  case (WCFG_WhileTrue b c')
  from VUses (while (b) c') (_0_). s V = s' V
  have all:"V. labels (while (b) c') 0 (while (b) c')  
              V  rhs (while (b) c')  (s V = s' V)"
    by fastforce
  obtain v' where [simp]:"v' = true" by simp
  with pred (λs. interpret b s = Some true) s
  have "interpret b s = Some v'" by simp
  have "labels (while (b) c') 0 (while (b) c')" by(rule Labels_Base)
  with all have "V  rhs_aux b. s V = s' V" by simp
  with interpret b s = Some v' have "interpret b s' = Some v'"
    by(rule rhs_interpret_eq)
  thus ?case by simp
next
  case (WCFG_WhileFalse b c')
  from VUses (while (b) c') (_0_). s V = s' V
  have all:"V. labels (while (b) c') 0 (while (b) c')  
              V  rhs (while (b) c')  (s V = s' V)"
    by fastforce
  obtain v' where [simp]:"v' = false" by simp
  with pred (λs. interpret b s = Some false) s
  have "interpret b s = Some v'" by simp
  have "labels (while (b) c') 0 (while (b) c')" by(rule Labels_Base)
  with all have "V  rhs_aux b. s V = s' V" by simp
  with interpret b s = Some v' have "interpret b s' = Some v'"
    by(rule rhs_interpret_eq)
  thus ?case by simp
next
  case (WCFG_WhileBody c' n et n' b)
  note IH = VUses c' n. s V = s' V; pred et s  pred et s'
  from VUses (while (b) c') (n  2). s V = s' V have "VUses c' n. s V = s' V"
    by auto(drule Labels_WhileBody[of _ _ _ b],erule_tac x="V" in allE,auto)
  from IH[OF this pred et s] show ?case .
next
  case (WCFG_WhileBodyExit c' n et b)
  note IH = VUses c' n. s V = s' V; pred et s  pred et s'
  from VUses (while (b) c') (n  2). s V = s' V have "VUses c' n. s V = s' V"
    by auto(drule Labels_WhileBody[of _ _ _ b],erule_tac x="V" in allE,auto)
  from IH[OF this pred et s] show ?case .
qed simp_all


(*<*)declare One_nat_def [simp](*>*)

interpretation While_CFG_wf: CFG_wf sourcenode targetnode kind 
  "valid_edge prog" Entry "Defs prog" "Uses prog" id
  for prog
proof(unfold_locales)
  show "Defs prog (_Entry_) = {}  Uses prog (_Entry_) = {}"
    by(simp add:Defs.simps Uses.simps)
next
  fix a V s
  assume "valid_edge prog a" and "V  Defs prog (sourcenode a)"
  obtain nx et nx' where [simp]:"a = (nx,et,nx')" by(cases a) auto
  with valid_edge prog a have "prog  nx -et nx'" by(simp add:valid_edge_def)
  with V  Defs prog (sourcenode a) show "id (transfer (kind a) s) V = id s V"
    by(fastforce intro:WCFG_edge_no_Defs_equal)
next
  fix a fix s s'::state
  assume "valid_edge prog a" 
    and "VUses prog (sourcenode a). id s V = id s' V"
  obtain nx et nx' where [simp]:"a = (nx,et,nx')" by(cases a) auto
  with valid_edge prog a have "prog  nx -et nx'" by(simp add:valid_edge_def)
  with VUses prog (sourcenode a). id s V = id s' V
  show "VDefs prog (sourcenode a).
             id (transfer (kind a) s) V = id (transfer (kind a) s') V"
    by -(drule WCFG_edge_transfer_uses_only_Uses,simp+)
next
  fix a s s'
  assume pred:"pred (kind a) s" and valid:"valid_edge prog a"
    and all:"VUses prog (sourcenode a). id s V = id s' V"
  obtain nx et nx' where [simp]:"a = (nx,et,nx')" by(cases a) auto
  with valid_edge prog a have "prog  nx -et nx'" by(simp add:valid_edge_def)
  with pred (kind a) s VUses prog (sourcenode a). id s V = id s' V
  show "pred (kind a) s'" by -(drule WCFG_edge_Uses_pred_eq,simp+)
next
  fix a a' 
  assume "valid_edge prog a" and "valid_edge prog a'" 
    and "sourcenode a = sourcenode a'" and "targetnode a  targetnode a'"
  thus "Q Q'. kind a = (Q)  kind a' = (Q')  
               (s. (Q s  ¬ Q' s)  (Q' s  ¬ Q s))"
    by(fastforce intro!:WCFG_deterministic simp:valid_edge_def)
qed


lemma While_CFGExit_wf_aux:"CFGExit_wf sourcenode targetnode kind 
  (valid_edge prog) Entry (Defs prog) (Uses prog) id Exit"
proof(unfold_locales)
  show "Defs prog (_Exit_) = {}  Uses prog (_Exit_) = {}"
    by(simp add:Defs.simps Uses.simps)
qed

interpretation While_CFGExit_wf: CFGExit_wf sourcenode targetnode kind 
  "valid_edge prog" Entry "Defs prog" "Uses prog" id Exit
  for prog
by(rule While_CFGExit_wf_aux)


end