Theory Enumerator

Up to index of Isabelle/HOL/Tame

theory Enumerator
imports Graph Vector
begin

```(*  ID:         \$Id: Enumerator.thy,v 1.1 2006/01/04 13:43:39 nipkow Exp \$
Author:     Gertrud Bauer
*)

theory Enumerator
imports Graph Vector
begin

text {*
Generates an Enumeration of lists.
(See Kepler98, PartIII, section 8, p.11).

Used to construct all possible extensions of an unfinished outer
face \$F\$ with \$outer\$ vertices
by a new finished inner face with \$inner\$ vertices, such a fixed
edge \$e\$ of the outer face is also contained in the inner face.

Label the vertices  of \$F\$ consecutively
\$0, \ldots, outer-1\$, with \$0\$ and \$outer-1\$ the endpoints of \$e\$.

Generate all lists \$\$[a0, \ldots,  a_{inner_1}]\$\$ of length
\$inner\$,
%such that \$0 = a_0 \le a_1 \ldots a_{outer - 2} < a_{outer -1}\$.
such that \$0 = a_0 \le a_1 \ldots a_{inner - 2} < a_{inner -1}\$.
Every list represents an inner face, with vertices
\$v_0, \ldots, v_{inner-1}\$.

Construct the vertices \$v_0, \ldots, v_{inner - 1}\$ inductively:
If \$i = 1\$ or \$a_i \not = a_{i -1}\$, we set \$v_i\$ to the vertex
with index
\$a_i\$ of F. But if  \$a_i = a_{i -1}\$, we add a new vertex \$v_i\$
to the planar map.
The new face is to be drawn along the edge \$e\$ over the face \$F\$.

As we run over all \$inner\$ and all lists
\$[a0, \ldots,  a_{inner_1}]\$,
we run over all osibilites fro the finishe face along the edge
\$e\$ inside \$F\$.
*}

text{* \paragraph{Executable enumeration of patches} *}

constdefs enumBase :: "nat => nat list list"
"enumBase nmax ≡ [[i]. i ∈ [0 .. nmax]]"

constdefs enumAppend :: "nat => nat list list => nat list list"
"enumAppend nmax iss ≡ \<Squnion>is∈iss [is @ [n]. n ∈ [last is .. nmax]]"

constdefs enumerator :: "nat => nat => nat list list" (* precondition inner >= 3 *)
"enumerator inner outer ≡
let nmax = outer - 2; k = inner - 3 in
[[0] @ is @ [outer - 1]. is ∈ ((enumAppend nmax)^k) (enumBase nmax)]"

enumTab :: "nat list list vector vector"
"enumTab ≡ [| enumerator inner outer. inner < 9, outer < 9 |]"

(* never used with > 8 but easier this way *)
enum :: "nat => nat => nat list list"
"enum inner outer ≡ if inner < 9 & outer < 9 then enumTab[|inner,outer|]
else enumerator inner outer"

text{* \paragraph{Conversion to list of vertices} *}

consts hideDupsRec :: "'a => 'a list => 'a option list"
primrec "hideDupsRec a [] = []"
"hideDupsRec a (b#bs) =
(if a = b then None # hideDupsRec b bs
else Some b # hideDupsRec b bs)"

consts hideDups :: "'a list => 'a option list"
primrec "hideDups [] = []"
"hideDups (b#bs) = Some b # hideDupsRec b bs"

constdefs indexToVertexList :: "face => vertex => nat list => vertex option list" (* precondition hd is = 0 *)
"indexToVertexList f v is ≡ hideDups [fk•v. k ∈ is]"

end
```