Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Lift_DList.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Quotient_Examples/Lift_DList.thy
    Author:     Ondrej Kuncar
*)

theory Lift_DList
imports Main
begin

subsection \<open>The type of distinct lists\<close>

typedef 'a dlist = "{xs::'a list. distinct xs}"
  morphisms list_of_dlist Abs_dlist
proof
  show "[] \ {xs. distinct xs}" by simp
qed

setup_lifting type_definition_dlist

text \<open>Fundamental operations:\<close>

lift_definition empty :: "'a dlist" is "[]"
by simp

lift_definition insert :: "'a \ 'a dlist \ 'a dlist" is List.insert
by simp

lift_definition remove :: "'a \ 'a dlist \ 'a dlist" is List.remove1
by simp

lift_definition map :: "('a \ 'b) \ 'a dlist \ 'b dlist" is "\f. remdups o List.map f"
by simp

lift_definition filter :: "('a \ bool) \ 'a dlist \ 'a dlist" is List.filter
by simp

text \<open>Derived operations:\<close>

lift_definition null :: "'a dlist \ bool" is List.null .

lift_definition member :: "'a dlist \ 'a \ bool" is List.member .

lift_definition length :: "'a dlist \ nat" is List.length .

lift_definition fold :: "('a \ 'b \ 'b) \ 'a dlist \ 'b \ 'b" is List.fold .

lift_definition foldr :: "('a \ 'b \ 'b) \ 'a dlist \ 'b \ 'b" is List.foldr .

lift_definition concat :: "'a dlist dlist \ 'a dlist" is "remdups o List.concat" by auto

text \<open>We can export code:\<close>

export_code empty insert remove map filter null member length fold foldr concat in SML
  file_prefix dlist

end

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.