Theory FaceDivision

(*  ID:         $Id: FaceDivision.thy,v 1.3 2006/01/18 07:20:43 nipkow Exp $
    Author:     Gertrud Bauer, Tobias Nipkow
*)

header{* Subdividing a Face *}

theory FaceDivision
imports Graph
begin

constdefs split_face :: "face => vertex => vertex => vertex list => face × face"
 "split_face f ram1 ram2 newVs ≡ let vs = vertices f;
     f1 = [ram1] @ between vs ram1 ram2 @ [ram2];
     f2 = [ram2] @ between vs ram2 ram1 @ [ram1] in
     (Face (rev newVs @ f1) Nonfinal,
     Face (f2 @ newVs) Nonfinal)"


constdefs replacefacesAt ::
     "nat list => face => face list => face list list => face list list"
 "replacefacesAt ns f fs F ≡ mapAt ns (replace f fs) F"


constdefs makeFaceFinalFaceList :: "face => face list => face list"
  "makeFaceFinalFaceList f fs ≡ replace f [setFinal f] fs"

constdefs makeFaceFinal :: "face => graph => graph"
 "makeFaceFinal f g ≡
     Graph (makeFaceFinalFaceList f (faces g))
           (countVertices g)
           [makeFaceFinalFaceList f fs. fs ∈ faceListAt g]
           (heights g)"


constdefs heightsNewVertices :: "nat => nat => nat => nat list"
 "heightsNewVertices h1 h2 n ≡ [min (h1 + i + 1) (h2 + n - i). i ∈ [0 ..< n]]"

constdefs splitFace
    :: "graph => vertex => vertex => face => vertex list => face × face × graph"
 "splitFace g ram1 ram2 oldF newVs ≡
     let fs = faces g;
     n = countVertices g;
     Fs = faceListAt g;
     h = heights g;
     vs1 = between (vertices oldF) ram1 ram2;
     vs2 = between (vertices oldF) ram2 ram1;
     (f1, f2) = split_face oldF ram1 ram2 newVs;
     Fs = replacefacesAt vs1 oldF [f1] Fs;
     Fs = replacefacesAt vs2 oldF [f2] Fs;
     Fs = replacefacesAt [ram1] oldF [f2, f1] Fs;
     Fs = replacefacesAt [ram2] oldF [f1, f2] Fs;
     Fs = Fs @ replicate |newVs| [f1, f2] in
     (f1, f2, Graph ((replace oldF [f2] fs)@ [f1])
                        (n + |newVs| )
                        Fs
                        (h @ heightsNewVertices (h!ram1)(h!ram2) |newVs| ))"



consts subdivFace' :: "graph => face => vertex => nat => vertex option list => graph"
primrec "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];
            (f1, f2, g') = splitFace g u v f ws in
            subdivFace' g' f2 v 0 vos)"

constdefs subdivFace :: "graph => face => vertex option list => graph"
"subdivFace g f vos ≡ subdivFace' g f (the(hd vos)) 0 (tl vos)"

end