Theory Enumerator

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

header {* Enumerating Patches *}

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