theory Heap_List

lemma heap_path_distinct_sym_prev_cases:
  "\<lbrakk>heap_path hp st xs ed; distinct xs; np \<in> set xs; hp p = Some np; sym_heap hp hp'\<rbrakk>
  \<Longrightarrow> st = Some np \<or> p \<in> set xs" apply (cases st; simp) apply (rename_tac stp) apply (case_tac "stp = np"; simp) apply (cases xs; simp del: heap_path.simps) apply (frule heap_path_head, simp) apply (cases ed, clarsimp) apply (frule sym_heap_ls_rev_Cons, fastforce) apply (drule heap_path_distinct_next_cases[where hp=hp']; simp add: sym_heap_def) apply simp apply (simp del: heap_path.simps) apply (frule (1) sym_heap_path_reverse[where hp'=hp', THEN iffD1]) apply simp apply (frule heap_path_distinct_next_cases[where hp=hp']; simp add: sym_heap_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_path hp st xs ed; distinct xs; np \<in> set xs; hp p = Some np; sym_heap hp hp'\<rbrakk> \<Longrightarrow> st = Some np \<or> p \<in> set xs proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>heap_path hp (Some a) xs ed; distinct xs; np \<in> set xs; hp p = Some np; sym_heap hp hp'; st = Some a\<rbrakk> \<Longrightarrow> a = np \<or> p \<in> set xs proof (prove)
goal (1 subgoal):
 1. \<And>stp. \<lbrakk>heap_path hp (Some stp) xs ed; distinct xs; np \<in> set xs; hp p = Some np; sym_heap hp hp'; st = Some stp\<rbrakk> \<Longrightarrow> stp = np \<or> p \<in> set xs proof (prove)
goal (1 subgoal):
 1. \<And>stp. \<lbrakk>heap_path hp (Some stp) xs ed; distinct xs; np \<in> set xs; hp p = Some np; sym_heap hp hp'; st = Some stp; stp \<noteq> np\<rbrakk> \<Longrightarrow> p \<in> set xs proof (prove)
goal (1 subgoal):
 1. \<And>stp a list. \<lbrakk>heap_path hp (Some stp) (a # list) ed; a \<notin> set list \<and> distinct list; np = a \<or> np \<in> set list; hp p = Some np; sym_heap hp hp'; st = Some stp; stp \<noteq> np; xs = a # list\<rbrakk> \<Longrightarrow> p = a \<or> p \<in> set list proof (prove)
goal (1 subgoal):
 1. \<And>stp a list. \<lbrakk>heap_path hp (Some stp) (a # list) ed; a \<notin> set list \<and> distinct list; np = a \<or> np \<in> set list; hp p = Some np; sym_heap hp hp'; st = Some stp; stp \<noteq> np; xs = a # list; Some stp = Some (hd (a # list))\<rbrakk> \<Longrightarrow> p = a \<or> p \<in> set list proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>heap_ls hp (hp a) list; np \<in> set list; hp p = Some np; sym_heap hp hp'; st = Some a; a \<noteq> np; xs = a # list; ed = None; a \<notin> set list; distinct list; p \<notin> set list\<rbrakk> \<Longrightarrow> p = a
 2. \<And>stp a list aa. \<lbrakk>heap_path hp (Some stp) (a # list) ed; a \<notin> set list \<and> distinct list; np = a \<or> np \<in> set list; hp p = Some np; sym_heap hp hp'; st = Some stp; stp \<noteq> np; xs = a # list; Some stp = Some (hd (a # list)); ed = Some aa\<rbrakk> \<Longrightarrow> p = a \<or> p \<in> set list proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>heap_ls hp (hp a) list; np \<in> set list; hp p = Some np; sym_heap hp hp'; st = Some a; a \<noteq> np; xs = a # list; ed = None; a \<notin> set list; distinct list; p \<notin> set list; heap_path hp' (Some (last (a # list))) (rev list) (Some a)\<rbrakk> \<Longrightarrow> p = a
 2. \<And>stp a list aa. \<lbrakk>heap_path hp (Some stp) (a # list) ed; a \<notin> set list \<and> distinct list; np = a \<or> np \<in> set list; hp p = Some np; sym_heap hp hp'; st = Some stp; stp \<noteq> np; xs = a # list; Some stp = Some (hd (a # list)); ed = Some aa\<rbrakk> \<Longrightarrow> p = a \<or> p \<in> set list proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>heap_ls hp (hp a) list; np \<in> set list; hp' np = Some p; \<forall>p p'. (hp p = Some p') = (hp' p' = Some p); st = Some a; a \<noteq> np; xs = a # list; ed = None; a \<notin> set list; distinct list; p \<notin> set list; a = np \<or> a = p \<or> p \<in> set list\<rbrakk> \<Longrightarrow> p = a
 2. \<And>stp a list aa. \<lbrakk>heap_path hp (Some stp) (a # list) ed; a \<notin> set list \<and> distinct list; np = a \<or> np \<in> set list; hp p = Some np; sym_heap hp hp'; st = Some stp; stp \<noteq> np; xs = a # list; Some stp = Some (hd (a # list)); ed = Some aa\<rbrakk> \<Longrightarrow> p = a \<or> p \<in> set list proof (prove)
goal (1 subgoal):
 1. \<And>stp a list aa. \<lbrakk>heap_path hp (Some stp) (a # list) ed; a \<notin> set list \<and> distinct list; np = a \<or> np \<in> set list; hp p = Some np; sym_heap hp hp'; st = Some stp; stp \<noteq> np; xs = a # list; Some stp = Some (hd (a # list)); ed = Some aa\<rbrakk> \<Longrightarrow> p = a \<or> p \<in> set list proof (prove)
goal (1 subgoal):
 1. \<And>stp a list aa. \<lbrakk>heap_path hp (Some a) (a # list) (Some aa); a \<notin> set list \<and> distinct list; np \<in> set list; hp p = Some np; sym_heap hp hp'; st = Some a; a \<noteq> np; xs = a # list; stp = a; ed = Some aa\<rbrakk> \<Longrightarrow> p = a \<or> p \<in> set list proof (prove)
goal (1 subgoal):
 1. \<And>stp a list aa. \<lbrakk>heap_path hp (Some a) (a # list) (Some aa); a \<notin> set list \<and> distinct list; np \<in> set list; hp p = Some np; sym_heap hp hp'; st = Some a; a \<noteq> np; xs = a # list; stp = a; ed = Some aa; heap_path hp' (Some aa) (aa # rev list) (Some a)\<rbrakk> \<Longrightarrow> p = a \<or> p \<in> set list proof (prove)
goal (1 subgoal):
 1. \<And>stp a list aa. \<lbrakk>heap_path hp (hp a) list (Some aa); a \<notin> set list \<and> distinct list; np \<in> set list; hp p = Some np; sym_heap hp hp'; st = Some a; a \<noteq> np; xs = a # list; stp = a; ed = Some aa; heap_path hp' (hp' aa) (rev list) (Some a)\<rbrakk> \<Longrightarrow> p = a \<or> p \<in> set list proof (prove)
goal (1 subgoal):
 1. \<And>stp a list aa. \<lbrakk>heap_path hp (hp a) list (Some aa); a \<notin> set list \<and> distinct list; np \<in> set list; hp' np = Some p; \<forall>p p'. (hp p = Some p') = (hp' p' = Some p); st = Some a; a \<noteq> np; xs = a # list; stp = a; ed = Some aa; heap_path hp' (hp' aa) (rev list) (Some a); a = np \<or> a = p \<or> p \<in> set list\<rbrakk> \<Longrightarrow> p = a \<or> p \<in> set list proof (prove)
goal:
No subgoals!