theory ListLibLemmas

lemma after_in_list_trancl_indexed_trancl: "distinct list \<Longrightarrow> {(p, q). after_in_list list p = Some q}\<^sup>+ = {(i, j). \<exists> p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j }\<^sup>+" apply (rule_tac f = "\<lambda> x. x\<^sup>+" in  arg_cong) apply (intro equalityI subsetI) apply (case_tac x, simp) apply (induct list) apply (simp) apply (case_tac "a = aa") apply (rule_tac x = 0 in exI, case_tac list, simp, simp) apply (case_tac list, simp, simp) apply (atomize, drule_tac x = x in spec, drule_tac x = aa in spec, drule_tac x = b in spec, simp) apply (erule exE, rule_tac x = "Suc p" in exI, simp) apply (case_tac x, simp) apply (induct list) apply (simp) apply (case_tac "a = aa") apply (erule exE) apply (subgoal_tac "p = 0") apply (case_tac list, simp, simp) apply (subgoal_tac "distinct (aa # list)") apply (frule_tac i = 0 and j = p and xs = "aa # list" in nth_eq_iff_index_eq) apply (simp, simp, simp, simp) apply (atomize, drule_tac x = x in spec, drule_tac x = aa in spec, drule_tac x = b in spec, simp) apply (drule mp) apply (erule exE) apply (case_tac p, simp, simp) apply (rule_tac x = nat in exI, simp) apply (case_tac list, simp, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct list \<Longrightarrow> {(p, q). after_in_list list p = Some q}\<^sup>+ = {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. distinct list \<Longrightarrow> {(p, q). after_in_list list p = Some q} = {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>distinct list; x \<in> {(p, q). after_in_list list p = Some q}\<rbrakk> \<Longrightarrow> x \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}
 2. \<And>x. \<lbrakk>distinct list; x \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<rbrakk> \<Longrightarrow> x \<in> {(p, q). after_in_list list p = Some q} proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>distinct list; after_in_list list a = Some b; x = (a, b)\<rbrakk> \<Longrightarrow> \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b
 2. \<And>x. \<lbrakk>distinct list; x \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<rbrakk> \<Longrightarrow> x \<in> {(p, q). after_in_list list p = Some q} proof (prove)
goal (3 subgoals):
 1. \<And>x a b. \<lbrakk>distinct []; after_in_list [] a = Some b; x = (a, b)\<rbrakk> \<Longrightarrow> \<exists>p. Suc p < length [] \<and> [] ! p = a \<and> [] ! Suc p = b
 2. \<And>a list x aa b. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; after_in_list list a = Some b; x = (a, b)\<rbrakk> \<Longrightarrow> \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; distinct (a # list); after_in_list (a # list) aa = Some b; x = (aa, b)\<rbrakk> \<Longrightarrow> \<exists>p. Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b
 3. \<And>x. \<lbrakk>distinct list; x \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<rbrakk> \<Longrightarrow> x \<in> {(p, q). after_in_list list p = Some q} proof (prove)
goal (2 subgoals):
 1. \<And>a list x aa b. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; after_in_list list a = Some b; x = (a, b)\<rbrakk> \<Longrightarrow> \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; distinct (a # list); after_in_list (a # list) aa = Some b; x = (aa, b)\<rbrakk> \<Longrightarrow> \<exists>p. Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b
 2. \<And>x. \<lbrakk>distinct list; x \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<rbrakk> \<Longrightarrow> x \<in> {(p, q). after_in_list list p = Some q} proof (prove)
goal (3 subgoals):
 1. \<And>a list x aa b. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; after_in_list list a = Some b; x = (a, b)\<rbrakk> \<Longrightarrow> \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; distinct (a # list); after_in_list (a # list) aa = Some b; x = (aa, b); a = aa\<rbrakk> \<Longrightarrow> \<exists>p. Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b
 2. \<And>a list x aa b. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; after_in_list list a = Some b; x = (a, b)\<rbrakk> \<Longrightarrow> \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; distinct (a # list); after_in_list (a # list) aa = Some b; x = (aa, b); a \<noteq> aa\<rbrakk> \<Longrightarrow> \<exists>p. Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b
 3. \<And>x. \<lbrakk>distinct list; x \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<rbrakk> \<Longrightarrow> x \<in> {(p, q). after_in_list list p = Some q} proof (prove)
goal (2 subgoals):
 1. \<And>a list x aa b. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; after_in_list list a = Some b; x = (a, b)\<rbrakk> \<Longrightarrow> \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; distinct (a # list); after_in_list (a # list) aa = Some b; x = (aa, b); a \<noteq> aa\<rbrakk> \<Longrightarrow> \<exists>p. Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b
 2. \<And>x. \<lbrakk>distinct list; x \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<rbrakk> \<Longrightarrow> x \<in> {(p, q). after_in_list list p = Some q} proof (prove)
goal (2 subgoals):
 1. \<And>a list x aa b ab lista. \<lbrakk>\<And>x a b. \<lbrakk>after_in_list (ab # lista) a = Some b; x = (a, b)\<rbrakk> \<Longrightarrow> \<exists>p<length lista. (ab # lista) ! p = a \<and> lista ! p = b; a \<noteq> ab \<and> a \<notin> set lista \<and> ab \<notin> set lista \<and> distinct lista; after_in_list (ab # lista) aa = Some b; x = (aa, b); a \<noteq> aa; list = ab # lista\<rbrakk> \<Longrightarrow> \<exists>p<Suc (length lista). (a # ab # lista) ! p = aa \<and> (ab # lista) ! p = b
 2. \<And>x. \<lbrakk>distinct list; x \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<rbrakk> \<Longrightarrow> x \<in> {(p, q). after_in_list list p = Some q} proof (prove)
goal (2 subgoals):
 1. \<And>a list x aa b ab lista. \<lbrakk>a \<noteq> ab \<and> a \<notin> set lista \<and> ab \<notin> set lista \<and> distinct lista; after_in_list (ab # lista) aa = Some b; x = (aa, b); a \<noteq> aa; list = ab # lista; \<exists>p<length lista. (ab # lista) ! p = aa \<and> lista ! p = b\<rbrakk> \<Longrightarrow> \<exists>p<Suc (length lista). (a # ab # lista) ! p = aa \<and> (ab # lista) ! p = b
 2. \<And>x. \<lbrakk>distinct list; x \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<rbrakk> \<Longrightarrow> x \<in> {(p, q). after_in_list list p = Some q} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>distinct list; x \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<rbrakk> \<Longrightarrow> x \<in> {(p, q). after_in_list list p = Some q} proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>distinct []; \<exists>p. Suc p < length [] \<and> [] ! p = a \<and> [] ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list [] a = Some b
 2. \<And>a list x aa b. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); \<exists>p. Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b; x = (aa, b)\<rbrakk> \<Longrightarrow> after_in_list (a # list) aa = Some b proof (prove)
goal (1 subgoal):
 1. \<And>a list x aa b. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); \<exists>p. Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b; x = (aa, b)\<rbrakk> \<Longrightarrow> after_in_list (a # list) aa = Some b proof (prove)
goal (2 subgoals):
 1. \<And>a list x aa b. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); \<exists>p. Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b; x = (aa, b); a = aa\<rbrakk> \<Longrightarrow> after_in_list (a # list) aa = Some b
 2. \<And>a list x aa b. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); \<exists>p. Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b; x = (aa, b); a \<noteq> aa\<rbrakk> \<Longrightarrow> after_in_list (a # list) aa = Some b proof (prove)
goal (2 subgoals):
 1. \<And>a list x aa b p. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); x = (aa, b); a = aa; Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b\<rbrakk> \<Longrightarrow> after_in_list (a # list) aa = Some b
 2. \<And>a list x aa b. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); \<exists>p. Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b; x = (aa, b); a \<noteq> aa\<rbrakk> \<Longrightarrow> after_in_list (a # list) aa = Some b proof (prove)
goal (3 subgoals):
 1. \<And>a list x aa b p. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); x = (aa, b); a = aa; Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b; p = 0\<rbrakk> \<Longrightarrow> after_in_list (a # list) aa = Some b
 2. \<And>a list x aa b p. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); x = (aa, b); a = aa; Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b\<rbrakk> \<Longrightarrow> p = 0
 3. \<And>a list x aa b. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); \<exists>p. Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b; x = (aa, b); a \<noteq> aa\<rbrakk> \<Longrightarrow> after_in_list (a # list) aa = Some b proof (prove)
goal (2 subgoals):
 1. \<And>a list x aa b p. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); x = (aa, b); a = aa; Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b\<rbrakk> \<Longrightarrow> p = 0
 2. \<And>a list x aa b. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); \<exists>p. Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b; x = (aa, b); a \<noteq> aa\<rbrakk> \<Longrightarrow> after_in_list (a # list) aa = Some b proof (prove)
goal (3 subgoals):
 1. \<And>a list x aa b p. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); x = (aa, b); a = aa; Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b; distinct (aa # list)\<rbrakk> \<Longrightarrow> p = 0
 2. \<And>a list x aa b p. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); x = (aa, b); a = aa; Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b\<rbrakk> \<Longrightarrow> distinct (aa # list)
 3. \<And>a list x aa b. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); \<exists>p. Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b; x = (aa, b); a \<noteq> aa\<rbrakk> \<Longrightarrow> after_in_list (a # list) aa = Some b proof (prove)
goal (5 subgoals):
 1. \<And>a list x aa b p. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); x = (aa, b); a = aa; Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b; distinct (aa # list)\<rbrakk> \<Longrightarrow> 0 < length (aa # list)
 2. \<And>a list x aa b p. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); x = (aa, b); a = aa; Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b; distinct (aa # list)\<rbrakk> \<Longrightarrow> p < length (aa # list)
 3. \<And>a list x aa b p. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); x = (aa, b); a = aa; Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b; distinct (aa # list); ((aa # list) ! 0 = (aa # list) ! p) = (0 = p)\<rbrakk> \<Longrightarrow> p = 0
 4. \<And>a list x aa b p. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); x = (aa, b); a = aa; Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b\<rbrakk> \<Longrightarrow> distinct (aa # list)
 5. \<And>a list x aa b. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); \<exists>p. Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b; x = (aa, b); a \<noteq> aa\<rbrakk> \<Longrightarrow> after_in_list (a # list) aa = Some b proof (prove)
goal (1 subgoal):
 1. \<And>a list x aa b. \<lbrakk>\<And>x a b. \<lbrakk>distinct list; \<exists>p. Suc p < length list \<and> list ! p = a \<and> list ! Suc p = b; x = (a, b)\<rbrakk> \<Longrightarrow> after_in_list list a = Some b; distinct (a # list); \<exists>p. Suc p < length (a # list) \<and> (a # list) ! p = aa \<and> (a # list) ! Suc p = b; x = (aa, b); a \<noteq> aa\<rbrakk> \<Longrightarrow> after_in_list (a # list) aa = Some b proof (prove)
goal (1 subgoal):
 1. \<And>a list x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; \<exists>p<length list. (a # list) ! p = aa \<and> list ! p = b; x = (aa, b); a \<noteq> aa; (\<exists>p. Suc p < length list \<and> list ! p = aa \<and> list ! Suc p = b) \<longrightarrow> after_in_list list aa = Some b\<rbrakk> \<Longrightarrow> after_in_list (a # list) aa = Some b proof (prove)
goal (2 subgoals):
 1. \<And>a list x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; \<exists>p<length list. (a # list) ! p = aa \<and> list ! p = b; x = (aa, b); a \<noteq> aa\<rbrakk> \<Longrightarrow> \<exists>p. Suc p < length list \<and> list ! p = aa \<and> list ! Suc p = b
 2. \<And>a list x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; \<exists>p<length list. (a # list) ! p = aa \<and> list ! p = b; x = (aa, b); a \<noteq> aa; after_in_list list aa = Some b\<rbrakk> \<Longrightarrow> after_in_list (a # list) aa = Some b proof (prove)
goal (2 subgoals):
 1. \<And>a list x aa b p. \<lbrakk>a \<notin> set list \<and> distinct list; x = (aa, b); a \<noteq> aa; p < length list \<and> (a # list) ! p = aa \<and> list ! p = b\<rbrakk> \<Longrightarrow> \<exists>p. Suc p < length list \<and> list ! p = aa \<and> list ! Suc p = b
 2. \<And>a list x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; \<exists>p<length list. (a # list) ! p = aa \<and> list ! p = b; x = (aa, b); a \<noteq> aa; after_in_list list aa = Some b\<rbrakk> \<Longrightarrow> after_in_list (a # list) aa = Some b proof (prove)
goal (2 subgoals):
 1. \<And>a list x p nat. \<lbrakk>a \<notin> set list \<and> distinct list; x = (list ! nat, list ! Suc nat); a \<noteq> list ! nat; Suc nat < length list; p = Suc nat\<rbrakk> \<Longrightarrow> \<exists>p. Suc p < length list \<and> list ! p = list ! nat \<and> list ! Suc p = list ! Suc nat
 2. \<And>a list x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; \<exists>p<length list. (a # list) ! p = aa \<and> list ! p = b; x = (aa, b); a \<noteq> aa; after_in_list list aa = Some b\<rbrakk> \<Longrightarrow> after_in_list (a # list) aa = Some b proof (prove)
goal (1 subgoal):
 1. \<And>a list x aa b. \<lbrakk>a \<notin> set list \<and> distinct list; \<exists>p<length list. (a # list) ! p = aa \<and> list ! p = b; x = (aa, b); a \<noteq> aa; after_in_list list aa = Some b\<rbrakk> \<Longrightarrow> after_in_list (a # list) aa = Some b proof (prove)
goal:
No subgoals!