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

by simp

lift_definition member :: "'a dlist => 'a => bool" is List.member

by simp

lift_definition length :: "'a dlist => nat" is List.length

by simp

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

by simp

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

by simp

lift_definition concat :: "'a dlist dlist => 'a dlist" is "remdups o List.concat"

proof -

{

fix x y

have "list_all2 cr_dlist x y ==> x = List.map list_of_dlist y"

unfolding list_all2_def cr_dlist_def by (induction x y rule: list_induct2') auto

}

note cr = this

fix x :: "'a list list" and y :: "'a list list"

assume "(list_all2 cr_dlist OO Lifting.invariant distinct OO (list_all2 cr_dlist)¯¯) x y"

then have "x = y" by (auto dest: cr simp add: Lifting.invariant_def)

then show "?thesis x y" unfolding Lifting.invariant_def by auto

qed

text {* We can export code: *}

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

end