dominators.thy

theory Dominators imports Main begin

typedecl node

axiomatization
  s0 :: "node" and
  R :: "node rel"
where
  reachable: "ALL n. (s0, n) : R^*"

inductive_set
  path_all :: "node list set"
where
  path_all_b [intro, simp]: "[s0] : path_all" |
  path_all_i [intro]: "[| p#ps : path_all; (p, q) : R |]
                    ==> q#p#ps : path_all"

definition path_to :: "node => node list set" where
  "path_to n == {ps. ps : path_all & hd ps = n}"

definition dominates :: "node => node => bool"  (infix "dominates" 60)
where "x dominates y == (ALL ps:path_to y. x : set ps)"

definition D :: "node => node set" where
  "D n == {x. x dominates n}"

lemma list_cut [rule_format]: "ALL a. a : set xs --> (EX ys zs. xs = ys @ (a # zs))"
apply(induct_tac xs)
apply(auto)
apply(drule_tac x="aa" in spec)
apply(auto)
by (metis append_Cons)

lemma path_prefix:
  "xs : path_all ==> ALL ys zs. zs ~=[] & ys @ zs = xs --> zs : path_all"
apply(erule path_all.induct)
apply(auto)
apply(case_tac zs)
apply(auto)
apply(case_tac ys)
apply(auto)
by (metis append_Nil list.distinct(1) list.sel(3) path_all.path_all_i tl_append2)

lemma dominates_trans: "[| x dominates y; y dominates z |] ==> x dominates z"
apply(unfold dominates_def path_to_def)
apply(auto)
apply(case_tac ps)
apply(auto)
apply(rotate_tac 1)
apply(drule_tac x="z#list" in spec)
apply(auto)
apply(drule list_cut)
apply(erule exE)
apply(erule exE)
apply(drule path_prefix)
apply(rotate_tac -1)
apply(drule_tac x="z # ys" in spec)
apply(rotate_tac -1)
apply(drule_tac x="y # zs" in spec)
apply(auto)
done

lemma dominates_refl [simp]: "x dominates x"
apply(unfold dominates_def path_to_def)
apply(auto)
apply(case_tac ps)
apply(auto)
done

lemma D_0 [simp]: "n : D n"
apply(unfold D_def)
apply(auto)
done

lemma dominates_s0 [rule_format]: "x dominates s0 --> x = s0"
apply(unfold dominates_def path_to_def)
apply(auto)
done

(*
lemma dominates_s0_1 [intro]:
  "d dominates n ==> d ~= s0"
apply(rule classical)
apply(simp)
apply(drule dominates_s0)
*)

lemma D_s0: "D s0 = {s0}"
apply(unfold D_def dominates_def path_to_def)
apply(auto)
apply(case_tac ps)
apply(auto)
done

lemma dominates_pred:
  "[| x dominates n; x ~= n; (p, n) : R |] ==> x dominates p"
apply(unfold dominates_def path_to_def)
apply(auto)
apply(case_tac ps)
apply(auto)
done

lemma ex_pred: "ALL n. n ~= s0 --> (EX p. (p, n) : R)"
apply(rule allI)
apply(insert reachable)
apply(drule_tac x="n" in spec)
by (metis rtranclE)

lemma all_ex_imp:
  "(ALL x. (EX y. P x y) --> Q x) = (ALL x y. P x y --> Q x)"
apply(auto)
done

lemma path_all_single [simp]:
  "[n] : path_all ==> n = s0"
apply(erule path_all.cases)
apply(auto)
done

lemma path_prefix0 [intro]:
  "n#p#ps : path_all ==> p#ps : path_all"
apply(drule path_prefix)
apply(drule_tac x="[n]" in spec)
apply(drule_tac x="p#ps" in spec)
apply(auto)
done

lemma pred_through:
  "[| n # ps : path_all; n ~= s0 |] ==> EX p ps'. (p, n) : R & ps = p#ps' & p#ps' : path_all"
apply(case_tac ps)
apply(auto)
apply(erule path_all.cases)
apply(auto)
done

lemma dominates_pred_all:
"[| ALL p. (p, n) : R --> x dominates p; n ~= s0 |] ==> x dominates n"
apply(unfold dominates_def path_to_def)
apply(auto)
apply(case_tac ps)
apply(auto)
apply(drule pred_through)
apply(clarsimp)
apply(clarsimp)
apply(drule_tac x="p" in spec)
apply(drule mp)
apply(simp)
apply(drule_tac x="p#ps'" in spec)
apply(clarsimp)
done

lemma D_step: "n ~= s0 ==> D n = {n} Un Inter {D p | p. (p, n) : R}"
apply(unfold D_def)
apply(auto)
apply(erule dominates_pred)
apply(auto)
apply(simp add: all_ex_imp)
apply(erule dominates_pred_all)
apply(simp)
done

(**************************************************************************)

(* immediate dominator idom *)

definition is_idom_of :: "node => node => bool" where
"is_idom_of d n == (d ~= n & d dominates n & (ALL x. x ~= n & x dominates n & d dominates x --> x = d))"

lemma rtrancl1 [rule_format]:
  "(x, y) : r^* ==>
     P x --> (ALL a b. (x, a) : r^* & P a & (a, b) : r --> P b) --> P y"
apply(erule rtrancl.induct)
apply(auto)
done

lemma path_ex: "ALL n. EX ps. n#ps : path_all"
apply(insert reachable)
apply(rule allI)
apply(drule_tac x="n" in spec)
apply(erule rtrancl1)
apply(rule_tac x="[]" in exI)
apply(clarsimp)
apply(clarsimp)
apply(rule_tac x="a#ps" in exI)
apply(auto)
done

lemma path_route [rule_format]:
  "ALL ps ys. d # ps : path_all --> xs @ d # ys : path_all
                                --> xs @ d # ps : path_all"
apply(induct_tac xs)
apply(auto)
apply(drule_tac x="ps" in spec)
apply(clarsimp)
apply(drule mp)
apply(rotate_tac -1)
apply(drule path_prefix)
apply(drule_tac x="[a]" in spec)
apply(drule_tac x="list@d#ys" in spec)
apply(clarsimp)
apply(rule_tac x="ys" in exI)
apply(clarsimp)
apply(case_tac list)
apply(auto)
apply(subgoal_tac "(d, a) : R")
apply(erule path_all_i)
apply(simp)
apply(rotate_tac -1)
apply(erule path_all.cases)
apply(auto)
apply(subgoal_tac "(aa, a) : R")
apply(erule path_all_i)
apply(simp)
apply(rotate_tac 1)
apply(erule path_all.cases)
apply(auto)
done

lemma dominates_ext:
  "[| d dominates n; d ~= n; d#ps : path_all |] ==> EX xs. n#xs @ d#ps : path_all"
apply(unfold dominates_def path_to_def)
apply(clarsimp)
apply(insert path_ex)
apply(rotate_tac -1)
apply(drule_tac x="n" in spec)
apply(clarsimp)
apply(drule_tac x="n#psa" in spec)
apply(auto)
apply(drule list_cut)
apply(clarsimp)
apply(rule_tac x="ys" in exI)
apply(drule_tac xs="n#ys" and ys="zs" in path_route)
apply(auto)
done

definition sdom :: "node => node => bool" (infix "sdom" 60)
where "d sdom n == (d dominates n & d ~= n)"

lemma sdom_ex [rule_format]: "n ~= s0 --> (EX d. d sdom n)"
apply(unfold sdom_def dominates_def path_to_def)
apply(clarsimp)
apply(rule_tac x="s0" in exI)
apply(auto)
apply(erule path_all.induct)
apply(auto)
done


lemma finite_path: "ALL p. EX k. (s0, p) : R^^k"
apply(insert reachable)
apply(rule)
apply(drule_tac x="p" in spec)
apply(erule rtrancl.induct)
apply(rule_tac x="0" in exI)
apply(clarsimp)
apply(clarsimp)
apply(rule_tac x="Suc k" in exI)
apply(auto)
done

lemma limited_lin [rule_format]: "ALL n. (s0, n) : R^^k --> (d ~= e & d ~= n & e ~= n & d dominates n & e dominates n) --> d dominates e | e dominates d"
apply(induct_tac k)
apply(clarsimp)
apply(drule dominates_s0)
apply(clarsimp)
apply(rule allI)
apply(rule impI)
apply(rule impI)
apply(erule relpow_Suc_E)
apply(drule_tac x="y" in spec)
apply(drule mp)
apply(clarsimp)
apply(case_tac "y=d")
apply(clarsimp)
apply(case_tac "na=e")
apply(clarsimp)
apply(drule_tac x="e" in dominates_pred)
apply(clarsimp)
apply(assumption)
apply(clarsimp)
apply(case_tac "y=e")
apply(clarsimp)
apply(drule_tac x="d" in dominates_pred)
apply(clarsimp)
apply(assumption)
apply(clarsimp)
apply(drule mp)
apply(clarsimp)
apply(rule conjI)
apply(drule_tac x="d" in dominates_pred)
apply(clarsimp)
apply(assumption)
apply(assumption)
apply(drule_tac x="e" in dominates_pred)
apply(clarsimp)
apply(assumption)
apply(assumption)
apply(clarsimp)
done

lemma dominates_linear:
  "[| d dominates n; e dominates n |] ==> d dominates e | e dominates d"
apply(case_tac "d=e")
apply(clarsimp)
apply(case_tac "d=n")
apply(clarsimp)
apply(case_tac "e=n")
apply(clarsimp)
apply(insert finite_path)
apply(drule_tac x="n" in spec)
apply(erule exE)
apply(erule limited_lin)
apply(clarsimp)
done

lemma D_subseteq: "x dominates y ==> D x <= D y"
apply(unfold D_def)
apply(clarsimp)
apply(erule dominates_trans)
apply(clarsimp)
done

lemma D_eq: "x dominates y & y dominates x --> D x = D y"
apply(rule impI)
apply(rule antisym)
apply(rule D_subseteq)
apply(clarsimp)
apply(rule D_subseteq)
apply(clarsimp)
done

lemma "(ALL m::nat. (ALL i. i < m --> P i) --> P m) --> (ALL n. P n)"
apply(rule impI)
apply(rule allI)
apply(rule_tac r="less_than" and a="n" in wf_induct)
apply(auto)
done

lemma nat_minimal: "P (n::nat) ==> (EX m. P m & (ALL i. i < m --> ~ P i))"
apply(erule contrapos_pp)
apply(rule_tac r="less_than" and a="n" in wf_induct)
apply(clarsimp)
apply(clarsimp)
apply(drule_tac x="x" in spec)
apply(clarsimp)
done

lemma route__shortest:
  "ALL n. EX k. (s0, n) : R^^k & (ALL i. i < k --> (s0, n) ~: R^^i)"
apply(insert finite_path)
apply(rule allI)
apply(drule_tac x="n" in spec)
apply(clarsimp)
apply(erule nat_minimal)
done

lemma path_to_ex: "ALL n. EX ps. ps : path_to n"
apply(insert path_ex)
apply(rule allI)
apply(drule_tac x="n" in spec)
apply(unfold path_to_def)
apply(auto)
done

lemma path_to_s0 [simp]: "[s0] : path_to s0"
apply(unfold path_to_def)
apply(auto)
done

lemma path_to_step [intro]:
  "[| y # ps : path_to y; (y, z) : R |]
      ==> z # y # ps : path_to z"
apply(unfold path_to_def)
apply(auto)
done

lemma path_to_ex2:
  "ALL n. EX k. (EX ps. n#ps : path_to n & k = length ps)"
apply(insert path_ex)
apply(rule allI)
apply(drule_tac x="n" in spec)
apply(clarsimp)
apply(unfold path_to_def)
apply(auto)
done

lemma path_shortest:
  "ALL n. EX k. (EX ps. n#ps : path_to n & k = length ps) &
                (ALL i. i < k --> ~(EX ps. n#ps : path_to n & i = length ps))"
apply(insert path_to_ex2)
apply(rule allI)
apply(drule_tac x="n" in spec)
apply(erule exE)
apply(erule nat_minimal)
done

lemma path_shortest2:
  "ALL n. EX ps. n#ps : path_to n &
          (ALL qs. n#qs : path_to n --> length ps <= length qs)"
apply(rule allI)
apply(insert path_shortest)
apply(drule_tac x="n" in spec)
apply(clarsimp)
apply(rule_tac x="ps" in exI)
apply(auto)
apply(drule_tac x="length qs" in spec)
apply(erule contrapos_pp)
apply(drule mp)
apply(clarsimp)
apply(clarsimp)
apply(drule_tac x="qs" in spec)
apply(clarsimp)
done

lemma path_to_hd: "ps : path_to n ==> EX qs. ps=n#qs"
apply(unfold path_to_def)
apply(auto)
apply(case_tac ps)
apply(auto)
done

lemma path_to_prefix:
  "x # ps @ y # qs : path_to x ==> y # qs : path_to y"
apply(unfold path_to_def)
apply(auto)
apply(drule path_prefix)
apply(auto)
done

lemma dominates_antisym:
  "[| x dominates y; y dominates x |] ==> x = y"
apply(unfold dominates_def)
apply(insert path_shortest2)
apply(rotate_tac -1)
apply(drule_tac x="x" in spec)
apply(clarsimp)
apply(rotate_tac 1)
apply(frule_tac x="x#ps" in bspec)
apply(auto)
apply(drule list_cut)
apply(clarsimp)
apply(drule path_to_prefix)
apply(rotate_tac -2)
apply(frule_tac x="y#zs" in bspec)
apply(auto)
apply(drule list_cut)
apply(clarsimp)
apply(drule path_to_prefix)
apply(rotate_tac 2)
apply(drule_tac x="zsa" in spec)
apply(clarsimp)
done

lemma is_idom_of_uniq:
  "[| is_idom_of d n; is_idom_of e n |] ==> d = e"
apply(unfold is_idom_of_def)
apply(auto)
apply(drule_tac x="e" in spec)
apply(drule_tac x="d" in spec)
apply(auto)
apply(subgoal_tac "d dominates e | e dominates d")
apply(clarsimp)
apply(erule dominates_linear)
apply(clarsimp)
done

lemma is_idom_of_s0: "~is_idom_of d s0"
apply(unfold is_idom_of_def)
apply(auto)
apply(drule dominates_s0)
apply(clarsimp)
done

lemma bound_finite_induct [rule_format]:
  "finite A ==>
 P {} -->
 (ALL x F. F <= A --> x : A --> x ~: F --> P F --> P (insert x F)) --> P A"
apply(erule finite_induct)
apply(auto)
done

lemma "finite A
  ==> A ~= {} --> (EX m::nat. m : A & (ALL x. x : A --> x <= m))"
apply(erule bound_finite_induct)
apply(clarsimp)
apply(clarsimp)
apply(case_tac "F={}")
apply(clarsimp)
apply(clarsimp)
apply(case_tac "x <= m")
apply(rule_tac x="m" in exI)
apply(clarsimp)
apply(rule_tac x="x" in exI)
apply(clarsimp)
apply(drule_tac x="xa" in spec)
apply(clarsimp)
done

lemma D_dominates [intro, dest]: "x : D n ==> x dominates n"
apply(unfold D_def)
apply(auto)
done

lemma idom_0: "finite ((D n) - {n})
  ==> (D n) - {n} ~= {} --> (EX m. m : (D n) - {n} & (ALL x. x : (D n) - {n} --> x dominates m))"
apply(erule bound_finite_induct)
apply(clarsimp)
apply(clarsimp)
apply(case_tac "F={}")
apply(clarsimp)
apply(clarsimp)
apply(case_tac "x dominates m")
apply(rule_tac x="m" in exI)
apply(clarsimp)
apply(rule_tac x="x" in exI)
apply(clarsimp)
apply(drule_tac x="xa" in spec)
apply(clarsimp)
apply(erule dominates_trans)
apply(subgoal_tac "m dominates x | x dominates m")
defer
apply(rule_tac n="n" in dominates_linear)
apply(rule D_dominates)
apply(rule_tac A="F" in subsetD)
apply(blast)
apply(clarsimp)
apply(rule D_dominates)
apply(clarsimp)
apply(clarsimp)
done

lemma path_all_s0: "ps : path_all ==> EX qs. ps = qs @ [s0]"
apply(erule path_all.induct)
apply(auto)
done

lemma s0_dominates [simp]: "s0 dominates n"
apply(case_tac "n=s0")
apply(auto)
apply(unfold dominates_def path_to_def)
apply(clarsimp)
apply(case_tac ps)
apply(auto)
apply(drule path_all_s0)
apply(auto)
apply(case_tac qs)
apply(auto)
done

lemma D_nonempty: "n ~= s0 ==> (D n) - {n} ~= {}"
apply(unfold D_def)
apply(clarsimp)
apply(simp add: subset_eq)
apply(drule_tac x="s0" in spec)
apply(clarsimp)
done

lemma D_path: "ps : path_to n ==> D n <= set ps"
apply(unfold D_def dominates_def path_to_def)
apply(clarsimp)
done

lemma D_finite [simp]: "finite (D n)"
apply(insert path_to_ex)
apply(drule_tac x="n" in spec)
apply(clarsimp)
apply(rule_tac f="id" and A="set ps" in finite_surj)
apply(clarsimp)
apply(drule D_path)
apply(clarsimp)
done

lemma idom_1:
  "n ~= s0 ==> EX m. m : (D n) - {n} & (ALL x. x : (D n) - {n} --> x dominates m)"
apply(rule idom_0[rule_format])
apply(subgoal_tac "finite (D n)")
apply(clarsimp)
apply(rule D_finite)
apply(erule D_nonempty)
done

definition idom :: "node => node" where
  "idom n = (THE d. is_idom_of d n)"

lemma D_mut: "[| x : D n; y : D n |] ==> x dominates y | y dominates x"
apply(unfold D_def)
apply(rule dominates_linear)
apply(auto)
done

lemma idom_ex: "n ~= s0 --> (EX d. is_idom_of d n)"
apply(unfold is_idom_of_def)
apply(clarsimp)
apply(drule idom_1)
apply(clarsimp)
apply(rule_tac x="m" in exI)
apply(clarsimp)
apply(rule conjI)
apply(erule D_dominates)
apply(clarsimp)
apply(drule_tac x="x" in spec)
apply(clarsimp)
apply(drule mp)
apply(subst D_def)
apply(clarsimp)
apply(erule dominates_antisym)
apply(clarsimp)
done

(**************************************************************************)

definition DF :: "node => node set" where
  "DF x = {w. EX p. (p, w) : R & x dominates p & ~(x sdom w)}"

definition DFlocal :: "node => node set" where
  "DFlocal n = {x. (n, x) : R & ~(n sdom x)}"

definition DFup :: "node => node set" where
  "DFup n = {x. x : DF n & ~((idom n) sdom x)}"

definition children :: "node => node set" where
  "children n = {x. x ~= s0 & idom x = n}"

lemma is_idom_of_n: "ALL n. ~is_idom_of n n"
apply(unfold is_idom_of_def)
apply(clarsimp)
done

lemma theD: "[| (THE x. P x) = y; P a; ALL x. P x --> x = a |] ==> P y"
apply(clarsimp)
apply(rule theI)
apply(auto)
done

lemma idom_neq: "n ~= s0 ==> idom n ~= n"
apply(unfold idom_def)
apply(rule classical)
apply(clarsimp)
apply(drule idom_ex[rule_format])
apply(clarsimp)
apply(drule theD)
apply(assumption)
apply(clarsimp)
apply(erule is_idom_of_uniq)
apply(assumption)
apply(insert is_idom_of_n)
apply(clarsimp)
done

lemma idom_dominates0: "n ~= s0 ==> idom n = d ==> d dominates n"
apply(unfold idom_def)
apply(drule idom_ex[rule_format])
apply(erule exE)
apply(drule theD)
apply(assumption)
apply(clarsimp)
apply(erule is_idom_of_uniq)
apply(assumption)
apply(unfold is_idom_of_def)
apply(clarsimp)
done

lemma idom_dominates: "n ~= s0 ==> (idom n) dominates n"
apply(rule idom_dominates0)
apply(auto)
done

lemma idom_sdom: "n ~= s0 ==> (idom n) sdom n"
apply(unfold sdom_def)
apply(rule conjI)
apply(erule idom_dominates)
apply(erule idom_neq)
done

lemma DFlocal_idom_1: "[| (n, x) : R; x ~= s0; idom x = n |] ==> n sdom x"
apply(subgoal_tac "(idom x) sdom x")
apply(clarsimp)
apply(erule idom_sdom)
done

lemma DFlocal_idom_2: "[| (n, x) : R; x ~= s0; n sdom x |] ==> idom x = n"
apply(unfold sdom_def idom_def)
apply(rule the_equality)
apply(unfold is_idom_of_def)
apply(clarsimp)
apply(rotate_tac -2)
apply(drule dominates_pred)
apply(assumption)
apply(assumption)
apply(erule dominates_antisym)
apply(assumption)
(**)
apply(clarsimp)
apply(drule_tac x="n" in spec)
apply(clarsimp)
apply(drule mp)
apply(rotate_tac -1)
apply(drule dominates_pred)
apply(assumption)
apply(assumption)
apply(assumption)
apply(clarsimp)
done

lemma DFlocal_idom:
  "ALL y. (n, y) : R --> y ~= s0 ==>
   DFlocal n = {y. (n, y) : R & idom y ~= n}"
apply(unfold DFlocal_def)
apply(rule antisym)
apply(rule subsetI)
apply(simp)
apply(erule conjE)
apply(erule contrapos_nn)
apply(drule_tac x="x" in spec)
apply(clarsimp)
apply(erule DFlocal_idom_1)
apply(assumption)
apply(clarsimp)
(*2*)
apply(rule subsetI)
apply(simp)
apply(erule conjE)
apply(erule contrapos_nn)
apply(drule_tac x="x" in spec)
apply(clarsimp)
apply(erule DFlocal_idom_2)
apply(assumption)
apply(assumption)
done

lemma idom_dominators0:
  "[| n ~= s0; d ~= n; d dominates n; idom n = x |] ==> d dominates x"
apply(case_tac "x=d")
apply(clarsimp)
apply(unfold idom_def)
apply(drule idom_ex[rule_format])
apply(erule exE)
apply(drule theD)
apply(assumption)
apply(clarsimp)
apply(erule is_idom_of_uniq)
apply(assumption)
apply(drule is_idom_of_uniq)
apply(assumption)
apply(clarsimp)
apply(unfold is_idom_of_def)
apply(clarsimp)
apply(drule_tac x="d" in spec)
apply(clarsimp)
apply(drule dominates_linear)
apply(assumption)
apply(clarsimp)
done

lemma idom_dominators: "[| d dominates n; n ~= s0; d ~= n |] ==> d dominates (idom n)"
apply(rule idom_dominators0)
apply(assumption)
apply(assumption)
apply(assumption)
apply(clarsimp)
done

lemma idom_idom:
  "[| n dominates x; n ~= x; idom x ~= n; x ~= s0 |] ==>
    EX y. y dominates x & idom y = n & y ~= s0"
apply(rotate_tac 2)
apply(erule contrapos_np)
apply(simp)
apply(subgoal_tac "is_idom_of n x")
apply(subst idom_def)
apply(rule the_equality)
apply(assumption)
apply(erule is_idom_of_uniq)
apply(assumption)
apply(unfold is_idom_of_def)
apply(auto)
sorry

lemma DF_1:
  "DF n <= DFlocal n Un Union {DFup c |c. c : children n}"
apply(unfold DF_def DFlocal_def DFup_def children_def sdom_def)
apply(clarsimp)
(*
  x : DF n

  n dominates p where p = pred x, i.e. (p, x) : R
  ~(n dom x)
*)

(* DFlocal case *)
apply(case_tac "(n, x) : R")
apply(assumption)

apply(erule contrapos_pp)
apply(clarsimp)
apply(case_tac "n=p")
apply(clarsimp)

apply(case_tac "idom p = n")
apply(case_tac "n=x")
apply(clarsimp)
apply(rule exI)
apply(rule conjI)
apply(rule_tac x="p" in exI)
apply(rule conjI)
apply(simp)
apply(rule conjI)
apply(rule classical)
apply(simp)
apply(drule dominates_s0)
apply(simp)
apply(simp)
apply(simp)
apply(rule_tac x="p" in exI)
apply(clarsimp)
apply(drule dominates_antisym)
apply(assumption)
apply(simp)

apply(rule exI)
apply(rule conjI)
apply(rule_tac x="p" in exI)
apply(rule conjI)
apply(simp)
apply(rule conjI)
apply(rule classical)
apply(simp)
apply(drule dominates_s0)
apply(simp)
apply(simp)
apply(simp)
apply(rule_tac x="p" in exI)
apply(clarsimp)
apply(drule dominates_trans)
apply(assumption)
apply(simp)

apply(frule idom_idom)
apply(assumption)
apply(assumption)
apply(rule classical)
apply(simp)
apply(drule dominates_s0)
apply(clarsimp)
apply(clarsimp)

apply(case_tac "n=x")
apply(clarsimp)
apply(rule exI)
apply(rule conjI)
apply(rule_tac x="y" in exI)
apply(rule conjI)
apply(simp)
apply(rule conjI)
apply(rule classical)
apply(simp)
apply(simp)
apply(clarsimp)
apply(rule_tac x="p" in exI)
apply(clarsimp)
apply(rotate_tac -3)
apply(frule idom_dominates)
apply(rotate_tac -1)
apply(drule dominates_antisym)
apply(assumption)
apply(simp)

apply(case_tac "x=y")
apply(clarsimp)
apply(rotate_tac -3)
apply(frule idom_dominates)
apply(simp)

apply(rule exI)
apply(rule conjI)
apply(rule_tac x="y" in exI)
apply(rule conjI)
apply(simp)
apply(rule conjI)
apply(simp)
apply(simp)
apply(clarsimp)

apply(rule_tac x="p" in exI)
apply(clarsimp)
apply(rotate_tac -5)
apply(frule idom_dominates)
apply(rotate_tac -1)
apply(drule dominates_trans)
apply(assumption)
apply(simp)
done

lemma DF_2:
  "x : DFlocal n ==> x : DF n"
apply(unfold DFlocal_def DF_def sdom_def)
apply(auto)
done

lemma idom_dominates2 [intro]:
  "d ~= s0 ==> d dominates n ==> (idom d) dominates n"
apply(frule idom_dominates)
apply(erule dominates_trans)
apply(assumption)
done

lemma DF_3:
  "[| x : DFup c; c : children n |] ==> x : DF n"
apply(unfold DFup_def children_def DF_def sdom_def)
apply(auto)
done

lemma "DF n = DFlocal n Un Union {DFup c |c. c : children n}"
apply(rule antisym)
apply(rule DF_1)
apply(auto)
apply(erule DF_2)
apply(erule DF_3)
apply(assumption)
done