theory ListLibLemmas

lemma list_replace_after_None_notin_old:
  "\<lbrakk>after_in_list list' p = None; p \<in> set list'; p \<notin> set list\<rbrakk>
    \<Longrightarrow> after_in_list (list_replace_list list slot list') p = after_in_list list slot" apply(induct list) apply(simp) apply(simp) apply(intro conjI impI) apply(simp) apply(case_tac list) apply(simp) apply(simp add: after_in_list_append_last_hd) apply(case_tac "list_replace_list list slot list'") apply(simp) apply(case_tac list, simp, simp) apply(simp) apply(case_tac list, simp, simp) done

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