Theory DL_Missing_Sublist
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