# Theory GraphProps

Up to index of Isabelle/HOL/Tame

theory GraphProps
imports Graph
begin

```(*  ID:         \$Id: GraphProps.thy,v 1.1 2006/01/04 13:43:50 nipkow Exp \$
Author:     Gertrud Bauer, Tobias Nipkow
*)

header{* Properties of Graph Utilities *}

theory GraphProps
imports Graph
begin

ML"fast_arith_neq_limit := 3"

lemma final_setFinal[iff]: "final(setFinal f)"

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 -
def 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]
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 {* @{text nextVertex} *}

lemma nextVertex_in_face'[simp]:
"vertices f ≠ [] ==> f • v ∈ \<V> f"
proof -
assume f: "vertices f ≠ []"
def 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(fastsimp simp:neq_Nil_conv)
done
qed

lemma nextVertex_in_face[simp]:
"v ∈ set (vertices f) ==> f • v ∈ \<V> f"
by (auto intro: nextVertex_in_face')

lemma nextVertex_prevVertex[simp]:
"[| distinct(vertices f); v ∈ \<V> f |]
==> f • (f-1 • v) = v"
by(simp add:prevVertex_def nextVertex_def nextElem_prevElem)

lemma prevVertex_nextVertex[simp]:
"[| distinct(vertices f); v ∈ \<V> f |]
==> f-1 • (f • v) = v"
by(simp add:prevVertex_def nextVertex_def prevElem_nextElem)

lemma prevVertex_in_face[simp]:
"v ∈ \<V> f ==> f-1 • v ∈ \<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 {* @{text"\<E>"} *}

lemma finite_edges: "finite(\<E>(f::face))"
apply(rule finite_surj[of "\<V> f" _ "%v. (v, f • v)"])
apply simp
apply blast
done

lemma edges_face_eq:
"((a,b) ∈ \<E> (f::face)) = ((f • a = b) ∧ a ∈ \<V> f)"
by (auto simp add: edges_face_def)

lemma edges_setFinal[simp]: "\<E>(setFinal f) = \<E> f"
by(induct f)(simp add:setFinal_def edges_face_def nextVertex_def)

lemma in_edges_in_vertices:
"(x,y) ∈ \<E>(f::face) ==> x ∈ \<V> f ∧ y ∈ \<V> f"
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:
"\<V>(f::face) = (\<Union>(a,b)∈\<E> f. {a})"
apply(induct f)
apply blast
done

lemma nextVertex_in_edges: "v ∈ \<V> f ==> (v, f • v) ∈ edges f"
by(auto simp:edges_face_def)

lemma prevVertex_in_edges:
"[|distinct(vertices f); v ∈ \<V> f|] ==> (f-1 • v, v) ∈ edges f"

subsection {* Triangles *}

lemma vertices_triangle:
"|vertices f| = 3 ==> a ∈ \<V> f ==>
distinct (vertices f) ==>
\<V> 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 ∈ \<V> 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 ∈ \<V> f
==> f • (f • (f • v)) = v"
apply(subgoal_tac "ALL (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 ∈ \<V> 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 ∈ \<V> f"
moreover assume "distinct (vertices f)"
ultimately show ?thesis
by (simp, elim disjE) (auto simp add: nextVertex_def prevVertex_def)
qed

subsection {* Quadrilaterals *}

"|vertices f| = 4 ==> a ∈ \<V> f ==>
distinct (vertices f) ==>
\<V> 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 ∈ \<V> f"
moreover assume "distinct (vertices f)"
ultimately show ?thesis
by (simp, elim disjE) (auto simp add: nextVertex_def)
qed

"[| |vertices f| = 4; distinct(vertices f); v ∈ \<V> f |] ==>
f • (f • (f • (f • v))) = v"
apply(subgoal_tac "ALL (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

"|vertices f| = 4 ==> a ∈ \<V> 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 ∈ \<V> 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 ∈ \<V> g"
by (simp add: facesAt_def split: split_if_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 ∈ \<V> f; u ∈ \<V> 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 split_if_asm)
done

lemma distinct_no_loop1:
"[| distinct(vertices f); v ∈ \<V> f; |vertices f| > 1 |] ==> f • v ≠ v"
apply(subgoal_tac "∃u ∈ \<V> 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"

lemma between_back:
"[| v ∉ set us; u ∉ set vs; v ≠ u |] ==> between (v # vs @ u # us) u v = us"

lemma next_between:
"[|distinct(vertices f); v ∈ \<V> f; u ∈ \<V> 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 ∈ \<V> f; u ∈ \<V> 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(fastsimp 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(fastsimp)
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 ∈ \<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_next:
"[| distinct(vertices f); u ∈ \<V> f; v ∈ \<V> f; f • v ≠ u |] ==>
between (vertices f) v u = f • v # between (vertices f) (f • v) u"
using split_between[OF _ _ _ next_between]
apply (simp add: between_next_empty split:split_if_asm)
apply(blast dest:distinct_no_loop2 intro:sym)
done

lemma unroll_between_next2:
"[| distinct(vertices f); u ∈ \<V> f; v ∈ \<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:split_if_asm)

lemma nextVertex_eq_lemma:
"[| distinct(vertices f); x ∈ \<V> f; y ∈ \<V> 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(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(fastsimp simp:append_eq_Cons_conv)
apply(drule split_list)
apply(clarsimp simp add:between_def split_def hd_append split:list.split)
apply(fastsimp 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(fastsimp 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(fastsimp 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(fastsimp simp: hd_append neq_Nil_conv split:list.split)
done

lemma nextVertex_eq_if_between_eq:
"[| between (vertices f) x y = between (vertices f') x y;
distinct(vertices f); distinct(vertices f'); x ≠ y;
x ∈ \<V> f; y ∈ \<V> f; x ∈ \<V> f'; y ∈ \<V> f';
v ∈ set(x # between (vertices f) x y) |] ==>
f • v = f' • v"
by(simp add:nextVertex_eq_lemma[where z = 0])

end
```

lemma final_setFinal:

`  final (setFinal f)`

lemma eq_setFinal_iff:

`  (f = setFinal f) = final f`

lemma setFinal_eq_iff:

`  (setFinal f = f) = final f`

lemma distinct_vertices:

`  distinct (vertices g)`

### @{const nextElem}

lemma nextElem_append:

`  y ∉ set xs ==> nextElem (xs @ ys) d y = nextElem ys d y`

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)```

lemma nextElem_notin_butlast:

`  y ∉ set (butlast xs) ==> nextElem xs x y = x`

lemma nextElem_in:

`  nextElem xs x y ∈ set (x # xs)`

lemma nextElem_notin:

`  a ∉ set as ==> nextElem as c a = c`

lemma nextElem_last:

`  distinct xs ==> nextElem xs c (last xs) = c`

lemma prevElem_nextElem:

```  [| distinct xs; x ∈ set xs |]
==> nextElem (rev xs) (last xs) (nextElem xs (hd xs) x) = x```

lemma nextElem_prevElem:

```  [| distinct xs; x ∈ set xs |]
==> nextElem xs (hd xs) (nextElem (rev xs) (last xs) x) = x```

lemma nextElem_nth:

```  [| distinct xs; i < |xs| |]
==> nextElem xs z (xs ! i) = (if |xs| = i + 1 then z else xs ! (i + 1))```

### @{text nextVertex}

lemma nextVertex_in_face':

`  vertices f ≠ [] ==> f • v ∈ \<V> f`

lemma nextVertex_in_face:

`  v ∈ \<V> f ==> f • v ∈ \<V> f`

lemma nextVertex_prevVertex:

`  [| distinct (vertices f); v ∈ \<V> f |] ==> f • (f-1 • v) = v`

lemma prevVertex_nextVertex:

`  [| distinct (vertices f); v ∈ \<V> f |] ==> f-1 • (f • v) = v`

lemma prevVertex_in_face:

`  v ∈ \<V> f ==> f-1 • v ∈ \<V> f`

lemma nextVertex_nth:

```  [| distinct (vertices f); i < |vertices f| |]
==> f • (vertices f ! i) = vertices f ! ((i + 1) mod |vertices f|)```

### @{text"\<E>"}

lemma finite_edges:

`  finite (\<E> f)`

lemma edges_face_eq:

`  ((a, b) ∈ \<E> f) = (f • a = b ∧ a ∈ \<V> f)`

lemma edges_setFinal:

`  \<E> (setFinal f) = \<E> f`

lemma in_edges_in_vertices:

`  (x, y) ∈ \<E> f ==> x ∈ \<V> f ∧ y ∈ \<V> f`

lemma vertices_conv_Union_edges:

`  \<V> f = (UN (a, b):\<E> f. {a})`

lemma nextVertex_in_edges:

`  v ∈ \<V> f ==> (v, f • v) ∈ \<E> f`

lemma prevVertex_in_edges:

`  [| distinct (vertices f); v ∈ \<V> f |] ==> (f-1 • v, v) ∈ \<E> f`

### Triangles

lemma vertices_triangle:

```  [| triangle f; a ∈ \<V> f; distinct (vertices f) |]
==> \<V> f = {a, f • a, f • (f • a)}```

lemma tri_next3_id:

`  [| triangle f; distinct (vertices f); v ∈ \<V> f |] ==> f • (f • (f • v)) = v`

lemma triangle_nextVertex_prevVertex:

`  [| triangle f; a ∈ \<V> f; distinct (vertices f) |] ==> f • (f • a) = f-1 • a`

```  [| |vertices f| = 4; a ∈ \<V> f; distinct (vertices f) |]
==> \<V> f = {a, f • a, f • (f • a), f • (f • (f • a))}```

```  [| |vertices f| = 4; distinct (vertices f); v ∈ \<V> f |]
==> f • (f • (f • (f • v))) = v```

```  [| |vertices f| = 4; a ∈ \<V> f; distinct (vertices f) |]
==> f • (f • (f • a)) = f-1 • a```

lemma C0:

`  f ∈ set (facesAt g v) ==> v ∈ \<V> g`

lemma len_faces_sum:

`  |faces g| = |finals g| + |nonFinals g|`

lemma graph_max_final_ex:

`  ∃f∈set (finals (graph n)). |vertices f| = n`

### No loops

lemma distinct_no_loop2:

`  [| distinct (vertices f); v ∈ \<V> f; u ∈ \<V> f; u ≠ v |] ==> f • v ≠ v`

lemma distinct_no_loop1:

`  [| distinct (vertices f); v ∈ \<V> f; 1 < |vertices f| |] ==> f • v ≠ v`

### @{const between}

lemma between_front:

`  v ∉ set us ==> between (u # us @ v # vs) u v = us`

lemma between_back:

`  [| v ∉ set us; u ∉ set vs; v ≠ u |] ==> between (v # vs @ u # us) u v = us`

lemma next_between:

```  [| distinct (vertices f); v ∈ \<V> f; u ∈ \<V> f; f • v ≠ u |]
==> f • v ∈ set (between (vertices f) v u)```

lemma next_between2:

```  [| distinct (vertices f); v ∈ \<V> f; u ∈ \<V> f; u ≠ v |]
==> v ∈ set (between (vertices f) u (f • v))```

lemma between_next_empty:

`  distinct (vertices f) ==> between (vertices f) v (f • v) = []`

lemma unroll_between_next:

```  [| distinct (vertices f); u ∈ \<V> f; v ∈ \<V> f; f • v ≠ u |]
==> between (vertices f) v u = f • v # between (vertices f) (f • v) u```

lemma unroll_between_next2:

```  [| distinct (vertices f); u ∈ \<V> f; v ∈ \<V> f; u ≠ v |]
==> between (vertices f) u (f • v) = between (vertices f) u v @ [v]```

lemma nextVertex_eq_lemma:

```  [| distinct (vertices f); x ∈ \<V> f; y ∈ \<V> f; x ≠ y;
v ∈ set (x # between (vertices f) x y) |]
==> f • v = nextElem (x # between (vertices f) x y @ [y]) z v```

lemma nextVertex_eq_if_between_eq:

```  [| between (vertices f) x y = between (vertices f') x y; distinct (vertices f);
distinct (vertices f'); x ≠ y; x ∈ \<V> f; y ∈ \<V> f; x ∈ \<V> f';
y ∈ \<V> f'; v ∈ set (x # between (vertices f) x y) |]
==> f • v = f' • v```