theory Heap_List

lemma heap_ls_remove_middle:
  "\<lbrakk>heap_ls hp st (xs @ a # ys); xs \<noteq> []; ys \<noteq> []\<rbrakk>
   \<Longrightarrow> heap_ls (hp(last xs := Some (hd ys), a := None)) st (xs @ ys)" apply (frule heap_ls_distinct) apply simp apply (rule_tac x="Some (hd ys)" in exI) apply (rule conjI) apply (fastforce intro: heap_path_heap_upd_not_in heap_path_last_update) apply (rule heap_path_heap_upd_not_in) apply (rule heap_path_heap_upd_not_in) using heap_path_head apply fastforce apply force apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st (xs @ a # ys); xs \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> heap_ls (hp(last xs \<mapsto> hd ys, a := None)) st (xs @ ys) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st (xs @ a # ys); xs \<noteq> []; ys \<noteq> []; distinct (xs @ a # ys)\<rbrakk> \<Longrightarrow> heap_ls (hp(last xs \<mapsto> hd ys, a := None)) st (xs @ ys) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_path hp st xs (Some a) \<and> heap_ls hp (hp a) ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> a \<notin> set ys \<and> distinct ys \<and> a \<notin> set xs \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> \<exists>x. heap_path (hp(last xs \<mapsto> hd ys, a := None)) st xs x \<and> heap_ls (hp(last xs \<mapsto> hd ys, a := None)) x ys proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_path hp st xs (Some a) \<and> heap_ls hp (hp a) ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> a \<notin> set ys \<and> distinct ys \<and> a \<notin> set xs \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> heap_path (hp(last xs \<mapsto> hd ys, a := None)) st xs (Some (hd ys)) \<and> heap_ls (hp(last xs \<mapsto> hd ys, a := None)) (Some (hd ys)) ys proof (prove)
goal (2 subgoals):
 1. \<lbrakk>heap_path hp st xs (Some a) \<and> heap_ls hp (hp a) ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> a \<notin> set ys \<and> distinct ys \<and> a \<notin> set xs \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> heap_path (hp(last xs \<mapsto> hd ys, a := None)) st xs (Some (hd ys))
 2. \<lbrakk>heap_path hp st xs (Some a) \<and> heap_ls hp (hp a) ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> a \<notin> set ys \<and> distinct ys \<and> a \<notin> set xs \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> heap_ls (hp(last xs \<mapsto> hd ys, a := None)) (Some (hd ys)) ys proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_path hp st xs (Some a) \<and> heap_ls hp (hp a) ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> a \<notin> set ys \<and> distinct ys \<and> a \<notin> set xs \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> heap_ls (hp(last xs \<mapsto> hd ys, a := None)) (Some (hd ys)) ys proof (prove)
goal (2 subgoals):
 1. \<lbrakk>heap_path hp st xs (Some a) \<and> heap_ls hp (hp a) ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> a \<notin> set ys \<and> distinct ys \<and> a \<notin> set xs \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> heap_ls (hp(last xs \<mapsto> hd ys)) (Some (hd ys)) ys
 2. \<lbrakk>heap_path hp st xs (Some a) \<and> heap_ls hp (hp a) ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> a \<notin> set ys \<and> distinct ys \<and> a \<notin> set xs \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> a \<notin> set ys proof (prove)
goal (3 subgoals):
 1. \<lbrakk>heap_path hp st xs (Some a) \<and> heap_ls hp (hp a) ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> a \<notin> set ys \<and> distinct ys \<and> a \<notin> set xs \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> heap_ls hp (Some (hd ys)) ys
 2. \<lbrakk>heap_path hp st xs (Some a) \<and> heap_ls hp (hp a) ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> a \<notin> set ys \<and> distinct ys \<and> a \<notin> set xs \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> last xs \<notin> set ys
 3. \<lbrakk>heap_path hp st xs (Some a) \<and> heap_ls hp (hp a) ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> a \<notin> set ys \<and> distinct ys \<and> a \<notin> set xs \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> a \<notin> set ys proof (prove)
using this:
\<lbrakk>heap_path ?hp ?st ?xs ?y; ?xs \<noteq> []\<rbrakk> \<Longrightarrow> ?st = Some (hd ?xs)

goal (3 subgoals):
 1. \<lbrakk>heap_path hp st xs (Some a) \<and> heap_ls hp (hp a) ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> a \<notin> set ys \<and> distinct ys \<and> a \<notin> set xs \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> heap_ls hp (Some (hd ys)) ys
 2. \<lbrakk>heap_path hp st xs (Some a) \<and> heap_ls hp (hp a) ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> a \<notin> set ys \<and> distinct ys \<and> a \<notin> set xs \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> last xs \<notin> set ys
 3. \<lbrakk>heap_path hp st xs (Some a) \<and> heap_ls hp (hp a) ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> a \<notin> set ys \<and> distinct ys \<and> a \<notin> set xs \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> a \<notin> set ys proof (prove)
goal (2 subgoals):
 1. \<lbrakk>heap_path hp st xs (Some a) \<and> heap_ls hp (hp a) ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> a \<notin> set ys \<and> distinct ys \<and> a \<notin> set xs \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> last xs \<notin> set ys
 2. \<lbrakk>heap_path hp st xs (Some a) \<and> heap_ls hp (hp a) ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> a \<notin> set ys \<and> distinct ys \<and> a \<notin> set xs \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> a \<notin> set ys proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_path hp st xs (Some a) \<and> heap_ls hp (hp a) ys; xs \<noteq> []; ys \<noteq> []; distinct xs \<and> a \<notin> set ys \<and> distinct ys \<and> a \<notin> set xs \<and> set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> a \<notin> set ys proof (prove)
goal:
No subgoals!