theory ListLibLemmas

lemma list_replace_after_notin_old:
  "\<lbrakk>after_in_list list' p = Some a; p \<notin> set list; slot \<in> set list\<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_in_hd) apply(simp) apply(case_tac "list_replace_list list slot list'") apply(simp) apply(simp) done

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