theory ListLibLemmas

lemma after_in_list_inj:
  "\<lbrakk>distinct list; after_in_list list a = Some x; after_in_list list b = Some x\<rbrakk>
    \<Longrightarrow> a = b" apply(induct list) apply(simp) apply(simp) apply(case_tac "a=aa") apply(case_tac list, simp) apply(simp add: hd_not_after_in_list split: if_split_asm) apply(case_tac list, simp) apply(simp add: hd_not_after_in_list split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct list; after_in_list list a = Some x; after_in_list list b = Some x\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct []; after_in_list [] a = Some x; after_in_list [] b = Some x\<rbrakk> \<Longrightarrow> a = b
 2. \<And>aa list. \<lbrakk>\<lbrakk>distinct list; after_in_list list a = Some x; after_in_list list b = Some x\<rbrakk> \<Longrightarrow> a = b; distinct (aa # list); after_in_list (aa # list) a = Some x; after_in_list (aa # list) b = Some x\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>\<lbrakk>distinct list; after_in_list list a = Some x; after_in_list list b = Some x\<rbrakk> \<Longrightarrow> a = b; distinct (aa # list); after_in_list (aa # list) a = Some x; after_in_list (aa # list) b = Some x\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>\<lbrakk>after_in_list list a = Some x; after_in_list list b = Some x\<rbrakk> \<Longrightarrow> a = b; aa \<notin> set list \<and> distinct list; after_in_list (aa # list) a = Some x; after_in_list (aa # list) b = Some x\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (2 subgoals):
 1. \<And>aa list. \<lbrakk>\<lbrakk>after_in_list list a = Some x; after_in_list list b = Some x\<rbrakk> \<Longrightarrow> a = b; aa \<notin> set list \<and> distinct list; after_in_list (aa # list) a = Some x; after_in_list (aa # list) b = Some x; a = aa\<rbrakk> \<Longrightarrow> a = b
 2. \<And>aa list. \<lbrakk>\<lbrakk>after_in_list list a = Some x; after_in_list list b = Some x\<rbrakk> \<Longrightarrow> a = b; aa \<notin> set list \<and> distinct list; after_in_list (aa # list) a = Some x; after_in_list (aa # list) b = Some x; a \<noteq> aa\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (2 subgoals):
 1. \<And>aa list aaa lista. \<lbrakk>\<lbrakk>after_in_list list a = Some x; after_in_list list b = Some x\<rbrakk> \<Longrightarrow> a = b; aa \<notin> set list \<and> distinct list; after_in_list (aa # list) a = Some x; after_in_list (aa # list) b = Some x; a = aa; list = aaa # lista\<rbrakk> \<Longrightarrow> a = b
 2. \<And>aa list. \<lbrakk>\<lbrakk>after_in_list list a = Some x; after_in_list list b = Some x\<rbrakk> \<Longrightarrow> a = b; aa \<notin> set list \<and> distinct list; after_in_list (aa # list) a = Some x; after_in_list (aa # list) b = Some x; a \<noteq> aa\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>\<lbrakk>after_in_list list a = Some x; after_in_list list b = Some x\<rbrakk> \<Longrightarrow> a = b; aa \<notin> set list \<and> distinct list; after_in_list (aa # list) a = Some x; after_in_list (aa # list) b = Some x; a \<noteq> aa\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (1 subgoal):
 1. \<And>aa list aaa lista. \<lbrakk>\<lbrakk>after_in_list list a = Some x; after_in_list list b = Some x\<rbrakk> \<Longrightarrow> a = b; aa \<notin> set list \<and> distinct list; after_in_list (aa # list) a = Some x; after_in_list (aa # list) b = Some x; a \<noteq> aa; list = aaa # lista\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal:
No subgoals!