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
```