Quotient example: Lists with distinct elements
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue Jul 12 16:00:05 2011 +0900 (2011-07-12)
changeset 437669545bb3cefac
parent 43765 24b8244d672b
child 43767 e0219ef7f84c
child 43785 2bd54d4b5f3d
Quotient example: Lists with distinct elements
src/HOL/Quotient_Examples/DList.thy
src/HOL/Quotient_Examples/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Quotient_Examples/DList.thy	Tue Jul 12 16:00:05 2011 +0900
     1.3 @@ -0,0 +1,293 @@
     1.4 +(*  Title:      HOL/Quotient_Examples/DList.thy
     1.5 +    Author:     Cezary Kaliszyk, University of Tsukuba
     1.6 +
     1.7 +Based on typedef version "Library/Dlist" by Florian Haftmann
     1.8 +and theory morphism version by Maksym Bortin
     1.9 +*)
    1.10 +
    1.11 +header {* Lists with distinct elements *}
    1.12 +
    1.13 +theory DList
    1.14 +imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List"
    1.15 +begin
    1.16 +
    1.17 +text {* Some facts about lists *}
    1.18 +
    1.19 +lemma remdups_removeAll_commute[simp]:
    1.20 +  "remdups (removeAll x l) = removeAll x (remdups l)"
    1.21 +  by (induct l) auto
    1.22 +
    1.23 +lemma removeAll_distinct[simp]:
    1.24 +  assumes "distinct l"
    1.25 +  shows "distinct (removeAll x l)"
    1.26 +  using assms by (induct l) simp_all
    1.27 +
    1.28 +lemma removeAll_commute:
    1.29 +  "removeAll x (removeAll y l) = removeAll y (removeAll x l)"
    1.30 +  by (induct l) auto
    1.31 +
    1.32 +lemma remdups_hd_notin_tl:
    1.33 +  "remdups dl = h # t \<Longrightarrow> h \<notin> set t"
    1.34 +  by (induct dl arbitrary: h t)
    1.35 +     (case_tac [!] "a \<in> set dl", auto)
    1.36 +
    1.37 +lemma remdups_repeat:
    1.38 +  "remdups dl = h # t \<Longrightarrow> t = remdups t"
    1.39 +  by (induct dl arbitrary: h t, case_tac [!] "a \<in> set dl")
    1.40 +     (simp_all, metis remdups_remdups)
    1.41 +
    1.42 +lemma remdups_nil_noteq_cons:
    1.43 +  "remdups (h # t) \<noteq> remdups []"
    1.44 +  "remdups [] \<noteq> remdups (h # t)"
    1.45 +  by auto
    1.46 +
    1.47 +lemma remdups_eq_map_eq:
    1.48 +  assumes "remdups xa = remdups ya"
    1.49 +    shows "remdups (map f xa) = remdups (map f ya)"
    1.50 +  using assms
    1.51 +  by (induct xa ya arbitrary: fx fy rule: list_induct2')
    1.52 +     (metis (full_types) remdups_nil_noteq_cons(2) remdups_map_remdups)+
    1.53 +
    1.54 +text {* Setting up the quotient type *}
    1.55 +
    1.56 +definition
    1.57 +  dlist_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.58 +where
    1.59 +  [simp]: "dlist_eq xs ys \<longleftrightarrow> remdups xs = remdups ys"
    1.60 +
    1.61 +lemma dlist_eq_reflp:
    1.62 +  "reflp dlist_eq"
    1.63 +  by (auto intro: reflpI)
    1.64 +
    1.65 +lemma dlist_eq_symp:
    1.66 +  "symp dlist_eq"
    1.67 +  by (auto intro: sympI)
    1.68 +
    1.69 +lemma dlist_eq_transp:
    1.70 +  "transp dlist_eq"
    1.71 +  by (auto intro: transpI)
    1.72 +
    1.73 +lemma dlist_eq_equivp:
    1.74 +  "equivp dlist_eq"
    1.75 +  by (auto intro: equivpI dlist_eq_reflp dlist_eq_symp dlist_eq_transp)
    1.76 +
    1.77 +quotient_type
    1.78 +  'a dlist = "'a list" / "dlist_eq"
    1.79 +  by (rule dlist_eq_equivp)
    1.80 +
    1.81 +text {* respectfulness and constant definitions *}
    1.82 +
    1.83 +definition [simp]: "card_remdups = length \<circ> remdups"
    1.84 +definition [simp]: "foldr_remdups f xs e = foldr f (remdups xs) e"
    1.85 +
    1.86 +lemma [quot_respect]:
    1.87 +  "(dlist_eq) Nil Nil"
    1.88 +  "(dlist_eq ===> op =) List.member List.member"
    1.89 +  "(op = ===> dlist_eq ===> dlist_eq) Cons Cons"
    1.90 +  "(op = ===> dlist_eq ===> dlist_eq) removeAll removeAll"
    1.91 +  "(dlist_eq ===> op =) card_remdups card_remdups"
    1.92 +  "(dlist_eq ===> op =) remdups remdups"
    1.93 +  "(op = ===> dlist_eq ===> op =) foldr_remdups foldr_remdups"
    1.94 +  "(op = ===> dlist_eq ===> dlist_eq) map map"
    1.95 +  "(op = ===> dlist_eq ===> dlist_eq) filter filter"
    1.96 +  by (auto intro!: fun_relI simp add: remdups_filter)
    1.97 +     (metis (full_types) member_set set_remdups remdups_eq_map_eq)+
    1.98 +
    1.99 +quotient_definition empty where "empty :: 'a dlist"
   1.100 +  is "Nil"
   1.101 +
   1.102 +quotient_definition insert where "insert :: 'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
   1.103 +  is "Cons"
   1.104 +
   1.105 +quotient_definition "member :: 'a dlist \<Rightarrow> 'a \<Rightarrow> bool"
   1.106 +  is "List.member"
   1.107 +
   1.108 +quotient_definition foldr where "foldr :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b"
   1.109 +  is "foldr_remdups"
   1.110 +
   1.111 +quotient_definition "remove :: 'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
   1.112 +  is "removeAll"
   1.113 +
   1.114 +quotient_definition card where "card :: 'a dlist \<Rightarrow> nat"
   1.115 +  is "card_remdups"
   1.116 +
   1.117 +quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist"
   1.118 +  is "List.map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
   1.119 +
   1.120 +quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
   1.121 +  is "List.filter"
   1.122 +
   1.123 +quotient_definition "list_of_dlist :: 'a dlist \<Rightarrow> 'a list"
   1.124 +  is "remdups"
   1.125 +
   1.126 +text {* lifted theorems *}
   1.127 +
   1.128 +lemma dlist_member_insert:
   1.129 +  "member dl x \<Longrightarrow> insert x dl = dl"
   1.130 +  by descending (simp add: List.member_def)
   1.131 +
   1.132 +lemma dlist_member_insert_eq:
   1.133 +  "member (insert y dl) x = (x = y \<or> member dl x)"
   1.134 +  by descending (simp add: List.member_def)
   1.135 +
   1.136 +lemma dlist_insert_idem:
   1.137 +  "insert x (insert x dl) = insert x dl"
   1.138 +  by descending simp
   1.139 +
   1.140 +lemma dlist_insert_not_empty:
   1.141 +  "insert x dl \<noteq> empty"
   1.142 +  by descending auto
   1.143 +
   1.144 +lemma not_dlist_member_empty:
   1.145 +  "\<not> member empty x"
   1.146 +  by descending (simp add: List.member_def)
   1.147 +
   1.148 +lemma not_dlist_member_remove:
   1.149 +  "\<not> member (remove x dl) x"
   1.150 +  by descending (simp add: List.member_def)
   1.151 +
   1.152 +lemma dlist_in_remove:
   1.153 +  "a \<noteq> b \<Longrightarrow> member (remove b dl) a = member dl a"
   1.154 +  by descending (simp add: List.member_def)
   1.155 +
   1.156 +lemma dlist_not_memb_remove:
   1.157 +  "\<not> member dl x \<Longrightarrow> remove x dl = dl"
   1.158 +  by descending (simp add: List.member_def)
   1.159 +
   1.160 +lemma dlist_no_memb_remove_insert:
   1.161 +"\<not> member dl x \<Longrightarrow> remove x (insert x dl) = dl"
   1.162 +  by descending (simp add: List.member_def)
   1.163 +
   1.164 +lemma dlist_remove_empty:
   1.165 +  "remove x empty = empty"
   1.166 +  by descending simp
   1.167 +
   1.168 +lemma dlist_remove_insert_commute:
   1.169 +  "a \<noteq> b \<Longrightarrow> remove a (insert b dl) = insert b (remove a dl)"
   1.170 +  by descending simp
   1.171 +
   1.172 +lemma dlist_remove_commute:
   1.173 +"remove a (remove b dl) = remove b (remove a dl)"
   1.174 +  by (lifting removeAll_commute)
   1.175 +
   1.176 +lemma dlist_foldr_empty:
   1.177 +  "foldr f empty e = e"
   1.178 +  by descending simp
   1.179 +
   1.180 +lemma dlist_no_memb_foldr:
   1.181 +  assumes "\<not> member dl x"
   1.182 +  shows "foldr f (insert x dl) e = f x (foldr f dl e)"
   1.183 +  using assms by descending (simp add: List.member_def)
   1.184 +
   1.185 +lemma dlist_foldr_insert_not_memb:
   1.186 +  assumes "\<not>member t h"
   1.187 +  shows "foldr f (insert h t) e = f h (foldr f t e)"
   1.188 +  using assms by descending (simp add: List.member_def)
   1.189 +
   1.190 +lemma list_of_dlist_empty[simp]:
   1.191 +  "list_of_dlist empty = []"
   1.192 +  by descending simp
   1.193 +
   1.194 +lemma list_of_dlist_insert[simp]:
   1.195 +  "list_of_dlist (insert x xs) =
   1.196 +    (if member xs x then (remdups (list_of_dlist xs))
   1.197 +    else x # (remdups (list_of_dlist xs)))"
   1.198 +  by descending (simp add: List.member_def remdups_remdups)
   1.199 +
   1.200 +lemma list_of_dlist_remove[simp]:
   1.201 +  "list_of_dlist (remove x dxs) = remove1 x (list_of_dlist dxs)"
   1.202 +  by descending (simp add: distinct_remove1_removeAll)
   1.203 +
   1.204 +lemma list_of_dlist_map[simp]:
   1.205 +  "list_of_dlist (map f dxs) = remdups (List.map f (list_of_dlist dxs))"
   1.206 +  by descending (simp add: remdups_map_remdups)
   1.207 +
   1.208 +lemma list_of_dlist_filter [simp]:
   1.209 +  "list_of_dlist (filter P dxs) = List.filter P (list_of_dlist dxs)"
   1.210 +  by descending (simp add: remdups_filter)
   1.211 +
   1.212 +lemma dlist_map_empty:
   1.213 +  "map f empty = empty"
   1.214 +  by descending simp
   1.215 +
   1.216 +lemma dlist_map_insert:
   1.217 +  "map f (insert x xs) = insert (f x) (map f xs)"
   1.218 +  by descending simp
   1.219 +
   1.220 +lemma dlist_eq_iff:
   1.221 +  "dxs = dys \<longleftrightarrow> list_of_dlist dxs = list_of_dlist dys"
   1.222 +  by descending simp
   1.223 +
   1.224 +lemma dlist_eqI:
   1.225 +  "list_of_dlist dxs = list_of_dlist dys \<Longrightarrow> dxs = dys"
   1.226 +  by (simp add: dlist_eq_iff)
   1.227 +
   1.228 +abbreviation
   1.229 +  "dlist xs \<equiv> abs_dlist xs"
   1.230 +
   1.231 +lemma distinct_list_of_dlist [simp, intro]:
   1.232 +  "distinct (list_of_dlist dxs)"
   1.233 +  by descending simp
   1.234 +
   1.235 +lemma list_of_dlist_dlist [simp]:
   1.236 +  "list_of_dlist (dlist xs) = remdups xs"
   1.237 +  unfolding list_of_dlist_def map_fun_apply id_def
   1.238 +  by (metis Quotient_rep_abs[OF Quotient_dlist] dlist_eq_def)
   1.239 +
   1.240 +lemma remdups_list_of_dlist [simp]:
   1.241 +  "remdups (list_of_dlist dxs) = list_of_dlist dxs"
   1.242 +  by simp
   1.243 +
   1.244 +lemma dlist_list_of_dlist [simp, code abstype]:
   1.245 +  "dlist (list_of_dlist dxs) = dxs"
   1.246 +  by (simp add: list_of_dlist_def)
   1.247 +  (metis Quotient_def Quotient_dlist dlist_eqI list_of_dlist_dlist remdups_list_of_dlist)
   1.248 +
   1.249 +lemma dlist_filter_simps:
   1.250 +  "filter P empty = empty"
   1.251 +  "filter P (insert x xs) = (if P x then insert x (filter P xs) else filter P xs)"
   1.252 +  by (lifting filter.simps)
   1.253 +
   1.254 +lemma dlist_induct:
   1.255 +  assumes "P empty"
   1.256 +      and "\<And>a dl. P dl \<Longrightarrow> P (insert a dl)"
   1.257 +    shows "P dl"
   1.258 +  using assms by descending (drule list.induct, simp)
   1.259 +
   1.260 +lemma dlist_induct_stronger:
   1.261 +  assumes a1: "P empty"
   1.262 +  and     a2: "\<And>x dl. \<lbrakk>\<not>member dl x; P dl\<rbrakk> \<Longrightarrow> P (insert x dl)"
   1.263 +  shows "P dl"
   1.264 +proof(induct dl rule: dlist_induct)
   1.265 +  show "P empty" using a1 by simp
   1.266 +next
   1.267 +  fix x dl
   1.268 +  assume "P dl"
   1.269 +  then show "P (insert x dl)" using a2
   1.270 +    by (cases "member dl x") (simp_all add: dlist_member_insert)
   1.271 +qed
   1.272 +
   1.273 +lemma dlist_card_induct:
   1.274 +  assumes "\<And>xs. (\<And>ys. card ys < card xs \<Longrightarrow> P ys) \<Longrightarrow> P xs"
   1.275 +    shows "P xs"
   1.276 +  using assms
   1.277 +  by descending (rule measure_induct [of card_remdups], blast)
   1.278 +
   1.279 +lemma dlist_cases:
   1.280 +  "dl = empty \<or> (\<exists>h t. dl = insert h t \<and> \<not> member t h)"
   1.281 +  apply (descending, simp add: List.member_def)
   1.282 +  by (metis list.exhaust remdups_eq_nil_iff remdups_hd_notin_tl remdups_repeat)
   1.283 +
   1.284 +lemma dlist_exhaust:
   1.285 +  assumes "y = empty \<Longrightarrow> P"
   1.286 +      and "\<And>a dl. y = insert a dl \<Longrightarrow> P"
   1.287 +    shows "P"
   1.288 +  using assms by (lifting list.exhaust)
   1.289 +
   1.290 +lemma dlist_exhaust_stronger:
   1.291 +  assumes "y = empty \<Longrightarrow> P"
   1.292 +      and "\<And>a dl. y = insert a dl \<Longrightarrow> \<not> member dl a \<Longrightarrow> P"
   1.293 +    shows "P"
   1.294 +  using assms by (metis dlist_cases)
   1.295 +
   1.296 +end
     2.1 --- a/src/HOL/Quotient_Examples/ROOT.ML	Mon Jul 11 23:20:40 2011 +0200
     2.2 +++ b/src/HOL/Quotient_Examples/ROOT.ML	Tue Jul 12 16:00:05 2011 +0900
     2.3 @@ -4,5 +4,5 @@
     2.4  Testing the quotient package.
     2.5  *)
     2.6  
     2.7 -use_thys ["FSet", "Quotient_Int", "Quotient_Message"];
     2.8 +use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message"];
     2.9