products/sources/formale sprachen/Cobol/Test-Suite/SQL P/xts/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: function_image_nonempty.prf   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.17 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff