Theory FaceDivision

(*  Author:     Gertrud Bauer, Tobias Nipkow
*)

section‹Subdividing a Face›

theory FaceDivision
imports Graph
begin

definition split_face :: "face ⇒ vertex ⇒ vertex ⇒ vertex list ⇒ face × face" where
 "split_face f ram⇩1 ram⇩2 newVs ≡ let vs = vertices f;
     f⇩1 = [ram⇩1] @ between vs ram⇩1 ram⇩2 @ [ram⇩2];
     f⇩2 = [ram⇩2] @ between vs ram⇩2 ram⇩1 @ [ram⇩1] in
     (Face (rev newVs @ f⇩1) Nonfinal,
     Face (f⇩2 @ newVs) Nonfinal)"


definition replacefacesAt :: "nat list ⇒ face ⇒ face list ⇒ face list list ⇒ face list list" where
 "replacefacesAt ns f fs F ≡ mapAt ns (replace f fs) F"


definition makeFaceFinalFaceList :: "face ⇒ face list ⇒ face list" where
  "makeFaceFinalFaceList f fs ≡ replace f [setFinal f] fs"

definition makeFaceFinal :: "face ⇒ graph ⇒ graph" where
 "makeFaceFinal f g ≡
     Graph (makeFaceFinalFaceList f (faces g))
           (countVertices g)
           [makeFaceFinalFaceList f fs. fs ← faceListAt g]
           (heights g)"


definition heightsNewVertices :: "nat ⇒ nat ⇒ nat ⇒ nat list" where
 "heightsNewVertices h⇩1 h⇩2 n ≡ [min (h⇩1 + i + 1) (h⇩2 + n - i). i ← [0 ..< n]]"

definition splitFace
 :: "graph ⇒ vertex ⇒ vertex ⇒ face ⇒ vertex list ⇒ face × face × graph" where
 "splitFace g ram⇩1 ram⇩2 oldF newVs ≡
     let fs = faces g;
     n = countVertices g;
     Fs = faceListAt g;
     h = heights g;
     vs⇩1 = between (vertices oldF) ram⇩1 ram⇩2;
     vs⇩2 = between (vertices oldF) ram⇩2 ram⇩1;
     (f⇩1, f⇩2) = split_face oldF ram⇩1 ram⇩2 newVs;
     Fs = replacefacesAt vs⇩1 oldF [f⇩1] Fs;
     Fs = replacefacesAt vs⇩2 oldF [f⇩2] Fs;
     Fs = replacefacesAt [ram⇩1] oldF [f⇩2, f⇩1] Fs;
     Fs = replacefacesAt [ram⇩2] oldF [f⇩1, f⇩2] Fs;
     Fs = Fs @ replicate |newVs| [f⇩1, f⇩2] in
     (f⇩1, f⇩2, Graph ((replace oldF [f⇩2] fs)@ [f⇩1])
                        (n + |newVs| )
                        Fs
                        (h @ heightsNewVertices (h!ram⇩1)(h!ram⇩2) |newVs| ))"



primrec subdivFace' :: "graph ⇒ face ⇒ vertex ⇒ nat ⇒ vertex option list ⇒ graph" where
  "subdivFace' g f u n [] = makeFaceFinal f g"
| "subdivFace' g f u n (vo#vos) =
     (case vo of None ⇒ subdivFace' g f u (Suc n) vos
         | (Some v) ⇒
            if f∙u = v ∧ n = 0
            then subdivFace' g f v 0 vos
            else let ws = [countVertices g  ..< countVertices g + n];
            (f⇩1, f⇩2, g') = splitFace g u v f ws in
            subdivFace' g' f⇩2 v 0 vos)"

definition subdivFace :: "graph ⇒ face ⇒ vertex option list ⇒ graph" where
"subdivFace g f vos ≡ subdivFace' g f (the(hd vos)) 0 (tl vos)"

end