theory Heap_List

lemma heap_path_distinct_next_cases: (* the other direction needs sym_heap *)
  "\<lbrakk>heap_path hp st xs ed; distinct xs; p \<in> set xs; hp p = Some np\<rbrakk>
  \<Longrightarrow> ed = Some p \<or> ed = Some np \<or> np \<in> set xs" apply (cases ed; simp) 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)") apply (drule heap_path_non_nil_lookup_next) apply (case_tac "drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs"; simp) apply (metis in_set_dropD list.set_intros(1)) apply simp apply (frule in_list_decompose_takeWhile) apply (subgoal_tac "heap_path hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs) ed") apply (frule heap_path_non_nil_lookup_next) apply (case_tac "drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs", simp) apply (simp split: if_split_asm) apply (drule (1) distinct_decompose2) apply clarsimp by (metis in_set_dropD list.set_intros(1)) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_path hp st xs ed; distinct xs; p \<in> set xs; hp p = Some np\<rbrakk> \<Longrightarrow> ed = Some p \<or> ed = Some np \<or> np \<in> set xs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>heap_ls hp st xs; distinct xs; p \<in> set xs; hp p = Some np; ed = None\<rbrakk> \<Longrightarrow> np \<in> set xs
 2. \<And>a. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; hp p = Some np; ed = Some a\<rbrakk> \<Longrightarrow> a = p \<or> a = np \<or> np \<in> set xs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>heap_ls hp st xs; distinct xs; p \<in> set xs; hp p = Some np; ed = None; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs\<rbrakk> \<Longrightarrow> np \<in> set xs
 2. \<And>a. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; hp p = Some np; ed = Some a\<rbrakk> \<Longrightarrow> a = p \<or> a = np \<or> np \<in> set xs proof (prove)
goal (3 subgoals):
 1. \<lbrakk>heap_ls hp st xs; distinct xs; p \<in> set xs; hp p = Some np; ed = None; 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> np \<in> set xs
 2. \<lbrakk>heap_ls hp st xs; distinct xs; p \<in> set xs; hp p = Some np; ed = None; 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)
 3. \<And>a. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; hp p = Some np; ed = Some a\<rbrakk> \<Longrightarrow> a = p \<or> a = np \<or> np \<in> set xs proof (prove)
goal (3 subgoals):
 1. \<lbrakk>heap_ls hp st xs; distinct xs; p \<in> set xs; hp p = Some np; ed = None; 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> np \<in> set xs
 2. \<lbrakk>heap_ls hp st xs; distinct xs; p \<in> set xs; hp p = Some np; ed = None; 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)
 3. \<And>a. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; hp p = Some np; ed = Some a\<rbrakk> \<Longrightarrow> a = p \<or> a = np \<or> np \<in> set xs proof (prove)
goal (3 subgoals):
 1. \<And>a list. \<lbrakk>heap_ls hp st xs; distinct xs; p \<in> set xs; a = np; ed = None; 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. \<lbrakk>heap_ls hp st xs; distinct xs; p \<in> set xs; hp p = Some np; ed = None; 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)
 3. \<And>a. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; hp p = Some np; ed = Some a\<rbrakk> \<Longrightarrow> a = p \<or> a = np \<or> np \<in> set xs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>heap_ls hp st xs; distinct xs; p \<in> set xs; hp p = Some np; ed = None; 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. \<And>a. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; hp p = Some np; ed = Some a\<rbrakk> \<Longrightarrow> a = p \<or> a = np \<or> np \<in> set xs proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; hp p = Some np; ed = Some a\<rbrakk> \<Longrightarrow> a = p \<or> a = np \<or> np \<in> set xs proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; hp p = Some np; ed = Some a; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs\<rbrakk> \<Longrightarrow> a = p \<or> a = np \<or> np \<in> set xs proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; hp p = Some np; ed = Some a; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs; heap_path hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs) ed\<rbrakk> \<Longrightarrow> a = p \<or> a = np \<or> np \<in> set xs
 2. \<And>a. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; hp p = Some np; ed = Some a; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs\<rbrakk> \<Longrightarrow> heap_path hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs) ed proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; hp p = Some np; ed = Some a; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs; heap_path hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs) ed; hp p = (case drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs of [] \<Rightarrow> ed | a # list \<Rightarrow> Some (hd (drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs)))\<rbrakk> \<Longrightarrow> a = p \<or> a = np \<or> np \<in> set xs
 2. \<And>a. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; hp p = Some np; ed = Some a; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs\<rbrakk> \<Longrightarrow> heap_path hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs) ed proof (prove)
goal (2 subgoals):
 1. \<And>a aa list. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; hp p = Some np; ed = Some a; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs; heap_path hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs) ed; hp p = (case drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs of [] \<Rightarrow> ed | a # list \<Rightarrow> Some (hd (drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs))); drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs = aa # list\<rbrakk> \<Longrightarrow> a = p \<or> a = np \<or> np \<in> set xs
 2. \<And>a. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; hp p = Some np; ed = Some a; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs\<rbrakk> \<Longrightarrow> heap_path hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs) ed proof (prove)
goal (2 subgoals):
 1. \<And>a aa list. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; aa = np; ed = Some a; xs = takeWhile ((\<noteq>) p) xs @ p # np # list; hp p = Some np; drop (Suc (length (takeWhile ((\<noteq>) p) xs))) xs = np # list\<rbrakk> \<Longrightarrow> a = p \<or> a = np \<or> np \<in> set xs
 2. \<And>a. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; hp p = Some np; ed = Some a; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs\<rbrakk> \<Longrightarrow> heap_path hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs) ed proof (prove)
goal (2 subgoals):
 1. \<And>a aa list. \<lbrakk>heap_path hp st xs (Some a); p \<in> set xs; aa = np; ed = Some a; xs = takeWhile ((\<noteq>) p) xs @ p # np # list; hp p = Some np; drop (Suc (length (takeWhile ((\<noteq>) p) xs))) xs = np # list; p \<noteq> np \<and> p \<notin> set (takeWhile ((\<noteq>) p) xs) \<and> np \<notin> set (takeWhile ((\<noteq>) p) xs) \<and> p \<notin> set list \<and> np \<notin> set list\<rbrakk> \<Longrightarrow> a = p \<or> a = np \<or> np \<in> set xs
 2. \<And>a. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; hp p = Some np; ed = Some a; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs\<rbrakk> \<Longrightarrow> heap_path hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs) ed proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>heap_path hp st xs (Some a); p \<in> set xs; ed = Some a; xs = takeWhile ((\<noteq>) p) xs @ p # np # list; hp p = Some np; drop (Suc (length (takeWhile ((\<noteq>) p) xs))) xs = np # list; p \<noteq> np; p \<notin> set (takeWhile ((\<noteq>) p) xs); np \<notin> set (takeWhile ((\<noteq>) p) xs); p \<notin> set list; np \<notin> set list; a \<noteq> p; np \<notin> set xs\<rbrakk> \<Longrightarrow> a = np
 2. \<And>a. \<lbrakk>heap_path hp st xs (Some a); distinct xs; p \<in> set xs; hp p = Some np; ed = Some a; xs = takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs\<rbrakk> \<Longrightarrow> heap_path hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs) ed