[isabelle] Is it possible to get back at a list after encapsulating it in a plain function ( as in Gauss-Jordan-Elim-Fun ? )



Hello,
       I am trying to encapsulate matrices/vectors/arrays/lists as functions, similar to the matrices in
Gauss-Jordan Elimination for Matrices Represented as Functions, but without passing the dimensions
explicitly.
For example,
------------------------------------------------------------------
definition "l2f (xs::'a list) = (λ (i::nat) . xs ! i)"
value "let a = l2f [10,11,12,13::real] in a 1"
------------------------------------------------------------------
Is it possible to define some
"( nat => 'a ) => nat" (the size of the original list)
or
"( nat => 'a ) => (nat × nat) " or "( nat => 'a ) => nat set" (the domain of the function) ?

If it is impossible to define a computable one, is it possible to define an incomputable specifictaion?

Du


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.