src/HOL/Quotient_Examples/Lift_DList.thy
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (23 months ago)
changeset 66816 212a3334e7da
parent 63167 0909deb8059b
child 70009 435fb018e8ee
permissions -rw-r--r--
more fundamental definition of div and mod on int
     1 (*  Title:      HOL/Quotient_Examples/Lift_DList.thy
     2     Author:     Ondrej Kuncar
     3 *)
     4 
     5 theory Lift_DList
     6 imports Main
     7 begin
     8 
     9 subsection \<open>The type of distinct lists\<close>
    10 
    11 typedef 'a dlist = "{xs::'a list. distinct xs}"
    12   morphisms list_of_dlist Abs_dlist
    13 proof
    14   show "[] \<in> {xs. distinct xs}" by simp
    15 qed
    16 
    17 setup_lifting type_definition_dlist
    18 
    19 text \<open>Fundamental operations:\<close>
    20 
    21 lift_definition empty :: "'a dlist" is "[]"
    22 by simp
    23   
    24 lift_definition insert :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" is List.insert
    25 by simp
    26 
    27 lift_definition remove :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" is List.remove1
    28 by simp
    29 
    30 lift_definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist" is "\<lambda>f. remdups o List.map f"
    31 by simp
    32 
    33 lift_definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" is List.filter
    34 by simp
    35 
    36 text \<open>Derived operations:\<close>
    37 
    38 lift_definition null :: "'a dlist \<Rightarrow> bool" is List.null .
    39 
    40 lift_definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" is List.member .
    41 
    42 lift_definition length :: "'a dlist \<Rightarrow> nat" is List.length .
    43 
    44 lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.fold .
    45 
    46 lift_definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.foldr .
    47 
    48 lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat" by auto
    49 
    50 text \<open>We can export code:\<close>
    51 
    52 export_code empty insert remove map filter null member length fold foldr concat in SML
    53 
    54 end