src/HOL/Library/Dlist.thy
author wenzelm
Mon Dec 28 01:28:28 2015 +0100 (2015-12-28)
changeset 61945 1135b8de26c3
parent 61115 3a4400985780
child 62139 519362f817c7
permissions -rw-r--r--
more symbols;
haftmann@35303
     1
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@35303
     2
wenzelm@60500
     3
section \<open>Lists with elements distinct as canonical example for datatype invariants\<close>
haftmann@35303
     4
haftmann@35303
     5
theory Dlist
haftmann@45990
     6
imports Main
haftmann@35303
     7
begin
haftmann@35303
     8
wenzelm@60500
     9
subsection \<open>The type of distinct lists\<close>
haftmann@35303
    10
wenzelm@49834
    11
typedef 'a dlist = "{xs::'a list. distinct xs}"
haftmann@35303
    12
  morphisms list_of_dlist Abs_dlist
haftmann@35303
    13
proof
wenzelm@45694
    14
  show "[] \<in> {xs. distinct xs}" by simp
haftmann@35303
    15
qed
haftmann@35303
    16
haftmann@39380
    17
lemma dlist_eq_iff:
haftmann@39380
    18
  "dxs = dys \<longleftrightarrow> list_of_dlist dxs = list_of_dlist dys"
haftmann@39380
    19
  by (simp add: list_of_dlist_inject)
haftmann@36274
    20
haftmann@39380
    21
lemma dlist_eqI:
haftmann@39380
    22
  "list_of_dlist dxs = list_of_dlist dys \<Longrightarrow> dxs = dys"
haftmann@39380
    23
  by (simp add: dlist_eq_iff)
haftmann@36112
    24
wenzelm@60500
    25
text \<open>Formal, totalized constructor for @{typ "'a dlist"}:\<close>
haftmann@35303
    26
haftmann@35303
    27
definition Dlist :: "'a list \<Rightarrow> 'a dlist" where
haftmann@37765
    28
  "Dlist xs = Abs_dlist (remdups xs)"
haftmann@35303
    29
haftmann@39380
    30
lemma distinct_list_of_dlist [simp, intro]:
haftmann@35303
    31
  "distinct (list_of_dlist dxs)"
haftmann@35303
    32
  using list_of_dlist [of dxs] by simp
haftmann@35303
    33
haftmann@35303
    34
lemma list_of_dlist_Dlist [simp]:
haftmann@35303
    35
  "list_of_dlist (Dlist xs) = remdups xs"
haftmann@35303
    36
  by (simp add: Dlist_def Abs_dlist_inverse)
haftmann@35303
    37
haftmann@39727
    38
lemma remdups_list_of_dlist [simp]:
haftmann@39727
    39
  "remdups (list_of_dlist dxs) = list_of_dlist dxs"
haftmann@39727
    40
  by simp
haftmann@39727
    41
haftmann@36112
    42
lemma Dlist_list_of_dlist [simp, code abstype]:
haftmann@35303
    43
  "Dlist (list_of_dlist dxs) = dxs"
haftmann@35303
    44
  by (simp add: Dlist_def list_of_dlist_inverse distinct_remdups_id)
haftmann@35303
    45
haftmann@35303
    46
wenzelm@60500
    47
text \<open>Fundamental operations:\<close>
haftmann@35303
    48
wenzelm@61115
    49
context
wenzelm@61115
    50
begin
wenzelm@61115
    51
wenzelm@61115
    52
qualified definition empty :: "'a dlist" where
haftmann@35303
    53
  "empty = Dlist []"
haftmann@35303
    54
wenzelm@61115
    55
qualified definition insert :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
haftmann@35303
    56
  "insert x dxs = Dlist (List.insert x (list_of_dlist dxs))"
haftmann@35303
    57
wenzelm@61115
    58
qualified definition remove :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
haftmann@35303
    59
  "remove x dxs = Dlist (remove1 x (list_of_dlist dxs))"
haftmann@35303
    60
wenzelm@61115
    61
qualified definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist" where
haftmann@35303
    62
  "map f dxs = Dlist (remdups (List.map f (list_of_dlist dxs)))"
haftmann@35303
    63
wenzelm@61115
    64
qualified definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
haftmann@35303
    65
  "filter P dxs = Dlist (List.filter P (list_of_dlist dxs))"
haftmann@35303
    66
wenzelm@61115
    67
end
wenzelm@61115
    68
haftmann@35303
    69
wenzelm@60500
    70
text \<open>Derived operations:\<close>
haftmann@35303
    71
wenzelm@61115
    72
context
wenzelm@61115
    73
begin
wenzelm@61115
    74
wenzelm@61115
    75
qualified definition null :: "'a dlist \<Rightarrow> bool" where
haftmann@35303
    76
  "null dxs = List.null (list_of_dlist dxs)"
haftmann@35303
    77
wenzelm@61115
    78
qualified definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" where
haftmann@35303
    79
  "member dxs = List.member (list_of_dlist dxs)"
haftmann@35303
    80
wenzelm@61115
    81
qualified definition length :: "'a dlist \<Rightarrow> nat" where
haftmann@35303
    82
  "length dxs = List.length (list_of_dlist dxs)"
haftmann@35303
    83
wenzelm@61115
    84
qualified definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
haftmann@46133
    85
  "fold f dxs = List.fold f (list_of_dlist dxs)"
haftmann@37022
    86
wenzelm@61115
    87
qualified definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
haftmann@37022
    88
  "foldr f dxs = List.foldr f (list_of_dlist dxs)"
haftmann@35303
    89
wenzelm@61115
    90
end
wenzelm@61115
    91
haftmann@35303
    92
wenzelm@60500
    93
subsection \<open>Executable version obeying invariant\<close>
haftmann@35303
    94
haftmann@35303
    95
lemma list_of_dlist_empty [simp, code abstract]:
wenzelm@61115
    96
  "list_of_dlist Dlist.empty = []"
wenzelm@61115
    97
  by (simp add: Dlist.empty_def)
haftmann@35303
    98
haftmann@35303
    99
lemma list_of_dlist_insert [simp, code abstract]:
wenzelm@61115
   100
  "list_of_dlist (Dlist.insert x dxs) = List.insert x (list_of_dlist dxs)"
wenzelm@61115
   101
  by (simp add: Dlist.insert_def)
haftmann@35303
   102
haftmann@35303
   103
lemma list_of_dlist_remove [simp, code abstract]:
wenzelm@61115
   104
  "list_of_dlist (Dlist.remove x dxs) = remove1 x (list_of_dlist dxs)"
wenzelm@61115
   105
  by (simp add: Dlist.remove_def)
haftmann@35303
   106
haftmann@35303
   107
lemma list_of_dlist_map [simp, code abstract]:
wenzelm@61115
   108
  "list_of_dlist (Dlist.map f dxs) = remdups (List.map f (list_of_dlist dxs))"
wenzelm@61115
   109
  by (simp add: Dlist.map_def)
haftmann@35303
   110
haftmann@35303
   111
lemma list_of_dlist_filter [simp, code abstract]:
wenzelm@61115
   112
  "list_of_dlist (Dlist.filter P dxs) = List.filter P (list_of_dlist dxs)"
wenzelm@61115
   113
  by (simp add: Dlist.filter_def)
haftmann@35303
   114
haftmann@35303
   115
wenzelm@60500
   116
text \<open>Explicit executable conversion\<close>
haftmann@36980
   117
haftmann@36980
   118
definition dlist_of_list [simp]:
haftmann@36980
   119
  "dlist_of_list = Dlist"
haftmann@36980
   120
haftmann@36980
   121
lemma [code abstract]:
haftmann@36980
   122
  "list_of_dlist (dlist_of_list xs) = remdups xs"
haftmann@36980
   123
  by simp
haftmann@36980
   124
haftmann@36980
   125
wenzelm@60500
   126
text \<open>Equality\<close>
haftmann@38512
   127
haftmann@38857
   128
instantiation dlist :: (equal) equal
haftmann@38512
   129
begin
haftmann@38512
   130
haftmann@38857
   131
definition "HOL.equal dxs dys \<longleftrightarrow> HOL.equal (list_of_dlist dxs) (list_of_dlist dys)"
haftmann@38512
   132
wenzelm@60679
   133
instance
wenzelm@60679
   134
  by standard (simp add: equal_dlist_def equal list_of_dlist_inject)
haftmann@38512
   135
haftmann@38512
   136
end
haftmann@38512
   137
haftmann@43764
   138
declare equal_dlist_def [code]
haftmann@43764
   139
wenzelm@60679
   140
lemma [code nbe]: "HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
haftmann@38857
   141
  by (fact equal_refl)
haftmann@38857
   142
haftmann@38512
   143
wenzelm@60500
   144
subsection \<open>Induction principle and case distinction\<close>
haftmann@37106
   145
haftmann@37106
   146
lemma dlist_induct [case_names empty insert, induct type: dlist]:
wenzelm@61115
   147
  assumes empty: "P Dlist.empty"
wenzelm@61115
   148
  assumes insrt: "\<And>x dxs. \<not> Dlist.member dxs x \<Longrightarrow> P dxs \<Longrightarrow> P (Dlist.insert x dxs)"
haftmann@37106
   149
  shows "P dxs"
haftmann@37106
   150
proof (cases dxs)
haftmann@37106
   151
  case (Abs_dlist xs)
wenzelm@61115
   152
  then have "distinct xs" and dxs: "dxs = Dlist xs"
wenzelm@61115
   153
    by (simp_all add: Dlist_def distinct_remdups_id)
wenzelm@60500
   154
  from \<open>distinct xs\<close> have "P (Dlist xs)"
haftmann@39915
   155
  proof (induct xs)
wenzelm@61115
   156
    case Nil from empty show ?case by (simp add: Dlist.empty_def)
haftmann@37106
   157
  next
haftmann@40122
   158
    case (Cons x xs)
wenzelm@61115
   159
    then have "\<not> Dlist.member (Dlist xs) x" and "P (Dlist xs)"
wenzelm@61115
   160
      by (simp_all add: Dlist.member_def List.member_def)
wenzelm@61115
   161
    with insrt have "P (Dlist.insert x (Dlist xs))" .
wenzelm@61115
   162
    with Cons show ?case by (simp add: Dlist.insert_def distinct_remdups_id)
haftmann@37106
   163
  qed
haftmann@37106
   164
  with dxs show "P dxs" by simp
haftmann@37106
   165
qed
haftmann@37106
   166
wenzelm@55913
   167
lemma dlist_case [cases type: dlist]:
wenzelm@61115
   168
  obtains (empty) "dxs = Dlist.empty"
wenzelm@61115
   169
    | (insert) x dys where "\<not> Dlist.member dys x" and "dxs = Dlist.insert x dys"
haftmann@37106
   170
proof (cases dxs)
haftmann@37106
   171
  case (Abs_dlist xs)
haftmann@37106
   172
  then have dxs: "dxs = Dlist xs" and distinct: "distinct xs"
haftmann@37106
   173
    by (simp_all add: Dlist_def distinct_remdups_id)
wenzelm@55913
   174
  show thesis
wenzelm@55913
   175
  proof (cases xs)
wenzelm@55913
   176
    case Nil with dxs
wenzelm@61115
   177
    have "dxs = Dlist.empty" by (simp add: Dlist.empty_def) 
wenzelm@55913
   178
    with empty show ?thesis .
haftmann@37106
   179
  next
haftmann@37106
   180
    case (Cons x xs)
wenzelm@61115
   181
    with dxs distinct have "\<not> Dlist.member (Dlist xs) x"
wenzelm@61115
   182
      and "dxs = Dlist.insert x (Dlist xs)"
wenzelm@61115
   183
      by (simp_all add: Dlist.member_def List.member_def Dlist.insert_def distinct_remdups_id)
wenzelm@55913
   184
    with insert show ?thesis .
haftmann@37106
   185
  qed
haftmann@37106
   186
qed
haftmann@37106
   187
haftmann@37106
   188
wenzelm@60500
   189
subsection \<open>Functorial structure\<close>
haftmann@40603
   190
blanchet@55467
   191
functor map: map
wenzelm@61115
   192
  by (simp_all add: remdups_map_remdups fun_eq_iff dlist_eq_iff)
haftmann@40603
   193
haftmann@48282
   194
wenzelm@60500
   195
subsection \<open>Quickcheck generators\<close>
bulwahn@45927
   196
wenzelm@61115
   197
quickcheck_generator dlist predicate: distinct constructors: Dlist.empty, Dlist.insert
haftmann@35303
   198
haftmann@35303
   199
end