--- a/NEWS Sun May 28 15:46:26 2017 +0200
+++ b/NEWS Mon May 29 09:14:15 2017 +0200
@@ -73,6 +73,9 @@
*** HOL ***
+* "sublist" from theory List renamed to "nths" in analogy with "nth".
+"sublisteq" renamed to "subseq". Minor INCOMPATIBILITY.
+
* Theories "GCD" and "Binomial" are already included in "Main" (instead
of "Complex_Main").
--- a/src/Doc/Main/Main_Doc.thy Sun May 28 15:46:26 2017 +0200
+++ b/src/Doc/Main/Main_Doc.thy Mon May 29 09:14:15 2017 +0200
@@ -552,6 +552,7 @@
@{const List.map} & @{typeof List.map}\\
@{const List.measures} & @{term_type_only List.measures "('a\<Rightarrow>nat)list\<Rightarrow>('a*'a)set"}\\
@{const List.nth} & @{typeof List.nth}\\
+@{const List.nths} & @{typeof List.nths}\\
@{const List.remdups} & @{typeof List.remdups}\\
@{const List.removeAll} & @{typeof List.removeAll}\\
@{const List.remove1} & @{typeof List.remove1}\\
@@ -560,10 +561,10 @@
@{const List.rotate} & @{typeof List.rotate}\\
@{const List.rotate1} & @{typeof List.rotate1}\\
@{const List.set} & @{term_type_only List.set "'a list \<Rightarrow> 'a set"}\\
+@{const List.shuffle} & @{typeof List.shuffle}\\
@{const List.sort} & @{typeof List.sort}\\
@{const List.sorted} & @{typeof List.sorted}\\
@{const List.splice} & @{typeof List.splice}\\
-@{const List.sublist} & @{typeof List.sublist}\\
@{const List.take} & @{typeof List.take}\\
@{const List.takeWhile} & @{typeof List.takeWhile}\\
@{const List.tl} & @{typeof List.tl}\\
@@ -656,4 +657,4 @@
\<close>
(*<*)
end
-(*>*)
\ No newline at end of file
+(*>*)
--- a/src/HOL/Codegenerator_Test/Candidates.thy Sun May 28 15:46:26 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates.thy Mon May 29 09:14:15 2017 +0200
@@ -7,7 +7,7 @@
imports
Complex_Main
"~~/src/HOL/Library/Library"
- "~~/src/HOL/Library/Sublist_Order"
+ "~~/src/HOL/Library/Subseq_Order"
"~~/src/HOL/Data_Structures/Tree_Map"
"~~/src/HOL/Data_Structures/Tree_Set"
"~~/src/HOL/Computational_Algebra/Computational_Algebra"
--- a/src/HOL/Enum.thy Sun May 28 15:46:26 2017 +0200
+++ b/src/HOL/Enum.thy Mon May 29 09:14:15 2017 +0200
@@ -385,7 +385,7 @@
begin
definition
- "enum = map set (sublists enum)"
+ "enum = map set (subseqs enum)"
definition
"enum_all P \<longleftrightarrow> (\<forall>A\<in>set enum. P (A::'a set))"
@@ -394,7 +394,7 @@
"enum_ex P \<longleftrightarrow> (\<exists>A\<in>set enum. P (A::'a set))"
instance proof
-qed (simp_all add: enum_set_def enum_all_set_def enum_ex_set_def sublists_powset distinct_set_sublists
+qed (simp_all add: enum_set_def enum_all_set_def enum_ex_set_def subseqs_powset distinct_set_subseqs
enum_distinct enum_UNIV)
end
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Sun May 28 15:46:26 2017 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Mon May 29 09:14:15 2017 +0200
@@ -533,7 +533,7 @@
and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> Array.get h1 a ! p \<le> j"
by (auto simp add: all_in_set_subarray_conv)
from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
- length_remains 1(5) pivot mset_sublist [of l p "Array.get h1 a" "Array.get h2 a"]
+ length_remains 1(5) pivot mset_nths [of l p "Array.get h1 a" "Array.get h2 a"]
have multiset_partconds1: "mset (subarray l p a h2) = mset (subarray l p a h1)"
unfolding Array.length_def subarray_def by (cases p, auto)
with left_subarray_remains part_conds1 pivot_unchanged
@@ -544,7 +544,7 @@
have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
by (auto simp add: subarray_eq_samelength_iff)
from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
- length_remains 1(5) pivot mset_sublist [of "p + 1" "r + 1" "Array.get h2 a" "Array.get h' a"]
+ length_remains 1(5) pivot mset_nths [of "p + 1" "r + 1" "Array.get h2 a" "Array.get h' a"]
have multiset_partconds2: "mset (subarray (p + 1) (r + 1) a h') = mset (subarray (p + 1) (r + 1) a h2)"
unfolding Array.length_def subarray_def by auto
with right_subarray_remains part_conds2 pivot_unchanged
@@ -556,8 +556,8 @@
by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis
unfolding subarray_def
- apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv)
- by (auto simp add: set_sublist' dest: order.trans [of _ "Array.get h' a ! p"])
+ apply (auto simp add: sorted_append sorted_Cons all_in_set_nths'_conv)
+ by (auto simp add: set_nths' dest: order.trans [of _ "Array.get h' a ! p"])
}
with True cr show ?thesis
unfolding quicksort.simps [of a l r]
@@ -575,7 +575,7 @@
unfolding Array.length_def by simp
next
case False
- from quicksort_sorts [OF effect] False have "sorted (sublist' 0 (List.length (Array.get h a)) (Array.get h' a))"
+ from quicksort_sorts [OF effect] False have "sorted (nths' 0 (List.length (Array.get h a)) (Array.get h' a))"
unfolding Array.length_def subarray_def by auto
with length_remains[OF effect] have "sorted (Array.get h' a)"
unfolding Array.length_def by simp
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Sun May 28 15:46:26 2017 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Mon May 29 09:14:15 2017 +0200
@@ -99,7 +99,7 @@
}
with assms(2) rev_length[OF assms(1)] show ?thesis
unfolding subarray_def Array.length_def
- by (auto simp add: length_sublist' rev_nth min_def nth_sublist' intro!: nth_equalityI)
+ by (auto simp add: length_nths' rev_nth min_def nth_nths' intro!: nth_equalityI)
qed
lemma rev2_rev:
--- a/src/HOL/Imperative_HOL/ex/List_Sublist.thy Sun May 28 15:46:26 2017 +0200
+++ b/src/HOL/Imperative_HOL/ex/List_Sublist.thy Mon May 29 09:14:15 2017 +0200
@@ -8,10 +8,10 @@
imports "~~/src/HOL/Library/Multiset"
begin
-lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}"
+lemma nths_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> nths xs {i..<j} @ nths xs {j..<k} = nths xs {i..<k}"
apply (induct xs arbitrary: i j k)
apply simp
-apply (simp only: sublist_Cons)
+apply (simp only: nths_Cons)
apply simp
apply safe
apply simp
@@ -42,27 +42,27 @@
apply fastforce
done
-lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds"
+lemma nths_update1: "i \<notin> inds \<Longrightarrow> nths (xs[i := v]) inds = nths xs inds"
apply (induct xs arbitrary: i inds)
apply simp
apply (case_tac i)
-apply (simp add: sublist_Cons)
-apply (simp add: sublist_Cons)
+apply (simp add: nths_Cons)
+apply (simp add: nths_Cons)
done
-lemma sublist_update2: "i \<in> inds \<Longrightarrow> sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \<in> inds. k < i}):= v]"
+lemma nths_update2: "i \<in> inds \<Longrightarrow> nths (xs[i := v]) inds = (nths xs inds)[(card {k \<in> inds. k < i}):= v]"
proof (induct xs arbitrary: i inds)
case Nil thus ?case by simp
next
case (Cons x xs)
thus ?case
proof (cases i)
- case 0 with Cons show ?thesis by (simp add: sublist_Cons)
+ case 0 with Cons show ?thesis by (simp add: nths_Cons)
next
case (Suc i')
with Cons show ?thesis
apply simp
- apply (simp add: sublist_Cons)
+ apply (simp add: nths_Cons)
apply auto
apply (auto simp add: nat.split)
apply (simp add: card_less_Suc[symmetric])
@@ -71,82 +71,82 @@
qed
qed
-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)"
-by (simp add: sublist_update1 sublist_update2)
+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)"
+by (simp add: nths_update1 nths_update2)
-lemma sublist_take: "sublist xs {j. j < m} = take m xs"
+lemma nths_take: "nths xs {j. j < m} = take m xs"
apply (induct xs arbitrary: m)
apply simp
apply (case_tac m)
apply simp
-apply (simp add: sublist_Cons)
+apply (simp add: nths_Cons)
done
-lemma sublist_take': "sublist xs {0..<m} = take m xs"
+lemma nths_take': "nths xs {0..<m} = take m xs"
apply (induct xs arbitrary: m)
apply simp
apply (case_tac m)
apply simp
-apply (simp add: sublist_Cons sublist_take)
+apply (simp add: nths_Cons nths_take)
done
-lemma sublist_all[simp]: "sublist xs {j. j < length xs} = xs"
+lemma nths_all[simp]: "nths xs {j. j < length xs} = xs"
apply (induct xs)
apply simp
-apply (simp add: sublist_Cons)
+apply (simp add: nths_Cons)
done
-lemma sublist_all'[simp]: "sublist xs {0..<length xs} = xs"
+lemma nths_all'[simp]: "nths xs {0..<length xs} = xs"
apply (induct xs)
apply simp
-apply (simp add: sublist_Cons)
+apply (simp add: nths_Cons)
done
-lemma sublist_single: "a < length xs \<Longrightarrow> sublist xs {a} = [xs ! a]"
+lemma nths_single: "a < length xs \<Longrightarrow> nths xs {a} = [xs ! a]"
apply (induct xs arbitrary: a)
apply simp
apply(case_tac aa)
apply simp
-apply (simp add: sublist_Cons)
+apply (simp add: nths_Cons)
apply simp
-apply (simp add: sublist_Cons)
+apply (simp add: nths_Cons)
done
-lemma sublist_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> sublist xs inds = []"
+lemma nths_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> nths xs inds = []"
apply (induct xs arbitrary: inds)
apply simp
-apply (simp add: sublist_Cons)
+apply (simp add: nths_Cons)
apply auto
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
apply auto
done
-lemma sublist_Nil': "sublist xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs"
+lemma nths_Nil': "nths xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs"
apply (induct xs arbitrary: inds)
apply simp
-apply (simp add: sublist_Cons)
+apply (simp add: nths_Cons)
apply (auto split: if_splits)
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
apply (case_tac x, auto)
done
-lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)"
+lemma nths_Nil[simp]: "(nths xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)"
apply (induct xs arbitrary: inds)
apply simp
-apply (simp add: sublist_Cons)
+apply (simp add: nths_Cons)
apply auto
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
apply (case_tac x, auto)
done
-lemma sublist_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; sublist xs inds = sublist ys inds \<rbrakk> \<Longrightarrow> sublist xs inds' = sublist ys inds'"
+lemma nths_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; nths xs inds = nths ys inds \<rbrakk> \<Longrightarrow> nths xs inds' = nths ys inds'"
apply (induct xs arbitrary: ys inds inds')
apply simp
apply (drule sym, rule sym)
-apply (simp add: sublist_Nil, fastforce)
+apply (simp add: nths_Nil, fastforce)
apply (case_tac ys)
-apply (simp add: sublist_Nil, fastforce)
-apply (auto simp add: sublist_Cons)
+apply (simp add: nths_Nil, fastforce)
+apply (auto simp add: nths_Cons)
apply (erule_tac x="list" in meta_allE)
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
@@ -157,13 +157,13 @@
apply fastforce
done
-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"
+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"
apply (induct xs arbitrary: ys inds)
apply simp
-apply (rule sym, simp add: sublist_Nil)
+apply (rule sym, simp add: nths_Nil)
apply (case_tac ys)
-apply (simp add: sublist_Nil)
-apply (auto simp add: sublist_Cons)
+apply (simp add: nths_Nil)
+apply (auto simp add: nths_Cons)
apply (erule_tac x="list" in meta_allE)
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
apply fastforce
@@ -172,64 +172,64 @@
apply fastforce
done
-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"
-by (rule sublist_eq, auto)
+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"
+by (rule nths_eq, auto)
-lemma sublist_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist xs inds = sublist ys inds) = (\<forall>i \<in> inds. xs ! i = ys ! i)"
+lemma nths_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (nths xs inds = nths ys inds) = (\<forall>i \<in> inds. xs ! i = ys ! i)"
apply (induct xs arbitrary: ys inds)
apply simp
-apply (rule sym, simp add: sublist_Nil)
+apply (rule sym, simp add: nths_Nil)
apply (case_tac ys)
-apply (simp add: sublist_Nil)
-apply (auto simp add: sublist_Cons)
+apply (simp add: nths_Nil)
+apply (auto simp add: nths_Cons)
apply (case_tac i)
apply auto
apply (case_tac i)
apply auto
done
-section \<open>Another sublist function\<close>
+section \<open>Another nths function\<close>
-function sublist' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
+function nths' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
- "sublist' n m [] = []"
-| "sublist' n 0 xs = []"
-| "sublist' 0 (Suc m) (x#xs) = (x#sublist' 0 m xs)"
-| "sublist' (Suc n) (Suc m) (x#xs) = sublist' n m xs"
+ "nths' n m [] = []"
+| "nths' n 0 xs = []"
+| "nths' 0 (Suc m) (x#xs) = (x#nths' 0 m xs)"
+| "nths' (Suc n) (Suc m) (x#xs) = nths' n m xs"
by pat_completeness auto
termination by lexicographic_order
-subsection \<open>Proving equivalence to the other sublist command\<close>
+subsection \<open>Proving equivalence to the other nths command\<close>
-lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \<le> j \<and> j < m}"
+lemma nths'_nths: "nths' n m xs = nths xs {j. n \<le> j \<and> j < m}"
apply (induct xs arbitrary: n m)
apply simp
apply (case_tac n)
apply (case_tac m)
apply simp
-apply (simp add: sublist_Cons)
+apply (simp add: nths_Cons)
apply (case_tac m)
apply simp
-apply (simp add: sublist_Cons)
+apply (simp add: nths_Cons)
done
-lemma "sublist' n m xs = sublist xs {n..<m}"
+lemma "nths' n m xs = nths xs {n..<m}"
apply (induct xs arbitrary: n m)
apply simp
apply (case_tac n, case_tac m)
apply simp
apply simp
-apply (simp add: sublist_take')
+apply (simp add: nths_take')
apply (case_tac m)
apply simp
-apply (simp add: sublist_Cons sublist'_sublist)
+apply (simp add: nths_Cons nths'_nths)
done
subsection \<open>Showing equivalence to use of drop and take for definition\<close>
-lemma "sublist' n m xs = take (m - n) (drop n xs)"
+lemma "nths' n m xs = take (m - n) (drop n xs)"
apply (induct xs arbitrary: n m)
apply simp
apply (case_tac m)
@@ -239,25 +239,25 @@
apply simp
done
-subsection \<open>General lemma about sublist\<close>
+subsection \<open>General lemma about nths\<close>
-lemma sublist'_Nil[simp]: "sublist' i j [] = []"
+lemma nths'_Nil[simp]: "nths' i j [] = []"
by simp
-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)"
+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)"
by (cases i) auto
-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))"
+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))"
apply (cases j)
apply auto
apply (cases i)
apply auto
done
-lemma sublist_n_0: "sublist' n 0 xs = []"
+lemma nths_n_0: "nths' n 0 xs = []"
by (induct xs, auto)
-lemma sublist'_Nil': "n \<ge> m \<Longrightarrow> sublist' n m xs = []"
+lemma nths'_Nil': "n \<ge> m \<Longrightarrow> nths' n m xs = []"
apply (induct xs arbitrary: n m)
apply simp
apply (case_tac m)
@@ -267,7 +267,7 @@
apply simp
done
-lemma sublist'_Nil2: "n \<ge> length xs \<Longrightarrow> sublist' n m xs = []"
+lemma nths'_Nil2: "n \<ge> length xs \<Longrightarrow> nths' n m xs = []"
apply (induct xs arbitrary: n m)
apply simp
apply (case_tac m)
@@ -277,7 +277,7 @@
apply simp
done
-lemma sublist'_Nil3: "(sublist' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
+lemma nths'_Nil3: "(nths' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
apply (induct xs arbitrary: n m)
apply simp
apply (case_tac m)
@@ -287,7 +287,7 @@
apply simp
done
-lemma sublist'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> sublist' n m xs \<noteq> []"
+lemma nths'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> nths' n m xs \<noteq> []"
apply (induct xs arbitrary: n m)
apply simp
apply (case_tac m)
@@ -297,16 +297,16 @@
apply simp
done
-lemma sublist'_single: "n < length xs \<Longrightarrow> sublist' n (Suc n) xs = [xs ! n]"
+lemma nths'_single: "n < length xs \<Longrightarrow> nths' n (Suc n) xs = [xs ! n]"
apply (induct xs arbitrary: n)
apply simp
apply simp
apply (case_tac n)
-apply (simp add: sublist_n_0)
+apply (simp add: nths_n_0)
apply simp
done
-lemma sublist'_update1: "i \<ge> m \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
+lemma nths'_update1: "i \<ge> m \<Longrightarrow> nths' n m (xs[i:=v]) = nths' n m xs"
apply (induct xs arbitrary: n m i)
apply simp
apply simp
@@ -315,7 +315,7 @@
apply simp
done
-lemma sublist'_update2: "i < n \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
+lemma nths'_update2: "i < n \<Longrightarrow> nths' n m (xs[i:=v]) = nths' n m xs"
apply (induct xs arbitrary: n m i)
apply simp
apply simp
@@ -324,7 +324,7 @@
apply simp
done
-lemma sublist'_update3: "\<lbrakk>n \<le> i; i < m\<rbrakk> \<Longrightarrow> sublist' n m (xs[i := v]) = (sublist' n m xs)[i - n := v]"
+lemma nths'_update3: "\<lbrakk>n \<le> i; i < m\<rbrakk> \<Longrightarrow> nths' n m (xs[i := v]) = (nths' n m xs)[i - n := v]"
proof (induct xs arbitrary: n m i)
case Nil thus ?case by auto
next
@@ -339,14 +339,14 @@
done
qed
-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"
+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"
proof (induct xs arbitrary: i j ys n m)
case Nil
thus ?case
apply -
apply (rule sym, drule sym)
- apply (simp add: sublist'_Nil)
- apply (simp add: sublist'_Nil3)
+ apply (simp add: nths'_Nil)
+ apply (simp add: nths'_Nil3)
apply arith
done
next
@@ -354,7 +354,7 @@
note c = this
thus ?case
proof (cases m)
- case 0 thus ?thesis by (simp add: sublist_n_0)
+ case 0 thus ?thesis by (simp add: nths_n_0)
next
case (Suc m')
note a = this
@@ -363,7 +363,7 @@
case 0 note b = this
show ?thesis
proof (cases ys)
- case Nil with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3)
+ case Nil with a b Cons.prems show ?thesis by (simp add: nths'_Nil3)
next
case (Cons y ys)
show ?thesis
@@ -380,7 +380,7 @@
case (Suc n')
show ?thesis
proof (cases ys)
- case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3)
+ case Nil with Suc a Cons.prems show ?thesis by (auto simp add: nths'_Nil3)
next
case (Cons y ys) with Suc a Cons.prems show ?thesis
apply -
@@ -404,10 +404,10 @@
qed
qed
-lemma length_sublist': "j \<le> length xs \<Longrightarrow> length (sublist' i j xs) = j - i"
+lemma length_nths': "j \<le> length xs \<Longrightarrow> length (nths' i j xs) = j - i"
by (induct xs arbitrary: i j, auto)
-lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs"
+lemma nths'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> nths' i j xs = xs ! i # nths' (Suc i) j xs"
apply (induct xs arbitrary: i j)
apply simp
apply (case_tac j)
@@ -417,14 +417,14 @@
apply simp
done
-lemma sublist'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]"
+lemma nths'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> nths' i j xs = nths' i (j - 1) xs @ [xs ! (j - 1)]"
apply (induct xs arbitrary: i j)
apply simp
apply simp
done
(* suffices that j \<le> length xs and length ys *)
-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')"
+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')"
proof (induct xs arbitrary: ys i j)
case Nil thus ?case by simp
next
@@ -442,54 +442,54 @@
done
qed
-lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs"
+lemma nths'_all[simp]: "nths' 0 (length xs) xs = xs"
by (induct xs, auto)
-lemma sublist'_sublist': "sublist' n m (sublist' i j xs) = sublist' (i + n) (min (i + m) j) xs"
+lemma nths'_nths': "nths' n m (nths' i j xs) = nths' (i + n) (min (i + m) j) xs"
by (induct xs arbitrary: i j n m) (auto simp add: min_diff)
-lemma sublist'_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow>(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs"
+lemma nths'_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow>(nths' i j xs) @ (nths' j k xs) = nths' i k xs"
by (induct xs arbitrary: i j k) auto
-lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
+lemma nth_nths': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (nths' i j xs) ! k = xs ! (i + k)"
apply (induct xs arbitrary: i j k)
apply simp
apply (case_tac k)
apply auto
done
-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}"
-apply (simp add: sublist'_sublist)
-apply (simp add: set_sublist)
+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}"
+apply (simp add: nths'_nths)
+apply (simp add: set_nths)
apply auto
done
-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))"
-unfolding set_sublist' by blast
+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))"
+unfolding set_nths' by blast
-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))"
-unfolding set_sublist' by blast
+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))"
+unfolding set_nths' by blast
-lemma mset_sublist:
+lemma mset_nths:
assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
assumes multiset: "mset xs = mset ys"
- shows "mset (sublist' l r xs) = mset (sublist' l r ys)"
+ shows "mset (nths' l r xs) = mset (nths' l r ys)"
proof -
- from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long")
- by (simp add: sublist'_append)
+ from l_r have xs_def: "xs = (nths' 0 l xs) @ (nths' l r xs) @ (nths' r (List.length xs) xs)" (is "_ = ?xs_long")
+ by (simp add: nths'_append)
from multiset have length_eq: "List.length xs = List.length ys" by (rule mset_eq_length)
- with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long")
- by (simp add: sublist'_append)
+ with l_r have ys_def: "ys = (nths' 0 l ys) @ (nths' l r ys) @ (nths' r (List.length ys) ys)" (is "_ = ?ys_long")
+ by (simp add: nths'_append)
from xs_def ys_def multiset have "mset ?xs_long = mset ?ys_long" by simp
moreover
- from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
- by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
+ from left l_r length_eq have "nths' 0 l xs = nths' 0 l ys"
+ by (auto simp add: length_nths' nth_nths' intro!: nth_equalityI)
moreover
- from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
- by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
+ from right l_r length_eq have "nths' r (List.length xs) xs = nths' r (List.length ys) ys"
+ by (auto simp add: length_nths' nth_nths' intro!: nth_equalityI)
ultimately show ?thesis by (simp add: mset_append)
qed
--- a/src/HOL/Imperative_HOL/ex/Subarray.thy Sun May 28 15:46:26 2017 +0200
+++ b/src/HOL/Imperative_HOL/ex/Subarray.thy Mon May 29 09:14:15 2017 +0200
@@ -9,63 +9,63 @@
begin
definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where
- "subarray n m a h \<equiv> sublist' n m (Array.get h a)"
+ "subarray n m a h \<equiv> nths' n m (Array.get h a)"
lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
apply (simp add: subarray_def Array.update_def)
-apply (simp add: sublist'_update1)
+apply (simp add: nths'_update1)
done
lemma subarray_upd2: " i < n \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
apply (simp add: subarray_def Array.update_def)
-apply (subst sublist'_update2)
+apply (subst nths'_update2)
apply fastforce
apply simp
done
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]"
unfolding subarray_def Array.update_def
-by (simp add: sublist'_update3)
+by (simp add: nths'_update3)
lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
-by (simp add: subarray_def sublist'_Nil')
+by (simp add: subarray_def nths'_Nil')
lemma subarray_single: "\<lbrakk> n < Array.length h a \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [Array.get h a ! n]"
-by (simp add: subarray_def length_def sublist'_single)
+by (simp add: subarray_def length_def nths'_single)
lemma length_subarray: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray n m a h) = m - n"
-by (simp add: subarray_def length_def length_sublist')
+by (simp add: subarray_def length_def length_nths')
lemma length_subarray_0: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray 0 m a h) = m"
by (simp add: length_subarray)
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"
unfolding Array.length_def subarray_def
-by (simp add: sublist'_front)
+by (simp add: nths'_front)
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)]"
unfolding Array.length_def subarray_def
-by (simp add: sublist'_back)
+by (simp add: nths'_back)
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"
unfolding subarray_def
-by (simp add: sublist'_append)
+by (simp add: nths'_append)
lemma subarray_all: "subarray 0 (Array.length h a) a h = Array.get h a"
unfolding Array.length_def subarray_def
-by (simp add: sublist'_all)
+by (simp add: nths'_all)
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)"
unfolding Array.length_def subarray_def
-by (simp add: nth_sublist')
+by (simp add: nth_nths')
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')"
-unfolding Array.length_def subarray_def by (rule sublist'_eq_samelength_iff)
+unfolding Array.length_def subarray_def by (rule nths'_eq_samelength_iff)
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))"
-unfolding subarray_def Array.length_def by (rule all_in_set_sublist'_conv)
+unfolding subarray_def Array.length_def by (rule all_in_set_nths'_conv)
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))"
-unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv)
+unfolding subarray_def Array.length_def by (rule ball_in_set_nths'_conv)
end
--- a/src/HOL/Library/Sublist.thy Sun May 28 15:46:26 2017 +0200
+++ b/src/HOL/Library/Sublist.thy Mon May 29 09:14:15 2017 +0200
@@ -1,6 +1,7 @@
(* Title: HOL/Library/Sublist.thy
- Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
+ Author: Tobias Nipkow and Markus Wenzel, TU München
Author: Christian Sternagel, JAIST
+ Author: Manuel Eberl, TU München
*)
section \<open>List prefixes, suffixes, and homeomorphic embedding\<close>
@@ -214,7 +215,7 @@
subsection \<open>Prefixes\<close>
-fun prefixes where
+primrec prefixes where
"prefixes [] = [[]]" |
"prefixes (x#xs) = [] # map (op # x) (prefixes xs)"
@@ -700,7 +701,7 @@
subsection \<open>Suffixes\<close>
-fun suffixes where
+primrec suffixes where
"suffixes [] = [[]]"
| "suffixes (x#xs) = suffixes xs @ [x # xs]"
@@ -919,49 +920,48 @@
"list_emb P (x#xs) [] \<longleftrightarrow> False"
"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)"
by simp_all
-
+
-
-subsection \<open>Sublists (special case of homeomorphic embedding)\<close>
+subsection \<open>Subsequences (special case of homeomorphic embedding)\<close>
-abbreviation sublisteq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
- where "sublisteq xs ys \<equiv> list_emb (op =) xs ys"
+abbreviation subseq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+ where "subseq xs ys \<equiv> list_emb (op =) xs ys"
-definition strict_sublist where "strict_sublist xs ys \<longleftrightarrow> xs \<noteq> ys \<and> sublisteq xs ys"
+definition strict_subseq where "strict_subseq xs ys \<longleftrightarrow> xs \<noteq> ys \<and> subseq xs ys"
-lemma sublisteq_Cons2: "sublisteq xs ys \<Longrightarrow> sublisteq (x#xs) (x#ys)" by auto
+lemma subseq_Cons2: "subseq xs ys \<Longrightarrow> subseq (x#xs) (x#ys)" by auto
-lemma sublisteq_same_length:
- assumes "sublisteq xs ys" and "length xs = length ys" shows "xs = ys"
+lemma subseq_same_length:
+ assumes "subseq xs ys" and "length xs = length ys" shows "xs = ys"
using assms by (induct) (auto dest: list_emb_length)
-lemma not_sublisteq_length [simp]: "length ys < length xs \<Longrightarrow> \<not> sublisteq xs ys"
+lemma not_subseq_length [simp]: "length ys < length xs \<Longrightarrow> \<not> subseq xs ys"
by (metis list_emb_length linorder_not_less)
-lemma sublisteq_Cons': "sublisteq (x#xs) ys \<Longrightarrow> sublisteq xs ys"
+lemma subseq_Cons': "subseq (x#xs) ys \<Longrightarrow> subseq xs ys"
by (induct xs, simp, blast dest: list_emb_ConsD)
-lemma sublisteq_Cons2':
- assumes "sublisteq (x#xs) (x#ys)" shows "sublisteq xs ys"
- using assms by (cases) (rule sublisteq_Cons')
+lemma subseq_Cons2':
+ assumes "subseq (x#xs) (x#ys)" shows "subseq xs ys"
+ using assms by (cases) (rule subseq_Cons')
-lemma sublisteq_Cons2_neq:
- assumes "sublisteq (x#xs) (y#ys)"
- shows "x \<noteq> y \<Longrightarrow> sublisteq (x#xs) ys"
+lemma subseq_Cons2_neq:
+ assumes "subseq (x#xs) (y#ys)"
+ shows "x \<noteq> y \<Longrightarrow> subseq (x#xs) ys"
using assms by (cases) auto
-lemma sublisteq_Cons2_iff [simp]:
- "sublisteq (x#xs) (y#ys) = (if x = y then sublisteq xs ys else sublisteq (x#xs) ys)"
+lemma subseq_Cons2_iff [simp]:
+ "subseq (x#xs) (y#ys) = (if x = y then subseq xs ys else subseq (x#xs) ys)"
by simp
-lemma sublisteq_append': "sublisteq (zs @ xs) (zs @ ys) \<longleftrightarrow> sublisteq xs ys"
+lemma subseq_append': "subseq (zs @ xs) (zs @ ys) \<longleftrightarrow> subseq xs ys"
by (induct zs) simp_all
-interpretation sublist_order: order sublisteq strict_sublist
+interpretation subseq_order: order subseq strict_subseq
proof
fix xs ys :: "'a list"
{
- assume "sublisteq xs ys" and "sublisteq ys xs"
+ assume "subseq xs ys" and "subseq ys xs"
thus "xs = ys"
proof (induct)
case list_emb_Nil
@@ -971,34 +971,34 @@
thus ?case by simp
next
case list_emb_Cons
- hence False using sublisteq_Cons' by fastforce
+ hence False using subseq_Cons' by fastforce
thus ?case ..
qed
}
- thus "strict_sublist xs ys \<longleftrightarrow> (sublisteq xs ys \<and> \<not>sublisteq ys xs)"
- by (auto simp: strict_sublist_def)
+ thus "strict_subseq xs ys \<longleftrightarrow> (subseq xs ys \<and> \<not>subseq ys xs)"
+ by (auto simp: strict_subseq_def)
qed (auto simp: list_emb_refl intro: list_emb_trans)
-lemma in_set_sublists [simp]: "xs \<in> set (sublists ys) \<longleftrightarrow> sublisteq xs ys"
+lemma in_set_subseqs [simp]: "xs \<in> set (subseqs ys) \<longleftrightarrow> subseq xs ys"
proof
- assume "xs \<in> set (sublists ys)"
- thus "sublisteq xs ys"
+ assume "xs \<in> set (subseqs ys)"
+ thus "subseq xs ys"
by (induction ys arbitrary: xs) (auto simp: Let_def)
next
- have [simp]: "[] \<in> set (sublists ys)" for ys :: "'a list"
+ have [simp]: "[] \<in> set (subseqs ys)" for ys :: "'a list"
by (induction ys) (auto simp: Let_def)
- assume "sublisteq xs ys"
- thus "xs \<in> set (sublists ys)"
+ assume "subseq xs ys"
+ thus "xs \<in> set (subseqs ys)"
by (induction xs ys rule: list_emb.induct) (auto simp: Let_def)
qed
-lemma set_sublists_eq: "set (sublists ys) = {xs. sublisteq xs ys}"
+lemma set_subseqs_eq: "set (subseqs ys) = {xs. subseq xs ys}"
by auto
-lemma sublisteq_append_le_same_iff: "sublisteq (xs @ ys) ys \<longleftrightarrow> xs = []"
+lemma subseq_append_le_same_iff: "subseq (xs @ ys) ys \<longleftrightarrow> xs = []"
by (auto dest: list_emb_length)
-lemma sublisteq_singleton_left: "sublisteq [x] ys \<longleftrightarrow> x \<in> set ys"
+lemma subseq_singleton_left: "subseq [x] ys \<longleftrightarrow> x \<in> set ys"
by (fastforce dest: list_emb_ConsD split_list_last)
lemma list_emb_append_mono:
@@ -1012,11 +1012,11 @@
subsection \<open>Appending elements\<close>
-lemma sublisteq_append [simp]:
- "sublisteq (xs @ zs) (ys @ zs) \<longleftrightarrow> sublisteq xs ys" (is "?l = ?r")
+lemma subseq_append [simp]:
+ "subseq (xs @ zs) (ys @ zs) \<longleftrightarrow> subseq xs ys" (is "?l = ?r")
proof
- { fix xs' ys' xs ys zs :: "'a list" assume "sublisteq xs' ys'"
- then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> sublisteq xs ys"
+ { fix xs' ys' xs ys zs :: "'a list" assume "subseq xs' ys'"
+ then have "xs' = xs @ zs & ys' = ys @ zs \<longrightarrow> subseq xs ys"
proof (induct arbitrary: xs ys zs)
case list_emb_Nil show ?case by simp
next
@@ -1038,11 +1038,11 @@
moreover assume ?l
ultimately show ?r by blast
next
- assume ?r then show ?l by (metis list_emb_append_mono sublist_order.order_refl)
+ assume ?r then show ?l by (metis list_emb_append_mono subseq_order.order_refl)
qed
-lemma sublisteq_append_iff:
- "sublisteq xs (ys @ zs) \<longleftrightarrow> (\<exists>xs1 xs2. xs = xs1 @ xs2 \<and> sublisteq xs1 ys \<and> sublisteq xs2 zs)"
+lemma subseq_append_iff:
+ "subseq xs (ys @ zs) \<longleftrightarrow> (\<exists>xs1 xs2. xs = xs1 @ xs2 \<and> subseq xs1 ys \<and> subseq xs2 zs)"
(is "?lhs = ?rhs")
proof
assume ?lhs thus ?rhs
@@ -1058,61 +1058,315 @@
qed auto
qed (auto intro: list_emb_append_mono)
-lemma sublisteq_appendE [case_names append]:
- assumes "sublisteq xs (ys @ zs)"
- obtains xs1 xs2 where "xs = xs1 @ xs2" "sublisteq xs1 ys" "sublisteq xs2 zs"
- using assms by (subst (asm) sublisteq_append_iff) auto
+lemma subseq_appendE [case_names append]:
+ assumes "subseq xs (ys @ zs)"
+ obtains xs1 xs2 where "xs = xs1 @ xs2" "subseq xs1 ys" "subseq xs2 zs"
+ using assms by (subst (asm) subseq_append_iff) auto
-lemma sublisteq_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (zs @ ys)"
+lemma subseq_drop_many: "subseq xs ys \<Longrightarrow> subseq xs (zs @ ys)"
by (induct zs) auto
-lemma sublisteq_rev_drop_many: "sublisteq xs ys \<Longrightarrow> sublisteq xs (ys @ zs)"
+lemma subseq_rev_drop_many: "subseq xs ys \<Longrightarrow> subseq xs (ys @ zs)"
by (metis append_Nil2 list_emb_Nil list_emb_append_mono)
subsection \<open>Relation to standard list operations\<close>
-lemma sublisteq_map:
- assumes "sublisteq xs ys" shows "sublisteq (map f xs) (map f ys)"
+lemma subseq_map:
+ assumes "subseq xs ys" shows "subseq (map f xs) (map f ys)"
using assms by (induct) auto
-lemma sublisteq_filter_left [simp]: "sublisteq (filter P xs) xs"
+lemma subseq_filter_left [simp]: "subseq (filter P xs) xs"
by (induct xs) auto
-lemma sublisteq_filter [simp]:
- assumes "sublisteq xs ys" shows "sublisteq (filter P xs) (filter P ys)"
+lemma subseq_filter [simp]:
+ assumes "subseq xs ys" shows "subseq (filter P xs) (filter P ys)"
using assms by induct auto
-lemma "sublisteq xs ys \<longleftrightarrow> (\<exists>N. xs = sublist ys N)" (is "?L = ?R")
+lemma subseq_conv_nths:
+ "subseq xs ys \<longleftrightarrow> (\<exists>N. xs = nths ys N)" (is "?L = ?R")
proof
assume ?L
then show ?R
proof (induct)
- case list_emb_Nil show ?case by (metis sublist_empty)
+ case list_emb_Nil show ?case by (metis nths_empty)
next
case (list_emb_Cons xs ys x)
- then obtain N where "xs = sublist ys N" by blast
- then have "xs = sublist (x#ys) (Suc ` N)"
- by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
+ then obtain N where "xs = nths ys N" by blast
+ then have "xs = nths (x#ys) (Suc ` N)"
+ by (clarsimp simp add: nths_Cons inj_image_mem_iff)
then show ?case by blast
next
case (list_emb_Cons2 x y xs ys)
- then obtain N where "xs = sublist ys N" by blast
- then have "x#xs = sublist (x#ys) (insert 0 (Suc ` N))"
- by (clarsimp simp add:sublist_Cons inj_image_mem_iff)
+ then obtain N where "xs = nths ys N" by blast
+ then have "x#xs = nths (x#ys) (insert 0 (Suc ` N))"
+ by (clarsimp simp add: nths_Cons inj_image_mem_iff)
moreover from list_emb_Cons2 have "x = y" by simp
ultimately show ?case by blast
qed
next
assume ?R
- then obtain N where "xs = sublist ys N" ..
- moreover have "sublisteq (sublist ys N) ys"
+ then obtain N where "xs = nths ys N" ..
+ moreover have "subseq (nths ys N) ys"
proof (induct ys arbitrary: N)
case Nil show ?case by simp
next
- case Cons then show ?case by (auto simp: sublist_Cons)
+ case Cons then show ?case by (auto simp: nths_Cons)
qed
ultimately show ?L by simp
qed
+
+
+subsection \<open>Contiguous sublists\<close>
+
+definition sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+ "sublist xs ys = (\<exists>ps ss. ys = ps @ xs @ ss)"
+
+definition strict_sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+ "strict_sublist xs ys \<longleftrightarrow> sublist xs ys \<and> xs \<noteq> ys"
+
+interpretation sublist_order: order sublist strict_sublist
+proof
+ fix xs ys zs :: "'a list"
+ assume "sublist xs ys" "sublist ys zs"
+ then obtain xs1 xs2 ys1 ys2 where "ys = xs1 @ xs @ xs2" "zs = ys1 @ ys @ ys2"
+ by (auto simp: sublist_def)
+ hence "zs = (ys1 @ xs1) @ xs @ (xs2 @ ys2)" by simp
+ thus "sublist xs zs" unfolding sublist_def by blast
+next
+ fix xs ys :: "'a list"
+ {
+ assume "sublist xs ys" "sublist ys xs"
+ then obtain as bs cs ds
+ where xs: "xs = as @ ys @ bs" and ys: "ys = cs @ xs @ ds"
+ by (auto simp: sublist_def)
+ have "xs = as @ cs @ xs @ ds @ bs" by (subst xs, subst ys) auto
+ also have "length \<dots> = length as + length cs + length xs + length bs + length ds"
+ by simp
+ finally have "as = []" "bs = []" by simp_all
+ with xs show "xs = ys" by simp
+ }
+ thus "strict_sublist xs ys \<longleftrightarrow> (sublist xs ys \<and> \<not>sublist ys xs)"
+ by (auto simp: strict_sublist_def)
+qed (auto simp: strict_sublist_def sublist_def intro: exI[of _ "[]"])
+
+lemma sublist_Nil_left [simp, intro]: "sublist [] ys"
+ by (auto simp: sublist_def)
+
+lemma sublist_Cons_Nil [simp]: "\<not>sublist (x#xs) []"
+ by (auto simp: sublist_def)
+
+lemma sublist_Nil_right [simp]: "sublist xs [] \<longleftrightarrow> xs = []"
+ by (cases xs) auto
+
+lemma sublist_appendI [simp, intro]: "sublist xs (ps @ xs @ ss)"
+ by (auto simp: sublist_def)
+
+lemma sublist_append_leftI [simp, intro]: "sublist xs (ps @ xs)"
+ by (auto simp: sublist_def intro: exI[of _ "[]"])
+
+lemma sublist_append_rightI [simp, intro]: "sublist xs (xs @ ss)"
+ by (auto simp: sublist_def intro: exI[of _ "[]"])
+
+lemma sublist_altdef: "sublist xs ys \<longleftrightarrow> (\<exists>ys'. prefix ys' ys \<and> suffix xs ys')"
+proof safe
+ assume "sublist xs ys"
+ then obtain ps ss where "ys = ps @ xs @ ss" by (auto simp: sublist_def)
+ thus "\<exists>ys'. prefix ys' ys \<and> suffix xs ys'"
+ by (intro exI[of _ "ps @ xs"] conjI suffix_appendI) auto
+next
+ fix ys'
+ assume "prefix ys' ys" "suffix xs ys'"
+ thus "sublist xs ys" by (auto simp: prefix_def suffix_def)
+qed
+
+lemma sublist_altdef': "sublist xs ys \<longleftrightarrow> (\<exists>ys'. suffix ys' ys \<and> prefix xs ys')"
+proof safe
+ assume "sublist xs ys"
+ then obtain ps ss where "ys = ps @ xs @ ss" by (auto simp: sublist_def)
+ thus "\<exists>ys'. suffix ys' ys \<and> prefix xs ys'"
+ by (intro exI[of _ "xs @ ss"] conjI suffixI) auto
+next
+ fix ys'
+ assume "suffix ys' ys" "prefix xs ys'"
+ thus "sublist xs ys" by (auto simp: prefix_def suffix_def)
+qed
+
+lemma sublist_Cons_right: "sublist xs (y # ys) \<longleftrightarrow> prefix xs (y # ys) \<or> sublist xs ys"
+ by (auto simp: sublist_def prefix_def Cons_eq_append_conv)
+
+lemma sublist_code [code]:
+ "sublist [] ys \<longleftrightarrow> True"
+ "sublist (x # xs) [] \<longleftrightarrow> False"
+ "sublist (x # xs) (y # ys) \<longleftrightarrow> prefix (x # xs) (y # ys) \<or> sublist (x # xs) ys"
+ by (simp_all add: sublist_Cons_right)
+
+
+lemma sublist_append:
+ "sublist xs (ys @ zs) \<longleftrightarrow>
+ sublist xs ys \<or> sublist xs zs \<or> (\<exists>xs1 xs2. xs = xs1 @ xs2 \<and> suffix xs1 ys \<and> prefix xs2 zs)"
+ by (auto simp: sublist_altdef prefix_append suffix_append)
+
+primrec sublists :: "'a list \<Rightarrow> 'a list list" where
+ "sublists [] = [[]]"
+| "sublists (x # xs) = sublists xs @ map (op # x) (prefixes xs)"
+
+lemma in_set_sublists [simp]: "xs \<in> set (sublists ys) \<longleftrightarrow> sublist xs ys"
+ by (induction ys arbitrary: xs) (auto simp: sublist_Cons_right prefix_Cons)
+
+lemma set_sublists_eq: "set (sublists xs) = {ys. sublist ys xs}"
+ by auto
+
+lemma length_sublists [simp]: "length (sublists xs) = Suc (length xs * Suc (length xs) div 2)"
+ by (induction xs) simp_all
+
+lemma sublist_length_le: "sublist xs ys \<Longrightarrow> length xs \<le> length ys"
+ by (auto simp add: sublist_def)
+
+lemma set_mono_sublist: "sublist xs ys \<Longrightarrow> set xs \<subseteq> set ys"
+ by (auto simp add: sublist_def)
+
+lemma prefix_imp_sublist [simp, intro]: "prefix xs ys \<Longrightarrow> sublist xs ys"
+ by (auto simp: sublist_def prefix_def intro: exI[of _ "[]"])
+
+lemma suffix_imp_sublist [simp, intro]: "suffix xs ys \<Longrightarrow> sublist xs ys"
+ by (auto simp: sublist_def suffix_def intro: exI[of _ "[]"])
+
+lemma sublist_take [simp, intro]: "sublist (take n xs) xs"
+ by (rule prefix_imp_sublist) (simp_all add: take_is_prefix)
+
+lemma sublist_drop [simp, intro]: "sublist (drop n xs) xs"
+ by (rule suffix_imp_sublist) (simp_all add: suffix_drop)
+
+lemma sublist_tl [simp, intro]: "sublist (tl xs) xs"
+ by (rule suffix_imp_sublist) (simp_all add: suffix_drop)
+
+lemma sublist_butlast [simp, intro]: "sublist (butlast xs) xs"
+ by (rule prefix_imp_sublist) (simp_all add: prefixeq_butlast)
+
+lemma sublist_rev [simp]: "sublist (rev xs) (rev ys) = sublist xs ys"
+proof
+ assume "sublist (rev xs) (rev ys)"
+ then obtain as bs where "rev ys = as @ rev xs @ bs"
+ by (auto simp: sublist_def)
+ also have "rev \<dots> = rev bs @ xs @ rev as" by simp
+ finally show "sublist xs ys" by simp
+next
+ assume "sublist xs ys"
+ then obtain as bs where "ys = as @ xs @ bs"
+ by (auto simp: sublist_def)
+ also have "rev \<dots> = rev bs @ rev xs @ rev as" by simp
+ finally show "sublist (rev xs) (rev ys)" by simp
+qed
+
+lemma sublist_rev_left: "sublist (rev xs) ys = sublist xs (rev ys)"
+ by (subst sublist_rev [symmetric]) (simp only: rev_rev_ident)
+
+lemma sublist_rev_right: "sublist xs (rev ys) = sublist (rev xs) ys"
+ by (subst sublist_rev [symmetric]) (simp only: rev_rev_ident)
+
+lemma snoc_sublist_snoc:
+ "sublist (xs @ [x]) (ys @ [y]) \<longleftrightarrow>
+ (x = y \<and> suffix xs ys \<or> sublist (xs @ [x]) ys) "
+ by (subst (1 2) sublist_rev [symmetric])
+ (simp del: sublist_rev add: sublist_Cons_right suffix_to_prefix)
+
+lemma sublist_snoc:
+ "sublist xs (ys @ [y]) \<longleftrightarrow> suffix xs (ys @ [y]) \<or> sublist xs ys"
+ by (subst (1 2) sublist_rev [symmetric])
+ (simp del: sublist_rev add: sublist_Cons_right suffix_to_prefix)
+
+subsection \<open>Parametricity\<close>
+
+context includes lifting_syntax
+begin
+
+private lemma prefix_primrec:
+ "prefix = rec_list (\<lambda>xs. True) (\<lambda>x xs xsa ys.
+ case ys of [] \<Rightarrow> False | y # ys \<Rightarrow> x = y \<and> xsa ys)"
+proof (intro ext, goal_cases)
+ case (1 xs ys)
+ show ?case by (induction xs arbitrary: ys) (auto simp: prefix_Cons split: list.splits)
+qed
+
+private lemma sublist_primrec:
+ "sublist = (\<lambda>xs ys. rec_list (\<lambda>xs. xs = []) (\<lambda>y ys ysa xs. prefix xs (y # ys) \<or> ysa xs) ys xs)"
+proof (intro ext, goal_cases)
+ case (1 xs ys)
+ show ?case by (induction ys) (auto simp: sublist_Cons_right)
+qed
+
+private lemma list_emb_primrec:
+ "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
+ | x # xs \<Rightarrow> if P x y then ysa P xs else ysa P (x # xs)) uuaa uu uua)"
+proof (intro ext, goal_cases)
+ case (1 P xs ys)
+ show ?case
+ by (induction ys arbitrary: xs)
+ (auto simp: list_emb_code List.null_def split: list.splits)
+qed
+
+lemma prefix_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A"
+ shows "(list_all2 A ===> list_all2 A ===> op =) prefix prefix"
+ unfolding prefix_primrec by transfer_prover
+
+lemma suffix_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A"
+ shows "(list_all2 A ===> list_all2 A ===> op =) suffix suffix"
+ unfolding suffix_to_prefix [abs_def] by transfer_prover
+
+lemma sublist_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A"
+ shows "(list_all2 A ===> list_all2 A ===> op =) sublist sublist"
+ unfolding sublist_primrec by transfer_prover
+
+lemma parallel_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A"
+ shows "(list_all2 A ===> list_all2 A ===> op =) parallel parallel"
+ unfolding parallel_def by transfer_prover
+
+
+
+lemma list_emb_transfer [transfer_rule]:
+ "((A ===> A ===> op =) ===> list_all2 A ===> list_all2 A ===> op =) list_emb list_emb"
+ unfolding list_emb_primrec by transfer_prover
+
+lemma strict_prefix_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A"
+ shows "(list_all2 A ===> list_all2 A ===> op =) strict_prefix strict_prefix"
+ unfolding strict_prefix_def by transfer_prover
+
+lemma strict_suffix_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A"
+ shows "(list_all2 A ===> list_all2 A ===> op =) strict_suffix strict_suffix"
+ unfolding strict_suffix_def by transfer_prover
+
+lemma strict_subseq_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A"
+ shows "(list_all2 A ===> list_all2 A ===> op =) strict_subseq strict_subseq"
+ unfolding strict_subseq_def by transfer_prover
+
+lemma strict_sublist_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A"
+ shows "(list_all2 A ===> list_all2 A ===> op =) strict_sublist strict_sublist"
+ unfolding strict_sublist_def by transfer_prover
+
+lemma prefixes_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A"
+ shows "(list_all2 A ===> list_all2 (list_all2 A)) prefixes prefixes"
+ unfolding prefixes_def by transfer_prover
+
+lemma suffixes_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A"
+ shows "(list_all2 A ===> list_all2 (list_all2 A)) suffixes suffixes"
+ unfolding suffixes_def by transfer_prover
+
+lemma sublists_transfer [transfer_rule]:
+ assumes [transfer_rule]: "bi_unique A"
+ shows "(list_all2 A ===> list_all2 (list_all2 A)) sublists sublists"
+ unfolding sublists_def by transfer_prover
end
+
+end
--- a/src/HOL/Library/Sublist_Order.thy Sun May 28 15:46:26 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-(* Title: HOL/Library/Sublist_Order.thy
- Author: Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
- Author: Florian Haftmann, , TU Muenchen
- Author: Tobias Nipkow, TU Muenchen
-*)
-
-section \<open>Sublist Ordering\<close>
-
-theory Sublist_Order
-imports Sublist
-begin
-
-text \<open>
- This theory defines sublist ordering on lists. A list \<open>ys\<close> is a sublist of a
- list \<open>xs\<close>, iff one obtains \<open>ys\<close> by erasing some elements from \<open>xs\<close>.
-\<close>
-
-subsection \<open>Definitions and basic lemmas\<close>
-
-instantiation list :: (type) ord
-begin
-
-definition "xs \<le> ys \<longleftrightarrow> sublisteq xs ys" for xs ys :: "'a list"
-definition "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list"
-
-instance ..
-
-end
-
-instance list :: (type) order
-proof
- fix xs ys zs :: "'a list"
- show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
- unfolding less_list_def ..
- show "xs \<le> xs"
- by (simp add: less_eq_list_def)
- show "xs = ys" if "xs \<le> ys" and "ys \<le> xs"
- using that unfolding less_eq_list_def by (rule sublist_order.antisym)
- show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs"
- using that unfolding less_eq_list_def by (rule sublist_order.order_trans)
-qed
-
-lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
- list_emb.induct [of "op =", folded less_eq_list_def]
-lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "op =", folded less_eq_list_def]
-lemmas le_list_Cons2_iff [simp, code] = sublisteq_Cons2_iff [folded less_eq_list_def]
-lemmas le_list_map = sublisteq_map [folded less_eq_list_def]
-lemmas le_list_filter = sublisteq_filter [folded less_eq_list_def]
-lemmas le_list_length = list_emb_length [of "op =", folded less_eq_list_def]
-
-lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
- by (metis list_emb_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def)
-
-lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
- by (metis less_eq_list_def list_emb_Nil order_less_le)
-
-lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
- by (metis list_emb_Nil less_eq_list_def less_list_def)
-
-lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
- by (unfold less_le less_eq_list_def) (auto)
-
-lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
- by (metis sublisteq_Cons2_iff less_list_def less_eq_list_def)
-
-lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
- by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le
- self_append_conv2 less_eq_list_def)
-
-lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
- by (metis less_list_def less_eq_list_def sublisteq_append')
-
-lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
- by (unfold less_le less_eq_list_def) auto
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Subseq_Order.thy Mon May 29 09:14:15 2017 +0200
@@ -0,0 +1,76 @@
+(* Title: HOL/Library/Subseq_Order.thy
+ Author: Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
+ Author: Florian Haftmann, TU Muenchen
+ Author: Tobias Nipkow, TU Muenchen
+*)
+
+section \<open>Subsequence Ordering\<close>
+
+theory Subseq_Order
+imports Sublist
+begin
+
+text \<open>
+ This theory defines subsequence ordering on lists. A list \<open>ys\<close> is a subsequence of a
+ list \<open>xs\<close>, iff one obtains \<open>ys\<close> by erasing some elements from \<open>xs\<close>.
+\<close>
+
+subsection \<open>Definitions and basic lemmas\<close>
+
+instantiation list :: (type) ord
+begin
+
+definition "xs \<le> ys \<longleftrightarrow> subseq xs ys" for xs ys :: "'a list"
+definition "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list"
+
+instance ..
+
+end
+
+instance list :: (type) order
+proof
+ fix xs ys zs :: "'a list"
+ show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
+ unfolding less_list_def ..
+ show "xs \<le> xs"
+ by (simp add: less_eq_list_def)
+ show "xs = ys" if "xs \<le> ys" and "ys \<le> xs"
+ using that unfolding less_eq_list_def by (rule subseq_order.antisym)
+ show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs"
+ using that unfolding less_eq_list_def by (rule subseq_order.order_trans)
+qed
+
+lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
+ list_emb.induct [of "op =", folded less_eq_list_def]
+lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "op =", folded less_eq_list_def]
+lemmas le_list_Cons2_iff [simp, code] = subseq_Cons2_iff [folded less_eq_list_def]
+lemmas le_list_map = subseq_map [folded less_eq_list_def]
+lemmas le_list_filter = subseq_filter [folded less_eq_list_def]
+lemmas le_list_length = list_emb_length [of "op =", folded less_eq_list_def]
+
+lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
+ by (metis list_emb_length subseq_same_length le_neq_implies_less less_list_def less_eq_list_def)
+
+lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
+ by (metis less_eq_list_def list_emb_Nil order_less_le)
+
+lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
+ by (metis list_emb_Nil less_eq_list_def less_list_def)
+
+lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
+ by (unfold less_le less_eq_list_def) (auto)
+
+lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
+ by (metis subseq_Cons2_iff less_list_def less_eq_list_def)
+
+lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
+ by (metis subseq_append_le_same_iff subseq_drop_many order_less_le
+ self_append_conv2 less_eq_list_def)
+
+lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
+ by (metis less_list_def less_eq_list_def subseq_append')
+
+lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
+ by (unfold less_le less_eq_list_def) auto
+
+end
--- a/src/HOL/List.thy Sun May 28 15:46:26 2017 +0200
+++ b/src/HOL/List.thy Mon May 29 09:14:15 2017 +0200
@@ -242,12 +242,12 @@
definition rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"rotate n = rotate1 ^^ n"
-definition sublist :: "'a list => nat set => 'a list" where
-"sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
-
-primrec sublists :: "'a list \<Rightarrow> 'a list list" where
-"sublists [] = [[]]" |
-"sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
+definition nths :: "'a list => nat set => 'a list" where
+"nths xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
+
+primrec subseqs :: "'a list \<Rightarrow> 'a list list" where
+"subseqs [] = [[]]" |
+"subseqs (x#xs) = (let xss = subseqs xs in map (Cons x) xss @ xss)"
primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
"n_lists 0 xs = [[]]" |
@@ -315,8 +315,8 @@
@{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
@{lemma "nth [a,b,c,d] 2 = c" by simp}\\
@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
-@{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
-@{lemma "sublists [a,b] = [[a, b], [a], [b], []]" by simp}\\
+@{lemma "nths [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:nths_def)}\\
+@{lemma "subseqs [a,b] = [[a, b], [a], [b], []]" by simp}\\
@{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)}\\
@{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\
@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\
@@ -4333,19 +4333,19 @@
using mod_less_divisor[of "length xs" n] by arith
-subsubsection \<open>@{const sublist} --- a generalization of @{const nth} to sets\<close>
-
-lemma sublist_empty [simp]: "sublist xs {} = []"
-by (auto simp add: sublist_def)
-
-lemma sublist_nil [simp]: "sublist [] A = []"
-by (auto simp add: sublist_def)
-
-lemma length_sublist:
- "length(sublist xs I) = card{i. i < length xs \<and> i : I}"
-by(simp add: sublist_def length_filter_conv_card cong:conj_cong)
-
-lemma sublist_shift_lemma_Suc:
+subsubsection \<open>@{const nths} --- a generalization of @{const nth} to sets\<close>
+
+lemma nths_empty [simp]: "nths xs {} = []"
+by (auto simp add: nths_def)
+
+lemma nths_nil [simp]: "nths [] A = []"
+by (auto simp add: nths_def)
+
+lemma length_nths:
+ "length (nths xs I) = card{i. i < length xs \<and> i : I}"
+by(simp add: nths_def length_filter_conv_card cong:conj_cong)
+
+lemma nths_shift_lemma_Suc:
"map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
apply(induct xs arbitrary: "is")
@@ -4355,92 +4355,88 @@
apply simp
done
-lemma sublist_shift_lemma:
+lemma nths_shift_lemma:
"map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
by (induct xs rule: rev_induct) (simp_all add: add.commute)
-lemma sublist_append:
- "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
-apply (unfold sublist_def)
+lemma nths_append:
+ "nths (l @ l') A = nths l A @ nths l' {j. j + length l : A}"
+apply (unfold nths_def)
apply (induct l' rule: rev_induct, simp)
-apply (simp add: upt_add_eq_append[of 0] sublist_shift_lemma)
+apply (simp add: upt_add_eq_append[of 0] nths_shift_lemma)
apply (simp add: add.commute)
done
-lemma sublist_Cons:
-"sublist (x # l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}"
+lemma nths_Cons:
+"nths (x # l) A = (if 0:A then [x] else []) @ nths l {j. Suc j : A}"
apply (induct l rule: rev_induct)
- apply (simp add: sublist_def)
-apply (simp del: append_Cons add: append_Cons[symmetric] sublist_append)
+ apply (simp add: nths_def)
+apply (simp del: append_Cons add: append_Cons[symmetric] nths_append)
done
-lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
+lemma set_nths: "set(nths xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
apply(induct xs arbitrary: I)
-apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
+apply(auto simp: nths_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
done
-lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
-by(auto simp add:set_sublist)
-
-lemma notin_set_sublistI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(sublist xs I)"
-by(auto simp add:set_sublist)
-
-lemma in_set_sublistD: "x \<in> set(sublist xs I) \<Longrightarrow> x \<in> set xs"
-by(auto simp add:set_sublist)
-
-lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"
-by (simp add: sublist_Cons)
-
-
-lemma distinct_sublistI[simp]: "distinct xs \<Longrightarrow> distinct(sublist xs I)"
-apply(induct xs arbitrary: I)
- apply simp
-apply(auto simp add:sublist_Cons)
-done
-
-
-lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"
-apply (induct l rule: rev_induct, simp)
-apply (simp split: nat_diff_split add: sublist_append)
-done
-
-lemma filter_in_sublist:
- "distinct xs \<Longrightarrow> filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"
+lemma set_nths_subset: "set(nths xs I) \<subseteq> set xs"
+by(auto simp add:set_nths)
+
+lemma notin_set_nthsI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(nths xs I)"
+by(auto simp add:set_nths)
+
+lemma in_set_nthsD: "x \<in> set(nths xs I) \<Longrightarrow> x \<in> set xs"
+by(auto simp add:set_nths)
+
+lemma nths_singleton [simp]: "nths [x] A = (if 0 : A then [x] else [])"
+by (simp add: nths_Cons)
+
+
+lemma distinct_nthsI[simp]: "distinct xs \<Longrightarrow> distinct (nths xs I)"
+ by (induct xs arbitrary: I) (auto simp: nths_Cons)
+
+
+lemma nths_upt_eq_take [simp]: "nths l {..<n} = take n l"
+ by (induct l rule: rev_induct)
+ (simp_all split: nat_diff_split add: nths_append)
+
+lemma filter_in_nths:
+ "distinct xs \<Longrightarrow> filter (%x. x \<in> set (nths xs s)) xs = nths xs s"
proof (induct xs arbitrary: s)
case Nil thus ?case by simp
next
case (Cons a xs)
then have "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
- with Cons show ?case by(simp add: sublist_Cons cong:filter_cong)
+ with Cons show ?case by(simp add: nths_Cons cong:filter_cong)
qed
-subsubsection \<open>@{const sublists} and @{const List.n_lists}\<close>
-
-lemma length_sublists: "length (sublists xs) = 2 ^ length xs"
+subsubsection \<open>@{const subseqs} and @{const List.n_lists}\<close>
+
+lemma length_subseqs: "length (subseqs xs) = 2 ^ length xs"
by (induct xs) (simp_all add: Let_def)
-lemma sublists_powset: "set ` set (sublists xs) = Pow (set xs)"
+lemma subseqs_powset: "set ` set (subseqs xs) = Pow (set xs)"
proof -
have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
by (auto simp add: image_def)
- have "set (map set (sublists xs)) = Pow (set xs)"
+ have "set (map set (subseqs xs)) = Pow (set xs)"
by (induct xs) (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
then show ?thesis by simp
qed
-lemma distinct_set_sublists:
+lemma distinct_set_subseqs:
assumes "distinct xs"
- shows "distinct (map set (sublists xs))"
+ shows "distinct (map set (subseqs xs))"
proof (rule card_distinct)
have "finite (set xs)" ..
then have "card (Pow (set xs)) = 2 ^ card (set xs)"
by (rule card_Pow)
with assms distinct_card [of xs] have "card (Pow (set xs)) = 2 ^ length xs"
by simp
- then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
- by (simp add: sublists_powset length_sublists)
+ then show "card (set (map set (subseqs xs))) = length (map set (subseqs xs))"
+ by (simp add: subseqs_powset length_subseqs)
qed
lemma n_lists_Nil [simp]: "List.n_lists n [] = (if n = 0 then [[]] else [])"
@@ -4464,20 +4460,20 @@
qed
qed
-lemma sublists_refl: "xs \<in> set (sublists xs)"
+lemma subseqs_refl: "xs \<in> set (subseqs xs)"
by (induct xs) (simp_all add: Let_def)
-lemma subset_sublists: "X \<subseteq> set xs \<Longrightarrow> X \<in> set ` set (sublists xs)"
- unfolding sublists_powset by simp
-
-lemma Cons_in_sublistsD: "y # ys \<in> set (sublists xs) \<Longrightarrow> ys \<in> set (sublists xs)"
+lemma subset_subseqs: "X \<subseteq> set xs \<Longrightarrow> X \<in> set ` set (subseqs xs)"
+ unfolding subseqs_powset by simp
+
+lemma Cons_in_subseqsD: "y # ys \<in> set (subseqs xs) \<Longrightarrow> ys \<in> set (subseqs xs)"
by (induct xs) (auto simp: Let_def)
-lemma sublists_distinctD: "\<lbrakk> ys \<in> set (sublists xs); distinct xs \<rbrakk> \<Longrightarrow> distinct ys"
+lemma subseqs_distinctD: "\<lbrakk> ys \<in> set (subseqs xs); distinct xs \<rbrakk> \<Longrightarrow> distinct ys"
proof (induct xs arbitrary: ys)
case (Cons x xs ys)
then show ?case
- by (auto simp: Let_def) (metis Pow_iff contra_subsetD image_eqI sublists_powset)
+ by (auto simp: Let_def) (metis Pow_iff contra_subsetD image_eqI subseqs_powset)
qed simp
@@ -7147,9 +7143,13 @@
"(op = ===> list_all2 A ===> list_all2 A) rotate rotate"
unfolding rotate_def [abs_def] by transfer_prover
-lemma sublist_transfer [transfer_rule]:
- "(list_all2 A ===> rel_set (op =) ===> list_all2 A) sublist sublist"
- unfolding sublist_def [abs_def] by transfer_prover
+lemma nths_transfer [transfer_rule]:
+ "(list_all2 A ===> rel_set (op =) ===> list_all2 A) nths nths"
+ unfolding nths_def [abs_def] by transfer_prover
+
+lemma subseqs_transfer [transfer_rule]:
+ "(list_all2 A ===> list_all2 (list_all2 A)) subseqs subseqs"
+ unfolding subseqs_def [abs_def] by transfer_prover
lemma partition_transfer [transfer_rule]:
"((A ===> op =) ===> list_all2 A ===> rel_prod (list_all2 A) (list_all2 A))
--- a/src/HOL/Quickcheck_Exhaustive.thy Sun May 28 15:46:26 2017 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy Mon May 29 09:14:15 2017 +0200
@@ -388,7 +388,7 @@
definition enum_term_of_set :: "'a set itself \<Rightarrow> unit \<Rightarrow> term list"
where "enum_term_of_set _ _ =
- map (setify (TYPE('a))) (sublists (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))"
+ map (setify (TYPE('a))) (subseqs (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))"
instance ..
--- a/src/HOL/ROOT Sun May 28 15:46:26 2017 +0200
+++ b/src/HOL/ROOT Mon May 29 09:14:15 2017 +0200
@@ -40,7 +40,7 @@
Prefix_Order
Product_Lexorder
Product_Order
- Sublist_Order
+ Subseq_Order
(*data refinements and dependent applications*)
AList_Mapping
Code_Binary_Nat
--- a/src/HOL/UNITY/Comp/AllocBase.thy Sun May 28 15:46:26 2017 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Mon May 29 09:14:15 2017 +0200
@@ -48,39 +48,38 @@
declare sum.cong [cong]
-lemma bag_of_sublist_lemma:
+lemma bag_of_nths_lemma:
"(\<Sum>i\<in> A Int lessThan k. {#if i<k then f i else g i#}) =
(\<Sum>i\<in> A Int lessThan k. {#f i#})"
by (rule sum.cong, auto)
-lemma bag_of_sublist:
- "bag_of (sublist l A) =
+lemma bag_of_nths:
+ "bag_of (nths l A) =
(\<Sum>i\<in> A Int lessThan (length l). {# l!i #})"
-apply (rule_tac xs = l in rev_induct, simp)
-apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append
- bag_of_sublist_lemma ac_simps)
-done
+ by (rule_tac xs = l in rev_induct)
+ (simp_all add: nths_append Int_insert_right lessThan_Suc nth_append
+ bag_of_nths_lemma ac_simps)
-lemma bag_of_sublist_Un_Int:
- "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) =
- bag_of (sublist l A) + bag_of (sublist l B)"
+lemma bag_of_nths_Un_Int:
+ "bag_of (nths l (A Un B)) + bag_of (nths l (A Int B)) =
+ bag_of (nths l A) + bag_of (nths l B)"
apply (subgoal_tac "A Int B Int {..<length l} =
(A Int {..<length l}) Int (B Int {..<length l}) ")
-apply (simp add: bag_of_sublist Int_Un_distrib2 sum.union_inter, blast)
+apply (simp add: bag_of_nths Int_Un_distrib2 sum.union_inter, blast)
done
-lemma bag_of_sublist_Un_disjoint:
+lemma bag_of_nths_Un_disjoint:
"A Int B = {}
- ==> bag_of (sublist l (A Un B)) =
- bag_of (sublist l A) + bag_of (sublist l B)"
-by (simp add: bag_of_sublist_Un_Int [symmetric])
+ ==> bag_of (nths l (A Un B)) =
+ bag_of (nths l A) + bag_of (nths l B)"
+by (simp add: bag_of_nths_Un_Int [symmetric])
-lemma bag_of_sublist_UN_disjoint [rule_format]:
+lemma bag_of_nths_UN_disjoint [rule_format]:
"[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]
- ==> bag_of (sublist l (UNION I A)) =
- (\<Sum>i\<in>I. bag_of (sublist l (A i)))"
-apply (auto simp add: bag_of_sublist)
+ ==> bag_of (nths l (UNION I A)) =
+ (\<Sum>i\<in>I. bag_of (nths l (A i)))"
+apply (auto simp add: bag_of_nths)
unfolding UN_simps [symmetric]
apply (subst sum.UNION_disjoint)
apply auto
--- a/src/HOL/UNITY/Comp/AllocImpl.thy Sun May 28 15:46:26 2017 +0200
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy Mon May 29 09:14:15 2017 +0200
@@ -78,7 +78,7 @@
(\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
guarantees
(\<Inter>i \<in> lessThan Nclients.
- (%s. sublist (merge.Out s)
+ (%s. nths (merge.Out s)
{k. k < size(merge.iOut s) & merge.iOut s! k = i})
Fols (sub i o merge.In))"
@@ -110,7 +110,7 @@
guarantees
(\<Inter>i \<in> lessThan Nclients.
(sub i o distr.Out) Fols
- (%s. sublist (distr.In s)
+ (%s. nths (distr.In s)
{k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"
definition
@@ -273,13 +273,13 @@
lemma Merge_Bag_Follows_lemma:
"[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
==> M \<squnion> G \<in> Always
- {s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (merge.Out s)
+ {s. (\<Sum>i \<in> lessThan Nclients. bag_of (nths (merge.Out s)
{k. k < length (iOut s) & iOut s ! k = i})) =
(bag_of o merge.Out) s}"
apply (rule Always_Compl_Un_eq [THEN iffD1])
apply (blast intro: Always_Int_I [OF Merge_Always_Out_eq_iOut Merge_Bounded])
apply (rule UNIV_AlwaysI, clarify)
-apply (subst bag_of_sublist_UN_disjoint [symmetric])
+apply (subst bag_of_nths_UN_disjoint [symmetric])
apply (simp)
apply blast
apply (simp add: set_conv_nth)
@@ -327,12 +327,12 @@
"[| G \<in> preserves distr.Out;
D \<squnion> G \<in> Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |]
==> D \<squnion> G \<in> Always
- {s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (distr.In s)
+ {s. (\<Sum>i \<in> lessThan Nclients. bag_of (nths (distr.In s)
{k. k < length (iIn s) & iIn s ! k = i})) =
- bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}"
+ bag_of (nths (distr.In s) (lessThan (length (iIn s))))}"
apply (erule Always_Compl_Un_eq [THEN iffD1])
apply (rule UNIV_AlwaysI, clarify)
-apply (subst bag_of_sublist_UN_disjoint [symmetric])
+apply (subst bag_of_nths_UN_disjoint [symmetric])
apply (simp (no_asm))
apply blast
apply (simp add: set_conv_nth)
@@ -357,7 +357,7 @@
(\<Inter>i \<in> lessThan Nclients.
(%s. \<Sum>i \<in> lessThan Nclients. (bag_of o sub i o distr.Out) s)
Fols
- (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))"
+ (%s. bag_of (nths (distr.In s) (lessThan (length(distr.iIn s))))))"
apply (rule guaranteesI, clarify)
apply (rule Distr_Bag_Follows_lemma [THEN Always_Follows2], auto)
apply (rule Follows_sum)