theory Lib

lemma length_takeWhile_gt:
  "n < length (takeWhile f xs)
       \<Longrightarrow> (\<exists>ys zs. length ys = Suc n \<and> xs = ys @ zs \<and> takeWhile f xs = ys @ takeWhile f zs)" apply (induct xs arbitrary: n; simp split: if_split_asm) apply (case_tac n; simp) apply (rule_tac x="[a]" in exI) apply simp apply (erule meta_allE, drule(1) meta_mp) apply clarsimp apply (rule_tac x="a # ys" in exI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < length (takeWhile f xs) \<Longrightarrow> \<exists>ys zs. length ys = Suc n \<and> xs = ys @ zs \<and> takeWhile f xs = ys @ takeWhile f zs proof (prove)
goal (1 subgoal):
 1. \<And>a xs n. \<lbrakk>\<And>n. n < length (takeWhile f xs) \<Longrightarrow> \<exists>ys. length ys = Suc n \<and> (\<exists>zs. xs = ys @ zs \<and> takeWhile f xs = ys @ takeWhile f zs); f a; n < Suc (length (takeWhile f xs))\<rbrakk> \<Longrightarrow> \<exists>ys. length ys = Suc n \<and> (\<exists>zs. a # xs = ys @ zs \<and> a # takeWhile f xs = ys @ takeWhile f zs) proof (prove)
goal (2 subgoals):
 1. \<And>a xs n. \<lbrakk>\<And>n. n < length (takeWhile f xs) \<Longrightarrow> \<exists>ys. length ys = Suc n \<and> (\<exists>zs. xs = ys @ zs \<and> takeWhile f xs = ys @ takeWhile f zs); f a; n = 0\<rbrakk> \<Longrightarrow> \<exists>ys. length ys = Suc 0 \<and> (\<exists>zs. a # xs = ys @ zs \<and> a # takeWhile f xs = ys @ takeWhile f zs)
 2. \<And>a xs n nat. \<lbrakk>\<And>n. n < length (takeWhile f xs) \<Longrightarrow> \<exists>ys. length ys = Suc n \<and> (\<exists>zs. xs = ys @ zs \<and> takeWhile f xs = ys @ takeWhile f zs); f a; nat < length (takeWhile f xs); n = Suc nat\<rbrakk> \<Longrightarrow> \<exists>ys. length ys = Suc (Suc nat) \<and> (\<exists>zs. a # xs = ys @ zs \<and> a # takeWhile f xs = ys @ takeWhile f zs) proof (prove)
goal (2 subgoals):
 1. \<And>a xs n. \<lbrakk>\<And>n. n < length (takeWhile f xs) \<Longrightarrow> \<exists>ys. length ys = Suc n \<and> (\<exists>zs. xs = ys @ zs \<and> takeWhile f xs = ys @ takeWhile f zs); f a; n = 0\<rbrakk> \<Longrightarrow> length [a] = Suc 0 \<and> (\<exists>zs. a # xs = [a] @ zs \<and> a # takeWhile f xs = [a] @ takeWhile f zs)
 2. \<And>a xs n nat. \<lbrakk>\<And>n. n < length (takeWhile f xs) \<Longrightarrow> \<exists>ys. length ys = Suc n \<and> (\<exists>zs. xs = ys @ zs \<and> takeWhile f xs = ys @ takeWhile f zs); f a; nat < length (takeWhile f xs); n = Suc nat\<rbrakk> \<Longrightarrow> \<exists>ys. length ys = Suc (Suc nat) \<and> (\<exists>zs. a # xs = ys @ zs \<and> a # takeWhile f xs = ys @ takeWhile f zs) proof (prove)
goal (1 subgoal):
 1. \<And>a xs n nat. \<lbrakk>\<And>n. n < length (takeWhile f xs) \<Longrightarrow> \<exists>ys. length ys = Suc n \<and> (\<exists>zs. xs = ys @ zs \<and> takeWhile f xs = ys @ takeWhile f zs); f a; nat < length (takeWhile f xs); n = Suc nat\<rbrakk> \<Longrightarrow> \<exists>ys. length ys = Suc (Suc nat) \<and> (\<exists>zs. a # xs = ys @ zs \<and> a # takeWhile f xs = ys @ takeWhile f zs) proof (prove)
goal (1 subgoal):
 1. \<And>a xs n nat. \<lbrakk>f a; nat < length (takeWhile f xs); n = Suc nat; \<exists>ys. length ys = Suc nat \<and> (\<exists>zs. xs = ys @ zs \<and> takeWhile f xs = ys @ takeWhile f zs)\<rbrakk> \<Longrightarrow> \<exists>ys. length ys = Suc (Suc nat) \<and> (\<exists>zs. a # xs = ys @ zs \<and> a # takeWhile f xs = ys @ takeWhile f zs) proof (prove)
goal (1 subgoal):
 1. \<And>a nat ys zs. \<lbrakk>f a; length ys = Suc nat; takeWhile f (ys @ zs) = ys @ takeWhile f zs\<rbrakk> \<Longrightarrow> \<exists>ysa. length ysa = Suc (Suc nat) \<and> (\<exists>zsa. a # ys @ zs = ysa @ zsa \<and> a # ys @ takeWhile f zs = ysa @ takeWhile f zsa) proof (prove)
goal (1 subgoal):
 1. \<And>a nat ys zs. \<lbrakk>f a; length ys = Suc nat; takeWhile f (ys @ zs) = ys @ takeWhile f zs\<rbrakk> \<Longrightarrow> length (a # ys) = Suc (Suc nat) \<and> (\<exists>zsa. a # ys @ zs = (a # ys) @ zsa \<and> a # ys @ takeWhile f zs = (a # ys) @ takeWhile f zsa) proof (prove)
goal:
No subgoals!