lemma least_idx:

  assumes "Q (i::nat)"

  obtains j where "j \<le> i" "Q j" "\<forall> k < j. \<not> Q k"

  using assms

  by (metis ex_least_nat_le le0 not_less0) 

lemma duration_idx:

  assumes "\<not> Q (i::nat)"

  and "Q j"

  and "i \<le> j"

  obtains k where "i \<le> k" "k < j" "\<not> Q k" "\<forall> i'. k < i' \<and> i' \<le> j \<longrightarrow> Q i'" 

proof -

  let ?Q = "\<lambda> t. t \<le> j \<and> \<not> Q (j - t)"

  have "?Q (j - i)" using assms by (simp add: assms(1)) 

  from least_idx [of ?Q, OF this]

  obtain l

  where h: "l \<le> j - i" "\<not> Q (j - l)" "\<forall>k<l. \<not> (k \<le> j \<and> \<not> Q (j - k))"

    by metis

  let ?k = "j - l"

  have "i \<le> ?k" using assms(3) h(1) by linarith 

  moreover have "?k < j" by (metis assms(2) diff_le_self h(2) le_neq_implies_less) 

  moreover have "\<not> Q ?k" by (simp add: h(2)) 

  moreover have "\<forall> i'. ?k < i' \<and> i' \<le> j \<longrightarrow> Q i'"

      by (metis diff_diff_cancel diff_le_self diff_less_mono2 h(3) 

              less_imp_diff_less not_less) 

  ultimately show ?thesis using that by metis

lemma p_split_gen: 

  assumes "Q s"

  and "\<not> Q (moment k s)"

  shows "(\<exists> i. i < length s \<and> k \<le> i \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))"

proof(cases "k \<le> length s")

  case True

  let ?Q = "\<lambda> t. Q (moment t s)"

  have "?Q (length s)" using assms(1) by simp

  from duration_idx[of ?Q, OF assms(2) this True]

  obtain i where h: "k \<le> i" "i < length s" "\<not> Q (moment i s)"

    "\<forall>i'. i < i' \<and> i' \<le> length s \<longrightarrow> Q (moment i' s)" by metis

  moreover have "(\<forall> i' > i. Q (moment i' s))" using h(4) assms(1) not_less

    by fastforce

  ultimately show ?thesis by metis

qed (insert assms, auto)

  assumes qs: "Q s"

  and nq: "\<not> Q []"

  shows "(\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))"

  show ?thesis by auto

  using assms 

  by (simp add:moment_def rev_take, 

      metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop)