[STATEMENT]
lemma filter_merge_wrt_2:
  assumes "\<And>x. x \<in> set xs \<Longrightarrow> P x \<Longrightarrow> False"
  shows "filter P (merge_wrt rel xs ys) = filter P ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter P (merge_wrt rel xs ys) = filter P ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> set xs; P ?x\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. filter P (merge_wrt rel xs ys) = filter P ys
[PROOF STEP]
proof (induct rel xs ys rule: merge_wrt.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>uu_ xs. (\<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> filter P (merge_wrt uu_ xs []) = filter P []
 2. \<And>rel v va. (\<And>x. \<lbrakk>x \<in> set []; P x\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> filter P (merge_wrt rel [] (v # va)) = filter P (v # va)
 3. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P ys; \<lbrakk>x \<noteq> y; rel x y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys); \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P ys; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (y # ys)
[PROOF STEP]
case (1 rel xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> set xs; P ?x\<rbrakk> \<Longrightarrow> False

goal (3 subgoals):
 1. \<And>uu_ xs. (\<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> filter P (merge_wrt uu_ xs []) = filter P []
 2. \<And>rel v va. (\<And>x. \<lbrakk>x \<in> set []; P x\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> filter P (merge_wrt rel [] (v # va)) = filter P (v # va)
 3. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P ys; \<lbrakk>x \<noteq> y; rel x y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys); \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P ys; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (y # ys)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> set xs; P ?x\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. filter P (merge_wrt rel xs []) = filter P []
[PROOF STEP]
by (auto simp: filter_empty_conv)
[PROOF STATE]
proof (state)
this:
filter P (merge_wrt rel xs []) = filter P []

goal (2 subgoals):
 1. \<And>rel v va. (\<And>x. \<lbrakk>x \<in> set []; P x\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> filter P (merge_wrt rel [] (v # va)) = filter P (v # va)
 2. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P ys; \<lbrakk>x \<noteq> y; rel x y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys); \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P ys; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (y # ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>rel v va. (\<And>x. \<lbrakk>x \<in> set []; P x\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> filter P (merge_wrt rel [] (v # va)) = filter P (v # va)
 2. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P ys; \<lbrakk>x \<noteq> y; rel x y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys); \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P ys; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (y # ys)
[PROOF STEP]
case (2 rel y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> set []; P ?x\<rbrakk> \<Longrightarrow> False

goal (2 subgoals):
 1. \<And>rel v va. (\<And>x. \<lbrakk>x \<in> set []; P x\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> filter P (merge_wrt rel [] (v # va)) = filter P (v # va)
 2. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P ys; \<lbrakk>x \<noteq> y; rel x y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys); \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P ys; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (y # ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter P (merge_wrt rel [] (y # ys)) = filter P (y # ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
filter P (merge_wrt rel [] (y # ys)) = filter P (y # ys)

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P ys; \<lbrakk>x \<noteq> y; rel x y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys); \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P ys; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (y # ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P ys; \<lbrakk>x \<noteq> y; rel x y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys); \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P ys; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (y # ys)
[PROOF STEP]
case (3 rel x xs y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P ys
\<lbrakk>x \<noteq> y; rel x y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys)
\<lbrakk>x \<noteq> y; \<not> rel x y; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P ys
\<lbrakk>?x \<in> set (x # xs); P ?x\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P ys; \<lbrakk>x \<noteq> y; rel x y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys); \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P ys; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (y # ys)
[PROOF STEP]
hence "\<not> P x" and x: "\<And>z. z \<in> set xs \<Longrightarrow> P z \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P ys
\<lbrakk>x \<noteq> y; rel x y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys)
\<lbrakk>x \<noteq> y; \<not> rel x y; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P ys
\<lbrakk>?x \<in> set (x # xs); P ?x\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> P x &&& (\<And>z. \<lbrakk>z \<in> set xs; P z\<rbrakk> \<Longrightarrow> False)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> P x
\<lbrakk>?z \<in> set xs; P ?z\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P ys; \<lbrakk>x \<noteq> y; rel x y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys); \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P ys; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (y # ys)
[PROOF STEP]
have a: "filter P (merge_wrt rel xs ys) = filter P ys" if "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter P (merge_wrt rel xs ys) = filter P ys
[PROOF STEP]
using that x
[PROOF STATE]
proof (prove)
using this:
x = y
\<lbrakk>?z \<in> set xs; P ?z\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. filter P (merge_wrt rel xs ys) = filter P ys
[PROOF STEP]
by (rule 3(1))
[PROOF STATE]
proof (state)
this:
x = y \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P ys

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P ys; \<lbrakk>x \<noteq> y; rel x y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys); \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P ys; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (y # ys)
[PROOF STEP]
have b: "filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys)" if "x \<noteq> y" and "rel x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys)
[PROOF STEP]
using that x
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
rel x y
\<lbrakk>?z \<in> set xs; P ?z\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys)
[PROOF STEP]
by (rule 3(2))
[PROOF STATE]
proof (state)
this:
\<lbrakk>x \<noteq> y; rel x y\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys)

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P ys; \<lbrakk>x \<noteq> y; rel x y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys); \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P ys; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (y # ys)
[PROOF STEP]
have c: "filter P (merge_wrt rel (x # xs) ys) = filter P ys" if "x \<noteq> y" and "\<not> rel x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter P (merge_wrt rel (x # xs) ys) = filter P ys
[PROOF STEP]
using that 3(4)
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
\<not> rel x y
\<lbrakk>?x \<in> set (x # xs); P ?x\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. filter P (merge_wrt rel (x # xs) ys) = filter P ys
[PROOF STEP]
by (rule 3(3))
[PROOF STATE]
proof (state)
this:
\<lbrakk>x \<noteq> y; \<not> rel x y\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P ys

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs ys) = filter P ys; \<lbrakk>x \<noteq> y; rel x y; \<And>x. \<lbrakk>x \<in> set xs; P x\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel xs (y # ys)) = filter P (y # ys); \<lbrakk>x \<noteq> y; \<not> rel x y; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) ys) = filter P ys; \<And>xa. \<lbrakk>xa \<in> set (x # xs); P xa\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (y # ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (y # ys)
[PROOF STEP]
by (simp add: a b c \<open>\<not> P x\<close>)
[PROOF STATE]
proof (state)
this:
filter P (merge_wrt rel (x # xs) (y # ys)) = filter P (y # ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_filter_le_1:
  assumes "length (filter P xs) \<le> 1" and "i < length xs" and "j < length xs"
    and "P (xs ! i)" and "P (xs ! j)"
  shows "i = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i = j
[PROOF STEP]
have *: thesis if "a < b" and "b < length xs"
    and "\<And>as bs cs. as @ ((xs ! a) # (bs @ ((xs ! b) # cs))) = xs \<Longrightarrow> thesis" for a b thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (rule that(3))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ?as @ xs ! a # ?bs @ xs ! b # ?cs = xs
[PROOF STEP]
from that(1, 2)
[PROOF STATE]
proof (chain)
picking this:
a < b
b < length xs
[PROOF STEP]
have 1: "a < length xs"
[PROOF STATE]
proof (prove)
using this:
a < b
b < length xs

goal (1 subgoal):
 1. a < length xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a < length xs

goal (1 subgoal):
 1. ?as @ xs ! a # ?bs @ xs ! b # ?cs = xs
[PROOF STEP]
with that(1, 2)
[PROOF STATE]
proof (chain)
picking this:
a < b
b < length xs
a < length xs
[PROOF STEP]
have 2: "b - Suc a < length (drop (Suc a) xs)"
[PROOF STATE]
proof (prove)
using this:
a < b
b < length xs
a < length xs

goal (1 subgoal):
 1. b - Suc a < length (drop (Suc a) xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b - Suc a < length (drop (Suc a) xs)

goal (1 subgoal):
 1. ?as @ xs ! a # ?bs @ xs ! b # ?cs = xs
[PROOF STEP]
from that(1) \<open>a < length xs\<close>
[PROOF STATE]
proof (chain)
picking this:
a < b
a < length xs
[PROOF STEP]
have eq: "xs ! b = drop (Suc a) xs ! (b - Suc a)"
[PROOF STATE]
proof (prove)
using this:
a < b
a < length xs

goal (1 subgoal):
 1. xs ! b = drop (Suc a) xs ! (b - Suc a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs ! b = drop (Suc a) xs ! (b - Suc a)

goal (1 subgoal):
 1. ?as @ xs ! a # ?bs @ xs ! b # ?cs = xs
[PROOF STEP]
show "(take a xs) @ ((xs ! a) # ((take (b - Suc a) (drop (Suc a) xs)) @ ((xs ! b) #
                  drop (Suc (b - Suc a)) (drop (Suc a) xs)))) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take a xs @ xs ! a # take (b - Suc a) (drop (Suc a) xs) @ xs ! b # drop (Suc (b - Suc a)) (drop (Suc a) xs) = xs
[PROOF STEP]
by (simp only: eq id_take_nth_drop[OF 1, symmetric] id_take_nth_drop[OF 2, symmetric])
[PROOF STATE]
proof (state)
this:
take a xs @ xs ! a # take (b - Suc a) (drop (Suc a) xs) @ xs ! b # drop (Suc (b - Suc a)) (drop (Suc a) xs) = xs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a < ?b; ?b < length xs; \<And>as bs cs. as @ xs ! ?a # bs @ xs ! ?b # cs = xs \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. i = j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = j
[PROOF STEP]
proof (rule linorder_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?x < ?y \<Longrightarrow> i = j
 2. ?x = ?y \<Longrightarrow> i = j
 3. ?y < ?x \<Longrightarrow> i = j
[PROOF STEP]
assume "i < j"
[PROOF STATE]
proof (state)
this:
i < j

goal (3 subgoals):
 1. ?x < ?y \<Longrightarrow> i = j
 2. ?x = ?y \<Longrightarrow> i = j
 3. ?y < ?x \<Longrightarrow> i = j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < j
[PROOF STEP]
obtain as bs cs where "as @ ((xs ! i) # (bs @ ((xs ! j) # cs))) = xs"
[PROOF STATE]
proof (prove)
using this:
i < j

goal (1 subgoal):
 1. (\<And>as bs cs. as @ xs ! i # bs @ xs ! j # cs = xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
i < j
j < length xs

goal (1 subgoal):
 1. (\<And>as bs cs. as @ xs ! i # bs @ xs ! j # cs = xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule *)
[PROOF STATE]
proof (state)
this:
as @ xs ! i # bs @ xs ! j # cs = xs

goal (3 subgoals):
 1. ?x < ?y \<Longrightarrow> i = j
 2. ?x = ?y \<Longrightarrow> i = j
 3. ?y < ?x \<Longrightarrow> i = j
[PROOF STEP]
hence "filter P xs = filter P (as @ ((xs ! i) # (bs @ ((xs ! j) # cs))))"
[PROOF STATE]
proof (prove)
using this:
as @ xs ! i # bs @ xs ! j # cs = xs

goal (1 subgoal):
 1. filter P xs = filter P (as @ xs ! i # bs @ xs ! j # cs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
filter P xs = filter P (as @ xs ! i # bs @ xs ! j # cs)

goal (3 subgoals):
 1. ?x < ?y \<Longrightarrow> i = j
 2. ?x = ?y \<Longrightarrow> i = j
 3. ?y < ?x \<Longrightarrow> i = j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
filter P xs = filter P (as @ xs ! i # bs @ xs ! j # cs)

goal (3 subgoals):
 1. ?x < ?y \<Longrightarrow> i = j
 2. ?x = ?y \<Longrightarrow> i = j
 3. ?y < ?x \<Longrightarrow> i = j
[PROOF STEP]
from assms(4, 5)
[PROOF STATE]
proof (chain)
picking this:
P (xs ! i)
P (xs ! j)
[PROOF STEP]
have "... = (filter P as) @ ((xs ! i) # ((filter P bs) @ ((xs ! j) # (filter P cs))))"
[PROOF STATE]
proof (prove)
using this:
P (xs ! i)
P (xs ! j)

goal (1 subgoal):
 1. filter P (as @ xs ! i # bs @ xs ! j # cs) = filter P as @ xs ! i # filter P bs @ xs ! j # filter P cs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
filter P (as @ xs ! i # bs @ xs ! j # cs) = filter P as @ xs ! i # filter P bs @ xs ! j # filter P cs

goal (3 subgoals):
 1. ?x < ?y \<Longrightarrow> i = j
 2. ?x = ?y \<Longrightarrow> i = j
 3. ?y < ?x \<Longrightarrow> i = j
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
filter P xs = filter P as @ xs ! i # filter P bs @ xs ! j # filter P cs
[PROOF STEP]
have "\<not> length (filter P xs) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
filter P xs = filter P as @ xs ! i # filter P bs @ xs ! j # filter P cs

goal (1 subgoal):
 1. \<not> length (filter P xs) \<le> 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> length (filter P xs) \<le> 1

goal (3 subgoals):
 1. ?x < ?y \<Longrightarrow> i = j
 2. ?x = ?y \<Longrightarrow> i = j
 3. ?y < ?x \<Longrightarrow> i = j
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> length (filter P xs) \<le> 1

goal (1 subgoal):
 1. i = j
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<not> length (filter P xs) \<le> 1
length (filter P xs) \<le> 1

goal (1 subgoal):
 1. i = j
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
i = j

goal (2 subgoals):
 1. i = j \<Longrightarrow> i = j
 2. j < i \<Longrightarrow> i = j
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = j \<Longrightarrow> i = j
 2. j < i \<Longrightarrow> i = j
[PROOF STEP]
assume "j < i"
[PROOF STATE]
proof (state)
this:
j < i

goal (2 subgoals):
 1. i = j \<Longrightarrow> i = j
 2. j < i \<Longrightarrow> i = j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j < i
[PROOF STEP]
obtain as bs cs where "as @ ((xs ! j) # (bs @ ((xs ! i) # cs))) = xs"
[PROOF STATE]
proof (prove)
using this:
j < i

goal (1 subgoal):
 1. (\<And>as bs cs. as @ xs ! j # bs @ xs ! i # cs = xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
j < i
i < length xs

goal (1 subgoal):
 1. (\<And>as bs cs. as @ xs ! j # bs @ xs ! i # cs = xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule *)
[PROOF STATE]
proof (state)
this:
as @ xs ! j # bs @ xs ! i # cs = xs

goal (2 subgoals):
 1. i = j \<Longrightarrow> i = j
 2. j < i \<Longrightarrow> i = j
[PROOF STEP]
hence "filter P xs = filter P (as @ ((xs ! j) # (bs @ ((xs ! i) # cs))))"
[PROOF STATE]
proof (prove)
using this:
as @ xs ! j # bs @ xs ! i # cs = xs

goal (1 subgoal):
 1. filter P xs = filter P (as @ xs ! j # bs @ xs ! i # cs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
filter P xs = filter P (as @ xs ! j # bs @ xs ! i # cs)

goal (2 subgoals):
 1. i = j \<Longrightarrow> i = j
 2. j < i \<Longrightarrow> i = j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
filter P xs = filter P (as @ xs ! j # bs @ xs ! i # cs)

goal (2 subgoals):
 1. i = j \<Longrightarrow> i = j
 2. j < i \<Longrightarrow> i = j
[PROOF STEP]
from assms(4, 5)
[PROOF STATE]
proof (chain)
picking this:
P (xs ! i)
P (xs ! j)
[PROOF STEP]
have "... = (filter P as) @ ((xs ! j) # ((filter P bs) @ ((xs ! i) # (filter P cs))))"
[PROOF STATE]
proof (prove)
using this:
P (xs ! i)
P (xs ! j)

goal (1 subgoal):
 1. filter P (as @ xs ! j # bs @ xs ! i # cs) = filter P as @ xs ! j # filter P bs @ xs ! i # filter P cs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
filter P (as @ xs ! j # bs @ xs ! i # cs) = filter P as @ xs ! j # filter P bs @ xs ! i # filter P cs

goal (2 subgoals):
 1. i = j \<Longrightarrow> i = j
 2. j < i \<Longrightarrow> i = j
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
filter P xs = filter P as @ xs ! j # filter P bs @ xs ! i # filter P cs
[PROOF STEP]
have "\<not> length (filter P xs) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
filter P xs = filter P as @ xs ! j # filter P bs @ xs ! i # filter P cs

goal (1 subgoal):
 1. \<not> length (filter P xs) \<le> 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> length (filter P xs) \<le> 1

goal (2 subgoals):
 1. i = j \<Longrightarrow> i = j
 2. j < i \<Longrightarrow> i = j
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> length (filter P xs) \<le> 1

goal (1 subgoal):
 1. i = j
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<not> length (filter P xs) \<le> 1
length (filter P xs) \<le> 1

goal (1 subgoal):
 1. i = j
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
i = j

goal (1 subgoal):
 1. i = j \<Longrightarrow> i = j
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i = j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_filter_eq [simp]: "length (filter ((=) x) xs) = count_list xs x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (filter ((=) x) xs) = count_list xs x
[PROOF STEP]
by (induct xs, simp_all)


[STATEMENT]
lemma nth_in_set_dropI:
  assumes "j \<le> i" and "i < length xs"
  shows "xs ! i \<in> set (drop j xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs ! i \<in> set (drop j xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
j \<le> i
i < length xs

goal (1 subgoal):
 1. xs ! i \<in> set (drop j xs)
[PROOF STEP]
proof (induct xs arbitrary: i j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>j \<le> i; i < length []\<rbrakk> \<Longrightarrow> [] ! i \<in> set (drop j [])
 2. \<And>a xs i j. \<lbrakk>\<And>i j. \<lbrakk>j \<le> i; i < length xs\<rbrakk> \<Longrightarrow> xs ! i \<in> set (drop j xs); j \<le> i; i < length (a # xs)\<rbrakk> \<Longrightarrow> (a # xs) ! i \<in> set (drop j (a # xs))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
j \<le> i
i < length []

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>j \<le> i; i < length []\<rbrakk> \<Longrightarrow> [] ! i \<in> set (drop j [])
 2. \<And>a xs i j. \<lbrakk>\<And>i j. \<lbrakk>j \<le> i; i < length xs\<rbrakk> \<Longrightarrow> xs ! i \<in> set (drop j xs); j \<le> i; i < length (a # xs)\<rbrakk> \<Longrightarrow> (a # xs) ! i \<in> set (drop j (a # xs))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
j \<le> i
i < length []

goal (1 subgoal):
 1. [] ! i \<in> set (drop j [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[] ! i \<in> set (drop j [])

goal (1 subgoal):
 1. \<And>a xs i j. \<lbrakk>\<And>i j. \<lbrakk>j \<le> i; i < length xs\<rbrakk> \<Longrightarrow> xs ! i \<in> set (drop j xs); j \<le> i; i < length (a # xs)\<rbrakk> \<Longrightarrow> (a # xs) ! i \<in> set (drop j (a # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs i j. \<lbrakk>\<And>i j. \<lbrakk>j \<le> i; i < length xs\<rbrakk> \<Longrightarrow> xs ! i \<in> set (drop j xs); j \<le> i; i < length (a # xs)\<rbrakk> \<Longrightarrow> (a # xs) ! i \<in> set (drop j (a # xs))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?j \<le> ?i; ?i < length xs\<rbrakk> \<Longrightarrow> xs ! ?i \<in> set (drop ?j xs)
j \<le> i
i < length (x # xs)

goal (1 subgoal):
 1. \<And>a xs i j. \<lbrakk>\<And>i j. \<lbrakk>j \<le> i; i < length xs\<rbrakk> \<Longrightarrow> xs ! i \<in> set (drop j xs); j \<le> i; i < length (a # xs)\<rbrakk> \<Longrightarrow> (a # xs) ! i \<in> set (drop j (a # xs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs) ! i \<in> set (drop j (x # xs))
[PROOF STEP]
proof (cases j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j = 0 \<Longrightarrow> (x # xs) ! i \<in> set (drop j (x # xs))
 2. \<And>nat. j = Suc nat \<Longrightarrow> (x # xs) ! i \<in> set (drop j (x # xs))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
j = 0

goal (2 subgoals):
 1. j = 0 \<Longrightarrow> (x # xs) ! i \<in> set (drop j (x # xs))
 2. \<And>nat. j = Suc nat \<Longrightarrow> (x # xs) ! i \<in> set (drop j (x # xs))
[PROOF STEP]
with Cons(3)
[PROOF STATE]
proof (chain)
picking this:
i < length (x # xs)
j = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i < length (x # xs)
j = 0

goal (1 subgoal):
 1. (x # xs) ! i \<in> set (drop j (x # xs))
[PROOF STEP]
by (metis drop0 nth_mem)
[PROOF STATE]
proof (state)
this:
(x # xs) ! i \<in> set (drop j (x # xs))

goal (1 subgoal):
 1. \<And>nat. j = Suc nat \<Longrightarrow> (x # xs) ! i \<in> set (drop j (x # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. j = Suc nat \<Longrightarrow> (x # xs) ! i \<in> set (drop j (x # xs))
[PROOF STEP]
case (Suc j0)
[PROOF STATE]
proof (state)
this:
j = Suc j0

goal (1 subgoal):
 1. \<And>nat. j = Suc nat \<Longrightarrow> (x # xs) ! i \<in> set (drop j (x # xs))
[PROOF STEP]
with Cons(2) Suc_le_D
[PROOF STATE]
proof (chain)
picking this:
j \<le> i
Suc ?n \<le> ?m' \<Longrightarrow> \<exists>m. ?m' = Suc m
j = Suc j0
[PROOF STEP]
obtain i0 where i: "i = Suc i0"
[PROOF STATE]
proof (prove)
using this:
j \<le> i
Suc ?n \<le> ?m' \<Longrightarrow> \<exists>m. ?m' = Suc m
j = Suc j0

goal (1 subgoal):
 1. (\<And>i0. i = Suc i0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i = Suc i0

goal (1 subgoal):
 1. \<And>nat. j = Suc nat \<Longrightarrow> (x # xs) ! i \<in> set (drop j (x # xs))
[PROOF STEP]
with Cons(2)
[PROOF STATE]
proof (chain)
picking this:
j \<le> i
i = Suc i0
[PROOF STEP]
have "j0 \<le> i0"
[PROOF STATE]
proof (prove)
using this:
j \<le> i
i = Suc i0

goal (1 subgoal):
 1. j0 \<le> i0
[PROOF STEP]
by (simp add: \<open>j = Suc j0\<close>)
[PROOF STATE]
proof (state)
this:
j0 \<le> i0

goal (1 subgoal):
 1. \<And>nat. j = Suc nat \<Longrightarrow> (x # xs) ! i \<in> set (drop j (x # xs))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j0 \<le> i0

goal (1 subgoal):
 1. \<And>nat. j = Suc nat \<Longrightarrow> (x # xs) ! i \<in> set (drop j (x # xs))
[PROOF STEP]
from Cons(3)
[PROOF STATE]
proof (chain)
picking this:
i < length (x # xs)
[PROOF STEP]
have "i0 < length xs"
[PROOF STATE]
proof (prove)
using this:
i < length (x # xs)

goal (1 subgoal):
 1. i0 < length xs
[PROOF STEP]
by (simp add: i)
[PROOF STATE]
proof (state)
this:
i0 < length xs

goal (1 subgoal):
 1. \<And>nat. j = Suc nat \<Longrightarrow> (x # xs) ! i \<in> set (drop j (x # xs))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j0 \<le> i0
i0 < length xs
[PROOF STEP]
have "xs ! i0 \<in> set (drop j0 xs)"
[PROOF STATE]
proof (prove)
using this:
j0 \<le> i0
i0 < length xs

goal (1 subgoal):
 1. xs ! i0 \<in> set (drop j0 xs)
[PROOF STEP]
by (rule Cons(1))
[PROOF STATE]
proof (state)
this:
xs ! i0 \<in> set (drop j0 xs)

goal (1 subgoal):
 1. \<And>nat. j = Suc nat \<Longrightarrow> (x # xs) ! i \<in> set (drop j (x # xs))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
xs ! i0 \<in> set (drop j0 xs)

goal (1 subgoal):
 1. (x # xs) ! i \<in> set (drop j (x # xs))
[PROOF STEP]
by (simp add: i \<open>j = Suc j0\<close>)
[PROOF STATE]
proof (state)
this:
(x # xs) ! i \<in> set (drop j (x # xs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x # xs) ! i \<in> set (drop j (x # xs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma count_list_upt [simp]: "count_list [a..<b] x = (if a \<le> x \<and> x < b then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list [a..<b] x = (if a \<le> x \<and> x < b then 1 else 0)
[PROOF STEP]
proof (cases "a \<le> b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> count_list [a..<b] x = (if a \<le> x \<and> x < b then 1 else 0)
 2. \<not> a \<le> b \<Longrightarrow> count_list [a..<b] x = (if a \<le> x \<and> x < b then 1 else 0)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<le> b

goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> count_list [a..<b] x = (if a \<le> x \<and> x < b then 1 else 0)
 2. \<not> a \<le> b \<Longrightarrow> count_list [a..<b] x = (if a \<le> x \<and> x < b then 1 else 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<le> b
[PROOF STEP]
obtain k where "b = a + k"
[PROOF STATE]
proof (prove)
using this:
a \<le> b

goal (1 subgoal):
 1. (\<And>k. b = a + k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using le_Suc_ex
[PROOF STATE]
proof (prove)
using this:
a \<le> b
?k \<le> ?l \<Longrightarrow> \<exists>n. ?l = ?k + n

goal (1 subgoal):
 1. (\<And>k. b = a + k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b = a + k

goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> count_list [a..<b] x = (if a \<le> x \<and> x < b then 1 else 0)
 2. \<not> a \<le> b \<Longrightarrow> count_list [a..<b] x = (if a \<le> x \<and> x < b then 1 else 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list [a..<b] x = (if a \<le> x \<and> x < b then 1 else 0)
[PROOF STEP]
unfolding \<open>b = a + k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list [a..<a + k] x = (if a \<le> x \<and> x < a + k then 1 else 0)
[PROOF STEP]
by (induct k, simp_all)
[PROOF STATE]
proof (state)
this:
count_list [a..<b] x = (if a \<le> x \<and> x < b then 1 else 0)

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> count_list [a..<b] x = (if a \<le> x \<and> x < b then 1 else 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> count_list [a..<b] x = (if a \<le> x \<and> x < b then 1 else 0)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> a \<le> b

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> count_list [a..<b] x = (if a \<le> x \<and> x < b then 1 else 0)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> a \<le> b

goal (1 subgoal):
 1. count_list [a..<b] x = (if a \<le> x \<and> x < b then 1 else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count_list [a..<b] x = (if a \<le> x \<and> x < b then 1 else 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sorted_wrt_upt_iff: "sorted_wrt rel [a..<b] \<longleftrightarrow> (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < b \<longrightarrow> rel i j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt rel [a..<b] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < b \<longrightarrow> rel i j)
[PROOF STEP]
proof (cases "a \<le> b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> sorted_wrt rel [a..<b] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < b \<longrightarrow> rel i j)
 2. \<not> a \<le> b \<Longrightarrow> sorted_wrt rel [a..<b] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < b \<longrightarrow> rel i j)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<le> b

goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> sorted_wrt rel [a..<b] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < b \<longrightarrow> rel i j)
 2. \<not> a \<le> b \<Longrightarrow> sorted_wrt rel [a..<b] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < b \<longrightarrow> rel i j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<le> b
[PROOF STEP]
obtain k where "b = a + k"
[PROOF STATE]
proof (prove)
using this:
a \<le> b

goal (1 subgoal):
 1. (\<And>k. b = a + k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using le_Suc_ex
[PROOF STATE]
proof (prove)
using this:
a \<le> b
?k \<le> ?l \<Longrightarrow> \<exists>n. ?l = ?k + n

goal (1 subgoal):
 1. (\<And>k. b = a + k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b = a + k

goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> sorted_wrt rel [a..<b] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < b \<longrightarrow> rel i j)
 2. \<not> a \<le> b \<Longrightarrow> sorted_wrt rel [a..<b] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < b \<longrightarrow> rel i j)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt rel [a..<b] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < b \<longrightarrow> rel i j)
[PROOF STEP]
unfolding \<open>b = a + k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt rel [a..<a + k] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + k \<longrightarrow> rel i j)
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sorted_wrt rel [a..<a + 0] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + 0 \<longrightarrow> rel i j)
 2. \<And>k. sorted_wrt rel [a..<a + k] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + k \<longrightarrow> rel i j) \<Longrightarrow> sorted_wrt rel [a..<a + Suc k] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + Suc k \<longrightarrow> rel i j)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. sorted_wrt rel [a..<a + 0] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + 0 \<longrightarrow> rel i j)
 2. \<And>k. sorted_wrt rel [a..<a + k] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + k \<longrightarrow> rel i j) \<Longrightarrow> sorted_wrt rel [a..<a + Suc k] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + Suc k \<longrightarrow> rel i j)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt rel [a..<a + 0] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + 0 \<longrightarrow> rel i j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sorted_wrt rel [a..<a + 0] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + 0 \<longrightarrow> rel i j)

goal (1 subgoal):
 1. \<And>k. sorted_wrt rel [a..<a + k] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + k \<longrightarrow> rel i j) \<Longrightarrow> sorted_wrt rel [a..<a + Suc k] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + Suc k \<longrightarrow> rel i j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. sorted_wrt rel [a..<a + k] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + k \<longrightarrow> rel i j) \<Longrightarrow> sorted_wrt rel [a..<a + Suc k] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + Suc k \<longrightarrow> rel i j)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
sorted_wrt rel [a..<a + k] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + k \<longrightarrow> rel i j)

goal (1 subgoal):
 1. \<And>k. sorted_wrt rel [a..<a + k] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + k \<longrightarrow> rel i j) \<Longrightarrow> sorted_wrt rel [a..<a + Suc k] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + Suc k \<longrightarrow> rel i j)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt rel [a..<a + Suc k] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + Suc k \<longrightarrow> rel i j)
[PROOF STEP]
proof (simp add: sorted_wrt_append Suc, intro iffI allI ballI impI conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>(\<forall>i\<ge>a. \<forall>j>i. j < a + k \<longrightarrow> rel i j) \<and> (\<forall>x\<in>{a..<a + k}. rel x (a + k)); a \<le> i; i < j; j < Suc (a + k)\<rbrakk> \<Longrightarrow> rel i j
 2. \<And>i j. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; a \<le> i; i < j; j < a + k\<rbrakk> \<Longrightarrow> rel i j
 3. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>(\<forall>i\<ge>a. \<forall>j>i. j < a + k \<longrightarrow> rel i j) \<and> (\<forall>x\<in>{a..<a + k}. rel x (a + k)); a \<le> i; i < j; j < Suc (a + k)\<rbrakk> \<Longrightarrow> rel i j
 2. \<And>i j. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; a \<le> i; i < j; j < a + k\<rbrakk> \<Longrightarrow> rel i j
 3. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
assume "(\<forall>i\<ge>a. \<forall>j>i. j < a + k \<longrightarrow> rel i j) \<and> (\<forall>x\<in>{a..<a + k}. rel x (a + k))"
[PROOF STATE]
proof (state)
this:
(\<forall>i\<ge>a. \<forall>j>i. j < a + k \<longrightarrow> rel i j) \<and> (\<forall>x\<in>{a..<a + k}. rel x (a + k))

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>(\<forall>i\<ge>a. \<forall>j>i. j < a + k \<longrightarrow> rel i j) \<and> (\<forall>x\<in>{a..<a + k}. rel x (a + k)); a \<le> i; i < j; j < Suc (a + k)\<rbrakk> \<Longrightarrow> rel i j
 2. \<And>i j. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; a \<le> i; i < j; j < a + k\<rbrakk> \<Longrightarrow> rel i j
 3. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
hence 1: "\<And>i' j'. a \<le> i' \<Longrightarrow> i' < j' \<Longrightarrow> j' < a + k \<Longrightarrow> rel i' j'"
        and 2: "\<And>x. a \<le> x \<Longrightarrow> x < a + k \<Longrightarrow> rel x (a + k)"
[PROOF STATE]
proof (prove)
using this:
(\<forall>i\<ge>a. \<forall>j>i. j < a + k \<longrightarrow> rel i j) \<and> (\<forall>x\<in>{a..<a + k}. rel x (a + k))

goal (1 subgoal):
 1. (\<And>i' j'. \<lbrakk>a \<le> i'; i' < j'; j' < a + k\<rbrakk> \<Longrightarrow> rel i' j') &&& (\<And>x. \<lbrakk>a \<le> x; x < a + k\<rbrakk> \<Longrightarrow> rel x (a + k))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<le> ?i'; ?i' < ?j'; ?j' < a + k\<rbrakk> \<Longrightarrow> rel ?i' ?j'
\<lbrakk>a \<le> ?x; ?x < a + k\<rbrakk> \<Longrightarrow> rel ?x (a + k)

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>(\<forall>i\<ge>a. \<forall>j>i. j < a + k \<longrightarrow> rel i j) \<and> (\<forall>x\<in>{a..<a + k}. rel x (a + k)); a \<le> i; i < j; j < Suc (a + k)\<rbrakk> \<Longrightarrow> rel i j
 2. \<And>i j. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; a \<le> i; i < j; j < a + k\<rbrakk> \<Longrightarrow> rel i j
 3. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
assume "a \<le> i" and "i < j"
[PROOF STATE]
proof (state)
this:
a \<le> i
i < j

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>(\<forall>i\<ge>a. \<forall>j>i. j < a + k \<longrightarrow> rel i j) \<and> (\<forall>x\<in>{a..<a + k}. rel x (a + k)); a \<le> i; i < j; j < Suc (a + k)\<rbrakk> \<Longrightarrow> rel i j
 2. \<And>i j. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; a \<le> i; i < j; j < a + k\<rbrakk> \<Longrightarrow> rel i j
 3. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
assume "j < Suc (a + k)"
[PROOF STATE]
proof (state)
this:
j < Suc (a + k)

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>(\<forall>i\<ge>a. \<forall>j>i. j < a + k \<longrightarrow> rel i j) \<and> (\<forall>x\<in>{a..<a + k}. rel x (a + k)); a \<le> i; i < j; j < Suc (a + k)\<rbrakk> \<Longrightarrow> rel i j
 2. \<And>i j. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; a \<le> i; i < j; j < a + k\<rbrakk> \<Longrightarrow> rel i j
 3. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
hence "j < a + k \<or> j = a + k"
[PROOF STATE]
proof (prove)
using this:
j < Suc (a + k)

goal (1 subgoal):
 1. j < a + k \<or> j = a + k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < a + k \<or> j = a + k

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>(\<forall>i\<ge>a. \<forall>j>i. j < a + k \<longrightarrow> rel i j) \<and> (\<forall>x\<in>{a..<a + k}. rel x (a + k)); a \<le> i; i < j; j < Suc (a + k)\<rbrakk> \<Longrightarrow> rel i j
 2. \<And>i j. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; a \<le> i; i < j; j < a + k\<rbrakk> \<Longrightarrow> rel i j
 3. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
thus "rel i j"
[PROOF STATE]
proof (prove)
using this:
j < a + k \<or> j = a + k

goal (1 subgoal):
 1. rel i j
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j < a + k \<Longrightarrow> rel i j
 2. j = a + k \<Longrightarrow> rel i j
[PROOF STEP]
assume "j < a + k"
[PROOF STATE]
proof (state)
this:
j < a + k

goal (2 subgoals):
 1. j < a + k \<Longrightarrow> rel i j
 2. j = a + k \<Longrightarrow> rel i j
[PROOF STEP]
with \<open>a \<le> i\<close> \<open>i < j\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<le> i
i < j
j < a + k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<le> i
i < j
j < a + k

goal (1 subgoal):
 1. rel i j
[PROOF STEP]
by (rule 1)
[PROOF STATE]
proof (state)
this:
rel i j

goal (1 subgoal):
 1. j = a + k \<Longrightarrow> rel i j
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j = a + k \<Longrightarrow> rel i j
[PROOF STEP]
assume "j = a + k"
[PROOF STATE]
proof (state)
this:
j = a + k

goal (1 subgoal):
 1. j = a + k \<Longrightarrow> rel i j
[PROOF STEP]
from \<open>a \<le> i\<close> \<open>i < j\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<le> i
i < j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<le> i
i < j

goal (1 subgoal):
 1. rel i j
[PROOF STEP]
unfolding \<open>j = a + k\<close>
[PROOF STATE]
proof (prove)
using this:
a \<le> i
i < a + k

goal (1 subgoal):
 1. rel i (a + k)
[PROOF STEP]
by (rule 2)
[PROOF STATE]
proof (state)
this:
rel i j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel i j

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; a \<le> i; i < j; j < a + k\<rbrakk> \<Longrightarrow> rel i j
 2. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; a \<le> i; i < j; j < a + k\<rbrakk> \<Longrightarrow> rel i j
 2. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; a \<le> i; i < j; j < a + k\<rbrakk> \<Longrightarrow> rel i j
 2. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
assume "\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j" and "a \<le> i" and "i < j" and "j < a + k"
[PROOF STATE]
proof (state)
this:
\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j
a \<le> i
i < j
j < a + k

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; a \<le> i; i < j; j < a + k\<rbrakk> \<Longrightarrow> rel i j
 2. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
thus "rel i j"
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j
a \<le> i
i < j
j < a + k

goal (1 subgoal):
 1. rel i j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rel i j

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
assume "x \<in> {a..<a + k}"
[PROOF STATE]
proof (state)
this:
x \<in> {a..<a + k}

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
hence "a \<le> x" and "x < a + k"
[PROOF STATE]
proof (prove)
using this:
x \<in> {a..<a + k}

goal (1 subgoal):
 1. a \<le> x &&& x < a + k
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
a \<le> x
x < a + k

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<le> x
x < a + k

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
assume "\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j"
[PROOF STATE]
proof (state)
this:
\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j; x \<in> {a..<a + k}\<rbrakk> \<Longrightarrow> rel x (a + k)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<le> x
x < a + k
\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j
[PROOF STEP]
show "rel x (a + k)"
[PROOF STATE]
proof (prove)
using this:
a \<le> x
x < a + k
\<forall>i\<ge>a. \<forall>j>i. j < Suc (a + k) \<longrightarrow> rel i j

goal (1 subgoal):
 1. rel x (a + k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rel x (a + k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sorted_wrt rel [a..<a + Suc k] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < a + Suc k \<longrightarrow> rel i j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sorted_wrt rel [a..<b] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < b \<longrightarrow> rel i j)

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> sorted_wrt rel [a..<b] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < b \<longrightarrow> rel i j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> sorted_wrt rel [a..<b] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < b \<longrightarrow> rel i j)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> a \<le> b

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> sorted_wrt rel [a..<b] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < b \<longrightarrow> rel i j)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> a \<le> b

goal (1 subgoal):
 1. sorted_wrt rel [a..<b] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < b \<longrightarrow> rel i j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sorted_wrt rel [a..<b] = (\<forall>i j. a \<le> i \<longrightarrow> i < j \<longrightarrow> j < b \<longrightarrow> rel i j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_insort_wrt:
  assumes "\<And>x. x \<in> set xs \<Longrightarrow> r2 (f y) (f x) \<longleftrightarrow> r1 y x"
  shows "map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> set xs \<Longrightarrow> r2 (f y) (f ?x) = r1 y ?x

goal (1 subgoal):
 1. map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs)
[PROOF STEP]
proof (induct xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> r2 (f y) (f x) = r1 y x) \<Longrightarrow> map f (insort_wrt r1 y []) = insort_wrt r2 (f y) (map f [])
 2. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> r2 (f y) (f x) = r1 y x) \<Longrightarrow> map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> r2 (f y) (f x) = r1 y x\<rbrakk> \<Longrightarrow> map f (insort_wrt r1 y (a # xs)) = insort_wrt r2 (f y) (map f (a # xs))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
?x \<in> set [] \<Longrightarrow> r2 (f y) (f ?x) = r1 y ?x

goal (2 subgoals):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> r2 (f y) (f x) = r1 y x) \<Longrightarrow> map f (insort_wrt r1 y []) = insort_wrt r2 (f y) (map f [])
 2. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> r2 (f y) (f x) = r1 y x) \<Longrightarrow> map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> r2 (f y) (f x) = r1 y x\<rbrakk> \<Longrightarrow> map f (insort_wrt r1 y (a # xs)) = insort_wrt r2 (f y) (map f (a # xs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f (insort_wrt r1 y []) = insort_wrt r2 (f y) (map f [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map f (insort_wrt r1 y []) = insort_wrt r2 (f y) (map f [])

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> r2 (f y) (f x) = r1 y x) \<Longrightarrow> map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> r2 (f y) (f x) = r1 y x\<rbrakk> \<Longrightarrow> map f (insort_wrt r1 y (a # xs)) = insort_wrt r2 (f y) (map f (a # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> r2 (f y) (f x) = r1 y x) \<Longrightarrow> map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> r2 (f y) (f x) = r1 y x\<rbrakk> \<Longrightarrow> map f (insort_wrt r1 y (a # xs)) = insort_wrt r2 (f y) (map f (a # xs))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
(\<And>x. x \<in> set xs \<Longrightarrow> r2 (f y) (f x) = r1 y x) \<Longrightarrow> map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs)
?x \<in> set (x # xs) \<Longrightarrow> r2 (f y) (f ?x) = r1 y ?x

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> r2 (f y) (f x) = r1 y x) \<Longrightarrow> map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> r2 (f y) (f x) = r1 y x\<rbrakk> \<Longrightarrow> map f (insort_wrt r1 y (a # xs)) = insort_wrt r2 (f y) (map f (a # xs))
[PROOF STEP]
have "x \<in> set (x # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set (x # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> set (x # xs)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> r2 (f y) (f x) = r1 y x) \<Longrightarrow> map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> r2 (f y) (f x) = r1 y x\<rbrakk> \<Longrightarrow> map f (insort_wrt r1 y (a # xs)) = insort_wrt r2 (f y) (map f (a # xs))
[PROOF STEP]
hence "r2 (f y) (f x) = r1 y x"
[PROOF STATE]
proof (prove)
using this:
x \<in> set (x # xs)

goal (1 subgoal):
 1. r2 (f y) (f x) = r1 y x
[PROOF STEP]
by (rule Cons(2))
[PROOF STATE]
proof (state)
this:
r2 (f y) (f x) = r1 y x

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> r2 (f y) (f x) = r1 y x) \<Longrightarrow> map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> r2 (f y) (f x) = r1 y x\<rbrakk> \<Longrightarrow> map f (insort_wrt r1 y (a # xs)) = insort_wrt r2 (f y) (map f (a # xs))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r2 (f y) (f x) = r1 y x

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> r2 (f y) (f x) = r1 y x) \<Longrightarrow> map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> r2 (f y) (f x) = r1 y x\<rbrakk> \<Longrightarrow> map f (insort_wrt r1 y (a # xs)) = insort_wrt r2 (f y) (map f (a # xs))
[PROOF STEP]
have "map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs)
[PROOF STEP]
proof (rule Cons(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set xs \<Longrightarrow> r2 (f y) (f x) = r1 y x
[PROOF STEP]
fix x'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set xs \<Longrightarrow> r2 (f y) (f x) = r1 y x
[PROOF STEP]
assume "x' \<in> set xs"
[PROOF STATE]
proof (state)
this:
x' \<in> set xs

goal (1 subgoal):
 1. \<And>x. x \<in> set xs \<Longrightarrow> r2 (f y) (f x) = r1 y x
[PROOF STEP]
hence "x' \<in> set (x # xs)"
[PROOF STATE]
proof (prove)
using this:
x' \<in> set xs

goal (1 subgoal):
 1. x' \<in> set (x # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x' \<in> set (x # xs)

goal (1 subgoal):
 1. \<And>x. x \<in> set xs \<Longrightarrow> r2 (f y) (f x) = r1 y x
[PROOF STEP]
thus "r2 (f y) (f x') = r1 y x'"
[PROOF STATE]
proof (prove)
using this:
x' \<in> set (x # xs)

goal (1 subgoal):
 1. r2 (f y) (f x') = r1 y x'
[PROOF STEP]
by (rule Cons(2))
[PROOF STATE]
proof (state)
this:
r2 (f y) (f x') = r1 y x'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> r2 (f y) (f x) = r1 y x) \<Longrightarrow> map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs); \<And>x. x \<in> set (a # xs) \<Longrightarrow> r2 (f y) (f x) = r1 y x\<rbrakk> \<Longrightarrow> map f (insort_wrt r1 y (a # xs)) = insort_wrt r2 (f y) (map f (a # xs))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r2 (f y) (f x) = r1 y x
map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
r2 (f y) (f x) = r1 y x
map f (insort_wrt r1 y xs) = insort_wrt r2 (f y) (map f xs)

goal (1 subgoal):
 1. map f (insort_wrt r1 y (x # xs)) = insort_wrt r2 (f y) (map f (x # xs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map f (insort_wrt r1 y (x # xs)) = insort_wrt r2 (f y) (map f (x # xs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_merge_wrt:
  assumes "f ` set xs \<inter> f ` set ys = {}"
    and "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set ys \<Longrightarrow> r2 (f x) (f y) \<longleftrightarrow> r1 x y"
  shows "map f (merge_wrt r1 xs ys) = merge_wrt r2 (map f xs) (map f ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f (merge_wrt r1 xs ys) = merge_wrt r2 (map f xs) (map f ys)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f ` set xs \<inter> f ` set ys = {}
\<lbrakk>?x \<in> set xs; ?y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f ?x) (f ?y) = r1 ?x ?y

goal (1 subgoal):
 1. map f (merge_wrt r1 xs ys) = merge_wrt r2 (map f xs) (map f ys)
[PROOF STEP]
proof (induct r1 xs ys rule: merge_wrt.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>uu_ xs. \<lbrakk>f ` set xs \<inter> f ` set [] = {}; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set []\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = uu_ x y\<rbrakk> \<Longrightarrow> map f (merge_wrt uu_ xs []) = merge_wrt r2 (map f xs) (map f [])
 2. \<And>rel v va. \<lbrakk>f ` set [] \<inter> f ` set (v # va) = {}; \<And>x y. \<lbrakk>x \<in> set []; y \<in> set (v # va)\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel [] (v # va)) = merge_wrt r2 (map f []) (map f (v # va))
 3. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; f ` set xs \<inter> f ` set ys = {}; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs ys) = merge_wrt r2 (map f xs) (map f ys); \<lbrakk>x \<noteq> y; rel x y; f ` set xs \<inter> f ` set (y # ys) = {}; \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = rel x ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys)); \<lbrakk>x \<noteq> y; \<not> rel x y; f ` set (x # xs) \<inter> f ` set ys = {}; \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = rel xa y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys); f ` set (x # xs) \<inter> f ` set (y # ys) = {}; \<And>xa ya. \<lbrakk>xa \<in> set (x # xs); ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f xa) (f ya) = rel xa ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) (y # ys)) = merge_wrt r2 (map f (x # xs)) (map f (y # ys))
[PROOF STEP]
case (1 uu xs)
[PROOF STATE]
proof (state)
this:
f ` set xs \<inter> f ` set [] = {}
\<lbrakk>?x \<in> set xs; ?y \<in> set []\<rbrakk> \<Longrightarrow> r2 (f ?x) (f ?y) = uu ?x ?y

goal (3 subgoals):
 1. \<And>uu_ xs. \<lbrakk>f ` set xs \<inter> f ` set [] = {}; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set []\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = uu_ x y\<rbrakk> \<Longrightarrow> map f (merge_wrt uu_ xs []) = merge_wrt r2 (map f xs) (map f [])
 2. \<And>rel v va. \<lbrakk>f ` set [] \<inter> f ` set (v # va) = {}; \<And>x y. \<lbrakk>x \<in> set []; y \<in> set (v # va)\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel [] (v # va)) = merge_wrt r2 (map f []) (map f (v # va))
 3. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; f ` set xs \<inter> f ` set ys = {}; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs ys) = merge_wrt r2 (map f xs) (map f ys); \<lbrakk>x \<noteq> y; rel x y; f ` set xs \<inter> f ` set (y # ys) = {}; \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = rel x ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys)); \<lbrakk>x \<noteq> y; \<not> rel x y; f ` set (x # xs) \<inter> f ` set ys = {}; \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = rel xa y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys); f ` set (x # xs) \<inter> f ` set (y # ys) = {}; \<And>xa ya. \<lbrakk>xa \<in> set (x # xs); ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f xa) (f ya) = rel xa ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) (y # ys)) = merge_wrt r2 (map f (x # xs)) (map f (y # ys))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f (merge_wrt uu xs []) = merge_wrt r2 (map f xs) (map f [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map f (merge_wrt uu xs []) = merge_wrt r2 (map f xs) (map f [])

goal (2 subgoals):
 1. \<And>rel v va. \<lbrakk>f ` set [] \<inter> f ` set (v # va) = {}; \<And>x y. \<lbrakk>x \<in> set []; y \<in> set (v # va)\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel [] (v # va)) = merge_wrt r2 (map f []) (map f (v # va))
 2. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; f ` set xs \<inter> f ` set ys = {}; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs ys) = merge_wrt r2 (map f xs) (map f ys); \<lbrakk>x \<noteq> y; rel x y; f ` set xs \<inter> f ` set (y # ys) = {}; \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = rel x ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys)); \<lbrakk>x \<noteq> y; \<not> rel x y; f ` set (x # xs) \<inter> f ` set ys = {}; \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = rel xa y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys); f ` set (x # xs) \<inter> f ` set (y # ys) = {}; \<And>xa ya. \<lbrakk>xa \<in> set (x # xs); ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f xa) (f ya) = rel xa ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) (y # ys)) = merge_wrt r2 (map f (x # xs)) (map f (y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>rel v va. \<lbrakk>f ` set [] \<inter> f ` set (v # va) = {}; \<And>x y. \<lbrakk>x \<in> set []; y \<in> set (v # va)\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel [] (v # va)) = merge_wrt r2 (map f []) (map f (v # va))
 2. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; f ` set xs \<inter> f ` set ys = {}; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs ys) = merge_wrt r2 (map f xs) (map f ys); \<lbrakk>x \<noteq> y; rel x y; f ` set xs \<inter> f ` set (y # ys) = {}; \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = rel x ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys)); \<lbrakk>x \<noteq> y; \<not> rel x y; f ` set (x # xs) \<inter> f ` set ys = {}; \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = rel xa y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys); f ` set (x # xs) \<inter> f ` set (y # ys) = {}; \<And>xa ya. \<lbrakk>xa \<in> set (x # xs); ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f xa) (f ya) = rel xa ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) (y # ys)) = merge_wrt r2 (map f (x # xs)) (map f (y # ys))
[PROOF STEP]
case (2 r1 v va)
[PROOF STATE]
proof (state)
this:
f ` set [] \<inter> f ` set (v # va) = {}
\<lbrakk>?x \<in> set []; ?y \<in> set (v # va)\<rbrakk> \<Longrightarrow> r2 (f ?x) (f ?y) = r1 ?x ?y

goal (2 subgoals):
 1. \<And>rel v va. \<lbrakk>f ` set [] \<inter> f ` set (v # va) = {}; \<And>x y. \<lbrakk>x \<in> set []; y \<in> set (v # va)\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel [] (v # va)) = merge_wrt r2 (map f []) (map f (v # va))
 2. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; f ` set xs \<inter> f ` set ys = {}; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs ys) = merge_wrt r2 (map f xs) (map f ys); \<lbrakk>x \<noteq> y; rel x y; f ` set xs \<inter> f ` set (y # ys) = {}; \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = rel x ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys)); \<lbrakk>x \<noteq> y; \<not> rel x y; f ` set (x # xs) \<inter> f ` set ys = {}; \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = rel xa y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys); f ` set (x # xs) \<inter> f ` set (y # ys) = {}; \<And>xa ya. \<lbrakk>xa \<in> set (x # xs); ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f xa) (f ya) = rel xa ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) (y # ys)) = merge_wrt r2 (map f (x # xs)) (map f (y # ys))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f (merge_wrt r1 [] (v # va)) = merge_wrt r2 (map f []) (map f (v # va))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map f (merge_wrt r1 [] (v # va)) = merge_wrt r2 (map f []) (map f (v # va))

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; f ` set xs \<inter> f ` set ys = {}; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs ys) = merge_wrt r2 (map f xs) (map f ys); \<lbrakk>x \<noteq> y; rel x y; f ` set xs \<inter> f ` set (y # ys) = {}; \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = rel x ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys)); \<lbrakk>x \<noteq> y; \<not> rel x y; f ` set (x # xs) \<inter> f ` set ys = {}; \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = rel xa y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys); f ` set (x # xs) \<inter> f ` set (y # ys) = {}; \<And>xa ya. \<lbrakk>xa \<in> set (x # xs); ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f xa) (f ya) = rel xa ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) (y # ys)) = merge_wrt r2 (map f (x # xs)) (map f (y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; f ` set xs \<inter> f ` set ys = {}; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs ys) = merge_wrt r2 (map f xs) (map f ys); \<lbrakk>x \<noteq> y; rel x y; f ` set xs \<inter> f ` set (y # ys) = {}; \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = rel x ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys)); \<lbrakk>x \<noteq> y; \<not> rel x y; f ` set (x # xs) \<inter> f ` set ys = {}; \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = rel xa y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys); f ` set (x # xs) \<inter> f ` set (y # ys) = {}; \<And>xa ya. \<lbrakk>xa \<in> set (x # xs); ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f xa) (f ya) = rel xa ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) (y # ys)) = merge_wrt r2 (map f (x # xs)) (map f (y # ys))
[PROOF STEP]
case (3 r1 x xs y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = y; f ` set xs \<inter> f ` set ys = {}; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = r1 x y\<rbrakk> \<Longrightarrow> map f (merge_wrt r1 xs ys) = merge_wrt r2 (map f xs) (map f ys)
\<lbrakk>x \<noteq> y; r1 x y; f ` set xs \<inter> f ` set (y # ys) = {}; \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = r1 x ya\<rbrakk> \<Longrightarrow> map f (merge_wrt r1 xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys))
\<lbrakk>x \<noteq> y; \<not> r1 x y; f ` set (x # xs) \<inter> f ` set ys = {}; \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = r1 xa y\<rbrakk> \<Longrightarrow> map f (merge_wrt r1 (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys)
f ` set (x # xs) \<inter> f ` set (y # ys) = {}
\<lbrakk>?x \<in> set (x # xs); ?y \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f ?x) (f ?y) = r1 ?x ?y

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; f ` set xs \<inter> f ` set ys = {}; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs ys) = merge_wrt r2 (map f xs) (map f ys); \<lbrakk>x \<noteq> y; rel x y; f ` set xs \<inter> f ` set (y # ys) = {}; \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = rel x ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys)); \<lbrakk>x \<noteq> y; \<not> rel x y; f ` set (x # xs) \<inter> f ` set ys = {}; \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = rel xa y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys); f ` set (x # xs) \<inter> f ` set (y # ys) = {}; \<And>xa ya. \<lbrakk>xa \<in> set (x # xs); ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f xa) (f ya) = rel xa ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) (y # ys)) = merge_wrt r2 (map f (x # xs)) (map f (y # ys))
[PROOF STEP]
from 3(4)
[PROOF STATE]
proof (chain)
picking this:
f ` set (x # xs) \<inter> f ` set (y # ys) = {}
[PROOF STEP]
have "f x \<noteq> f y" and 1: "f ` set xs \<inter> f ` set (y # ys) = {}"
    and 2: "f ` set (x # xs) \<inter> f ` set ys = {}"
[PROOF STATE]
proof (prove)
using this:
f ` set (x # xs) \<inter> f ` set (y # ys) = {}

goal (1 subgoal):
 1. f x \<noteq> f y &&& f ` set xs \<inter> f ` set (y # ys) = {} &&& f ` set (x # xs) \<inter> f ` set ys = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f x \<noteq> f y
f ` set xs \<inter> f ` set (y # ys) = {}
f ` set (x # xs) \<inter> f ` set ys = {}

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; f ` set xs \<inter> f ` set ys = {}; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs ys) = merge_wrt r2 (map f xs) (map f ys); \<lbrakk>x \<noteq> y; rel x y; f ` set xs \<inter> f ` set (y # ys) = {}; \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = rel x ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys)); \<lbrakk>x \<noteq> y; \<not> rel x y; f ` set (x # xs) \<inter> f ` set ys = {}; \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = rel xa y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys); f ` set (x # xs) \<inter> f ` set (y # ys) = {}; \<And>xa ya. \<lbrakk>xa \<in> set (x # xs); ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f xa) (f ya) = rel xa ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) (y # ys)) = merge_wrt r2 (map f (x # xs)) (map f (y # ys))
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
f x \<noteq> f y
[PROOF STEP]
have "x \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
f x \<noteq> f y

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; f ` set xs \<inter> f ` set ys = {}; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs ys) = merge_wrt r2 (map f xs) (map f ys); \<lbrakk>x \<noteq> y; rel x y; f ` set xs \<inter> f ` set (y # ys) = {}; \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = rel x ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys)); \<lbrakk>x \<noteq> y; \<not> rel x y; f ` set (x # xs) \<inter> f ` set ys = {}; \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = rel xa y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys); f ` set (x # xs) \<inter> f ` set (y # ys) = {}; \<And>xa ya. \<lbrakk>xa \<in> set (x # xs); ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f xa) (f ya) = rel xa ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) (y # ys)) = merge_wrt r2 (map f (x # xs)) (map f (y # ys))
[PROOF STEP]
have eq2: "map f (merge_wrt r1 xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys))"
    if "r1 x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f (merge_wrt r1 xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys))
[PROOF STEP]
using \<open>x \<noteq> y\<close> that 1
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
r1 x y
f ` set xs \<inter> f ` set (y # ys) = {}

goal (1 subgoal):
 1. map f (merge_wrt r1 xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys))
[PROOF STEP]
proof (rule 3(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = r1 x ya
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = r1 x ya
[PROOF STEP]
assume "a \<in> set xs"
[PROOF STATE]
proof (state)
this:
a \<in> set xs

goal (1 subgoal):
 1. \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = r1 x ya
[PROOF STEP]
hence "a \<in> set (x # xs)"
[PROOF STATE]
proof (prove)
using this:
a \<in> set xs

goal (1 subgoal):
 1. a \<in> set (x # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<in> set (x # xs)

goal (1 subgoal):
 1. \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = r1 x ya
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<in> set (x # xs)

goal (1 subgoal):
 1. \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = r1 x ya
[PROOF STEP]
assume "b \<in> set (y # ys)"
[PROOF STATE]
proof (state)
this:
b \<in> set (y # ys)

goal (1 subgoal):
 1. \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = r1 x ya
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<in> set (x # xs)
b \<in> set (y # ys)
[PROOF STEP]
show "r2 (f a) (f b) \<longleftrightarrow> r1 a b"
[PROOF STATE]
proof (prove)
using this:
a \<in> set (x # xs)
b \<in> set (y # ys)

goal (1 subgoal):
 1. r2 (f a) (f b) = r1 a b
[PROOF STEP]
by (rule 3(5))
[PROOF STATE]
proof (state)
this:
r2 (f a) (f b) = r1 a b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
r1 x y \<Longrightarrow> map f (merge_wrt r1 xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys))

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; f ` set xs \<inter> f ` set ys = {}; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs ys) = merge_wrt r2 (map f xs) (map f ys); \<lbrakk>x \<noteq> y; rel x y; f ` set xs \<inter> f ` set (y # ys) = {}; \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = rel x ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys)); \<lbrakk>x \<noteq> y; \<not> rel x y; f ` set (x # xs) \<inter> f ` set ys = {}; \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = rel xa y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys); f ` set (x # xs) \<inter> f ` set (y # ys) = {}; \<And>xa ya. \<lbrakk>xa \<in> set (x # xs); ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f xa) (f ya) = rel xa ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) (y # ys)) = merge_wrt r2 (map f (x # xs)) (map f (y # ys))
[PROOF STEP]
have eq3: "map f (merge_wrt r1 (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys)"
    if "\<not> r1 x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f (merge_wrt r1 (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys)
[PROOF STEP]
using \<open>x \<noteq> y\<close> that 2
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
\<not> r1 x y
f ` set (x # xs) \<inter> f ` set ys = {}

goal (1 subgoal):
 1. map f (merge_wrt r1 (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys)
[PROOF STEP]
proof (rule 3(3))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = r1 xa y
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = r1 xa y
[PROOF STEP]
assume "a \<in> set (x # xs)"
[PROOF STATE]
proof (state)
this:
a \<in> set (x # xs)

goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = r1 xa y
[PROOF STEP]
assume "b \<in> set ys"
[PROOF STATE]
proof (state)
this:
b \<in> set ys

goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = r1 xa y
[PROOF STEP]
hence "b \<in> set (y # ys)"
[PROOF STATE]
proof (prove)
using this:
b \<in> set ys

goal (1 subgoal):
 1. b \<in> set (y # ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b \<in> set (y # ys)

goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = r1 xa y
[PROOF STEP]
with \<open>a \<in> set (x # xs)\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<in> set (x # xs)
b \<in> set (y # ys)
[PROOF STEP]
show "r2 (f a) (f b) \<longleftrightarrow> r1 a b"
[PROOF STATE]
proof (prove)
using this:
a \<in> set (x # xs)
b \<in> set (y # ys)

goal (1 subgoal):
 1. r2 (f a) (f b) = r1 a b
[PROOF STEP]
by (rule 3(5))
[PROOF STATE]
proof (state)
this:
r2 (f a) (f b) = r1 a b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> r1 x y \<Longrightarrow> map f (merge_wrt r1 (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys)

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; f ` set xs \<inter> f ` set ys = {}; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs ys) = merge_wrt r2 (map f xs) (map f ys); \<lbrakk>x \<noteq> y; rel x y; f ` set xs \<inter> f ` set (y # ys) = {}; \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = rel x ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys)); \<lbrakk>x \<noteq> y; \<not> rel x y; f ` set (x # xs) \<inter> f ` set ys = {}; \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = rel xa y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys); f ` set (x # xs) \<inter> f ` set (y # ys) = {}; \<And>xa ya. \<lbrakk>xa \<in> set (x # xs); ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f xa) (f ya) = rel xa ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) (y # ys)) = merge_wrt r2 (map f (x # xs)) (map f (y # ys))
[PROOF STEP]
have eq4: "r2 (f x) (f y) \<longleftrightarrow> r1 x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r2 (f x) (f y) = r1 x y
[PROOF STEP]
by (rule 3(5), simp_all)
[PROOF STATE]
proof (state)
this:
r2 (f x) (f y) = r1 x y

goal (1 subgoal):
 1. \<And>rel x xs y ys. \<lbrakk>\<lbrakk>x = y; f ` set xs \<inter> f ` set ys = {}; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f x) (f y) = rel x y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs ys) = merge_wrt r2 (map f xs) (map f ys); \<lbrakk>x \<noteq> y; rel x y; f ` set xs \<inter> f ` set (y # ys) = {}; \<And>x ya. \<lbrakk>x \<in> set xs; ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f x) (f ya) = rel x ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel xs (y # ys)) = merge_wrt r2 (map f xs) (map f (y # ys)); \<lbrakk>x \<noteq> y; \<not> rel x y; f ` set (x # xs) \<inter> f ` set ys = {}; \<And>xa y. \<lbrakk>xa \<in> set (x # xs); y \<in> set ys\<rbrakk> \<Longrightarrow> r2 (f xa) (f y) = rel xa y\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) ys) = merge_wrt r2 (map f (x # xs)) (map f ys); f ` set (x # xs) \<inter> f ` set (y # ys) = {}; \<And>xa ya. \<lbrakk>xa \<in> set (x # xs); ya \<in> set (y # ys)\<rbrakk> \<Longrightarrow> r2 (f xa) (f ya) = rel xa ya\<rbrakk> \<Longrightarrow> map f (merge_wrt rel (x # xs) (y # ys)) = merge_wrt r2 (map f (x # xs)) (map f (y # ys))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map f (merge_wrt r1 (x # xs) (y # ys)) = merge_wrt r2 (map f (x # xs)) (map f (y # ys))
[PROOF STEP]
by (simp add: eq2 eq3 eq4 \<open>f x \<noteq> f y\<close> \<open>x \<noteq> y\<close>)
[PROOF STATE]
proof (state)
this:
map f (merge_wrt r1 (x # xs) (y # ys)) = merge_wrt r2 (map f (x # xs)) (map f (y # ys))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma domI:
  assumes "\<not> Q x \<Longrightarrow> dom (h x)"
  shows "dom x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dom x
[PROOF STEP]
proof (cases "Q x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Q x \<Longrightarrow> local.dom x
 2. \<not> Q x \<Longrightarrow> local.dom x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Q x

goal (2 subgoals):
 1. Q x \<Longrightarrow> local.dom x
 2. \<not> Q x \<Longrightarrow> local.dom x
[PROOF STEP]
hence "Q ((h ^^ 0) x)"
[PROOF STATE]
proof (prove)
using this:
Q x

goal (1 subgoal):
 1. Q ((h ^^ 0) x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Q ((h ^^ 0) x)

goal (2 subgoals):
 1. Q x \<Longrightarrow> local.dom x
 2. \<not> Q x \<Longrightarrow> local.dom x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Q ((h ^^ 0) x)

goal (1 subgoal):
 1. local.dom x
[PROOF STEP]
unfolding dom_def
[PROOF STATE]
proof (prove)
using this:
Q ((h ^^ 0) x)

goal (1 subgoal):
 1. \<exists>k. Q ((h ^^ k) x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
local.dom x

goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> local.dom x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> local.dom x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> Q x

goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> local.dom x
[PROOF STEP]
hence "dom (h x)"
[PROOF STATE]
proof (prove)
using this:
\<not> Q x

goal (1 subgoal):
 1. local.dom (h x)
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
this:
local.dom (h x)

goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> local.dom x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.dom (h x)
[PROOF STEP]
obtain k where "Q ((h ^^ k) (h x))"
[PROOF STATE]
proof (prove)
using this:
local.dom (h x)

goal (1 subgoal):
 1. (\<And>k. Q ((h ^^ k) (h x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dom_def
[PROOF STATE]
proof (prove)
using this:
\<exists>k. Q ((h ^^ k) (h x))

goal (1 subgoal):
 1. (\<And>k. Q ((h ^^ k) (h x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Q ((h ^^ k) (h x))

goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> local.dom x
[PROOF STEP]
hence "Q ((h ^^ (Suc k)) x)"
[PROOF STATE]
proof (prove)
using this:
Q ((h ^^ k) (h x))

goal (1 subgoal):
 1. Q ((h ^^ Suc k) x)
[PROOF STEP]
by (simp add: funpow_swap1)
[PROOF STATE]
proof (state)
this:
Q ((h ^^ Suc k) x)

goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> local.dom x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Q ((h ^^ Suc k) x)

goal (1 subgoal):
 1. local.dom x
[PROOF STEP]
unfolding dom_def
[PROOF STATE]
proof (prove)
using this:
Q ((h ^^ Suc k) x)

goal (1 subgoal):
 1. \<exists>k. Q ((h ^^ k) x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
local.dom x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma domD:
  assumes "dom x" and "\<not> Q x"
  shows "dom (h x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dom (h x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.dom (h x)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
local.dom x
[PROOF STEP]
obtain k where *: "Q ((h ^^ k) x)"
[PROOF STATE]
proof (prove)
using this:
local.dom x

goal (1 subgoal):
 1. (\<And>k. Q ((h ^^ k) x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dom_def
[PROOF STATE]
proof (prove)
using this:
\<exists>k. Q ((h ^^ k) x)

goal (1 subgoal):
 1. (\<And>k. Q ((h ^^ k) x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Q ((h ^^ k) x)

goal (1 subgoal):
 1. local.dom (h x)
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<not> Q x
Q ((h ^^ k) x)
[PROOF STEP]
have "k \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> Q x
Q ((h ^^ k) x)

goal (1 subgoal):
 1. k \<noteq> 0
[PROOF STEP]
using funpow_0
[PROOF STATE]
proof (prove)
using this:
\<not> Q x
Q ((h ^^ k) x)
(?f ^^ 0) ?x = ?x

goal (1 subgoal):
 1. k \<noteq> 0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
k \<noteq> 0

goal (1 subgoal):
 1. local.dom (h x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<noteq> 0
[PROOF STEP]
obtain m where "k = Suc m"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0

goal (1 subgoal):
 1. (\<And>m. k = Suc m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using nat.exhaust
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
\<lbrakk>?y = 0 \<Longrightarrow> ?P; \<And>x2. ?y = Suc x2 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>m. k = Suc m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k = Suc m

goal (1 subgoal):
 1. local.dom (h x)
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
Q ((h ^^ k) x)
k = Suc m
[PROOF STEP]
have "Q ((h ^^ m) (h x))"
[PROOF STATE]
proof (prove)
using this:
Q ((h ^^ k) x)
k = Suc m

goal (1 subgoal):
 1. Q ((h ^^ m) (h x))
[PROOF STEP]
by (simp add: funpow_swap1)
[PROOF STATE]
proof (state)
this:
Q ((h ^^ m) (h x))

goal (1 subgoal):
 1. local.dom (h x)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Q ((h ^^ m) (h x))

goal (1 subgoal):
 1. local.dom (h x)
[PROOF STEP]
unfolding dom_def
[PROOF STATE]
proof (prove)
using this:
Q ((h ^^ m) (h x))

goal (1 subgoal):
 1. \<exists>k. Q ((h ^^ k) (h x))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
local.dom (h x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma recfun_aux_domI:
  assumes "dom x"
  shows "recfun_aux_dom x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfun_aux_dom x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. recfun_aux_dom x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
local.dom x
[PROOF STEP]
obtain k where "Q ((h ^^ k) x)"
[PROOF STATE]
proof (prove)
using this:
local.dom x

goal (1 subgoal):
 1. (\<And>k. Q ((h ^^ k) x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dom_def
[PROOF STATE]
proof (prove)
using this:
\<exists>k. Q ((h ^^ k) x)

goal (1 subgoal):
 1. (\<And>k. Q ((h ^^ k) x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Q ((h ^^ k) x)

goal (1 subgoal):
 1. recfun_aux_dom x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Q ((h ^^ k) x)

goal (1 subgoal):
 1. recfun_aux_dom x
[PROOF STEP]
proof (induct k arbitrary: x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. Q ((h ^^ 0) x) \<Longrightarrow> recfun_aux_dom x
 2. \<And>k x. \<lbrakk>\<And>x. Q ((h ^^ k) x) \<Longrightarrow> recfun_aux_dom x; Q ((h ^^ Suc k) x)\<rbrakk> \<Longrightarrow> recfun_aux_dom x
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
Q ((h ^^ 0) x)

goal (2 subgoals):
 1. \<And>x. Q ((h ^^ 0) x) \<Longrightarrow> recfun_aux_dom x
 2. \<And>k x. \<lbrakk>\<And>x. Q ((h ^^ k) x) \<Longrightarrow> recfun_aux_dom x; Q ((h ^^ Suc k) x)\<rbrakk> \<Longrightarrow> recfun_aux_dom x
[PROOF STEP]
hence "Q x"
[PROOF STATE]
proof (prove)
using this:
Q ((h ^^ 0) x)

goal (1 subgoal):
 1. Q x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Q x

goal (2 subgoals):
 1. \<And>x. Q ((h ^^ 0) x) \<Longrightarrow> recfun_aux_dom x
 2. \<And>k x. \<lbrakk>\<And>x. Q ((h ^^ k) x) \<Longrightarrow> recfun_aux_dom x; Q ((h ^^ Suc k) x)\<rbrakk> \<Longrightarrow> recfun_aux_dom x
[PROOF STEP]
with recfun_aux.domintros
[PROOF STATE]
proof (chain)
picking this:
(\<not> Q ?x \<Longrightarrow> recfun_aux_dom (h ?x)) \<Longrightarrow> recfun_aux_dom ?x
Q x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<not> Q ?x \<Longrightarrow> recfun_aux_dom (h ?x)) \<Longrightarrow> recfun_aux_dom ?x
Q x

goal (1 subgoal):
 1. recfun_aux_dom x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
recfun_aux_dom x

goal (1 subgoal):
 1. \<And>k x. \<lbrakk>\<And>x. Q ((h ^^ k) x) \<Longrightarrow> recfun_aux_dom x; Q ((h ^^ Suc k) x)\<rbrakk> \<Longrightarrow> recfun_aux_dom x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k x. \<lbrakk>\<And>x. Q ((h ^^ k) x) \<Longrightarrow> recfun_aux_dom x; Q ((h ^^ Suc k) x)\<rbrakk> \<Longrightarrow> recfun_aux_dom x
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
Q ((h ^^ k) ?x) \<Longrightarrow> recfun_aux_dom ?x
Q ((h ^^ Suc k) x)

goal (1 subgoal):
 1. \<And>k x. \<lbrakk>\<And>x. Q ((h ^^ k) x) \<Longrightarrow> recfun_aux_dom x; Q ((h ^^ Suc k) x)\<rbrakk> \<Longrightarrow> recfun_aux_dom x
[PROOF STEP]
from Suc(2)
[PROOF STATE]
proof (chain)
picking this:
Q ((h ^^ Suc k) x)
[PROOF STEP]
have "Q ((h ^^ k) (h x))"
[PROOF STATE]
proof (prove)
using this:
Q ((h ^^ Suc k) x)

goal (1 subgoal):
 1. Q ((h ^^ k) (h x))
[PROOF STEP]
by (simp add: funpow_swap1)
[PROOF STATE]
proof (state)
this:
Q ((h ^^ k) (h x))

goal (1 subgoal):
 1. \<And>k x. \<lbrakk>\<And>x. Q ((h ^^ k) x) \<Longrightarrow> recfun_aux_dom x; Q ((h ^^ Suc k) x)\<rbrakk> \<Longrightarrow> recfun_aux_dom x
[PROOF STEP]
hence "recfun_aux_dom (h x)"
[PROOF STATE]
proof (prove)
using this:
Q ((h ^^ k) (h x))

goal (1 subgoal):
 1. recfun_aux_dom (h x)
[PROOF STEP]
by (rule Suc(1))
[PROOF STATE]
proof (state)
this:
recfun_aux_dom (h x)

goal (1 subgoal):
 1. \<And>k x. \<lbrakk>\<And>x. Q ((h ^^ k) x) \<Longrightarrow> recfun_aux_dom x; Q ((h ^^ Suc k) x)\<rbrakk> \<Longrightarrow> recfun_aux_dom x
[PROOF STEP]
with recfun_aux.domintros
[PROOF STATE]
proof (chain)
picking this:
(\<not> Q ?x \<Longrightarrow> recfun_aux_dom (h ?x)) \<Longrightarrow> recfun_aux_dom ?x
recfun_aux_dom (h x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<not> Q ?x \<Longrightarrow> recfun_aux_dom (h ?x)) \<Longrightarrow> recfun_aux_dom ?x
recfun_aux_dom (h x)

goal (1 subgoal):
 1. recfun_aux_dom x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
recfun_aux_dom x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
recfun_aux_dom x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma recfun_aux_domD:
  assumes "recfun_aux_dom x"
  shows "dom x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dom x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
recfun_aux_dom x

goal (1 subgoal):
 1. local.dom x
[PROOF STEP]
proof (induct x rule: recfun_aux.pinduct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>recfun_aux_dom x; \<not> Q x \<Longrightarrow> local.dom (h x)\<rbrakk> \<Longrightarrow> local.dom x
[PROOF STEP]
case (1 x)
[PROOF STATE]
proof (state)
this:
recfun_aux_dom x
\<not> Q x \<Longrightarrow> local.dom (h x)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>recfun_aux_dom x; \<not> Q x \<Longrightarrow> local.dom (h x)\<rbrakk> \<Longrightarrow> local.dom x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dom x
[PROOF STEP]
proof (cases "Q x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Q x \<Longrightarrow> local.dom x
 2. \<not> Q x \<Longrightarrow> local.dom x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Q x

goal (2 subgoals):
 1. Q x \<Longrightarrow> local.dom x
 2. \<not> Q x \<Longrightarrow> local.dom x
[PROOF STEP]
with domI
[PROOF STATE]
proof (chain)
picking this:
(\<not> Q ?x \<Longrightarrow> local.dom (h ?x)) \<Longrightarrow> local.dom ?x
Q x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<not> Q ?x \<Longrightarrow> local.dom (h ?x)) \<Longrightarrow> local.dom ?x
Q x

goal (1 subgoal):
 1. local.dom x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
local.dom x

goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> local.dom x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> local.dom x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> Q x

goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> local.dom x
[PROOF STEP]
hence "dom (h x)"
[PROOF STATE]
proof (prove)
using this:
\<not> Q x

goal (1 subgoal):
 1. local.dom (h x)
[PROOF STEP]
by (rule 1(2))
[PROOF STATE]
proof (state)
this:
local.dom (h x)

goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> local.dom x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
local.dom (h x)

goal (1 subgoal):
 1. local.dom x
[PROOF STEP]
using domI
[PROOF STATE]
proof (prove)
using this:
local.dom (h x)
(\<not> Q ?x \<Longrightarrow> local.dom (h ?x)) \<Longrightarrow> local.dom ?x

goal (1 subgoal):
 1. local.dom x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
local.dom x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.dom x

goal:
No subgoals!
[PROOF STEP]
qed