Theory Enumerator

(*  Author:     Gertrud Bauer
*)

section ‹Enumerating Patches›

theory Enumerator
imports Graph IArray_Syntax
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}›

definition enumBase :: "nat ⇒ nat list list" where
 "enumBase nmax ≡ [[i]. i ← [0 ..< Suc nmax]]"

definition enumAppend :: "nat ⇒ nat list list ⇒ nat list list" where
 "enumAppend nmax iss ≡ ⨆⇘is∈iss⇙ [is @ [n]. n ← [last is ..< Suc nmax]]"

definition enumerator :: "nat ⇒ nat ⇒ nat list list" where (* precondition inner ≥ 3 *)
 "enumerator inner outer ≡
     let nmax = outer - 2; k = inner - 3 in 
     [[0] @ is @ [outer - 1]. is ← (enumAppend nmax ^^ k) (enumBase nmax)]"    

definition enumTab :: "nat list list iarray iarray" where
"enumTab ≡ ⟦ enumerator inner outer. inner < 9, outer < 9 ⟧"

(* never used with > 8 but easier this way *)
definition enum :: "nat ⇒ nat ⇒ nat list list" where
"enum inner outer ≡ if inner < 9 ∧ outer < 9 then enumTab⟦inner,outer⟧
                    else enumerator inner outer"

text‹\paragraph{Conversion to list of vertices}›

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

primrec hideDups :: "'a list ⇒ 'a option list" where
  "hideDups [] = []"
| "hideDups (b#bs) = Some b # hideDupsRec b bs"

definition indexToVertexList :: "face ⇒ vertex ⇒ nat list ⇒ vertex option list" where (* precondition hd is = 0 *)
 "indexToVertexList f v is ≡ hideDups [f⇗k⇖∙v. k ← is]" 

end