Theory GraphProps

(*  Author:  Gertrud Bauer, Tobias Nipkow  *)

section‹Properties of Graph Utilities›

theory GraphProps
imports Graph
begin

declare [[linarith_neq_limit = 3]]

lemma final_setFinal[iff]: "final(setFinal f)"
by (simp add:setFinal_def)


lemma eq_setFinal_iff[iff]: "(f = setFinal f) = final f"
proof (induct f)
  case (Face f t)
  then show ?case
    by (cases t) (simp_all add: setFinal_def)
qed

lemma setFinal_eq_iff[iff]: "(setFinal f = f) = final f"
by (blast dest:sym intro:sym)


lemma distinct_vertices[iff]: "distinct(vertices(g::graph))"
by(induct g) simp


subsection‹@{const nextElem}›

lemma nextElem_append[simp]:
 "y ∉ set xs ⟹ nextElem (xs @ ys) d y = nextElem ys d y"
by(induct xs) auto

lemma nextElem_cases:
"nextElem xs d x = y ⟹
 x ∉ set xs ∧ y = d ∨
 xs ≠ [] ∧ x = last xs ∧ y = d ∧ x ∉ set(butlast xs) ∨
 (∃us vs. xs = us @ [x,y] @ vs ∧ x ∉ set us)"
apply(induct xs)
 apply simp
apply simp
apply(split if_splits)
 apply(simp split:list.splits)
 apply(rule_tac x = "[]" in exI)
 apply simp
apply simp
apply(erule disjE)
 apply simp
apply(erule disjE)
 apply clarsimp
apply(rule conjI)
 apply clarsimp
apply (clarsimp)
apply(erule_tac x = "a#us" in allE)
apply simp
done


lemma nextElem_notin_butlast[rule_format,simp]:
 "y ∉ set(butlast xs) ⟶ nextElem xs x y = x"
by(induct xs) auto

lemma nextElem_in: "nextElem xs x y : set(x#xs)"
apply (induct xs)
 apply simp
apply auto
apply(clarsimp split: list.splits)
apply(clarsimp split: list.splits)
done

lemma nextElem_notin[simp]: "a ∉ set as ⟹ nextElem as c a = c"
by(erule nextElem_append[where ys = "[]", simplified])

lemma nextElem_last[simp]: assumes dist: "distinct xs"
shows "nextElem xs c (last xs) = c"
proof cases
  assume "xs = []" thus ?thesis by simp
next
  let ?xs = "butlast xs @ [last xs]"
  assume xs: "xs ≠ []"
  with dist have "distinct ?xs" by simp
  hence notin: "last xs ∉ set(butlast xs)" by simp
  from xs have "nextElem xs c (last xs) = nextElem ?xs c (last xs)" by simp
  also from notin have "… = c" by simp
  finally show ?thesis .
qed


lemma prevElem_nextElem:
assumes dist: "distinct xs" and xxs: "x : set xs"
shows "nextElem (rev xs) (last xs) (nextElem xs (hd xs) x) = x"
proof -
  define x' where "x' = nextElem xs (hd xs) x"
  hence nE: "nextElem xs (hd xs) x = x'" by simp
  have "xs ≠ [] ∧ x = last xs ∧ x' = hd xs ∨ (∃us vs. xs = us @ [x, x'] @ vs)"
    (is "?A ∨ ?B")
    using nextElem_cases[OF nE] xxs by blast
  thus ?thesis
  proof
    assume ?A
    thus ?thesis using dist by(clarsimp simp:neq_Nil_conv)
  next
    assume ?B
    then obtain us vs where [simp]: "xs = us @ [x, x'] @ vs" by blast
    thus ?thesis using dist by simp
  qed
qed

lemma nextElem_prevElem:
 "⟦ distinct xs; x : set xs ⟧ ⟹
  nextElem xs (hd xs) (nextElem (rev xs) (last xs) x) = x"
apply(cases "xs = []")
 apply simp
using prevElem_nextElem[where xs = "rev xs" and x=x]
apply(simp add:hd_rev last_rev)
done


lemma nextElem_nth:
 "⋀i. ⟦distinct xs; i < length xs ⟧
   ⟹ nextElem xs z (xs!i) = (if length xs = i+1 then z else xs!(i+1))"
apply(induct xs) apply simp
apply(case_tac i)
 apply(simp split:list.split)
apply clarsimp
done


subsection ‹‹nextVertex››

lemma nextVertex_in_face'[simp]:
  "vertices f ≠ [] ⟹ f ∙ v ∈ 𝒱 f"
proof -
  assume f: "vertices f ≠ []"
  define c where "c = nextElem (vertices f) (hd (vertices f)) v"
  then have "nextElem (vertices f) (hd (vertices f)) v = c" by auto
  with f show ?thesis
    apply (simp add: nextVertex_def)
    apply (drule_tac nextElem_cases)
    apply(fastforce simp:neq_Nil_conv)
    done
qed

lemma nextVertex_in_face[simp]:
  "v ∈ set (vertices f) ⟹ f ∙ v ∈ 𝒱 f"
 by (auto intro: nextVertex_in_face')


lemma nextVertex_prevVertex[simp]:
 "⟦ distinct(vertices f); v ∈ 𝒱 f ⟧
 ⟹ f ∙ (f⇗-1⇖ ∙ v) = v"
by(simp add:prevVertex_def nextVertex_def nextElem_prevElem)

lemma prevVertex_nextVertex[simp]:
 "⟦ distinct(vertices f); v ∈ 𝒱 f ⟧
 ⟹ f⇗-1⇖ ∙ (f ∙ v) = v"
by(simp add:prevVertex_def nextVertex_def prevElem_nextElem)

lemma prevVertex_in_face[simp]:
 "v ∈ 𝒱 f ⟹ f⇗-1⇖ ∙ v ∈ 𝒱 f"
apply(cases "vertices f = []")
 apply simp
using nextElem_in[of "rev (vertices f)" "(last (vertices f))" v]
apply (auto simp add: prevVertex_def)
done

lemma nextVertex_nth:
 "⟦ distinct(vertices f); i < |vertices f| ⟧ ⟹
  f ∙ (vertices f ! i) = vertices f ! ((i+1) mod |vertices f| )"
apply(cases "vertices f = []") apply simp
apply(simp add:nextVertex_def nextElem_nth hd_conv_nth)
done


subsection ‹‹ℰ››

lemma edges_face_eq:
 "((a,b) ∈ ℰ (f::face)) = ((f ∙ a = b) ∧ a ∈ 𝒱 f)"
by (auto simp add: edges_face_def)


lemma edges_setFinal[simp]: "ℰ(setFinal f) = ℰ f"
by(induct f)(simp add:setFinal_def edges_face_def nextVertex_def)

lemma in_edges_in_vertices:
 "(x,y) ∈ ℰ(f::face) ⟹ x ∈ 𝒱 f ∧ y ∈ 𝒱 f"
apply(simp add:edges_face_eq nextVertex_def)
apply(cut_tac xs= "vertices f" and x= "hd(vertices f)" and y=x in nextElem_in)
apply(cases "vertices f")
apply(auto)
done


lemma vertices_conv_Union_edges:
 "𝒱(f::face) = (⋃(a,b)∈ℰ f. {a})"
apply(induct f)
apply(simp add:vertices_face_def edges_face_def)
apply blast
done


lemma nextVertex_in_edges: "v ∈ 𝒱 f ⟹ (v, f ∙ v) ∈ edges f"
by(auto simp:edges_face_def)

lemma prevVertex_in_edges:
 "⟦distinct(vertices f); v ∈ 𝒱 f⟧ ⟹ (f⇗-1⇖ ∙ v, v) ∈ edges f"
by(simp add:edges_face_eq)


subsection ‹Triangles›

lemma vertices_triangle:
   "|vertices f| = 3 ⟹ a ∈ 𝒱 f ⟹
  distinct (vertices f) ⟹
  𝒱 f = {a, f ∙ a, f ∙ (f ∙ a)}"
proof -
  assume "|vertices f| = 3"
  then obtain a1 a2 a3 where "vertices f = [a1, a2, a3]"
    by (auto dest!:  length3D)
  moreover assume "a ∈ 𝒱 f"
  moreover assume "distinct (vertices f)"
  ultimately show ?thesis
    by (simp, elim disjE) (auto simp add: nextVertex_def)
qed

(* could be generalized from 3 to n
   but presburger would no longer do the job *)
lemma tri_next3_id:
 "|vertices f| = 3 ⟹ distinct(vertices f) ⟹ v ∈ 𝒱 f
  ⟹ f ∙ (f ∙ (f ∙ v)) = v"
apply(subgoal_tac "∀(i::nat) < 3. (((((i+1) mod 3)+1) mod 3)+1) mod 3 = i")
 apply(clarsimp simp:in_set_conv_nth nextVertex_nth)
apply(presburger)
done


lemma triangle_nextVertex_prevVertex:
 "|vertices f| = 3 ⟹ a ∈ 𝒱 f ⟹
  distinct (vertices f) ⟹
  f ∙ (f ∙ a) = f⇗-1⇖ ∙ a"
proof -
  assume "|vertices f| = 3"
  then obtain a1 a2 a3 where "vertices f = [a1, a2, a3]"
    by (auto dest!:length3D)
  moreover assume "a ∈ 𝒱 f"
  moreover assume "distinct (vertices f)"
  ultimately show ?thesis
    by (simp, elim disjE) (auto simp add: nextVertex_def prevVertex_def)
qed

subsection ‹Quadrilaterals›


lemma vertices_quad:
  "|vertices f| = 4 ⟹ a ∈ 𝒱 f ⟹
  distinct (vertices f) ⟹
  𝒱 f = {a, f ∙ a, f ∙ (f ∙ a), f ∙ (f ∙ (f ∙ a))}"
proof -
  assume "|vertices f| = 4"
  then obtain a1 a2 a3 a4 where "vertices f = [a1, a2, a3, a4]"
    by (auto dest!: length4D)
  moreover assume "a ∈ 𝒱 f"
  moreover assume "distinct (vertices f)"
  ultimately show ?thesis
    by (simp, elim disjE) (auto simp add: nextVertex_def)
qed

lemma quad_next4_id:
 "⟦ |vertices f| = 4; distinct(vertices f); v ∈ 𝒱 f ⟧ ⟹
  f ∙ (f ∙ (f ∙ (f ∙ v))) = v"
apply(subgoal_tac "∀(i::nat) < 4.
 (((((((i+1) mod 4)+1) mod 4)+1) mod 4)+1) mod 4 = i")
 apply(clarsimp simp:in_set_conv_nth nextVertex_nth)
apply(presburger)
done


lemma quad_nextVertex_prevVertex:
 "|vertices f| = 4 ⟹ a ∈ 𝒱 f ⟹ distinct (vertices f) ⟹
  f ∙ (f ∙ (f ∙ a)) = f⇗-1⇖ ∙ a"
proof -
  assume "|vertices f| = 4"
  then obtain a1 a2 a3 a4 where "vertices f = [a1, a2, a3, a4]"
    by (auto dest!: length4D)
  moreover assume "a ∈ 𝒱 f"
  moreover assume "distinct (vertices f)"
  ultimately show ?thesis
    by (auto) (auto simp add: nextVertex_def prevVertex_def)
qed

(*
lemma C0[dest]: "f ∈ set (facesAt g v) ⟹ v ∈ 𝒱 g"
  by (simp add: facesAt_def split: if_split_asm)
*)

lemma len_faces_sum: "|faces g| = |finals g| + |nonFinals g|"
by(simp add:finals_def nonFinals_def sum_length_filter_compl)


lemma graph_max_final_ex:
 "∃f∈set (finals (graph n)). |vertices f| = n"
proof (induct "n")
  case 0 then show ?case by (simp add: graph_def finals_def)
next
  case (Suc n) then show ?case
   by (simp add: graph_def finals_def)
qed


subsection‹No loops›

lemma distinct_no_loop2:
 "⟦ distinct(vertices f); v ∈ 𝒱 f; u ∈ 𝒱 f; u ≠ v ⟧ ⟹ f ∙ v ≠ v"
apply(frule split_list[of v])
apply(clarsimp simp: nextVertex_def neq_Nil_conv hd_append
  split:list.splits if_split_asm)
done

lemma distinct_no_loop1:
 "⟦ distinct(vertices f); v ∈ 𝒱 f; |vertices f| > 1 ⟧ ⟹ f ∙ v ≠ v"
apply(subgoal_tac "∃u ∈ 𝒱 f. u ≠ v")
 apply(blast dest:distinct_no_loop2)
apply(cases "vertices f") apply simp
apply(rename_tac a as)
apply (clarsimp simp:neq_Nil_conv)
done


subsection‹@{const between}›

lemma between_front[simp]:
 "v ∉ set us ⟹ between (u # us @ v # vs) u v = us"
by(simp add:between_def split_def)

lemma between_back:
 "⟦ v ∉ set us; u ∉ set vs; v ≠ u ⟧ ⟹ between (v # vs @ u # us) u v = us"
by(simp add:between_def split_def)


lemma next_between:
 "⟦distinct(vertices f); v ∈ 𝒱 f; u ∈ 𝒱 f; f ∙ v ≠ u ⟧
  ⟹ f ∙ v ∈ set(between (vertices f) v u)"
apply(frule split_list[of u])
apply(clarsimp)
apply(erule disjE)
 apply(clarsimp simp:set_between_id nextVertex_def hd_append split:list.split)
apply(erule disjE)
 apply(frule split_list[of v])
 apply(clarsimp simp: between_def split_def nextVertex_def split:list.split)
 apply(clarsimp simp:append_eq_Cons_conv)
apply(frule split_list[of v])
apply(clarsimp simp: between_def split_def nextVertex_def split:list.split)
apply(clarsimp simp: hd_append)
done


lemma next_between2:
 "⟦ distinct(vertices f); v ∈ 𝒱 f; u ∈ 𝒱 f; u ≠ v ⟧ ⟹
  v ∈ set(between (vertices f) u (f ∙ v))"
apply(frule split_list[of u])
apply(clarsimp)
apply(erule disjE)
 apply(clarsimp simp: nextVertex_def hd_append split:list.split)
 apply(rule conjI)
  apply(clarsimp)
 apply(frule split_list[of v])
 apply(clarsimp simp: between_def split_def split:list.split)
 apply(fastforce simp: append_eq_Cons_conv)
apply(frule split_list[of v])
apply(clarsimp simp: between_def split_def nextVertex_def split:list.splits)
apply(clarsimp simp: hd_append)
apply(erule disjE)
 apply(clarsimp)
apply(frule split_list)
apply(fastforce)
done


(* distinctness seems not to be necessary but simplifies the proof *)
lemma between_next_empty:
 "distinct(vertices f) ⟹ between (vertices f) v (f ∙ v) = []"
apply(cases "v ∈ 𝒱 f")
 apply(frule split_list)
 apply(clarsimp simp:between_def split_def nextVertex_def
   neq_Nil_conv hd_append split:list.split)
 apply(clarsimp simp:between_def split_def nextVertex_def)
apply(cases "vertices f")
 apply simp
apply simp
done


lemma unroll_between_next2:
 "⟦ distinct(vertices f); u ∈ 𝒱 f; v ∈ 𝒱 f; u ≠ v ⟧ ⟹
  between (vertices f) u (f ∙ v) = between (vertices f) u v @ [v]"
using split_between[OF _ _ _ next_between2]
by (simp add: between_next_empty split:if_split_asm)


lemma nextVertex_eq_lemma:
 "⟦ distinct(vertices f); x ∈ 𝒱 f; y ∈ 𝒱 f; x ≠ y;
    v ∈ set(x # between (vertices f) x y) ⟧ ⟹
  f ∙ v = nextElem (x # between (vertices f) x y @ [y]) z v"
apply(drule split_list[of x])
apply(simp add:nextVertex_def)
apply(erule disjE)
 apply(clarsimp)
 apply(erule disjE)
  apply(drule split_list)
  apply(clarsimp simp add:between_def split_def hd_append split:list.split)
  apply(fastforce simp:append_eq_Cons_conv)
 apply(drule split_list)
 apply(clarsimp simp add:between_def split_def hd_append split:list.split)
 apply(fastforce simp:append_eq_Cons_conv)
apply(clarsimp)
 apply(erule disjE)
 apply(drule split_list[of y])
 apply(clarsimp simp:between_def split_def)
 apply(erule disjE)
  apply(drule split_list[of v])
  apply(fastforce simp: hd_append neq_Nil_conv split:list.split)
 apply(drule split_list[of v])
 apply(clarsimp)
 apply(clarsimp simp: hd_append split:list.split)
 apply(fastforce simp:append_eq_Cons_conv)
apply(drule split_list[of y])
apply(clarsimp simp:between_def split_def)
apply(drule split_list[of v])
apply(clarsimp)
apply(clarsimp simp: hd_append split:list.split)
apply(clarsimp simp:append_eq_Cons_conv)
apply(fastforce simp: hd_append neq_Nil_conv split:list.split)
done

end