Quelle  Lift_DList.thy

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

theory Lift_DList
imports Main
begin

subsection ‹The type of distinct lists›

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 ‹Fundamental operations:›

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 ‹Derived operations:›

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 ‹We can export code:›

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

end