What I had in mind was something as can be found e.g. in src/HOL/Library/Dlist.thy:
definition empty :: "'a dlist" where "empty = Dlist []" definition insert :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where "insert x dxs = Dlist (List.insert x (list_of_dlist dxs))" definition remove :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where "remove x dxs = Dlist (remove1 x (list_of_dlist dxs))" definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist" where "map f dxs = Dlist (remdups (List.map f (list_of_dlist dxs)))" definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where "filter P dxs = Dlist (List.filter P (list_of_dlist dxs))" lemma list_of_dlist_empty [simp, code abstract]: "list_of_dlist empty = []" by (simp add: empty_def) lemma list_of_dlist_insert [simp, code abstract]: "list_of_dlist (insert x dxs) = List.insert x (list_of_dlist dxs)" by (simp add: insert_def) lemma list_of_dlist_remove [simp, code abstract]: "list_of_dlist (remove x dxs) = remove1 x (list_of_dlist dxs)" by (simp add: remove_def) lemma list_of_dlist_map [simp, code abstract]: "list_of_dlist (map f dxs) = remdups (List.map f (list_of_dlist dxs))" by (simp add: map_def) lemma list_of_dlist_filter [simp, code abstract]: "list_of_dlist (filter P dxs) = List.filter P (list_of_dlist dxs)" by (simp add: filter_def) Here, the derived equations *are* simplification rules, in the sense that they simplify from abstract to concrete values. This pattern enables convient proofs of abstract equational properties by using extensionality and then default simplicifcation. Hence the idea of ».simp«. Anyway, I do not object to ».rep«, although the disadvantage is that the corresponding operation will seldom be named »rep«. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev