# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1310454005 -32400
# Node ID 9545bb3cefac21c6529eec51bbe98798db306359
# Parent  24b8244d672bf6e4809f120b14ac49ca87787d1c
Quotient example: Lists with distinct elements

diff -r 24b8244d672b -r 9545bb3cefac src/HOL/Quotient_Examples/DList.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/DList.thy	Tue Jul 12 16:00:05 2011 +0900
@@ -0,0 +1,293 @@
+(*  Title:      HOL/Quotient_Examples/DList.thy
+    Author:     Cezary Kaliszyk, University of Tsukuba
+
+Based on typedef version "Library/Dlist" by Florian Haftmann
+and theory morphism version by Maksym Bortin
+*)
+
+header {* Lists with distinct elements *}
+
+theory DList
+imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List"
+begin
+
+text {* Some facts about lists *}
+
+lemma remdups_removeAll_commute[simp]:
+  "remdups (removeAll x l) = removeAll x (remdups l)"
+  by (induct l) auto
+
+lemma removeAll_distinct[simp]:
+  assumes "distinct l"
+  shows "distinct (removeAll x l)"
+  using assms by (induct l) simp_all
+
+lemma removeAll_commute:
+  "removeAll x (removeAll y l) = removeAll y (removeAll x l)"
+  by (induct l) auto
+
+lemma remdups_hd_notin_tl:
+  "remdups dl = h # t \<Longrightarrow> h \<notin> set t"
+  by (induct dl arbitrary: h t)
+     (case_tac [!] "a \<in> set dl", auto)
+
+lemma remdups_repeat:
+  "remdups dl = h # t \<Longrightarrow> t = remdups t"
+  by (induct dl arbitrary: h t, case_tac [!] "a \<in> set dl")
+     (simp_all, metis remdups_remdups)
+
+lemma remdups_nil_noteq_cons:
+  "remdups (h # t) \<noteq> remdups []"
+  "remdups [] \<noteq> remdups (h # t)"
+  by auto
+
+lemma remdups_eq_map_eq:
+  assumes "remdups xa = remdups ya"
+    shows "remdups (map f xa) = remdups (map f ya)"
+  using assms
+  by (induct xa ya arbitrary: fx fy rule: list_induct2')
+     (metis (full_types) remdups_nil_noteq_cons(2) remdups_map_remdups)+
+
+text {* Setting up the quotient type *}
+
+definition
+  dlist_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+where
+  [simp]: "dlist_eq xs ys \<longleftrightarrow> remdups xs = remdups ys"
+
+lemma dlist_eq_reflp:
+  "reflp dlist_eq"
+  by (auto intro: reflpI)
+
+lemma dlist_eq_symp:
+  "symp dlist_eq"
+  by (auto intro: sympI)
+
+lemma dlist_eq_transp:
+  "transp dlist_eq"
+  by (auto intro: transpI)
+
+lemma dlist_eq_equivp:
+  "equivp dlist_eq"
+  by (auto intro: equivpI dlist_eq_reflp dlist_eq_symp dlist_eq_transp)
+
+quotient_type
+  'a dlist = "'a list" / "dlist_eq"
+  by (rule dlist_eq_equivp)
+
+text {* respectfulness and constant definitions *}
+
+definition [simp]: "card_remdups = length \<circ> remdups"
+definition [simp]: "foldr_remdups f xs e = foldr f (remdups xs) e"
+
+lemma [quot_respect]:
+  "(dlist_eq) Nil Nil"
+  "(dlist_eq ===> op =) List.member List.member"
+  "(op = ===> dlist_eq ===> dlist_eq) Cons Cons"
+  "(op = ===> dlist_eq ===> dlist_eq) removeAll removeAll"
+  "(dlist_eq ===> op =) card_remdups card_remdups"
+  "(dlist_eq ===> op =) remdups remdups"
+  "(op = ===> dlist_eq ===> op =) foldr_remdups foldr_remdups"
+  "(op = ===> dlist_eq ===> dlist_eq) map map"
+  "(op = ===> dlist_eq ===> dlist_eq) filter filter"
+  by (auto intro!: fun_relI simp add: remdups_filter)
+     (metis (full_types) member_set set_remdups remdups_eq_map_eq)+
+
+quotient_definition empty where "empty :: 'a dlist"
+  is "Nil"
+
+quotient_definition insert where "insert :: 'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
+  is "Cons"
+
+quotient_definition "member :: 'a dlist \<Rightarrow> 'a \<Rightarrow> bool"
+  is "List.member"
+
+quotient_definition foldr where "foldr :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b"
+  is "foldr_remdups"
+
+quotient_definition "remove :: 'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
+  is "removeAll"
+
+quotient_definition card where "card :: 'a dlist \<Rightarrow> nat"
+  is "card_remdups"
+
+quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist"
+  is "List.map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
+
+quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
+  is "List.filter"
+
+quotient_definition "list_of_dlist :: 'a dlist \<Rightarrow> 'a list"
+  is "remdups"
+
+text {* lifted theorems *}
+
+lemma dlist_member_insert:
+  "member dl x \<Longrightarrow> insert x dl = dl"
+  by descending (simp add: List.member_def)
+
+lemma dlist_member_insert_eq:
+  "member (insert y dl) x = (x = y \<or> member dl x)"
+  by descending (simp add: List.member_def)
+
+lemma dlist_insert_idem:
+  "insert x (insert x dl) = insert x dl"
+  by descending simp
+
+lemma dlist_insert_not_empty:
+  "insert x dl \<noteq> empty"
+  by descending auto
+
+lemma not_dlist_member_empty:
+  "\<not> member empty x"
+  by descending (simp add: List.member_def)
+
+lemma not_dlist_member_remove:
+  "\<not> member (remove x dl) x"
+  by descending (simp add: List.member_def)
+
+lemma dlist_in_remove:
+  "a \<noteq> b \<Longrightarrow> member (remove b dl) a = member dl a"
+  by descending (simp add: List.member_def)
+
+lemma dlist_not_memb_remove:
+  "\<not> member dl x \<Longrightarrow> remove x dl = dl"
+  by descending (simp add: List.member_def)
+
+lemma dlist_no_memb_remove_insert:
+"\<not> member dl x \<Longrightarrow> remove x (insert x dl) = dl"
+  by descending (simp add: List.member_def)
+
+lemma dlist_remove_empty:
+  "remove x empty = empty"
+  by descending simp
+
+lemma dlist_remove_insert_commute:
+  "a \<noteq> b \<Longrightarrow> remove a (insert b dl) = insert b (remove a dl)"
+  by descending simp
+
+lemma dlist_remove_commute:
+"remove a (remove b dl) = remove b (remove a dl)"
+  by (lifting removeAll_commute)
+
+lemma dlist_foldr_empty:
+  "foldr f empty e = e"
+  by descending simp
+
+lemma dlist_no_memb_foldr:
+  assumes "\<not> member dl x"
+  shows "foldr f (insert x dl) e = f x (foldr f dl e)"
+  using assms by descending (simp add: List.member_def)
+
+lemma dlist_foldr_insert_not_memb:
+  assumes "\<not>member t h"
+  shows "foldr f (insert h t) e = f h (foldr f t e)"
+  using assms by descending (simp add: List.member_def)
+
+lemma list_of_dlist_empty[simp]:
+  "list_of_dlist empty = []"
+  by descending simp
+
+lemma list_of_dlist_insert[simp]:
+  "list_of_dlist (insert x xs) =
+    (if member xs x then (remdups (list_of_dlist xs))
+    else x # (remdups (list_of_dlist xs)))"
+  by descending (simp add: List.member_def remdups_remdups)
+
+lemma list_of_dlist_remove[simp]:
+  "list_of_dlist (remove x dxs) = remove1 x (list_of_dlist dxs)"
+  by descending (simp add: distinct_remove1_removeAll)
+
+lemma list_of_dlist_map[simp]:
+  "list_of_dlist (map f dxs) = remdups (List.map f (list_of_dlist dxs))"
+  by descending (simp add: remdups_map_remdups)
+
+lemma list_of_dlist_filter [simp]:
+  "list_of_dlist (filter P dxs) = List.filter P (list_of_dlist dxs)"
+  by descending (simp add: remdups_filter)
+
+lemma dlist_map_empty:
+  "map f empty = empty"
+  by descending simp
+
+lemma dlist_map_insert:
+  "map f (insert x xs) = insert (f x) (map f xs)"
+  by descending simp
+
+lemma dlist_eq_iff:
+  "dxs = dys \<longleftrightarrow> list_of_dlist dxs = list_of_dlist dys"
+  by descending simp
+
+lemma dlist_eqI:
+  "list_of_dlist dxs = list_of_dlist dys \<Longrightarrow> dxs = dys"
+  by (simp add: dlist_eq_iff)
+
+abbreviation
+  "dlist xs \<equiv> abs_dlist xs"
+
+lemma distinct_list_of_dlist [simp, intro]:
+  "distinct (list_of_dlist dxs)"
+  by descending simp
+
+lemma list_of_dlist_dlist [simp]:
+  "list_of_dlist (dlist xs) = remdups xs"
+  unfolding list_of_dlist_def map_fun_apply id_def
+  by (metis Quotient_rep_abs[OF Quotient_dlist] dlist_eq_def)
+
+lemma remdups_list_of_dlist [simp]:
+  "remdups (list_of_dlist dxs) = list_of_dlist dxs"
+  by simp
+
+lemma dlist_list_of_dlist [simp, code abstype]:
+  "dlist (list_of_dlist dxs) = dxs"
+  by (simp add: list_of_dlist_def)
+  (metis Quotient_def Quotient_dlist dlist_eqI list_of_dlist_dlist remdups_list_of_dlist)
+
+lemma dlist_filter_simps:
+  "filter P empty = empty"
+  "filter P (insert x xs) = (if P x then insert x (filter P xs) else filter P xs)"
+  by (lifting filter.simps)
+
+lemma dlist_induct:
+  assumes "P empty"
+      and "\<And>a dl. P dl \<Longrightarrow> P (insert a dl)"
+    shows "P dl"
+  using assms by descending (drule list.induct, simp)
+
+lemma dlist_induct_stronger:
+  assumes a1: "P empty"
+  and     a2: "\<And>x dl. \<lbrakk>\<not>member dl x; P dl\<rbrakk> \<Longrightarrow> P (insert x dl)"
+  shows "P dl"
+proof(induct dl rule: dlist_induct)
+  show "P empty" using a1 by simp
+next
+  fix x dl
+  assume "P dl"
+  then show "P (insert x dl)" using a2
+    by (cases "member dl x") (simp_all add: dlist_member_insert)
+qed
+
+lemma dlist_card_induct:
+  assumes "\<And>xs. (\<And>ys. card ys < card xs \<Longrightarrow> P ys) \<Longrightarrow> P xs"
+    shows "P xs"
+  using assms
+  by descending (rule measure_induct [of card_remdups], blast)
+
+lemma dlist_cases:
+  "dl = empty \<or> (\<exists>h t. dl = insert h t \<and> \<not> member t h)"
+  apply (descending, simp add: List.member_def)
+  by (metis list.exhaust remdups_eq_nil_iff remdups_hd_notin_tl remdups_repeat)
+
+lemma dlist_exhaust:
+  assumes "y = empty \<Longrightarrow> P"
+      and "\<And>a dl. y = insert a dl \<Longrightarrow> P"
+    shows "P"
+  using assms by (lifting list.exhaust)
+
+lemma dlist_exhaust_stronger:
+  assumes "y = empty \<Longrightarrow> P"
+      and "\<And>a dl. y = insert a dl \<Longrightarrow> \<not> member dl a \<Longrightarrow> P"
+    shows "P"
+  using assms by (metis dlist_cases)
+
+end
diff -r 24b8244d672b -r 9545bb3cefac src/HOL/Quotient_Examples/ROOT.ML
--- a/src/HOL/Quotient_Examples/ROOT.ML	Mon Jul 11 23:20:40 2011 +0200
+++ b/src/HOL/Quotient_Examples/ROOT.ML	Tue Jul 12 16:00:05 2011 +0900
@@ -4,5 +4,5 @@
 Testing the quotient package.
 *)
 
-use_thys ["FSet", "Quotient_Int", "Quotient_Message"];
+use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message"];