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.haftm...@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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
