Quellcode-Bibliothek Lift_DList.thy Sprache: 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

quality100%

¤ 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.0.1Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.