theory ListLibLemmas

lemma after_distinct_one_sibling: "distinct list \<Longrightarrow> list = xs @ x # y # ys \<Longrightarrow> after_in_list list x = Some y" apply (induct xs) apply simp apply simp apply clarsimp apply (subgoal_tac "after_in_list ((a # xs) @ (x # y # ys)) x = after_in_list (x # y # ys) x") apply simp apply (rule after_ignore_head) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct list; list = xs @ x # y # ys\<rbrakk> \<Longrightarrow> after_in_list list x = Some y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct list; list = [] @ x # y # ys\<rbrakk> \<Longrightarrow> after_in_list list x = Some y
 2. \<And>a xs. \<lbrakk>\<lbrakk>distinct list; list = xs @ x # y # ys\<rbrakk> \<Longrightarrow> after_in_list list x = Some y; distinct list; list = (a # xs) @ x # y # ys\<rbrakk> \<Longrightarrow> after_in_list list x = Some y proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>distinct list; list = xs @ x # y # ys\<rbrakk> \<Longrightarrow> after_in_list list x = Some y; distinct list; list = (a # xs) @ x # y # ys\<rbrakk> \<Longrightarrow> after_in_list list x = Some y proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>a \<noteq> x \<and> a \<noteq> y \<and> a \<notin> set xs \<and> a \<notin> set ys \<and> distinct xs \<and> x \<noteq> y \<and> x \<notin> set ys \<and> y \<notin> set ys \<and> distinct ys \<and> x \<notin> set xs \<and> y \<notin> set xs \<and> set xs \<inter> set ys = {}; list = a # xs @ x # y # ys\<rbrakk> \<Longrightarrow> after_in_list (a # xs @ x # y # ys) x = Some y proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>list = a # xs @ x # y # ys; a \<noteq> x; a \<noteq> y; a \<notin> set xs; a \<notin> set ys; distinct xs; x \<noteq> y; x \<notin> set ys; y \<notin> set ys; distinct ys; x \<notin> set xs; y \<notin> set xs; set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> after_in_list (a # xs @ x # y # ys) x = Some y proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>list = a # xs @ x # y # ys; a \<noteq> x; a \<noteq> y; a \<notin> set xs; a \<notin> set ys; distinct xs; x \<noteq> y; x \<notin> set ys; y \<notin> set ys; distinct ys; x \<notin> set xs; y \<notin> set xs; set xs \<inter> set ys = {}; after_in_list ((a # xs) @ x # y # ys) x = after_in_list (x # y # ys) x\<rbrakk> \<Longrightarrow> after_in_list (a # xs @ x # y # ys) x = Some y
 2. \<And>a xs. \<lbrakk>list = a # xs @ x # y # ys; a \<noteq> x; a \<noteq> y; a \<notin> set xs; a \<notin> set ys; distinct xs; x \<noteq> y; x \<notin> set ys; y \<notin> set ys; distinct ys; x \<notin> set xs; y \<notin> set xs; set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> after_in_list ((a # xs) @ x # y # ys) x = after_in_list (x # y # ys) x proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>list = a # xs @ x # y # ys; a \<noteq> x; a \<noteq> y; a \<notin> set xs; a \<notin> set ys; distinct xs; x \<noteq> y; x \<notin> set ys; y \<notin> set ys; distinct ys; x \<notin> set xs; y \<notin> set xs; set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> after_in_list ((a # xs) @ x # y # ys) x = after_in_list (x # y # ys) x proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>list = a # xs @ x # y # ys; a \<noteq> x; a \<noteq> y; a \<notin> set xs; a \<notin> set ys; distinct xs; x \<noteq> y; x \<notin> set ys; y \<notin> set ys; distinct ys; x \<notin> set xs; y \<notin> set xs; set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> x \<notin> set (a # xs) proof (prove)
goal:
No subgoals!