FLAT_CONV : conv
STRUCTURE
listLib
SYNOPSIS
Computes by inference the result of flattening a list of lists.
DESCRIPTION
FLAT_CONV takes a term tm in the following form: 
   FLAT [[x00;...x0n]; ...; [xm0;...xmn]]
It returns the theorem 
   |- FLAT [[x00;...x0n];...;[xm0;...xmn]] = [x00;...x0n;...;xm0;...xmn]

FAILURE
FLAT_CONV tm fails if tm is not of the form described above.
EXAMPLE
Evaluating 
   FLAT_CONV “FLAT [[0;2;4];[0;1;2;3;4]]”;
returns the following theorem: 
   |- FLAT[[0;2;4];[0;1;2;3;4]] = [0;2;4;0;1;2;3;4]
SEEALSO
FOLDL_CONV, FOLDR_CONV, list_FOLD_CONV
HOL  Kananaskis-14