kings-crown/FVELER_Isabelle huggingface dataset:
theory Heap_List

lemma in_list_decompose_takeWhile:
  "x \<in> set xs \<Longrightarrow>
   xs = (takeWhile ((\<noteq>) x) xs) @ x # (drop (length (takeWhile ((\<noteq>) x) xs) + 1) xs)" by (induct xs arbitrary: x; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> xs = takeWhile ((\<noteq>) x) xs @ x # drop (length (takeWhile ((\<noteq>) x) xs) + 1) xs
theory Heap_List

lemma takeWhile_neq_hd_eq_Nil[simp]:
  "takeWhile ((\<noteq>) (hd xs)) xs = Nil" by (metis (full_types) hd_Cons_tl takeWhile.simps(1) takeWhile.simps(2))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. takeWhile ((\<noteq>) (hd xs)) xs = []
theory Heap_List

lemma heap_path_takeWhile_lookup_next:
  "\<lbrakk> heap_path hp st rs ed; r \<in> set rs \<rbrakk>
   \<Longrightarrow> heap_path hp st (takeWhile ((\<noteq>) r) rs) (Some r)" apply (drule heap_path_prefix) apply (subgoal_tac "takeWhile ((\<noteq>) r) rs @ [r] \<le> rs", fastforce) by (fastforce dest!: in_list_decompose_takeWhile intro: Prefix_Order.prefixI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_path hp st rs ed; r \<in> set rs\<rbrakk> \<Longrightarrow> heap_path hp st (takeWhile ((\<noteq>) r) rs) (Some r) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> set rs; \<forall>xs\<le>rs. heap_path hp st xs (if xs = [] then st else hp (last xs))\<rbrakk> \<Longrightarrow> heap_path hp st (takeWhile ((\<noteq>) r) rs) (Some r) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> set rs; \<forall>xs\<le>rs. heap_path hp st xs (if xs = [] then st else hp (last xs))\<rbrakk> \<Longrightarrow> takeWhile ((\<noteq>) r) rs @ [r] \<le> rs
theory Heap_List

lemma heap_path_heap_upd_not_in:
  "\<lbrakk>heap_path hp st rs ed; r \<notin> set rs\<rbrakk> \<Longrightarrow> heap_path (hp(r:= x)) st rs ed" by (induct rs arbitrary: st; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_path hp st rs ed; r \<notin> set rs\<rbrakk> \<Longrightarrow> heap_path (hp(r := x)) st rs ed
theory Heap_List

lemma heap_walk_lb:
  "heap_walk hp x xs \<ge> xs" apply (induct xs rule: heap_walk.induct; clarsimp) by (metis Prefix_Order.prefixE Prefix_Order.prefixI append_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xs \<le> heap_walk hp x xs proof (prove)
goal (1 subgoal):
 1. \<And>hp x xs. \<lbrakk>xs @ [x] \<le> heap_walk hp (hp x) (xs @ [x]); x \<notin> set xs\<rbrakk> \<Longrightarrow> xs \<le> heap_walk hp (hp x) (xs @ [x])
theory Heap_List

lemma heal_walk_Some_nonempty':
  "heap_walk hp (Some x) [] > []" by (fastforce intro: heap_walk_lb less_le_trans[where y="[x]"])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. [] < heap_walk hp (Some x) []
theory Heap_List

lemma heap_walk_Nil_None:
  "heap_walk hp st [] = [] \<Longrightarrow> st = None" by (case_tac st; simp only: heal_walk_Some_nonempty)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_walk hp st [] = [] \<Longrightarrow> st = None
theory Heap_List

lemma sym_heapD1:
  "sym_heap hp hp' \<Longrightarrow> hp p = Some p' \<Longrightarrow> hp' p' = Some p" by (clarsimp simp: sym_heap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_heap hp hp'; hp p = Some p'\<rbrakk> \<Longrightarrow> hp' p' = Some p
theory Heap_List

lemma sym_heapD2:
  "sym_heap hp hp' \<Longrightarrow> hp' p' = Some p \<Longrightarrow> hp p = Some p'" by (clarsimp simp: sym_heap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_heap hp hp'; hp' p' = Some p\<rbrakk> \<Longrightarrow> hp p = Some p'
theory Heap_List

lemma sym_heap_symmetric:
  "sym_heap hp hp' \<longleftrightarrow> sym_heap hp' hp" unfolding sym_heap_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sym_heap hp hp' = sym_heap hp' hp proof (prove)
goal (1 subgoal):
 1. (\<forall>p p'. (hp p = Some p') = (hp' p' = Some p)) = (\<forall>p p'. (hp' p = Some p') = (hp p' = Some p))
theory Heap_List

lemma sym_heap_None:
  "\<lbrakk>sym_heap hp hp'; hp p = None\<rbrakk> \<Longrightarrow> \<forall>p'. hp' p' \<noteq> Some p" unfolding sym_heap_def by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_heap hp hp'; hp p = None\<rbrakk> \<Longrightarrow> \<forall>p'. hp' p' \<noteq> Some p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p p'. (hp p = Some p') = (hp' p' = Some p); hp p = None\<rbrakk> \<Longrightarrow> \<forall>p'. hp' p' \<noteq> Some p
theory Heap_List

lemma sym_heap_remove_only:
  "\<lbrakk>sym_heap hp hp'; hp' y = Some x\<rbrakk> \<Longrightarrow> sym_heap (hp(x := None)) (hp'(y := None))" apply (clarsimp simp: sym_heap_def) apply (metis option.inject) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_heap hp hp'; hp' y = Some x\<rbrakk> \<Longrightarrow> sym_heap (hp(x := None)) (hp'(y := None)) proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>\<forall>p p'. (hp p = Some p') = (hp' p' = Some p); hp' y = Some x; p' \<noteq> y; hp' p' = Some x\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Heap_List

lemma sym_heap_remove_only':
  "\<lbrakk>sym_heap hp hp'; hp y = Some x\<rbrakk> \<Longrightarrow> sym_heap (hp(y := None)) (hp'(x := None))" apply (clarsimp simp: sym_heap_def) apply (metis option.inject) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_heap hp hp'; hp y = Some x\<rbrakk> \<Longrightarrow> sym_heap (hp(y := None)) (hp'(x := None)) proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>\<forall>p p'. (hp p = Some p') = (hp' p' = Some p); hp' x = Some y; p' \<noteq> x; hp' p' = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Heap_List

lemma sym_heap_remove_middle_from_chain:
  "\<lbrakk>sym_heap hp hp'; before \<noteq> middle; middle \<noteq> after;
    hp before = Some middle; hp middle = Some after\<rbrakk>
   \<Longrightarrow> sym_heap (hp(before := Some after, middle := None))
                (hp'(after := Some before, middle := None))" apply (clarsimp simp: sym_heap_def) apply (metis option.simps(1)) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_heap hp hp'; before \<noteq> middle; middle \<noteq> after; hp before = Some middle; hp middle = Some after\<rbrakk> \<Longrightarrow> sym_heap (hp(before \<mapsto> after, middle := None)) (hp'(after \<mapsto> before, middle := None)) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p p'. (hp p = Some p') = (hp' p' = Some p); before \<noteq> middle; middle \<noteq> after; hp' middle = Some before; hp' after = Some middle\<rbrakk> \<Longrightarrow> (p = before \<longrightarrow> (\<forall>p'. p' \<noteq> after \<longrightarrow> p' \<noteq> middle \<longrightarrow> hp' p' \<noteq> Some before)) \<and> (p \<noteq> before \<longrightarrow> p = middle \<longrightarrow> (\<forall>p'. p' \<noteq> after \<longrightarrow> p' \<noteq> middle \<longrightarrow> hp' p' \<noteq> Some middle)) proof (prove)
goal:
No subgoals!
theory Heap_List

lemma sym_heap_connect:
  "\<lbrakk>sym_heap hp hp'; hp a = None; hp' b = None \<rbrakk> \<Longrightarrow> sym_heap (hp(a \<mapsto> b)) (hp'(b \<mapsto> a))" by (force simp: sym_heap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_heap hp hp'; hp a = None; hp' b = None\<rbrakk> \<Longrightarrow> sym_heap (hp(a \<mapsto> b)) (hp'(b \<mapsto> a))
theory Heap_List

lemma sym_heap_insert_into_middle_of_chain:
  "\<lbrakk>sym_heap hp hp'; hp before = Some after; hp middle = None; hp' middle = None\<rbrakk>
   \<Longrightarrow> sym_heap (hp(before \<mapsto> middle, middle \<mapsto> after)) (hp'(after \<mapsto> middle, middle \<mapsto> before))" apply (clarsimp simp: sym_heap_def) apply (metis option.simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_heap hp hp'; hp before = Some after; hp middle = None; hp' middle = None\<rbrakk> \<Longrightarrow> sym_heap (hp(before \<mapsto> middle, middle \<mapsto> after)) (hp'(after \<mapsto> middle, middle \<mapsto> before)) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p p'. (hp p = Some p') = (hp' p' = Some p); hp' after = Some before; hp middle = None; hp' middle = None\<rbrakk> \<Longrightarrow> (p = before \<longrightarrow> (before = middle \<longrightarrow> (\<forall>p'. p' \<noteq> after \<longrightarrow> (p' = middle \<longrightarrow> after = middle) \<and> (p' \<noteq> middle \<longrightarrow> hp' p' \<noteq> Some middle))) \<and> (before \<noteq> middle \<longrightarrow> (\<forall>p'. p' \<noteq> after \<longrightarrow> p' \<noteq> middle \<longrightarrow> hp' p' \<noteq> Some before))) \<and> (p \<noteq> before \<longrightarrow> p = middle \<longrightarrow> (\<forall>p'. (p' = after \<longrightarrow> after = middle \<longrightarrow> before = middle) \<and> (p' \<noteq> after \<longrightarrow> (p' = middle \<longrightarrow> (after = middle) = (before = middle)) \<and> (p' \<noteq> middle \<longrightarrow> hp' p' \<noteq> Some middle)))) proof (prove)
goal:
No subgoals!
theory Heap_List

lemma sym_heap_path_reverse:
  "sym_heap hp hp' \<Longrightarrow>
      heap_path hp (Some p) (p#ps) (Some p')
          \<longleftrightarrow> heap_path hp' (Some p') (p'#(rev ps)) (Some p)" unfolding sym_heap_def by (induct ps arbitrary: p p' rule: rev_induct; force)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sym_heap hp hp' \<Longrightarrow> heap_path hp (Some p) (p # ps) (Some p') = heap_path hp' (Some p') (p' # rev ps) (Some p) proof (prove)
goal (1 subgoal):
 1. \<forall>p p'. (hp p = Some p') = (hp' p' = Some p) \<Longrightarrow> heap_path hp (Some p) (p # ps) (Some p') = heap_path hp' (Some p') (p' # rev ps) (Some p)
theory Heap_List

lemma sym_heap_ls_rev_Cons:
  "\<lbrakk>sym_heap hp hp'; heap_ls hp (Some p) (p#ps)\<rbrakk>
  \<Longrightarrow> heap_path hp' (Some (last (p#ps))) (rev ps) (Some p)" supply rev.simps[simp del] apply (induct ps arbitrary: p rule: rev_induct; simp add: rev.simps) by (auto dest!: sym_heap_path_reverse[THEN iffD1])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_heap hp hp'; heap_ls hp (Some p) (p # ps)\<rbrakk> \<Longrightarrow> heap_path hp' (Some (last (p # ps))) (rev ps) (Some p) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_heap hp hp'; heap_ls hp (Some p) (p # ps)\<rbrakk> \<Longrightarrow> heap_path hp' (Some (last (p # ps))) (rev ps) (Some p) proof (prove)
goal (1 subgoal):
 1. \<And>x xs p. \<lbrakk>\<And>p. heap_ls hp (hp p) xs \<Longrightarrow> heap_path hp' (Some (if xs = [] then p else last xs)) (rev xs) (Some p); sym_heap hp hp'; heap_path hp (hp p) xs (Some x) \<and> hp x = None\<rbrakk> \<Longrightarrow> heap_path hp' (hp' x) (rev xs) (Some p)
theory Heap_List

lemma sym_heap_ls_rev:
  "\<lbrakk>sym_heap hp hp'; heap_ls hp (Some p) ps\<rbrakk>
  \<Longrightarrow> heap_path hp' (Some (last ps)) (butlast (rev ps)) (Some p)
      \<and> hp (last ps) = None" apply (induct ps arbitrary: p rule: rev_induct, simp) apply (frule heap_path_head; clarsimp) by (auto dest!: sym_heap_path_reverse[THEN iffD1])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_heap hp hp'; heap_ls hp (Some p) ps\<rbrakk> \<Longrightarrow> heap_path hp' (Some (last ps)) (butlast (rev ps)) (Some p) \<and> hp (last ps) = None proof (prove)
goal (1 subgoal):
 1. \<And>x xs p. \<lbrakk>\<And>p. \<lbrakk>sym_heap hp hp'; heap_ls hp (Some p) xs\<rbrakk> \<Longrightarrow> heap_path hp' (Some (last xs)) (butlast (rev xs)) (Some p) \<and> hp (last xs) = None; sym_heap hp hp'; heap_ls hp (Some p) (xs @ [x])\<rbrakk> \<Longrightarrow> heap_path hp' (Some (last (xs @ [x]))) (butlast (rev (xs @ [x]))) (Some p) \<and> hp (last (xs @ [x])) = None proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<And>p. heap_ls hp (Some p) xs \<Longrightarrow> heap_path hp' (Some (last xs)) (rev (tl xs)) (Some p) \<and> hp (last xs) = None; sym_heap hp hp'; heap_path hp (Some (hd xs)) xs (Some x); hp x = None; xs \<noteq> []\<rbrakk> \<Longrightarrow> heap_path hp' (hp' x) (rev (tl xs)) (Some (hd xs))
theory Heap_List

lemma heap_path_sym_heap_non_nil_lookup_prev:
  "\<lbrakk>heap_ls hp x (xs @ z # ys); sym_heap hp hp'; xs \<noteq> []\<rbrakk> \<Longrightarrow> hp' z = (Some (last xs))" supply heap_path_append[simp del] apply (cut_tac xs="butlast xs" and z="last xs" and ys="z # ys"
              in heap_path_non_nil_lookup_next[where hp=hp and x=x and y=None]) apply (frule append_butlast_last_id) apply (metis append_eq_Cons_conv append_eq_append_conv2) apply (fastforce dest: sym_heapD1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp x (xs @ z # ys); sym_heap hp hp'; xs \<noteq> []\<rbrakk> \<Longrightarrow> hp' z = Some (last xs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp x (xs @ z # ys); sym_heap hp hp'; xs \<noteq> []\<rbrakk> \<Longrightarrow> hp' z = Some (last xs) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>heap_ls hp x (xs @ z # ys); sym_heap hp hp'; xs \<noteq> []\<rbrakk> \<Longrightarrow> heap_ls hp x (butlast xs @ last xs # z # ys)
 2. \<lbrakk>heap_ls hp x (xs @ z # ys); sym_heap hp hp'; xs \<noteq> []; hp (last xs) = (case z # ys of [] \<Rightarrow> None | a # list \<Rightarrow> Some (hd (z # ys)))\<rbrakk> \<Longrightarrow> hp' z = Some (last xs) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>heap_ls hp x (xs @ z # ys); sym_heap hp hp'; xs \<noteq> []; butlast xs @ [last xs] = xs\<rbrakk> \<Longrightarrow> heap_ls hp x (butlast xs @ last xs # z # ys)
 2. \<lbrakk>heap_ls hp x (xs @ z # ys); sym_heap hp hp'; xs \<noteq> []; hp (last xs) = (case z # ys of [] \<Rightarrow> None | a # list \<Rightarrow> Some (hd (z # ys)))\<rbrakk> \<Longrightarrow> hp' z = Some (last xs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp x (xs @ z # ys); sym_heap hp hp'; xs \<noteq> []; hp (last xs) = (case z # ys of [] \<Rightarrow> None | a # list \<Rightarrow> Some (hd (z # ys)))\<rbrakk> \<Longrightarrow> hp' z = Some (last xs) proof (prove)
goal:
No subgoals!
theory Heap_List

lemma heap_ls_prev_of_last:
  "\<lbrakk>t = last ls; Suc 0 < length ls; heap_ls hp st ls; sym_heap hp hp'\<rbrakk>
   \<Longrightarrow> hp' t = Some (last (butlast ls))" apply (cut_tac hp=hp and xs="butlast ls" and z=t and ys="[]"
              in heap_path_sym_heap_non_nil_lookup_prev) apply (prop_tac "ls \<noteq> []", fastforce) apply fastforce apply fastforce apply (fastforce intro!: length_gt_1_imp_butlast_nonempty) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t = last ls; Suc 0 < length ls; heap_ls hp st ls; sym_heap hp hp'\<rbrakk> \<Longrightarrow> hp' t = Some (last (butlast ls)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>t = last ls; Suc 0 < length ls; heap_ls hp st ls; sym_heap hp hp'\<rbrakk> \<Longrightarrow> heap_ls hp ?x (butlast ls @ [t])
 2. \<lbrakk>t = last ls; Suc 0 < length ls; heap_ls hp st ls; sym_heap hp hp'\<rbrakk> \<Longrightarrow> sym_heap hp ?hp'
 3. \<lbrakk>t = last ls; Suc 0 < length ls; heap_ls hp st ls; sym_heap hp hp'\<rbrakk> \<Longrightarrow> butlast ls \<noteq> []
 4. \<lbrakk>t = last ls; Suc 0 < length ls; heap_ls hp st ls; sym_heap hp hp'; ?hp' t = Some (last (butlast ls))\<rbrakk> \<Longrightarrow> hp' t = Some (last (butlast ls)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>t = last ls; Suc 0 < length ls; heap_ls hp st ls; sym_heap hp hp'; ls \<noteq> []\<rbrakk> \<Longrightarrow> heap_ls hp ?x (butlast ls @ [t])
 2. \<lbrakk>t = last ls; Suc 0 < length ls; heap_ls hp st ls; sym_heap hp hp'\<rbrakk> \<Longrightarrow> sym_heap hp ?hp'
 3. \<lbrakk>t = last ls; Suc 0 < length ls; heap_ls hp st ls; sym_heap hp hp'\<rbrakk> \<Longrightarrow> butlast ls \<noteq> []
 4. \<lbrakk>t = last ls; Suc 0 < length ls; heap_ls hp st ls; sym_heap hp hp'; ?hp' t = Some (last (butlast ls))\<rbrakk> \<Longrightarrow> hp' t = Some (last (butlast ls)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>t = last ls; Suc 0 < length ls; heap_ls hp st ls; sym_heap hp hp'\<rbrakk> \<Longrightarrow> sym_heap hp ?hp'
 2. \<lbrakk>t = last ls; Suc 0 < length ls; heap_ls hp st ls; sym_heap hp hp'\<rbrakk> \<Longrightarrow> butlast ls \<noteq> []
 3. \<lbrakk>t = last ls; Suc 0 < length ls; heap_ls hp st ls; sym_heap hp hp'; ?hp' t = Some (last (butlast ls))\<rbrakk> \<Longrightarrow> hp' t = Some (last (butlast ls)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t = last ls; Suc 0 < length ls; heap_ls hp st ls; sym_heap hp hp'\<rbrakk> \<Longrightarrow> butlast ls \<noteq> []
 2. \<lbrakk>t = last ls; Suc 0 < length ls; heap_ls hp st ls; sym_heap hp hp'; hp' t = Some (last (butlast ls))\<rbrakk> \<Longrightarrow> hp' t = Some (last (butlast ls)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t = last ls; Suc 0 < length ls; heap_ls hp st ls; sym_heap hp hp'; hp' t = Some (last (butlast ls))\<rbrakk> \<Longrightarrow> hp' t = Some (last (butlast ls)) proof (prove)
goal:
No subgoals!
theory Heap_List

lemma ptr_in_middle_prev_next:
  "\<lbrakk>heap_ls hp st (xs @ ptr # ys); xs \<noteq> []; ys \<noteq> []; sym_heap hp hp'\<rbrakk>
   \<Longrightarrow> hp' ptr = Some (last xs) \<and> hp ptr = Some (hd ys)" apply (rule conjI) apply (fastforce dest: heap_path_sym_heap_non_nil_lookup_prev) apply (cut_tac hp=hp in heap_path_non_nil_lookup_next) apply fastforce apply (cases ys; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st (xs @ ptr # ys); xs \<noteq> []; ys \<noteq> []; sym_heap hp hp'\<rbrakk> \<Longrightarrow> hp' ptr = Some (last xs) \<and> hp ptr = Some (hd ys) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>heap_ls hp st (xs @ ptr # ys); xs \<noteq> []; ys \<noteq> []; sym_heap hp hp'\<rbrakk> \<Longrightarrow> hp' ptr = Some (last xs)
 2. \<lbrakk>heap_ls hp st (xs @ ptr # ys); xs \<noteq> []; ys \<noteq> []; sym_heap hp hp'\<rbrakk> \<Longrightarrow> hp ptr = Some (hd ys) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st (xs @ ptr # ys); xs \<noteq> []; ys \<noteq> []; sym_heap hp hp'\<rbrakk> \<Longrightarrow> hp ptr = Some (hd ys) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>heap_ls hp st (xs @ ptr # ys); xs \<noteq> []; ys \<noteq> []; sym_heap hp hp'\<rbrakk> \<Longrightarrow> heap_path hp ?x6 (?xs6 @ ?z6 # ?ys6) ?y6
 2. \<lbrakk>heap_ls hp st (xs @ ptr # ys); xs \<noteq> []; ys \<noteq> []; sym_heap hp hp'; hp ?z6 = (case ?ys6 of [] \<Rightarrow> ?y6 | a # list \<Rightarrow> Some (hd ?ys6))\<rbrakk> \<Longrightarrow> hp ptr = Some (hd ys) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st (xs @ ptr # ys); xs \<noteq> []; ys \<noteq> []; sym_heap hp hp'; hp ptr = (case ys of [] \<Rightarrow> None | a # list \<Rightarrow> Some (hd ys))\<rbrakk> \<Longrightarrow> hp ptr = Some (hd ys) proof (prove)
goal:
No subgoals!
theory Heap_List

lemma heap_ls_no_loops:
  "\<lbrakk>heap_ls hp st xs; p \<in> set xs\<rbrakk> \<Longrightarrow> hp p \<noteq> Some p" apply (frule heap_ls_distinct) apply (fastforce dest: split_list heap_path_non_nil_lookup_next split: list.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; p \<in> set xs\<rbrakk> \<Longrightarrow> hp p \<noteq> Some p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; p \<in> set xs; distinct xs\<rbrakk> \<Longrightarrow> hp p \<noteq> Some p proof (prove)
goal:
No subgoals!
theory Heap_List

lemma heap_ls_prev_no_loops:
  "\<lbrakk>heap_ls hp st xs; p \<in> set xs; sym_heap hp hp'\<rbrakk> \<Longrightarrow> hp' p \<noteq> Some p" by (fastforce dest: heap_ls_no_loops sym_heapD2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; p \<in> set xs; sym_heap hp hp'\<rbrakk> \<Longrightarrow> hp' p \<noteq> Some p
theory Heap_List

lemma heap_path_extend:
  "heap_path hp st (ls @ [p]) (hp p) \<longleftrightarrow> heap_path hp st ls (Some p)" by (induct ls rule: rev_induct; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_path hp st (ls @ [p]) (hp p) = heap_path hp st ls (Some p)
theory Heap_List

lemma heap_path_prefix_heap_ls:
  "\<lbrakk>heap_ls hp st xs; heap_path hp st ys ed\<rbrakk> \<Longrightarrow> ys \<le> xs" apply (induct xs arbitrary: ys st, simp) apply (case_tac ys; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; heap_path hp st ys ed\<rbrakk> \<Longrightarrow> ys \<le> xs proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys st. \<lbrakk>\<And>ys st. \<lbrakk>heap_ls hp st xs; heap_path hp st ys ed\<rbrakk> \<Longrightarrow> ys \<le> xs; heap_ls hp st (a # xs); heap_path hp st ys ed\<rbrakk> \<Longrightarrow> ys \<le> a # xs proof (prove)
goal:
No subgoals!
theory Heap_List

lemma distinct_decompose2:
  "\<lbrakk>distinct xs; xs = ys @ x # y # zs\<rbrakk>
   \<Longrightarrow> x \<noteq> y \<and> x \<notin> set ys \<and> y \<notin> set ys \<and> x \<notin> set zs \<and> y \<notin> set zs" by (simp add: in_set_conv_decomp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; xs = ys @ x # y # zs\<rbrakk> \<Longrightarrow> x \<noteq> y \<and> x \<notin> set ys \<and> y \<notin> set ys \<and> x \<notin> set zs \<and> y \<notin> set zs
theory Heap_List

lemma heap_ls_next_in_list:
  "\<lbrakk>heap_ls hp st xs; p \<in> set xs; hp p = Some np\<rbrakk>
  \<Longrightarrow> np \<in> set xs" apply (subgoal_tac "distinct xs") by (fastforce dest!: heap_path_distinct_next_cases) (erule heap_ls_distinct)

(* 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> np \<in> set xs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>heap_ls hp st xs; p \<in> set xs; hp p = Some np; distinct xs\<rbrakk> \<Longrightarrow> np \<in> set xs
 2. \<lbrakk>heap_ls hp st xs; p \<in> set xs; hp p = Some np\<rbrakk> \<Longrightarrow> distinct xs
theory Heap_List

lemma heap_ls_prev_cases:
  "\<lbrakk>heap_ls hp st xs; np \<in> set xs; hp p = Some np; sym_heap hp hp'\<rbrakk>
  \<Longrightarrow> st = Some np \<or> p \<in> set xs" apply (subgoal_tac "distinct xs") by (fastforce dest!: heap_path_distinct_sym_prev_cases) (erule heap_ls_distinct)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st 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 (2 subgoals):
 1. \<lbrakk>heap_ls hp st xs; np \<in> set xs; hp p = Some np; sym_heap hp hp'; distinct xs\<rbrakk> \<Longrightarrow> st = Some np \<or> p \<in> set xs
 2. \<lbrakk>heap_ls hp st xs; np \<in> set xs; hp p = Some np; sym_heap hp hp'\<rbrakk> \<Longrightarrow> distinct xs
theory Heap_List

lemma heap_ls_prev_not_in:
  "\<lbrakk>heap_ls hp st xs; np \<notin> set xs; hp p = Some np\<rbrakk>
  \<Longrightarrow> p \<notin> set xs" by (meson heap_ls_next_in_list)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp st xs; np \<notin> set xs; hp p = Some np\<rbrakk> \<Longrightarrow> p \<notin> set xs
theory Heap_List

lemma heap_path_distinct_prev_not_in:
  "\<lbrakk>heap_path hp st xs ed; distinct xs; np \<notin> set xs; hp p = Some np; ed \<noteq> Some np; ed \<noteq> Some p\<rbrakk>
  \<Longrightarrow> p \<notin> set xs" using heap_path_distinct_next_cases by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_path hp st xs ed; distinct xs; np \<notin> set xs; hp p = Some np; ed \<noteq> Some np; ed \<noteq> Some p\<rbrakk> \<Longrightarrow> p \<notin> set xs proof (prove)
using this:
\<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

goal (1 subgoal):
 1. \<lbrakk>heap_path hp st xs ed; distinct xs; np \<notin> set xs; hp p = Some np; ed \<noteq> Some np; ed \<noteq> Some p\<rbrakk> \<Longrightarrow> p \<notin> set xs