(* Author: Alexander Bentkamp, Universität des Saarlandes *) section ‹Missing Lemmas of Sublist› theory DL_Missing_Sublist imports Main begin lemma nths_only_one: assumes "{i. i < length xs ∧ i∈I} = {j}" shows "nths xs I = [xs!j]" proof - have "set (nths xs I) = {xs!j}" unfolding set_nths using subset_antisym assms by fastforce moreover have "length (nths xs I) = 1" unfolding length_nths assms by auto ultimately show ?thesis by (metis One_nat_def length_0_conv length_Suc_conv the_elem_eq the_elem_set) qed lemma nths_replicate: "nths (replicate n x) A = (replicate (card {i. i < n ∧ i ∈ A}) x)" proof (induction n) case 0 then show ?case by simp next case (Suc n) then show ?case proof (cases "n∈A") case True then have 0:"(if 0 ∈ {j. j + length (replicate n x) ∈ A} then [x] else []) = [x]" by simp have "{i. i < Suc n ∧ i ∈ A} = insert n {i. i < n ∧ i ∈ A}" using True by auto have "Suc (card {i. i < n ∧ i ∈ A}) = card {i. i < Suc n ∧ i ∈ A}" unfolding ‹{i. i < Suc n ∧ i ∈ A} = insert n {i. i < n ∧ i ∈ A}› using finite_Collect_conjI[THEN card_insert_if] finite_Collect_less_nat less_irrefl_nat mem_Collect_eq by simp then show ?thesis unfolding replicate_Suc replicate_append_same[symmetric] nths_append Suc nths_singleton 0 unfolding replicate_append_same replicate_Suc[symmetric] by simp next case False then have 0:"(if 0 ∈ {j. j + length (replicate n x) ∈ A} then [x] else []) = []" by simp have "{i. i < Suc n ∧ i ∈ A} = {i. i < n ∧ i ∈ A}" using False using le_less less_Suc_eq_le by auto then show ?thesis unfolding replicate_Suc replicate_append_same[symmetric] nths_append Suc nths_singleton 0 by simp qed qed lemma length_nths_even: assumes "even (length xs)" shows "length (nths xs (Collect even)) = length (nths xs (Collect odd))" using assms proof (induction "length xs div 2" arbitrary:xs) case 0 then have "length xs = 0" by (auto elim: evenE) then show ?case by simp next case (Suc l xs) then have length_drop2: "length (nths (drop 2 xs) (Collect even)) = length (nths (drop 2 xs) {a. odd a})" by simp have "length (take 2 xs) = 2" using Suc.hyps(2) by auto then have plus_odd: "{j. j + length (take 2 xs) ∈ Collect odd} = Collect odd" and plus_even: "{j. j + length (take 2 xs) ∈ Collect even} = Collect even" by simp_all have nths_take2: "nths (take 2 xs) (Collect even) = [take 2 xs ! 0]" "nths (take 2 xs) (Collect odd) = [take 2 xs ! 1]" using ‹length (take 2 xs) = 2› less_2_cases nths_only_one[of "take 2 xs" "Collect even" 0] nths_only_one[of "take 2 xs" "Collect odd" 1] by fastforce+ then have "length (nths (take 2 xs @ drop 2 xs) (Collect even)) = length (nths (take 2 xs @ drop 2 xs) {a. odd a})" unfolding nths_append length_append plus_odd plus_even nths_take2 length_drop2 by auto then show ?case using append_take_drop_id[of 2 xs] by simp qed lemma nths_map: "nths (map f xs) A = map f (nths xs A)" proof (induction xs arbitrary:A) case Nil then show ?case by simp next case (Cons x xs) then show ?case by (simp add: nths_Cons) qed section "Pick" fun pick :: "nat set ⇒ nat ⇒ nat" where "pick S 0 = (LEAST a. a∈S)" | "pick S (Suc n) = (LEAST a. a∈S ∧ a > pick S n)" lemma pick_in_set_inf: assumes "infinite S" shows "pick S n ∈ S" proof (cases n) show "n = 0 ⟹ pick S n ∈ S" unfolding pick.simps using ‹infinite S› LeastI pick.simps(1) by (metis Collect_mem_eq not_finite_existsD) next fix n' assume "n = Suc n'" obtain a where "a∈S ∧ a > pick S n'" using assms by (metis bounded_nat_set_is_finite less_Suc_eq nat_neq_iff) show "pick S n ∈ S" unfolding ‹n = Suc n'› pick.simps(2) using LeastI[of "λa. a ∈ S ∧ pick S n' < a" a, OF ‹a∈S ∧ a > pick S n'›] by blast qed lemma pick_mono_inf: assumes "infinite S" shows "m < n ⟹ pick S m < pick S n" using assms proof (induction n) case 0 then show ?case by auto next case (Suc n) then obtain a where "a ∈ S ∧ pick S n < a" by (metis bounded_nat_set_is_finite less_Suc_eq nat_neq_iff) then have "pick S n < pick S (Suc n)" unfolding pick.simps using LeastI[of "λa. a ∈ S ∧ pick S n < a" a, OF ‹a∈S ∧ a > pick S n›] by simp then show ?case using Suc.IH Suc.prems(1) assms dual_order.strict_trans less_Suc_eq by auto qed lemma pick_eq_iff_inf: assumes "infinite S" shows "x = y ⟷ pick S x = pick S y" by (metis assms nat_neq_iff pick_mono_inf) lemma card_le_pick_inf: assumes "infinite S" and "pick S n ≥ i" shows "card {a∈S. a < i} ≤ n" using assms proof (induction n arbitrary:i) case 0 then show ?case unfolding pick.simps using not_less_Least by (metis (no_types, lifting) Collect_empty_eq card_0_eq card_ge_0_finite dual_order.strict_trans1 leI le_0_eq) next case (Suc n) then show ?case proof - have "card {a ∈ S. a < pick S n} ≤ n" using Suc by blast have "{a ∈ S. a < i} ⊆ {a ∈ S. a < pick S (Suc n)}" using Suc.prems(2) by auto have "{a ∈ S. a < pick S (Suc n)} = {a ∈ S. a < pick S n} ∪ {pick S n}" apply (rule subset_antisym; rule subsetI) using not_less_Least UnCI mem_Collect_eq nat_neq_iff singleton_conv pick_mono_inf[OF Suc.prems(1), of n "Suc n"] pick_in_set_inf[OF Suc.prems(1), of n] by fastforce+ then have "card {a ∈ S. a < i} ≤ card {a ∈ S. a < pick S n} + card {pick S n}" using card_Un_disjoint card_mono[OF _ ‹{a ∈ S. a < i} ⊆ {a ∈ S. a < pick S (Suc n)}›] by simp then show ?thesis using ‹card {a ∈ S. a < pick S n} ≤ n› by auto qed qed lemma card_pick_inf: assumes "infinite S" shows "card {a∈S. a < pick S n} = n" using assms proof (induction n) case 0 then show ?case unfolding pick.simps using not_less_Least by auto next case (Suc n) then show "card {a∈S. a < pick S (Suc n)} = Suc n" proof - have "{a ∈ S. a < pick S (Suc n)} = {a ∈ S. a < pick S n} ∪ {pick S n}" apply (rule subset_antisym; rule subsetI) using not_less_Least UnCI mem_Collect_eq nat_neq_iff singleton_conv pick_mono_inf[OF Suc.prems, of n "Suc n"] pick_in_set_inf[OF Suc.prems, of n] by fastforce+ then have "card {a ∈ S. a < pick S (Suc n)} = card {a ∈ S. a < pick S n} + card {pick S n}" using card_Un_disjoint by auto then show ?thesis by (metis One_nat_def Suc_eq_plus1 Suc card_empty card_insert_if empty_iff finite.emptyI) qed qed lemma assumes "n < card S" shows pick_in_set_le:"pick S n ∈ S" and card_pick_le: "card {a∈S. a < pick S n} = n" and pick_mono_le: "m < n ⟹ pick S m < pick S n" using assms proof (induction n) assume "0 < card S" then obtain x where "x∈S" by fastforce then show "pick S 0 ∈ S" unfolding pick.simps by (meson LeastI) then show "card {a ∈ S. a < pick S 0} = 0" using not_less_Least by auto show "m < 0 ⟹ pick S m < pick S 0" by auto next fix n assume "n < card S ⟹ pick S n ∈ S" and "n < card S ⟹ card {a ∈ S. a < pick S n} = n" and "Suc n < card S" and "m < n ⟹ n < card S ⟹ pick S m < pick S n" then have "card {a ∈ S. a < pick S n} = n" "pick S n ∈ S" by linarith+ have "card {a ∈ S. a > pick S n} > 0" proof - have "S = {a ∈ S. a < pick S n} ∪ {a ∈ S. a ≥ pick S n}" by fastforce then have "card {a ∈ S. a ≥ pick S n} > 1" using ‹Suc n < card S› ‹card {a ∈ S. a < pick S n} = n› card_Un_le[of "{a ∈ S. a < pick S n}" "{a ∈ S. pick S n ≤ a}"] by force then have 0:"{a ∈ S. a ≥ pick S n} ⊆ {pick S n} ∪ {a ∈ S. a > pick S n}" by auto have 1:"finite ({pick S n} ∪ {a ∈ S. pick S n < a})" unfolding finite_Un using Collect_mem_eq assms card_infinite conjI by force have "1 < card {pick S n} + card {a ∈ S. pick S n < a}" using card_mono[OF 1 0] card_Un_le[of "{pick S n}" "{a ∈ S. a > pick S n}"] ‹card {a ∈ S. a ≥ pick S n} > 1› by linarith then show ?thesis by simp qed then show "pick S (Suc n) ∈ S" unfolding pick.simps by (metis (no_types, lifting) Collect_empty_eq LeastI card_0_eq card_infinite less_numeral_extra(3)) have "pick S (Suc n) > pick S n" by (metis (no_types, lifting) pick.simps(2) ‹card {a ∈ S. a > pick S n} > 0› Collect_empty_eq LeastI card_0_eq card_infinite less_numeral_extra(3)) then show "m < Suc n ⟹ pick S m < pick S (Suc n)" using ‹m < n ⟹ n < card S ⟹ pick S m < pick S n› using ‹Suc n < card S› dual_order.strict_trans less_Suc_eq by auto then show "card {a∈S. a < pick S (Suc n)} = Suc n" proof - have "{a ∈ S. a < pick S (Suc n)} = {a ∈ S. a < pick S n} ∪ {pick S n}" apply (rule subset_antisym; rule subsetI) using pick.simps not_less_Least ‹pick S (Suc n) > pick S n› ‹pick S n ∈ S› by fastforce+ then have "card {a ∈ S. a < pick S (Suc n)} = card {a ∈ S. a < pick S n} + card {pick S n}" using card_Un_disjoint by auto then show ?thesis by (metis One_nat_def Suc_eq_plus1 ‹card {a ∈ S. a < pick S n} = n› card_empty card_insert_if empty_iff finite.emptyI) qed qed lemma card_le_pick_le: assumes "n < card S" and "pick S n ≥ i" shows "card {a∈S. a < i} ≤ n" using assms proof (induction n arbitrary:i) case 0 then show ?case unfolding pick.simps using not_less_Least by (metis (no_types, lifting) Collect_empty_eq card_0_eq card_ge_0_finite dual_order.strict_trans1 leI le_0_eq) next case (Suc n) have "card {a ∈ S. a < pick S n} ≤ n" using Suc by (simp add: less_eq_Suc_le nat_less_le) have "{a ∈ S. a < i} ⊆ {a ∈ S. a < pick S (Suc n)}" using Suc.prems(2) by auto have "{a ∈ S. a < pick S (Suc n)} = {a ∈ S. a < pick S n} ∪ {pick S n}" apply (rule subset_antisym; rule subsetI) using pick.simps not_less_Least pick_mono_le[OF Suc.prems(1), of n, OF lessI] pick_in_set_le[of n S] Suc by fastforce+ then have "card {a ∈ S. a < i} ≤ card {a ∈ S. a < pick S n} + card {pick S n}" using card_Un_disjoint card_mono[OF _ ‹{a ∈ S. a < i} ⊆ {a ∈ S. a < pick S (Suc n)}›] by simp then show ?case using ‹card {a ∈ S. a < pick S n} ≤ n› by auto qed lemma assumes "n < card S ∨ infinite S" shows pick_in_set:"pick S n ∈ S" and card_le_pick: "i ≤ pick S n ==> card {a∈S. a < i} ≤ n" and card_pick: "card {a∈S. a < pick S n} = n" and pick_mono: "m < n ⟹ pick S m < pick S n" using assms pick_in_set_inf pick_in_set_le card_pick_inf card_pick_le card_le_pick_le card_le_pick_inf pick_mono_inf pick_mono_le by auto lemma pick_card: "pick I (card {a∈I. a < i}) = (LEAST a. a∈I ∧ a ≥ i)" proof (induction i) case 0 then show ?case by (simp add: pick_in_set_le) next case (Suc i) then show ?case proof (cases "i∈I") case True then have 1:"pick I (card {a∈I. a < i}) = i" by (metis (mono_tags, lifting) Least_equality Suc.IH order_refl) have "{a ∈ I. a < Suc i} = {a ∈ I. a < i} ∪ {i}" using True by auto then have 2:"card {a ∈ I. a < Suc i} = Suc (card {a ∈ I. a < i})" by auto then show ?thesis unfolding 2 pick.simps 1 using Suc_le_eq by auto next case False then have 1:"{a ∈ I. a < Suc i} = {a ∈ I. a < i}" using Collect_cong less_Suc_eq by auto have 2:"⋀a. (a ∈ I ∧ Suc i ≤ a) = (a ∈ I ∧ i ≤ a)" using False Suc_leD le_less_Suc_eq not_le by blast then show ?thesis unfolding 1 2 using Suc.IH by blast qed qed lemma pick_card_in_set: "i∈I ⟹ pick I (card {a∈I. a < i}) = i" unfolding pick_card using Least_equality order_refl by (metis (no_types, lifting)) section "Sublist" lemma nth_nths_card: assumes "j<length xs" and "j∈J" shows "nths xs J ! card {j0. j0 < j ∧ j0 ∈ J} = xs!j" using assms proof (induction xs rule:rev_induct) case Nil then show ?case using gr_implies_not0 list.size(3) by auto next case (snoc x xs) then show ?case proof (cases "j < length xs") case True have "{j0. j0 < j ∧ j0 ∈ J} ⊂ {i. i < length xs ∧ i ∈ J}" using True snoc.prems(2) by auto then have "card {j0. j0 < j ∧ j0 ∈ J} < length (nths xs J)" unfolding length_nths using psubset_card_mono[of "{i. i < length xs ∧ i ∈ J}"] by simp then show ?thesis unfolding nths_append nth_append by (simp add: True snoc.IH snoc.prems(2)) next case False then have "length xs = j" using length_append_singleton less_antisym snoc.prems(1) by auto then show ?thesis unfolding nths_append nth_append length_nths ‹length xs = j› by (simp add: snoc.prems(2)) qed qed lemma pick_reduce_set: assumes "i<card {a. a<m ∧ a∈I}" shows "pick I i = pick {a. a < m ∧ a ∈ I} i" using assms proof (induction i) let ?L = "LEAST a. a ∈ {a. a < m ∧ a ∈ I}" case 0 then have "{a. a < m ∧ a ∈ I} ≠ {}" using card_empty less_numeral_extra(3) by fastforce then have "?L ∈ I" "?L < m" by (metis (mono_tags, lifting) Collect_empty_eq LeastI mem_Collect_eq)+ have "⋀x. x ∈ {a. a < m ∧ a ∈ I} ⟹ ?L ≤ x" by (simp add: Least_le) have "⋀x. x ∈ I ⟹ ?L ≤ x" by (metis (mono_tags) ‹?L < m› ‹⋀x. x ∈ {a. a < m ∧ a ∈ I} ⟹ ?L ≤ x› dual_order.strict_trans2 le_cases mem_Collect_eq) then show ?case unfolding pick.simps using Least_equality[of "λx. x∈I", OF ‹?L ∈ I›] by blast next case (Suc i) let ?L = "LEAST x. x ∈ {a. a < m ∧ a ∈ I} ∧ pick I i < x" have 0:"pick {a. a < m ∧ a ∈ I} i = pick I i" using Suc_lessD Suc by linarith then have "?L ∈ {a. a < m ∧ a ∈ I}" "pick I i < ?L" using LeastI[of "λa. a ∈ {a. a < m ∧ a ∈ I} ∧ pick I i < a"] using Suc.prems pick_in_set_le pick_mono_le by fastforce+ then have "?L ∈ I" by blast show ?case unfolding pick.simps 0 using Least_equality[of "λa. a ∈ I ∧ pick I i < a" ?L] by (metis (no_types, lifting) Least_le ‹?L ∈ {a. a < m ∧ a ∈ I}› ‹pick I i < ?L› mem_Collect_eq not_le not_less_iff_gr_or_eq order.trans) qed lemma nth_nths: assumes "i<card {i. i<length xs ∧ i∈I}" shows "nths xs I ! i = xs ! pick I i" proof - have "{a ∈ {i. i < length xs ∧ i ∈ I}. a < pick {i. i < length xs ∧ i ∈ I} i} = {a. a < pick {i. i < length xs ∧ i ∈ I} i ∧ a ∈ I}" using assms pick_in_set by fastforce then have "card {a. a < pick {i. i < length xs ∧ i ∈ I} i ∧ a ∈ I} = i" using card_pick_le[OF assms] by simp then have "nths xs I ! i = xs ! pick {i. i < length xs ∧ i ∈ I} i" using nth_nths_card[where j = "pick {i. i < length xs ∧ i ∈ I} i", of xs I] assms pick_in_set pick_in_set by auto then show ?thesis using pick_reduce_set using assms by auto qed lemma pick_UNIV: "pick UNIV j = j" by (induction j, simp, metis (no_types, lifting) LeastI pick.simps(2) Suc_mono UNIV_I less_Suc_eq not_less_Least) lemma pick_le: assumes "n < card {a. a < i ∧ a ∈ S}" shows "pick S n < i" proof - have 0:"{a ∈ {a. a < i ∧ a ∈ S}. a < i} = {a. a < i ∧ a ∈ S}" by blast show ?thesis apply (rule ccontr) using card_le_pick_le[OF assms, unfolded pick_reduce_set[OF assms, symmetric], of i, unfolded 0] assms not_less not_le by blast qed lemma prod_list_complementary_nthss: fixes f ::"'a ⇒ 'b::comm_monoid_mult" shows "prod_list (map f xs) = prod_list (map f (nths xs A)) * prod_list (map f (nths xs (-A)))" proof (induction xs rule:rev_induct) case Nil then show ?case by simp next case (snoc x xs) show ?case unfolding map_append "prod_list.append" nths_append nths_singleton snoc by (cases "(length xs)∈A"; simp;metis mult.assoc mult.commute) qed lemma nths_zip: "nths (zip xs ys) I = zip (nths xs I) (nths ys I)" proof (rule nth_equalityI) show "length (nths (zip xs ys) I) = length (zip (nths xs I) (nths ys I))" proof (cases "length xs ≤ length ys") case True then have "{i. i < length xs ∧ i ∈ I} ⊆ {i. i < length ys ∧ i ∈ I}" by (simp add: Collect_mono less_le_trans) then have "card {i. i < length xs ∧ i ∈ I} ≤ card {i. i < length ys ∧ i ∈ I}" by (metis (mono_tags, lifting) card_mono finite_nat_set_iff_bounded mem_Collect_eq) then show ?thesis unfolding length_nths length_zip using True using min_def by linarith next case False then have "{i. i < length ys ∧ i ∈ I} ⊆ {i. i < length xs ∧ i ∈ I}" by (simp add: Collect_mono less_le_trans) then have "card {i. i < length ys ∧ i ∈ I} ≤ card {i. i < length xs ∧ i ∈ I}" by (metis (mono_tags, lifting) card_mono finite_nat_set_iff_bounded mem_Collect_eq) then show ?thesis unfolding length_nths length_zip using False using min_def by linarith qed show "nths (zip xs ys) I ! i = zip (nths xs I) (nths ys I) ! i" if "i < length (nths (zip xs ys) I)" for i proof - have "i < length (nths xs I)" "i < length (nths ys I)" using that by (simp_all add: ‹length (nths (zip xs ys) I) = length (zip (nths xs I) (nths ys I))›) show "nths (zip xs ys) I ! i = zip (nths xs I) (nths ys I) ! i" unfolding nth_nths[OF ‹i < length (nths (zip xs ys) I)›[unfolded length_nths]] unfolding nth_zip[OF ‹i < length (nths xs I)› ‹i < length (nths ys I)›] unfolding nth_zip[OF pick_le[OF ‹i < length (nths xs I)›[unfolded length_nths]] pick_le[OF ‹i < length (nths ys I)›[unfolded length_nths]]] by (metis (full_types) ‹i < length (nths xs I)› ‹i < length (nths ys I)› length_nths nth_nths) qed qed section "weave" definition weave :: "nat set ⇒ 'a list ⇒ 'a list ⇒ 'a list" where "weave A xs ys = map (λi. if i∈A then xs!(card {a∈A. a<i}) else ys!(card {a∈-A. a<i})) [0..<length xs + length ys]" lemma length_weave: shows "length (weave A xs ys) = length xs + length ys" unfolding weave_def length_map by simp lemma nth_weave: assumes "i < length (weave A xs ys)" shows "weave A xs ys ! i = (if i∈A then xs!(card {a∈A. a<i}) else ys!(card {a∈-A. a<i}))" proof - have "i < length xs + length ys" using length_weave using assms by metis then have "i < length [0..<length xs + length ys]" by auto then have "[0..<length xs + length ys] ! i = i" by (metis ‹i < length xs + length ys› add.left_neutral nth_upt) then show ?thesis unfolding weave_def nth_map[OF ‹i < length [0..<length xs + length ys]›] by presburger qed lemma weave_append1: assumes "length xs + length ys ∈ A" assumes "length xs = card {a∈A. a < length xs + length ys}" shows "weave A (xs @ [x]) ys = weave A xs ys @ [x]" proof (rule nth_equalityI) show "length (weave A (xs @ [x]) ys) = length (weave A xs ys @ [x])" unfolding weave_def length_map by simp show "weave A (xs @ [x]) ys ! i = (weave A xs ys @ [x]) ! i" if "i < length (weave A (xs @ [x]) ys)" for i proof - show "weave A (xs @ [x]) ys ! i = (weave A xs ys @ [x]) ! i" proof (cases "i = length xs + length ys") case True then have "(weave A xs ys @ [x]) ! i = x" using length_weave by (metis nth_append_length) have "card {a ∈ A. a < i} = length xs" using assms(2) True by auto then show ?thesis unfolding nth_weave[OF ‹i < length (weave A (xs @ [x]) ys)›] ‹(weave A xs ys @ [x]) ! i = x› using True assms(1) by simp next case False have "i < length (weave A xs ys)" using ‹i < length (weave A (xs @ [x]) ys)› ‹length (weave A (xs @ [x]) ys) = length (weave A xs ys @ [x])› length_append_singleton length_weave less_antisym False by fastforce then have "(weave A xs ys @ [x]) ! i = (weave A xs ys) ! i" by (simp add: nth_append) { assume "i∈A" have "i<length xs + length ys" by (metis ‹i < length (weave A xs ys)› length_weave) then have "{a ∈ A. a < i} ⊂ {a∈A. a < length xs + length ys}" using assms(1) ‹i<length xs + length ys› ‹i∈A› by auto then have "card {a ∈ A. a < i} < card {a∈A. a < length xs + length ys}" using psubset_card_mono[of "{a∈A. a < length xs + length ys}" "{a ∈ A. a < i}"] by simp then have "(xs @ [x]) ! card {a ∈ A. a < i} = xs ! card {a ∈ A. a < i}" by (metis (no_types, lifting) assms(2) nth_append) } then show ?thesis unfolding nth_weave[OF ‹i < length (weave A (xs @ [x]) ys)›] ‹(weave A xs ys @ [x]) ! i = (weave A xs ys) ! i› nth_weave[OF ‹i < length (weave A xs ys)›] by simp qed qed qed lemma weave_append2: assumes "length xs + length ys ∉ A" assumes "length ys = card {a∈-A. a < length xs + length ys}" shows "weave A xs (ys @ [y]) = weave A xs ys @ [y]" proof (rule nth_equalityI) show "length (weave A xs (ys @ [y])) = length (weave A xs ys @ [y])" unfolding weave_def length_map by simp show "weave A xs (ys @ [y]) ! i = (weave A xs ys @ [y]) ! i" if "i < length (weave A xs (ys @ [y]))" for i proof - show "weave A xs (ys @ [y]) ! i = (weave A xs ys @ [y]) ! i" proof (cases "i = length xs + length ys") case True then have "(weave A xs ys @ [y]) ! i = y" using length_weave by (metis nth_append_length) have "card {a ∈ -A. a < i} = length ys" using assms(2) True by auto then show ?thesis unfolding nth_weave[OF ‹i < length (weave A xs (ys @ [y]))›] ‹(weave A xs ys @ [y]) ! i = y› using True assms(1) by simp next case False have "i < length (weave A xs ys)" using ‹i < length (weave A xs (ys @ [y]))› ‹length (weave A xs (ys @ [y])) = length (weave A xs ys @ [y])› length_append_singleton length_weave less_antisym False by fastforce then have "(weave A xs ys @ [y]) ! i = (weave A xs ys) ! i" by (simp add: nth_append) { assume "i∉A" have "i<length xs + length ys" by (metis ‹i < length (weave A xs ys)› length_weave) then have "{a ∈ -A. a < i} ⊂ {a∈-A. a < length xs + length ys}" using assms(1) ‹i<length xs + length ys› ‹i∉A› by auto then have "card {a ∈ -A. a < i} < card {a∈-A. a < length xs + length ys}" using psubset_card_mono[of "{a∈-A. a < length xs + length ys}" "{a ∈ -A. a < i}"] by simp then have "(ys @ [y]) ! card {a ∈ -A. a < i} = ys ! card {a ∈ -A. a < i}" by (metis (no_types, lifting) assms(2) nth_append) } then show ?thesis unfolding nth_weave[OF ‹i < length (weave A xs (ys @ [y]))›] ‹(weave A xs ys @ [y]) ! i = (weave A xs ys) ! i› nth_weave[OF ‹i < length (weave A xs ys)›] by simp qed qed qed lemma nths_nth: assumes "n∈A" "n<length xs" shows "nths xs A ! (card {i. i<n ∧ i∈A}) = xs ! n" using assms proof (induction xs rule:rev_induct) case (snoc x xs) then show ?case proof (cases "n = length xs") case True then show ?thesis unfolding nths_append[of xs "[x]" A] nth_append using length_nths[of xs A] nths_singleton snoc.prems(1) by auto next case False then have "n < length xs" using snoc by auto then have 0:"nths xs A ! card {i. i < n ∧ i ∈ A} = xs ! n" using snoc by auto have "{i. i < n ∧ i ∈ A} ⊂ {i. i < length xs ∧ i ∈ A}" using ‹n < length xs› snoc by force then have "card {i. i < n ∧ i ∈ A} < length (nths xs A)" unfolding length_nths by (simp add: psubset_card_mono) then show ?thesis unfolding nths_append[of xs "[x]" A] nth_append using 0 by (simp add: ‹n < length xs›) qed qed simp lemma list_all2_nths: assumes "list_all2 P (nths xs A) (nths ys A)" and "list_all2 P (nths xs (-A)) (nths ys (-A))" shows "list_all2 P xs ys" proof - have "length xs = length ys" proof (rule ccontr; cases "length xs < length ys") case True then show False proof (cases "length xs ∈ A") case False have "{i. i < length xs ∧ i ∈ - A} ⊂ {i. i < length ys ∧ i ∈ - A}" using False ‹length xs < length ys› by force then have "length (nths ys (-A)) > length (nths xs (-A))" unfolding length_nths by (simp add: psubset_card_mono) then show False using assms(2) list_all2_lengthD not_less_iff_gr_or_eq by blast next case True have "{i. i < length xs ∧ i ∈ A} ⊂ {i. i < length ys ∧ i ∈ A}" using True ‹length xs < length ys› by force then have "length (nths ys A) > length (nths xs A)" unfolding length_nths by (simp add: psubset_card_mono) then show False using assms(1) list_all2_lengthD not_less_iff_gr_or_eq by blast qed next assume "length xs ≠ length ys" case False then have "length xs > length ys" using ‹length xs ≠ length ys› by auto then show False proof (cases "length ys ∈ A") case False have "{i. i < length ys ∧ i ∈ -A} ⊂ {i. i < length xs ∧ i ∈ -A}" using False ‹length xs > length ys› by force then have "length (nths xs (-A)) > length (nths ys (-A))" unfolding length_nths by (simp add: psubset_card_mono) then show False using assms(2) list_all2_lengthD dual_order.strict_implies_not_eq by blast next case True have "{i. i < length ys ∧ i ∈ A} ⊂ {i. i < length xs ∧ i ∈ A}" using True ‹length xs > length ys› by force then have "length (nths xs A) > length (nths ys A)" unfolding length_nths by (simp add: psubset_card_mono) then show False using assms(1) list_all2_lengthD dual_order.strict_implies_not_eq by blast qed qed have "⋀n. n < length xs ⟹ P (xs ! n) (ys ! n)" proof - fix n assume "n < length xs" then have "n < length ys" using ‹length xs = length ys› by auto then show "P (xs ! n) (ys ! n)" proof (cases "n∈A") case True have "{i. i < n ∧ i ∈ A} ⊂ {i. i < length xs ∧ i ∈ A}" using ‹n < length xs› ‹n∈A› by force then have "card {i. i < n ∧ i ∈ A} < length (nths xs A)" unfolding length_nths by (simp add: psubset_card_mono) show ?thesis using nths_nth[OF ‹n∈A› ‹n < length xs›] nths_nth[OF ‹n∈A› ‹n < length ys›] list_all2_nthD[OF assms(1), of "card {i. i < n ∧ i ∈ A}"] length_nths by (simp add: ‹card {i. i < n ∧ i ∈ A} < length (nths xs A)›) next case False then have "n∈-A" by auto have "{i. i < n ∧ i ∈ -A} ⊂ {i. i < length xs ∧ i ∈ -A}" using ‹n < length xs› ‹n∈-A› by force then have "card {i. i < n ∧ i ∈ -A} < length (nths xs (-A))" unfolding length_nths by (simp add: psubset_card_mono) show ?thesis using nths_nth[OF ‹n∈-A› ‹n < length xs›] nths_nth[OF ‹n∈-A› ‹n < length ys›] list_all2_nthD[OF assms(2), of "card {i. i < n ∧ i ∈ -A}"] length_nths using ‹card {i. i < n ∧ i ∈ - A} < length (nths xs (- A))› by auto next qed qed then show ?thesis using ‹length xs = length ys› list_all2_all_nthI by blast qed lemma nths_weave: assumes "length xs = card {a∈A. a < length xs + length ys}" assumes "length ys = card {a∈(-A). a < length xs + length ys}" shows "nths (weave A xs ys) A = xs ∧ nths (weave A xs ys) (-A) = ys" using assms proof (induction "length xs + length ys" arbitrary: xs ys) case 0 then show ?case unfolding weave_def nths_map by simp next case (Suc l) then show ?case proof (cases "l∈A") case True then have "l∈{a ∈ A. a < length xs + length ys}" using Suc.hyps mem_Collect_eq zero_less_Suc by auto then have "length xs > 0" using Suc by fastforce then obtain xs' x where "xs = xs' @ [x]" by (metis append_butlast_last_id length_greater_0_conv) then have "l = length xs' + length ys" using Suc.hyps by simp have length_xs':"length xs' = card {a ∈ A. a < length xs' + length ys}" proof - have "{a ∈ A. a < length xs + length ys} = {a ∈ A. a < length xs' + length ys} ∪ {l}" using ‹xs = xs' @ [x]› ‹l∈{a ∈ A. a < length xs + length ys}› ‹l = length xs' + length ys› by force then have "card {a ∈ A. a < length xs + length ys} = card {a ∈ A. a < length xs' + length ys} + 1" using ‹l = length xs' + length ys› by fastforce then show ?thesis by (metis One_nat_def Suc.prems(1) ‹xs = xs' @ [x]› add_right_imp_eq length_Cons length_append list.size(3)) qed have length_ys:"length ys = card {a ∈ - A. a < length xs' + length ys}" proof - have "l∉{a ∈ - A. a < length xs + length ys}" using ‹l∈A› ‹l = length xs' + length ys› by blast have "{a ∈ -A. a < length xs + length ys} = {a ∈ -A. a < length xs' + length ys}" apply (rule subset_antisym) using ‹l = length xs' + length ys› ‹Suc l = length xs + length ys› ‹l∉{a ∈ - A. a < length xs + length ys}› apply (metis (no_types, lifting) Collect_mono less_Suc_eq mem_Collect_eq) using Collect_mono Suc.hyps(2) ‹l = length xs' + length ys› by auto then show ?thesis using Suc.prems(2) by auto qed have "length xs' + length ys ∈ A" using ‹l∈A› ‹l = length xs' + length ys› by blast then have "nths (weave A xs ys) A = nths (weave A xs' ys @ [x]) A" unfolding ‹xs = xs' @ [x]› using weave_append1[OF ‹length xs' + length ys ∈ A› length_xs'] by metis also have "... = nths (weave A xs' ys) A @ nths [x] {a. a + (length xs' + length ys) ∈ A}" using nths_append length_weave by metis also have "... = nths (weave A xs' ys) A @ [x]" using nths_singleton ‹length xs' + length ys ∈ A› by auto also have "... = xs" using Suc.hyps(1)[OF ‹l = length xs' + length ys› length_xs' length_ys] ‹xs = xs' @ [x]› by presburger finally have "nths (weave A xs ys) A = xs" by metis have "nths (weave A xs ys) (-A) = nths (weave A xs' ys @ [x]) (-A)" unfolding ‹xs = xs' @ [x]› using weave_append1[OF ‹length xs' + length ys ∈ A› length_xs'] by metis also have "... = nths (weave A xs' ys) (-A) @ nths [x] {a. a + (length xs' + length ys) ∈ (-A)}" using nths_append length_weave by metis also have "... = nths (weave A xs' ys) (-A)" using nths_singleton ‹length xs' + length ys ∈ A› by auto also have "... = ys" using Suc.hyps(1)[OF ‹l = length xs' + length ys› length_xs' length_ys] by presburger finally show ?thesis using ‹nths (weave A xs ys) A = xs› by auto next case False then have "l∉{a ∈ A. a < length xs + length ys}" using Suc.hyps mem_Collect_eq zero_less_Suc by auto then have "length ys > 0" using Suc by fastforce then obtain ys' y where "ys = ys' @ [y]" by (metis append_butlast_last_id length_greater_0_conv) then have "l = length xs + length ys'" using Suc.hyps by simp have length_ys':"length ys' = card {a ∈ -A. a < length xs + length ys'}" proof - have "{a ∈ -A. a < length xs + length ys} = {a ∈ -A. a < length xs + length ys'} ∪ {l}" using ‹ys = ys' @ [y]› ‹l∉{a ∈ A. a < length xs + length ys}› ‹l = length xs + length ys'› by force then have "card {a ∈ -A. a < length xs + length ys} = card {a ∈ -A. a < length xs + length ys'} + 1" using ‹l = length xs + length ys'› by fastforce then show ?thesis by (metis One_nat_def Suc.prems(2) ‹ys = ys' @ [y]› add_right_imp_eq length_Cons length_append list.size(3)) qed have length_xs:"length xs = card {a ∈ A. a < length xs + length ys'}" proof - have "l∉{a ∈ A. a < length xs + length ys}" using ‹l∉A› ‹l = length xs + length ys'› by blast have "{a ∈ A. a < length xs + length ys} = {a ∈ A. a < length xs + length ys'}" apply (rule subset_antisym) using ‹l = length xs + length ys'› ‹Suc l = length xs + length ys› ‹l∉{a ∈ A. a < length xs + length ys}› apply (metis (no_types, lifting) Collect_mono less_Suc_eq mem_Collect_eq) using Collect_mono Suc.hyps(2) ‹l = length xs + length ys'› by auto then show ?thesis using Suc.prems(1) by auto qed have "length xs + length ys' ∉ A" using ‹l∉A› ‹l = length xs + length ys'› by blast then have "nths (weave A xs ys) A = nths (weave A xs ys' @ [y]) A" unfolding ‹ys = ys' @ [y]› using weave_append2[OF ‹length xs + length ys' ∉ A› length_ys'] by metis also have "... = nths (weave A xs ys') A @ nths [y] {a. a + (length xs + length ys') ∈ A}" using nths_append length_weave by metis also have "... = nths (weave A xs ys') A" using nths_singleton ‹length xs + length ys' ∉ A› by auto also have "... = xs" using Suc.hyps(1)[OF ‹l = length xs + length ys'› length_xs length_ys'] by auto finally have "nths (weave A xs ys) A = xs" by auto have "nths (weave A xs ys) (-A) = nths (weave A xs ys' @ [y]) (-A)" unfolding ‹ys = ys' @ [y]› using weave_append2[OF ‹length xs + length ys' ∉ A› length_ys'] by metis also have "... = nths (weave A xs ys') (-A) @ nths [y] {a. a + (length xs + length ys') ∈ (-A)}" using nths_append length_weave by metis also have "... = nths (weave A xs ys') (-A) @ [y]" using nths_singleton ‹length xs + length ys' ∉ A› by auto also have "... = ys" using Suc.hyps(1)[OF ‹l = length xs + length ys'› length_xs length_ys'] ‹ys = ys' @ [y]› by simp finally show ?thesis using ‹nths (weave A xs ys) A = xs› by auto qed qed lemma set_weave: assumes "length xs = card {a∈A. a < length xs + length ys}" assumes "length ys = card {a∈-A. a < length xs + length ys}" shows "set (weave A xs ys) = set xs ∪ set ys" proof show "set (weave A xs ys) ⊆ set xs ∪ set ys" proof fix x assume "x∈set (weave A xs ys)" then obtain i where "weave A xs ys ! i = x" "i<length (weave A xs ys)" by (meson in_set_conv_nth) show "x ∈ set xs ∪ set ys" proof (cases "i∈A") case True then have "i ∈ {a∈A. a < length xs + length ys}" unfolding length_weave by (metis ‹i < length (weave A xs ys)› length_weave mem_Collect_eq) then have "{a ∈ A. a < i} ⊂ {a∈A. a < length xs + length ys}" using Collect_mono ‹i < length (weave A xs ys)›[unfolded length_weave] le_Suc_ex less_imp_le_nat trans_less_add1 le_neq_trans less_irrefl mem_Collect_eq by auto then have "card {a ∈ A. a < i} < card {a∈A. a < length xs + length ys}" by (simp add: psubset_card_mono) then show "x ∈ set xs ∪ set ys" unfolding nth_weave[OF ‹i<length (weave A xs ys)›, unfolded ‹weave A xs ys ! i = x›] using True using UnI1 assms(1) nth_mem by auto next case False have "i∉A ⟹ i ∈ {a∈-A. a < length xs + length ys}" unfolding length_weave by (metis ComplI ‹i < length (weave A xs ys)› length_weave mem_Collect_eq) then have "{a ∈ -A. a < i} ⊂ {a∈-A. a < length xs + length ys}" using Collect_mono ‹i < length (weave A xs ys)›[unfolded length_weave] le_Suc_ex less_imp_le_nat trans_less_add1 le_neq_trans less_irrefl mem_Collect_eq using False by auto then have "card {a ∈ -A. a < i} < card {a∈-A. a < length xs + length ys}" by (simp add: psubset_card_mono) then show "x ∈ set xs ∪ set ys" unfolding nth_weave[OF ‹i<length (weave A xs ys)›, unfolded ‹weave A xs ys ! i = x›] using False using UnI1 assms(2) nth_mem by auto qed qed show "set xs ∪ set ys ⊆ set (weave A xs ys)" using nths_weave[OF assms] by (metis Un_subset_iff set_nths_subset) qed lemma weave_complementary_nthss[simp]: "weave A (nths xs A) (nths xs (-A)) = xs" proof (induction xs rule:rev_induct) case Nil then show ?case by (metis gen_length_def length_0_conv length_code length_weave nths_nil) next case (snoc x xs) have length_xs:"length xs = length (nths xs A) + length (nths xs (-A))" by (metis length_weave snoc.IH) show ?case proof (cases "(length xs)∈A") case True have 0:"length (nths xs A) + length (nths xs (-A)) ∈ A" using length_xs True by metis have 1:"length (nths xs A) = card {a ∈ A. a < length (nths xs A) + length (nths xs (-A))}" using length_nths[of xs A] by (metis (no_types, lifting) Collect_cong length_xs) have 2:"nths (xs @ [x]) A = nths xs A @ [x]" unfolding nths_append[of xs "[x]" A] using nths_singleton True by auto have 3:"nths (xs @ [x]) (-A) = nths xs (-A)" unfolding nths_append[of xs "[x]" "-A"] using True by auto show ?thesis unfolding 2 3 weave_append1[OF 0 1] snoc.IH by metis next case False have 0:"length (nths xs A) + length (nths xs (-A)) ∉ A" using length_xs False by metis have 1:"length (nths xs (-A)) = card {a ∈ -A. a < length (nths xs A) + length (nths xs (-A))}" using length_nths[of xs "-A"] by (metis (no_types, lifting) Collect_cong length_xs) have 2:"nths (xs @ [x]) A = nths xs A" unfolding nths_append[of xs "[x]" A] using nths_singleton False by auto have 3:"nths (xs @ [x]) (-A) = nths xs (-A) @ [x]" unfolding nths_append[of xs "[x]" "-A"] using False by auto show ?thesis unfolding 2 3 weave_append2[OF 0 1] snoc.IH by metis qed qed lemma length_nths': "length (nths xs I) = card {i∈I. i < length xs}" unfolding length_nths by meson end