theory ListLibLemmas

lemma indexed_trancl_as_set_helper : "\<lbrakk>p < q; q < length list; list ! p = a; list ! q = b;
        q = Suc (p + k); Suc n < length list\<rbrakk>
       \<Longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p <length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+" apply (induct k arbitrary: p q a b) apply (rule r_into_trancl,simp, rule_tac x = p in exI, simp) apply (atomize) apply (erule_tac x = p in allE, erule_tac x = "Suc (p + k)" in allE, erule_tac x = "a" in allE, erule_tac x = "list ! Suc (p + k)" in allE) apply (elim impE) apply (simp)+ apply (rule_tac b = "list ! Suc (p + k)" in trancl_into_trancl) apply (simp)+ apply (rule_tac x = "Suc (p + k)" in exI, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k); Suc n < length list\<rbrakk> \<Longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>p q a b. \<lbrakk>p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + 0); Suc n < length list\<rbrakk> \<Longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+
 2. \<And>k p q a b. \<lbrakk>\<And>p q a b. \<lbrakk>p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k); Suc n < length list\<rbrakk> \<Longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + Suc k); Suc n < length list\<rbrakk> \<Longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>k p q a b. \<lbrakk>\<And>p q a b. \<lbrakk>p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + k); Suc n < length list\<rbrakk> \<Longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + Suc k); Suc n < length list\<rbrakk> \<Longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>k p q a b. \<lbrakk>\<forall>p q a b. p < q \<longrightarrow> q < length list \<longrightarrow> list ! p = a \<longrightarrow> list ! q = b \<longrightarrow> q = Suc (p + k) \<longrightarrow> Suc n < length list \<longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+; p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + Suc k); Suc n < length list\<rbrakk> \<Longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>k p q a b. \<lbrakk>p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + Suc k); Suc n < length list; p < Suc (p + k) \<longrightarrow> Suc (p + k) < length list \<longrightarrow> list ! p = a \<longrightarrow> list ! Suc (p + k) = list ! Suc (p + k) \<longrightarrow> Suc (p + k) = Suc (p + k) \<longrightarrow> Suc n < length list \<longrightarrow> (a, list ! Suc (p + k)) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ proof (prove)
goal (7 subgoals):
 1. \<And>k p q a b. \<lbrakk>p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + Suc k); Suc n < length list\<rbrakk> \<Longrightarrow> p < Suc (p + k)
 2. \<And>k p q a b. \<lbrakk>p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + Suc k); Suc n < length list\<rbrakk> \<Longrightarrow> Suc (p + k) < length list
 3. \<And>k p q a b. \<lbrakk>p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + Suc k); Suc n < length list\<rbrakk> \<Longrightarrow> list ! p = a
 4. \<And>k p q a b. \<lbrakk>p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + Suc k); Suc n < length list\<rbrakk> \<Longrightarrow> list ! Suc (p + k) = list ! Suc (p + k)
 5. \<And>k p q a b. \<lbrakk>p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + Suc k); Suc n < length list\<rbrakk> \<Longrightarrow> Suc (p + k) = Suc (p + k)
 6. \<And>k p q a b. \<lbrakk>p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + Suc k); Suc n < length list\<rbrakk> \<Longrightarrow> Suc n < length list
 7. \<And>k p q a b. \<lbrakk>p < q; q < length list; list ! p = a; list ! q = b; q = Suc (p + Suc k); Suc n < length list; (a, list ! Suc (p + k)) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>k p q a b. \<lbrakk>Suc (Suc (p + k)) < length list; list ! p = a; list ! Suc (Suc (p + k)) = b; q = Suc (Suc (p + k)); Suc n < length list; (a, list ! Suc (p + k)) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+\<rbrakk> \<Longrightarrow> (a, b) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>k p q a b. \<lbrakk>Suc (Suc (p + k)) < length list; list ! p = a; list ! Suc (Suc (p + k)) = b; q = Suc (Suc (p + k)); Suc n < length list; (a, list ! Suc (p + k)) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+\<rbrakk> \<Longrightarrow> (a, list ! Suc (p + k)) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+
 2. \<And>k p q a b. \<lbrakk>Suc (Suc (p + k)) < length list; list ! p = a; list ! Suc (Suc (p + k)) = b; q = Suc (Suc (p + k)); Suc n < length list; (a, list ! Suc (p + k)) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+\<rbrakk> \<Longrightarrow> (list ! Suc (p + k), b) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j} proof (prove)
goal (1 subgoal):
 1. \<And>k p q a b. \<lbrakk>Suc (Suc (p + k)) < length list; list ! p = a; list ! Suc (Suc (p + k)) = b; q = Suc (Suc (p + k)); Suc n < length list; (a, list ! Suc (p + k)) \<in> {(i, j). \<exists>p. Suc p < length list \<and> list ! p = i \<and> list ! Suc p = j}\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>pa. Suc pa < length list \<and> list ! pa = list ! Suc (p + k) \<and> list ! Suc pa = b proof (prove)
goal:
No subgoals!