# HG changeset patch # User eberlm # Date 1496042055 -7200 # Node ID 639eb3617a86fed35f64d1ecb964dcd3b7fd5a4a # Parent 0616ba637b14ee2beb36addffa40ed3ffcb9bb0d reorganised material on sublists diff -r 0616ba637b14 -r 639eb3617a86 NEWS --- 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"). diff -r 0616ba637b14 -r 639eb3617a86 src/Doc/Main/Main_Doc.thy --- 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\nat)list\('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 \ '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 @@ \ (*<*) end -(*>*) \ No newline at end of file +(*>*) diff -r 0616ba637b14 -r 639eb3617a86 src/HOL/Codegenerator_Test/Candidates.thy --- 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" diff -r 0616ba637b14 -r 639eb3617a86 src/HOL/Enum.thy --- 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 \ (\A\set enum. P (A::'a set))" @@ -394,7 +394,7 @@ "enum_ex P \ (\A\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 diff -r 0616ba637b14 -r 639eb3617a86 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy --- 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: "\j. j \ set (subarray (p + 1) (r + 1) a h1) \ Array.get h1 a ! p \ 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 diff -r 0616ba637b14 -r 639eb3617a86 src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy --- 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: diff -r 0616ba637b14 -r 639eb3617a86 src/HOL/Imperative_HOL/ex/List_Sublist.thy --- 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 \ j \ j \ k \ sublist xs {i.. j \ j \ k \ nths xs {i.. inds \ sublist (xs[i := v]) inds = sublist xs inds" +lemma nths_update1: "i \ inds \ 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 \ inds \ sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \ inds. k < i}):= v]" +lemma nths_update2: "i \ inds \ nths (xs[i := v]) inds = (nths xs inds)[(card {k \ 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 \ inds then (sublist xs inds)[(card {k \ 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 \ inds then (nths xs inds)[(card {k \ 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.. sublist xs {a} = [xs ! a]" +lemma nths_single: "a < length xs \ 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: "\i \ inds. i \ length xs \ sublist xs inds = []" +lemma nths_is_Nil: "\i \ inds. i \ length xs \ 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 \ inds}" in meta_allE) apply auto done -lemma sublist_Nil': "sublist xs inds = [] \ \i \ inds. i \ length xs" +lemma nths_Nil': "nths xs inds = [] \ \i \ inds. i \ 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 \ inds}" in meta_allE) apply (case_tac x, auto) done -lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\i \ inds. i \ length xs)" +lemma nths_Nil[simp]: "(nths xs inds = []) = (\i \ inds. i \ 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 \ inds}" in meta_allE) apply (case_tac x, auto) done -lemma sublist_eq_subseteq: " \ inds' \ inds; sublist xs inds = sublist ys inds \ \ sublist xs inds' = sublist ys inds'" +lemma nths_eq_subseteq: " \ inds' \ inds; nths xs inds = nths ys inds \ \ 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 \ inds}" in meta_allE) apply (erule_tac x="{j. Suc j \ inds'}" in meta_allE) @@ -157,13 +157,13 @@ apply fastforce done -lemma sublist_eq: "\ \i \ inds. ((i < length xs) \ (i < length ys)) \ ((i \ length xs ) \ (i \ length ys)); \i \ inds. xs ! i = ys ! i \ \ sublist xs inds = sublist ys inds" +lemma nths_eq: "\ \i \ inds. ((i < length xs) \ (i < length ys)) \ ((i \ length xs ) \ (i \ length ys)); \i \ inds. xs ! i = ys ! i \ \ 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 \ inds}" in meta_allE) apply fastforce @@ -172,64 +172,64 @@ apply fastforce done -lemma sublist_eq_samelength: "\ length xs = length ys; \i \ inds. xs ! i = ys ! i \ \ sublist xs inds = sublist ys inds" -by (rule sublist_eq, auto) +lemma nths_eq_samelength: "\ length xs = length ys; \i \ inds. xs ! i = ys ! i \ \ nths xs inds = nths ys inds" +by (rule nths_eq, auto) -lemma sublist_eq_samelength_iff: "length xs = length ys \ (sublist xs inds = sublist ys inds) = (\i \ inds. xs ! i = ys ! i)" +lemma nths_eq_samelength_iff: "length xs = length ys \ (nths xs inds = nths ys inds) = (\i \ 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 \Another sublist function\ +section \Another nths function\ -function sublist' :: "nat \ nat \ 'a list \ 'a list" +function nths' :: "nat \ nat \ 'a list \ '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 \Proving equivalence to the other sublist command\ +subsection \Proving equivalence to the other nths command\ -lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \ j \ j < m}" +lemma nths'_nths: "nths' n m xs = nths xs {j. n \ j \ 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..Showing equivalence to use of drop and take for definition\ -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 \General lemma about sublist\ +subsection \General lemma about nths\ -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 \ (x # sublist' 0 j xs) | Suc i' \ sublist' i' j xs)" +lemma nths'_Cons[simp]: "nths' i (Suc j) (x#xs) = (case i of 0 \ (x # nths' 0 j xs) | Suc i' \ 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 \ m \ sublist' n m xs = []" +lemma nths'_Nil': "n \ m \ 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 \ length xs \ sublist' n m xs = []" +lemma nths'_Nil2: "n \ length xs \ 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 \ m) \ (n \ length xs))" +lemma nths'_Nil3: "(nths' n m xs = []) = ((n \ m) \ (n \ length xs))" apply (induct xs arbitrary: n m) apply simp apply (case_tac m) @@ -287,7 +287,7 @@ apply simp done -lemma sublist'_notNil: "\ n < length xs; n < m \ \ sublist' n m xs \ []" +lemma nths'_notNil: "\ n < length xs; n < m \ \ nths' n m xs \ []" 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 \ sublist' n (Suc n) xs = [xs ! n]" +lemma nths'_single: "n < length xs \ 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 \ m \ sublist' n m (xs[i:=v]) = sublist' n m xs" +lemma nths'_update1: "i \ m \ 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 \ sublist' n m (xs[i:=v]) = sublist' n m xs" +lemma nths'_update2: "i < n \ 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: "\n \ i; i < m\ \ sublist' n m (xs[i := v]) = (sublist' n m xs)[i - n := v]" +lemma nths'_update3: "\n \ i; i < m\ \ 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 "\ sublist' i j xs = sublist' i j ys; n \ i; m \ j \ \ sublist' n m xs = sublist' n m ys" +lemma "\ nths' i j xs = nths' i j ys; n \ i; m \ j \ \ 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 \ length xs \ length (sublist' i j xs) = j - i" +lemma length_nths': "j \ length xs \ length (nths' i j xs) = j - i" by (induct xs arbitrary: i j, auto) -lemma sublist'_front: "\ i < j; i < length xs \ \ sublist' i j xs = xs ! i # sublist' (Suc i) j xs" +lemma nths'_front: "\ i < j; i < length xs \ \ 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: "\ i < j; j \ length xs \ \ sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]" +lemma nths'_back: "\ i < j; j \ length xs \ \ 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 \ length xs and length ys *) -lemma sublist'_eq_samelength_iff: "length xs = length ys \ (sublist' i j xs = sublist' i j ys) = (\i'. i \ i' \ i' < j \ xs ! i' = ys ! i')" +lemma nths'_eq_samelength_iff: "length xs = length ys \ (nths' i j xs = nths' i j ys) = (\i'. i \ i' \ i' < j \ 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: "\ i \ j; j \ k \ \(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs" +lemma nths'_append: "\ i \ j; j \ k \ \(nths' i j xs) @ (nths' j k xs) = nths' i k xs" by (induct xs arbitrary: i j k) auto -lemma nth_sublist': "\ k < j - i; j \ length xs \ \ (sublist' i j xs) ! k = xs ! (i + k)" +lemma nth_nths': "\ k < j - i; j \ length xs \ \ (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. \k. i \ k \ k < j \ k < List.length xs \ x = xs ! k}" -apply (simp add: sublist'_sublist) -apply (simp add: set_sublist) +lemma set_nths': "set (nths' i j xs) = {x. \k. i \ k \ k < j \ k < List.length xs \ x = xs ! k}" +apply (simp add: nths'_nths) +apply (simp add: set_nths) apply auto done -lemma all_in_set_sublist'_conv: "(\j. j \ set (sublist' l r xs) \ P j) = (\k. l \ k \ k < r \ k < List.length xs \ P (xs ! k))" -unfolding set_sublist' by blast +lemma all_in_set_nths'_conv: "(\j. j \ set (nths' l r xs) \ P j) = (\k. l \ k \ k < r \ k < List.length xs \ P (xs ! k))" +unfolding set_nths' by blast -lemma ball_in_set_sublist'_conv: "(\j \ set (sublist' l r xs). P j) = (\k. l \ k \ k < r \ k < List.length xs \ P (xs ! k))" -unfolding set_sublist' by blast +lemma ball_in_set_nths'_conv: "(\j \ set (nths' l r xs). P j) = (\k. l \ k \ k < r \ k < List.length xs \ P (xs ! k))" +unfolding set_nths' by blast -lemma mset_sublist: +lemma mset_nths: assumes l_r: "l \ r \ r \ List.length xs" assumes left: "\ i. i < l \ (xs::'a list) ! i = ys ! i" assumes right: "\ i. i \ r \ (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 diff -r 0616ba637b14 -r 639eb3617a86 src/HOL/Imperative_HOL/ex/Subarray.thy --- 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 \ nat \ ('a::heap) array \ heap \ 'a list" where - "subarray n m a h \ sublist' n m (Array.get h a)" + "subarray n m a h \ nths' n m (Array.get h a)" lemma subarray_upd: "i \ m \ 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 \ 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: "\ n \ i; i < m\ \ 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 \ m \ subarray n m a h = []" -by (simp add: subarray_def sublist'_Nil') +by (simp add: subarray_def nths'_Nil') lemma subarray_single: "\ n < Array.length h a \ \ 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 \ Array.length h a \ 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 \ Array.length h a \ List.length (subarray 0 m a h) = m" by (simp add: length_subarray) lemma subarray_nth_array_Cons: "\ i < Array.length h a; i < j \ \ (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: "\ i < j; j \ Array.length h a\ \ 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: "\ i \ j; j \ k \ \ 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: "\ k < j - i; j \ Array.length h a \ \ 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 \ (subarray i j a h = subarray i j a h') = (\i'. i \ i' \ i' < j \ 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: "(\j. j \ set (subarray l r a h) \ P j) = (\k. l \ k \ k < r \ k < Array.length h a \ 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: "(\j \ set (subarray l r a h). P j) = (\k. l \ k \ k < r \ k < Array.length h a \ 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 diff -r 0616ba637b14 -r 639eb3617a86 src/HOL/Library/Sublist.thy --- 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 \List prefixes, suffixes, and homeomorphic embedding\ @@ -214,7 +215,7 @@ subsection \Prefixes\ -fun prefixes where +primrec prefixes where "prefixes [] = [[]]" | "prefixes (x#xs) = [] # map (op # x) (prefixes xs)" @@ -700,7 +701,7 @@ subsection \Suffixes\ -fun suffixes where +primrec suffixes where "suffixes [] = [[]]" | "suffixes (x#xs) = suffixes xs @ [x # xs]" @@ -919,49 +920,48 @@ "list_emb P (x#xs) [] \ False" "list_emb P (x#xs) (y#ys) \ (if P x y then list_emb P xs ys else list_emb P (x#xs) ys)" by simp_all - + - -subsection \Sublists (special case of homeomorphic embedding)\ +subsection \Subsequences (special case of homeomorphic embedding)\ -abbreviation sublisteq :: "'a list \ 'a list \ bool" - where "sublisteq xs ys \ list_emb (op =) xs ys" +abbreviation subseq :: "'a list \ 'a list \ bool" + where "subseq xs ys \ list_emb (op =) xs ys" -definition strict_sublist where "strict_sublist xs ys \ xs \ ys \ sublisteq xs ys" +definition strict_subseq where "strict_subseq xs ys \ xs \ ys \ subseq xs ys" -lemma sublisteq_Cons2: "sublisteq xs ys \ sublisteq (x#xs) (x#ys)" by auto +lemma subseq_Cons2: "subseq xs ys \ 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 \ \ sublisteq xs ys" +lemma not_subseq_length [simp]: "length ys < length xs \ \ subseq xs ys" by (metis list_emb_length linorder_not_less) -lemma sublisteq_Cons': "sublisteq (x#xs) ys \ sublisteq xs ys" +lemma subseq_Cons': "subseq (x#xs) ys \ 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 \ y \ sublisteq (x#xs) ys" +lemma subseq_Cons2_neq: + assumes "subseq (x#xs) (y#ys)" + shows "x \ y \ 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) \ sublisteq xs ys" +lemma subseq_append': "subseq (zs @ xs) (zs @ ys) \ 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 \ (sublisteq xs ys \ \sublisteq ys xs)" - by (auto simp: strict_sublist_def) + thus "strict_subseq xs ys \ (subseq xs ys \ \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 \ set (sublists ys) \ sublisteq xs ys" +lemma in_set_subseqs [simp]: "xs \ set (subseqs ys) \ subseq xs ys" proof - assume "xs \ set (sublists ys)" - thus "sublisteq xs ys" + assume "xs \ set (subseqs ys)" + thus "subseq xs ys" by (induction ys arbitrary: xs) (auto simp: Let_def) next - have [simp]: "[] \ set (sublists ys)" for ys :: "'a list" + have [simp]: "[] \ set (subseqs ys)" for ys :: "'a list" by (induction ys) (auto simp: Let_def) - assume "sublisteq xs ys" - thus "xs \ set (sublists ys)" + assume "subseq xs ys" + thus "xs \ 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 \ xs = []" +lemma subseq_append_le_same_iff: "subseq (xs @ ys) ys \ xs = []" by (auto dest: list_emb_length) -lemma sublisteq_singleton_left: "sublisteq [x] ys \