Quelle  Cfg.thy

(* Author: Nan Jiang *)

section ‹The specification of computing dominators›

theory Cfg
imports Main 
begin

text ‹The specification of computing dominators is defined.
 For fast data flow analysis presented by CHK cite‹"Dominance_Algorithm"›,
 a directed graph with explicit node list and sets of initial nodes is defined.
 Each node refers to its rPO (reverse PostOrder) number w.r.t a DFST, and
 related properties as assumptions are handled using a locale.›

type_synonym 'a digraph = "('a ×'a) set"

record 'a graph_rec =
  g_V  :: "'a list"
  g_V0 :: "'a set" 
  g_E  :: "'a digraph"  
 
  tail :: "'a × 'a ==> 'a"
  head :: "'a × 'a ==> 'a"

definition wf_cfg :: "'a graph_rec ==> bool" where
  "wf_cfg G ≡ g_V0 G ⊆ set( g_V G)"

type_synonym node = nat

locale cfg_doms =
  ―‹Nodes are rPO numbers›
  fixes G :: "nat graph_rec" (structure) 

  ―‹General properties›
  assumes wf_cfg: "wf_cfg G"
  assumes tail[simp]: "e = (u,v) ==> tail G e = u"
  assumes head[simp]: "e = (u,v) ==> head G e = v"
  assumes tail_in_verts[simp]: "e ∈ g_E G ==> tail G e ∈ set (g_V G)"
  assumes head_in_verts[simp]: "e ∈ g_E G ==> head G e ∈ set (g_V G)"

  ―‹Properties of a cfg where nodes are rPO numbers›
  assumes entry0:    "g_V0 G = {0}"
  assumes dfst:      "∀v ∈ set (g_V G) - {0}. ∃prev. (prev, v) ∈ g_E G ∧ prev < v" 
  assumes reachable: "∀v ∈ set (g_V G). v ∈ (g_E G)^* `` {0}"    
  assumes verts:     "g_V G = [0 ..< (length (g_V G))]"

 ―‹It is required that the entry node has an immediate successor which is not itself;
 Otherwise, no need to compute dominators
 It is required for proving the lemma: "wf\_dom start (unstables r step start)".›
  assumes succ_of_entry0: "∃s. (0,s) ∈ g_E G ∧ s ≠ 0"

begin

inductive path_entry :: "nat digraph ==> nat list ==> nat ==> bool" for E where
  path_entry0: "path_entry E [] 0"
| path_entry_prepend: "[ (u,v)∈ E; path_entry E l u ] ==> path_entry E (u#l) v"

lemma path_entry0_empty_conv: "path_entry E [] v ⟷ v = 0" 
 by (auto intro: path_entry0 elim: path_entry.cases)

inductive_cases path_entry_uncons: "path_entry E (u'#l) w"
inductive_simps path_entry_cons_conv: "path_entry E (u'#l) w"

lemma single_path_entry: "path_entry E [p] w ==> p = 0" 
  by (simp add: path_entry_cons_conv path_entry0_empty_conv)

lemma path_entry_append: 
  "[ path_entry E l v; (v,w)∈E ] ==> path_entry E (v#l) w"
  by (rule path_entry_prepend)

lemma entry_rtrancl_is_path:
  assumes "(0,v) ∈ E^*"
  obtains p where "path_entry E p v" 
    using assms 
    by induct (auto intro:path_entry0 path_entry_prepend)

lemma path_entry_is_trancl: 
  assumes "path_entry E l v"
  and "l ≠ []"
  shows "(0,v)∈E⁺"
  using assms 
  apply induct
  apply auto []
  apply (case_tac l)
  apply (auto simp add:path_entry0_empty_conv)
  done

lemma tail_is_vert: "(u,v) ∈ g_E G ==> u ∈ set (g_V G)"
  by (auto dest: tail_in_verts[of "(u,v)"])

lemma head_is_vert: "(u,v) ∈ g_E G ==> v ∈ set (g_V G)"
  by (auto dest: head_in_verts[of "(u,v)"])

lemma tail_is_vert2: "(u,v) ∈ (g_E G)⁺ ==> u ∈ set (g_V G)"
  by (induct rule:trancl.induct)(auto dest: tail_in_verts)

lemma head_is_vert2: "(u,v) ∈ (g_E G)⁺ ==> v ∈ set (g_V G)"
  by (induct rule:trancl.induct)(auto dest: head_in_verts)

lemma verts_set: "set (g_V G) = {0 ..< length (g_V G)}"   
proof-
  from verts have "set (g_V G) = set [0 ..< (length (g_V G))]" by simp
  also have "set [0 ..< (length (g_V G))] = {0 ..< (length (g_V G))}" by simp
  ultimately show ?thesis by auto
qed

lemma fin_verts: "finite (set (g_V G))" 
  by (auto)

lemma zero_in_verts: "0 ∈ set (g_V G)"
  using wf_cfg entry0 by (unfold wf_cfg_def)  auto

lemma verts_not_empty: "g_V G ≠ []"
  using zero_in_verts by auto

lemma len_verts_gt0: "length (g_V G) > 0" 
  by (simp add:verts_not_empty)

lemma len_verts_gt1: "length (g_V G) > 1"
proof-
  from succ_of_entry0 obtain s where "s ∈ set (g_V G)" and "s ≠ 0" using head_is_vert by auto
  with zero_in_verts have "{0,s} ⊆ set (g_V G)" and c: "card {0, s} > 1" by auto
  then have "card {0, s} ≤ card (set (g_V G))" by (auto simp add:card_mono)
  with c have "card (set (g_V G)) > 1" by simp
  then show ?thesis using card_length[of "g_V G"] by auto
qed

lemma verts_ge_Suc0 : "¬ [0..<length (g_V G)] = [0]"
proof
  assume "[0..<length (g_V G)] = [0]"
  then have "length [0..<length (g_V G)] = 1" by simp
  with len_verts_gt1 show False by auto
qed

lemma distinct_verts1: "distinct [0..<length (g_V G)] " 
  by simp

lemma distinct_verts2: "distinct (g_V G)" 
  by (insert distinct_verts1 verts)  simp

lemma single_entry: "is_singleton (g_V0 G)" 
  by (simp add:entry0)

lemma entry_is_0: "the_elem (g_V0 G) = 0" 
  by (simp add: entry0)

lemma wf_digraph: "cfg_doms G" by intro_locales

lemma path_entry_prepend_conv: "path_entry (g_E G) p n ==> p ≠ [] ==> ∃v. path_entry (g_E G) (tl p) v ∧ (v, n) ∈ (g_E G)" 
proof (induct rule:path_entry.induct)
  case path_entry0 then show ?case by auto
next
  case (path_entry_prepend u v l) 
  then show ?case by auto
qed

lemma path_verts: "path_entry (g_E G) p n ==> n ∈ set (g_V G)" 
proof (cases "p = []")
  case True
  assume "path_entry (g_E G) p n" and "p = []"
  then show ?thesis by (simp add:path_entry0_empty_conv zero_in_verts)
next
  case False
  assume "path_entry (g_E G) p n" and "p ≠ []"
  then have "(0,n)∈(g_E G)⁺" by (auto simp add:path_entry_is_trancl)
  then show ?thesis using head_is_vert2 by simp
qed

lemma path_in_verts: 
  assumes "path_entry (g_E G) l v"
    shows "set l ⊆ set (g_V G)"
  using assms 
proof (induct rule:path_entry.induct)
  case path_entry0 then show ?case by auto
next
  case (path_entry_prepend u v l) 
  then show ?case using path_verts by auto
qed

lemma any_node_exits_path: 
  assumes "v ∈ set (g_V G) "
    shows "∃p. path_entry (g_E G) p v" 
  using assms
proof (cases "v = 0")
  assume "v ∈ set (g_V G)" and "v = 0" 
  have "path_entry (g_E G) [] 0" by (auto simp add:path_entry0)
  then show ?thesis using ‹v = 0› by auto
next
  assume "v ∈ set (g_V G)" and "v ≠ 0" 
  with reachable have "v ∈ (g_E G)^* `` {0}" by auto
  then have "(0,v) ∈ (g_E G)^*"  by (simp add:Image_iff)
  then show ?thesis by (auto intro:entry_rtrancl_is_path)
qed

lemma entry0_path: "path_entry (g_E G) [] 0"
  by (auto simp add:path_entry.path_entry0)

definition reachable :: "node ==> bool" 
  where "reachable v ≡ v ∈ (g_E G)^* `` {0}"

lemma path_entry_reachable: 
  assumes "path_entry (g_E G) p n"
    shows "reachable n" 
  using assms reachable 
  by (fastforce intro:path_verts simp add:reachable_def)

lemma nin_nodes_reachable: "n ∉ set (g_V G) ==> ¬ reachable n"
proof(rule ccontr)
  assume "n ∉ set (g_V G)" and nn: " ¬ ¬ reachable n"
  from ‹n ∉ set (g_V G)› have "n ≠ 0" using verts_set len_verts_gt0 entry0  by auto
  from nn have "reachable n" by auto
  then have "n ∈ (g_E G)^* `` {0}" by (simp add: reachable_def)
  then have " (0, n) ∈ (g_E G)^* " by (auto simp add:Image_def)  
  with ‹n ≠ 0› have "∃n'. (0,n') ∈ (g_E G)^* ∧ (n', n) ∈ (g_E G)" by (auto intro:rtranclE)
  then obtain n' where "(0,n') ∈ (g_E G)^* " and " (n', n) ∈ (g_E G)"by auto
  then have "n ∈ set (g_V G)" using head_is_vert by auto
  with ‹n ∉ set (g_V G)› show False
    by auto
qed

lemma reachable_path_entry: "reachable n ==> ∃p. path_entry (g_E G) p n" 
proof-
  assume "reachable n"
  then have "(0,n) ∈ (g_E G)^*" by (auto simp add:reachable_def Image_iff)
  then have "0 = n ∨ 0 ≠ n ∧ (0,n) ∈ (g_E G)⁺" by (auto simp add: rtrancl_eq_or_trancl)
  then show ?thesis 
  proof
    assume "0 = n" 
    have "path_entry (g_E G) [] 0" by (simp add:path_entry0)
    with ‹0 = n› show ?thesis by auto
  next
    assume "0 ≠ n ∧ (0,n) ∈ (g_E G)⁺"
    then have "(0,n) ∈ (g_E G)⁺"  by (auto simp add:rtranclpD)
    then have "n ∈ set (g_V G)" by (simp add:head_is_vert2)
    then show ?thesis by (rule any_node_exits_path)
  qed
qed

lemma path_entry_unconc:
  assumes "path_entry (g_E G) (la@lb) w"
  obtains v where "path_entry (g_E G) lb v"
  using assms 
  apply (induct "la@lb" w arbitrary:la lb rule: path_entry.induct)
   apply (fastforce intro:path_entry.intros)
  by (auto intro:path_entry.intros iff add: Cons_eq_append_conv)

lemma path_entry_append_conv:
  "path_entry (g_E G) (v#l) w ⟷ (path_entry (g_E G) l v ∧ (v,w) ∈ (g_E G))"
proof
  assume "path_entry (g_E G) (v # l) w " 
  then show "path_entry (g_E G) l v ∧ (v, w) ∈ g_E G" 
    by (auto simp add:path_entry_cons_conv)   
next
  assume "path_entry (g_E G) l v ∧ (v, w) ∈ g_E G"
  then show "path_entry (g_E G) (v # l) w " by (fastforce intro: path_entry_append)
qed

lemma takeWhileNot_path_entry:
  assumes "path_entry E p x"
      and "v ∈ set p"
      and "takeWhile ((≠) v) (rev p) = c"
    shows "path_entry E (rev c) v"
  using assms
proof (induct rule: path_entry.induct)
  case path_entry0 
  then show ?case by auto
next
  case (path_entry_prepend u va l)
  then show ?case
  proof(cases "v ∈ set l")
    case True note v_in = this
    then have "takeWhile ((≠) v) (rev (u # l)) = takeWhile ((≠) v) (rev l)" by auto
    with path_entry_prepend.prems(2) have "takeWhile ((≠) v) (rev l) = c" by simp
    with v_in show ?thesis using path_entry_prepend.hyps(3) by auto
  next
    case False note v_nin = this    
    with path_entry_prepend.prems(1) have v_u: "v = u" by auto
    then have take_eq: "takeWhile ((≠) v) (rev (u # l)) = takeWhile ((≠) v) ((rev l) @ [u])"  by auto 
    from v_nin have "∧x. x ∈ set (rev l) ==> ((≠) v) x" by auto
    then have "takeWhile ((≠) v) ((rev l) @ [u]) = (rev l) @ takeWhile ((≠) v) [u]" 
      by (rule takeWhile_append2) simp
    with v_u take_eq have "takeWhile ((≠) v) (rev (u # l)) = (rev l)" by simp
    then show ?thesis using path_entry_prepend.prems(2) path_entry_prepend.hyps(2) v_u by auto
  qed
qed

lemma path_entry_last: "path_entry (g_E G) p n ==> p ≠ [] ==> last p = 0" 
  apply (induct rule: path_entry.induct)
   apply simp  
  apply (simp add: path_entry_cons_conv neq_Nil_conv)
  apply (auto simp add:path_entry0_empty_conv)
  done

lemma path_entry_loop: 
  assumes n_path: "path_entry (g_E G) p n"
      and n:      "n ∈ set p "
    shows "∃p'. path_entry (g_E G) p' n ∧ n ∉ set p'" 
  using assms
proof -
  let ?c = "takeWhile ((≠) n) (rev ( p))"
  have "∀z ∈ set ?c. z ≠ n" by (auto dest: set_takeWhileD)
  then have n_nin: "n ∉ set (rev ?c)" by auto
 
  from n_path  obtain v where "path_entry (g_E G) ( p) v" using path_entry_prepend_conv by auto  
  with n have "path_entry (g_E G) (rev ?c) n" by (auto intro:takeWhileNot_path_entry)  
  with n_nin show ?thesis by fastforce
qed

lemma path_entry_hd_edge: 
  assumes "path_entry (g_E G) pa p "   
      and "pa ≠ []"
    shows "(hd pa, p) ∈ (g_E G)" 
  using assms
  by (induct rule: path_entry.induct) auto

lemma path_entry_edge: 
  assumes "pa ≠ [] "
      and "path_entry (g_E G) pa p "
    shows "∃u∈set pa. (path_entry (g_E G) (rev (takeWhile ((≠) u) (rev pa))) u) ∧ (u,p) ∈ (g_E G)"
  using assms
proof-
  from assms have 1: "path_entry (g_E G) (rev (takeWhile ((≠) (hd pa)) (rev pa))) (hd pa)" by (auto intro:takeWhileNot_path_entry)
  from assms have 2: "(hd pa, p)∈ (g_E G)" by (auto intro: path_entry_hd_edge)
  have "hd pa ∈ set pa" using assms(1) by auto
  with 1 2 show ?thesis by auto
qed

definition is_tail :: "node ==> node × node ==> bool"
  where "is_tail v e = (v = tail G e)"

definition is_head :: "node ==> node × node ==> bool"
  where "is_head v e = (v = head G e)"

definition succs:: "node ==> node set"
  where "succs v = (g_E G) `` {v}"

lemma succ_in_verts: "s ∈ succs n ==> {s,n} ⊆ set (g_V G)"
  by( simp add:succs_def tail_is_vert head_is_vert)

lemma succ0_not_nil: "succs 0 ≠ {}"
  using succ_of_entry0 by (auto simp add:succs_def)

definition prevs:: "node ==> node set" where
  "prevs v = (converse (g_E G))`` {v}"

lemma "v ∈ succs u ⟷ u ∈ prevs v"
  by (auto simp add:succs_def prevs_def)

lemma succ_edge: "∀v ∈ succs n. (n,v) ∈ g_E G"
  by (auto simp add:succs_def)

lemma prev_edge: "u ∈ set (g_V G) ==> ∀v ∈ prevs u. (v, u) ∈ g_E G"
  by (auto simp add:prevs_def)

lemma succ_in_G: "∀v ∈ succs n. v ∈ set (g_V G)"  
  by (auto simp add: succs_def dest:head_in_verts)

lemma succ_is_subset_of_verts: "∀v ∈ set (g_V G). succs v ⊆ set(g_V G)"
  by (insert succ_in_G) auto

lemma fin_succs: "∀v ∈ set (g_V G). finite (succs v)"
  by (insert succ_is_subset_of_verts) (auto intro:rev_finite_subset)

lemma fin_succs': "v < length (g_V G) ==> finite (succs v)" 
  by (subgoal_tac "v ∈ set (g_V G)")
   (auto simp add: fin_succs verts_set)

lemma succ_range: "∀v ∈ succs n. v < length (g_V G)" 
  by (insert succ_in_G verts_set) auto

lemma path_entry_gt: 
  assumes "∀p. path_entry E p n ⟶ d ∈ set p"
      and "∀p. path_entry E p n' ⟶ n ∈ set p"
    shows "∀p. path_entry E p n' ⟶ d ∈ set p" 
  using assms
proof (intro strip)
  fix p
  let ?npath = "takeWhile ((≠) n) (rev p)" 
  have sub: "set ?npath ⊆ set p" apply (induct p) by (auto dest:set_takeWhileD)

  assume ass: "path_entry E p n' "
  with assms(2) have n_in_p: "n ∈ set p" by auto
  then have "n ∈ set (rev p)" by auto
  with ass have "path_entry E (rev ?npath) n" 
    using takeWhileNot_path_entry by auto
  with assms(1) have "d ∈ set ?npath" by fastforce   
  with sub show "d ∈ set p" by auto
qed

definition dominate :: "nat ==> nat ==> bool" 
  where "dominate n1 n2 ≡
         ∀pa. path_entry (g_E G) pa n2 ⟶
         (n1 ∈ set pa ∨ n1 = n2)"

definition strict_dominate:: "nat ==> nat ==> bool" where
  "strict_dominate n1 n2 ≡
   ∀pa. path_entry (g_E G) pa n2 ⟶
   (n1 ∈ set pa ∧ n1 ≠ n2)"

lemma any_dominate_unreachable: "¬ reachable n ==> dominate d n"
proof(unfold reachable_def dominate_def)
  assume ass: "n ∉ (g_E G)^* `` {0}"

  have "¬ (∃p. path_entry (g_E G) p n)" 
  proof (rule ccontr)
    assume " ¬ (¬ (∃p. path_entry (g_E G) p n))"
    then obtain p where p: "path_entry (g_E G) p n" by auto
    then have "n = 0 ∨ reachable n" by (auto intro:path_entry_reachable)
    then show False
    proof
      assume "n = 0" 
      then show False using ass by auto
    next
      assume "reachable n" 
      then show False using ass by (auto simp add:reachable_def)
    qed
  qed
  then show "∀pa. path_entry (g_E G) pa n ⟶ d ∈ set pa ∨ d = n" by auto
qed

lemma any_sdominate_unreachable: "¬ reachable n ==> strict_dominate d n"
proof(unfold reachable_def strict_dominate_def)
  assume ass:"n ∉ (g_E G)^* `` {0} "

  have "¬ (∃p. path_entry (g_E G) p n)" 
  proof (rule ccontr)
    assume " ¬ (¬ (∃p. path_entry (g_E G) p n))"
    then obtain p where p: "path_entry (g_E G) p n" by auto
    then have "n = 0 ∨ reachable n" by (auto intro:path_entry_reachable)
    then show False    
    proof 
      assume "n = 0" 
      then show False using ass by auto
    next
      assume "reachable n" 
      then show False using ass by (auto simp add:reachable_def)
    qed
  qed
  then show "∀pa. path_entry (g_E G) pa n ⟶ d ∈ set pa ∧ d ≠ n" by auto
qed

lemma dom_reachable: "reachable n ==> dominate d n ==> reachable d"
proof -
  assume reach_n: "reachable n"
     and dom_n: "dominate d n" 
  from reach_n have "∃p. path_entry (g_E G) p n" by (rule reachable_path_entry)
  then obtain p where p: "path_entry (g_E G) p n" by auto

  show "reachable d"
  proof (cases "d ≠ n")
    case True     
    with dom_n p have d_in: "d ∈ set p" by (auto simp add:dominate_def)
    let ?pa = "takeWhile ((≠) d) (rev p)"
    from d_in p have "path_entry (g_E G) (rev ?pa) d" using takeWhileNot_path_entry by auto
    then show ?thesis using path_entry_reachable by auto
  next
    case False
    with reach_n show ?thesis by auto
  qed
qed

lemma dominate_refl: "dominate n n" 
  by (simp add:dominate_def)

lemma entry0_dominates_all: "∀p ∈ set (g_V G). dominate 0 p"  
proof(intro strip)  
  fix p 
  assume "p ∈ set (g_V G)"
  show "dominate 0 p" 
  proof (cases "p = 0")
    case True
    then show ?thesis by (auto simp add:dominate_def)
  next
    case False
    assume p_neq0: "p ≠ 0"
    have "∀pa. path_entry (g_E G) pa p ⟶ 0 ∈ set pa"
    proof (intro strip)
      fix pa
      assume path_p: "path_entry (g_E G) pa p"
      show "0 ∈ set pa"
      proof (cases "pa ≠ []")
        case True note pa_n_nil = this
        with path_p have last_pa: "last pa = 0" using path_entry_last by auto
        from pa_n_nil have "last pa ∈ set pa" by simp
        with last_pa show ?thesis by simp
      next
        case False 
        with path_p have "p = 0" by (simp add:path_entry0_empty_conv)
        with p_neq0 show ?thesis by auto
      qed
    qed
    then show ?thesis by (auto simp add:dominate_def)
  qed
qed

lemma "strict_dominate i j ==> j ∈ set (g_V G) ==> i ≠ j" 
  using  any_node_exits_path
  by (auto simp add:strict_dominate_def)

definition non_strict_dominate:: "nat ==> nat ==> bool" where
  "non_strict_dominate n1 n2 ≡ ∃pa. path_entry (g_E G) pa n2 ∧ (n1 ∉ set pa)"

lemma any_sdominate_0: "n ∈ set (g_V G) ==> non_strict_dominate n 0"
  apply (simp add:non_strict_dominate_def)
  by (auto intro:path_entry0)

(*
lemma non_strict_dominate_refl: "n \<in> set (g_V G) \<Longrightarrow> non_strict_dominate n n"
proof(unfold non_strict_dominate_def)
  assume n_in: "n \<in> set (g_V G)"
  then obtain p where p_n: "path_entry (g_E G) p n" using any_node_exits_path by auto

  have pa0: "path_entry (g_E G) [] 0" by (rule path_entry0)

  show "\<exists>pa. path_entry (g_E G) pa n \<and> n \<notin> set pa"
  proof(cases "n = 0")
    case True 
    then show ?thesis using pa0 by (auto simp add:non_strict_dominate_def)
  next 
    case False note n_neq_0 = this 
    with p_n have "p \<noteq> []" using path_entry0_empty_conv by auto 
    then show ?thesis using p_n by (auto intro: path_entry_loop)    
  qed
qed
*)
lemma non_sdominate_succ: "(i,j ) ∈ g_E G ==> k ≠ i ==> non_strict_dominate k i ==> non_strict_dominate k j" 
proof -
  assume i_j: "(i,j ) ∈ g_E G" and k_neq_i: "k ≠ i" and "non_strict_dominate k i"
  then obtain pa where "path_entry (g_E G) pa i" and k_nin_pa: "k ∉ set pa" by (auto simp add:non_strict_dominate_def)
  with i_j have "path_entry (g_E G) (i#pa) j" by (auto simp add:path_entry_prepend)
  with k_neq_i k_nin_pa show ?thesis by (auto simp add:non_strict_dominate_def)
qed

lemma any_node_non_sdom0: "non_strict_dominate k 0"
  by (auto intro:entry0_path simp add:non_strict_dominate_def)

lemma nonstrict_eq: "non_strict_dominate i j ==> ¬ strict_dominate i j" 
  by (auto simp add:non_strict_dominate_def strict_dominate_def)

lemma dominate_trans: 
  assumes "dominate n1 n2"
      and "dominate n2 n3"
    shows "dominate n1 n3"
  using assms
proof(cases "n1 = n2")
  case True
  then show ?thesis using assms(2) by auto
next
  case False
  then show "dominate n1 n3"
  proof (cases "n1 = n3")
    case True
    then show ?thesis by (auto simp add:dominate_def)
  next
    case False
    show "dominate n1 n3" 
    proof (cases "n2 = n3")
      case True
      then show ?thesis using assms(1) by auto
    next
      case False
      with ‹n1 ≠ n2› ‹n1 ≠ n3› show ?thesis
      proof (auto simp add: dominate_def)
        fix pa
        assume "n1 ≠ n2" and "n1 ≠ n3" and "n2 ≠ n3"
        from ‹n1 ≠ n2› assms(1) have n1_n2_pa: "∀pa. path_entry (g_E G) pa n2 ⟶ n1 ∈ set pa" 
          by (auto simp add:dominate_def)
        from ‹n2 ≠ n3› assms(2) have "∀pa. path_entry (g_E G) pa n3 ⟶ n2 ∈ set pa" 
          by (auto simp add:dominate_def)
        with n1_n2_pa have "∀pa. path_entry (g_E G) pa n3 ⟶ n1 ∈ set pa" 
          by (rule path_entry_gt)
        then show "∧pa. path_entry (g_E G) pa n3 ==> n1 ∈ set pa" by auto
      qed
    qed
  qed
qed

lemma len_takeWhile_lt: "x ∈ set xs ==> length (takeWhile ((≠) x) xs) < length xs"
  by (induct xs) auto

lemma len_takeWhile_comp: 
  assumes "n1 ∈ set xs"
      and "n2 ∈ set xs"
      and "n1 ≠ n2"
    shows "length (takeWhile ((≠) n1) xs) ≠ length (takeWhile ((≠) n2) xs)"
  using assms
  by (induct xs) auto

lemma len_takeWhile_comp1: 
  assumes "n1 ∈ set xs"
      and "n2 ∈ set xs"
      and "n1 ≠ n2"
    shows "length (takeWhile ((≠) n1) (rev (x # xs))) ≠ length (takeWhile ((≠) n2) (rev (x # xs)))"
  using assms len_takeWhile_comp[of "n1" "rev xs" "n2"] by fastforce

lemma len_takeWhile_comp2: 
  assumes "n1 ∈ set xs"
      and "n2 ∉ set xs"
    shows "length (takeWhile ((≠) n1) (rev (x # xs))) ≠ length (takeWhile ((≠) n2) (rev (x # xs)))"
  using assms
proof-
  let ?xs1 = "takeWhile ((≠) n1) (rev (x # xs))"
  let ?xs2 = "takeWhile ((≠) n2) (rev (x # xs))"
  from assms have len1: "length (takeWhile ((≠) n1) (rev xs)) < length (rev xs)" 
    using len_takeWhile_lt[of _"rev xs"] by auto

  from assms(1) have "?xs1 = takeWhile ((≠) n1) (rev xs)" by auto
  then have len2: "length ?xs1 < length (rev xs)" using len1 by auto
  
  from assms(2) have "takeWhile ((≠) n2) (rev xs @ [x]) = (rev xs) @ takeWhile ((≠) n2) [x]" 
    by (fastforce intro:takeWhile_append2)
  then have "?xs2 = (rev xs) @ takeWhile ((≠) n2) [x]" by simp
  then show ?thesis using len2 by auto 
qed

lemma len_compare1: 
  assumes "n1 = x" and "n2 ≠ x"
    shows "length (takeWhile ((≠) n1) (rev (x # xs))) ≠ length (takeWhile ((≠) n2) (rev (x # xs)))"
  using assms
proof(cases "n1 ∈ set xs ∧ n2 ∈ set xs")
  case True
  with assms show ?thesis using len_takeWhile_comp1 by fastforce
next
  let ?xs1 = "takeWhile ((≠) n1) (rev (x # xs))"
  let ?xs2 = "takeWhile ((≠) n2) (rev (x # xs))"

  case False
  then have "n1 ∈ set xs ∧ n2 ∉ set xs ∨ n1 ∉ set xs ∧ n2 ∈ set xs ∨ n1 ∉ set xs ∧ n2 ∉ set xs" by auto
  then show ?thesis
  proof
    assume "n1 ∈ set xs ∧ n2 ∉ set xs"
    then show ?thesis by (fastforce dest: len_takeWhile_comp2)
  next
    assume "n1 ∉ set xs ∧ n2 ∈ set xs ∨ n1 ∉ set xs ∧ n2 ∉ set xs"
    then show ?thesis 
    proof
      assume "n1 ∉ set xs ∧ n2 ∈ set xs"
      then have n1: "n1 ∉ set xs" and n2: "n2 ∈ set xs" by auto
      have "length ?xs2 ≠ length ?xs1" using len_takeWhile_comp2[OF n2 n1] by auto
      then show ?thesis by simp
    next
      assume "n1 ∉ set xs ∧ n2 ∉ set xs"
      then have n1_nin: "n1 ∉ set xs" and n2_nin: "n2 ∉ set xs" by auto
      then  have t1: "takeWhile ((≠) n1) (rev xs @ [x]) = (rev xs) @ takeWhile ((≠) n1) [x]" 
             and     "takeWhile ((≠) n2) (rev xs @ [x]) = (rev xs) @ takeWhile ((≠) n2) [x]" 
        by (fastforce intro:takeWhile_append2)+
      with ‹n1 = x› ‹n2 ≠ x›  have t1': "takeWhile ((≠) n1) (rev xs @ [x]) = rev xs" 
                               and      "takeWhile ((≠) n2) (rev xs @ [x]) = (rev xs) @ [x]" by auto      
      then have "length (takeWhile ((≠) n2) (rev xs @ [x])) = length ((rev xs) @ [x])" 
        using arg_cong[of "takeWhile ((≠) n2) (rev xs @ [x])" "rev xs @ [x]" "length"] by fastforce       
      with t1' show ?thesis by auto
    qed
  qed
qed

lemma len_compare2: 
  assumes "n1 ∈ set xs"
      and "n1 ≠ n2"
    shows "length (takeWhile ((≠) n1) (rev (x # xs))) ≠ length (takeWhile ((≠) n2) (rev (x # xs)))"
  using assms 
  apply(case_tac "n2 ∈ set xs") 
   apply (fastforce dest: len_takeWhile_comp1 ) 
  apply (fastforce dest:len_takeWhile_comp2)
  done

lemma len_takeWhile_set: 
  assumes "length (takeWhile ((≠) n1) xs) > length (takeWhile ((≠) n2) xs)"
      and "n1 ≠ n2"
      and "n1 ∈ set xs" 
      and "n2 ∈ set xs"
    shows "set (takeWhile ((≠) n2) xs) ⊆ set (takeWhile ((≠) n1) xs)"
  using assms
proof (induct xs)
  case Nil then show ?case by auto
next
  case (Cons y ys)
  note ind_hyp = Cons(1)
  note len_n2_lt_n1_y_ys = Cons(2)
  note n1_n_n2 = Cons(3)
  note n1_in_y_ys = Cons(4)
  note n2_in_y_ys = Cons(5)
 
  let ?ys1_take = "takeWhile ((≠) n1) ys"
  let ?ys2_take = "takeWhile ((≠) n2) ys"

  show ?case
  proof(cases "n1 ∈ set ys")
    case True note n1_in_ys = this
    show ?thesis 
    proof(cases "n2 ∈ set ys")
      case True note n2_in_ys = this
      show ?thesis 
      proof (cases "n1 ≠ y")
        case True note n1_neq_y = this
        show ?thesis 
        proof (cases "n2 ≠ y")
          case True note n2_neq_y = this
          from len_n2_lt_n1_y_ys have "length ?ys2_take < length ?ys1_take" 
            using n1_n_n2 n1_in_ys n2_in_ys n1_neq_y n2_neq_y by (induct ys) auto
          from ind_hyp[OF this n1_n_n2 n1_in_ys n2_in_ys]
          have "set (takeWhile ((≠) n2) ys) ⊆ set (takeWhile ((≠) n1) ys)" by auto
          then show ?thesis using n1_neq_y n2_neq_y by (induct ys) auto
        next
          case False
          with n1_n_n2 show ?thesis by auto
        qed
      next
        case False 
        with n1_n_n2 show ?thesis using len_n2_lt_n1_y_ys by auto
      qed
    next
      case False
      with n2_in_y_ys have "n2 = y" by auto
      then show ?thesis by auto
    qed
  next
    case False
    with n1_in_y_ys have "n1 = y" by auto
    with n1_n_n2 show ?thesis using len_n2_lt_n1_y_ys by auto
  qed
qed
    
lemma reachable_dom_acyclic:
  assumes "reachable n2"
      and "dominate n1 n2"
      and "dominate n2 n1"
    shows "n1 = n2" 
  using assms 
proof -
  from assms(1) assms(2) have "reachable n1" by (auto intro: dom_reachable)
  then have "∃pa. path_entry (g_E G) pa n1" by (auto intro: reachable_path_entry)
  then obtain pa where pa: "path_entry (g_E G) pa n1" by auto

  let ?n_take_n1 = "takeWhile ((≠) n1) (rev pa)"
  let ?n_take_n2 = "takeWhile ((≠) n2) (rev pa)"

  show "n1 = n2" 
  proof(rule ccontr)
    assume n1_neq_n2:  "n1 ≠ n2" 
    then have pa_n1_n2: "∀pa. path_entry (g_E G) pa n2 ⟶ n1 ∈ set pa" 
          and pa_n2_n1: "∀pa. path_entry (g_E G) pa n1 ⟶ n2 ∈ set pa" using assms(2) assms(3)
      by (auto simp add:dominate_def)
    then have n1_n1_pa: "∀pa. path_entry (g_E G) pa n1 ⟶ n1 ∈ set pa" by (rule path_entry_gt)
    with pa pa_n2_n1 have n1_in_pa: "n1 ∈ set pa" 
                      and n2_in_pa: "n2 ∈ set pa" by auto
    with n1_neq_n2 have len_neq: "length ?n_take_n1 ≠ length ?n_take_n2" 
      by (auto simp add: len_takeWhile_comp)
    
    from pa n1_in_pa n2_in_pa have path1: "path_entry (g_E G) (rev ?n_take_n1) n1"  
                               and path2: "path_entry (g_E G) (rev ?n_take_n2) n2"  
      using takeWhileNot_path_entry by auto

    have n1_not_in: "n1 ∉ set ?n_take_n1" by (auto dest: set_takeWhileD[of _ _ "rev pa"])
    have n2_not_in: "n2 ∉ set ?n_take_n2" by (auto dest: set_takeWhileD[of _ _ "rev pa"])

    show False
    proof(cases "length ?n_take_n1 > length ?n_take_n2")
      case True
      then have "set ?n_take_n2 ⊆ set ?n_take_n1" 
        using n1_in_pa n2_in_pa by (auto dest: len_takeWhile_set[of _ "rev pa"])       
      then have "n1 ∉ set ?n_take_n2 " using n1_not_in by auto
      with path2 show False using pa_n1_n2 by auto
    next
      case False
      with len_neq have "length ?n_take_n2 > length ?n_take_n1" by auto
      then have "set ?n_take_n1 ⊆ set ?n_take_n2" 
        using n1_neq_n2 n2_in_pa n1_in_pa  by (auto dest: len_takeWhile_set)  
      then have "n2 ∉ set ?n_take_n1 " using n2_not_in by auto
      with path1 show False using pa_n2_n1 by auto
    qed
  qed
qed

lemma sdom_dom: "strict_dominate n1 n2 ==> dominate n1 n2" 
  by (auto simp add:strict_dominate_def dominate_def)

lemma dominate_sdominate: "dominate n1 n2 ==> n1 ≠ n2 ==> strict_dominate n1 n2" 
  by (auto simp add:strict_dominate_def dominate_def)

lemma sdom_neq: 
  assumes "reachable n2"
      and "strict_dominate n1 n2"
    shows "n1 ≠ n2" 
  using assms
proof -
  from assms(1) have "∃p. path_entry (g_E G) p n2" by (rule reachable_path_entry) 
  then obtain p where "path_entry (g_E G) p n2" by auto
  with assms(2) show ?thesis by (auto simp add:strict_dominate_def)
qed
  
lemma reachable_dom_acyclic2:
  assumes "reachable n2 "
      and "strict_dominate n1 n2"
    shows "¬ dominate n2 n1" 
  using assms
proof -
  from assms have n1_dom_n2: "dominate n1 n2" and n1_neq_n2: "n1 ≠ n2" 
    by (auto simp add:sdom_dom sdom_neq)
  with assms(1) have "dominate n2 n1 ==> n1 = n2" using reachable_dom_acyclic by auto
  with n1_neq_n2 show ?thesis by auto
qed

lemma not_dom_eq_not_sdom: "¬ dominate n1 n2 ==> ¬ strict_dominate n1 n2" 
  by (auto simp add:strict_dominate_def dominate_def)

lemma reachable_sdom_acyclic:
  assumes "reachable n2"
      and "strict_dominate n1 n2"
    shows "¬ strict_dominate n2 n1" 
  using assms 
  apply (insert reachable_dom_acyclic2[OF assms(1) assms(2)])
  by (auto simp add:not_dom_eq_not_sdom) 

lemma strict_dominate_trans1: 
  assumes "strict_dominate n1 n2" 
      and "dominate n2 n3" 
    shows "strict_dominate n1 n3" 
  using assms
proof (cases "reachable n2")
  case True note reach_n2 = this
  with assms(1) have n1_dom_n2: "dominate n1 n2" and n1_neq_n2: "n1 ≠ n2"
    by (auto simp add:sdom_dom sdom_neq)
  with assms(2) have n1_dom_n3: "dominate n1 n3" by (auto intro: dominate_trans)
  have n1_neq_n3: "n1 ≠ n3"
  proof (rule ccontr)
    assume "¬ n1 ≠ n3" then have "n1 = n3" by simp
    with assms(2) have n2_dom_n1: "dominate n2 n1" by simp
    with reach_n2 n1_dom_n2 have "n1 = n2" by (auto dest:reachable_dom_acyclic)
    with n1_neq_n2 show False by auto
  qed
  with n1_dom_n3 show ?thesis by (simp add:strict_dominate_def dominate_def)
next
  case False note not_reach_n2 = this
  have "¬ reachable n3" 
  proof (rule ccontr)
    assume "¬ ¬ reachable n3 " 
    with assms(2) have "reachable n2" by (auto intro: dom_reachable)
    with not_reach_n2 show False by auto
  qed
  then show ?thesis by (auto intro:any_sdominate_unreachable)
qed

lemma strict_dominate_trans2: 
  assumes "dominate n1 n2" 
      and "strict_dominate n2 n3" 
    shows "strict_dominate n1 n3" 
  using assms
proof (cases "reachable n3")
  case True
  with assms(2) have n2_dom_n3: "dominate n2 n3" and n1_neq_n2: "n2 ≠ n3"
    by (auto simp add:sdom_dom sdom_neq)
  with assms(1) have n1_dom_n3: "dominate n1 n3" by (auto intro: dominate_trans)
  have n1_neq_n3: "n1 ≠ n3"
  proof (rule ccontr)
    assume "¬ n1 ≠ n3" then have "n1 = n3" by simp
    with assms(1) have "dominate n3 n2" by simp
    with ‹reachable n3› n2_dom_n3 have "n2 = n3" by (auto dest:reachable_dom_acyclic)
    with n1_neq_n2 show False by auto
  qed
  with n1_dom_n3 show ?thesis by (simp add:strict_dominate_def dominate_def)
next
  case False
  then have "¬ reachable n3" by simp
  then show ?thesis by (auto intro:any_sdominate_unreachable)
qed

lemma strict_dominate_trans: 
  assumes "strict_dominate n1 n2"
      and "strict_dominate n2 n3"
    shows "strict_dominate n1 n3"
  using assms
  apply(subgoal_tac "dominate n2 n3")
   apply(rule strict_dominate_trans1)
  apply (auto simp add: strict_dominate_def dominate_def)
  done

lemma sdominate_dominate_succs: 
  assumes i_sdom_j:    "strict_dominate i j"
      and j_in_succ_k: "j ∈ succs k"
    shows              "dominate i k"
proof (rule ccontr)
  assume ass:"¬ dominate i k" 
  then obtain p where path_k: "path_entry (g_E G) p k" and i_nin_p: "i ∉ set p" by (auto simp add:dominate_def)
  with j_in_succ_k i_sdom_j have i: "i = k ∨ i = j" by (auto intro:path_entry_append simp add:succs_def strict_dominate_def)

  from j_in_succ_k have "reachable j" using succ_in_verts reachable by (auto simp add:reachable_def)
  with i_sdom_j have "i ≠ j" by (auto simp add: sdom_neq)
  with i have "i = k" by auto
  then have "dominate i k" by (auto simp add:dominate_refl)
  with ass show False by auto
qed

end

end