# Theory FaceDivision

Up to index of Isabelle/HOL/Tame

theory FaceDivision
imports Graph
begin

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

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
```