theory ListLibLemmas

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

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