Theory DFS_Framework_Misc (Isabelle2014: August 2014)

(* TODO: Integrate into Misc*)
theory DFS_Framework_Misc
imports Misc
begin

(* Functions *) 
abbreviation comp2 (infixl "oo" 55) where "f oo g ≡ λx. f o (g x)"
abbreviation comp3 (infixl "ooo" 55) where "f ooo g ≡ λx. f oo (g x)"

notation (xsymbols)
  comp2  (infixl "oo" 55) and
  comp3  (infixl "ooo" 55)

notation (HTML output)
  comp2  (infixl "oo" 55) and
  comp3  (infixl "ooo" 55)

(* General *)
lemma tri_caseE:
  "[|[|¬P;¬Q|] ==> R; P ==> R; [|¬P; Q|] ==> R|] ==> R"
by auto

(* TODO: How often have we formalized this now? *)
definition "opt_tag x y ≡ x=y"
lemma opt_tagI: "opt_tag x x" unfolding opt_tag_def by simp
lemma opt_tagD: "opt_tag x y ==> x=y" unfolding opt_tag_def by simp

(* Usage example, to simplify term
  schematic_lemma "term = ?c"
    apply (rule opt_tagD)
    apply simp, unfold, whatever ...
    by (rule opt_tagI)
*)

(* Maps *)
lemma map_update_eta_repair[simp]:
  (* An update operation may get simplified, if it happens to be eta-expanded.
    This lemma tries to repair some common expressions *)
  "dom (λx. if x=k then Some v else m x) = insert k (dom m)"
  "m k = None ==> ran (λx. if x=k then Some v else m x) = insert v (ran m)"
  apply auto []
  apply (force simp: ran_def)
  done



(* Sets *)
  lemma subset_Collect_conv: "S ⊆ Collect P <-> (∀x∈S. P x)"
    by auto

  lemma memb_imp_not_empty: "x∈S ==> S≠{}"
    by auto


(* Relation *)

definition "bijective R ≡ 
  (∀x y z. (x,y)∈R ∧ (x,z)∈R --> y=z) ∧
  (∀x y z. (x,z)∈R ∧ (y,z)∈R --> x=y)"

lemma bijective_alt: "bijective R <-> single_valued R ∧ single_valued (R¯)"
  unfolding bijective_def single_valued_def by blast

lemma bijective_Id[simp, intro!]: "bijective Id"
  by (auto simp: bijective_def)

lemma bijective_Empty[simp, intro!]: "bijective {}"
  by (auto simp: bijective_def)


definition "fun_of_rel R x ≡ SOME y. (x,y)∈R"

lemma for_in_RI(*[intro]*): "x∈Domain R ==> (x,fun_of_rel R x)∈R"
  unfolding fun_of_rel_def
  by (auto intro: someI)

lemma finite_Field_eq_finite[simp]: "finite (Field R) <-> finite R"
  by (metis finite_cartesian_product finite_subset R_subset_Field finite_Field)


lemma trancl_Image_unfold_left: "E⇧⁺``S = E⇧^*``E``S"
  by (auto simp: trancl_unfold_left)

lemma trancl_Image_unfold_right: "E⇧⁺``S = E``E⇧^*``S"
  by (auto simp: trancl_unfold_right)

lemma trancl_Image_advance_ss: "(u,v)∈E ==> E⇧⁺``{v} ⊆ E⇧⁺``{u}"
  by auto

lemma rtrancl_Image_advance_ss: "(u,v)∈E ==> E⇧^*``{v} ⊆ E⇧^*``{u}"
  by auto



lemma rtrancl_restrictI_aux:
  assumes "(u,v)∈(E-UNIV×R)⇧^*"
  assumes "u∉R"
  shows "(u,v)∈(rel_restrict E R)⇧^* ∧ v∉R"
  using assms
  by (induction) (auto simp: rel_restrict_def intro: rtrancl.intros)

corollary rtrancl_restrictI: 
  assumes "(u,v)∈(E-UNIV×R)⇧^*"
  assumes "u∉R"
  shows "(u,v)∈(rel_restrict E R)⇧^*"
  using rtrancl_restrictI_aux[OF assms] ..

lemma E_closed_restr_reach_cases:
  assumes P: "(u,v)∈E⇧^*"
  assumes CL: "E``R ⊆ R"
  obtains "v∈R" | "u∉R" "(u,v)∈(rel_restrict E R)⇧^*"
  using P
proof (cases rule: rtrancl_last_visit[where S=R])
  case no_visit
  show ?thesis proof (cases "u∈R")
    case True with P have "v∈R" 
      using rtrancl_reachable_induct[OF _ CL, where I="{u}"] 
      by auto
    thus ?thesis ..
  next
    case False with no_visit have "(u,v)∈(rel_restrict E R)⇧^*" 
      by (rule rtrancl_restrictI)
    with False show ?thesis ..
  qed
next
  case (last_visit_point x)
  from ‹(x, v) ∈ (E - UNIV × R)⇧^*› have "(x,v)∈E⇧^*" 
    by (rule rtrancl_mono_mp[rotated]) auto
  with ‹x∈R› have "v∈R" 
    using rtrancl_reachable_induct[OF _ CL, where I="{x}"] 
    by auto
  thus ?thesis ..
qed

lemma rel_restrict_trancl_notR:
  assumes "(v,w) ∈ (rel_restrict E R)⇧⁺"
  shows "v ∉ R" and "w ∉ R"
  using assms
  by (metis rel_restrict_trancl_mem rel_restrict_notR)+

lemma rel_restrict_tranclI:
  assumes "(x,y) ∈ E⇧⁺"
  and "x ∉ R" "y ∉ R"
  and "E `` R ⊆ R"
  shows "(x,y) ∈ (rel_restrict E R)⇧⁺"
  using assms
  proof (induct)
    case base thus ?case by (metis r_into_trancl rel_restrictI)
  next
    case (step y z) hence "y ∉ R" by auto
    with step show ?case by (metis trancl_into_trancl rel_restrictI)
  qed

lemma trancl_sub:
  "R ⊆ R⇧⁺"
by auto

lemma trancl_single[simp]:
  "{(a,b)}⇧⁺ = {(a,b)}"
proof -
  {
    fix x y
    assume "(x,y) ∈ {(a,b)}⇧⁺"
    hence "(x,y) ∈ {(a,b)}"
      by (induct rule: trancl.induct) auto
  }
  with trancl_sub show ?thesis by auto
qed

(* FIXME: nicer name *)
lemma trancl_union_outside:
  assumes "(v,w) ∈ (E∪U)⇧⁺"
  and "(v,w) ∉ E⇧⁺"
  shows "∃x y. (v,x) ∈ (E∪U)⇧^* ∧ (x,y) ∈ U ∧ (y,w) ∈ (E∪U)⇧^*" 
using assms
proof (induction)
  case base thus ?case by auto
next
  case (step w x)
  show ?case
  proof (cases "(v,w)∈E⇧⁺")
    case True 
    from step have "(v,w)∈(E∪U)⇧^*" by simp
    moreover from True step have "(w,x) ∈ U" by (metis Un_iff trancl.simps)
    moreover have "(x,x) ∈ (E∪U)⇧^*" by simp
    ultimately show ?thesis by blast
  next
    case False with step.IH obtain a b where "(v,a) ∈ (E∪U)⇧^*" "(a,b) ∈ U" "(b,w) ∈ (E∪U)⇧^*" by blast
    moreover with step have "(b,x) ∈ (E∪U)⇧^*" by (metis rtrancl_into_rtrancl)
    ultimately show ?thesis by blast
  qed
qed

lemma trancl_restrict_reachable:
  assumes "(u,v) ∈ E⇧⁺"
  assumes "E``S ⊆ S"
  assumes "u∈S"
  shows "(u,v) ∈ (E∩S×S)⇧⁺"
  using assms
  by (induction rule: converse_trancl_induct)
     (auto intro: trancl_into_trancl2)

lemma rtrancl_image_unfold_right: "E``E⇧^*``V ⊆ E⇧^*``V"
  by (auto intro: rtrancl_into_rtrancl)

lemma Field_not_elem:
  "v ∉ Field R ==> ∀(x,y) ∈ R. x ≠ v ∧ y ≠ v"
unfolding Field_def by auto

lemma trancl_Image_in_Range:
  "R⇧⁺ `` V ⊆ Range R"
by (auto elim: trancl.induct)
  
lemma rtrancl_Image_in_Field:
  "R⇧^* `` V ⊆ Field R ∪ V"
proof -
  from trancl_Image_in_Range have "R⇧⁺ `` V ⊆ Field R" 
    unfolding Field_def by fast
  hence "R⇧⁺ `` V ∪ V ⊆ Field R ∪ V" by blast
  with trancl_image_by_rtrancl show ?thesis by metis
qed

lemma rtrancl_sub_insert_rtrancl:
  "R⇧^* ⊆ (insert x R)⇧^*"
by (auto elim: rtrancl.induct rtrancl_into_rtrancl)

lemma trancl_sub_insert_trancl:
  "R⇧⁺ ⊆ (insert x R)⇧⁺"
by (auto elim: trancl.induct trancl_into_trancl)

lemma Restr_rtrancl_mono:
  "(v,w) ∈ (Restr E U)⇧^* ==> (v,w) ∈ E⇧^*"
  by (metis inf_le1 rtrancl_mono subsetCE)

lemma Restr_trancl_mono:
  "(v,w) ∈ (Restr E U)⇧⁺ ==> (v,w) ∈ E⇧⁺"
  by (metis inf_le1 trancl_mono)

lemma Sigma_UNIV_cancel[simp]: "(A × X - A × UNIV) = {}" by auto

lemma cyclic_subset:
  "[| ¬ acyclic R; R ⊆ S |] ==> ¬ acyclic S"
  unfolding acyclic_def
  by (blast intro: trancl_mono)

(* Lists *)
lemma in_hd_or_tl_conv[simp]: "l≠[] ==> x=hd l ∨ x∈set (tl l) <-> x∈set l"
  by (cases l) auto

lemma rev_split_conv[simp]:
  "l ≠ [] ==> rev (tl l) @ [hd l] = rev l"
by (induct l) simp_all

lemma neq_Nil_rev_conv: "l≠[] <-> (∃xs x. l = xs@[x])"
  by (cases l rule: rev_cases) auto

lemma rev_butlast_is_tl_rev: "rev (butlast l) = tl (rev l)"
  by (induct l) auto

lemma hd_last_singletonI:
  "[|xs ≠ []; hd xs = last xs; distinct xs|] ==> xs = [hd xs]"
  by (induct xs rule: list_nonempty_induct) auto

lemma last_filter:
  "[|xs ≠ []; P (last xs)|] ==> last (filter P xs) = last xs"
  by (induct xs rule: rev_nonempty_induct) simp_all

lemma length_dropWhile_takeWhile:
  assumes "x < length (dropWhile P xs)"
  shows "x + length (takeWhile P xs) < length xs"
  using assms
  by (induct xs) auto

(* As the following two rules are similar in nature to list_induct2',
   they are named accordingly. *)
lemma rev_induct2' [case_names empty snocl snocr snoclr]: 
  assumes empty: "P [] []"
  and snocl: "!!x xs. P (xs@[x]) []"
  and snocr: "!!y ys. P [] (ys@[y])"
  and snoclr: "!!x xs y ys.  P xs ys  ==> P (xs@[x]) (ys@[y])"
  shows "P xs ys"
proof (induct xs arbitrary: ys rule: rev_induct)
  case Nil thus ?case using empty snocr 
    by (cases ys rule: rev_exhaust) simp_all
next
  case snoc thus ?case using snocl snoclr
    by (cases ys rule: rev_exhaust) simp_all
qed

lemma rev_nonempty_induct2' [case_names single snocl snocr snoclr, consumes 2]: 
  assumes "xs ≠ []" "ys ≠ []"
  assumes single': "!!x y. P [x] [y]"
  and snocl: "!!x xs y. xs ≠ [] ==> P (xs@[x]) [y]"
  and snocr: "!!x y ys. ys ≠ [] ==> P [x] (ys@[y])"
  and snoclr: "!!x xs y ys. [|P xs ys; xs ≠ []; ys≠[]|]  ==> P (xs@[x]) (ys@[y])"
  shows "P xs ys"
  using assms(1,2)
proof (induct xs arbitrary: ys rule: rev_nonempty_induct)
  case single then obtain z zs where "ys = zs@[z]" by (metis rev_exhaust)
  thus ?case using single' snocr
    by (cases "zs = []") simp_all
next
  case (snoc x xs) then obtain z zs where zs: "ys = zs@[z]" by (metis rev_exhaust)
  thus ?case using snocl snoclr snoc
    by (cases "zs = []") simp_all
qed

end