theory RangeMap

lemma list_pairwise_as_indices:
  "list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j))" apply (induct xs) apply simp apply (rule iffI) apply clarsimp apply (case_tac "i = 0") apply simp apply simp apply (drule_tac x="i - 1" in spec, drule_tac x="j - 1" in spec) apply simp apply linarith apply simp apply (rule conjI) apply clarsimp apply (subst (asm) in_set_conv_nth, erule exE) apply (rename_tac j) apply (drule_tac x="0" in spec, drule_tac x="j + 1" in spec) apply simp apply clarsimp apply (drule_tac x="i + 1" in spec, drule_tac x="j + 1" in spec) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)) proof (prove)
goal (2 subgoals):
 1. list_pairwise P [] = (\<forall>i j. i < j \<and> j < length [] \<longrightarrow> P ([] ! i) ([] ! j))
 2. \<And>a xs. list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)) \<Longrightarrow> list_pairwise P (a # xs) = (\<forall>i j. i < j \<and> j < length (a # xs) \<longrightarrow> P ((a # xs) ! i) ((a # xs) ! j)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)) \<Longrightarrow> list_pairwise P (a # xs) = (\<forall>i j. i < j \<and> j < length (a # xs) \<longrightarrow> P ((a # xs) ! i) ((a # xs) ! j)) proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); list_pairwise P (a # xs)\<rbrakk> \<Longrightarrow> \<forall>i j. i < j \<and> j < length (a # xs) \<longrightarrow> P ((a # xs) ! i) ((a # xs) ! j)
 2. \<And>a xs. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < length (a # xs) \<longrightarrow> P ((a # xs) ! i) ((a # xs) ! j)\<rbrakk> \<Longrightarrow> list_pairwise P (a # xs) proof (prove)
goal (2 subgoals):
 1. \<And>a xs i j. \<lbrakk>list_pairwise P xs; \<forall>x\<in>set xs. P a x; \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j); i < j; j < Suc (length xs)\<rbrakk> \<Longrightarrow> P ((a # xs) ! i) (xs ! (j - Suc 0))
 2. \<And>a xs. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < length (a # xs) \<longrightarrow> P ((a # xs) ! i) ((a # xs) ! j)\<rbrakk> \<Longrightarrow> list_pairwise P (a # xs) proof (prove)
goal (3 subgoals):
 1. \<And>a xs i j. \<lbrakk>list_pairwise P xs; \<forall>x\<in>set xs. P a x; \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j); i < j; j < Suc (length xs); i = 0\<rbrakk> \<Longrightarrow> P ((a # xs) ! i) (xs ! (j - Suc 0))
 2. \<And>a xs i j. \<lbrakk>list_pairwise P xs; \<forall>x\<in>set xs. P a x; \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j); i < j; j < Suc (length xs); i \<noteq> 0\<rbrakk> \<Longrightarrow> P ((a # xs) ! i) (xs ! (j - Suc 0))
 3. \<And>a xs. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < length (a # xs) \<longrightarrow> P ((a # xs) ! i) ((a # xs) ! j)\<rbrakk> \<Longrightarrow> list_pairwise P (a # xs) proof (prove)
goal (2 subgoals):
 1. \<And>a xs i j. \<lbrakk>list_pairwise P xs; \<forall>x\<in>set xs. P a x; \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j); i < j; j < Suc (length xs); i \<noteq> 0\<rbrakk> \<Longrightarrow> P ((a # xs) ! i) (xs ! (j - Suc 0))
 2. \<And>a xs. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < length (a # xs) \<longrightarrow> P ((a # xs) ! i) ((a # xs) ! j)\<rbrakk> \<Longrightarrow> list_pairwise P (a # xs) proof (prove)
goal (2 subgoals):
 1. \<And>a xs i j. \<lbrakk>list_pairwise P xs; \<forall>x\<in>set xs. P a x; \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j); i < j; j < Suc (length xs); 0 < i\<rbrakk> \<Longrightarrow> P (xs ! (i - Suc 0)) (xs ! (j - Suc 0))
 2. \<And>a xs. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < length (a # xs) \<longrightarrow> P ((a # xs) ! i) ((a # xs) ! j)\<rbrakk> \<Longrightarrow> list_pairwise P (a # xs) proof (prove)
goal (2 subgoals):
 1. \<And>a xs i j. \<lbrakk>list_pairwise P xs; \<forall>x\<in>set xs. P a x; i < j; j < Suc (length xs); 0 < i; i - 1 < j - 1 \<and> j - 1 < length xs \<longrightarrow> P (xs ! (i - 1)) (xs ! (j - 1))\<rbrakk> \<Longrightarrow> P (xs ! (i - Suc 0)) (xs ! (j - Suc 0))
 2. \<And>a xs. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < length (a # xs) \<longrightarrow> P ((a # xs) ! i) ((a # xs) ! j)\<rbrakk> \<Longrightarrow> list_pairwise P (a # xs) proof (prove)
goal (2 subgoals):
 1. \<And>a xs i j. \<lbrakk>list_pairwise P xs; \<forall>x\<in>set xs. P a x; i < j; j < Suc (length xs); 0 < i; i - Suc 0 < j - Suc 0 \<and> j - Suc 0 < length xs \<longrightarrow> P (xs ! (i - Suc 0)) (xs ! (j - Suc 0))\<rbrakk> \<Longrightarrow> P (xs ! (i - Suc 0)) (xs ! (j - Suc 0))
 2. \<And>a xs. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < length (a # xs) \<longrightarrow> P ((a # xs) ! i) ((a # xs) ! j)\<rbrakk> \<Longrightarrow> list_pairwise P (a # xs) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < length (a # xs) \<longrightarrow> P ((a # xs) ! i) ((a # xs) ! j)\<rbrakk> \<Longrightarrow> list_pairwise P (a # xs) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < Suc (length xs) \<longrightarrow> P ((a # xs) ! i) (xs ! (j - Suc 0))\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set xs. P a x) \<and> (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)) proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < Suc (length xs) \<longrightarrow> P ((a # xs) ! i) (xs ! (j - Suc 0))\<rbrakk> \<Longrightarrow> \<forall>x\<in>set xs. P a x
 2. \<And>a xs. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < Suc (length xs) \<longrightarrow> P ((a # xs) ! i) (xs ! (j - Suc 0))\<rbrakk> \<Longrightarrow> \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j) proof (prove)
goal (2 subgoals):
 1. \<And>a xs x. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < Suc (length xs) \<longrightarrow> P ((a # xs) ! i) (xs ! (j - Suc 0)); x \<in> set xs\<rbrakk> \<Longrightarrow> P a x
 2. \<And>a xs. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < Suc (length xs) \<longrightarrow> P ((a # xs) ! i) (xs ! (j - Suc 0))\<rbrakk> \<Longrightarrow> \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j) proof (prove)
goal (2 subgoals):
 1. \<And>a xs x i. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < Suc (length xs) \<longrightarrow> P ((a # xs) ! i) (xs ! (j - Suc 0)); i < length xs \<and> xs ! i = x\<rbrakk> \<Longrightarrow> P a x
 2. \<And>a xs. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < Suc (length xs) \<longrightarrow> P ((a # xs) ! i) (xs ! (j - Suc 0))\<rbrakk> \<Longrightarrow> \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j) proof (prove)
goal (2 subgoals):
 1. \<And>a xs x j. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < Suc (length xs) \<longrightarrow> P ((a # xs) ! i) (xs ! (j - Suc 0)); j < length xs \<and> xs ! j = x\<rbrakk> \<Longrightarrow> P a x
 2. \<And>a xs. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < Suc (length xs) \<longrightarrow> P ((a # xs) ! i) (xs ! (j - Suc 0))\<rbrakk> \<Longrightarrow> \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j) proof (prove)
goal (2 subgoals):
 1. \<And>a xs x j. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); j < length xs \<and> xs ! j = x; 0 < j + 1 \<and> j + 1 < Suc (length xs) \<longrightarrow> P ((a # xs) ! 0) (xs ! (j + 1 - Suc 0))\<rbrakk> \<Longrightarrow> P a x
 2. \<And>a xs. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < Suc (length xs) \<longrightarrow> P ((a # xs) ! i) (xs ! (j - Suc 0))\<rbrakk> \<Longrightarrow> \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < Suc (length xs) \<longrightarrow> P ((a # xs) ! i) (xs ! (j - Suc 0))\<rbrakk> \<Longrightarrow> \<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j) proof (prove)
goal (1 subgoal):
 1. \<And>a xs i j. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); \<forall>i j. i < j \<and> j < Suc (length xs) \<longrightarrow> P ((a # xs) ! i) (xs ! (j - Suc 0)); i < j; j < length xs\<rbrakk> \<Longrightarrow> P (xs ! i) (xs ! j) proof (prove)
goal (1 subgoal):
 1. \<And>a xs i j. \<lbrakk>list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j)); i < j; j < length xs; i + 1 < j + 1 \<and> j + 1 < Suc (length xs) \<longrightarrow> P ((a # xs) ! (i + 1)) (xs ! (j + 1 - Suc 0))\<rbrakk> \<Longrightarrow> P (xs ! i) (xs ! j) proof (prove)
goal:
No subgoals!