Theory FaceDivision

(*  Author:     Gertrud Bauer, Tobias Nipkow
*)

header{* 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 \<leftarrow> 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 \<leftarrow> [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