reorganised material on sublists
authoreberlm <eberlm@in.tum.de>
Mon May 29 09:14:15 2017 +0200 (23 months ago)
changeset 65956639eb3617a86
parent 65955 0616ba637b14
child 65957 558ba6b37f5c
child 65958 6338355b2a88
reorganised material on sublists
NEWS
src/Doc/Main/Main_Doc.thy
src/HOL/Codegenerator_Test/Candidates.thy
src/HOL/Enum.thy
src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
src/HOL/Imperative_HOL/ex/List_Sublist.thy
src/HOL/Imperative_HOL/ex/Subarray.thy
src/HOL/Library/Sublist.thy
src/HOL/Library/Sublist_Order.thy
src/HOL/Library/Subseq_Order.thy
src/HOL/List.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/ROOT
src/HOL/UNITY/Comp/AllocBase.thy
src/HOL/UNITY/Comp/AllocImpl.thy
     1.1 --- a/NEWS	Sun May 28 15:46:26 2017 +0200
     1.2 +++ b/NEWS	Mon May 29 09:14:15 2017 +0200
     1.3 @@ -73,6 +73,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* "sublist" from theory List renamed to "nths" in analogy with "nth".
     1.8 +"sublisteq" renamed to "subseq".  Minor INCOMPATIBILITY.
     1.9 +
    1.10  * Theories "GCD" and "Binomial" are already included in "Main" (instead
    1.11  of "Complex_Main").
    1.12  
     2.1 --- a/src/Doc/Main/Main_Doc.thy	Sun May 28 15:46:26 2017 +0200
     2.2 +++ b/src/Doc/Main/Main_Doc.thy	Mon May 29 09:14:15 2017 +0200
     2.3 @@ -552,6 +552,7 @@
     2.4  @{const List.map} & @{typeof List.map}\\
     2.5  @{const List.measures} & @{term_type_only List.measures "('a\<Rightarrow>nat)list\<Rightarrow>('a*'a)set"}\\
     2.6  @{const List.nth} & @{typeof List.nth}\\
     2.7 +@{const List.nths} & @{typeof List.nths}\\
     2.8  @{const List.remdups} & @{typeof List.remdups}\\
     2.9  @{const List.removeAll} & @{typeof List.removeAll}\\
    2.10  @{const List.remove1} & @{typeof List.remove1}\\
    2.11 @@ -560,10 +561,10 @@
    2.12  @{const List.rotate} & @{typeof List.rotate}\\
    2.13  @{const List.rotate1} & @{typeof List.rotate1}\\
    2.14  @{const List.set} & @{term_type_only List.set "'a list \<Rightarrow> 'a set"}\\
    2.15 +@{const List.shuffle} & @{typeof List.shuffle}\\
    2.16  @{const List.sort} & @{typeof List.sort}\\
    2.17  @{const List.sorted} & @{typeof List.sorted}\\
    2.18  @{const List.splice} & @{typeof List.splice}\\
    2.19 -@{const List.sublist} & @{typeof List.sublist}\\
    2.20  @{const List.take} & @{typeof List.take}\\
    2.21  @{const List.takeWhile} & @{typeof List.takeWhile}\\
    2.22  @{const List.tl} & @{typeof List.tl}\\
    2.23 @@ -656,4 +657,4 @@
    2.24  \<close>
    2.25  (*<*)
    2.26  end
    2.27 -(*>*)
    2.28 \ No newline at end of file
    2.29 +(*>*)
     3.1 --- a/src/HOL/Codegenerator_Test/Candidates.thy	Sun May 28 15:46:26 2017 +0200
     3.2 +++ b/src/HOL/Codegenerator_Test/Candidates.thy	Mon May 29 09:14:15 2017 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  imports
     3.5    Complex_Main
     3.6    "~~/src/HOL/Library/Library"
     3.7 -  "~~/src/HOL/Library/Sublist_Order"
     3.8 +  "~~/src/HOL/Library/Subseq_Order"
     3.9    "~~/src/HOL/Data_Structures/Tree_Map"
    3.10    "~~/src/HOL/Data_Structures/Tree_Set"
    3.11    "~~/src/HOL/Computational_Algebra/Computational_Algebra"
     4.1 --- a/src/HOL/Enum.thy	Sun May 28 15:46:26 2017 +0200
     4.2 +++ b/src/HOL/Enum.thy	Mon May 29 09:14:15 2017 +0200
     4.3 @@ -385,7 +385,7 @@
     4.4  begin
     4.5  
     4.6  definition
     4.7 -  "enum = map set (sublists enum)"
     4.8 +  "enum = map set (subseqs enum)"
     4.9  
    4.10  definition
    4.11    "enum_all P \<longleftrightarrow> (\<forall>A\<in>set enum. P (A::'a set))"
    4.12 @@ -394,7 +394,7 @@
    4.13    "enum_ex P \<longleftrightarrow> (\<exists>A\<in>set enum. P (A::'a set))"
    4.14  
    4.15  instance proof
    4.16 -qed (simp_all add: enum_set_def enum_all_set_def enum_ex_set_def sublists_powset distinct_set_sublists
    4.17 +qed (simp_all add: enum_set_def enum_all_set_def enum_ex_set_def subseqs_powset distinct_set_subseqs
    4.18    enum_distinct enum_UNIV)
    4.19  
    4.20  end
     5.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Sun May 28 15:46:26 2017 +0200
     5.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon May 29 09:14:15 2017 +0200
     5.3 @@ -533,7 +533,7 @@
     5.4          and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> Array.get h1 a ! p \<le> j"
     5.5          by (auto simp add: all_in_set_subarray_conv)
     5.6        from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
     5.7 -        length_remains 1(5) pivot mset_sublist [of l p "Array.get h1 a" "Array.get h2 a"]
     5.8 +        length_remains 1(5) pivot mset_nths [of l p "Array.get h1 a" "Array.get h2 a"]
     5.9        have multiset_partconds1: "mset (subarray l p a h2) = mset (subarray l p a h1)"
    5.10          unfolding Array.length_def subarray_def by (cases p, auto)
    5.11        with left_subarray_remains part_conds1 pivot_unchanged
    5.12 @@ -544,7 +544,7 @@
    5.13        have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
    5.14          by (auto simp add: subarray_eq_samelength_iff)
    5.15        from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
    5.16 -        length_remains 1(5) pivot mset_sublist [of "p + 1" "r + 1" "Array.get h2 a" "Array.get h' a"]
    5.17 +        length_remains 1(5) pivot mset_nths [of "p + 1" "r + 1" "Array.get h2 a" "Array.get h' a"]
    5.18        have multiset_partconds2: "mset (subarray (p + 1) (r + 1) a h') = mset (subarray (p + 1) (r + 1) a h2)"
    5.19          unfolding Array.length_def subarray_def by auto
    5.20        with right_subarray_remains part_conds2 pivot_unchanged
    5.21 @@ -556,8 +556,8 @@
    5.22          by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
    5.23        with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis
    5.24          unfolding subarray_def
    5.25 -        apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv)
    5.26 -        by (auto simp add: set_sublist' dest: order.trans [of _ "Array.get h' a ! p"])
    5.27 +        apply (auto simp add: sorted_append sorted_Cons all_in_set_nths'_conv)
    5.28 +        by (auto simp add: set_nths' dest: order.trans [of _ "Array.get h' a ! p"])
    5.29      }
    5.30      with True cr show ?thesis
    5.31        unfolding quicksort.simps [of a l r]
    5.32 @@ -575,7 +575,7 @@
    5.33    unfolding Array.length_def by simp
    5.34  next
    5.35    case False
    5.36 -  from quicksort_sorts [OF effect] False have "sorted (sublist' 0 (List.length (Array.get h a)) (Array.get h' a))"
    5.37 +  from quicksort_sorts [OF effect] False have "sorted (nths' 0 (List.length (Array.get h a)) (Array.get h' a))"
    5.38      unfolding Array.length_def subarray_def by auto
    5.39    with length_remains[OF effect] have "sorted (Array.get h' a)"
    5.40      unfolding Array.length_def by simp
     6.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Sun May 28 15:46:26 2017 +0200
     6.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Mon May 29 09:14:15 2017 +0200
     6.3 @@ -99,7 +99,7 @@
     6.4    } 
     6.5    with assms(2) rev_length[OF assms(1)] show ?thesis
     6.6    unfolding subarray_def Array.length_def
     6.7 -  by (auto simp add: length_sublist' rev_nth min_def nth_sublist' intro!: nth_equalityI)
     6.8 +  by (auto simp add: length_nths' rev_nth min_def nth_nths' intro!: nth_equalityI)
     6.9  qed
    6.10  
    6.11  lemma rev2_rev: 
     7.1 --- a/src/HOL/Imperative_HOL/ex/List_Sublist.thy	Sun May 28 15:46:26 2017 +0200
     7.2 +++ b/src/HOL/Imperative_HOL/ex/List_Sublist.thy	Mon May 29 09:14:15 2017 +0200
     7.3 @@ -8,10 +8,10 @@
     7.4  imports "~~/src/HOL/Library/Multiset"
     7.5  begin
     7.6  
     7.7 -lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" 
     7.8 +lemma nths_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> nths xs {i..<j} @ nths xs {j..<k} = nths xs {i..<k}" 
     7.9  apply (induct xs arbitrary: i j k)
    7.10  apply simp
    7.11 -apply (simp only: sublist_Cons)
    7.12 +apply (simp only: nths_Cons)
    7.13  apply simp
    7.14  apply safe
    7.15  apply simp
    7.16 @@ -42,27 +42,27 @@
    7.17  apply fastforce
    7.18  done
    7.19  
    7.20 -lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds"
    7.21 +lemma nths_update1: "i \<notin> inds \<Longrightarrow> nths (xs[i := v]) inds = nths xs inds"
    7.22  apply (induct xs arbitrary: i inds)
    7.23  apply simp
    7.24  apply (case_tac i)
    7.25 -apply (simp add: sublist_Cons)
    7.26 -apply (simp add: sublist_Cons)
    7.27 +apply (simp add: nths_Cons)
    7.28 +apply (simp add: nths_Cons)
    7.29  done
    7.30  
    7.31 -lemma sublist_update2: "i \<in> inds \<Longrightarrow> sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \<in> inds. k < i}):= v]"
    7.32 +lemma nths_update2: "i \<in> inds \<Longrightarrow> nths (xs[i := v]) inds = (nths xs inds)[(card {k \<in> inds. k < i}):= v]"
    7.33  proof (induct xs arbitrary: i inds)
    7.34    case Nil thus ?case by simp
    7.35  next
    7.36    case (Cons x xs)
    7.37    thus ?case
    7.38    proof (cases i)
    7.39 -    case 0 with Cons show ?thesis by (simp add: sublist_Cons)
    7.40 +    case 0 with Cons show ?thesis by (simp add: nths_Cons)
    7.41    next
    7.42      case (Suc i')
    7.43      with Cons show ?thesis
    7.44        apply simp
    7.45 -      apply (simp add: sublist_Cons)
    7.46 +      apply (simp add: nths_Cons)
    7.47        apply auto
    7.48        apply (auto simp add: nat.split)
    7.49        apply (simp add: card_less_Suc[symmetric])
    7.50 @@ -71,82 +71,82 @@
    7.51    qed
    7.52  qed
    7.53  
    7.54 -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)"
    7.55 -by (simp add: sublist_update1 sublist_update2)
    7.56 +lemma nths_update: "nths (xs[i := v]) inds = (if i \<in> inds then (nths xs inds)[(card {k \<in> inds. k < i}) := v] else nths xs inds)"
    7.57 +by (simp add: nths_update1 nths_update2)
    7.58  
    7.59 -lemma sublist_take: "sublist xs {j. j < m} = take m xs"
    7.60 +lemma nths_take: "nths xs {j. j < m} = take m xs"
    7.61  apply (induct xs arbitrary: m)
    7.62  apply simp
    7.63  apply (case_tac m)
    7.64  apply simp
    7.65 -apply (simp add: sublist_Cons)
    7.66 +apply (simp add: nths_Cons)
    7.67  done
    7.68  
    7.69 -lemma sublist_take': "sublist xs {0..<m} = take m xs"
    7.70 +lemma nths_take': "nths xs {0..<m} = take m xs"
    7.71  apply (induct xs arbitrary: m)
    7.72  apply simp
    7.73  apply (case_tac m)
    7.74  apply simp
    7.75 -apply (simp add: sublist_Cons sublist_take)
    7.76 +apply (simp add: nths_Cons nths_take)
    7.77  done
    7.78  
    7.79 -lemma sublist_all[simp]: "sublist xs {j. j < length xs} = xs"
    7.80 +lemma nths_all[simp]: "nths xs {j. j < length xs} = xs"
    7.81  apply (induct xs)
    7.82  apply simp
    7.83 -apply (simp add: sublist_Cons)
    7.84 +apply (simp add: nths_Cons)
    7.85  done
    7.86  
    7.87 -lemma sublist_all'[simp]: "sublist xs {0..<length xs} = xs"
    7.88 +lemma nths_all'[simp]: "nths xs {0..<length xs} = xs"
    7.89  apply (induct xs)
    7.90  apply simp
    7.91 -apply (simp add: sublist_Cons)
    7.92 +apply (simp add: nths_Cons)
    7.93  done
    7.94  
    7.95 -lemma sublist_single: "a < length xs \<Longrightarrow> sublist xs {a} = [xs ! a]"
    7.96 +lemma nths_single: "a < length xs \<Longrightarrow> nths xs {a} = [xs ! a]"
    7.97  apply (induct xs arbitrary: a)
    7.98  apply simp
    7.99  apply(case_tac aa)
   7.100  apply simp
   7.101 -apply (simp add: sublist_Cons)
   7.102 +apply (simp add: nths_Cons)
   7.103  apply simp
   7.104 -apply (simp add: sublist_Cons)
   7.105 +apply (simp add: nths_Cons)
   7.106  done
   7.107  
   7.108 -lemma sublist_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> sublist xs inds = []" 
   7.109 +lemma nths_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> nths xs inds = []" 
   7.110  apply (induct xs arbitrary: inds)
   7.111  apply simp
   7.112 -apply (simp add: sublist_Cons)
   7.113 +apply (simp add: nths_Cons)
   7.114  apply auto
   7.115  apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   7.116  apply auto
   7.117  done
   7.118  
   7.119 -lemma sublist_Nil': "sublist xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs"
   7.120 +lemma nths_Nil': "nths xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs"
   7.121  apply (induct xs arbitrary: inds)
   7.122  apply simp
   7.123 -apply (simp add: sublist_Cons)
   7.124 +apply (simp add: nths_Cons)
   7.125  apply (auto split: if_splits)
   7.126  apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   7.127  apply (case_tac x, auto)
   7.128  done
   7.129  
   7.130 -lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)"
   7.131 +lemma nths_Nil[simp]: "(nths xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)"
   7.132  apply (induct xs arbitrary: inds)
   7.133  apply simp
   7.134 -apply (simp add: sublist_Cons)
   7.135 +apply (simp add: nths_Cons)
   7.136  apply auto
   7.137  apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   7.138  apply (case_tac x, auto)
   7.139  done
   7.140  
   7.141 -lemma sublist_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; sublist xs inds = sublist ys inds \<rbrakk> \<Longrightarrow> sublist xs inds' = sublist ys inds'"
   7.142 +lemma nths_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; nths xs inds = nths ys inds \<rbrakk> \<Longrightarrow> nths xs inds' = nths ys inds'"
   7.143  apply (induct xs arbitrary: ys inds inds')
   7.144  apply simp
   7.145  apply (drule sym, rule sym)
   7.146 -apply (simp add: sublist_Nil, fastforce)
   7.147 +apply (simp add: nths_Nil, fastforce)
   7.148  apply (case_tac ys)
   7.149 -apply (simp add: sublist_Nil, fastforce)
   7.150 -apply (auto simp add: sublist_Cons)
   7.151 +apply (simp add: nths_Nil, fastforce)
   7.152 +apply (auto simp add: nths_Cons)
   7.153  apply (erule_tac x="list" in meta_allE)
   7.154  apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   7.155  apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
   7.156 @@ -157,13 +157,13 @@
   7.157  apply fastforce
   7.158  done
   7.159  
   7.160 -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"
   7.161 +lemma nths_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> nths xs inds = nths ys inds"
   7.162  apply (induct xs arbitrary: ys inds)
   7.163  apply simp
   7.164 -apply (rule sym, simp add: sublist_Nil)
   7.165 +apply (rule sym, simp add: nths_Nil)
   7.166  apply (case_tac ys)
   7.167 -apply (simp add: sublist_Nil)
   7.168 -apply (auto simp add: sublist_Cons)
   7.169 +apply (simp add: nths_Nil)
   7.170 +apply (auto simp add: nths_Cons)
   7.171  apply (erule_tac x="list" in meta_allE)
   7.172  apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   7.173  apply fastforce
   7.174 @@ -172,64 +172,64 @@
   7.175  apply fastforce
   7.176  done
   7.177  
   7.178 -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"
   7.179 -by (rule sublist_eq, auto)
   7.180 +lemma nths_eq_samelength: "\<lbrakk> length xs = length ys; \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> nths xs inds = nths ys inds"
   7.181 +by (rule nths_eq, auto)
   7.182  
   7.183 -lemma sublist_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist xs inds = sublist ys inds) = (\<forall>i \<in> inds. xs ! i = ys ! i)"
   7.184 +lemma nths_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (nths xs inds = nths ys inds) = (\<forall>i \<in> inds. xs ! i = ys ! i)"
   7.185  apply (induct xs arbitrary: ys inds)
   7.186  apply simp
   7.187 -apply (rule sym, simp add: sublist_Nil)
   7.188 +apply (rule sym, simp add: nths_Nil)
   7.189  apply (case_tac ys)
   7.190 -apply (simp add: sublist_Nil)
   7.191 -apply (auto simp add: sublist_Cons)
   7.192 +apply (simp add: nths_Nil)
   7.193 +apply (auto simp add: nths_Cons)
   7.194  apply (case_tac i)
   7.195  apply auto
   7.196  apply (case_tac i)
   7.197  apply auto
   7.198  done
   7.199  
   7.200 -section \<open>Another sublist function\<close>
   7.201 +section \<open>Another nths function\<close>
   7.202  
   7.203 -function sublist' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
   7.204 +function nths' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
   7.205  where
   7.206 -  "sublist' n m [] = []"
   7.207 -| "sublist' n 0 xs = []"
   7.208 -| "sublist' 0 (Suc m) (x#xs) = (x#sublist' 0 m xs)"
   7.209 -| "sublist' (Suc n) (Suc m) (x#xs) = sublist' n m xs"
   7.210 +  "nths' n m [] = []"
   7.211 +| "nths' n 0 xs = []"
   7.212 +| "nths' 0 (Suc m) (x#xs) = (x#nths' 0 m xs)"
   7.213 +| "nths' (Suc n) (Suc m) (x#xs) = nths' n m xs"
   7.214  by pat_completeness auto
   7.215  termination by lexicographic_order
   7.216  
   7.217 -subsection \<open>Proving equivalence to the other sublist command\<close>
   7.218 +subsection \<open>Proving equivalence to the other nths command\<close>
   7.219  
   7.220 -lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \<le> j \<and> j < m}"
   7.221 +lemma nths'_nths: "nths' n m xs = nths xs {j. n \<le> j \<and> j < m}"
   7.222  apply (induct xs arbitrary: n m)
   7.223  apply simp
   7.224  apply (case_tac n)
   7.225  apply (case_tac m)
   7.226  apply simp
   7.227 -apply (simp add: sublist_Cons)
   7.228 +apply (simp add: nths_Cons)
   7.229  apply (case_tac m)
   7.230  apply simp
   7.231 -apply (simp add: sublist_Cons)
   7.232 +apply (simp add: nths_Cons)
   7.233  done
   7.234  
   7.235  
   7.236 -lemma "sublist' n m xs = sublist xs {n..<m}"
   7.237 +lemma "nths' n m xs = nths xs {n..<m}"
   7.238  apply (induct xs arbitrary: n m)
   7.239  apply simp
   7.240  apply (case_tac n, case_tac m)
   7.241  apply simp
   7.242  apply simp
   7.243 -apply (simp add: sublist_take')
   7.244 +apply (simp add: nths_take')
   7.245  apply (case_tac m)
   7.246  apply simp
   7.247 -apply (simp add: sublist_Cons sublist'_sublist)
   7.248 +apply (simp add: nths_Cons nths'_nths)
   7.249  done
   7.250  
   7.251  
   7.252  subsection \<open>Showing equivalence to use of drop and take for definition\<close>
   7.253  
   7.254 -lemma "sublist' n m xs = take (m - n) (drop n xs)"
   7.255 +lemma "nths' n m xs = take (m - n) (drop n xs)"
   7.256  apply (induct xs arbitrary: n m)
   7.257  apply simp
   7.258  apply (case_tac m)
   7.259 @@ -239,25 +239,25 @@
   7.260  apply simp
   7.261  done
   7.262  
   7.263 -subsection \<open>General lemma about sublist\<close>
   7.264 +subsection \<open>General lemma about nths\<close>
   7.265  
   7.266 -lemma sublist'_Nil[simp]: "sublist' i j [] = []"
   7.267 +lemma nths'_Nil[simp]: "nths' i j [] = []"
   7.268  by simp
   7.269  
   7.270 -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)"
   7.271 +lemma nths'_Cons[simp]: "nths' i (Suc j) (x#xs) = (case i of 0 \<Rightarrow> (x # nths' 0 j xs) | Suc i' \<Rightarrow>  nths' i' j xs)"
   7.272  by (cases i) auto
   7.273  
   7.274 -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))"
   7.275 +lemma nths'_Cons2[simp]: "nths' i j (x#xs) = (if (j = 0) then [] else ((if (i = 0) then [x] else []) @ nths' (i - 1) (j - 1) xs))"
   7.276  apply (cases j)
   7.277  apply auto
   7.278  apply (cases i)
   7.279  apply auto
   7.280  done
   7.281  
   7.282 -lemma sublist_n_0: "sublist' n 0 xs = []"
   7.283 +lemma nths_n_0: "nths' n 0 xs = []"
   7.284  by (induct xs, auto)
   7.285  
   7.286 -lemma sublist'_Nil': "n \<ge> m \<Longrightarrow> sublist' n m xs = []"
   7.287 +lemma nths'_Nil': "n \<ge> m \<Longrightarrow> nths' n m xs = []"
   7.288  apply (induct xs arbitrary: n m)
   7.289  apply simp
   7.290  apply (case_tac m)
   7.291 @@ -267,7 +267,7 @@
   7.292  apply simp
   7.293  done
   7.294  
   7.295 -lemma sublist'_Nil2: "n \<ge> length xs \<Longrightarrow> sublist' n m xs = []"
   7.296 +lemma nths'_Nil2: "n \<ge> length xs \<Longrightarrow> nths' n m xs = []"
   7.297  apply (induct xs arbitrary: n m)
   7.298  apply simp
   7.299  apply (case_tac m)
   7.300 @@ -277,7 +277,7 @@
   7.301  apply simp
   7.302  done
   7.303  
   7.304 -lemma sublist'_Nil3: "(sublist' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
   7.305 +lemma nths'_Nil3: "(nths' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
   7.306  apply (induct xs arbitrary: n m)
   7.307  apply simp
   7.308  apply (case_tac m)
   7.309 @@ -287,7 +287,7 @@
   7.310  apply simp
   7.311  done
   7.312  
   7.313 -lemma sublist'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> sublist' n m xs \<noteq> []"
   7.314 +lemma nths'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> nths' n m xs \<noteq> []"
   7.315  apply (induct xs arbitrary: n m)
   7.316  apply simp
   7.317  apply (case_tac m)
   7.318 @@ -297,16 +297,16 @@
   7.319  apply simp
   7.320  done
   7.321  
   7.322 -lemma sublist'_single: "n < length xs \<Longrightarrow> sublist' n (Suc n) xs = [xs ! n]"
   7.323 +lemma nths'_single: "n < length xs \<Longrightarrow> nths' n (Suc n) xs = [xs ! n]"
   7.324  apply (induct xs arbitrary: n)
   7.325  apply simp
   7.326  apply simp
   7.327  apply (case_tac n)
   7.328 -apply (simp add: sublist_n_0)
   7.329 +apply (simp add: nths_n_0)
   7.330  apply simp
   7.331  done
   7.332  
   7.333 -lemma sublist'_update1: "i \<ge> m \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
   7.334 +lemma nths'_update1: "i \<ge> m \<Longrightarrow> nths' n m (xs[i:=v]) = nths' n m xs"
   7.335  apply (induct xs arbitrary: n m i)
   7.336  apply simp
   7.337  apply simp
   7.338 @@ -315,7 +315,7 @@
   7.339  apply simp
   7.340  done
   7.341  
   7.342 -lemma sublist'_update2: "i < n \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
   7.343 +lemma nths'_update2: "i < n \<Longrightarrow> nths' n m (xs[i:=v]) = nths' n m xs"
   7.344  apply (induct xs arbitrary: n m i)
   7.345  apply simp
   7.346  apply simp
   7.347 @@ -324,7 +324,7 @@
   7.348  apply simp
   7.349  done
   7.350  
   7.351 -lemma sublist'_update3: "\<lbrakk>n \<le> i; i < m\<rbrakk> \<Longrightarrow> sublist' n m (xs[i := v]) = (sublist' n m xs)[i - n := v]"
   7.352 +lemma nths'_update3: "\<lbrakk>n \<le> i; i < m\<rbrakk> \<Longrightarrow> nths' n m (xs[i := v]) = (nths' n m xs)[i - n := v]"
   7.353  proof (induct xs arbitrary: n m i)
   7.354    case Nil thus ?case by auto
   7.355  next
   7.356 @@ -339,14 +339,14 @@
   7.357      done
   7.358  qed
   7.359  
   7.360 -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"
   7.361 +lemma "\<lbrakk> nths' i j xs = nths' i j ys; n \<ge> i; m \<le> j \<rbrakk> \<Longrightarrow> nths' n m xs = nths' n m ys"
   7.362  proof (induct xs arbitrary: i j ys n m)
   7.363    case Nil
   7.364    thus ?case
   7.365      apply -
   7.366      apply (rule sym, drule sym)
   7.367 -    apply (simp add: sublist'_Nil)
   7.368 -    apply (simp add: sublist'_Nil3)
   7.369 +    apply (simp add: nths'_Nil)
   7.370 +    apply (simp add: nths'_Nil3)
   7.371      apply arith
   7.372      done
   7.373  next
   7.374 @@ -354,7 +354,7 @@
   7.375    note c = this
   7.376    thus ?case
   7.377    proof (cases m)
   7.378 -    case 0 thus ?thesis by (simp add: sublist_n_0)
   7.379 +    case 0 thus ?thesis by (simp add: nths_n_0)
   7.380    next
   7.381      case (Suc m')
   7.382      note a = this
   7.383 @@ -363,7 +363,7 @@
   7.384        case 0 note b = this
   7.385        show ?thesis
   7.386        proof (cases ys)
   7.387 -        case Nil  with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3)
   7.388 +        case Nil  with a b Cons.prems show ?thesis by (simp add: nths'_Nil3)
   7.389        next
   7.390          case (Cons y ys)
   7.391          show ?thesis
   7.392 @@ -380,7 +380,7 @@
   7.393        case (Suc n')
   7.394        show ?thesis
   7.395        proof (cases ys)
   7.396 -        case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3)
   7.397 +        case Nil with Suc a Cons.prems show ?thesis by (auto simp add: nths'_Nil3)
   7.398        next
   7.399          case (Cons y ys) with Suc a Cons.prems show ?thesis
   7.400            apply -
   7.401 @@ -404,10 +404,10 @@
   7.402    qed
   7.403  qed
   7.404  
   7.405 -lemma length_sublist': "j \<le> length xs \<Longrightarrow> length (sublist' i j xs) = j - i"
   7.406 +lemma length_nths': "j \<le> length xs \<Longrightarrow> length (nths' i j xs) = j - i"
   7.407  by (induct xs arbitrary: i j, auto)
   7.408  
   7.409 -lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs"
   7.410 +lemma nths'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> nths' i j xs = xs ! i # nths' (Suc i) j xs"
   7.411  apply (induct xs arbitrary: i j)
   7.412  apply simp
   7.413  apply (case_tac j)
   7.414 @@ -417,14 +417,14 @@
   7.415  apply simp
   7.416  done
   7.417  
   7.418 -lemma sublist'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]"
   7.419 +lemma nths'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> nths' i j xs = nths' i (j - 1) xs @ [xs ! (j - 1)]"
   7.420  apply (induct xs arbitrary: i j)
   7.421  apply simp
   7.422  apply simp
   7.423  done
   7.424  
   7.425  (* suffices that j \<le> length xs and length ys *) 
   7.426 -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')"
   7.427 +lemma nths'_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (nths' i j xs  = nths' i j ys) = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> xs ! i' = ys ! i')"
   7.428  proof (induct xs arbitrary: ys i j)
   7.429    case Nil thus ?case by simp
   7.430  next
   7.431 @@ -442,54 +442,54 @@
   7.432      done
   7.433  qed
   7.434  
   7.435 -lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs"
   7.436 +lemma nths'_all[simp]: "nths' 0 (length xs) xs = xs"
   7.437  by (induct xs, auto)
   7.438  
   7.439 -lemma sublist'_sublist': "sublist' n m (sublist' i j xs) = sublist' (i + n) (min (i + m) j) xs" 
   7.440 +lemma nths'_nths': "nths' n m (nths' i j xs) = nths' (i + n) (min (i + m) j) xs" 
   7.441  by (induct xs arbitrary: i j n m) (auto simp add: min_diff)
   7.442  
   7.443 -lemma sublist'_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow>(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs"
   7.444 +lemma nths'_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow>(nths' i j xs) @ (nths' j k xs) = nths' i k xs"
   7.445  by (induct xs arbitrary: i j k) auto
   7.446  
   7.447 -lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
   7.448 +lemma nth_nths': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (nths' i j xs) ! k = xs ! (i + k)"
   7.449  apply (induct xs arbitrary: i j k)
   7.450  apply simp
   7.451  apply (case_tac k)
   7.452  apply auto
   7.453  done
   7.454  
   7.455 -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}"
   7.456 -apply (simp add: sublist'_sublist)
   7.457 -apply (simp add: set_sublist)
   7.458 +lemma set_nths': "set (nths' i j xs) = {x. \<exists>k. i \<le> k \<and> k < j \<and> k < List.length xs \<and> x = xs ! k}"
   7.459 +apply (simp add: nths'_nths)
   7.460 +apply (simp add: set_nths)
   7.461  apply auto
   7.462  done
   7.463  
   7.464 -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))"
   7.465 -unfolding set_sublist' by blast
   7.466 +lemma all_in_set_nths'_conv: "(\<forall>j. j \<in> set (nths' l r xs) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
   7.467 +unfolding set_nths' by blast
   7.468  
   7.469 -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))"
   7.470 -unfolding set_sublist' by blast
   7.471 +lemma ball_in_set_nths'_conv: "(\<forall>j \<in> set (nths' l r xs). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
   7.472 +unfolding set_nths' by blast
   7.473  
   7.474  
   7.475 -lemma mset_sublist:
   7.476 +lemma mset_nths:
   7.477  assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
   7.478  assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
   7.479  assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
   7.480  assumes multiset: "mset xs = mset ys"
   7.481 -  shows "mset (sublist' l r xs) = mset (sublist' l r ys)"
   7.482 +  shows "mset (nths' l r xs) = mset (nths' l r ys)"
   7.483  proof -
   7.484 -  from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long") 
   7.485 -    by (simp add: sublist'_append)
   7.486 +  from l_r have xs_def: "xs = (nths' 0 l xs) @ (nths' l r xs) @ (nths' r (List.length xs) xs)" (is "_ = ?xs_long") 
   7.487 +    by (simp add: nths'_append)
   7.488    from multiset have length_eq: "List.length xs = List.length ys" by (rule mset_eq_length)
   7.489 -  with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long") 
   7.490 -    by (simp add: sublist'_append)
   7.491 +  with l_r have ys_def: "ys = (nths' 0 l ys) @ (nths' l r ys) @ (nths' r (List.length ys) ys)" (is "_ = ?ys_long") 
   7.492 +    by (simp add: nths'_append)
   7.493    from xs_def ys_def multiset have "mset ?xs_long = mset ?ys_long" by simp
   7.494    moreover
   7.495 -  from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
   7.496 -    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
   7.497 +  from left l_r length_eq have "nths' 0 l xs = nths' 0 l ys"
   7.498 +    by (auto simp add: length_nths' nth_nths' intro!: nth_equalityI)
   7.499    moreover
   7.500 -  from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
   7.501 -    by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
   7.502 +  from right l_r length_eq have "nths' r (List.length xs) xs = nths' r (List.length ys) ys"
   7.503 +    by (auto simp add: length_nths' nth_nths' intro!: nth_equalityI)
   7.504    ultimately show ?thesis by (simp add: mset_append)
   7.505  qed
   7.506  
     8.1 --- a/src/HOL/Imperative_HOL/ex/Subarray.thy	Sun May 28 15:46:26 2017 +0200
     8.2 +++ b/src/HOL/Imperative_HOL/ex/Subarray.thy	Mon May 29 09:14:15 2017 +0200
     8.3 @@ -9,63 +9,63 @@
     8.4  begin
     8.5  
     8.6  definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where
     8.7 -  "subarray n m a h \<equiv> sublist' n m (Array.get h a)"
     8.8 +  "subarray n m a h \<equiv> nths' n m (Array.get h a)"
     8.9  
    8.10  lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
    8.11  apply (simp add: subarray_def Array.update_def)
    8.12 -apply (simp add: sublist'_update1)
    8.13 +apply (simp add: nths'_update1)
    8.14  done
    8.15  
    8.16  lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
    8.17  apply (simp add: subarray_def Array.update_def)
    8.18 -apply (subst sublist'_update2)
    8.19 +apply (subst nths'_update2)
    8.20  apply fastforce
    8.21  apply simp
    8.22  done
    8.23  
    8.24  lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h[i - n := v]"
    8.25  unfolding subarray_def Array.update_def
    8.26 -by (simp add: sublist'_update3)
    8.27 +by (simp add: nths'_update3)
    8.28  
    8.29  lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
    8.30 -by (simp add: subarray_def sublist'_Nil')
    8.31 +by (simp add: subarray_def nths'_Nil')
    8.32  
    8.33  lemma subarray_single: "\<lbrakk> n < Array.length h a \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [Array.get h a ! n]" 
    8.34 -by (simp add: subarray_def length_def sublist'_single)
    8.35 +by (simp add: subarray_def length_def nths'_single)
    8.36  
    8.37  lemma length_subarray: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray n m a h) = m - n"
    8.38 -by (simp add: subarray_def length_def length_sublist')
    8.39 +by (simp add: subarray_def length_def length_nths')
    8.40  
    8.41  lemma length_subarray_0: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray 0 m a h) = m"
    8.42  by (simp add: length_subarray)
    8.43  
    8.44  lemma subarray_nth_array_Cons: "\<lbrakk> i < Array.length h a; i < j \<rbrakk> \<Longrightarrow> (Array.get h a ! i) # subarray (Suc i) j a h = subarray i j a h"
    8.45  unfolding Array.length_def subarray_def
    8.46 -by (simp add: sublist'_front)
    8.47 +by (simp add: nths'_front)
    8.48  
    8.49  lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Array.length h a\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [Array.get h a ! (j - 1)]"
    8.50  unfolding Array.length_def subarray_def
    8.51 -by (simp add: sublist'_back)
    8.52 +by (simp add: nths'_back)
    8.53  
    8.54  lemma subarray_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow> subarray i j a h @ subarray j k a h = subarray i k a h"
    8.55  unfolding subarray_def
    8.56 -by (simp add: sublist'_append)
    8.57 +by (simp add: nths'_append)
    8.58  
    8.59  lemma subarray_all: "subarray 0 (Array.length h a) a h = Array.get h a"
    8.60  unfolding Array.length_def subarray_def
    8.61 -by (simp add: sublist'_all)
    8.62 +by (simp add: nths'_all)
    8.63  
    8.64  lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Array.length h a \<rbrakk> \<Longrightarrow> subarray i j a h ! k = Array.get h a ! (i + k)"
    8.65  unfolding Array.length_def subarray_def
    8.66 -by (simp add: nth_sublist')
    8.67 +by (simp add: nth_nths')
    8.68  
    8.69  lemma subarray_eq_samelength_iff: "Array.length h a = Array.length h' a \<Longrightarrow> (subarray i j a h = subarray i j a h') = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> Array.get h a ! i' = Array.get h' a ! i')"
    8.70 -unfolding Array.length_def subarray_def by (rule sublist'_eq_samelength_iff)
    8.71 +unfolding Array.length_def subarray_def by (rule nths'_eq_samelength_iff)
    8.72  
    8.73  lemma all_in_set_subarray_conv: "(\<forall>j. j \<in> set (subarray l r a h) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length h a \<longrightarrow> P (Array.get h a ! k))"
    8.74 -unfolding subarray_def Array.length_def by (rule all_in_set_sublist'_conv)
    8.75 +unfolding subarray_def Array.length_def by (rule all_in_set_nths'_conv)
    8.76  
    8.77  lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length h a \<longrightarrow> P (Array.get h a ! k))"
    8.78 -unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv)
    8.79 +unfolding subarray_def Array.length_def by (rule ball_in_set_nths'_conv)
    8.80  
    8.81  end
     9.1 --- a/src/HOL/Library/Sublist.thy	Sun May 28 15:46:26 2017 +0200
     9.2 +++ b/src/HOL/Library/Sublist.thy	Mon May 29 09:14:15 2017 +0200
     9.3 @@ -1,6 +1,7 @@
     9.4  (*  Title:      HOL/Library/Sublist.thy
     9.5 -    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     9.6 +    Author:     Tobias Nipkow and Markus Wenzel, TU München
     9.7      Author:     Christian Sternagel, JAIST
     9.8 +    Author:     Manuel Eberl, TU München
     9.9  *)
    9.10  
    9.11  section \<open>List prefixes, suffixes, and homeomorphic embedding\<close>
    9.12 @@ -214,7 +215,7 @@
    9.13  
    9.14  subsection \<open>Prefixes\<close>
    9.15  
    9.16 -fun prefixes where
    9.17 +primrec prefixes where
    9.18  "prefixes [] = [[]]" |
    9.19  "prefixes (x#xs) = [] # map (op # x) (prefixes xs)"
    9.20  
    9.21 @@ -700,7 +701,7 @@
    9.22  
    9.23  subsection \<open>Suffixes\<close>
    9.24  
    9.25 -fun suffixes where
    9.26 +primrec suffixes where
    9.27    "suffixes [] = [[]]"
    9.28  | "suffixes (x#xs) = suffixes xs @ [x # xs]"
    9.29  
    9.30 @@ -919,49 +920,48 @@
    9.31    "list_emb P (x#xs) [] \<longleftrightarrow> False"
    9.32    "list_emb P (x#xs) (y#ys) \<longleftrightarrow> (if P x y then list_emb P xs ys else list_emb P (x#xs) ys)"
    9.33    by simp_all
    9.34 -  
    9.35 +    
    9.36  
    9.37 -
    9.38 -subsection \<open>Sublists (special case of homeomorphic embedding)\<close>
    9.39 +subsection \<open>Subsequences (special case of homeomorphic embedding)\<close>
    9.40  
    9.41 -abbreviation sublisteq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    9.42 -  where "sublisteq xs ys \<equiv> list_emb (op =) xs ys"
    9.43 +abbreviation subseq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    9.44 +  where "subseq xs ys \<equiv> list_emb (op =) xs ys"
    9.45    
    9.46 -definition strict_sublist where "strict_sublist xs ys \<longleftrightarrow> xs \<noteq> ys \<and> sublisteq xs ys"
    9.47 +definition strict_subseq where "strict_subseq xs ys \<longleftrightarrow> xs \<noteq> ys \<and> subseq xs ys"
    9.48  
    9.49 -lemma sublisteq_Cons2: "sublisteq xs ys \<Longrightarrow> sublisteq (x#xs) (x#ys)" by auto
    9.50 +lemma subseq_Cons2: "subseq xs ys \<Longrightarrow> subseq (x#xs) (x#ys)" by auto
    9.51  
    9.52 -lemma sublisteq_same_length:
    9.53 -  assumes "sublisteq xs ys" and "length xs = length ys" shows "xs = ys"
    9.54 +lemma subseq_same_length:
    9.55 +  assumes "subseq xs ys" and "length xs = length ys" shows "xs = ys"
    9.56    using assms by (induct) (auto dest: list_emb_length)
    9.57  
    9.58 -lemma not_sublisteq_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sublisteq xs ys"
    9.59 +lemma not_subseq_length [simp]: "length ys < length xs \<Longrightarrow> \<not> subseq xs ys"
    9.60    by (metis list_emb_length linorder_not_less)
    9.61  
    9.62 -lemma sublisteq_Cons': "sublisteq (x#xs) ys \<Longrightarrow> sublisteq xs ys"
    9.63 +lemma subseq_Cons': "subseq (x#xs) ys \<Longrightarrow> subseq xs ys"
    9.64    by (induct xs, simp, blast dest: list_emb_ConsD)
    9.65  
    9.66 -lemma sublisteq_Cons2':
    9.67 -  assumes "sublisteq (x#xs) (x#ys)" shows "sublisteq xs ys"
    9.68 -  using assms by (cases) (rule sublisteq_Cons')
    9.69 +lemma subseq_Cons2':
    9.70 +  assumes "subseq (x#xs) (x#ys)" shows "subseq xs ys"
    9.71 +  using assms by (cases) (rule subseq_Cons')
    9.72  
    9.73 -lemma sublisteq_Cons2_neq:
    9.74 -  assumes "sublisteq (x#xs) (y#ys)"
    9.75 -  shows "x \<noteq> y \<Longrightarrow> sublisteq (x#xs) ys"
    9.76 +lemma subseq_Cons2_neq:
    9.77 +  assumes "subseq (x#xs) (y#ys)"
    9.78 +  shows "x \<noteq> y \<Longrightarrow> subseq (x#xs) ys"
    9.79    using assms by (cases) auto
    9.80  
    9.81 -lemma sublisteq_Cons2_iff [simp]:
    9.82 -  "sublisteq (x#xs) (y#ys) = (if x = y then sublisteq xs ys else sublisteq (x#xs) ys)"
    9.83 +lemma subseq_Cons2_iff [simp]:
    9.84 +  "subseq (x#xs) (y#ys) = (if x = y then subseq xs ys else subseq (x#xs) ys)"
    9.85    by simp
    9.86  
    9.87 -lemma sublisteq_append': "sublisteq (zs @ xs) (zs @ ys) \<longleftrightarrow> sublisteq xs ys"
    9.88 +lemma subseq_append': "subseq (zs @ xs) (zs @ ys) \<longleftrightarrow> subseq xs ys"
    9.89    by (induct zs) simp_all
    9.90      
    9.91 -interpretation sublist_order: order sublisteq strict_sublist
    9.92 +interpretation subseq_order: order subseq strict_subseq
    9.93  proof
    9.94    fix xs ys :: "'a list"
    9.95    {
    9.96 -    assume "sublisteq xs ys" and "sublisteq ys xs"
    9.97 +    assume "subseq xs ys" and "subseq ys xs"
    9.98      thus "xs = ys"
    9.99      proof (induct)
   9.100        case list_emb_Nil
   9.101 @@ -971,34 +971,34 @@
   9.102        thus ?case by simp
   9.103      next
   9.104        case list_emb_Cons
   9.105 -      hence False using sublisteq_Cons' by fastforce
   9.106 +      hence False using subseq_Cons' by fastforce
   9.107        thus ?case ..
   9.108      qed
   9.109    }
   9.110 -  thus "strict_sublist xs ys \<longleftrightarrow> (sublisteq xs ys \<and> \<not>sublisteq ys xs)"
   9.111 -    by (auto simp: strict_sublist_def)
   9.112 +  thus "strict_subseq xs ys \<longleftrightarrow> (subseq xs ys \<and> \<not>subseq ys xs)"
   9.113 +    by (auto simp: strict_subseq_def)
   9.114  qed (auto simp: list_emb_refl intro: list_emb_trans)
   9.115  
   9.116 -lemma in_set_sublists [simp]: "xs \<in> set (sublists ys) \<longleftrightarrow> sublisteq xs ys"
   9.117 +lemma in_set_subseqs [simp]: "xs \<in> set (subseqs ys) \<longleftrightarrow> subseq xs ys"
   9.118  proof
   9.119 -  assume "xs \<in> set (sublists ys)"
   9.120 -  thus "sublisteq xs ys"
   9.121 +  assume "xs \<in> set (subseqs ys)"
   9.122 +  thus "subseq xs ys"
   9.123      by (induction ys arbitrary: xs) (auto simp: Let_def)
   9.124  next
   9.125 -  have [simp]: "[] \<in> set (sublists ys)" for ys :: "'a list" 
   9.126 +  have [simp]: "[] \<in> set (subseqs ys)" for ys :: "'a list" 
   9.127      by (induction ys) (auto simp: Let_def)
   9.128 -  assume "sublisteq xs ys"
   9.129 -  thus "xs \<in> set (sublists ys)"
   9.130 +  assume "subseq xs ys"
   9.131 +  thus "xs \<in> set (subseqs ys)"
   9.132      by (induction xs ys rule: list_emb.induct) (auto simp: Let_def)
   9.133  qed
   9.134  
   9.135 -lemma set_sublists_eq: "set (sublists ys) = {xs. sublisteq xs ys}"
   9.136 +lemma set_subseqs_eq: "set (subseqs ys) = {xs. subseq xs ys}"
   9.137    by auto
   9.138  
   9.139 -lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []"
   9.140 +lemma subseq_append_le_same_iff: "subseq (xs @ ys) ys \<longleftrightarrow> xs = []"
   9.141    by (auto dest: list_emb_length)
   9.142  
   9.143 -lemma sublisteq_singleton_left: "sublisteq [x] ys \<longleftrightarrow> x \<in> set ys"
   9.144 +lemma subseq_singleton_left: "subseq [x] ys \<longleftrightarrow> x \<in> set ys"
   9.145    by (fastforce dest: list_emb_ConsD split_list_last)
   9.146  
   9.147  lemma list_emb_append_mono:
   9.148 @@ -1012,11 +1012,11 @@
   9.149  
   9.150  subsection \<open>Appending elements\<close>
   9.151  
   9.152 -lemma sublisteq_append [simp]:
   9.153 -  "sublisteq (xs @ zs) (ys @ zs) \<longleftrightarrow> sublisteq xs ys" (is "?l = ?r")
   9.154 +lemma subseq_append [simp]:
   9.155 +  "subseq (xs @ zs) (ys @ zs) \<longleftrightarrow> subseq xs ys" (is "?l = ?r")
   9.156  proof
   9.157 -  { fix xs' ys' xs ys zs :: "'a list" assume "sublisteq xs' ys'"
   9.158 -    then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sublisteq xs ys"
   9.159 +  { fix xs' ys' xs ys zs :: "'a list" assume "subseq xs' ys'"
   9.160 +    then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> subseq xs ys"
   9.161      proof (induct arbitrary: xs ys zs)
   9.162        case list_emb_Nil show ?case by simp
   9.163      next
   9.164 @@ -1038,11 +1038,11 @@
   9.165    moreover assume ?l
   9.166    ultimately show ?r by blast
   9.167  next
   9.168 -  assume ?r then show ?l by (metis list_emb_append_mono sublist_order.order_refl)
   9.169 +  assume ?r then show ?l by (metis list_emb_append_mono subseq_order.order_refl)
   9.170  qed
   9.171  
   9.172 -lemma sublisteq_append_iff: 
   9.173 -  "sublisteq xs (ys @ zs) \<longleftrightarrow> (\<exists>xs1 xs2. xs = xs1 @ xs2 \<and> sublisteq xs1 ys \<and> sublisteq xs2 zs)"
   9.174 +lemma subseq_append_iff: 
   9.175 +  "subseq xs (ys @ zs) \<longleftrightarrow> (\<exists>xs1 xs2. xs = xs1 @ xs2 \<and> subseq xs1 ys \<and> subseq xs2 zs)"
   9.176    (is "?lhs = ?rhs")
   9.177  proof
   9.178    assume ?lhs thus ?rhs
   9.179 @@ -1058,61 +1058,315 @@
   9.180    qed auto
   9.181  qed (auto intro: list_emb_append_mono)
   9.182  
   9.183 -lemma sublisteq_appendE [case_names append]: 
   9.184 -  assumes "sublisteq xs (ys @ zs)"
   9.185 -  obtains xs1 xs2 where "xs = xs1 @ xs2" "sublisteq xs1 ys" "sublisteq xs2 zs"
   9.186 -  using assms by (subst (asm) sublisteq_append_iff) auto
   9.187 +lemma subseq_appendE [case_names append]: 
   9.188 +  assumes "subseq xs (ys @ zs)"
   9.189 +  obtains xs1 xs2 where "xs = xs1 @ xs2" "subseq xs1 ys" "subseq xs2 zs"
   9.190 +  using assms by (subst (asm) subseq_append_iff) auto
   9.191  
   9.192 -lemma sublisteq_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (zs @ ys)"
   9.193 +lemma subseq_drop_many: "subseq xs ys \<Longrightarrow> subseq xs (zs @ ys)"
   9.194    by (induct zs) auto
   9.195  
   9.196 -lemma sublisteq_rev_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (ys @ zs)"
   9.197 +lemma subseq_rev_drop_many: "subseq xs ys \<Longrightarrow> subseq xs (ys @ zs)"
   9.198    by (metis append_Nil2 list_emb_Nil list_emb_append_mono)
   9.199  
   9.200  
   9.201  subsection \<open>Relation to standard list operations\<close>
   9.202  
   9.203 -lemma sublisteq_map:
   9.204 -  assumes "sublisteq xs ys" shows "sublisteq (map f xs) (map f ys)"
   9.205 +lemma subseq_map:
   9.206 +  assumes "subseq xs ys" shows "subseq (map f xs) (map f ys)"
   9.207    using assms by (induct) auto
   9.208  
   9.209 -lemma sublisteq_filter_left [simp]: "sublisteq (filter P xs) xs"
   9.210 +lemma subseq_filter_left [simp]: "subseq (filter P xs) xs"
   9.211    by (induct xs) auto
   9.212  
   9.213 -lemma sublisteq_filter [simp]:
   9.214 -  assumes "sublisteq xs ys" shows "sublisteq (filter P xs) (filter P ys)"
   9.215 +lemma subseq_filter [simp]:
   9.216 +  assumes "subseq xs ys" shows "subseq (filter P xs) (filter P ys)"
   9.217    using assms by induct auto
   9.218  
   9.219 -lemma "sublisteq xs ys \<longleftrightarrow> (\<exists>N. xs = sublist ys N)" (is "?L = ?R")
   9.220 +lemma subseq_conv_nths: 
   9.221 +  "subseq xs ys \<longleftrightarrow> (\<exists>N. xs = nths ys N)" (is "?L = ?R")
   9.222  proof
   9.223    assume ?L
   9.224    then show ?R
   9.225    proof (induct)
   9.226 -    case list_emb_Nil show ?case by (metis sublist_empty)
   9.227 +    case list_emb_Nil show ?case by (metis nths_empty)
   9.228    next
   9.229      case (list_emb_Cons xs ys x)
   9.230 -    then obtain N where "xs = sublist ys N" by blast
   9.231 -    then have "xs = sublist (x#ys) (Suc ` N)"
   9.232 -      by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   9.233 +    then obtain N where "xs = nths ys N" by blast
   9.234 +    then have "xs = nths (x#ys) (Suc ` N)"
   9.235 +      by (clarsimp simp add: nths_Cons inj_image_mem_iff)
   9.236      then show ?case by blast
   9.237    next
   9.238      case (list_emb_Cons2 x y xs ys)
   9.239 -    then obtain N where "xs = sublist ys N" by blast
   9.240 -    then have "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
   9.241 -      by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
   9.242 +    then obtain N where "xs = nths ys N" by blast
   9.243 +    then have "x#xs = nths (x#ys) (insert 0 (Suc ` N))"
   9.244 +      by (clarsimp simp add: nths_Cons inj_image_mem_iff)
   9.245      moreover from list_emb_Cons2 have "x = y" by simp
   9.246      ultimately show ?case by blast
   9.247    qed
   9.248  next
   9.249    assume ?R
   9.250 -  then obtain N where "xs = sublist ys N" ..
   9.251 -  moreover have "sublisteq (sublist ys N) ys"
   9.252 +  then obtain N where "xs = nths ys N" ..
   9.253 +  moreover have "subseq (nths ys N) ys"
   9.254    proof (induct ys arbitrary: N)
   9.255      case Nil show ?case by simp
   9.256    next
   9.257 -    case Cons then show ?case by (auto simp: sublist_Cons)
   9.258 +    case Cons then show ?case by (auto simp: nths_Cons)
   9.259    qed
   9.260    ultimately show ?L by simp
   9.261  qed
   9.262 +  
   9.263 +  
   9.264 +subsection \<open>Contiguous sublists\<close>
   9.265 +
   9.266 +definition sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where 
   9.267 +  "sublist xs ys = (\<exists>ps ss. ys = ps @ xs @ ss)"
   9.268 +  
   9.269 +definition strict_sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where 
   9.270 +  "strict_sublist xs ys \<longleftrightarrow> sublist xs ys \<and> xs \<noteq> ys"
   9.271 +
   9.272 +interpretation sublist_order: order sublist strict_sublist
   9.273 +proof
   9.274 +  fix xs ys zs :: "'a list"
   9.275 +  assume "sublist xs ys" "sublist ys zs"
   9.276 +  then obtain xs1 xs2 ys1 ys2 where "ys = xs1 @ xs @ xs2" "zs = ys1 @ ys @ ys2"
   9.277 +    by (auto simp: sublist_def)
   9.278 +  hence "zs = (ys1 @ xs1) @ xs @ (xs2 @ ys2)" by simp
   9.279 +  thus "sublist xs zs" unfolding sublist_def by blast
   9.280 +next
   9.281 +  fix xs ys :: "'a list"
   9.282 +  {
   9.283 +    assume "sublist xs ys" "sublist ys xs"
   9.284 +    then obtain as bs cs ds 
   9.285 +      where xs: "xs = as @ ys @ bs" and ys: "ys = cs @ xs @ ds" 
   9.286 +      by (auto simp: sublist_def)
   9.287 +    have "xs = as @ cs @ xs @ ds @ bs" by (subst xs, subst ys) auto
   9.288 +    also have "length \<dots> = length as + length cs + length xs + length bs + length ds" 
   9.289 +      by simp
   9.290 +    finally have "as = []" "bs = []" by simp_all
   9.291 +    with xs show "xs = ys" by simp
   9.292 +  }
   9.293 +  thus "strict_sublist xs ys \<longleftrightarrow> (sublist xs ys \<and> \<not>sublist ys xs)"
   9.294 +    by (auto simp: strict_sublist_def)
   9.295 +qed (auto simp: strict_sublist_def sublist_def intro: exI[of _ "[]"])
   9.296 +  
   9.297 +lemma sublist_Nil_left [simp, intro]: "sublist [] ys"
   9.298 +  by (auto simp: sublist_def)
   9.299 +    
   9.300 +lemma sublist_Cons_Nil [simp]: "\<not>sublist (x#xs) []"
   9.301 +  by (auto simp: sublist_def)
   9.302 +    
   9.303 +lemma sublist_Nil_right [simp]: "sublist xs [] \<longleftrightarrow> xs = []"
   9.304 +  by (cases xs) auto
   9.305 +    
   9.306 +lemma sublist_appendI [simp, intro]: "sublist xs (ps @ xs @ ss)"
   9.307 +  by (auto simp: sublist_def)
   9.308 +    
   9.309 +lemma sublist_append_leftI [simp, intro]: "sublist xs (ps @ xs)"
   9.310 +  by (auto simp: sublist_def intro: exI[of _ "[]"])
   9.311 +    
   9.312 +lemma sublist_append_rightI [simp, intro]: "sublist xs (xs @ ss)"
   9.313 +  by (auto simp: sublist_def intro: exI[of _ "[]"]) 
   9.314 +
   9.315 +lemma sublist_altdef: "sublist xs ys \<longleftrightarrow> (\<exists>ys'. prefix ys' ys \<and> suffix xs ys')"
   9.316 +proof safe
   9.317 +  assume "sublist xs ys"
   9.318 +  then obtain ps ss where "ys = ps @ xs @ ss" by (auto simp: sublist_def)
   9.319 +  thus "\<exists>ys'. prefix ys' ys \<and> suffix xs ys'"
   9.320 +    by (intro exI[of _ "ps @ xs"] conjI suffix_appendI) auto
   9.321 +next
   9.322 +  fix ys'
   9.323 +  assume "prefix ys' ys" "suffix xs ys'"
   9.324 +  thus "sublist xs ys" by (auto simp: prefix_def suffix_def)
   9.325 +qed
   9.326 +  
   9.327 +lemma sublist_altdef': "sublist xs ys \<longleftrightarrow> (\<exists>ys'. suffix ys' ys \<and> prefix xs ys')"
   9.328 +proof safe
   9.329 +  assume "sublist xs ys"
   9.330 +  then obtain ps ss where "ys = ps @ xs @ ss" by (auto simp: sublist_def)
   9.331 +  thus "\<exists>ys'. suffix ys' ys \<and> prefix xs ys'"
   9.332 +    by (intro exI[of _ "xs @ ss"] conjI suffixI) auto
   9.333 +next
   9.334 +  fix ys'
   9.335 +  assume "suffix ys' ys" "prefix xs ys'"
   9.336 +  thus "sublist xs ys" by (auto simp: prefix_def suffix_def)
   9.337 +qed
   9.338 +
   9.339 +lemma sublist_Cons_right: "sublist xs (y # ys) \<longleftrightarrow> prefix xs (y # ys) \<or> sublist xs ys"
   9.340 +  by (auto simp: sublist_def prefix_def Cons_eq_append_conv)
   9.341 +    
   9.342 +lemma sublist_code [code]:
   9.343 +  "sublist [] ys \<longleftrightarrow> True"
   9.344 +  "sublist (x # xs) [] \<longleftrightarrow> False"
   9.345 +  "sublist (x # xs) (y # ys) \<longleftrightarrow> prefix (x # xs) (y # ys) \<or> sublist (x # xs) ys"
   9.346 +  by (simp_all add: sublist_Cons_right)
   9.347 +
   9.348 +
   9.349 +lemma sublist_append:
   9.350 +  "sublist xs (ys @ zs) \<longleftrightarrow> 
   9.351 +     sublist xs ys \<or> sublist xs zs \<or> (\<exists>xs1 xs2. xs = xs1 @ xs2 \<and> suffix xs1 ys \<and> prefix xs2 zs)"
   9.352 +  by (auto simp: sublist_altdef prefix_append suffix_append)
   9.353 +
   9.354 +primrec sublists :: "'a list \<Rightarrow> 'a list list" where
   9.355 +  "sublists [] = [[]]"
   9.356 +| "sublists (x # xs) = sublists xs @ map (op # x) (prefixes xs)"
   9.357 +
   9.358 +lemma in_set_sublists [simp]: "xs \<in> set (sublists ys) \<longleftrightarrow> sublist xs ys" 
   9.359 +  by (induction ys arbitrary: xs) (auto simp: sublist_Cons_right prefix_Cons)
   9.360 +
   9.361 +lemma set_sublists_eq: "set (sublists xs) = {ys. sublist ys xs}"
   9.362 +  by auto
   9.363 +
   9.364 +lemma length_sublists [simp]: "length (sublists xs) = Suc (length xs * Suc (length xs) div 2)"
   9.365 +  by (induction xs) simp_all
   9.366 +
   9.367 +lemma sublist_length_le: "sublist xs ys \<Longrightarrow> length xs \<le> length ys"
   9.368 +  by (auto simp add: sublist_def)
   9.369 +
   9.370 +lemma set_mono_sublist: "sublist xs ys \<Longrightarrow> set xs \<subseteq> set ys"
   9.371 +  by (auto simp add: sublist_def)
   9.372 +    
   9.373 +lemma prefix_imp_sublist [simp, intro]: "prefix xs ys \<Longrightarrow> sublist xs ys"
   9.374 +  by (auto simp: sublist_def prefix_def intro: exI[of _ "[]"])
   9.375 +    
   9.376 +lemma suffix_imp_sublist [simp, intro]: "suffix xs ys \<Longrightarrow> sublist xs ys"
   9.377 +  by (auto simp: sublist_def suffix_def intro: exI[of _ "[]"])
   9.378 +
   9.379 +lemma sublist_take [simp, intro]: "sublist (take n xs) xs"
   9.380 +  by (rule prefix_imp_sublist) (simp_all add: take_is_prefix)
   9.381 +
   9.382 +lemma sublist_drop [simp, intro]: "sublist (drop n xs) xs"
   9.383 +  by (rule suffix_imp_sublist) (simp_all add: suffix_drop)
   9.384 +    
   9.385 +lemma sublist_tl [simp, intro]: "sublist (tl xs) xs"
   9.386 +  by (rule suffix_imp_sublist) (simp_all add: suffix_drop)
   9.387 +    
   9.388 +lemma sublist_butlast [simp, intro]: "sublist (butlast xs) xs"
   9.389 +  by (rule prefix_imp_sublist) (simp_all add: prefixeq_butlast)
   9.390 +    
   9.391 +lemma sublist_rev [simp]: "sublist (rev xs) (rev ys) = sublist xs ys"
   9.392 +proof
   9.393 +  assume "sublist (rev xs) (rev ys)"
   9.394 +  then obtain as bs where "rev ys = as @ rev xs @ bs"
   9.395 +    by (auto simp: sublist_def)
   9.396 +  also have "rev \<dots> = rev bs @ xs @ rev as" by simp
   9.397 +  finally show "sublist xs ys" by simp
   9.398 +next
   9.399 +  assume "sublist xs ys"
   9.400 +  then obtain as bs where "ys = as @ xs @ bs"
   9.401 +    by (auto simp: sublist_def)
   9.402 +  also have "rev \<dots> = rev bs @ rev xs @ rev as" by simp
   9.403 +  finally show "sublist (rev xs) (rev ys)" by simp
   9.404 +qed
   9.405 +    
   9.406 +lemma sublist_rev_left: "sublist (rev xs) ys = sublist xs (rev ys)"
   9.407 +  by (subst sublist_rev [symmetric]) (simp only: rev_rev_ident)
   9.408 +    
   9.409 +lemma sublist_rev_right: "sublist xs (rev ys) = sublist (rev xs) ys"
   9.410 +  by (subst sublist_rev [symmetric]) (simp only: rev_rev_ident)
   9.411 +
   9.412 +lemma snoc_sublist_snoc: 
   9.413 +  "sublist (xs @ [x]) (ys @ [y]) \<longleftrightarrow> 
   9.414 +     (x = y \<and> suffix xs ys \<or> sublist (xs @ [x]) ys) "
   9.415 +  by (subst (1 2) sublist_rev [symmetric])
   9.416 +     (simp del: sublist_rev add: sublist_Cons_right suffix_to_prefix)
   9.417 +
   9.418 +lemma sublist_snoc:
   9.419 +  "sublist xs (ys @ [y]) \<longleftrightarrow> suffix xs (ys @ [y]) \<or> sublist xs ys"
   9.420 +  by (subst (1 2) sublist_rev [symmetric])
   9.421 +     (simp del: sublist_rev add: sublist_Cons_right suffix_to_prefix)     
   9.422 +
   9.423 +subsection \<open>Parametricity\<close>
   9.424 +
   9.425 +context includes lifting_syntax
   9.426 +begin    
   9.427 +  
   9.428 +private lemma prefix_primrec:
   9.429 +  "prefix = rec_list (\<lambda>xs. True) (\<lambda>x xs xsa ys.
   9.430 +              case ys of [] \<Rightarrow> False | y # ys \<Rightarrow> x = y \<and> xsa ys)"
   9.431 +proof (intro ext, goal_cases)
   9.432 +  case (1 xs ys)
   9.433 +  show ?case by (induction xs arbitrary: ys) (auto simp: prefix_Cons split: list.splits)
   9.434 +qed
   9.435 +
   9.436 +private lemma sublist_primrec:
   9.437 +  "sublist = (\<lambda>xs ys. rec_list (\<lambda>xs. xs = []) (\<lambda>y ys ysa xs. prefix xs (y # ys) \<or> ysa xs) ys xs)"
   9.438 +proof (intro ext, goal_cases)
   9.439 +  case (1 xs ys)
   9.440 +  show ?case by (induction ys) (auto simp: sublist_Cons_right)
   9.441 +qed
   9.442 +
   9.443 +private lemma list_emb_primrec:
   9.444 +  "list_emb = (\<lambda>uu uua uuaa. rec_list (\<lambda>P xs. List.null xs) (\<lambda>y ys ysa P xs. case xs of [] \<Rightarrow> True 
   9.445 +     | x # xs \<Rightarrow> if P x y then ysa P xs else ysa P (x # xs)) uuaa uu uua)"
   9.446 +proof (intro ext, goal_cases)
   9.447 +  case (1 P xs ys)
   9.448 +  show ?case
   9.449 +    by (induction ys arbitrary: xs)
   9.450 +       (auto simp: list_emb_code List.null_def split: list.splits)
   9.451 +qed
   9.452 +
   9.453 +lemma prefix_transfer [transfer_rule]:
   9.454 +  assumes [transfer_rule]: "bi_unique A"
   9.455 +  shows   "(list_all2 A ===> list_all2 A ===> op =) prefix prefix"  
   9.456 +  unfolding prefix_primrec by transfer_prover
   9.457 +    
   9.458 +lemma suffix_transfer [transfer_rule]:
   9.459 +  assumes [transfer_rule]: "bi_unique A"
   9.460 +  shows   "(list_all2 A ===> list_all2 A ===> op =) suffix suffix"  
   9.461 +  unfolding suffix_to_prefix [abs_def] by transfer_prover
   9.462 +
   9.463 +lemma sublist_transfer [transfer_rule]:
   9.464 +  assumes [transfer_rule]: "bi_unique A"
   9.465 +  shows   "(list_all2 A ===> list_all2 A ===> op =) sublist sublist"
   9.466 +  unfolding sublist_primrec by transfer_prover
   9.467 +
   9.468 +lemma parallel_transfer [transfer_rule]:
   9.469 +  assumes [transfer_rule]: "bi_unique A"
   9.470 +  shows   "(list_all2 A ===> list_all2 A ===> op =) parallel parallel"
   9.471 +  unfolding parallel_def by transfer_prover
   9.472 +    
   9.473 +
   9.474 +
   9.475 +lemma list_emb_transfer [transfer_rule]:
   9.476 +  "((A ===> A ===> op =) ===> list_all2 A ===> list_all2 A ===> op =) list_emb list_emb"
   9.477 +  unfolding list_emb_primrec by transfer_prover
   9.478 +
   9.479 +lemma strict_prefix_transfer [transfer_rule]:
   9.480 +  assumes [transfer_rule]: "bi_unique A"
   9.481 +  shows   "(list_all2 A ===> list_all2 A ===> op =) strict_prefix strict_prefix"  
   9.482 +  unfolding strict_prefix_def by transfer_prover
   9.483 +    
   9.484 +lemma strict_suffix_transfer [transfer_rule]:
   9.485 +  assumes [transfer_rule]: "bi_unique A"
   9.486 +  shows   "(list_all2 A ===> list_all2 A ===> op =) strict_suffix strict_suffix"  
   9.487 +  unfolding strict_suffix_def by transfer_prover
   9.488 +    
   9.489 +lemma strict_subseq_transfer [transfer_rule]:
   9.490 +  assumes [transfer_rule]: "bi_unique A"
   9.491 +  shows   "(list_all2 A ===> list_all2 A ===> op =) strict_subseq strict_subseq"  
   9.492 +  unfolding strict_subseq_def by transfer_prover
   9.493 +    
   9.494 +lemma strict_sublist_transfer [transfer_rule]:
   9.495 +  assumes [transfer_rule]: "bi_unique A"
   9.496 +  shows   "(list_all2 A ===> list_all2 A ===> op =) strict_sublist strict_sublist"  
   9.497 +  unfolding strict_sublist_def by transfer_prover
   9.498 +
   9.499 +lemma prefixes_transfer [transfer_rule]:
   9.500 +  assumes [transfer_rule]: "bi_unique A"
   9.501 +  shows   "(list_all2 A ===> list_all2 (list_all2 A)) prefixes prefixes"
   9.502 +  unfolding prefixes_def by transfer_prover
   9.503 +    
   9.504 +lemma suffixes_transfer [transfer_rule]:
   9.505 +  assumes [transfer_rule]: "bi_unique A"
   9.506 +  shows   "(list_all2 A ===> list_all2 (list_all2 A)) suffixes suffixes"
   9.507 +  unfolding suffixes_def by transfer_prover
   9.508 +    
   9.509 +lemma sublists_transfer [transfer_rule]:
   9.510 +  assumes [transfer_rule]: "bi_unique A"
   9.511 +  shows   "(list_all2 A ===> list_all2 (list_all2 A)) sublists sublists"
   9.512 +  unfolding sublists_def by transfer_prover
   9.513  
   9.514  end
   9.515 +
   9.516 +end
    10.1 --- a/src/HOL/Library/Sublist_Order.thy	Sun May 28 15:46:26 2017 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,76 +0,0 @@
    10.4 -(*  Title:      HOL/Library/Sublist_Order.thy
    10.5 -    Author:     Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
    10.6 -    Author:     Florian Haftmann, , TU Muenchen
    10.7 -    Author:     Tobias Nipkow, TU Muenchen
    10.8 -*)
    10.9 -
   10.10 -section \<open>Sublist Ordering\<close>
   10.11 -
   10.12 -theory Sublist_Order
   10.13 -imports Sublist
   10.14 -begin
   10.15 -
   10.16 -text \<open>
   10.17 -  This theory defines sublist ordering on lists. A list \<open>ys\<close> is a sublist of a
   10.18 -  list \<open>xs\<close>, iff one obtains \<open>ys\<close> by erasing some elements from \<open>xs\<close>.
   10.19 -\<close>
   10.20 -
   10.21 -subsection \<open>Definitions and basic lemmas\<close>
   10.22 -
   10.23 -instantiation list :: (type) ord
   10.24 -begin
   10.25 -
   10.26 -definition "xs \<le> ys \<longleftrightarrow> sublisteq xs ys" for xs ys :: "'a list"
   10.27 -definition "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list"
   10.28 -
   10.29 -instance ..
   10.30 -
   10.31 -end
   10.32 -
   10.33 -instance list :: (type) order
   10.34 -proof
   10.35 -  fix xs ys zs :: "'a list"
   10.36 -  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
   10.37 -    unfolding less_list_def ..
   10.38 -  show "xs \<le> xs"
   10.39 -    by (simp add: less_eq_list_def)
   10.40 -  show "xs = ys" if "xs \<le> ys" and "ys \<le> xs"
   10.41 -    using that unfolding less_eq_list_def by (rule sublist_order.antisym)
   10.42 -  show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs"
   10.43 -    using that unfolding less_eq_list_def by (rule sublist_order.order_trans)
   10.44 -qed
   10.45 -
   10.46 -lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
   10.47 -  list_emb.induct [of "op =", folded less_eq_list_def]
   10.48 -lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "op =", folded less_eq_list_def]
   10.49 -lemmas le_list_Cons2_iff [simp, code] = sublisteq_Cons2_iff [folded less_eq_list_def]
   10.50 -lemmas le_list_map = sublisteq_map [folded less_eq_list_def]
   10.51 -lemmas le_list_filter = sublisteq_filter [folded less_eq_list_def]
   10.52 -lemmas le_list_length = list_emb_length [of "op =", folded less_eq_list_def]
   10.53 -
   10.54 -lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
   10.55 -  by (metis list_emb_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def)
   10.56 -
   10.57 -lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
   10.58 -  by (metis less_eq_list_def list_emb_Nil order_less_le)
   10.59 -
   10.60 -lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
   10.61 -  by (metis list_emb_Nil less_eq_list_def less_list_def)
   10.62 -
   10.63 -lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
   10.64 -  by (unfold less_le less_eq_list_def) (auto)
   10.65 -
   10.66 -lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
   10.67 -  by (metis sublisteq_Cons2_iff less_list_def less_eq_list_def)
   10.68 -
   10.69 -lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
   10.70 -  by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le
   10.71 -      self_append_conv2 less_eq_list_def)
   10.72 -
   10.73 -lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
   10.74 -  by (metis less_list_def less_eq_list_def sublisteq_append')
   10.75 -
   10.76 -lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
   10.77 -  by (unfold less_le less_eq_list_def) auto
   10.78 -
   10.79 -end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Library/Subseq_Order.thy	Mon May 29 09:14:15 2017 +0200
    11.3 @@ -0,0 +1,76 @@
    11.4 +(*  Title:      HOL/Library/Subseq_Order.thy
    11.5 +    Author:     Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
    11.6 +    Author:     Florian Haftmann, TU Muenchen
    11.7 +    Author:     Tobias Nipkow, TU Muenchen
    11.8 +*)
    11.9 +
   11.10 +section \<open>Subsequence Ordering\<close>
   11.11 +
   11.12 +theory Subseq_Order
   11.13 +imports Sublist
   11.14 +begin
   11.15 +
   11.16 +text \<open>
   11.17 +  This theory defines subsequence ordering on lists. A list \<open>ys\<close> is a subsequence of a
   11.18 +  list \<open>xs\<close>, iff one obtains \<open>ys\<close> by erasing some elements from \<open>xs\<close>.
   11.19 +\<close>
   11.20 +
   11.21 +subsection \<open>Definitions and basic lemmas\<close>
   11.22 +
   11.23 +instantiation list :: (type) ord
   11.24 +begin
   11.25 +
   11.26 +definition "xs \<le> ys \<longleftrightarrow> subseq xs ys" for xs ys :: "'a list"
   11.27 +definition "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list"
   11.28 +
   11.29 +instance ..
   11.30 +
   11.31 +end
   11.32 +
   11.33 +instance list :: (type) order
   11.34 +proof
   11.35 +  fix xs ys zs :: "'a list"
   11.36 +  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
   11.37 +    unfolding less_list_def ..
   11.38 +  show "xs \<le> xs"
   11.39 +    by (simp add: less_eq_list_def)
   11.40 +  show "xs = ys" if "xs \<le> ys" and "ys \<le> xs"
   11.41 +    using that unfolding less_eq_list_def by (rule subseq_order.antisym)
   11.42 +  show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs"
   11.43 +    using that unfolding less_eq_list_def by (rule subseq_order.order_trans)
   11.44 +qed
   11.45 +
   11.46 +lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
   11.47 +  list_emb.induct [of "op =", folded less_eq_list_def]
   11.48 +lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "op =", folded less_eq_list_def]
   11.49 +lemmas le_list_Cons2_iff [simp, code] = subseq_Cons2_iff [folded less_eq_list_def]
   11.50 +lemmas le_list_map = subseq_map [folded less_eq_list_def]
   11.51 +lemmas le_list_filter = subseq_filter [folded less_eq_list_def]
   11.52 +lemmas le_list_length = list_emb_length [of "op =", folded less_eq_list_def]
   11.53 +
   11.54 +lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
   11.55 +  by (metis list_emb_length subseq_same_length le_neq_implies_less less_list_def less_eq_list_def)
   11.56 +
   11.57 +lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
   11.58 +  by (metis less_eq_list_def list_emb_Nil order_less_le)
   11.59 +
   11.60 +lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
   11.61 +  by (metis list_emb_Nil less_eq_list_def less_list_def)
   11.62 +
   11.63 +lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
   11.64 +  by (unfold less_le less_eq_list_def) (auto)
   11.65 +
   11.66 +lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
   11.67 +  by (metis subseq_Cons2_iff less_list_def less_eq_list_def)
   11.68 +
   11.69 +lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
   11.70 +  by (metis subseq_append_le_same_iff subseq_drop_many order_less_le
   11.71 +      self_append_conv2 less_eq_list_def)
   11.72 +
   11.73 +lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
   11.74 +  by (metis less_list_def less_eq_list_def subseq_append')
   11.75 +
   11.76 +lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
   11.77 +  by (unfold less_le less_eq_list_def) auto
   11.78 +
   11.79 +end
    12.1 --- a/src/HOL/List.thy	Sun May 28 15:46:26 2017 +0200
    12.2 +++ b/src/HOL/List.thy	Mon May 29 09:14:15 2017 +0200
    12.3 @@ -242,12 +242,12 @@
    12.4  definition rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    12.5  "rotate n = rotate1 ^^ n"
    12.6  
    12.7 -definition sublist :: "'a list => nat set => 'a list" where
    12.8 -"sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
    12.9 -
   12.10 -primrec sublists :: "'a list \<Rightarrow> 'a list list" where
   12.11 -"sublists [] = [[]]" |
   12.12 -"sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
   12.13 +definition nths :: "'a list => nat set => 'a list" where
   12.14 +"nths xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
   12.15 +
   12.16 +primrec subseqs :: "'a list \<Rightarrow> 'a list list" where
   12.17 +"subseqs [] = [[]]" |
   12.18 +"subseqs (x#xs) = (let xss = subseqs xs in map (Cons x) xss @ xss)"
   12.19  
   12.20  primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
   12.21  "n_lists 0 xs = [[]]" |
   12.22 @@ -315,8 +315,8 @@
   12.23  @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
   12.24  @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
   12.25  @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
   12.26 -@{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
   12.27 -@{lemma "sublists [a,b] = [[a, b], [a], [b], []]" by simp}\\
   12.28 +@{lemma "nths [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:nths_def)}\\
   12.29 +@{lemma "subseqs [a,b] = [[a, b], [a], [b], []]" by simp}\\
   12.30  @{lemma "List.n_lists 2 [a,b,c] = [[a, a], [b, a], [c, a], [a, b], [b, b], [c, b], [a, c], [b, c], [c, c]]" by (simp add: eval_nat_numeral)}\\
   12.31  @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\
   12.32  @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\
   12.33 @@ -4333,19 +4333,19 @@
   12.34  using mod_less_divisor[of "length xs" n] by arith
   12.35  
   12.36  
   12.37 -subsubsection \<open>@{const sublist} --- a generalization of @{const nth} to sets\<close>
   12.38 -
   12.39 -lemma sublist_empty [simp]: "sublist xs {} = []"
   12.40 -by (auto simp add: sublist_def)
   12.41 -
   12.42 -lemma sublist_nil [simp]: "sublist [] A = []"
   12.43 -by (auto simp add: sublist_def)
   12.44 -
   12.45 -lemma length_sublist:
   12.46 -  "length(sublist xs I) = card{i. i < length xs \<and> i : I}"
   12.47 -by(simp add: sublist_def length_filter_conv_card cong:conj_cong)
   12.48 -
   12.49 -lemma sublist_shift_lemma_Suc:
   12.50 +subsubsection \<open>@{const nths} --- a generalization of @{const nth} to sets\<close>
   12.51 +
   12.52 +lemma nths_empty [simp]: "nths xs {} = []"
   12.53 +by (auto simp add: nths_def)
   12.54 +
   12.55 +lemma nths_nil [simp]: "nths [] A = []"
   12.56 +by (auto simp add: nths_def)
   12.57 +
   12.58 +lemma length_nths:
   12.59 +  "length (nths xs I) = card{i. i < length xs \<and> i : I}"
   12.60 +by(simp add: nths_def length_filter_conv_card cong:conj_cong)
   12.61 +
   12.62 +lemma nths_shift_lemma_Suc:
   12.63    "map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
   12.64     map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
   12.65  apply(induct xs arbitrary: "is")
   12.66 @@ -4355,92 +4355,88 @@
   12.67  apply simp
   12.68  done
   12.69  
   12.70 -lemma sublist_shift_lemma:
   12.71 +lemma nths_shift_lemma:
   12.72       "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
   12.73        map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
   12.74  by (induct xs rule: rev_induct) (simp_all add: add.commute)
   12.75  
   12.76 -lemma sublist_append:
   12.77 -     "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
   12.78 -apply (unfold sublist_def)
   12.79 +lemma nths_append:
   12.80 +     "nths (l @ l') A = nths l A @ nths l' {j. j + length l : A}"
   12.81 +apply (unfold nths_def)
   12.82  apply (induct l' rule: rev_induct, simp)
   12.83 -apply (simp add: upt_add_eq_append[of 0] sublist_shift_lemma)
   12.84 +apply (simp add: upt_add_eq_append[of 0] nths_shift_lemma)
   12.85  apply (simp add: add.commute)
   12.86  done
   12.87  
   12.88 -lemma sublist_Cons:
   12.89 -"sublist (x # l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}"
   12.90 +lemma nths_Cons:
   12.91 +"nths (x # l) A = (if 0:A then [x] else []) @ nths l {j. Suc j : A}"
   12.92  apply (induct l rule: rev_induct)
   12.93 - apply (simp add: sublist_def)
   12.94 -apply (simp del: append_Cons add: append_Cons[symmetric] sublist_append)
   12.95 + apply (simp add: nths_def)
   12.96 +apply (simp del: append_Cons add: append_Cons[symmetric] nths_append)
   12.97  done
   12.98  
   12.99 -lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
  12.100 +lemma set_nths: "set(nths xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
  12.101  apply(induct xs arbitrary: I)
  12.102 -apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
  12.103 +apply(auto simp: nths_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
  12.104  done
  12.105  
  12.106 -lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
  12.107 -by(auto simp add:set_sublist)
  12.108 -
  12.109 -lemma notin_set_sublistI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(sublist xs I)"
  12.110 -by(auto simp add:set_sublist)
  12.111 -
  12.112 -lemma in_set_sublistD: "x \<in> set(sublist xs I) \<Longrightarrow> x \<in> set xs"
  12.113 -by(auto simp add:set_sublist)
  12.114 -
  12.115 -lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"
  12.116 -by (simp add: sublist_Cons)
  12.117 -
  12.118 -
  12.119 -lemma distinct_sublistI[simp]: "distinct xs \<Longrightarrow> distinct(sublist xs I)"
  12.120 -apply(induct xs arbitrary: I)
  12.121 - apply simp
  12.122 -apply(auto simp add:sublist_Cons)
  12.123 -done
  12.124 -
  12.125 -
  12.126 -lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"
  12.127 -apply (induct l rule: rev_induct, simp)
  12.128 -apply (simp split: nat_diff_split add: sublist_append)
  12.129 -done
  12.130 -
  12.131 -lemma filter_in_sublist:
  12.132 - "distinct xs \<Longrightarrow> filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"
  12.133 +lemma set_nths_subset: "set(nths xs I) \<subseteq> set xs"
  12.134 +by(auto simp add:set_nths)
  12.135 +
  12.136 +lemma notin_set_nthsI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(nths xs I)"
  12.137 +by(auto simp add:set_nths)
  12.138 +
  12.139 +lemma in_set_nthsD: "x \<in> set(nths xs I) \<Longrightarrow> x \<in> set xs"
  12.140 +by(auto simp add:set_nths)
  12.141 +
  12.142 +lemma nths_singleton [simp]: "nths [x] A = (if 0 : A then [x] else [])"
  12.143 +by (simp add: nths_Cons)
  12.144 +
  12.145 +
  12.146 +lemma distinct_nthsI[simp]: "distinct xs \<Longrightarrow> distinct (nths xs I)"
  12.147 +  by (induct xs arbitrary: I) (auto simp: nths_Cons)
  12.148 +
  12.149 +
  12.150 +lemma nths_upt_eq_take [simp]: "nths l {..<n} = take n l"
  12.151 +  by (induct l rule: rev_induct)
  12.152 +     (simp_all split: nat_diff_split add: nths_append)
  12.153 +
  12.154 +lemma filter_in_nths:
  12.155 + "distinct xs \<Longrightarrow> filter (%x. x \<in> set (nths xs s)) xs = nths xs s"
  12.156  proof (induct xs arbitrary: s)
  12.157    case Nil thus ?case by simp
  12.158  next
  12.159    case (Cons a xs)
  12.160    then have "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
  12.161 -  with Cons show ?case by(simp add: sublist_Cons cong:filter_cong)
  12.162 +  with Cons show ?case by(simp add: nths_Cons cong:filter_cong)
  12.163  qed
  12.164  
  12.165  
  12.166 -subsubsection \<open>@{const sublists} and @{const List.n_lists}\<close>
  12.167 -
  12.168 -lemma length_sublists: "length (sublists xs) = 2 ^ length xs"
  12.169 +subsubsection \<open>@{const subseqs} and @{const List.n_lists}\<close>
  12.170 +
  12.171 +lemma length_subseqs: "length (subseqs xs) = 2 ^ length xs"
  12.172    by (induct xs) (simp_all add: Let_def)
  12.173  
  12.174 -lemma sublists_powset: "set ` set (sublists xs) = Pow (set xs)"
  12.175 +lemma subseqs_powset: "set ` set (subseqs xs) = Pow (set xs)"
  12.176  proof -
  12.177    have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
  12.178      by (auto simp add: image_def)
  12.179 -  have "set (map set (sublists xs)) = Pow (set xs)"
  12.180 +  have "set (map set (subseqs xs)) = Pow (set xs)"
  12.181      by (induct xs) (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
  12.182    then show ?thesis by simp
  12.183  qed
  12.184  
  12.185 -lemma distinct_set_sublists:
  12.186 +lemma distinct_set_subseqs:
  12.187    assumes "distinct xs"
  12.188 -  shows "distinct (map set (sublists xs))"
  12.189 +  shows "distinct (map set (subseqs xs))"
  12.190  proof (rule card_distinct)
  12.191    have "finite (set xs)" ..
  12.192    then have "card (Pow (set xs)) = 2 ^ card (set xs)"
  12.193      by (rule card_Pow)
  12.194    with assms distinct_card [of xs] have "card (Pow (set xs)) = 2 ^ length xs"
  12.195      by simp
  12.196 -  then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
  12.197 -    by (simp add: sublists_powset length_sublists)
  12.198 +  then show "card (set (map set (subseqs xs))) = length (map set (subseqs xs))"
  12.199 +    by (simp add: subseqs_powset length_subseqs)
  12.200  qed
  12.201  
  12.202  lemma n_lists_Nil [simp]: "List.n_lists n [] = (if n = 0 then [[]] else [])"
  12.203 @@ -4464,20 +4460,20 @@
  12.204    qed
  12.205  qed
  12.206  
  12.207 -lemma sublists_refl: "xs \<in> set (sublists xs)"
  12.208 +lemma subseqs_refl: "xs \<in> set (subseqs xs)"
  12.209    by (induct xs) (simp_all add: Let_def)
  12.210  
  12.211 -lemma subset_sublists: "X \<subseteq> set xs \<Longrightarrow> X \<in> set ` set (sublists xs)"
  12.212 -  unfolding sublists_powset by simp
  12.213 -
  12.214 -lemma Cons_in_sublistsD: "y # ys \<in> set (sublists xs) \<Longrightarrow> ys \<in> set (sublists xs)"
  12.215 +lemma subset_subseqs: "X \<subseteq> set xs \<Longrightarrow> X \<in> set ` set (subseqs xs)"
  12.216 +  unfolding subseqs_powset by simp
  12.217 +
  12.218 +lemma Cons_in_subseqsD: "y # ys \<in> set (subseqs xs) \<Longrightarrow> ys \<in> set (subseqs xs)"
  12.219    by (induct xs) (auto simp: Let_def)
  12.220  
  12.221 -lemma sublists_distinctD: "\<lbrakk> ys \<in> set (sublists xs); distinct xs \<rbrakk> \<Longrightarrow> distinct ys"
  12.222 +lemma subseqs_distinctD: "\<lbrakk> ys \<in> set (subseqs xs); distinct xs \<rbrakk> \<Longrightarrow> distinct ys"
  12.223  proof (induct xs arbitrary: ys)
  12.224    case (Cons x xs ys)
  12.225    then show ?case
  12.226 -    by (auto simp: Let_def) (metis Pow_iff contra_subsetD image_eqI sublists_powset)
  12.227 +    by (auto simp: Let_def) (metis Pow_iff contra_subsetD image_eqI subseqs_powset)
  12.228  qed simp
  12.229  
  12.230  
  12.231 @@ -7147,9 +7143,13 @@
  12.232    "(op = ===> list_all2 A ===> list_all2 A) rotate rotate"
  12.233    unfolding rotate_def [abs_def] by transfer_prover
  12.234  
  12.235 -lemma sublist_transfer [transfer_rule]:
  12.236 -  "(list_all2 A ===> rel_set (op =) ===> list_all2 A) sublist sublist"
  12.237 -  unfolding sublist_def [abs_def] by transfer_prover
  12.238 +lemma nths_transfer [transfer_rule]:
  12.239 +  "(list_all2 A ===> rel_set (op =) ===> list_all2 A) nths nths"
  12.240 +  unfolding nths_def [abs_def] by transfer_prover
  12.241 +    
  12.242 +lemma subseqs_transfer [transfer_rule]:
  12.243 +  "(list_all2 A ===> list_all2 (list_all2 A)) subseqs subseqs"
  12.244 +  unfolding subseqs_def [abs_def] by transfer_prover
  12.245  
  12.246  lemma partition_transfer [transfer_rule]:
  12.247    "((A ===> op =) ===> list_all2 A ===> rel_prod (list_all2 A) (list_all2 A))
    13.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Sun May 28 15:46:26 2017 +0200
    13.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Mon May 29 09:14:15 2017 +0200
    13.3 @@ -388,7 +388,7 @@
    13.4  
    13.5  definition enum_term_of_set :: "'a set itself \<Rightarrow> unit \<Rightarrow> term list"
    13.6    where "enum_term_of_set _ _ =
    13.7 -    map (setify (TYPE('a))) (sublists (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))"
    13.8 +    map (setify (TYPE('a))) (subseqs (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))"
    13.9  
   13.10  instance ..
   13.11  
    14.1 --- a/src/HOL/ROOT	Sun May 28 15:46:26 2017 +0200
    14.2 +++ b/src/HOL/ROOT	Mon May 29 09:14:15 2017 +0200
    14.3 @@ -40,7 +40,7 @@
    14.4      Prefix_Order
    14.5      Product_Lexorder
    14.6      Product_Order
    14.7 -    Sublist_Order
    14.8 +    Subseq_Order
    14.9      (*data refinements and dependent applications*)
   14.10      AList_Mapping
   14.11      Code_Binary_Nat
    15.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Sun May 28 15:46:26 2017 +0200
    15.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Mon May 29 09:14:15 2017 +0200
    15.3 @@ -48,39 +48,38 @@
    15.4  
    15.5  declare sum.cong [cong]
    15.6  
    15.7 -lemma bag_of_sublist_lemma:
    15.8 +lemma bag_of_nths_lemma:
    15.9       "(\<Sum>i\<in> A Int lessThan k. {#if i<k then f i else g i#}) =  
   15.10        (\<Sum>i\<in> A Int lessThan k. {#f i#})"
   15.11  by (rule sum.cong, auto)
   15.12  
   15.13 -lemma bag_of_sublist:
   15.14 -     "bag_of (sublist l A) =  
   15.15 +lemma bag_of_nths:
   15.16 +     "bag_of (nths l A) =  
   15.17        (\<Sum>i\<in> A Int lessThan (length l). {# l!i #})"
   15.18 -apply (rule_tac xs = l in rev_induct, simp)
   15.19 -apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append 
   15.20 -                 bag_of_sublist_lemma ac_simps)
   15.21 -done
   15.22 +  by (rule_tac xs = l in rev_induct)
   15.23 +     (simp_all add: nths_append Int_insert_right lessThan_Suc nth_append 
   15.24 +                    bag_of_nths_lemma ac_simps)
   15.25  
   15.26  
   15.27 -lemma bag_of_sublist_Un_Int:
   15.28 -     "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) =  
   15.29 -      bag_of (sublist l A) + bag_of (sublist l B)"
   15.30 +lemma bag_of_nths_Un_Int:
   15.31 +     "bag_of (nths l (A Un B)) + bag_of (nths l (A Int B)) =  
   15.32 +      bag_of (nths l A) + bag_of (nths l B)"
   15.33  apply (subgoal_tac "A Int B Int {..<length l} =
   15.34                      (A Int {..<length l}) Int (B Int {..<length l}) ")
   15.35 -apply (simp add: bag_of_sublist Int_Un_distrib2 sum.union_inter, blast)
   15.36 +apply (simp add: bag_of_nths Int_Un_distrib2 sum.union_inter, blast)
   15.37  done
   15.38  
   15.39 -lemma bag_of_sublist_Un_disjoint:
   15.40 +lemma bag_of_nths_Un_disjoint:
   15.41       "A Int B = {}  
   15.42 -      ==> bag_of (sublist l (A Un B)) =  
   15.43 -          bag_of (sublist l A) + bag_of (sublist l B)"
   15.44 -by (simp add: bag_of_sublist_Un_Int [symmetric])
   15.45 +      ==> bag_of (nths l (A Un B)) =  
   15.46 +          bag_of (nths l A) + bag_of (nths l B)"
   15.47 +by (simp add: bag_of_nths_Un_Int [symmetric])
   15.48  
   15.49 -lemma bag_of_sublist_UN_disjoint [rule_format]:
   15.50 +lemma bag_of_nths_UN_disjoint [rule_format]:
   15.51       "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]  
   15.52 -      ==> bag_of (sublist l (UNION I A)) =   
   15.53 -          (\<Sum>i\<in>I. bag_of (sublist l (A i)))"
   15.54 -apply (auto simp add: bag_of_sublist)
   15.55 +      ==> bag_of (nths l (UNION I A)) =   
   15.56 +          (\<Sum>i\<in>I. bag_of (nths l (A i)))"
   15.57 +apply (auto simp add: bag_of_nths)
   15.58  unfolding UN_simps [symmetric]
   15.59  apply (subst sum.UNION_disjoint)
   15.60  apply auto
    16.1 --- a/src/HOL/UNITY/Comp/AllocImpl.thy	Sun May 28 15:46:26 2017 +0200
    16.2 +++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Mon May 29 09:14:15 2017 +0200
    16.3 @@ -78,7 +78,7 @@
    16.4           (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
    16.5           guarantees
    16.6           (\<Inter>i \<in> lessThan Nclients.
    16.7 -          (%s. sublist (merge.Out s)
    16.8 +          (%s. nths (merge.Out s)
    16.9                         {k. k < size(merge.iOut s) & merge.iOut s! k = i})
   16.10            Fols (sub i o merge.In))"
   16.11  
   16.12 @@ -110,7 +110,7 @@
   16.13           guarantees
   16.14           (\<Inter>i \<in> lessThan Nclients.
   16.15            (sub i o distr.Out) Fols
   16.16 -          (%s. sublist (distr.In s)
   16.17 +          (%s. nths (distr.In s)
   16.18                         {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"
   16.19  
   16.20  definition
   16.21 @@ -273,13 +273,13 @@
   16.22  lemma Merge_Bag_Follows_lemma:
   16.23       "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
   16.24    ==> M \<squnion> G \<in> Always
   16.25 -          {s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (merge.Out s)
   16.26 +          {s. (\<Sum>i \<in> lessThan Nclients. bag_of (nths (merge.Out s)
   16.27                                    {k. k < length (iOut s) & iOut s ! k = i})) =
   16.28                (bag_of o merge.Out) s}"
   16.29  apply (rule Always_Compl_Un_eq [THEN iffD1])
   16.30  apply (blast intro: Always_Int_I [OF Merge_Always_Out_eq_iOut Merge_Bounded])
   16.31  apply (rule UNIV_AlwaysI, clarify)
   16.32 -apply (subst bag_of_sublist_UN_disjoint [symmetric])
   16.33 +apply (subst bag_of_nths_UN_disjoint [symmetric])
   16.34    apply (simp)
   16.35   apply blast
   16.36  apply (simp add: set_conv_nth)
   16.37 @@ -327,12 +327,12 @@
   16.38       "[| G \<in> preserves distr.Out;
   16.39           D \<squnion> G \<in> Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |]
   16.40    ==> D \<squnion> G \<in> Always
   16.41 -          {s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (distr.In s)
   16.42 +          {s. (\<Sum>i \<in> lessThan Nclients. bag_of (nths (distr.In s)
   16.43                                    {k. k < length (iIn s) & iIn s ! k = i})) =
   16.44 -              bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}"
   16.45 +              bag_of (nths (distr.In s) (lessThan (length (iIn s))))}"
   16.46  apply (erule Always_Compl_Un_eq [THEN iffD1])
   16.47  apply (rule UNIV_AlwaysI, clarify)
   16.48 -apply (subst bag_of_sublist_UN_disjoint [symmetric])
   16.49 +apply (subst bag_of_nths_UN_disjoint [symmetric])
   16.50    apply (simp (no_asm))
   16.51   apply blast
   16.52  apply (simp add: set_conv_nth)
   16.53 @@ -357,7 +357,7 @@
   16.54         (\<Inter>i \<in> lessThan Nclients.
   16.55          (%s. \<Sum>i \<in> lessThan Nclients. (bag_of o sub i o distr.Out) s)
   16.56          Fols
   16.57 -        (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))"
   16.58 +        (%s. bag_of (nths (distr.In s) (lessThan (length(distr.iIn s))))))"
   16.59  apply (rule guaranteesI, clarify)
   16.60  apply (rule Distr_Bag_Follows_lemma [THEN Always_Follows2], auto)
   16.61  apply (rule Follows_sum)