section ‹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 ‹@›› 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