author | kuncar |
Wed, 04 Apr 2012 17:51:12 +0200 | |
changeset 47361 | 87c0eaf04bad |
parent 47308 | 9caab698dbe4 |
child 49834 | b27bbb021df1 |
permissions | -rw-r--r-- |
47308 | 1 |
(* Title: HOL/Quotient_Examples/Lift_DList.thy |
2 |
Author: Ondrej Kuncar |
|
3 |
*) |
|
4 |
||
5 |
theory Lift_DList |
|
6 |
imports Main "~~/src/HOL/Library/Quotient_List" |
|
7 |
begin |
|
8 |
||
9 |
subsection {* The type of distinct lists *} |
|
10 |
||
11 |
typedef (open) '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 {* Fundamental operations: *} |
|
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 {* Derived operations: *} |
|
37 |
||
38 |
lift_definition null :: "'a dlist \<Rightarrow> bool" is List.null |
|
39 |
by simp |
|
40 |
||
41 |
lift_definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" is List.member |
|
42 |
by simp |
|
43 |
||
44 |
lift_definition length :: "'a dlist \<Rightarrow> nat" is List.length |
|
45 |
by simp |
|
46 |
||
47 |
lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.fold |
|
48 |
by simp |
|
49 |
||
50 |
lift_definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.foldr |
|
51 |
by simp |
|
52 |
||
53 |
lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat" |
|
54 |
proof - |
|
55 |
{ |
|
56 |
fix x y |
|
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47308
diff
changeset
|
57 |
have "list_all2 cr_dlist x y \<Longrightarrow> x = List.map list_of_dlist y" |
47308 | 58 |
unfolding list_all2_def cr_dlist_def by (induction x y rule: list_induct2') auto |
59 |
} |
|
60 |
note cr = this |
|
61 |
fix x :: "'a list list" and y :: "'a list list" |
|
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47308
diff
changeset
|
62 |
assume "(list_all2 cr_dlist OO Lifting.invariant distinct OO (list_all2 cr_dlist)\<inverse>\<inverse>) x y" |
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47308
diff
changeset
|
63 |
then have "x = y" by (auto dest: cr simp add: Lifting.invariant_def) |
47308 | 64 |
then show "?thesis x y" unfolding Lifting.invariant_def by auto |
65 |
qed |
|
66 |
||
67 |
text {* We can export code: *} |
|
68 |
||
69 |
export_code empty insert remove map filter null member length fold foldr concat in SML |
|
70 |
||
71 |
end |