src/HOL/Library/Sublist.thy
author blanchet
Wed Nov 20 18:58:00 2013 +0100 (2013-11-20)
changeset 54538 ba7392b52a7c
parent 54483 9f24325c2550
child 55579 207538943038
permissions -rw-r--r--
factor 'List_Prefix' out of 'Sublist' and move to 'Main' (needed for codatatypes)
Christian@49087
     1
(*  Title:      HOL/Library/Sublist.thy
wenzelm@10330
     2
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
Christian@49087
     3
    Author:     Christian Sternagel, JAIST
wenzelm@10330
     4
*)
wenzelm@10330
     5
blanchet@54538
     6
header {* Parallel lists, list suffixes, and homeomorphic embedding *}
wenzelm@10330
     7
Christian@49087
     8
theory Sublist
Christian@49087
     9
imports Main
nipkow@15131
    10
begin
wenzelm@10330
    11
wenzelm@10389
    12
subsection {* Parallel lists *}
wenzelm@10389
    13
Christian@50516
    14
definition parallel :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "\<parallel>" 50)
wenzelm@49107
    15
  where "(xs \<parallel> ys) = (\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs)"
wenzelm@10389
    16
Christian@50516
    17
lemma parallelI [intro]: "\<not> prefixeq xs ys \<Longrightarrow> \<not> prefixeq ys xs \<Longrightarrow> xs \<parallel> ys"
wenzelm@25692
    18
  unfolding parallel_def by blast
wenzelm@10330
    19
wenzelm@10389
    20
lemma parallelE [elim]:
wenzelm@25692
    21
  assumes "xs \<parallel> ys"
Christian@49087
    22
  obtains "\<not> prefixeq xs ys \<and> \<not> prefixeq ys xs"
wenzelm@25692
    23
  using assms unfolding parallel_def by blast
wenzelm@10330
    24
Christian@49087
    25
theorem prefixeq_cases:
Christian@49087
    26
  obtains "prefixeq xs ys" | "prefix ys xs" | "xs \<parallel> ys"
Christian@49087
    27
  unfolding parallel_def prefix_def by blast
wenzelm@10330
    28
wenzelm@10389
    29
theorem parallel_decomp:
Christian@50516
    30
  "xs \<parallel> ys \<Longrightarrow> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
wenzelm@10408
    31
proof (induct xs rule: rev_induct)
wenzelm@11987
    32
  case Nil
wenzelm@23254
    33
  then have False by auto
wenzelm@23254
    34
  then show ?case ..
wenzelm@10408
    35
next
wenzelm@11987
    36
  case (snoc x xs)
wenzelm@11987
    37
  show ?case
Christian@49087
    38
  proof (rule prefixeq_cases)
Christian@49087
    39
    assume le: "prefixeq xs ys"
wenzelm@10408
    40
    then obtain ys' where ys: "ys = xs @ ys'" ..
wenzelm@10408
    41
    show ?thesis
wenzelm@10408
    42
    proof (cases ys')
nipkow@25564
    43
      assume "ys' = []"
Christian@49087
    44
      then show ?thesis by (metis append_Nil2 parallelE prefixeqI snoc.prems ys)
wenzelm@10389
    45
    next
wenzelm@10408
    46
      fix c cs assume ys': "ys' = c # cs"
blanchet@54483
    47
      have "x \<noteq> c" using snoc.prems ys ys' by fastforce
blanchet@54483
    48
      thus "\<exists>as b bs c cs. b \<noteq> c \<and> xs @ [x] = as @ b # bs \<and> ys = as @ c # cs"
blanchet@54483
    49
        using ys ys' by blast
wenzelm@10389
    50
    qed
wenzelm@10408
    51
  next
wenzelm@49107
    52
    assume "prefix ys xs"
wenzelm@49107
    53
    then have "prefixeq ys (xs @ [x])" by (simp add: prefix_def)
wenzelm@11987
    54
    with snoc have False by blast
wenzelm@23254
    55
    then show ?thesis ..
wenzelm@10408
    56
  next
wenzelm@10408
    57
    assume "xs \<parallel> ys"
wenzelm@11987
    58
    with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
wenzelm@10408
    59
      and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
wenzelm@10408
    60
      by blast
wenzelm@10408
    61
    from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp
wenzelm@10408
    62
    with neq ys show ?thesis by blast
wenzelm@10389
    63
  qed
wenzelm@10389
    64
qed
wenzelm@10330
    65
nipkow@25564
    66
lemma parallel_append: "a \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d"
wenzelm@25692
    67
  apply (rule parallelI)
wenzelm@25692
    68
    apply (erule parallelE, erule conjE,
Christian@49087
    69
      induct rule: not_prefixeq_induct, simp+)+
wenzelm@25692
    70
  done
kleing@25299
    71
wenzelm@25692
    72
lemma parallel_appendI: "xs \<parallel> ys \<Longrightarrow> x = xs @ xs' \<Longrightarrow> y = ys @ ys' \<Longrightarrow> x \<parallel> y"
wenzelm@25692
    73
  by (simp add: parallel_append)
kleing@25299
    74
wenzelm@25692
    75
lemma parallel_commute: "a \<parallel> b \<longleftrightarrow> b \<parallel> a"
wenzelm@25692
    76
  unfolding parallel_def by auto
oheimb@14538
    77
wenzelm@25356
    78
Christian@49087
    79
subsection {* Suffix order on lists *}
wenzelm@17201
    80
wenzelm@49107
    81
definition suffixeq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
wenzelm@49107
    82
  where "suffixeq xs ys = (\<exists>zs. ys = zs @ xs)"
Christian@49087
    83
wenzelm@49107
    84
definition suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
wenzelm@49107
    85
  where "suffix xs ys \<longleftrightarrow> (\<exists>us. ys = us @ xs \<and> us \<noteq> [])"
oheimb@14538
    86
Christian@49087
    87
lemma suffix_imp_suffixeq:
Christian@49087
    88
  "suffix xs ys \<Longrightarrow> suffixeq xs ys"
Christian@49087
    89
  by (auto simp: suffixeq_def suffix_def)
Christian@49087
    90
Christian@50516
    91
lemma suffixeqI [intro?]: "ys = zs @ xs \<Longrightarrow> suffixeq xs ys"
Christian@49087
    92
  unfolding suffixeq_def by blast
wenzelm@21305
    93
Christian@49087
    94
lemma suffixeqE [elim?]:
Christian@49087
    95
  assumes "suffixeq xs ys"
Christian@49087
    96
  obtains zs where "ys = zs @ xs"
Christian@49087
    97
  using assms unfolding suffixeq_def by blast
wenzelm@21305
    98
Christian@49087
    99
lemma suffixeq_refl [iff]: "suffixeq xs xs"
Christian@49087
   100
  by (auto simp add: suffixeq_def)
Christian@49087
   101
lemma suffix_trans:
Christian@49087
   102
  "suffix xs ys \<Longrightarrow> suffix ys zs \<Longrightarrow> suffix xs zs"
Christian@49087
   103
  by (auto simp: suffix_def)
Christian@49087
   104
lemma suffixeq_trans: "\<lbrakk>suffixeq xs ys; suffixeq ys zs\<rbrakk> \<Longrightarrow> suffixeq xs zs"
Christian@49087
   105
  by (auto simp add: suffixeq_def)
Christian@49087
   106
lemma suffixeq_antisym: "\<lbrakk>suffixeq xs ys; suffixeq ys xs\<rbrakk> \<Longrightarrow> xs = ys"
Christian@49087
   107
  by (auto simp add: suffixeq_def)
Christian@49087
   108
Christian@49087
   109
lemma suffixeq_tl [simp]: "suffixeq (tl xs) xs"
Christian@49087
   110
  by (induct xs) (auto simp: suffixeq_def)
oheimb@14538
   111
Christian@49087
   112
lemma suffix_tl [simp]: "xs \<noteq> [] \<Longrightarrow> suffix (tl xs) xs"
Christian@49087
   113
  by (induct xs) (auto simp: suffix_def)
oheimb@14538
   114
Christian@49087
   115
lemma Nil_suffixeq [iff]: "suffixeq [] xs"
Christian@49087
   116
  by (simp add: suffixeq_def)
Christian@49087
   117
lemma suffixeq_Nil [simp]: "(suffixeq xs []) = (xs = [])"
Christian@49087
   118
  by (auto simp add: suffixeq_def)
Christian@49087
   119
wenzelm@49107
   120
lemma suffixeq_ConsI: "suffixeq xs ys \<Longrightarrow> suffixeq xs (y # ys)"
Christian@49087
   121
  by (auto simp add: suffixeq_def)
wenzelm@49107
   122
lemma suffixeq_ConsD: "suffixeq (x # xs) ys \<Longrightarrow> suffixeq xs ys"
Christian@49087
   123
  by (auto simp add: suffixeq_def)
oheimb@14538
   124
Christian@49087
   125
lemma suffixeq_appendI: "suffixeq xs ys \<Longrightarrow> suffixeq xs (zs @ ys)"
Christian@49087
   126
  by (auto simp add: suffixeq_def)
Christian@49087
   127
lemma suffixeq_appendD: "suffixeq (zs @ xs) ys \<Longrightarrow> suffixeq xs ys"
Christian@49087
   128
  by (auto simp add: suffixeq_def)
Christian@49087
   129
Christian@49087
   130
lemma suffix_set_subset:
Christian@49087
   131
  "suffix xs ys \<Longrightarrow> set xs \<subseteq> set ys" by (auto simp: suffix_def)
oheimb@14538
   132
Christian@49087
   133
lemma suffixeq_set_subset:
Christian@49087
   134
  "suffixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys" by (auto simp: suffixeq_def)
Christian@49087
   135
wenzelm@49107
   136
lemma suffixeq_ConsD2: "suffixeq (x # xs) (y # ys) \<Longrightarrow> suffixeq xs ys"
wenzelm@21305
   137
proof -
wenzelm@49107
   138
  assume "suffixeq (x # xs) (y # ys)"
wenzelm@49107
   139
  then obtain zs where "y # ys = zs @ x # xs" ..
Christian@49087
   140
  then show ?thesis
Christian@49087
   141
    by (induct zs) (auto intro!: suffixeq_appendI suffixeq_ConsI)
wenzelm@21305
   142
qed
oheimb@14538
   143
Christian@49087
   144
lemma suffixeq_to_prefixeq [code]: "suffixeq xs ys \<longleftrightarrow> prefixeq (rev xs) (rev ys)"
Christian@49087
   145
proof
Christian@49087
   146
  assume "suffixeq xs ys"
Christian@49087
   147
  then obtain zs where "ys = zs @ xs" ..
Christian@49087
   148
  then have "rev ys = rev xs @ rev zs" by simp
Christian@49087
   149
  then show "prefixeq (rev xs) (rev ys)" ..
Christian@49087
   150
next
Christian@49087
   151
  assume "prefixeq (rev xs) (rev ys)"
Christian@49087
   152
  then obtain zs where "rev ys = rev xs @ zs" ..
Christian@49087
   153
  then have "rev (rev ys) = rev zs @ rev (rev xs)" by simp
Christian@49087
   154
  then have "ys = rev zs @ xs" by simp
Christian@49087
   155
  then show "suffixeq xs ys" ..
wenzelm@21305
   156
qed
oheimb@14538
   157
Christian@49087
   158
lemma distinct_suffixeq: "distinct ys \<Longrightarrow> suffixeq xs ys \<Longrightarrow> distinct xs"
Christian@49087
   159
  by (clarsimp elim!: suffixeqE)
wenzelm@17201
   160
Christian@49087
   161
lemma suffixeq_map: "suffixeq xs ys \<Longrightarrow> suffixeq (map f xs) (map f ys)"
Christian@49087
   162
  by (auto elim!: suffixeqE intro: suffixeqI)
kleing@25299
   163
Christian@49087
   164
lemma suffixeq_drop: "suffixeq (drop n as) as"
Christian@49087
   165
  unfolding suffixeq_def
wenzelm@25692
   166
  apply (rule exI [where x = "take n as"])
wenzelm@25692
   167
  apply simp
wenzelm@25692
   168
  done
kleing@25299
   169
Christian@49087
   170
lemma suffixeq_take: "suffixeq xs ys \<Longrightarrow> ys = take (length ys - length xs) ys @ xs"
wenzelm@49107
   171
  by (auto elim!: suffixeqE)
kleing@25299
   172
wenzelm@49107
   173
lemma suffixeq_suffix_reflclp_conv: "suffixeq = suffix\<^sup>=\<^sup>="
Christian@49087
   174
proof (intro ext iffI)
Christian@49087
   175
  fix xs ys :: "'a list"
Christian@49087
   176
  assume "suffixeq xs ys"
Christian@49087
   177
  show "suffix\<^sup>=\<^sup>= xs ys"
Christian@49087
   178
  proof
Christian@49087
   179
    assume "xs \<noteq> ys"
wenzelm@49107
   180
    with `suffixeq xs ys` show "suffix xs ys"
wenzelm@49107
   181
      by (auto simp: suffixeq_def suffix_def)
Christian@49087
   182
  qed
Christian@49087
   183
next
Christian@49087
   184
  fix xs ys :: "'a list"
Christian@49087
   185
  assume "suffix\<^sup>=\<^sup>= xs ys"
wenzelm@49107
   186
  then show "suffixeq xs ys"
Christian@49087
   187
  proof
wenzelm@49107
   188
    assume "suffix xs ys" then show "suffixeq xs ys"
wenzelm@49107
   189
      by (rule suffix_imp_suffixeq)
Christian@49087
   190
  next
wenzelm@49107
   191
    assume "xs = ys" then show "suffixeq xs ys"
wenzelm@49107
   192
      by (auto simp: suffixeq_def)
Christian@49087
   193
  qed
Christian@49087
   194
qed
Christian@49087
   195
Christian@49087
   196
lemma parallelD1: "x \<parallel> y \<Longrightarrow> \<not> prefixeq x y"
wenzelm@25692
   197
  by blast
kleing@25299
   198
Christian@49087
   199
lemma parallelD2: "x \<parallel> y \<Longrightarrow> \<not> prefixeq y x"
wenzelm@25692
   200
  by blast
wenzelm@25355
   201
wenzelm@25355
   202
lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []"
wenzelm@25692
   203
  unfolding parallel_def by simp
wenzelm@25355
   204
kleing@25299
   205
lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x"
wenzelm@25692
   206
  unfolding parallel_def by simp
kleing@25299
   207
nipkow@25564
   208
lemma Cons_parallelI1: "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs"
wenzelm@25692
   209
  by auto
kleing@25299
   210
nipkow@25564
   211
lemma Cons_parallelI2: "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs"
Christian@49087
   212
  by (metis Cons_prefixeq_Cons parallelE parallelI)
nipkow@25665
   213
kleing@25299
   214
lemma not_equal_is_parallel:
kleing@25299
   215
  assumes neq: "xs \<noteq> ys"
wenzelm@25356
   216
    and len: "length xs = length ys"
wenzelm@25356
   217
  shows "xs \<parallel> ys"
kleing@25299
   218
  using len neq
wenzelm@25355
   219
proof (induct rule: list_induct2)
haftmann@26445
   220
  case Nil
wenzelm@25356
   221
  then show ?case by simp
kleing@25299
   222
next
haftmann@26445
   223
  case (Cons a as b bs)
wenzelm@25355
   224
  have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact
kleing@25299
   225
  show ?case
kleing@25299
   226
  proof (cases "a = b")
wenzelm@25355
   227
    case True
haftmann@26445
   228
    then have "as \<noteq> bs" using Cons by simp
wenzelm@25355
   229
    then show ?thesis by (rule Cons_parallelI2 [OF True ih])
kleing@25299
   230
  next
kleing@25299
   231
    case False
wenzelm@25355
   232
    then show ?thesis by (rule Cons_parallelI1)
kleing@25299
   233
  qed
kleing@25299
   234
qed
haftmann@22178
   235
wenzelm@49107
   236
lemma suffix_reflclp_conv: "suffix\<^sup>=\<^sup>= = suffixeq"
Christian@49087
   237
  by (intro ext) (auto simp: suffixeq_def suffix_def)
Christian@49087
   238
wenzelm@49107
   239
lemma suffix_lists: "suffix xs ys \<Longrightarrow> ys \<in> lists A \<Longrightarrow> xs \<in> lists A"
Christian@49087
   240
  unfolding suffix_def by auto
Christian@49087
   241
Christian@49087
   242
Christian@50516
   243
subsection {* Homeomorphic embedding on lists *}
Christian@49087
   244
Christian@50516
   245
inductive list_hembeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
Christian@49087
   246
  for P :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
Christian@49087
   247
where
Christian@50516
   248
  list_hembeq_Nil [intro, simp]: "list_hembeq P [] ys"
Christian@50516
   249
| list_hembeq_Cons [intro] : "list_hembeq P xs ys \<Longrightarrow> list_hembeq P xs (y#ys)"
Christian@50516
   250
| list_hembeq_Cons2 [intro]: "P\<^sup>=\<^sup>= x y \<Longrightarrow> list_hembeq P xs ys \<Longrightarrow> list_hembeq P (x#xs) (y#ys)"
Christian@50516
   251
Christian@50516
   252
lemma list_hembeq_Nil2 [simp]:
Christian@50516
   253
  assumes "list_hembeq P xs []" shows "xs = []"
Christian@50516
   254
  using assms by (cases rule: list_hembeq.cases) auto
Christian@49087
   255
Christian@50516
   256
lemma list_hembeq_refl [simp, intro!]:
Christian@50516
   257
  "list_hembeq P xs xs"
Christian@50516
   258
  by (induct xs) auto
Christian@49087
   259
Christian@50516
   260
lemma list_hembeq_Cons_Nil [simp]: "list_hembeq P (x#xs) [] = False"
Christian@49087
   261
proof -
Christian@50516
   262
  { assume "list_hembeq P (x#xs) []"
Christian@50516
   263
    from list_hembeq_Nil2 [OF this] have False by simp
Christian@49087
   264
  } moreover {
Christian@49087
   265
    assume False
Christian@50516
   266
    then have "list_hembeq P (x#xs) []" by simp
Christian@49087
   267
  } ultimately show ?thesis by blast
Christian@49087
   268
qed
Christian@49087
   269
Christian@50516
   270
lemma list_hembeq_append2 [intro]: "list_hembeq P xs ys \<Longrightarrow> list_hembeq P xs (zs @ ys)"
Christian@49087
   271
  by (induct zs) auto
Christian@49087
   272
Christian@50516
   273
lemma list_hembeq_prefix [intro]:
Christian@50516
   274
  assumes "list_hembeq P xs ys" shows "list_hembeq P xs (ys @ zs)"
Christian@49087
   275
  using assms
Christian@49087
   276
  by (induct arbitrary: zs) auto
Christian@49087
   277
Christian@50516
   278
lemma list_hembeq_ConsD:
Christian@50516
   279
  assumes "list_hembeq P (x#xs) ys"
Christian@50516
   280
  shows "\<exists>us v vs. ys = us @ v # vs \<and> P\<^sup>=\<^sup>= x v \<and> list_hembeq P xs vs"
Christian@49087
   281
using assms
wenzelm@49107
   282
proof (induct x \<equiv> "x # xs" ys arbitrary: x xs)
Christian@50516
   283
  case list_hembeq_Cons
wenzelm@49107
   284
  then show ?case by (metis append_Cons)
Christian@49087
   285
next
Christian@50516
   286
  case (list_hembeq_Cons2 x y xs ys)
blanchet@54483
   287
  then show ?case by blast
Christian@49087
   288
qed
Christian@49087
   289
Christian@50516
   290
lemma list_hembeq_appendD:
Christian@50516
   291
  assumes "list_hembeq P (xs @ ys) zs"
Christian@50516
   292
  shows "\<exists>us vs. zs = us @ vs \<and> list_hembeq P xs us \<and> list_hembeq P ys vs"
Christian@49087
   293
using assms
Christian@49087
   294
proof (induction xs arbitrary: ys zs)
wenzelm@49107
   295
  case Nil then show ?case by auto
Christian@49087
   296
next
Christian@49087
   297
  case (Cons x xs)
blanchet@54483
   298
  then obtain us v vs where
blanchet@54483
   299
    zs: "zs = us @ v # vs" and p: "P\<^sup>=\<^sup>= x v" and lh: "list_hembeq P (xs @ ys) vs"
blanchet@54483
   300
    by (auto dest: list_hembeq_ConsD)
blanchet@54483
   301
  obtain sk\<^sub>0 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" and sk\<^sub>1 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
blanchet@54483
   302
    sk: "\<forall>x\<^sub>0 x\<^sub>1. \<not> list_hembeq P (xs @ x\<^sub>0) x\<^sub>1 \<or> sk\<^sub>0 x\<^sub>0 x\<^sub>1 @ sk\<^sub>1 x\<^sub>0 x\<^sub>1 = x\<^sub>1 \<and> list_hembeq P xs (sk\<^sub>0 x\<^sub>0 x\<^sub>1) \<and> list_hembeq P x\<^sub>0 (sk\<^sub>1 x\<^sub>0 x\<^sub>1)"
blanchet@54483
   303
    using Cons(1) by (metis (no_types))
blanchet@54483
   304
  hence "\<forall>x\<^sub>2. list_hembeq P (x # xs) (x\<^sub>2 @ v # sk\<^sub>0 ys vs)" using p lh by auto
blanchet@54483
   305
  thus ?case using lh zs sk by (metis (no_types) append_Cons append_assoc)
Christian@49087
   306
qed
Christian@49087
   307
Christian@50516
   308
lemma list_hembeq_suffix:
Christian@50516
   309
  assumes "list_hembeq P xs ys" and "suffix ys zs"
Christian@50516
   310
  shows "list_hembeq P xs zs"
Christian@50516
   311
  using assms(2) and list_hembeq_append2 [OF assms(1)] by (auto simp: suffix_def)
Christian@49087
   312
Christian@50516
   313
lemma list_hembeq_suffixeq:
Christian@50516
   314
  assumes "list_hembeq P xs ys" and "suffixeq ys zs"
Christian@50516
   315
  shows "list_hembeq P xs zs"
Christian@50516
   316
  using assms and list_hembeq_suffix unfolding suffixeq_suffix_reflclp_conv by auto
Christian@49087
   317
Christian@50516
   318
lemma list_hembeq_length: "list_hembeq P xs ys \<Longrightarrow> length xs \<le> length ys"
Christian@50516
   319
  by (induct rule: list_hembeq.induct) auto
Christian@49087
   320
Christian@50516
   321
lemma list_hembeq_trans:
Christian@50516
   322
  assumes "\<And>x y z. \<lbrakk>x \<in> A; y \<in> A; z \<in> A; P x y; P y z\<rbrakk> \<Longrightarrow> P x z"
Christian@50516
   323
  shows "\<And>xs ys zs. \<lbrakk>xs \<in> lists A; ys \<in> lists A; zs \<in> lists A;
Christian@50516
   324
    list_hembeq P xs ys; list_hembeq P ys zs\<rbrakk> \<Longrightarrow> list_hembeq P xs zs"
Christian@50516
   325
proof -
Christian@49087
   326
  fix xs ys zs
Christian@50516
   327
  assume "list_hembeq P xs ys" and "list_hembeq P ys zs"
Christian@49087
   328
    and "xs \<in> lists A" and "ys \<in> lists A" and "zs \<in> lists A"
Christian@50516
   329
  then show "list_hembeq P xs zs"
Christian@49087
   330
  proof (induction arbitrary: zs)
Christian@50516
   331
    case list_hembeq_Nil show ?case by blast
Christian@49087
   332
  next
Christian@50516
   333
    case (list_hembeq_Cons xs ys y)
Christian@50516
   334
    from list_hembeq_ConsD [OF `list_hembeq P (y#ys) zs`] obtain us v vs
Christian@50516
   335
      where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_hembeq P ys vs" by blast
Christian@50516
   336
    then have "list_hembeq P ys (v#vs)" by blast
Christian@50516
   337
    then have "list_hembeq P ys zs" unfolding zs by (rule list_hembeq_append2)
Christian@50516
   338
    from list_hembeq_Cons.IH [OF this] and list_hembeq_Cons.prems show ?case by simp
Christian@49087
   339
  next
Christian@50516
   340
    case (list_hembeq_Cons2 x y xs ys)
Christian@50516
   341
    from list_hembeq_ConsD [OF `list_hembeq P (y#ys) zs`] obtain us v vs
Christian@50516
   342
      where zs: "zs = us @ v # vs" and "P\<^sup>=\<^sup>= y v" and "list_hembeq P ys vs" by blast
Christian@50516
   343
    with list_hembeq_Cons2 have "list_hembeq P xs vs" by simp
Christian@50516
   344
    moreover have "P\<^sup>=\<^sup>= x v"
Christian@49087
   345
    proof -
Christian@49087
   346
      from zs and `zs \<in> lists A` have "v \<in> A" by auto
Christian@50516
   347
      moreover have "x \<in> A" and "y \<in> A" using list_hembeq_Cons2 by simp_all
Christian@50516
   348
      ultimately show ?thesis
Christian@50516
   349
        using `P\<^sup>=\<^sup>= x y` and `P\<^sup>=\<^sup>= y v` and assms
Christian@50516
   350
        by blast
Christian@49087
   351
    qed
Christian@50516
   352
    ultimately have "list_hembeq P (x#xs) (v#vs)" by blast
Christian@50516
   353
    then show ?case unfolding zs by (rule list_hembeq_append2)
Christian@49087
   354
  qed
Christian@49087
   355
qed
Christian@49087
   356
Christian@49087
   357
Christian@50516
   358
subsection {* Sublists (special case of homeomorphic embedding) *}
Christian@49087
   359
Christian@50516
   360
abbreviation sublisteq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
Christian@50516
   361
  where "sublisteq xs ys \<equiv> list_hembeq (op =) xs ys"
Christian@49087
   362
Christian@50516
   363
lemma sublisteq_Cons2: "sublisteq xs ys \<Longrightarrow> sublisteq (x#xs) (x#ys)" by auto
Christian@49087
   364
Christian@50516
   365
lemma sublisteq_same_length:
Christian@50516
   366
  assumes "sublisteq xs ys" and "length xs = length ys" shows "xs = ys"
Christian@50516
   367
  using assms by (induct) (auto dest: list_hembeq_length)
Christian@49087
   368
Christian@50516
   369
lemma not_sublisteq_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sublisteq xs ys"
Christian@50516
   370
  by (metis list_hembeq_length linorder_not_less)
Christian@49087
   371
Christian@49087
   372
lemma [code]:
Christian@50516
   373
  "list_hembeq P [] ys \<longleftrightarrow> True"
Christian@50516
   374
  "list_hembeq P (x#xs) [] \<longleftrightarrow> False"
Christian@49087
   375
  by (simp_all)
Christian@49087
   376
Christian@50516
   377
lemma sublisteq_Cons': "sublisteq (x#xs) ys \<Longrightarrow> sublisteq xs ys"
blanchet@54483
   378
  by (induct xs, simp, blast dest: list_hembeq_ConsD)
Christian@49087
   379
Christian@50516
   380
lemma sublisteq_Cons2':
Christian@50516
   381
  assumes "sublisteq (x#xs) (x#ys)" shows "sublisteq xs ys"
Christian@50516
   382
  using assms by (cases) (rule sublisteq_Cons')
Christian@49087
   383
Christian@50516
   384
lemma sublisteq_Cons2_neq:
Christian@50516
   385
  assumes "sublisteq (x#xs) (y#ys)"
Christian@50516
   386
  shows "x \<noteq> y \<Longrightarrow> sublisteq (x#xs) ys"
Christian@49087
   387
  using assms by (cases) auto
Christian@49087
   388
Christian@50516
   389
lemma sublisteq_Cons2_iff [simp, code]:
Christian@50516
   390
  "sublisteq (x#xs) (y#ys) = (if x = y then sublisteq xs ys else sublisteq (x#xs) ys)"
Christian@50516
   391
  by (metis list_hembeq_Cons sublisteq_Cons2 sublisteq_Cons2' sublisteq_Cons2_neq)
Christian@49087
   392
Christian@50516
   393
lemma sublisteq_append': "sublisteq (zs @ xs) (zs @ ys) \<longleftrightarrow> sublisteq xs ys"
Christian@49087
   394
  by (induct zs) simp_all
Christian@49087
   395
Christian@50516
   396
lemma sublisteq_refl [simp, intro!]: "sublisteq xs xs" by (induct xs) simp_all
Christian@49087
   397
Christian@50516
   398
lemma sublisteq_antisym:
Christian@50516
   399
  assumes "sublisteq xs ys" and "sublisteq ys xs"
Christian@49087
   400
  shows "xs = ys"
Christian@49087
   401
using assms
Christian@49087
   402
proof (induct)
Christian@50516
   403
  case list_hembeq_Nil
Christian@50516
   404
  from list_hembeq_Nil2 [OF this] show ?case by simp
Christian@49087
   405
next
Christian@50516
   406
  case list_hembeq_Cons2
blanchet@54483
   407
  thus ?case by simp
Christian@49087
   408
next
Christian@50516
   409
  case list_hembeq_Cons
blanchet@54483
   410
  hence False using sublisteq_Cons' by fastforce
blanchet@54483
   411
  thus ?case ..
Christian@49087
   412
qed
Christian@49087
   413
Christian@50516
   414
lemma sublisteq_trans: "sublisteq xs ys \<Longrightarrow> sublisteq ys zs \<Longrightarrow> sublisteq xs zs"
Christian@50516
   415
  by (rule list_hembeq_trans [of UNIV "op ="]) auto
Christian@49087
   416
Christian@50516
   417
lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []"
Christian@50516
   418
  by (auto dest: list_hembeq_length)
Christian@49087
   419
Christian@50516
   420
lemma list_hembeq_append_mono:
Christian@50516
   421
  "\<lbrakk> list_hembeq P xs xs'; list_hembeq P ys ys' \<rbrakk> \<Longrightarrow> list_hembeq P (xs@ys) (xs'@ys')"
Christian@50516
   422
  apply (induct rule: list_hembeq.induct)
Christian@50516
   423
    apply (metis eq_Nil_appendI list_hembeq_append2)
Christian@50516
   424
   apply (metis append_Cons list_hembeq_Cons)
Christian@50516
   425
  apply (metis append_Cons list_hembeq_Cons2)
wenzelm@49107
   426
  done
Christian@49087
   427
Christian@49087
   428
Christian@49087
   429
subsection {* Appending elements *}
Christian@49087
   430
Christian@50516
   431
lemma sublisteq_append [simp]:
Christian@50516
   432
  "sublisteq (xs @ zs) (ys @ zs) \<longleftrightarrow> sublisteq xs ys" (is "?l = ?r")
Christian@49087
   433
proof
Christian@50516
   434
  { fix xs' ys' xs ys zs :: "'a list" assume "sublisteq xs' ys'"
Christian@50516
   435
    then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sublisteq xs ys"
Christian@49087
   436
    proof (induct arbitrary: xs ys zs)
Christian@50516
   437
      case list_hembeq_Nil show ?case by simp
Christian@49087
   438
    next
Christian@50516
   439
      case (list_hembeq_Cons xs' ys' x)
Christian@50516
   440
      { assume "ys=[]" then have ?case using list_hembeq_Cons(1) by auto }
Christian@49087
   441
      moreover
Christian@49087
   442
      { fix us assume "ys = x#us"
Christian@50516
   443
        then have ?case using list_hembeq_Cons(2) by(simp add: list_hembeq.list_hembeq_Cons) }
Christian@49087
   444
      ultimately show ?case by (auto simp:Cons_eq_append_conv)
Christian@49087
   445
    next
Christian@50516
   446
      case (list_hembeq_Cons2 x y xs' ys')
Christian@50516
   447
      { assume "xs=[]" then have ?case using list_hembeq_Cons2(1) by auto }
Christian@49087
   448
      moreover
Christian@50516
   449
      { fix us vs assume "xs=x#us" "ys=x#vs" then have ?case using list_hembeq_Cons2 by auto}
Christian@49087
   450
      moreover
Christian@50516
   451
      { fix us assume "xs=x#us" "ys=[]" then have ?case using list_hembeq_Cons2(2) by bestsimp }
Christian@50516
   452
      ultimately show ?case using `op =\<^sup>=\<^sup>= x y` by (auto simp: Cons_eq_append_conv)
Christian@49087
   453
    qed }
Christian@49087
   454
  moreover assume ?l
Christian@49087
   455
  ultimately show ?r by blast
Christian@49087
   456
next
Christian@50516
   457
  assume ?r then show ?l by (metis list_hembeq_append_mono sublisteq_refl)
Christian@49087
   458
qed
Christian@49087
   459
Christian@50516
   460
lemma sublisteq_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (zs @ ys)"
Christian@49087
   461
  by (induct zs) auto
Christian@49087
   462
Christian@50516
   463
lemma sublisteq_rev_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (ys @ zs)"
Christian@50516
   464
  by (metis append_Nil2 list_hembeq_Nil list_hembeq_append_mono)
Christian@49087
   465
Christian@49087
   466
Christian@49087
   467
subsection {* Relation to standard list operations *}
Christian@49087
   468
Christian@50516
   469
lemma sublisteq_map:
Christian@50516
   470
  assumes "sublisteq xs ys" shows "sublisteq (map f xs) (map f ys)"
Christian@49087
   471
  using assms by (induct) auto
Christian@49087
   472
Christian@50516
   473
lemma sublisteq_filter_left [simp]: "sublisteq (filter P xs) xs"
Christian@49087
   474
  by (induct xs) auto
Christian@49087
   475
Christian@50516
   476
lemma sublisteq_filter [simp]:
Christian@50516
   477
  assumes "sublisteq xs ys" shows "sublisteq (filter P xs) (filter P ys)"
blanchet@54483
   478
  using assms by induct auto
Christian@49087
   479
Christian@50516
   480
lemma "sublisteq xs ys \<longleftrightarrow> (\<exists>N. xs = sublist ys N)" (is "?L = ?R")
Christian@49087
   481
proof
Christian@49087
   482
  assume ?L
wenzelm@49107
   483
  then show ?R
Christian@49087
   484
  proof (induct)
Christian@50516
   485
    case list_hembeq_Nil show ?case by (metis sublist_empty)
Christian@49087
   486
  next
Christian@50516
   487
    case (list_hembeq_Cons xs ys x)
Christian@49087
   488
    then obtain N where "xs = sublist ys N" by blast
wenzelm@49107
   489
    then have "xs = sublist (x#ys) (Suc ` N)"
Christian@49087
   490
      by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
wenzelm@49107
   491
    then show ?case by blast
Christian@49087
   492
  next
Christian@50516
   493
    case (list_hembeq_Cons2 x y xs ys)
Christian@49087
   494
    then obtain N where "xs = sublist ys N" by blast
wenzelm@49107
   495
    then have "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
Christian@49087
   496
      by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
Christian@50516
   497
    moreover from list_hembeq_Cons2 have "x = y" by simp
Christian@50516
   498
    ultimately show ?case by blast
Christian@49087
   499
  qed
Christian@49087
   500
next
Christian@49087
   501
  assume ?R
Christian@49087
   502
  then obtain N where "xs = sublist ys N" ..
Christian@50516
   503
  moreover have "sublisteq (sublist ys N) ys"
wenzelm@49107
   504
  proof (induct ys arbitrary: N)
Christian@49087
   505
    case Nil show ?case by simp
Christian@49087
   506
  next
wenzelm@49107
   507
    case Cons then show ?case by (auto simp: sublist_Cons)
Christian@49087
   508
  qed
Christian@49087
   509
  ultimately show ?L by simp
Christian@49087
   510
qed
Christian@49087
   511
wenzelm@10330
   512
end