src/HOL/Library/More_List.thy
author haftmann
Wed Apr 05 13:47:38 2017 +0200 (2017-04-05)
changeset 65388 a8d868477bc0
parent 63540 f8652d0534fa
child 67399 eab6ce8368fa
permissions -rw-r--r--
more on lists
haftmann@58199
     1
(* Author: Andreas Lochbihler, ETH Z├╝rich
haftmann@58199
     2
   Author: Florian Haftmann, TU Muenchen  *)
haftmann@58199
     3
wenzelm@58881
     4
section \<open>Less common functions on lists\<close>
haftmann@58199
     5
haftmann@58199
     6
theory More_List
haftmann@58199
     7
imports Main
haftmann@58199
     8
begin
haftmann@58199
     9
haftmann@58199
    10
definition strip_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
haftmann@58199
    11
where
haftmann@58199
    12
  "strip_while P = rev \<circ> dropWhile P \<circ> rev"
haftmann@58199
    13
haftmann@58295
    14
lemma strip_while_rev [simp]:
haftmann@58295
    15
  "strip_while P (rev xs) = rev (dropWhile P xs)"
haftmann@58295
    16
  by (simp add: strip_while_def)
haftmann@58295
    17
  
haftmann@58199
    18
lemma strip_while_Nil [simp]:
haftmann@58199
    19
  "strip_while P [] = []"
haftmann@58199
    20
  by (simp add: strip_while_def)
haftmann@58199
    21
haftmann@58199
    22
lemma strip_while_append [simp]:
haftmann@58199
    23
  "\<not> P x \<Longrightarrow> strip_while P (xs @ [x]) = xs @ [x]"
haftmann@58199
    24
  by (simp add: strip_while_def)
haftmann@58199
    25
haftmann@58199
    26
lemma strip_while_append_rec [simp]:
haftmann@58199
    27
  "P x \<Longrightarrow> strip_while P (xs @ [x]) = strip_while P xs"
haftmann@58199
    28
  by (simp add: strip_while_def)
haftmann@58199
    29
haftmann@58199
    30
lemma strip_while_Cons [simp]:
haftmann@58199
    31
  "\<not> P x \<Longrightarrow> strip_while P (x # xs) = x # strip_while P xs"
haftmann@58199
    32
  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
haftmann@58199
    33
haftmann@58199
    34
lemma strip_while_eq_Nil [simp]:
haftmann@58199
    35
  "strip_while P xs = [] \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
haftmann@58199
    36
  by (simp add: strip_while_def)
haftmann@58199
    37
haftmann@58199
    38
lemma strip_while_eq_Cons_rec:
haftmann@58199
    39
  "strip_while P (x # xs) = x # strip_while P xs \<longleftrightarrow> \<not> (P x \<and> (\<forall>x\<in>set xs. P x))"
haftmann@58199
    40
  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
haftmann@58199
    41
haftmann@58199
    42
lemma split_strip_while_append:
haftmann@58199
    43
  fixes xs :: "'a list"
haftmann@58199
    44
  obtains ys zs :: "'a list"
haftmann@58199
    45
  where "strip_while P xs = ys" and "\<forall>x\<in>set zs. P x" and "xs = ys @ zs"
haftmann@58199
    46
proof (rule that)
haftmann@58199
    47
  show "strip_while P xs = strip_while P xs" ..
haftmann@58199
    48
  show "\<forall>x\<in>set (rev (takeWhile P (rev xs))). P x" by (simp add: takeWhile_eq_all_conv [symmetric])
haftmann@58199
    49
  have "rev xs = rev (strip_while P xs @ rev (takeWhile P (rev xs)))"
haftmann@58199
    50
    by (simp add: strip_while_def)
haftmann@58199
    51
  then show "xs = strip_while P xs @ rev (takeWhile P (rev xs))"
haftmann@58199
    52
    by (simp only: rev_is_rev_conv)
haftmann@58199
    53
qed
haftmann@58199
    54
haftmann@58199
    55
lemma strip_while_snoc [simp]:
haftmann@58199
    56
  "strip_while P (xs @ [x]) = (if P x then strip_while P xs else xs @ [x])"
haftmann@58199
    57
  by (simp add: strip_while_def)
haftmann@58199
    58
haftmann@58199
    59
lemma strip_while_map:
haftmann@58199
    60
  "strip_while P (map f xs) = map f (strip_while (P \<circ> f) xs)"
haftmann@58199
    61
  by (simp add: strip_while_def rev_map dropWhile_map)
haftmann@58199
    62
haftmann@65388
    63
lemma strip_while_dropWhile_commute:
haftmann@65388
    64
  "strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)"
haftmann@65388
    65
proof (induct xs)
haftmann@65388
    66
  case Nil
haftmann@65388
    67
  then show ?case
haftmann@65388
    68
    by simp
haftmann@65388
    69
next
haftmann@65388
    70
  case (Cons x xs)
haftmann@65388
    71
  show ?case
haftmann@65388
    72
  proof (cases "\<forall>y\<in>set xs. P y")
haftmann@65388
    73
    case True
haftmann@65388
    74
    with dropWhile_append2 [of "rev xs"] show ?thesis
haftmann@65388
    75
      by (auto simp add: strip_while_def dest: set_dropWhileD)
haftmann@65388
    76
  next
haftmann@65388
    77
    case False
haftmann@65388
    78
    then obtain y where "y \<in> set xs" and "\<not> P y"
haftmann@65388
    79
      by blast
haftmann@65388
    80
    with Cons dropWhile_append3 [of P y "rev xs"] show ?thesis
haftmann@65388
    81
      by (simp add: strip_while_def)
haftmann@65388
    82
  qed
haftmann@65388
    83
qed
haftmann@65388
    84
haftmann@65388
    85
lemma dropWhile_strip_while_commute:
haftmann@65388
    86
  "dropWhile P (strip_while Q xs) = strip_while Q (dropWhile P xs)"
haftmann@65388
    87
  by (simp add: strip_while_dropWhile_commute)
haftmann@65388
    88
haftmann@58295
    89
haftmann@58295
    90
definition no_leading :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
haftmann@58295
    91
where
haftmann@58295
    92
  "no_leading P xs \<longleftrightarrow> (xs \<noteq> [] \<longrightarrow> \<not> P (hd xs))"
haftmann@58295
    93
haftmann@58295
    94
lemma no_leading_Nil [simp, intro!]:
haftmann@58295
    95
  "no_leading P []"
haftmann@58295
    96
  by (simp add: no_leading_def)
haftmann@58295
    97
haftmann@58295
    98
lemma no_leading_Cons [simp, intro!]:
haftmann@58295
    99
  "no_leading P (x # xs) \<longleftrightarrow> \<not> P x"
haftmann@58295
   100
  by (simp add: no_leading_def)
haftmann@58295
   101
haftmann@58295
   102
lemma no_leading_append [simp]:
haftmann@58295
   103
  "no_leading P (xs @ ys) \<longleftrightarrow> no_leading P xs \<and> (xs = [] \<longrightarrow> no_leading P ys)"
haftmann@58295
   104
  by (induct xs) simp_all
haftmann@58295
   105
haftmann@58295
   106
lemma no_leading_dropWhile [simp]:
haftmann@58295
   107
  "no_leading P (dropWhile P xs)"
haftmann@58295
   108
  by (induct xs) simp_all
haftmann@58295
   109
haftmann@58295
   110
lemma dropWhile_eq_obtain_leading:
haftmann@58295
   111
  assumes "dropWhile P xs = ys"
haftmann@58295
   112
  obtains zs where "xs = zs @ ys" and "\<And>z. z \<in> set zs \<Longrightarrow> P z" and "no_leading P ys"
haftmann@58295
   113
proof -
haftmann@58295
   114
  from assms have "\<exists>zs. xs = zs @ ys \<and> (\<forall>z \<in> set zs. P z) \<and> no_leading P ys"
haftmann@58295
   115
  proof (induct xs arbitrary: ys)
haftmann@58295
   116
    case Nil then show ?case by simp
haftmann@58295
   117
  next
haftmann@58295
   118
    case (Cons x xs ys)
haftmann@58295
   119
    show ?case proof (cases "P x")
haftmann@58295
   120
      case True with Cons.hyps [of ys] Cons.prems
haftmann@58295
   121
      have "\<exists>zs. xs = zs @ ys \<and> (\<forall>a\<in>set zs. P a) \<and> no_leading P ys"
haftmann@58295
   122
        by simp
haftmann@58295
   123
      then obtain zs where "xs = zs @ ys" and "\<And>z. z \<in> set zs \<Longrightarrow> P z"
haftmann@58295
   124
        and *: "no_leading P ys"
haftmann@58295
   125
        by blast
haftmann@58295
   126
      with True have "x # xs = (x # zs) @ ys" and "\<And>z. z \<in> set (x # zs) \<Longrightarrow> P z"
haftmann@58295
   127
        by auto
haftmann@58295
   128
      with * show ?thesis
haftmann@58295
   129
        by blast    next
haftmann@58295
   130
      case False
haftmann@58295
   131
      with Cons show ?thesis by (cases ys) simp_all
haftmann@58295
   132
    qed
haftmann@58295
   133
  qed
haftmann@58295
   134
  with that show thesis
haftmann@58295
   135
    by blast
haftmann@58295
   136
qed
haftmann@58295
   137
haftmann@58295
   138
lemma dropWhile_idem_iff:
haftmann@58295
   139
  "dropWhile P xs = xs \<longleftrightarrow> no_leading P xs"
haftmann@58295
   140
  by (cases xs) (auto elim: dropWhile_eq_obtain_leading)
haftmann@58295
   141
haftmann@58199
   142
haftmann@58295
   143
abbreviation no_trailing :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
haftmann@58295
   144
where
haftmann@58295
   145
  "no_trailing P xs \<equiv> no_leading P (rev xs)"
haftmann@58295
   146
haftmann@58295
   147
lemma no_trailing_unfold:
haftmann@58295
   148
  "no_trailing P xs \<longleftrightarrow> (xs \<noteq> [] \<longrightarrow> \<not> P (last xs))"
haftmann@58295
   149
  by (induct xs) simp_all
haftmann@58295
   150
haftmann@58295
   151
lemma no_trailing_Nil [simp, intro!]:
haftmann@58295
   152
  "no_trailing P []"
haftmann@58295
   153
  by simp
haftmann@58295
   154
haftmann@58295
   155
lemma no_trailing_Cons [simp]:
haftmann@58295
   156
  "no_trailing P (x # xs) \<longleftrightarrow> no_trailing P xs \<and> (xs = [] \<longrightarrow> \<not> P x)"
haftmann@58295
   157
  by simp
haftmann@58295
   158
haftmann@65388
   159
lemma no_trailing_append:
haftmann@65388
   160
  "no_trailing P (xs @ ys) \<longleftrightarrow> no_trailing P ys \<and> (ys = [] \<longrightarrow> no_trailing P xs)"
haftmann@65388
   161
  by (induct xs) simp_all
haftmann@65388
   162
haftmann@58295
   163
lemma no_trailing_append_Cons [simp]:
haftmann@58295
   164
  "no_trailing P (xs @ y # ys) \<longleftrightarrow> no_trailing P (y # ys)"
haftmann@58295
   165
  by simp
haftmann@58295
   166
haftmann@58295
   167
lemma no_trailing_strip_while [simp]:
haftmann@58295
   168
  "no_trailing P (strip_while P xs)"
haftmann@58295
   169
  by (induct xs rule: rev_induct) simp_all
haftmann@58295
   170
haftmann@65388
   171
lemma strip_while_idem [simp]:
haftmann@65388
   172
  "no_trailing P xs \<Longrightarrow> strip_while P xs = xs"
haftmann@65388
   173
  by (cases xs rule: rev_cases) simp_all
haftmann@65388
   174
haftmann@58295
   175
lemma strip_while_eq_obtain_trailing:
haftmann@58295
   176
  assumes "strip_while P xs = ys"
haftmann@58295
   177
  obtains zs where "xs = ys @ zs" and "\<And>z. z \<in> set zs \<Longrightarrow> P z" and "no_trailing P ys"
haftmann@58295
   178
proof -
haftmann@58295
   179
  from assms have "rev (rev (dropWhile P (rev xs))) = rev ys"
haftmann@58295
   180
    by (simp add: strip_while_def)
haftmann@58295
   181
  then have "dropWhile P (rev xs) = rev ys"
haftmann@58295
   182
    by simp
haftmann@58295
   183
  then obtain zs where A: "rev xs = zs @ rev ys" and B: "\<And>z. z \<in> set zs \<Longrightarrow> P z"
haftmann@58295
   184
    and C: "no_trailing P ys"
haftmann@58295
   185
    using dropWhile_eq_obtain_leading by blast
haftmann@58295
   186
  from A have "rev (rev xs) = rev (zs @ rev ys)"
haftmann@58295
   187
    by simp
haftmann@58295
   188
  then have "xs = ys @ rev zs"
haftmann@58295
   189
    by simp
haftmann@58295
   190
  moreover from B have "\<And>z. z \<in> set (rev zs) \<Longrightarrow> P z"
haftmann@58295
   191
    by simp
haftmann@58295
   192
  ultimately show thesis using that C by blast
haftmann@58295
   193
qed
haftmann@58295
   194
haftmann@58295
   195
lemma strip_while_idem_iff:
haftmann@58295
   196
  "strip_while P xs = xs \<longleftrightarrow> no_trailing P xs"
haftmann@58295
   197
proof -
wenzelm@63040
   198
  define ys where "ys = rev xs"
haftmann@58295
   199
  moreover have "strip_while P (rev ys) = rev ys \<longleftrightarrow> no_trailing P (rev ys)"
haftmann@58295
   200
    by (simp add: dropWhile_idem_iff)
haftmann@58295
   201
  ultimately show ?thesis by simp
haftmann@58295
   202
qed
haftmann@58295
   203
haftmann@58295
   204
lemma no_trailing_map:
haftmann@65388
   205
  "no_trailing P (map f xs) \<longleftrightarrow> no_trailing (P \<circ> f) xs"
haftmann@58295
   206
  by (simp add: last_map no_trailing_unfold)
haftmann@58295
   207
haftmann@65388
   208
lemma no_trailing_drop [simp]:
haftmann@65388
   209
  "no_trailing P (drop n xs)" if "no_trailing P xs"
haftmann@65388
   210
proof -
haftmann@65388
   211
  from that have "no_trailing P (take n xs @ drop n xs)"
haftmann@65388
   212
    by simp
haftmann@65388
   213
  then show ?thesis
haftmann@65388
   214
    by (simp only: no_trailing_append)
haftmann@65388
   215
qed
haftmann@65388
   216
haftmann@58295
   217
lemma no_trailing_upt [simp]:
haftmann@58295
   218
  "no_trailing P [n..<m] \<longleftrightarrow> (n < m \<longrightarrow> \<not> P (m - 1))"
haftmann@58295
   219
  by (auto simp add: no_trailing_unfold)
haftmann@58199
   220
haftmann@58199
   221
haftmann@58199
   222
definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a"
haftmann@58199
   223
where
haftmann@58437
   224
  "nth_default dflt xs n = (if n < length xs then xs ! n else dflt)"
haftmann@58199
   225
haftmann@58199
   226
lemma nth_default_nth:
haftmann@58437
   227
  "n < length xs \<Longrightarrow> nth_default dflt xs n = xs ! n"
haftmann@58199
   228
  by (simp add: nth_default_def)
haftmann@58199
   229
haftmann@58199
   230
lemma nth_default_beyond:
haftmann@58437
   231
  "length xs \<le> n \<Longrightarrow> nth_default dflt xs n = dflt"
haftmann@58437
   232
  by (simp add: nth_default_def)
haftmann@58437
   233
haftmann@58437
   234
lemma nth_default_Nil [simp]:
haftmann@58437
   235
  "nth_default dflt [] n = dflt"
haftmann@58437
   236
  by (simp add: nth_default_def)
haftmann@58437
   237
haftmann@58437
   238
lemma nth_default_Cons:
haftmann@58437
   239
  "nth_default dflt (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default dflt xs n')"
haftmann@58437
   240
  by (simp add: nth_default_def split: nat.split)
haftmann@58437
   241
haftmann@58437
   242
lemma nth_default_Cons_0 [simp]:
haftmann@58437
   243
  "nth_default dflt (x # xs) 0 = x"
haftmann@58437
   244
  by (simp add: nth_default_Cons)
haftmann@58437
   245
haftmann@58437
   246
lemma nth_default_Cons_Suc [simp]:
haftmann@58437
   247
  "nth_default dflt (x # xs) (Suc n) = nth_default dflt xs n"
haftmann@58437
   248
  by (simp add: nth_default_Cons)
haftmann@58437
   249
haftmann@58437
   250
lemma nth_default_replicate_dflt [simp]:
haftmann@58437
   251
  "nth_default dflt (replicate n dflt) m = dflt"
haftmann@58199
   252
  by (simp add: nth_default_def)
haftmann@58199
   253
haftmann@58437
   254
lemma nth_default_append:
haftmann@58437
   255
  "nth_default dflt (xs @ ys) n =
haftmann@58437
   256
    (if n < length xs then nth xs n else nth_default dflt ys (n - length xs))"
haftmann@58437
   257
  by (auto simp add: nth_default_def nth_append)
haftmann@58437
   258
haftmann@58437
   259
lemma nth_default_append_trailing [simp]:
haftmann@58437
   260
  "nth_default dflt (xs @ replicate n dflt) = nth_default dflt xs"
haftmann@58437
   261
  by (simp add: fun_eq_iff nth_default_append) (simp add: nth_default_def)
haftmann@58437
   262
haftmann@58437
   263
lemma nth_default_snoc_default [simp]:
haftmann@58437
   264
  "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
haftmann@58437
   265
  by (auto simp add: nth_default_def fun_eq_iff nth_append)
haftmann@58437
   266
haftmann@58437
   267
lemma nth_default_eq_dflt_iff:
haftmann@58437
   268
  "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
haftmann@58437
   269
  by (simp add: nth_default_def)
haftmann@58437
   270
haftmann@58437
   271
lemma in_enumerate_iff_nth_default_eq:
haftmann@58437
   272
  "x \<noteq> dflt \<Longrightarrow> (n, x) \<in> set (enumerate 0 xs) \<longleftrightarrow> nth_default dflt xs n = x"
haftmann@58437
   273
  by (auto simp add: nth_default_def in_set_conv_nth enumerate_eq_zip)
haftmann@58437
   274
haftmann@58437
   275
lemma last_conv_nth_default:
haftmann@58437
   276
  assumes "xs \<noteq> []"
haftmann@58437
   277
  shows "last xs = nth_default dflt xs (length xs - 1)"
haftmann@58437
   278
  using assms by (simp add: nth_default_def last_conv_nth)
haftmann@58437
   279
  
haftmann@58437
   280
lemma nth_default_map_eq:
haftmann@58437
   281
  "f dflt' = dflt \<Longrightarrow> nth_default dflt (map f xs) n = f (nth_default dflt' xs n)"
haftmann@58437
   282
  by (simp add: nth_default_def)
haftmann@58437
   283
haftmann@58437
   284
lemma finite_nth_default_neq_default [simp]:
haftmann@58437
   285
  "finite {k. nth_default dflt xs k \<noteq> dflt}"
haftmann@58437
   286
  by (simp add: nth_default_def)
haftmann@58437
   287
haftmann@58437
   288
lemma sorted_list_of_set_nth_default:
haftmann@58437
   289
  "sorted_list_of_set {k. nth_default dflt xs k \<noteq> dflt} = map fst (filter (\<lambda>(_, x). x \<noteq> dflt) (enumerate 0 xs))"
haftmann@58437
   290
  by (rule sorted_distinct_set_unique) (auto simp add: nth_default_def in_set_conv_nth
haftmann@58437
   291
    sorted_filter distinct_map_filter enumerate_eq_zip intro: rev_image_eqI)
haftmann@58437
   292
haftmann@58437
   293
lemma map_nth_default:
haftmann@58437
   294
  "map (nth_default x xs) [0..<length xs] = xs"
haftmann@58437
   295
proof -
haftmann@58437
   296
  have *: "map (nth_default x xs) [0..<length xs] = map (List.nth xs) [0..<length xs]"
haftmann@58437
   297
    by (rule map_cong) (simp_all add: nth_default_nth)
haftmann@58437
   298
  show ?thesis by (simp add: * map_nth)
haftmann@58437
   299
qed
haftmann@58437
   300
haftmann@58199
   301
lemma range_nth_default [simp]:
haftmann@58199
   302
  "range (nth_default dflt xs) = insert dflt (set xs)"
haftmann@58437
   303
  by (auto simp add: nth_default_def [abs_def] in_set_conv_nth)
haftmann@58199
   304
haftmann@58199
   305
lemma nth_strip_while:
haftmann@58199
   306
  assumes "n < length (strip_while P xs)"
haftmann@58199
   307
  shows "strip_while P xs ! n = xs ! n"
haftmann@58199
   308
proof -
haftmann@58199
   309
  have "length (dropWhile P (rev xs)) + length (takeWhile P (rev xs)) = length xs"
haftmann@58199
   310
    by (subst add.commute)
haftmann@58199
   311
      (simp add: arg_cong [where f=length, OF takeWhile_dropWhile_id, unfolded length_append])
haftmann@58199
   312
  then show ?thesis using assms
haftmann@58199
   313
    by (simp add: strip_while_def rev_nth dropWhile_nth)
haftmann@58199
   314
qed
haftmann@58199
   315
haftmann@58199
   316
lemma length_strip_while_le:
haftmann@58199
   317
  "length (strip_while P xs) \<le> length xs"
haftmann@58199
   318
  unfolding strip_while_def o_def length_rev
haftmann@58199
   319
  by (subst (2) length_rev[symmetric])
haftmann@58199
   320
    (simp add: strip_while_def length_dropWhile_le del: length_rev)
haftmann@58199
   321
haftmann@58199
   322
lemma nth_default_strip_while_dflt [simp]:
haftmann@58437
   323
  "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs"
haftmann@58199
   324
  by (induct xs rule: rev_induct) auto
haftmann@58199
   325
haftmann@58437
   326
lemma nth_default_eq_iff:
haftmann@58437
   327
  "nth_default dflt xs = nth_default dflt ys
haftmann@58437
   328
     \<longleftrightarrow> strip_while (HOL.eq dflt) xs = strip_while (HOL.eq dflt) ys" (is "?P \<longleftrightarrow> ?Q")
haftmann@58437
   329
proof
haftmann@58437
   330
  let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
haftmann@58437
   331
  assume ?P
haftmann@58437
   332
  then have eq: "nth_default dflt ?xs = nth_default dflt ?ys"
haftmann@58437
   333
    by simp
haftmann@58437
   334
  have len: "length ?xs = length ?ys"
haftmann@58437
   335
  proof (rule ccontr)
haftmann@58437
   336
    assume len: "length ?xs \<noteq> length ?ys"
haftmann@58437
   337
    { fix xs ys :: "'a list"
haftmann@58437
   338
      let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
haftmann@58437
   339
      assume eq: "nth_default dflt ?xs = nth_default dflt ?ys"
haftmann@58437
   340
      assume len: "length ?xs < length ?ys"
haftmann@58437
   341
      then have "length ?ys > 0" by arith
haftmann@58437
   342
      then have "?ys \<noteq> []" by simp
haftmann@58437
   343
      with last_conv_nth_default [of ?ys dflt]
haftmann@58437
   344
      have "last ?ys = nth_default dflt ?ys (length ?ys - 1)"
haftmann@58437
   345
        by auto
wenzelm@60500
   346
      moreover from \<open>?ys \<noteq> []\<close> no_trailing_strip_while [of "HOL.eq dflt" ys]
haftmann@58437
   347
        have "last ?ys \<noteq> dflt" by (simp add: no_trailing_unfold)
haftmann@58437
   348
      ultimately have "nth_default dflt ?xs (length ?ys - 1) \<noteq> dflt"
haftmann@58437
   349
        using eq by simp
haftmann@58437
   350
      moreover from len have "length ?ys - 1 \<ge> length ?xs" by simp
haftmann@58437
   351
      ultimately have False by (simp only: nth_default_beyond) simp
haftmann@58437
   352
    } 
haftmann@58437
   353
    from this [of xs ys] this [of ys xs] len eq show False
haftmann@58437
   354
      by (auto simp only: linorder_class.neq_iff)
haftmann@58437
   355
  qed
haftmann@58437
   356
  then show ?Q
haftmann@58437
   357
  proof (rule nth_equalityI [rule_format])
haftmann@58437
   358
    fix n
wenzelm@63540
   359
    assume n: "n < length ?xs"
wenzelm@63540
   360
    with len have "n < length ?ys"
haftmann@58437
   361
      by simp
wenzelm@63540
   362
    with n have xs: "nth_default dflt ?xs n = ?xs ! n"
haftmann@58437
   363
      and ys: "nth_default dflt ?ys n = ?ys ! n"
haftmann@58437
   364
      by (simp_all only: nth_default_nth)
haftmann@58437
   365
    with eq show "?xs ! n = ?ys ! n"
haftmann@58437
   366
      by simp
haftmann@58437
   367
  qed
haftmann@58437
   368
next
haftmann@58437
   369
  assume ?Q
haftmann@58437
   370
  then have "nth_default dflt (strip_while (HOL.eq dflt) xs) = nth_default dflt (strip_while (HOL.eq dflt) ys)"
haftmann@58437
   371
    by simp
haftmann@58437
   372
  then show ?P
haftmann@58437
   373
    by simp
haftmann@58437
   374
qed
haftmann@58199
   375
haftmann@58199
   376
end
haftmann@58295
   377