theory ListLibLemmas

lemma takeWhile_dropWhile_insert_list_before:
  "\<lbrakk>distinct ls; sorted (map f ls); sfx \<noteq> []; suffix sfx ls;
    \<forall>pfx v. pfx @ sfx = ls \<and> v \<in> set pfx \<longrightarrow> f v \<le> f new; f new < f (hd sfx)\<rbrakk> \<Longrightarrow>
   map fst (takeWhile (\<lambda>(_, t). t \<le> f new) (zip ls (map f ls)))
    @ new
    # map fst (dropWhile (\<lambda>(_, t). t \<le> f new) (zip ls (map f ls)))
   = list_insert_before ls (hd sfx) new" apply (cases sfx; simp) apply (simp add: suffix_def map_fst_takeWhile_zip map_fst_dropWhile_zip) apply (elim exE, rename_tac xs) apply (cut_tac xs=xs and ys="a # list" and new=new in list_insert_before_distinct) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct ls; sorted (map f ls); sfx \<noteq> []; suffix sfx ls; \<forall>pfx v. pfx @ sfx = ls \<and> v \<in> set pfx \<longrightarrow> f v \<le> f new; f new < f (hd sfx)\<rbrakk> \<Longrightarrow> map fst (takeWhile (\<lambda>(uu_, t). t \<le> f new) (zip ls (map f ls))) @ new # map fst (dropWhile (\<lambda>(uu_, t). t \<le> f new) (zip ls (map f ls))) = list_insert_before ls (hd sfx) new proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>distinct ls; sorted (map f ls); suffix (a # list) ls; \<forall>pfx v. pfx @ a # list = ls \<and> v \<in> set pfx \<longrightarrow> f v \<le> f new; f new < f a; sfx = a # list\<rbrakk> \<Longrightarrow> takeWhile (\<lambda>t. f t \<le> f new) ls @ new # dropWhile (\<lambda>t. f t \<le> f new) ls = list_insert_before ls a new proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>distinct ls; sorted (map f ls); \<exists>zs. ls = zs @ a # list; \<forall>pfx v. pfx @ a # list = ls \<and> v \<in> set pfx \<longrightarrow> f v \<le> f new; f new < f a; sfx = a # list\<rbrakk> \<Longrightarrow> takeWhile (\<lambda>t. f t \<le> f new) ls @ new # dropWhile (\<lambda>t. f t \<le> f new) ls = list_insert_before ls a new proof (prove)
goal (1 subgoal):
 1. \<And>a list xs. \<lbrakk>distinct ls; sorted (map f ls); \<forall>pfx v. pfx @ a # list = ls \<and> v \<in> set pfx \<longrightarrow> f v \<le> f new; f new < f a; sfx = a # list; ls = xs @ a # list\<rbrakk> \<Longrightarrow> takeWhile (\<lambda>t. f t \<le> f new) ls @ new # dropWhile (\<lambda>t. f t \<le> f new) ls = list_insert_before ls a new proof (prove)
goal (3 subgoals):
 1. \<And>a list xs. \<lbrakk>distinct ls; sorted (map f ls); \<forall>pfx v. pfx @ a # list = ls \<and> v \<in> set pfx \<longrightarrow> f v \<le> f new; f new < f a; sfx = a # list; ls = xs @ a # list\<rbrakk> \<Longrightarrow> distinct (xs @ a # list)
 2. \<And>a list xs. \<lbrakk>distinct ls; sorted (map f ls); \<forall>pfx v. pfx @ a # list = ls \<and> v \<in> set pfx \<longrightarrow> f v \<le> f new; f new < f a; sfx = a # list; ls = xs @ a # list\<rbrakk> \<Longrightarrow> a # list \<noteq> []
 3. \<And>a list xs. \<lbrakk>distinct ls; sorted (map f ls); \<forall>pfx v. pfx @ a # list = ls \<and> v \<in> set pfx \<longrightarrow> f v \<le> f new; f new < f a; sfx = a # list; ls = xs @ a # list; list_insert_before (xs @ a # list) (hd (a # list)) new = xs @ new # a # list\<rbrakk> \<Longrightarrow> takeWhile (\<lambda>t. f t \<le> f new) ls @ new # dropWhile (\<lambda>t. f t \<le> f new) ls = list_insert_before ls a new proof (prove)
goal:
No subgoals!