# Theory Plane4

Up to index of Isabelle/HOL/Tame

theory Plane4
imports While_Combinator Tame
begin

```(*  ID:         \$Id: Plane4.thy,v 1.1 2006/01/04 13:44:01 nipkow Exp \$
Author:     Tobias Nipkow
*)

theory Plane4
imports While_Combinator Tame
begin

constdefs
norm_subset :: "vertex list list => vertex list list => bool"
"norm_subset xs ys ≡ let zs = map rotate_min ys
in ∀x ∈ set xs. rotate_min x ∈ set zs"

consts remrevdups :: "'a list list => 'a list list"
primrec
"remrevdups [] = []"
"remrevdups (xs#xss) = (if xs mem xss ∨ rev xs mem xss then remrevdups xss
else xs # remrevdups xss)"

constdefs
find_cycles1 :: "nat => graph => vertex => vertex list list"
"find_cycles1 n g v ≡
snd(snd(
while (%(vs,wss,res). vs ≠ [])
(%(vs,wss,res).
let ws = hd wss in
if ws = [] then (tl vs, tl wss, res)
else if length vs = n
then (tl vs, tl wss, if last vs ∈ set ws then vs#res else res)
else let vs' = (if length vs + 1 = n then butlast vs else vs);
xs = filter (%x. x ∉ set vs') (neighbors g (hd ws)) in
(hd ws # vs, xs # tl ws # tl wss, res))
([v], [neighbors g v], [])
))"

find_cycles :: "nat => graph => vertex list list"
"find_cycles n g ≡
remrevdups(map rotate_min (foldr (%v vss. find_cycles1 n g v @ vss) (vertices g) []))"

constdefs
(* Not needed but could be used to get rid of makeTrianglesFinal
ok3 :: "graph => vertex list => bool"
"ok3 g vs  ≡
let f = [hd vs, hd(tl vs), hd(tl(tl vs))];
nf = rotate_min f; nrf = rotate_min(rev f)
in ∃f' ∈ set(map (rotate_min o vertices) (faces g)). f' = nf ∨ f' = nrf"

is_tame2 :: "graph => bool"
"is_tame2 g ≡ ∀vs ∈ set(find_cycles 3 g).
distinct vs ∧ |vs| = 3 ∧ is_cycle g vs --> ok3 g vs"
*)

ok42 :: "vertex list => vertex list list => vertex => vertex => vertex => vertex => bool"
"ok42 vs fs a b c d ==
norm_subset (tameConf1 a b c d) fs ∨
norm_subset (tameConf2 a b c d) fs ∨
norm_subset (tameConf2 b c d a) fs ∨
(EX e:set vs. e ∉ set[a,b,c,d] ∧
(norm_subset (tameConf3 a b c d e) fs ∨
norm_subset (tameConf3 b c d a e) fs ∨
norm_subset (tameConf3 c d a b e) fs ∨
norm_subset (tameConf3 d a b c e) fs ∨
norm_subset (tameConf4 a b c d e) fs)
)"

ok4 :: "graph => vertex list => bool"
"ok4 g vs  ≡
let fs = map vertices (faces g); gvs = vertices g;
a = hd vs; b = hd(tl vs); c = hd(tl(tl vs)); d = hd(tl(tl(tl vs)))
in ok42 gvs fs a b c d ∨ ok42 gvs fs d c b a"

is_tame3 :: "graph => bool"
"is_tame3 g ≡ ∀vs ∈ set(find_cycles 4 g).
is_cycle g vs ∧ distinct vs ∧ |vs| = 4 --> ok4 g vs"

end
```