author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47361  87c0eaf04bad 
child 49834  b27bbb021df1 
permissions  rwrr 
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 nonopen 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 nonopen 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 nonopen 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 