theory ListLibLemmas

lemma list_insert_after_after:
  "\<lbrakk>distinct list; b \<notin> set list; a \<in> set list\<rbrakk>
    \<Longrightarrow> after_in_list (list_insert_after list a b) p
    = (if p = a then Some b else if p = b then after_in_list list a else after_in_list list p)" apply(induct list p rule: after_in_list.induct) apply (simp split: if_split_asm)+ apply fastforce done

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