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:
 "fset (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