theory ListLibLemmas

lemma list_replace_empty_after_empty:
  "\<lbrakk>after_in_list list p = Some slot; distinct list\<rbrakk>
    \<Longrightarrow> after_in_list (list_replace_list list slot []) p = after_in_list list slot" apply(induct list slot rule: after_in_list.induct) apply (simp split: if_split_asm)+ apply (case_tac xs,simp+) apply (case_tac xs,simp+) apply (auto dest!: after_in_list_in_list) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>after_in_list list p = Some slot; distinct list\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list list slot []) p = after_in_list list slot proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>after_in_list [] p = Some a; distinct []\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list [] a []) p = after_in_list [] a
 2. \<And>x a. \<lbrakk>after_in_list [x] p = Some a; distinct [x]\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list [x] a []) p = after_in_list [x] a
 3. \<And>x y xs a. \<lbrakk>\<lbrakk>a \<noteq> x; after_in_list (y # xs) p = Some a; distinct (y # xs)\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list (y # xs) a []) p = after_in_list (y # xs) a; after_in_list (x # y # xs) p = Some a; distinct (x # y # xs)\<rbrakk> \<Longrightarrow> after_in_list (list_replace_list (x # y # xs) a []) p = after_in_list (x # y # xs) a proof (prove)
goal (2 subgoals):
 1. \<And>x y xs a. \<lbrakk>after_in_list (a # xs) x = Some a \<Longrightarrow> after_in_list xs x = after_in_list (a # xs) a; p = x; x \<noteq> a; x \<notin> set xs; a \<notin> set xs; distinct xs; y = a\<rbrakk> \<Longrightarrow> after_in_list (x # xs) x = after_in_list (a # xs) a
 2. \<And>x y xs a. \<lbrakk>a \<noteq> x \<Longrightarrow> after_in_list (if y = a then [] @ xs else y # list_replace_list xs a []) p = after_in_list (y # xs) a; p \<noteq> x; x \<noteq> y; x \<notin> set xs; y \<notin> set xs; distinct xs; after_in_list (y # xs) p = Some a\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a = x \<longrightarrow> after_in_list (x # xs) p = Some x) \<and> (a \<noteq> x \<longrightarrow> after_in_list (x # xs) p = after_in_list (a # xs) a)) \<and> (y \<noteq> a \<longrightarrow> a \<noteq> x \<and> (a \<noteq> x \<longrightarrow> after_in_list (y # list_replace_list xs a []) p = after_in_list (y # xs) a)) proof (prove)
goal (1 subgoal):
 1. \<And>x y xs a. \<lbrakk>a \<noteq> x \<Longrightarrow> after_in_list (if y = a then [] @ xs else y # list_replace_list xs a []) p = after_in_list (y # xs) a; p \<noteq> x; x \<noteq> y; x \<notin> set xs; y \<notin> set xs; distinct xs; after_in_list (y # xs) p = Some a\<rbrakk> \<Longrightarrow> (y = a \<longrightarrow> (a = x \<longrightarrow> after_in_list (x # xs) p = Some x) \<and> (a \<noteq> x \<longrightarrow> after_in_list (x # xs) p = after_in_list (a # xs) a)) \<and> (y \<noteq> a \<longrightarrow> a \<noteq> x \<and> (a \<noteq> x \<longrightarrow> after_in_list (y # list_replace_list xs a []) p = after_in_list (y # xs) a)) proof (prove)
goal (1 subgoal):
 1. \<And>x y xs a aa list. \<lbrakk>a \<noteq> x \<Longrightarrow> after_in_list (if y = a then [] @ xs else y # list_replace_list xs a []) p = (if a = y then Some aa else after_in_list (aa # list) a); p \<noteq> x; x \<noteq> y; x \<noteq> aa \<and> x \<notin> set list; y \<noteq> aa \<and> y \<notin> set list; aa \<notin> set list \<and> distinct list; (if p = y then Some aa else after_in_list (aa # list) p) = Some a; xs = aa # list\<rbrakk> \<Longrightarrow> (p = y \<longrightarrow> (aa = a \<longrightarrow> (y = a \<longrightarrow> (a = x \<longrightarrow> after_in_list (x # list) x = Some x) \<and> (a \<noteq> x \<longrightarrow> after_in_list (a # list) a = Some a)) \<and> (y \<noteq> a \<longrightarrow> a \<noteq> x \<and> (a \<noteq> x \<longrightarrow> after_in_list (y # list) y = after_in_list (a # list) a))) \<and> (aa \<noteq> a \<longrightarrow> (y = a \<longrightarrow> (a = x \<longrightarrow> after_in_list (aa # list) x = Some x) \<and> (a \<noteq> x \<longrightarrow> after_in_list (aa # list) a = Some aa)) \<and> (y \<noteq> a \<longrightarrow> a \<noteq> x \<and> (a \<noteq> x \<longrightarrow> Some aa = after_in_list (aa # list) a)))) \<and> (p \<noteq> y \<longrightarrow> (aa = a \<longrightarrow> (y = a \<longrightarrow> (a = x \<longrightarrow> after_in_list (x # list) p = Some x) \<and> (a \<noteq> x \<longrightarrow> after_in_list (a # list) p = Some a)) \<and> (y \<noteq> a \<longrightarrow> a \<noteq> x \<and> (a \<noteq> x \<longrightarrow> after_in_list (y # list) p = after_in_list (a # list) a))) \<and> (aa \<noteq> a \<longrightarrow> (y = a \<longrightarrow> (a = x \<longrightarrow> after_in_list (aa # list) p = Some x) \<and> (a \<noteq> x \<longrightarrow> after_in_list (aa # list) p = Some aa)) \<and> (y \<noteq> a \<longrightarrow> a \<noteq> x \<and> (a \<noteq> x \<longrightarrow> after_in_list (aa # list_replace_list list a []) p = after_in_list (aa # list) a)))) proof (prove)
goal:
No subgoals!