# Theory Lift_DList

Up to index of Isabelle/HOL/HOL-Quotient_Examples

theory Lift_DList
imports Quotient_List
`(*  Title:      HOL/Quotient_Examples/Lift_DList.thy    Author:     Ondrej Kuncar*)theory Lift_DListimports Main "~~/src/HOL/Library/Quotient_List"beginsubsection {* The type of distinct lists *}typedef 'a dlist = "{xs::'a list. distinct xs}"  morphisms list_of_dlist Abs_dlistproof  show "[] ∈ {xs. distinct xs}" by simpqedsetup_lifting type_definition_dlisttext {* Fundamental operations: *}lift_definition empty :: "'a dlist" is "[]"by simp  lift_definition insert :: "'a => 'a dlist => 'a dlist" is List.insertby simplift_definition remove :: "'a => 'a dlist => 'a dlist" is List.remove1by simplift_definition map :: "('a => 'b) => 'a dlist => 'b dlist" is "λf. remdups o List.map f"by simplift_definition filter :: "('a => bool) => 'a dlist => 'a dlist" is List.filterby simptext {* Derived operations: *}lift_definition null :: "'a dlist => bool" is List.nullby simplift_definition member :: "'a dlist => 'a => bool" is List.memberby simplift_definition length :: "'a dlist => nat" is List.lengthby simplift_definition fold :: "('a => 'b => 'b) => 'a dlist => 'b => 'b" is List.foldby simplift_definition foldr :: "('a => 'b => 'b) => 'a dlist => 'b => 'b" is List.foldrby simplift_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 autoqedtext {* We can export code: *}export_code empty insert remove map filter null member length fold foldr concat in SMLend`