[isabelle-dev] sets and code generation

[Christian Sternagel]

Maybe the AFP entry for executable matrix operations is useful for you.

http://afp.sourceforge.net/entries/Matrix.shtml

cheers

chris

On 03/23/2012 07:45 PM, Jesus Aransay wrote:
> Dear all,
>
> after reading the thread about code generation from sets I was
> wondering myself if there would be any chance to apply such ideas to
> the definition of matrices in the distribution
> (HOL/Matrix/Matrix.thy).
>
> The matrix type definition reads as follows:
>
> type_synonym 'a infmatrix = "nat \<Rightarrow>  nat \<Rightarrow>  'a"
>
> definition nonzero_positions :: "(nat \<Rightarrow>  nat \<Rightarrow>
> 'a::zero) \<Rightarrow>  (nat \<times>  nat) set" where
>    "nonzero_positions A = {pos. A (fst pos) (snd pos) ~= 0}"
>
> typedef 'a matrix = "{(f::(nat \<Rightarrow>  nat \<Rightarrow>
> 'a::zero)). finite (nonzero_positions f)}"
> proof -
>    have "(\<lambda>j i. 0) \<in>  {(f::(nat \<Rightarrow>  nat
> \<Rightarrow>  'a::zero)). finite (nonzero_positions f)}"
>      by (simp add: nonzero_positions_def)
>    then show ?thesis by auto
> qed
>
> I know there is an alternative way to get that, by means of sparse
> matrices (SparseMatrix.thy), but it demands translating every
> operation over the matrix type to its equivalent version for "sparse
> matrices", which may be sometimes hard work.
>
> Thanks in advance for any hint,
>
> Jesus
>
> On Wed, Mar 21, 2012 at 5:40 PM, Florian Haftmann
> <florian.haftmann at informatik.tu-muenchen.de>  wrote:
>> Hi Christian,
>>
>>> since set is a proper type some code equations that used to work, no
>>> longer do, e.g.,
>>>
>>> "op |>  = {(x, y). supt_impl x y}"
>>
>> there is a couple of issues you are hitting at here.
>>
>> A. The (re-)introduction of the set type constructor
>>
>> See
>> http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg01736.html
>> for one possible entry into the motivation and discussion concerning that.
>>
>> B. The default code generation for setup
>>
>> You can always turn back to sets-as-predicates by
>>
>>         code_datatype Collect
>>
>> and then proving appropriate theorems for the set operation etc. – this
>> would fir best into a library theory which could then be part of the
>> distribution.  But I guess your issue is mainly with…
>>
>> C. Relations
>>
>> Both kinds of relations 'a =>  'a =>  bool and ('a * 'a) set are present
>> in their own right, but with disjoint developments in the HOL theoris.
>> Note that you can convert between both using pred/set conversions, the
>> same infrastructure as inductive_set is using.
>>
>> So, if you want predicate relations, it seems to be best to convert your
>> stuff to them, filling existing gaps in the HOL theories by additional
>> definitions and suitable pred/set conversion declarations.
>>
>> See theory "Relation" for examples for making use of pred/set
>> conversions by means of attributes "to_set" and "to_pred"; and
>> declarations of pred/set conversions by means of attribute "pred_set_conv".
>>
>> Unfortunately, there is no reference for them in the Isabelle Reference
>> Manual.  Maybe one day this is subsumed by an emerging generic »lifting«
>> infrastructure.
>>
>> Hope this helps,
>>         Florian
>>
>> --
>>
>> PGP available:
>> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>
>
>