src/HOL/Imperative_HOL/ex/Sublist.thy
author haftmann
Mon Mar 23 19:01:17 2009 +0100 (2009-03-23 ago)
changeset 30689 b14b2cc4e25e
parent 29920 src/HOL/ex/Sublist.thy@b95f5b8b93dd
child 32580 5b88ae4307ff
permissions -rw-r--r--
moved Imperative_HOL examples to Imperative_HOL/ex
bulwahn@27656
     1
(* $Id$ *)
bulwahn@27656
     2
bulwahn@27656
     3
header {* Slices of lists *}
bulwahn@27656
     4
bulwahn@27656
     5
theory Sublist
bulwahn@27656
     6
imports Multiset
bulwahn@27656
     7
begin
bulwahn@27656
     8
bulwahn@27656
     9
bulwahn@27656
    10
lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" 
bulwahn@27656
    11
apply (induct xs arbitrary: i j k)
bulwahn@27656
    12
apply simp
bulwahn@27656
    13
apply (simp only: sublist_Cons)
bulwahn@27656
    14
apply simp
bulwahn@27656
    15
apply safe
bulwahn@27656
    16
apply simp
bulwahn@27656
    17
apply (erule_tac x="0" in meta_allE)
bulwahn@27656
    18
apply (erule_tac x="j - 1" in meta_allE)
bulwahn@27656
    19
apply (erule_tac x="k - 1" in meta_allE)
bulwahn@27656
    20
apply (subgoal_tac "0 \<le> j - 1 \<and> j - 1 \<le> k - 1")
bulwahn@27656
    21
apply simp
bulwahn@27656
    22
apply (subgoal_tac "{ja. Suc ja < j} = {0..<j - Suc 0}")
bulwahn@27656
    23
apply (subgoal_tac "{ja. j \<le> Suc ja \<and> Suc ja < k} = {j - Suc 0..<k - Suc 0}")
bulwahn@27656
    24
apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}")
bulwahn@27656
    25
apply simp
bulwahn@27656
    26
apply fastsimp
bulwahn@27656
    27
apply fastsimp
bulwahn@27656
    28
apply fastsimp
bulwahn@27656
    29
apply fastsimp
bulwahn@27656
    30
apply (erule_tac x="i - 1" in meta_allE)
bulwahn@27656
    31
apply (erule_tac x="j - 1" in meta_allE)
bulwahn@27656
    32
apply (erule_tac x="k - 1" in meta_allE)
bulwahn@27656
    33
apply (subgoal_tac " {ja. i \<le> Suc ja \<and> Suc ja < j} = {i - 1 ..<j - 1}")
bulwahn@27656
    34
apply (subgoal_tac " {ja. j \<le> Suc ja \<and> Suc ja < k} = {j - 1..<k - 1}")
bulwahn@27656
    35
apply (subgoal_tac "{j. i \<le> Suc j \<and> Suc j < k} = {i - 1..<k - 1}")
bulwahn@27656
    36
apply (subgoal_tac " i - 1 \<le> j - 1 \<and> j - 1 \<le> k - 1")
bulwahn@27656
    37
apply simp
bulwahn@27656
    38
apply fastsimp
bulwahn@27656
    39
apply fastsimp
bulwahn@27656
    40
apply fastsimp
bulwahn@27656
    41
apply fastsimp
bulwahn@27656
    42
done
bulwahn@27656
    43
bulwahn@27656
    44
lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds"
bulwahn@27656
    45
apply (induct xs arbitrary: i inds)
bulwahn@27656
    46
apply simp
bulwahn@27656
    47
apply (case_tac i)
bulwahn@27656
    48
apply (simp add: sublist_Cons)
bulwahn@27656
    49
apply (simp add: sublist_Cons)
bulwahn@27656
    50
done
bulwahn@27656
    51
bulwahn@27656
    52
lemma sublist_update2: "i \<in> inds \<Longrightarrow> sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \<in> inds. k < i}):= v]"
bulwahn@27656
    53
proof (induct xs arbitrary: i inds)
bulwahn@27656
    54
  case Nil thus ?case by simp
bulwahn@27656
    55
next
bulwahn@27656
    56
  case (Cons x xs)
bulwahn@27656
    57
  thus ?case
bulwahn@27656
    58
  proof (cases i)
bulwahn@27656
    59
    case 0 with Cons show ?thesis by (simp add: sublist_Cons)
bulwahn@27656
    60
  next
bulwahn@27656
    61
    case (Suc i')
bulwahn@27656
    62
    with Cons show ?thesis
bulwahn@27656
    63
      apply simp
bulwahn@27656
    64
      apply (simp add: sublist_Cons)
bulwahn@27656
    65
      apply auto
bulwahn@27656
    66
      apply (auto simp add: nat.split)
bulwahn@27656
    67
      apply (simp add: card_less_Suc[symmetric])
bulwahn@27656
    68
      apply (simp add: card_less_Suc2)
bulwahn@27656
    69
      done
bulwahn@27656
    70
  qed
bulwahn@27656
    71
qed
bulwahn@27656
    72
bulwahn@27656
    73
lemma sublist_update: "sublist (xs[i := v]) inds = (if i \<in> inds then (sublist xs inds)[(card {k \<in> inds. k < i}) := v] else sublist xs inds)"
bulwahn@27656
    74
by (simp add: sublist_update1 sublist_update2)
bulwahn@27656
    75
bulwahn@27656
    76
lemma sublist_take: "sublist xs {j. j < m} = take m xs"
bulwahn@27656
    77
apply (induct xs arbitrary: m)
bulwahn@27656
    78
apply simp
bulwahn@27656
    79
apply (case_tac m)
bulwahn@27656
    80
apply simp
bulwahn@27656
    81
apply (simp add: sublist_Cons)
bulwahn@27656
    82
done
bulwahn@27656
    83
bulwahn@27656
    84
lemma sublist_take': "sublist xs {0..<m} = take m xs"
bulwahn@27656
    85
apply (induct xs arbitrary: m)
bulwahn@27656
    86
apply simp
bulwahn@27656
    87
apply (case_tac m)
bulwahn@27656
    88
apply simp
bulwahn@27656
    89
apply (simp add: sublist_Cons sublist_take)
bulwahn@27656
    90
done
bulwahn@27656
    91
bulwahn@27656
    92
lemma sublist_all[simp]: "sublist xs {j. j < length xs} = xs"
bulwahn@27656
    93
apply (induct xs)
bulwahn@27656
    94
apply simp
bulwahn@27656
    95
apply (simp add: sublist_Cons)
bulwahn@27656
    96
done
bulwahn@27656
    97
bulwahn@27656
    98
lemma sublist_all'[simp]: "sublist xs {0..<length xs} = xs"
bulwahn@27656
    99
apply (induct xs)
bulwahn@27656
   100
apply simp
bulwahn@27656
   101
apply (simp add: sublist_Cons)
bulwahn@27656
   102
done
bulwahn@27656
   103
bulwahn@27656
   104
lemma sublist_single: "a < length xs \<Longrightarrow> sublist xs {a} = [xs ! a]"
bulwahn@27656
   105
apply (induct xs arbitrary: a)
bulwahn@27656
   106
apply simp
bulwahn@27656
   107
apply(case_tac aa)
bulwahn@27656
   108
apply simp
bulwahn@27656
   109
apply (simp add: sublist_Cons)
bulwahn@27656
   110
apply simp
bulwahn@27656
   111
apply (simp add: sublist_Cons)
bulwahn@27656
   112
done
bulwahn@27656
   113
bulwahn@27656
   114
lemma sublist_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> sublist xs inds = []" 
bulwahn@27656
   115
apply (induct xs arbitrary: inds)
bulwahn@27656
   116
apply simp
bulwahn@27656
   117
apply (simp add: sublist_Cons)
bulwahn@27656
   118
apply auto
bulwahn@27656
   119
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
bulwahn@27656
   120
apply auto
bulwahn@27656
   121
done
bulwahn@27656
   122
bulwahn@27656
   123
lemma sublist_Nil': "sublist xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs"
bulwahn@27656
   124
apply (induct xs arbitrary: inds)
bulwahn@27656
   125
apply simp
bulwahn@27656
   126
apply (simp add: sublist_Cons)
bulwahn@27656
   127
apply (auto split: if_splits)
bulwahn@27656
   128
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
bulwahn@27656
   129
apply (case_tac x, auto)
bulwahn@27656
   130
done
bulwahn@27656
   131
bulwahn@27656
   132
lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)"
bulwahn@27656
   133
apply (induct xs arbitrary: inds)
bulwahn@27656
   134
apply simp
bulwahn@27656
   135
apply (simp add: sublist_Cons)
bulwahn@27656
   136
apply auto
bulwahn@27656
   137
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
bulwahn@27656
   138
apply (case_tac x, auto)
bulwahn@27656
   139
done
bulwahn@27656
   140
bulwahn@27656
   141
lemma sublist_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; sublist xs inds = sublist ys inds \<rbrakk> \<Longrightarrow> sublist xs inds' = sublist ys inds'"
bulwahn@27656
   142
apply (induct xs arbitrary: ys inds inds')
bulwahn@27656
   143
apply simp
bulwahn@27656
   144
apply (drule sym, rule sym)
bulwahn@27656
   145
apply (simp add: sublist_Nil, fastsimp)
bulwahn@27656
   146
apply (case_tac ys)
bulwahn@27656
   147
apply (simp add: sublist_Nil, fastsimp)
bulwahn@27656
   148
apply (auto simp add: sublist_Cons)
bulwahn@27656
   149
apply (erule_tac x="list" in meta_allE)
bulwahn@27656
   150
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
bulwahn@27656
   151
apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
bulwahn@27656
   152
apply fastsimp
bulwahn@27656
   153
apply (erule_tac x="list" in meta_allE)
bulwahn@27656
   154
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
bulwahn@27656
   155
apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
bulwahn@27656
   156
apply fastsimp
bulwahn@27656
   157
done
bulwahn@27656
   158
bulwahn@27656
   159
lemma sublist_eq: "\<lbrakk> \<forall>i \<in> inds. ((i < length xs) \<and> (i < length ys)) \<or> ((i \<ge> length xs ) \<and> (i \<ge> length ys)); \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
bulwahn@27656
   160
apply (induct xs arbitrary: ys inds)
bulwahn@27656
   161
apply simp
bulwahn@27656
   162
apply (rule sym, simp add: sublist_Nil)
bulwahn@27656
   163
apply (case_tac ys)
bulwahn@27656
   164
apply (simp add: sublist_Nil)
bulwahn@27656
   165
apply (auto simp add: sublist_Cons)
bulwahn@27656
   166
apply (erule_tac x="list" in meta_allE)
bulwahn@27656
   167
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
bulwahn@27656
   168
apply fastsimp
bulwahn@27656
   169
apply (erule_tac x="list" in meta_allE)
bulwahn@27656
   170
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
bulwahn@27656
   171
apply fastsimp
bulwahn@27656
   172
done
bulwahn@27656
   173
bulwahn@27656
   174
lemma sublist_eq_samelength: "\<lbrakk> length xs = length ys; \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
bulwahn@27656
   175
by (rule sublist_eq, auto)
bulwahn@27656
   176
bulwahn@27656
   177
lemma sublist_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist xs inds = sublist ys inds) = (\<forall>i \<in> inds. xs ! i = ys ! i)"
bulwahn@27656
   178
apply (induct xs arbitrary: ys inds)
bulwahn@27656
   179
apply simp
bulwahn@27656
   180
apply (rule sym, simp add: sublist_Nil)
bulwahn@27656
   181
apply (case_tac ys)
bulwahn@27656
   182
apply (simp add: sublist_Nil)
bulwahn@27656
   183
apply (auto simp add: sublist_Cons)
bulwahn@27656
   184
apply (case_tac i)
bulwahn@27656
   185
apply auto
bulwahn@27656
   186
apply (case_tac i)
bulwahn@27656
   187
apply auto
bulwahn@27656
   188
done
bulwahn@27656
   189
bulwahn@27656
   190
section {* Another sublist function *}
bulwahn@27656
   191
bulwahn@27656
   192
function sublist' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
bulwahn@27656
   193
where
bulwahn@27656
   194
  "sublist' n m [] = []"
bulwahn@27656
   195
| "sublist' n 0 xs = []"
bulwahn@27656
   196
| "sublist' 0 (Suc m) (x#xs) = (x#sublist' 0 m xs)"
bulwahn@27656
   197
| "sublist' (Suc n) (Suc m) (x#xs) = sublist' n m xs"
bulwahn@27656
   198
by pat_completeness auto
bulwahn@27656
   199
termination by lexicographic_order
bulwahn@27656
   200
bulwahn@27656
   201
subsection {* Proving equivalence to the other sublist command *}
bulwahn@27656
   202
bulwahn@27656
   203
lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \<le> j \<and> j < m}"
bulwahn@27656
   204
apply (induct xs arbitrary: n m)
bulwahn@27656
   205
apply simp
bulwahn@27656
   206
apply (case_tac n)
bulwahn@27656
   207
apply (case_tac m)
bulwahn@27656
   208
apply simp
bulwahn@27656
   209
apply (simp add: sublist_Cons)
bulwahn@27656
   210
apply (case_tac m)
bulwahn@27656
   211
apply simp
bulwahn@27656
   212
apply (simp add: sublist_Cons)
bulwahn@27656
   213
done
bulwahn@27656
   214
bulwahn@27656
   215
bulwahn@27656
   216
lemma "sublist' n m xs = sublist xs {n..<m}"
bulwahn@27656
   217
apply (induct xs arbitrary: n m)
bulwahn@27656
   218
apply simp
bulwahn@27656
   219
apply (case_tac n, case_tac m)
bulwahn@27656
   220
apply simp
bulwahn@27656
   221
apply simp
bulwahn@27656
   222
apply (simp add: sublist_take')
bulwahn@27656
   223
apply (case_tac m)
bulwahn@27656
   224
apply simp
bulwahn@27656
   225
apply (simp add: sublist_Cons sublist'_sublist)
bulwahn@27656
   226
done
bulwahn@27656
   227
bulwahn@27656
   228
bulwahn@27656
   229
subsection {* Showing equivalence to use of drop and take for definition *}
bulwahn@27656
   230
bulwahn@27656
   231
lemma "sublist' n m xs = take (m - n) (drop n xs)"
bulwahn@27656
   232
apply (induct xs arbitrary: n m)
bulwahn@27656
   233
apply simp
bulwahn@27656
   234
apply (case_tac m)
bulwahn@27656
   235
apply simp
bulwahn@27656
   236
apply (case_tac n)
bulwahn@27656
   237
apply simp
bulwahn@27656
   238
apply simp
bulwahn@27656
   239
done
bulwahn@27656
   240
bulwahn@27656
   241
subsection {* General lemma about sublist *}
bulwahn@27656
   242
bulwahn@27656
   243
lemma sublist'_Nil[simp]: "sublist' i j [] = []"
bulwahn@27656
   244
by simp
bulwahn@27656
   245
bulwahn@27656
   246
lemma sublist'_Cons[simp]: "sublist' i (Suc j) (x#xs) = (case i of 0 \<Rightarrow> (x # sublist' 0 j xs) | Suc i' \<Rightarrow>  sublist' i' j xs)"
bulwahn@27656
   247
by (cases i) auto
bulwahn@27656
   248
bulwahn@27656
   249
lemma sublist'_Cons2[simp]: "sublist' i j (x#xs) = (if (j = 0) then [] else ((if (i = 0) then [x] else []) @ sublist' (i - 1) (j - 1) xs))"
bulwahn@27656
   250
apply (cases j)
bulwahn@27656
   251
apply auto
bulwahn@27656
   252
apply (cases i)
bulwahn@27656
   253
apply auto
bulwahn@27656
   254
done
bulwahn@27656
   255
bulwahn@27656
   256
lemma sublist_n_0: "sublist' n 0 xs = []"
bulwahn@27656
   257
by (induct xs, auto)
bulwahn@27656
   258
bulwahn@27656
   259
lemma sublist'_Nil': "n \<ge> m \<Longrightarrow> sublist' n m xs = []"
bulwahn@27656
   260
apply (induct xs arbitrary: n m)
bulwahn@27656
   261
apply simp
bulwahn@27656
   262
apply (case_tac m)
bulwahn@27656
   263
apply simp
bulwahn@27656
   264
apply (case_tac n)
bulwahn@27656
   265
apply simp
bulwahn@27656
   266
apply simp
bulwahn@27656
   267
done
bulwahn@27656
   268
bulwahn@27656
   269
lemma sublist'_Nil2: "n \<ge> length xs \<Longrightarrow> sublist' n m xs = []"
bulwahn@27656
   270
apply (induct xs arbitrary: n m)
bulwahn@27656
   271
apply simp
bulwahn@27656
   272
apply (case_tac m)
bulwahn@27656
   273
apply simp
bulwahn@27656
   274
apply (case_tac n)
bulwahn@27656
   275
apply simp
bulwahn@27656
   276
apply simp
bulwahn@27656
   277
done
bulwahn@27656
   278
bulwahn@27656
   279
lemma sublist'_Nil3: "(sublist' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
bulwahn@27656
   280
apply (induct xs arbitrary: n m)
bulwahn@27656
   281
apply simp
bulwahn@27656
   282
apply (case_tac m)
bulwahn@27656
   283
apply simp
bulwahn@27656
   284
apply (case_tac n)
bulwahn@27656
   285
apply simp
bulwahn@27656
   286
apply simp
bulwahn@27656
   287
done
bulwahn@27656
   288
bulwahn@27656
   289
lemma sublist'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> sublist' n m xs \<noteq> []"
bulwahn@27656
   290
apply (induct xs arbitrary: n m)
bulwahn@27656
   291
apply simp
bulwahn@27656
   292
apply (case_tac m)
bulwahn@27656
   293
apply simp
bulwahn@27656
   294
apply (case_tac n)
bulwahn@27656
   295
apply simp
bulwahn@27656
   296
apply simp
bulwahn@27656
   297
done
bulwahn@27656
   298
bulwahn@27656
   299
lemma sublist'_single: "n < length xs \<Longrightarrow> sublist' n (Suc n) xs = [xs ! n]"
bulwahn@27656
   300
apply (induct xs arbitrary: n)
bulwahn@27656
   301
apply simp
bulwahn@27656
   302
apply simp
bulwahn@27656
   303
apply (case_tac n)
bulwahn@27656
   304
apply (simp add: sublist_n_0)
bulwahn@27656
   305
apply simp
bulwahn@27656
   306
done
bulwahn@27656
   307
bulwahn@27656
   308
lemma sublist'_update1: "i \<ge> m \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
bulwahn@27656
   309
apply (induct xs arbitrary: n m i)
bulwahn@27656
   310
apply simp
bulwahn@27656
   311
apply simp
bulwahn@27656
   312
apply (case_tac i)
bulwahn@27656
   313
apply simp
bulwahn@27656
   314
apply simp
bulwahn@27656
   315
done
bulwahn@27656
   316
bulwahn@27656
   317
lemma sublist'_update2: "i < n \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
bulwahn@27656
   318
apply (induct xs arbitrary: n m i)
bulwahn@27656
   319
apply simp
bulwahn@27656
   320
apply simp
bulwahn@27656
   321
apply (case_tac i)
bulwahn@27656
   322
apply simp
bulwahn@27656
   323
apply simp
bulwahn@27656
   324
done
bulwahn@27656
   325
bulwahn@27656
   326
lemma sublist'_update3: "\<lbrakk>n \<le> i; i < m\<rbrakk> \<Longrightarrow> sublist' n m (xs[i := v]) = (sublist' n m xs)[i - n := v]"
bulwahn@27656
   327
proof (induct xs arbitrary: n m i)
bulwahn@27656
   328
  case Nil thus ?case by auto
bulwahn@27656
   329
next
bulwahn@27656
   330
  case (Cons x xs)
bulwahn@27656
   331
  thus ?case
bulwahn@27656
   332
    apply -
bulwahn@27656
   333
    apply auto
bulwahn@27656
   334
    apply (cases i)
bulwahn@27656
   335
    apply auto
bulwahn@27656
   336
    apply (cases i)
bulwahn@27656
   337
    apply auto
bulwahn@27656
   338
    done
bulwahn@27656
   339
qed
bulwahn@27656
   340
bulwahn@27656
   341
lemma "\<lbrakk> sublist' i j xs = sublist' i j ys; n \<ge> i; m \<le> j \<rbrakk> \<Longrightarrow> sublist' n m xs = sublist' n m ys"
bulwahn@27656
   342
proof (induct xs arbitrary: i j ys n m)
bulwahn@27656
   343
  case Nil
bulwahn@27656
   344
  thus ?case
bulwahn@27656
   345
    apply -
bulwahn@27656
   346
    apply (rule sym, drule sym)
bulwahn@27656
   347
    apply (simp add: sublist'_Nil)
bulwahn@27656
   348
    apply (simp add: sublist'_Nil3)
bulwahn@27656
   349
    apply arith
bulwahn@27656
   350
    done
bulwahn@27656
   351
next
bulwahn@27656
   352
  case (Cons x xs i j ys n m)
bulwahn@27656
   353
  note c = this
bulwahn@27656
   354
  thus ?case
bulwahn@27656
   355
  proof (cases m)
bulwahn@27656
   356
    case 0 thus ?thesis by (simp add: sublist_n_0)
bulwahn@27656
   357
  next
bulwahn@27656
   358
    case (Suc m')
bulwahn@27656
   359
    note a = this
bulwahn@27656
   360
    thus ?thesis
bulwahn@27656
   361
    proof (cases n)
bulwahn@27656
   362
      case 0 note b = this
bulwahn@27656
   363
      show ?thesis
bulwahn@27656
   364
      proof (cases ys)
bulwahn@27656
   365
	case Nil  with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3)
bulwahn@27656
   366
      next
bulwahn@27656
   367
	case (Cons y ys)
bulwahn@27656
   368
	show ?thesis
bulwahn@27656
   369
	proof (cases j)
bulwahn@27656
   370
	  case 0 with a b Cons.prems show ?thesis by simp
bulwahn@27656
   371
	next
bulwahn@27656
   372
	  case (Suc j') with a b Cons.prems Cons show ?thesis 
bulwahn@27656
   373
	    apply -
bulwahn@27656
   374
	    apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto)
bulwahn@27656
   375
	    done
bulwahn@27656
   376
	qed
bulwahn@27656
   377
      qed
bulwahn@27656
   378
    next
bulwahn@27656
   379
      case (Suc n')
bulwahn@27656
   380
      show ?thesis
bulwahn@27656
   381
      proof (cases ys)
bulwahn@27656
   382
	case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3)
bulwahn@27656
   383
      next
bulwahn@27656
   384
	case (Cons y ys) with Suc a Cons.prems show ?thesis
bulwahn@27656
   385
	  apply -
bulwahn@27656
   386
	  apply simp
bulwahn@27656
   387
	  apply (cases j)
bulwahn@27656
   388
	  apply simp
bulwahn@27656
   389
	  apply (cases i)
bulwahn@27656
   390
	  apply simp
bulwahn@27656
   391
	  apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"])
bulwahn@27656
   392
	  apply simp
bulwahn@27656
   393
	  apply simp
bulwahn@27656
   394
	  apply simp
bulwahn@27656
   395
	  apply simp
bulwahn@27656
   396
	  apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"])
bulwahn@27656
   397
	  apply simp
bulwahn@27656
   398
	  apply simp
bulwahn@27656
   399
	  apply simp
bulwahn@27656
   400
	  done
bulwahn@27656
   401
      qed
bulwahn@27656
   402
    qed
bulwahn@27656
   403
  qed
bulwahn@27656
   404
qed
bulwahn@27656
   405
bulwahn@27656
   406
lemma length_sublist': "j \<le> length xs \<Longrightarrow> length (sublist' i j xs) = j - i"
bulwahn@27656
   407
by (induct xs arbitrary: i j, auto)
bulwahn@27656
   408
bulwahn@27656
   409
lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs"
bulwahn@27656
   410
apply (induct xs arbitrary: a i j)
bulwahn@27656
   411
apply simp
bulwahn@27656
   412
apply (case_tac j)
bulwahn@27656
   413
apply simp
bulwahn@27656
   414
apply (case_tac i)
bulwahn@27656
   415
apply simp
bulwahn@27656
   416
apply simp
bulwahn@27656
   417
done
bulwahn@27656
   418
bulwahn@27656
   419
lemma sublist'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]"
bulwahn@27656
   420
apply (induct xs arbitrary: a i j)
bulwahn@27656
   421
apply simp
bulwahn@27656
   422
apply simp
bulwahn@27656
   423
apply (case_tac j)
bulwahn@27656
   424
apply simp
bulwahn@27656
   425
apply auto
bulwahn@27656
   426
apply (case_tac nat)
bulwahn@27656
   427
apply auto
bulwahn@27656
   428
done
bulwahn@27656
   429
bulwahn@27656
   430
(* suffices that j \<le> length xs and length ys *) 
bulwahn@27656
   431
lemma sublist'_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist' i j xs  = sublist' i j ys) = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> xs ! i' = ys ! i')"
bulwahn@27656
   432
proof (induct xs arbitrary: ys i j)
bulwahn@27656
   433
  case Nil thus ?case by simp
bulwahn@27656
   434
next
bulwahn@27656
   435
  case (Cons x xs)
bulwahn@27656
   436
  thus ?case
bulwahn@27656
   437
    apply -
bulwahn@27656
   438
    apply (cases ys)
bulwahn@27656
   439
    apply simp
bulwahn@27656
   440
    apply simp
bulwahn@27656
   441
    apply auto
bulwahn@27656
   442
    apply (case_tac i', auto)
bulwahn@27656
   443
    apply (erule_tac x="Suc i'" in allE, auto)
bulwahn@27656
   444
    apply (erule_tac x="i' - 1" in allE, auto)
bulwahn@27656
   445
    apply (case_tac i', auto)
bulwahn@27656
   446
    apply (erule_tac x="Suc i'" in allE, auto)
bulwahn@27656
   447
    done
bulwahn@27656
   448
qed
bulwahn@27656
   449
bulwahn@27656
   450
lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs"
bulwahn@27656
   451
by (induct xs, auto)
bulwahn@27656
   452
bulwahn@27656
   453
lemma sublist'_sublist': "sublist' n m (sublist' i j xs) = sublist' (i + n) (min (i + m) j) xs" 
bulwahn@27656
   454
by (induct xs arbitrary: i j n m) (auto simp add: min_diff)
bulwahn@27656
   455
bulwahn@27656
   456
lemma sublist'_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow>(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs"
bulwahn@27656
   457
by (induct xs arbitrary: i j k) auto
bulwahn@27656
   458
bulwahn@27656
   459
lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
bulwahn@27656
   460
apply (induct xs arbitrary: i j k)
bulwahn@27656
   461
apply auto
bulwahn@27656
   462
apply (case_tac k)
bulwahn@27656
   463
apply auto
bulwahn@27656
   464
apply (case_tac i)
bulwahn@27656
   465
apply auto
bulwahn@27656
   466
done
bulwahn@27656
   467
bulwahn@27656
   468
lemma set_sublist': "set (sublist' i j xs) = {x. \<exists>k. i \<le> k \<and> k < j \<and> k < List.length xs \<and> x = xs ! k}"
bulwahn@27656
   469
apply (simp add: sublist'_sublist)
bulwahn@27656
   470
apply (simp add: set_sublist)
bulwahn@27656
   471
apply auto
bulwahn@27656
   472
done
bulwahn@27656
   473
bulwahn@27656
   474
lemma all_in_set_sublist'_conv: "(\<forall>j. j \<in> set (sublist' l r xs) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
bulwahn@27656
   475
unfolding set_sublist' by blast
bulwahn@27656
   476
bulwahn@27656
   477
lemma ball_in_set_sublist'_conv: "(\<forall>j \<in> set (sublist' l r xs). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
bulwahn@27656
   478
unfolding set_sublist' by blast
bulwahn@27656
   479
bulwahn@27656
   480
bulwahn@27656
   481
lemma multiset_of_sublist:
bulwahn@27656
   482
assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
bulwahn@27656
   483
assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
bulwahn@27656
   484
assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
bulwahn@27656
   485
assumes multiset: "multiset_of xs = multiset_of ys"
bulwahn@27656
   486
  shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)"
bulwahn@27656
   487
proof -
bulwahn@27656
   488
  from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long") 
bulwahn@27656
   489
    by (simp add: sublist'_append)
bulwahn@27656
   490
  from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length)
bulwahn@27656
   491
  with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long") 
bulwahn@27656
   492
    by (simp add: sublist'_append)
bulwahn@27656
   493
  from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp
bulwahn@27656
   494
  moreover
bulwahn@27656
   495
  from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
bulwahn@27656
   496
    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
bulwahn@27656
   497
  moreover
bulwahn@27656
   498
  from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
bulwahn@27656
   499
    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
bulwahn@27656
   500
  moreover
bulwahn@27656
   501
  ultimately show ?thesis by (simp add: multiset_of_append)
bulwahn@27656
   502
qed
bulwahn@27656
   503
bulwahn@27656
   504
bulwahn@27656
   505
end