Theory Plane4

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

header {* Checking Final Quadrilaterals *}

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