header {* \isaheader{Auxiliary lemmas} *}
theory AuxLemmas imports Main begin
abbreviation "arbitrary == undefined"
text {* Lemmas about left- and rightmost elements in lists *}
lemma leftmost_element_property:
assumes "∃x ∈ set xs. P x"
obtains zs x' ys where "xs = zs@x'#ys" and "P x'" and "∀z ∈ set zs. ¬ P z"
proof(atomize_elim)
from `∃x ∈ set xs. P x`
show "∃zs x' ys. xs = zs @ x' # ys ∧ P x' ∧ (∀z∈set zs. ¬ P z)"
proof(induct xs)
case Nil thus ?case by simp
next
case (Cons x' xs')
note IH = `∃a∈set xs'. P a
==> ∃zs x' ys. xs' = zs@x'#ys ∧ P x' ∧ (∀z∈set zs. ¬ P z)`
show ?case
proof (cases "P x'")
case True
then have "(∃ys. x' # xs' = [] @ x' # ys) ∧ P x' ∧ (∀x∈set []. ¬ P x)" by simp
then show ?thesis by blast
next
case False
with `∃y∈set (x'#xs'). P y` have "∃y∈set xs'. P y" by simp
from IH[OF this] obtain y ys zs where "xs' = zs@y#ys"
and "P y" and "∀z∈set zs. ¬ P z" by blast
from `∀z∈set zs. ¬ P z` False have "∀z∈set (x'#zs). ¬ P z" by simp
with `xs' = zs@y#ys` `P y` show ?thesis by (metis Cons_eq_append_conv)
qed
qed
qed
lemma rightmost_element_property:
assumes "∃x ∈ set xs. P x"
obtains ys x' zs where "xs = ys@x'#zs" and "P x'" and "∀z ∈ set zs. ¬ P z"
proof(atomize_elim)
from `∃x ∈ set xs. P x`
show "∃ys x' zs. xs = ys @ x' # zs ∧ P x' ∧ (∀z∈set zs. ¬ P z)"
proof(induct xs)
case Nil thus ?case by simp
next
case (Cons x' xs')
note IH = `∃a∈set xs'. P a
==> ∃ys x' zs. xs' = ys @ x' # zs ∧ P x' ∧ (∀z∈set zs. ¬ P z)`
show ?case
proof(cases "∃y∈set xs'. P y")
case True
from IH[OF this] obtain y ys zs where "xs' = ys @ y # zs"
and "P y" and "∀z∈set zs. ¬ P z" by blast
thus ?thesis by (metis Cons_eq_append_conv)
next
case False
with `∃y∈set (x'#xs'). P y` have "P x'" by simp
with False show ?thesis by (metis eq_Nil_appendI)
qed
qed
qed
text {* Lemma concerning maps and @{text @} *}
lemma map_append_append_maps:
assumes map:"map f xs = ys@zs"
obtains xs' xs'' where "map f xs' = ys" and "map f xs'' = zs" and "xs=xs'@xs''"
by (metis append_eq_conv_conj append_take_drop_id assms drop_map take_map that)
text {* Lemma concerning splitting of @{term list}s *}
lemma path_split_general:
assumes all:"∀zs. xs ≠ ys@zs"
obtains j zs where "xs = (take j ys)@zs" and "j < length ys"
and "∀k > j. ∀zs'. xs ≠ (take k ys)@zs'"
proof(atomize_elim)
from `∀zs. xs ≠ ys@zs`
show "∃j zs. xs = take j ys @ zs ∧ j < length ys ∧
(∀k>j. ∀zs'. xs ≠ take k ys @ zs')"
proof(induct ys arbitrary:xs)
case Nil thus ?case by auto
next
case (Cons y' ys')
note IH = `!!xs. ∀zs. xs ≠ ys' @ zs ==>
∃j zs. xs = take j ys' @ zs ∧ j < length ys' ∧
(∀k. j < k --> (∀zs'. xs ≠ take k ys' @ zs'))`
show ?case
proof(cases xs)
case Nil thus ?thesis by simp
next
case (Cons x' xs')
with `∀zs. xs ≠ (y' # ys') @ zs` have "x' ≠ y' ∨ (∀zs. xs' ≠ ys' @ zs)"
by simp
show ?thesis
proof(cases "x' = y'")
case True
with `x' ≠ y' ∨ (∀zs. xs' ≠ ys' @ zs)` have "∀zs. xs' ≠ ys' @ zs" by simp
from IH[OF this] have "∃j zs. xs' = take j ys' @ zs ∧ j < length ys' ∧
(∀k. j < k --> (∀zs'. xs' ≠ take k ys' @ zs'))" .
then obtain j zs where "xs' = take j ys' @ zs"
and "j < length ys'"
and all_sub:"∀k. j < k --> (∀zs'. xs' ≠ take k ys' @ zs')"
by blast
from `xs' = take j ys' @ zs` True
have "(x'#xs') = take (Suc j) (y' # ys') @ zs"
by simp
from all_sub True have all_imp:"∀k. j < k -->
(∀zs'. (x'#xs') ≠ take (Suc k) (y' # ys') @ zs')"
by auto
{ fix l assume "(Suc j) < l"
then obtain k where [simp]:"l = Suc k" by(cases l) auto
with `(Suc j) < l` have "j < k" by simp
with all_imp
have "∀zs'. (x'#xs') ≠ take (Suc k) (y' # ys') @ zs'"
by simp
hence "∀zs'. (x'#xs') ≠ take l (y' # ys') @ zs'"
by simp }
with `(x'#xs') = take (Suc j) (y' # ys') @ zs` `j < length ys'` Cons
show ?thesis by (metis Suc_length_conv less_Suc_eq_0_disj)
next
case False
with Cons have "∀i zs'. i > 0 --> xs ≠ take i (y' # ys') @ zs'"
by auto(case_tac i,auto)
moreover
have "∃zs. xs = take 0 (y' # ys') @ zs" by simp
ultimately show ?thesis by(rule_tac x="0" in exI,auto)
qed
qed
qed
qed
end