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