[isabelle-dev] sets and code generation

[Jesus Aransay]

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
>



-- 
Jesús María Aransay Azofra
Universidad de La Rioja
Dpto. de Matemáticas y Computación
tlf.: (+34) 941299438 fax: (+34) 941299460
mail: jesus-maria.aransay at unirioja.es ; web: http://www.unirioja.es/cu/jearansa
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España