theory ListLibLemmas

lemma list_replace_after_notin_new:
  "\<lbrakk>after_in_list list p = Some a; a \<noteq> slot; p \<notin> set list'; p \<noteq> slot\<rbrakk>
    \<Longrightarrow> after_in_list (list_replace_list list slot list') p = Some a" apply(induct list) apply(simp) apply(simp) apply(intro conjI impI) apply(simp add: after_in_list_append_notin_hd) apply(case_tac list, simp, simp) apply(case_tac list, simp, simp split: if_split_asm) apply(insert after_in_list_append_notin_hd) apply(atomize) apply(erule_tac x=p in allE, erule_tac x="[aa]" in allE, erule_tac x="list' @ lista" in allE) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>after_in_list list p = Some a; a \<noteq> slot; p \<notin> set list'; p \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list list slot list') p = Some a proof (prove)
goal (2 subgoals):
 1. \<lbrakk>after_in_list [] p = Some a; a \<noteq> slot; p \<notin> set list'; p \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list [] slot list') p = Some a
 2. \<And>aa list. \<lbrakk>\<lbrakk>after_in_list list p = Some a; a \<noteq> slot; p \<notin> set list'; p \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list list slot list') p = Some a; after_in_list (aa # list) p = Some a; a \<noteq> slot; p \<notin> set list'; p \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list (aa # list) slot list') p = Some a proof (prove)
goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>\<lbrakk>after_in_list list p = Some a; a \<noteq> slot; p \<notin> set list'; p \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list list slot list') p = Some a; after_in_list (aa # list) p = Some a; a \<noteq> slot; p \<notin> set list'; p \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list (aa # list) slot list') p = Some a proof (prove)
goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>after_in_list list p = Some a \<Longrightarrow> after_in_list (list_replace_list list slot list') p = Some a; after_in_list (aa # list) p = Some a; a \<noteq> slot; p \<notin> set list'; p \<noteq> slot\<rbrakk> \<Longrightarrow> (aa = slot \<longrightarrow> after_in_list (list' @ list) p = Some a) \<and> (aa \<noteq> slot \<longrightarrow> after_in_list (aa # list_replace_list list slot list') p = Some a) proof (prove)
goal (2 subgoals):
 1. \<And>aa list. \<lbrakk>after_in_list list p = Some a \<Longrightarrow> after_in_list (list_replace_list list slot list') p = Some a; after_in_list (aa # list) p = Some a; a \<noteq> slot; p \<notin> set list'; p \<noteq> slot; aa = slot\<rbrakk> \<Longrightarrow> after_in_list (list' @ list) p = Some a
 2. \<And>aa list. \<lbrakk>after_in_list list p = Some a \<Longrightarrow> after_in_list (list_replace_list list slot list') p = Some a; after_in_list (aa # list) p = Some a; a \<noteq> slot; p \<notin> set list'; p \<noteq> slot; aa \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list (aa # list_replace_list list slot list') p = Some a proof (prove)
goal (2 subgoals):
 1. \<And>aa list. \<lbrakk>after_in_list list p = Some a \<Longrightarrow> after_in_list (list_replace_list list slot list') p = Some a; after_in_list (slot # list) p = Some a; a \<noteq> slot; p \<notin> set list'; p \<noteq> slot; aa = slot\<rbrakk> \<Longrightarrow> after_in_list list p = Some a
 2. \<And>aa list. \<lbrakk>after_in_list list p = Some a \<Longrightarrow> after_in_list (list_replace_list list slot list') p = Some a; after_in_list (aa # list) p = Some a; a \<noteq> slot; p \<notin> set list'; p \<noteq> slot; aa \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list (aa # list_replace_list list slot list') p = Some a proof (prove)
goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>after_in_list list p = Some a \<Longrightarrow> after_in_list (list_replace_list list slot list') p = Some a; after_in_list (aa # list) p = Some a; a \<noteq> slot; p \<notin> set list'; p \<noteq> slot; aa \<noteq> slot\<rbrakk> \<Longrightarrow> after_in_list (aa # list_replace_list list slot list') p = Some a proof (prove)
goal (1 subgoal):
 1. \<And>aa list aaa lista. \<lbrakk>a \<noteq> slot; p \<notin> set list'; p \<noteq> slot; aa \<noteq> slot; list = slot # lista; p \<noteq> aa; after_in_list (slot # lista) p = Some a; aaa = slot; after_in_list (list' @ lista) p = Some a\<rbrakk> \<Longrightarrow> after_in_list (aa # list' @ lista) p = Some a proof (prove)
goal (1 subgoal):
 1. \<And>aa list aaa lista. \<lbrakk>a \<noteq> slot; p \<notin> set list'; p \<noteq> slot; aa \<noteq> slot; list = slot # lista; p \<noteq> aa; after_in_list (slot # lista) p = Some a; aaa = slot; after_in_list (list' @ lista) p = Some a; \<And>p list' list. p \<notin> set list' \<Longrightarrow> after_in_list (list' @ list) p = after_in_list list p\<rbrakk> \<Longrightarrow> after_in_list (aa # list' @ lista) p = Some a proof (prove)
goal (1 subgoal):
 1. \<And>aa list aaa lista. \<lbrakk>a \<noteq> slot; p \<notin> set list'; p \<noteq> slot; aa \<noteq> slot; list = slot # lista; p \<noteq> aa; after_in_list (slot # lista) p = Some a; aaa = slot; after_in_list (list' @ lista) p = Some a; \<forall>p list' list. p \<notin> set list' \<longrightarrow> after_in_list (list' @ list) p = after_in_list list p\<rbrakk> \<Longrightarrow> after_in_list (aa # list' @ lista) p = Some a proof (prove)
goal (1 subgoal):
 1. \<And>aa list aaa lista. \<lbrakk>a \<noteq> slot; p \<notin> set list'; p \<noteq> slot; aa \<noteq> slot; list = slot # lista; p \<noteq> aa; after_in_list (slot # lista) p = Some a; aaa = slot; after_in_list (list' @ lista) p = Some a; p \<notin> set [aa] \<longrightarrow> after_in_list ([aa] @ list' @ lista) p = after_in_list (list' @ lista) p\<rbrakk> \<Longrightarrow> after_in_list (aa # list' @ lista) p = Some a proof (prove)
goal:
No subgoals!