Theory Slicing.CFG

section ‹CFG›

theory CFG imports BasicDefs begin

subsection ‹The abstract CFG›

locale CFG =
  fixes sourcenode :: "'edge  'node"
  fixes targetnode :: "'edge  'node"
  fixes kind :: "'edge  'state edge_kind"
  fixes valid_edge :: "'edge  bool"
  fixes Entry::"'node" ("'('_Entry'_')")
  assumes Entry_target [dest]: "valid_edge a; targetnode a = (_Entry_)  False"
  and edge_det: 
  "valid_edge a; valid_edge a'; sourcenode a = sourcenode a'; 
    targetnode a = targetnode a'  a = a'"

begin

definition valid_node :: "'node  bool"
  where "valid_node n  
  (a. valid_edge a  (n = sourcenode a  n = targetnode a))"

lemma [simp]: "valid_edge a  valid_node (sourcenode a)"
  by(fastforce simp:valid_node_def)

lemma [simp]: "valid_edge a  valid_node (targetnode a)"
  by(fastforce simp:valid_node_def)


subsection ‹CFG paths and lemmas›

inductive path :: "'node  'edge list  'node  bool"
  ("_ -_→* _" [51,0,0] 80)
where 
  empty_path:"valid_node n  n -[]→* n"

  | Cons_path:
  "n'' -as→* n'; valid_edge a; sourcenode a = n; targetnode a = n''
     n -a#as→* n'"


lemma path_valid_node:
  assumes "n -as→* n'" shows "valid_node n" and "valid_node n'"
  using n -as→* n'
  by(induct rule:path.induct,auto)

lemma empty_path_nodes [dest]:"n -[]→* n'  n = n'"
  by(fastforce elim:path.cases)

lemma path_valid_edges:"n -as→* n'  a  set as. valid_edge a"
by(induct rule:path.induct) auto


lemma path_edge:"valid_edge a  sourcenode a -[a]→* targetnode a"
  by(fastforce intro:Cons_path empty_path)


lemma path_Entry_target [dest]:
  assumes "n -as→* (_Entry_)"
  shows "n = (_Entry_)" and "as = []"
using n -as→* (_Entry_)
proof(induct n as n'"(_Entry_)" rule:path.induct)
  case (Cons_path n'' as a n)
  from targetnode a = n'' valid_edge a n'' = (_Entry_) have False
    by -(rule Entry_target,simp_all)
  { case 1
    with False show ?case ..
  next
    case 2
    with False show ?case ..
  }
qed simp_all



lemma path_Append:"n -as→* n''; n'' -as'→* n' 
   n -as@as'→* n'"
by(induct rule:path.induct,auto intro:Cons_path)


lemma path_split:
  assumes "n -as@a#as'→* n'"
  shows "n -as→* sourcenode a" and "valid_edge a" and "targetnode a -as'→* n'"
  using n -as@a#as'→* n'
proof(induct as arbitrary:n)
  case Nil case 1
  thus ?case by(fastforce elim:path.cases intro:empty_path)
next
  case Nil case 2
  thus ?case by(fastforce elim:path.cases intro:path_edge)
next
  case Nil case 3
  thus ?case by(fastforce elim:path.cases)
next
  case (Cons ax asx) 
  note IH1 = n. n -asx@a#as'→* n'  n -asx→* sourcenode a
  note IH2 = n. n -asx@a#as'→* n'  valid_edge a
  note IH3 = n. n -asx@a#as'→* n'  targetnode a -as'→* n'
  { case 1 
    hence "sourcenode ax = n" and "targetnode ax -asx@a#as'→* n'" and "valid_edge ax"
      by(auto elim:path.cases)
    from IH1[OF targetnode ax -asx@a#as'→* n'] 
    have "targetnode ax -asx→* sourcenode a" .
    with sourcenode ax = n valid_edge ax show ?case by(fastforce intro:Cons_path)
  next
    case 2 hence "targetnode ax -asx@a#as'→* n'" by(auto elim:path.cases)
    from IH2[OF this] show ?case .
  next
    case 3 hence "targetnode ax -asx@a#as'→* n'" by(auto elim:path.cases)
    from IH3[OF this] show ?case .
  }
qed


lemma path_split_Cons:
  assumes "n -as→* n'" and "as  []"
  obtains a' as' where "as = a'#as'" and "n = sourcenode a'"
  and "valid_edge a'" and "targetnode a' -as'→* n'"
proof -
  from as  [] obtain a' as' where "as = a'#as'" by(cases as) auto
  with n -as→* n' have "n -[]@a'#as'→* n'" by simp
  hence "n -[]→* sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'"
    by(rule path_split)+
  from n -[]→* sourcenode a' have "n = sourcenode a'" by fast
  with as = a'#as' valid_edge a' targetnode a' -as'→* n' that show ?thesis 
    by fastforce
qed


lemma path_split_snoc:
  assumes "n -as→* n'" and "as  []"
  obtains a' as' where "as = as'@[a']" and "n -as'→* sourcenode a'"
  and "valid_edge a'" and "n' = targetnode a'"
proof -
  from as  [] obtain a' as' where "as = as'@[a']" by(cases as rule:rev_cases) auto
  with n -as→* n' have "n -as'@a'#[]→* n'" by simp
  hence "n -as'→* sourcenode a'" and "valid_edge a'" and "targetnode a' -[]→* n'"
    by(rule path_split)+
  from targetnode a' -[]→* n' have "n' = targetnode a'" by fast
  with as = as'@[a'] valid_edge a' n -as'→* sourcenode a' that show ?thesis 
    by fastforce
qed


lemma path_split_second:
  assumes "n -as@a#as'→* n'" shows "sourcenode a -a#as'→* n'"
proof -
  from n -as@a#as'→* n' have "valid_edge a" and "targetnode a -as'→* n'"
    by(auto intro:path_split)
  thus ?thesis by(fastforce intro:Cons_path)
qed


lemma path_Entry_Cons:
  assumes "(_Entry_) -as→* n'" and "n'  (_Entry_)"
  obtains n a where "sourcenode a = (_Entry_)" and "targetnode a = n"
  and "n -tl as→* n'" and "valid_edge a" and "a = hd as"
proof -
  from (_Entry_) -as→* n' n'  (_Entry_) have "as  []"
    by(cases as,auto elim:path.cases)
  with (_Entry_) -as→* n' obtain a' as' where "as = a'#as'" 
    and "(_Entry_) = sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'"
    by(erule path_split_Cons)
  with that show ?thesis by fastforce
qed


lemma path_det:
  "n -as→* n'; n -as→* n''  n' = n''"
proof(induct as arbitrary:n)
  case Nil thus ?case by(auto elim:path.cases)
next
  case (Cons a' as')
  note IH = n. n -as'→* n'; n -as'→* n''  n' = n''
  from n -a'#as'→* n' have "targetnode a' -as'→* n'" 
    by(fastforce elim:path_split_Cons)
  from n -a'#as'→* n'' have "targetnode a' -as'→* n''" 
    by(fastforce elim:path_split_Cons)
  from IH[OF targetnode a' -as'→* n' this] show ?thesis .
qed


definition
  sourcenodes :: "'edge list  'node list"
  where "sourcenodes xs  map sourcenode xs"

definition
  kinds :: "'edge list  'state edge_kind list"
  where "kinds xs  map kind xs"

definition
  targetnodes :: "'edge list  'node list"
  where "targetnodes xs  map targetnode xs"


lemma path_sourcenode:
  "n -as→* n'; as  []  hd (sourcenodes as) = n"
by(fastforce elim:path_split_Cons simp:sourcenodes_def)



lemma path_targetnode:
  "n -as→* n'; as  []  last (targetnodes as) = n'"
by(fastforce elim:path_split_snoc simp:targetnodes_def)



lemma sourcenodes_is_n_Cons_butlast_targetnodes:
  "n -as→* n'; as  []  
  sourcenodes as = n#(butlast (targetnodes as))"
proof(induct as arbitrary:n)
  case Nil thus ?case by simp
next
  case (Cons a' as')
  note IH = n. n -as'→* n'; as'  []
             sourcenodes as' = n#(butlast (targetnodes as'))
  from n -a'#as'→* n' have "n = sourcenode a'" and "targetnode a' -as'→* n'"
    by(auto elim:path_split_Cons)
  show ?case
  proof(cases "as' = []")
    case True
    with targetnode a' -as'→* n' have "targetnode a' = n'" by fast
    with True n = sourcenode a' show ?thesis
      by(simp add:sourcenodes_def targetnodes_def)
  next
    case False
    from IH[OF targetnode a' -as'→* n' this] 
    have "sourcenodes as' = targetnode a' # butlast (targetnodes as')" .
    with n = sourcenode a' False show ?thesis
      by(simp add:sourcenodes_def targetnodes_def)
  qed
qed



lemma targetnodes_is_tl_sourcenodes_App_n':
  "n -as→* n'; as  []  
    targetnodes as = (tl (sourcenodes as))@[n']"
proof(induct as arbitrary:n' rule:rev_induct)
  case Nil thus ?case by simp
next
  case (snoc a' as')
  note IH = n'. n -as'→* n'; as'  []
     targetnodes as' = tl (sourcenodes as') @ [n']
  from n -as'@[a']→* n' have "n -as'→* sourcenode a'" and "n' = targetnode a'"
    by(auto elim:path_split_snoc)
  show ?case
  proof(cases "as' = []")
    case True
    with n -as'→* sourcenode a' have "n = sourcenode a'" by fast
    with True n' = targetnode a' show ?thesis
      by(simp add:sourcenodes_def targetnodes_def)
  next
    case False
    from IH[OF n -as'→* sourcenode a' this]
    have "targetnodes as' = tl (sourcenodes as')@[sourcenode a']" .
    with n' = targetnode a' False show ?thesis
      by(simp add:sourcenodes_def targetnodes_def)
  qed
qed

lemma Entry_sourcenode_hd:
  assumes "n -as→* n'" and "(_Entry_)  set (sourcenodes as)"
  shows "n = (_Entry_)" and "(_Entry_)  set (sourcenodes (tl as))"
  using n -as→* n' (_Entry_)  set (sourcenodes as)
proof(induct rule:path.induct)
  case (empty_path n) case 1
  thus ?case by(simp add:sourcenodes_def)
next
  case (empty_path n) case 2
  thus ?case by(simp add:sourcenodes_def)
next
  case (Cons_path n'' as n' a n)
  note IH1 = (_Entry_)  set(sourcenodes as)  n'' = (_Entry_)
  note IH2 = (_Entry_)  set(sourcenodes as)  (_Entry_)  set(sourcenodes(tl as))
  have "(_Entry_)  set (sourcenodes(tl(a#as)))"
  proof
    assume "(_Entry_)  set (sourcenodes (tl (a#as)))"
    hence "(_Entry_)  set (sourcenodes as)" by simp
    from IH1[OF this] have "n'' = (_Entry_)" by simp
    with targetnode a = n'' valid_edge a show False by -(erule Entry_target,simp)
  qed
  hence "(_Entry_)  set (sourcenodes(tl(a#as)))" by fastforce
  { case 1
    with (_Entry_)  set (sourcenodes(tl(a#as))) sourcenode a = n
    show ?case by(simp add:sourcenodes_def)
  next
    case 2
    with (_Entry_)  set (sourcenodes(tl(a#as))) sourcenode a = n
    show ?case by(simp add:sourcenodes_def)
  }
qed

end

end