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