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


 The "function from indices to values" form throws away information, so you've got to supply it back when you try to invert. There's no way to extract the "length" of the original list from the function, as it's got to be well defined for every possible index (functions in HOL are total, even if the result isn't visibly defined). Your l2f function returns *some* value a for *any* index i that you pass it.

 One way of encoding the information you want might be a partial function, that's only defined for those indices in the original list, but that's likely to be less convenient to work with. Even then, you need to "know" that the function came from a list in order to find the length (to take, say, the largest index for which the output isn't None, you'll need to supply a proof that there *is* such a maximum).


On 19/10/17 08:10, ducis wrote:
        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
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)
"( 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?


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