(* 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)"
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 -
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]
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 {* @{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(simp add:edges_face_def)
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(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:
"\<V>(f::face) = (\<Union>(a,b)∈\<E> f. {a})"
apply(induct f)
apply(simp add:vertices_face_def edges_face_def)
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"
by(simp add:edges_face_eq)
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 *}
lemma vertices_quad:
"|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
lemma quad_next4_id:
"[| |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
lemma quad_nextVertex_prevVertex:
"|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"
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 ∈ \<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(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(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)
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))
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|)
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
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
lemma vertices_quad:
[| |vertices f| = 4; a ∈ \<V> f; distinct (vertices f) |] ==> \<V> f = {a, f • a, f • (f • a), f • (f • (f • a))}
lemma quad_next4_id:
[| |vertices f| = 4; distinct (vertices f); v ∈ \<V> f |] ==> f • (f • (f • (f • v))) = v
lemma quad_nextVertex_prevVertex:
[| |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
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
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