theory Heap_List

lemma heap_ls_next_takeWhile_append:
  "\<lbrakk>heap_ls hp st xs; p \<in> set xs; hp p = Some np\<rbrakk>
  \<Longrightarrow> takeWhile ((\<noteq>) np) xs = (takeWhile ((\<noteq>) p) xs) @ [p]" apply (frule heap_ls_distinct) apply (frule in_list_decompose_takeWhile) apply (subgoal_tac "heap_ls hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs)") prefer 2 apply simp apply (drule heap_path_non_nil_lookup_next) apply (case_tac "drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs"; simp) apply (subgoal_tac "np \<in> set xs") prefer 2 apply (erule (2) heap_ls_next_in_list) apply (frule in_list_decompose_takeWhile[where x=np]) apply (drule (1) distinct_inj_middle[where x=np and xa="takeWhile ((\<noteq>) np) xs" and ya="takeWhile ((\<noteq>) p) xs @ [p]"]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; p \<in> set xs; hp p = Some np\<rbrakk> \<Longrightarrow> takeWhile ((\<noteq>) np) xs = takeWhile ((\<noteq>) p) xs @ [p] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; p \<in> set xs; hp p = Some np; distinct xs\<rbrakk> \<Longrightarrow> takeWhile ((\<noteq>) np) xs = takeWhile ((\<noteq>) p) xs @ [p] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; p \<in> set xs; hp p = Some np; distinct xs; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs\<rbrakk> \<Longrightarrow> takeWhile ((\<noteq>) np) xs = takeWhile ((\<noteq>) p) xs @ [p] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>heap_ls hp st xs; p \<in> set xs; hp p = Some np; distinct xs; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs; heap_ls hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs)\<rbrakk> \<Longrightarrow> takeWhile ((\<noteq>) np) xs = takeWhile ((\<noteq>) p) xs @ [p]
 2. \<lbrakk>heap_ls hp st xs; p \<in> set xs; hp p = Some np; distinct xs; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs\<rbrakk> \<Longrightarrow> heap_ls hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>heap_ls hp st xs; p \<in> set xs; hp p = Some np; distinct xs; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs\<rbrakk> \<Longrightarrow> heap_ls hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs)
 2. \<lbrakk>heap_ls hp st xs; p \<in> set xs; hp p = Some np; distinct xs; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs; heap_ls hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs)\<rbrakk> \<Longrightarrow> takeWhile ((\<noteq>) np) xs = takeWhile ((\<noteq>) p) xs @ [p] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; p \<in> set xs; hp p = Some np; distinct xs; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs; heap_ls hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs)\<rbrakk> \<Longrightarrow> takeWhile ((\<noteq>) np) xs = takeWhile ((\<noteq>) p) xs @ [p] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; p \<in> set xs; hp p = Some np; distinct xs; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs; hp p = (case drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs of [] \<Rightarrow> None | a # list \<Rightarrow> Some (hd (drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs)))\<rbrakk> \<Longrightarrow> takeWhile ((\<noteq>) np) xs = takeWhile ((\<noteq>) p) xs @ [p] proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>heap_ls hp st xs; p \<in> set xs; a = np; distinct xs; xs = takeWhile ((\<noteq>) p) xs @ p # np # list; hp p = Some np; drop (Suc (length (takeWhile ((\<noteq>) p) xs))) xs = np # list\<rbrakk> \<Longrightarrow> takeWhile ((\<noteq>) np) xs = takeWhile ((\<noteq>) p) xs @ [p] proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>heap_ls hp st xs; p \<in> set xs; a = np; distinct xs; xs = takeWhile ((\<noteq>) p) xs @ p # np # list; hp p = Some np; drop (Suc (length (takeWhile ((\<noteq>) p) xs))) xs = np # list; np \<in> set xs\<rbrakk> \<Longrightarrow> takeWhile ((\<noteq>) np) xs = takeWhile ((\<noteq>) p) xs @ [p]
 2. \<And>a list. \<lbrakk>heap_ls hp st xs; p \<in> set xs; a = np; distinct xs; xs = takeWhile ((\<noteq>) p) xs @ p # np # list; hp p = Some np; drop (Suc (length (takeWhile ((\<noteq>) p) xs))) xs = np # list\<rbrakk> \<Longrightarrow> np \<in> set xs proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>heap_ls hp st xs; p \<in> set xs; a = np; distinct xs; xs = takeWhile ((\<noteq>) p) xs @ p # np # list; hp p = Some np; drop (Suc (length (takeWhile ((\<noteq>) p) xs))) xs = np # list\<rbrakk> \<Longrightarrow> np \<in> set xs
 2. \<And>a list. \<lbrakk>heap_ls hp st xs; p \<in> set xs; a = np; distinct xs; xs = takeWhile ((\<noteq>) p) xs @ p # np # list; hp p = Some np; drop (Suc (length (takeWhile ((\<noteq>) p) xs))) xs = np # list; np \<in> set xs\<rbrakk> \<Longrightarrow> takeWhile ((\<noteq>) np) xs = takeWhile ((\<noteq>) p) xs @ [p] proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>heap_ls hp st xs; p \<in> set xs; a = np; distinct xs; xs = takeWhile ((\<noteq>) p) xs @ p # np # list; hp p = Some np; drop (Suc (length (takeWhile ((\<noteq>) p) xs))) xs = np # list; np \<in> set xs\<rbrakk> \<Longrightarrow> takeWhile ((\<noteq>) np) xs = takeWhile ((\<noteq>) p) xs @ [p] proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>heap_ls hp st xs; p \<in> set xs; a = np; distinct xs; xs = takeWhile ((\<noteq>) p) xs @ p # np # list; hp p = Some np; drop (Suc (length (takeWhile ((\<noteq>) p) xs))) xs = np # list; np \<in> set xs; xs = takeWhile ((\<noteq>) np) xs @ np # drop (length (takeWhile ((\<noteq>) np) xs) + 1) xs\<rbrakk> \<Longrightarrow> takeWhile ((\<noteq>) np) xs = takeWhile ((\<noteq>) p) xs @ [p] proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>heap_ls hp st xs; p \<in> set xs; a = np; xs = takeWhile ((\<noteq>) p) xs @ p # np # list; hp p = Some np; drop (Suc (length (takeWhile ((\<noteq>) p) xs))) xs = np # list; np \<in> set xs; xs = takeWhile ((\<noteq>) np) xs @ np # drop (length (takeWhile ((\<noteq>) np) xs) + 1) xs\<rbrakk> \<Longrightarrow> xs = (takeWhile ((\<noteq>) p) xs @ [p]) @ np # ?yb20 a list
 2. \<And>a list. \<lbrakk>heap_ls hp st xs; p \<in> set xs; a = np; xs = takeWhile ((\<noteq>) p) xs @ p # np # list; hp p = Some np; drop (Suc (length (takeWhile ((\<noteq>) p) xs))) xs = np # list; np \<in> set xs; xs = takeWhile ((\<noteq>) np) xs @ np # drop (length (takeWhile ((\<noteq>) np) xs) + 1) xs; takeWhile ((\<noteq>) np) xs = takeWhile ((\<noteq>) p) xs @ [p] \<and> drop (length (takeWhile ((\<noteq>) np) xs) + 1) xs = ?yb20 a list\<rbrakk> \<Longrightarrow> takeWhile ((\<noteq>) np) xs = takeWhile ((\<noteq>) p) xs @ [p] proof (prove)
goal:
No subgoals!