src/HOL/Quotient_Examples/DList.thy
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (23 months ago)
changeset 66816 212a3334e7da
parent 66453 cc19f7ca2ed6
permissions -rw-r--r--
more fundamental definition of div and mod on int
     1 (*  Title:      HOL/Quotient_Examples/DList.thy
     2     Author:     Cezary Kaliszyk, University of Tsukuba
     3 
     4 Based on typedef version "Library/Dlist" by Florian Haftmann
     5 and theory morphism version by Maksym Bortin
     6 *)
     7 
     8 section \<open>Lists with distinct elements\<close>
     9 
    10 theory DList
    11 imports "HOL-Library.Quotient_List"
    12 begin
    13 
    14 text \<open>Some facts about lists\<close>
    15 
    16 lemma remdups_removeAll_commute[simp]:
    17   "remdups (removeAll x l) = removeAll x (remdups l)"
    18   by (induct l) auto
    19 
    20 lemma removeAll_distinct[simp]:
    21   assumes "distinct l"
    22   shows "distinct (removeAll x l)"
    23   using assms by (induct l) simp_all
    24 
    25 lemma removeAll_commute:
    26   "removeAll x (removeAll y l) = removeAll y (removeAll x l)"
    27   by (induct l) auto
    28 
    29 lemma remdups_hd_notin_tl:
    30   "remdups dl = h # t \<Longrightarrow> h \<notin> set t"
    31 proof (induct dl arbitrary: h t)
    32   case Nil
    33   then show ?case by simp
    34 next
    35   case (Cons a dl)
    36   then show ?case by (cases "a \<in> set dl") auto
    37 qed
    38 
    39 lemma remdups_repeat:
    40   "remdups dl = h # t \<Longrightarrow> t = remdups t"
    41 proof (induct dl arbitrary: h t)
    42   case Nil
    43   then show ?case by simp
    44 next
    45   case (Cons a dl)
    46   then show ?case by (cases "a \<in> set dl") (auto simp: remdups_remdups)
    47 qed
    48 
    49 lemma remdups_nil_noteq_cons:
    50   "remdups (h # t) \<noteq> remdups []"
    51   "remdups [] \<noteq> remdups (h # t)"
    52   by auto
    53 
    54 lemma remdups_eq_map_eq:
    55   assumes "remdups xa = remdups ya"
    56     shows "remdups (map f xa) = remdups (map f ya)"
    57   using assms
    58   by (induct xa ya rule: list_induct2')
    59      (metis (full_types) remdups_nil_noteq_cons(2) remdups_map_remdups)+
    60 
    61 lemma remdups_eq_member_eq:
    62   assumes "remdups xa = remdups ya"
    63     shows "List.member xa = List.member ya"
    64   using assms
    65   unfolding fun_eq_iff List.member_def
    66   by (induct xa ya rule: list_induct2')
    67      (metis remdups_nil_noteq_cons set_remdups)+
    68 
    69 text \<open>Setting up the quotient type\<close>
    70 
    71 definition
    72   dlist_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    73 where
    74   [simp]: "dlist_eq xs ys \<longleftrightarrow> remdups xs = remdups ys"
    75 
    76 lemma dlist_eq_reflp:
    77   "reflp dlist_eq"
    78   by (auto intro: reflpI)
    79 
    80 lemma dlist_eq_symp:
    81   "symp dlist_eq"
    82   by (auto intro: sympI)
    83 
    84 lemma dlist_eq_transp:
    85   "transp dlist_eq"
    86   by (auto intro: transpI)
    87 
    88 lemma dlist_eq_equivp:
    89   "equivp dlist_eq"
    90   by (auto intro: equivpI dlist_eq_reflp dlist_eq_symp dlist_eq_transp)
    91 
    92 quotient_type
    93   'a dlist = "'a list" / "dlist_eq"
    94   by (rule dlist_eq_equivp)
    95 
    96 text \<open>respectfulness and constant definitions\<close>
    97 
    98 definition [simp]: "card_remdups = length \<circ> remdups"
    99 definition [simp]: "foldr_remdups f xs e = foldr f (remdups xs) e"
   100 
   101 quotient_definition empty where "empty :: 'a dlist"
   102   is "Nil" .
   103 
   104 quotient_definition insert where "insert :: 'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
   105   is "Cons" by (metis (mono_tags) List.insert_def dlist_eq_def remdups.simps(2) set_remdups)
   106 
   107 quotient_definition "member :: 'a dlist \<Rightarrow> 'a \<Rightarrow> bool"
   108   is "List.member" by (metis dlist_eq_def remdups_eq_member_eq)
   109 
   110 quotient_definition foldr where "foldr :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b"
   111   is "foldr_remdups" by auto
   112 
   113 quotient_definition "remove :: 'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
   114   is "removeAll" by force
   115 
   116 quotient_definition card where "card :: 'a dlist \<Rightarrow> nat"
   117   is "card_remdups" by fastforce
   118 
   119 quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist"
   120   is "List.map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" by (metis dlist_eq_def remdups_eq_map_eq)
   121 
   122 quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
   123   is "List.filter" by (metis dlist_eq_def remdups_filter)
   124 
   125 quotient_definition "list_of_dlist :: 'a dlist \<Rightarrow> 'a list"
   126   is "remdups" by simp
   127 
   128 text \<open>lifted theorems\<close>
   129 
   130 lemma dlist_member_insert:
   131   "member dl x \<Longrightarrow> insert x dl = dl"
   132   by descending (simp add: List.member_def)
   133 
   134 lemma dlist_member_insert_eq:
   135   "member (insert y dl) x = (x = y \<or> member dl x)"
   136   by descending (simp add: List.member_def)
   137 
   138 lemma dlist_insert_idem:
   139   "insert x (insert x dl) = insert x dl"
   140   by descending simp
   141 
   142 lemma dlist_insert_not_empty:
   143   "insert x dl \<noteq> empty"
   144   by descending auto
   145 
   146 lemma not_dlist_member_empty:
   147   "\<not> member empty x"
   148   by descending (simp add: List.member_def)
   149 
   150 lemma not_dlist_member_remove:
   151   "\<not> member (remove x dl) x"
   152   by descending (simp add: List.member_def)
   153 
   154 lemma dlist_in_remove:
   155   "a \<noteq> b \<Longrightarrow> member (remove b dl) a = member dl a"
   156   by descending (simp add: List.member_def)
   157 
   158 lemma dlist_not_memb_remove:
   159   "\<not> member dl x \<Longrightarrow> remove x dl = dl"
   160   by descending (simp add: List.member_def)
   161 
   162 lemma dlist_no_memb_remove_insert:
   163   "\<not> member dl x \<Longrightarrow> remove x (insert x dl) = dl"
   164   by descending (simp add: List.member_def)
   165 
   166 lemma dlist_remove_empty:
   167   "remove x empty = empty"
   168   by descending simp
   169 
   170 lemma dlist_remove_insert_commute:
   171   "a \<noteq> b \<Longrightarrow> remove a (insert b dl) = insert b (remove a dl)"
   172   by descending simp
   173 
   174 lemma dlist_remove_commute:
   175 "remove a (remove b dl) = remove b (remove a dl)"
   176   by (lifting removeAll_commute)
   177 
   178 lemma dlist_foldr_empty:
   179   "foldr f empty e = e"
   180   by descending simp
   181 
   182 lemma dlist_no_memb_foldr:
   183   assumes "\<not> member dl x"
   184   shows "foldr f (insert x dl) e = f x (foldr f dl e)"
   185   using assms by descending (simp add: List.member_def)
   186 
   187 lemma dlist_foldr_insert_not_memb:
   188   assumes "\<not>member t h"
   189   shows "foldr f (insert h t) e = f h (foldr f t e)"
   190   using assms by descending (simp add: List.member_def)
   191 
   192 lemma list_of_dlist_empty[simp]:
   193   "list_of_dlist empty = []"
   194   by descending simp
   195 
   196 lemma list_of_dlist_insert[simp]:
   197   "list_of_dlist (insert x xs) =
   198     (if member xs x then (remdups (list_of_dlist xs))
   199     else x # (remdups (list_of_dlist xs)))"
   200   by descending (simp add: List.member_def remdups_remdups)
   201 
   202 lemma list_of_dlist_remove[simp]:
   203   "list_of_dlist (remove x dxs) = remove1 x (list_of_dlist dxs)"
   204   by descending (simp add: distinct_remove1_removeAll)
   205 
   206 lemma list_of_dlist_map[simp]:
   207   "list_of_dlist (map f dxs) = remdups (List.map f (list_of_dlist dxs))"
   208   by descending (simp add: remdups_map_remdups)
   209 
   210 lemma list_of_dlist_filter [simp]:
   211   "list_of_dlist (filter P dxs) = List.filter P (list_of_dlist dxs)"
   212   by descending (simp add: remdups_filter)
   213 
   214 lemma dlist_map_empty:
   215   "map f empty = empty"
   216   by descending simp
   217 
   218 lemma dlist_map_insert:
   219   "map f (insert x xs) = insert (f x) (map f xs)"
   220   by descending simp
   221 
   222 lemma dlist_eq_iff:
   223   "dxs = dys \<longleftrightarrow> list_of_dlist dxs = list_of_dlist dys"
   224   by descending simp
   225 
   226 lemma dlist_eqI:
   227   "list_of_dlist dxs = list_of_dlist dys \<Longrightarrow> dxs = dys"
   228   by (simp add: dlist_eq_iff)
   229 
   230 abbreviation
   231   "dlist xs \<equiv> abs_dlist xs"
   232 
   233 lemma distinct_list_of_dlist [simp, intro]:
   234   "distinct (list_of_dlist dxs)"
   235   by descending simp
   236 
   237 lemma list_of_dlist_dlist [simp]:
   238   "list_of_dlist (dlist xs) = remdups xs"
   239   unfolding list_of_dlist_def map_fun_apply id_def
   240   by (metis Quotient3_rep_abs[OF Quotient3_dlist] dlist_eq_def)
   241 
   242 lemma remdups_list_of_dlist [simp]:
   243   "remdups (list_of_dlist dxs) = list_of_dlist dxs"
   244   by simp
   245 
   246 lemma dlist_list_of_dlist [simp, code abstype]:
   247   "dlist (list_of_dlist dxs) = dxs"
   248   by (simp add: list_of_dlist_def)
   249   (metis Quotient3_def Quotient3_dlist dlist_eqI list_of_dlist_dlist remdups_list_of_dlist)
   250 
   251 lemma dlist_filter_simps:
   252   "filter P empty = empty"
   253   "filter P (insert x xs) = (if P x then insert x (filter P xs) else filter P xs)"
   254   by (lifting filter.simps)
   255 
   256 lemma dlist_induct:
   257   assumes "P empty"
   258       and "\<And>a dl. P dl \<Longrightarrow> P (insert a dl)"
   259     shows "P dl"
   260   using assms by descending (drule list.induct, simp)
   261 
   262 lemma dlist_induct_stronger:
   263   assumes a1: "P empty"
   264   and     a2: "\<And>x dl. \<lbrakk>\<not>member dl x; P dl\<rbrakk> \<Longrightarrow> P (insert x dl)"
   265   shows "P dl"
   266 proof(induct dl rule: dlist_induct)
   267   show "P empty" using a1 by simp
   268 next
   269   fix x dl
   270   assume "P dl"
   271   then show "P (insert x dl)" using a2
   272     by (cases "member dl x") (simp_all add: dlist_member_insert)
   273 qed
   274 
   275 lemma dlist_card_induct:
   276   assumes "\<And>xs. (\<And>ys. card ys < card xs \<Longrightarrow> P ys) \<Longrightarrow> P xs"
   277     shows "P xs"
   278   using assms
   279   by descending (rule measure_induct [of card_remdups], blast)
   280 
   281 lemma dlist_cases:
   282   "dl = empty \<or> (\<exists>h t. dl = insert h t \<and> \<not> member t h)"
   283   by descending
   284     (metis List.member_def dlist_eq_def hd_Cons_tl list_of_dlist_dlist remdups_hd_notin_tl remdups_list_of_dlist)
   285 
   286 lemma dlist_exhaust:
   287   obtains "y = empty" | a dl where "y = insert a dl"
   288   by (lifting list.exhaust)
   289 
   290 lemma dlist_exhaust_stronger:
   291   obtains "y = empty" | a dl where "y = insert a dl" "\<not> member dl a"
   292   by (metis dlist_cases)
   293 
   294 end