[STATEMENT]
lemma right_unique_rel_set_lemma:
  assumes "right_unique R" and "rel_set R X Y"
  obtains f where "Y = image f X" and "\<forall>x\<in>X. R x (f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R x (?f2 x)
[PROOF STEP]
define f where "f x = (THE y. R x y)" for x
[PROOF STATE]
proof (state)
this:
f ?x = (THE y. R ?x y)

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R x (?f2 x)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
f ?x = (THE y. R ?x y)

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R x (?f2 x)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R x (?f2 x)
[PROOF STEP]
assume "x \<in> X"
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R x (?f2 x)
[PROOF STEP]
with \<open>rel_set R X Y\<close> \<open>right_unique R\<close>
[PROOF STATE]
proof (chain)
picking this:
rel_set R X Y
right_unique R
x \<in> X
[PROOF STEP]
have "R x (f x)"
[PROOF STATE]
proof (prove)
using this:
rel_set R X Y
right_unique R
x \<in> X

goal (1 subgoal):
 1. R x (f x)
[PROOF STEP]
by (simp add: right_unique_def rel_set_def f_def) (metis theI)
[PROOF STATE]
proof (state)
this:
R x (f x)

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R x (?f2 x)
[PROOF STEP]
with assms \<open>x \<in> X\<close>
[PROOF STATE]
proof (chain)
picking this:
right_unique R
rel_set R X Y
x \<in> X
R x (f x)
[PROOF STEP]
have  "R x (f x)" "f x \<in> Y"
[PROOF STATE]
proof (prove)
using this:
right_unique R
rel_set R X Y
x \<in> X
R x (f x)

goal (1 subgoal):
 1. R x (f x) &&& f x \<in> Y
[PROOF STEP]
by (fastforce simp add: right_unique_def rel_set_def)+
[PROOF STATE]
proof (state)
this:
R x (f x)
f x \<in> Y

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R x (?f2 x)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> X \<Longrightarrow> R ?x2 (f ?x2)
?x2 \<in> X \<Longrightarrow> f ?x2 \<in> Y

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R x (?f2 x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x2 \<in> X \<Longrightarrow> R ?x2 (f ?x2)
?x2 \<in> X \<Longrightarrow> f ?x2 \<in> Y

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R x (?f2 x)
[PROOF STEP]
have "\<exists>x\<in>X. y = f x" if "y \<in> Y" for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>X. y = f x
[PROOF STEP]
using \<open>rel_set R X Y\<close> that
[PROOF STATE]
proof (prove)
using this:
rel_set R X Y
y \<in> Y

goal (1 subgoal):
 1. \<exists>x\<in>X. y = f x
[PROOF STEP]
by(auto simp add: f_def dest!: rel_setD2 dest: right_uniqueD[OF \<open>right_unique R\<close>]
        intro: the_equality[symmetric])
[PROOF STATE]
proof (state)
this:
?y \<in> Y \<Longrightarrow> \<exists>x\<in>X. ?y = f x

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R x (f x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R x (?f2 x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?x2 \<in> X \<Longrightarrow> R ?x2 (f ?x2)
?x2 \<in> X \<Longrightarrow> f ?x2 \<in> Y
?y \<in> Y \<Longrightarrow> \<exists>x\<in>X. ?y = f x
[PROOF STEP]
show "\<forall>x\<in>X. R x (f x)" "Y = image f X"
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> X \<Longrightarrow> R ?x2 (f ?x2)
?x2 \<in> X \<Longrightarrow> f ?x2 \<in> Y
?y \<in> Y \<Longrightarrow> \<exists>x\<in>X. ?y = f x

goal (1 subgoal):
 1. \<forall>x\<in>X. R x (f x) &&& Y = f ` X
[PROOF STEP]
by (auto simp: inj_on_def image_iff)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>X. R x (f x)
Y = f ` X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma left_unique_rel_set_lemma:
  assumes "left_unique R" and "rel_set R Y X"
  obtains f where "Y = image f X" and "\<forall>x\<in>X. R (f x) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R (?f2 x) x
[PROOF STEP]
define f where "f x = (THE y. R y x)" for x
[PROOF STATE]
proof (state)
this:
f ?x = (THE y. R y ?x)

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R (?f2 x) x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
f ?x = (THE y. R y ?x)

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R (?f2 x) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R (?f2 x) x
[PROOF STEP]
assume "x \<in> X"
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R (?f2 x) x
[PROOF STEP]
with \<open>rel_set R Y X\<close> \<open>left_unique R\<close>
[PROOF STATE]
proof (chain)
picking this:
rel_set R Y X
left_unique R
x \<in> X
[PROOF STEP]
have "R (f x) x"
[PROOF STATE]
proof (prove)
using this:
rel_set R Y X
left_unique R
x \<in> X

goal (1 subgoal):
 1. R (f x) x
[PROOF STEP]
by (simp add: left_unique_def rel_set_def f_def)  (metis theI)
[PROOF STATE]
proof (state)
this:
R (f x) x

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R (?f2 x) x
[PROOF STEP]
with assms \<open>x \<in> X\<close>
[PROOF STATE]
proof (chain)
picking this:
left_unique R
rel_set R Y X
x \<in> X
R (f x) x
[PROOF STEP]
have  "R (f x) x" "f x \<in> Y"
[PROOF STATE]
proof (prove)
using this:
left_unique R
rel_set R Y X
x \<in> X
R (f x) x

goal (1 subgoal):
 1. R (f x) x &&& f x \<in> Y
[PROOF STEP]
by (fastforce simp add: left_unique_def rel_set_def)+
[PROOF STATE]
proof (state)
this:
R (f x) x
f x \<in> Y

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R (?f2 x) x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 \<in> X \<Longrightarrow> R (f ?x2) ?x2
?x2 \<in> X \<Longrightarrow> f ?x2 \<in> Y

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R (?f2 x) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x2 \<in> X \<Longrightarrow> R (f ?x2) ?x2
?x2 \<in> X \<Longrightarrow> f ?x2 \<in> Y

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R (?f2 x) x
[PROOF STEP]
have "\<exists>x\<in>X. y = f x" if "y \<in> Y" for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>X. y = f x
[PROOF STEP]
using \<open>rel_set R Y X\<close> that
[PROOF STATE]
proof (prove)
using this:
rel_set R Y X
y \<in> Y

goal (1 subgoal):
 1. \<exists>x\<in>X. y = f x
[PROOF STEP]
by(auto simp add: f_def dest!: rel_setD1 dest: left_uniqueD[OF \<open>left_unique R\<close>]
        intro: the_equality[symmetric])
[PROOF STATE]
proof (state)
this:
?y \<in> Y \<Longrightarrow> \<exists>x\<in>X. ?y = f x

goal (2 subgoals):
 1. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> Y = ?f2 ` X
 2. (\<And>f. \<lbrakk>Y = f ` X; \<forall>x\<in>X. R (f x) x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> \<forall>x\<in>X. R (?f2 x) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?x2 \<in> X \<Longrightarrow> R (f ?x2) ?x2
?x2 \<in> X \<Longrightarrow> f ?x2 \<in> Y
?y \<in> Y \<Longrightarrow> \<exists>x\<in>X. ?y = f x
[PROOF STEP]
show "\<forall>x\<in>X. R (f x) x" "Y = image f X"
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> X \<Longrightarrow> R (f ?x2) ?x2
?x2 \<in> X \<Longrightarrow> f ?x2 \<in> Y
?y \<in> Y \<Longrightarrow> \<exists>x\<in>X. ?y = f x

goal (1 subgoal):
 1. \<forall>x\<in>X. R (f x) x &&& Y = f ` X
[PROOF STEP]
by (auto simp: inj_on_def image_iff)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>X. R (f x) x
Y = f ` X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma neg_distr_cond_bset_right_unique:
  "right_unique C \<Longrightarrow> neg_distr_cond_bset C D tytok"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. right_unique C \<Longrightarrow> neg_distr_cond_bset C D tytok
[PROOF STEP]
unfolding neg_distr_cond_bset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. right_unique C \<Longrightarrow> rel_bset (C OO D) \<le> rel_bset C OO rel_bset D
[PROOF STEP]
apply(rule predicate2I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>right_unique C; rel_bset (C OO D) x y\<rbrakk> \<Longrightarrow> (rel_bset C OO rel_bset D) x y
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y C D. \<lbrakk>finite x \<and> card x \<le> CARD('d); finite y \<and> card y \<le> CARD('d); right_unique C; rel_set (C OO D) x y\<rbrakk> \<Longrightarrow> \<exists>ya\<in>{A. finite A \<and> card A \<le> CARD('d)}. rel_set C x ya \<and> rel_set D ya y
[PROOF STEP]
apply(auto 6 2 intro: card_image_le[THEN order_trans] elim: right_unique_rel_set_lemma
      simp add: rel_set_OO[symmetric])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma neg_distr_cond_bset_left_unique:
  "left_unique D \<Longrightarrow> neg_distr_cond_bset C D tytok"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left_unique D \<Longrightarrow> neg_distr_cond_bset C D tytok
[PROOF STEP]
unfolding neg_distr_cond_bset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left_unique D \<Longrightarrow> rel_bset (C OO D) \<le> rel_bset C OO rel_bset D
[PROOF STEP]
apply(rule predicate2I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>left_unique D; rel_bset (C OO D) x y\<rbrakk> \<Longrightarrow> (rel_bset C OO rel_bset D) x y
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y D C. \<lbrakk>finite x \<and> card x \<le> CARD('d); finite y \<and> card y \<le> CARD('d); left_unique D; rel_set (C OO D) x y\<rbrakk> \<Longrightarrow> \<exists>ya\<in>{A. finite A \<and> card A \<le> CARD('d)}. rel_set C x ya \<and> rel_set D ya y
[PROOF STEP]
apply(auto 6 2 intro: card_image_le[THEN order_trans] elim: left_unique_rel_set_lemma
      simp add: rel_set_OO[symmetric])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma neg_distr_cond_bset_eq: "neg_distr_cond_bset (=) (=) tytok"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neg_distr_cond_bset (=) (=) tytok
[PROOF STEP]
by (intro neg_distr_cond_bset_right_unique right_unique_eq)


[STATEMENT]
lemma rel_pred_mono: "A' \<le> A \<Longrightarrow> rel_pred A \<le> rel_pred A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' \<le> A \<Longrightarrow> rel_pred A \<le> rel_pred A'
[PROOF STEP]
unfolding rel_pred_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' \<le> A \<Longrightarrow> A ===> (=) \<le> A' ===> (=)
[PROOF STEP]
by(auto elim!: rel_fun_mono)


[STATEMENT]
lemma rel_pred_eq: "rel_pred (=) = (=)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pred (=) = (=)
[PROOF STEP]
by(simp add: rel_pred_def rel_fun_eq)


[STATEMENT]
lemma rel_pred_conversep: "rel_pred A\<inverse>\<inverse> = (rel_pred A)\<inverse>\<inverse>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pred A\<inverse>\<inverse> = (rel_pred A)\<inverse>\<inverse>
[PROOF STEP]
using rel_fun_conversep[of _ "(=)"]
[PROOF STATE]
proof (prove)
using this:
?A\<inverse>\<inverse> ===> (=)\<inverse>\<inverse> = (?A ===> (=))\<inverse>\<inverse>

goal (1 subgoal):
 1. rel_pred A\<inverse>\<inverse> = (rel_pred A)\<inverse>\<inverse>
[PROOF STEP]
by (simp add: rel_pred_def)


[STATEMENT]
lemma map_pred_id0: "map_pred id = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pred id = id
[PROOF STEP]
by (simp add: map_pred_def map_fun_id)


[STATEMENT]
lemma map_pred_comp: "map_pred f \<circ> map_pred g = map_pred (g \<circ> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pred f \<circ> map_pred g = map_pred (g \<circ> f)
[PROOF STEP]
using map_fun_comp[where g=id and g'=id]
[PROOF STATE]
proof (prove)
using this:
?f ---> id \<circ> (?f' ---> id) = (?f' \<circ> ?f) ---> id \<circ> id

goal (1 subgoal):
 1. map_pred f \<circ> map_pred g = map_pred (g \<circ> f)
[PROOF STEP]
by (simp add: map_pred_def)


[STATEMENT]
lemma map_pred_parametric: "((A' ===> A) ===> rel_pred A ===> rel_pred A') map_pred map_pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A' ===> A) ===> rel_pred A ===> rel_pred A') map_pred map_pred
[PROOF STEP]
by (simp add: rel_fun_def rel_pred_def map_pred_def)


[STATEMENT]
lemma rel_pred_pos_distr_iff [simp]: "rel_pred_pos_distr_cond A B = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pred_pos_distr_cond A B = True
[PROOF STEP]
unfolding rel_pred_pos_distr_cond_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_pred A OO rel_pred B \<le> rel_pred (A OO B)) = True
[PROOF STEP]
by (auto simp add: rel_pred_def rel_fun_def)


[STATEMENT]
lemma neg_fun_distr3:
  assumes 1: "left_unique R" "right_total R"
    and 2: "right_unique S" "left_total S"
  shows "rel_fun (R OO R') (S OO S') \<le> rel_fun R S OO rel_fun R' S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R OO R' ===> S OO S' \<le> (R ===> S) OO (R' ===> S')
[PROOF STEP]
using functional_converse_relation[OF 1] functional_relation[OF 2]
[PROOF STATE]
proof (prove)
using this:
\<forall>y. \<exists>!x. R x y
\<forall>x. \<exists>!y. S x y

goal (1 subgoal):
 1. R OO R' ===> S OO S' \<le> (R ===> S) OO (R' ===> S')
[PROOF STEP]
unfolding rel_fun_def OO_def
[PROOF STATE]
proof (prove)
using this:
\<forall>y. \<exists>!x. R x y
\<forall>x. \<exists>!y. S x y

goal (1 subgoal):
 1. (\<lambda>f g. \<forall>x y. (\<exists>ya. R x ya \<and> R' ya y) \<longrightarrow> (\<exists>ya. S (f x) ya \<and> S' ya (g y))) \<le> (\<lambda>x z. \<exists>y. (\<forall>xa ya. R xa ya \<longrightarrow> S (x xa) (y ya)) \<and> (\<forall>x ya. R' x ya \<longrightarrow> S' (y x) (z ya)))
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>y. \<exists>!x. R x y; \<forall>x. \<exists>!y. S x y; \<forall>xa ya. (\<exists>y. R xa y \<and> R' y ya) \<longrightarrow> (\<exists>yb. S (x xa) yb \<and> S' yb (y ya))\<rbrakk> \<Longrightarrow> \<exists>ya. (\<forall>xa y. R xa y \<longrightarrow> S (x xa) (ya y)) \<and> (\<forall>x yb. R' x yb \<longrightarrow> S' (ya x) (y yb))
[PROOF STEP]
apply (subst all_comm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>y. \<exists>!x. R x y; \<forall>x. \<exists>!y. S x y; \<forall>xa ya. (\<exists>y. R xa y \<and> R' y ya) \<longrightarrow> (\<exists>yb. S (x xa) yb \<and> S' yb (y ya))\<rbrakk> \<Longrightarrow> \<exists>ya. (\<forall>y xa. R xa y \<longrightarrow> S (x xa) (ya y)) \<and> (\<forall>x yb. R' x yb \<longrightarrow> S' (ya x) (y yb))
[PROOF STEP]
apply (subst all_conj_distrib[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>y. \<exists>!x. R x y; \<forall>x. \<exists>!y. S x y; \<forall>xa ya. (\<exists>y. R xa y \<and> R' y ya) \<longrightarrow> (\<exists>yb. S (x xa) yb \<and> S' yb (y ya))\<rbrakk> \<Longrightarrow> \<exists>ya. \<forall>xa. (\<forall>xb. R xb xa \<longrightarrow> S (x xb) (ya xa)) \<and> (\<forall>yb. R' xa yb \<longrightarrow> S' (ya xa) (y yb))
[PROOF STEP]
apply (intro choice)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>y. \<exists>!x. R x y; \<forall>x. \<exists>!y. S x y; \<forall>xa ya. (\<exists>y. R xa y \<and> R' y ya) \<longrightarrow> (\<exists>yb. S (x xa) yb \<and> S' yb (y ya))\<rbrakk> \<Longrightarrow> \<forall>xa. \<exists>ya. (\<forall>xb. R xb xa \<longrightarrow> S (x xb) ya) \<and> (\<forall>yb. R' xa yb \<longrightarrow> S' ya (y yb))
[PROOF STEP]
by metis


[STATEMENT]
lemma rel_pred_neg_distr_imp:
  "right_unique B \<and> left_total B \<or> left_unique A \<and> right_total A \<Longrightarrow> rel_pred_neg_distr_cond A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. right_unique B \<and> left_total B \<or> left_unique A \<and> right_total A \<Longrightarrow> rel_pred_neg_distr_cond A B
[PROOF STEP]
unfolding rel_pred_neg_distr_cond_def rel_pred_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. right_unique B \<and> left_total B \<or> left_unique A \<and> right_total A \<Longrightarrow> A OO B ===> (=) \<le> (A ===> (=)) OO (B ===> (=))
[PROOF STEP]
apply(clarsimp simp add: vimage2p_def rel_pred_neg_distr_cond_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>right_unique B \<and> left_total B \<or> left_unique A \<and> right_total A; (A OO B ===> (=)) x y\<rbrakk> \<Longrightarrow> ((A ===> (=)) OO (B ===> (=))) x y
[PROOF STEP]
apply(rewrite in "rel_fun _ \<hole>" in asm eq_OO[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>right_unique B \<and> left_total B \<or> left_unique A \<and> right_total A; (A OO B ===> (=) OO (=)) x y\<rbrakk> \<Longrightarrow> ((A ===> (=)) OO (B ===> (=))) x y
[PROOF STEP]
apply(elim disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>(A OO B ===> (=) OO (=)) x y; right_unique B \<and> left_total B\<rbrakk> \<Longrightarrow> ((A ===> (=)) OO (B ===> (=))) x y
 2. \<And>x y. \<lbrakk>(A OO B ===> (=) OO (=)) x y; left_unique A \<and> right_total A\<rbrakk> \<Longrightarrow> ((A ===> (=)) OO (B ===> (=))) x y
[PROOF STEP]
apply(drule neg_fun_distr2[THEN predicate2D, rotated -1];
      (simp add: left_unique_eq right_unique_eq left_total_eq right_total_eq)?)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(A OO B ===> (=) OO (=)) x y; left_unique A \<and> right_total A\<rbrakk> \<Longrightarrow> ((A ===> (=)) OO (B ===> (=))) x y
[PROOF STEP]
apply(drule neg_fun_distr3[THEN predicate2D, rotated -1];
      (simp add: left_unique_eq right_unique_eq left_total_eq right_total_eq)?)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rel_pred_neg_distr_cond_eq: "rel_pred_neg_distr_cond (=) (=)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pred_neg_distr_cond (=) (=)
[PROOF STEP]
by(blast intro: rel_pred_neg_distr_imp left_unique_eq right_total_eq)


[STATEMENT]
lemma left_unique_rel_pred: "left_total A \<Longrightarrow> left_unique (rel_pred A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left_total A \<Longrightarrow> left_unique (rel_pred A)
[PROOF STEP]
unfolding rel_pred_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left_total A \<Longrightarrow> left_unique (A ===> (=))
[PROOF STEP]
by (erule left_unique_fun) (rule left_unique_eq)


[STATEMENT]
lemma right_unique_rel_pred: "right_total A \<Longrightarrow> right_unique (rel_pred A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. right_total A \<Longrightarrow> right_unique (rel_pred A)
[PROOF STEP]
unfolding rel_pred_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. right_total A \<Longrightarrow> right_unique (A ===> (=))
[PROOF STEP]
by (erule right_unique_fun) (rule right_unique_eq)


[STATEMENT]
lemma right_total_rel_pred: "right_unique A \<Longrightarrow> right_total (rel_pred A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. right_unique A \<Longrightarrow> right_total (rel_pred A)
[PROOF STEP]
unfolding rel_pred_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. right_unique A \<Longrightarrow> right_total (A ===> (=))
[PROOF STEP]
by (erule right_total_fun) (rule right_total_eq)


[STATEMENT]
lemma map_filter_closed:
  includes lifting_syntax
  assumes "is_filter F"
  shows "is_filter (((f ---> id) ---> id) F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_filter (((f ---> id) ---> id) F)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_filter (((f ---> id) ---> id) F)
[PROOF STEP]
define F' where "F' = Abs_filter F"
[PROOF STATE]
proof (state)
this:
F' = Abs_filter F

goal (1 subgoal):
 1. is_filter (((f ---> id) ---> id) F)
[PROOF STEP]
have "is_filter (((f ---> id) ---> id) (\<lambda>P. eventually P F'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_filter (((f ---> id) ---> id) (\<lambda>P. eventually P F'))
[PROOF STEP]
by (rule is_filter.intro)(auto elim!: eventually_rev_mp simp add: map_fun_def o_def)
[PROOF STATE]
proof (state)
this:
is_filter (((f ---> id) ---> id) (\<lambda>P. eventually P F'))

goal (1 subgoal):
 1. is_filter (((f ---> id) ---> id) F)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_filter (((f ---> id) ---> id) (\<lambda>P. eventually P F'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_filter (((f ---> id) ---> id) (\<lambda>P. eventually P F'))

goal (1 subgoal):
 1. is_filter (((f ---> id) ---> id) F)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_filter (((f ---> id) ---> id) (\<lambda>P. eventually P F'))
is_filter F

goal (1 subgoal):
 1. is_filter (((f ---> id) ---> id) F)
[PROOF STEP]
by(simp add: F'_def eventually_Abs_filter)
[PROOF STATE]
proof (state)
this:
is_filter (((f ---> id) ---> id) F)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_filter_neg_distr_cond'_stronger:
  assumes "rel_filter_neg_distr_cond' C C'"
  shows "rel_pred2_neg_distr_cond C C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pred2_neg_distr_cond C C'
[PROOF STEP]
unfolding rel_pred2_neg_distr_cond_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pred (rel_pred (C OO C')) \<le> rel_pred (rel_pred C) OO rel_pred (rel_pred C')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_pred (rel_pred (C OO C')) \<le> rel_pred (rel_pred C) OO rel_pred (rel_pred C')
[PROOF STEP]
have "rel_pred (rel_pred (C OO C')) \<le> rel_pred (rel_pred C OO rel_pred C')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pred (rel_pred (C OO C')) \<le> rel_pred (rel_pred C OO rel_pred C')
[PROOF STEP]
by (auto intro!: rel_pred_mono rel_pred_pos_distr)
[PROOF STATE]
proof (state)
this:
rel_pred (rel_pred (C OO C')) \<le> rel_pred (rel_pred C OO rel_pred C')

goal (1 subgoal):
 1. rel_pred (rel_pred (C OO C')) \<le> rel_pred (rel_pred C) OO rel_pred (rel_pred C')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rel_pred (rel_pred (C OO C')) \<le> rel_pred (rel_pred C OO rel_pred C')

goal (1 subgoal):
 1. rel_pred (rel_pred (C OO C')) \<le> rel_pred (rel_pred C) OO rel_pred (rel_pred C')
[PROOF STEP]
have "... \<le> rel_pred (rel_pred C) OO rel_pred (rel_pred C')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pred (rel_pred C OO rel_pred C') \<le> rel_pred (rel_pred C) OO rel_pred (rel_pred C')
[PROOF STEP]
apply (rule rel_pred_neg_distr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pred_neg_distr_cond (rel_pred C) (rel_pred C')
[PROOF STEP]
apply (rule rel_pred_neg_distr_imp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. right_unique (rel_pred C') \<and> left_total (rel_pred C') \<or> left_unique (rel_pred C) \<and> right_total (rel_pred C)
[PROOF STEP]
apply (insert assms[unfolded rel_filter_neg_distr_cond'_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left_total C \<and> right_unique C \<or> right_total C' \<and> left_unique C' \<Longrightarrow> right_unique (rel_pred C') \<and> left_total (rel_pred C') \<or> left_unique (rel_pred C) \<and> right_total (rel_pred C)
[PROOF STEP]
by (blast dest: left_unique_rel_pred right_total_rel_pred right_unique_rel_pred left_total_rel_pred)
[PROOF STATE]
proof (state)
this:
rel_pred (rel_pred C OO rel_pred C') \<le> rel_pred (rel_pred C) OO rel_pred (rel_pred C')

goal (1 subgoal):
 1. rel_pred (rel_pred (C OO C')) \<le> rel_pred (rel_pred C) OO rel_pred (rel_pred C')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rel_pred (rel_pred (C OO C')) \<le> rel_pred (rel_pred C) OO rel_pred (rel_pred C')
[PROOF STEP]
show "rel_pred (rel_pred (C OO C')) \<le> ..."
[PROOF STATE]
proof (prove)
using this:
rel_pred (rel_pred (C OO C')) \<le> rel_pred (rel_pred C) OO rel_pred (rel_pred C')

goal (1 subgoal):
 1. rel_pred (rel_pred (C OO C')) \<le> rel_pred (rel_pred C) OO rel_pred (rel_pred C')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
rel_pred (rel_pred (C OO C')) \<le> rel_pred (rel_pred C) OO rel_pred (rel_pred C')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_filter_neg_distr_cond'_eq: "rel_filter_neg_distr_cond' (=) (=)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_filter_neg_distr_cond' (=) (=)
[PROOF STEP]
unfolding rel_filter_neg_distr_cond'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left_total (=) \<and> right_unique (=) \<or> right_total (=) \<and> left_unique (=)
[PROOF STEP]
by (simp add: left_total_eq right_unique_eq)


[STATEMENT]
lemma is_filter_rel_witness:
  assumes F: "is_filter F" and G: "is_filter G"
    and FG: "rel_pred (rel_pred (C OO C')) F G"
    and cond: "rel_filter_neg_distr_cond' C C'"
  shows "is_filter (rel_pred2_witness C C' (F, G))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_filter (rel_pred2_witness C C' (F, G))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. rel_pred2_witness C C' (F, G) (\<lambda>x. True)
 2. \<And>P Q. \<lbrakk>rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 3. \<And>P Q. \<lbrakk>\<forall>x. P x \<longrightarrow> Q x; rel_pred2_witness C C' (F, G) P\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
let ?C = "rel_pred (rel_pred C)" and ?C' = "rel_pred (rel_pred C')"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. rel_pred2_witness C C' (F, G) (\<lambda>x. True)
 2. \<And>P Q. \<lbrakk>rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 3. \<And>P Q. \<lbrakk>\<forall>x. P x \<longrightarrow> Q x; rel_pred2_witness C C' (F, G) P\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
let ?wit = "rel_pred2_witness C C' (F, G)"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. rel_pred2_witness C C' (F, G) (\<lambda>x. True)
 2. \<And>P Q. \<lbrakk>rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 3. \<And>P Q. \<lbrakk>\<forall>x. P x \<longrightarrow> Q x; rel_pred2_witness C C' (F, G) P\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
have "rel_pred2_neg_distr_cond C C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pred2_neg_distr_cond C C'
[PROOF STEP]
using cond
[PROOF STATE]
proof (prove)
using this:
rel_filter_neg_distr_cond' C C'

goal (1 subgoal):
 1. rel_pred2_neg_distr_cond C C'
[PROOF STEP]
by (rule rel_filter_neg_distr_cond'_stronger)
[PROOF STATE]
proof (state)
this:
rel_pred2_neg_distr_cond C C'

goal (3 subgoals):
 1. rel_pred2_witness C C' (F, G) (\<lambda>x. True)
 2. \<And>P Q. \<lbrakk>rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 3. \<And>P Q. \<lbrakk>\<forall>x. P x \<longrightarrow> Q x; rel_pred2_witness C C' (F, G) P\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
with FG
[PROOF STATE]
proof (chain)
picking this:
rel_pred (rel_pred (C OO C')) F G
rel_pred2_neg_distr_cond C C'
[PROOF STEP]
have wit1: "?C F ?wit" and wit2: "?C' ?wit G"
[PROOF STATE]
proof (prove)
using this:
rel_pred (rel_pred (C OO C')) F G
rel_pred2_neg_distr_cond C C'

goal (1 subgoal):
 1. rel_pred (rel_pred C) F (rel_pred2_witness C C' (F, G)) &&& rel_pred (rel_pred C') (rel_pred2_witness C C' (F, G)) G
[PROOF STEP]
by (rule rel_pred2_witness[rotated])+
[PROOF STATE]
proof (state)
this:
rel_pred (rel_pred C) F (rel_pred2_witness C C' (F, G))
rel_pred (rel_pred C') (rel_pred2_witness C C' (F, G)) G

goal (3 subgoals):
 1. rel_pred2_witness C C' (F, G) (\<lambda>x. True)
 2. \<And>P Q. \<lbrakk>rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 3. \<And>P Q. \<lbrakk>\<forall>x. P x \<longrightarrow> Q x; rel_pred2_witness C C' (F, G) P\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
from wit1[unfolded rel_pred_def, THEN rel_funD, of "\<lambda>_. True" "\<lambda>_. True"] F
[PROOF STATE]
proof (chain)
picking this:
(C ===> (=)) (\<lambda>_. True) (\<lambda>_. True) \<Longrightarrow> F (\<lambda>_. True) = rel_pred2_witness C C' (F, G) (\<lambda>_. True)
is_filter F
[PROOF STEP]
show "?wit (\<lambda>_. True)"
[PROOF STATE]
proof (prove)
using this:
(C ===> (=)) (\<lambda>_. True) (\<lambda>_. True) \<Longrightarrow> F (\<lambda>_. True) = rel_pred2_witness C C' (F, G) (\<lambda>_. True)
is_filter F

goal (1 subgoal):
 1. rel_pred2_witness C C' (F, G) (\<lambda>_. True)
[PROOF STEP]
by (auto simp add: is_filter.True)
[PROOF STATE]
proof (state)
this:
rel_pred2_witness C C' (F, G) (\<lambda>_. True)

goal (2 subgoals):
 1. \<And>P Q. \<lbrakk>rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 2. \<And>P Q. \<lbrakk>\<forall>x. P x \<longrightarrow> Q x; rel_pred2_witness C C' (F, G) P\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
fix P Q
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q. \<lbrakk>rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 2. \<And>P Q. \<lbrakk>\<forall>x. P x \<longrightarrow> Q x; rel_pred2_witness C C' (F, G) P\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
have *: "(?wit P \<longrightarrow> ?wit Q \<longrightarrow> ?wit (\<lambda>x. P x \<and> Q x)) \<and> (?wit P \<longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<longrightarrow> ?wit Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_pred2_witness C C' (F, G) P \<longrightarrow> rel_pred2_witness C C' (F, G) Q \<longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)) \<and> (rel_pred2_witness C C' (F, G) P \<longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<longrightarrow> rel_pred2_witness C C' (F, G) Q)
[PROOF STEP]
using cond
[PROOF STATE]
proof (prove)
using this:
rel_filter_neg_distr_cond' C C'

goal (1 subgoal):
 1. (rel_pred2_witness C C' (F, G) P \<longrightarrow> rel_pred2_witness C C' (F, G) Q \<longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)) \<and> (rel_pred2_witness C C' (F, G) P \<longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<longrightarrow> rel_pred2_witness C C' (F, G) Q)
[PROOF STEP]
unfolding rel_filter_neg_distr_cond'_def
[PROOF STATE]
proof (prove)
using this:
left_total C \<and> right_unique C \<or> right_total C' \<and> left_unique C'

goal (1 subgoal):
 1. (rel_pred2_witness C C' (F, G) P \<longrightarrow> rel_pred2_witness C C' (F, G) Q \<longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)) \<and> (rel_pred2_witness C C' (F, G) P \<longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<longrightarrow> rel_pred2_witness C C' (F, G) Q)
[PROOF STEP]
proof(elim disjE conjE; use nothing in \<open>intro conjI strip\<close>)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>left_total C; right_unique C; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 2. \<lbrakk>left_total C; right_unique C; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
 3. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 4. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
assume "left_total C" "right_unique C"
[PROOF STATE]
proof (state)
this:
left_total C
right_unique C

goal (4 subgoals):
 1. \<lbrakk>left_total C; right_unique C; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 2. \<lbrakk>left_total C; right_unique C; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
 3. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 4. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
hence "left_unique (C ===> (=))" "right_total (C ===> (=))"
[PROOF STATE]
proof (prove)
using this:
left_total C
right_unique C

goal (1 subgoal):
 1. left_unique (C ===> (=)) &&& right_total (C ===> (=))
[PROOF STEP]
by(blast intro: left_unique_fun left_unique_eq right_total_fun right_total_eq)+
[PROOF STATE]
proof (state)
this:
left_unique (C ===> (=))
right_total (C ===> (=))

goal (4 subgoals):
 1. \<lbrakk>left_total C; right_unique C; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 2. \<lbrakk>left_total C; right_unique C; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
 3. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 4. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
from functional_converse_relation[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. \<exists>!x. (C ===> (=)) x y
[PROOF STEP]
obtain P' Q'
      where P' [transfer_rule]: "(C ===> (=)) P' P" and Q' [transfer_rule]: "(C ===> (=)) Q' Q"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. \<exists>!x. (C ===> (=)) x y

goal (1 subgoal):
 1. (\<And>P' Q'. \<lbrakk>(C ===> (=)) P' P; (C ===> (=)) Q' Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(C ===> (=)) P' P
(C ===> (=)) Q' Q

goal (4 subgoals):
 1. \<lbrakk>left_total C; right_unique C; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 2. \<lbrakk>left_total C; right_unique C; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
 3. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 4. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
have PQ: "(C ===> (=)) (\<lambda>x. P' x \<and> Q' x) (\<lambda>x. P x \<and> Q x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C ===> (=)) (\<lambda>x. P' x \<and> Q' x) (\<lambda>x. P x \<and> Q x)
[PROOF STEP]
by transfer_prover
[PROOF STATE]
proof (state)
this:
(C ===> (=)) (\<lambda>x. P' x \<and> Q' x) (\<lambda>x. P x \<and> Q x)

goal (4 subgoals):
 1. \<lbrakk>left_total C; right_unique C; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 2. \<lbrakk>left_total C; right_unique C; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
 3. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 4. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
with wit1 P' Q'
[PROOF STATE]
proof (chain)
picking this:
rel_pred (rel_pred C) F (rel_pred2_witness C C' (F, G))
(C ===> (=)) P' P
(C ===> (=)) Q' Q
(C ===> (=)) (\<lambda>x. P' x \<and> Q' x) (\<lambda>x. P x \<and> Q x)
[PROOF STEP]
have P: "?wit P \<longleftrightarrow> F P'" and Q: "?wit Q \<longleftrightarrow> F Q'"
      and PQ: "?wit (\<lambda>x. P x \<and> Q x) \<longleftrightarrow> F (\<lambda>x. P' x \<and> Q' x)"
[PROOF STATE]
proof (prove)
using this:
rel_pred (rel_pred C) F (rel_pred2_witness C C' (F, G))
(C ===> (=)) P' P
(C ===> (=)) Q' Q
(C ===> (=)) (\<lambda>x. P' x \<and> Q' x) (\<lambda>x. P x \<and> Q x)

goal (1 subgoal):
 1. rel_pred2_witness C C' (F, G) P = F P' &&& rel_pred2_witness C C' (F, G) Q = F Q' &&& rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x) = F (\<lambda>x. P' x \<and> Q' x)
[PROOF STEP]
by(auto dest: rel_funD simp add: rel_pred_def)
[PROOF STATE]
proof (state)
this:
rel_pred2_witness C C' (F, G) P = F P'
rel_pred2_witness C C' (F, G) Q = F Q'
rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x) = F (\<lambda>x. P' x \<and> Q' x)

goal (4 subgoals):
 1. \<lbrakk>left_total C; right_unique C; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 2. \<lbrakk>left_total C; right_unique C; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
 3. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 4. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
show "?wit (\<lambda>x. P x \<and> Q x)" if "?wit P" "?wit Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
[PROOF STEP]
using that P Q PQ
[PROOF STATE]
proof (prove)
using this:
rel_pred2_witness C C' (F, G) P
rel_pred2_witness C C' (F, G) Q
rel_pred2_witness C C' (F, G) P = F P'
rel_pred2_witness C C' (F, G) Q = F Q'
rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x) = F (\<lambda>x. P' x \<and> Q' x)

goal (1 subgoal):
 1. rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
[PROOF STEP]
by(auto intro: is_filter.conj[OF F])
[PROOF STATE]
proof (state)
this:
\<lbrakk>rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)

goal (3 subgoals):
 1. \<lbrakk>left_total C; right_unique C; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
 2. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 3. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
assume "\<forall>x. P x \<longrightarrow> Q x"
[PROOF STATE]
proof (state)
this:
\<forall>x. P x \<longrightarrow> Q x

goal (3 subgoals):
 1. \<lbrakk>left_total C; right_unique C; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
 2. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 3. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
with P' Q' \<open>left_total C\<close>
[PROOF STATE]
proof (chain)
picking this:
(C ===> (=)) P' P
(C ===> (=)) Q' Q
left_total C
\<forall>x. P x \<longrightarrow> Q x
[PROOF STEP]
have "\<forall>x. P' x \<longrightarrow> Q' x"
[PROOF STATE]
proof (prove)
using this:
(C ===> (=)) P' P
(C ===> (=)) Q' Q
left_total C
\<forall>x. P x \<longrightarrow> Q x

goal (1 subgoal):
 1. \<forall>x. P' x \<longrightarrow> Q' x
[PROOF STEP]
by(metis (full_types) apply_rsp' left_total_def)
[PROOF STATE]
proof (state)
this:
\<forall>x. P' x \<longrightarrow> Q' x

goal (3 subgoals):
 1. \<lbrakk>left_total C; right_unique C; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
 2. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 3. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. P' x \<longrightarrow> Q' x
[PROOF STEP]
show "?wit Q" if "?wit P"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. P' x \<longrightarrow> Q' x

goal (1 subgoal):
 1. rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
using P Q that
[PROOF STATE]
proof (prove)
using this:
\<forall>x. P' x \<longrightarrow> Q' x
rel_pred2_witness C C' (F, G) P = F P'
rel_pred2_witness C C' (F, G) Q = F Q'
rel_pred2_witness C C' (F, G) P

goal (1 subgoal):
 1. rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
by(simp add: is_filter.mono[OF F])
[PROOF STATE]
proof (state)
this:
rel_pred2_witness C C' (F, G) P \<Longrightarrow> rel_pred2_witness C C' (F, G) Q

goal (2 subgoals):
 1. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 2. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 2. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
assume "right_total C'" "left_unique C'"
[PROOF STATE]
proof (state)
this:
right_total C'
left_unique C'

goal (2 subgoals):
 1. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 2. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
hence "right_unique (C' ===> (=))" "left_total (C' ===> (=))"
[PROOF STATE]
proof (prove)
using this:
right_total C'
left_unique C'

goal (1 subgoal):
 1. right_unique (C' ===> (=)) &&& left_total (C' ===> (=))
[PROOF STEP]
by(blast intro: right_unique_fun right_unique_eq left_total_fun left_total_eq)+
[PROOF STATE]
proof (state)
this:
right_unique (C' ===> (=))
left_total (C' ===> (=))

goal (2 subgoals):
 1. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 2. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
from functional_relation[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. \<exists>!y. (C' ===> (=)) x y
[PROOF STEP]
obtain P' Q'
      where P' [transfer_rule]: "(C' ===> (=)) P P'" and Q' [transfer_rule]: "(C' ===> (=)) Q Q'"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. \<exists>!y. (C' ===> (=)) x y

goal (1 subgoal):
 1. (\<And>P' Q'. \<lbrakk>(C' ===> (=)) P P'; (C' ===> (=)) Q Q'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(C' ===> (=)) P P'
(C' ===> (=)) Q Q'

goal (2 subgoals):
 1. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 2. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
have PQ: "(C' ===> (=)) (\<lambda>x. P x \<and> Q x) (\<lambda>x. P' x \<and> Q' x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C' ===> (=)) (\<lambda>x. P x \<and> Q x) (\<lambda>x. P' x \<and> Q' x)
[PROOF STEP]
by transfer_prover
[PROOF STATE]
proof (state)
this:
(C' ===> (=)) (\<lambda>x. P x \<and> Q x) (\<lambda>x. P' x \<and> Q' x)

goal (2 subgoals):
 1. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 2. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
with wit2 P' Q'
[PROOF STATE]
proof (chain)
picking this:
rel_pred (rel_pred C') (rel_pred2_witness C C' (F, G)) G
(C' ===> (=)) P P'
(C' ===> (=)) Q Q'
(C' ===> (=)) (\<lambda>x. P x \<and> Q x) (\<lambda>x. P' x \<and> Q' x)
[PROOF STEP]
have P: "?wit P \<longleftrightarrow> G P'" and Q: "?wit Q \<longleftrightarrow> G Q'"
      and PQ: "?wit (\<lambda>x. P x \<and> Q x) \<longleftrightarrow> G (\<lambda>x. P' x \<and> Q' x)"
[PROOF STATE]
proof (prove)
using this:
rel_pred (rel_pred C') (rel_pred2_witness C C' (F, G)) G
(C' ===> (=)) P P'
(C' ===> (=)) Q Q'
(C' ===> (=)) (\<lambda>x. P x \<and> Q x) (\<lambda>x. P' x \<and> Q' x)

goal (1 subgoal):
 1. rel_pred2_witness C C' (F, G) P = G P' &&& rel_pred2_witness C C' (F, G) Q = G Q' &&& rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x) = G (\<lambda>x. P' x \<and> Q' x)
[PROOF STEP]
by(auto dest: rel_funD simp add: rel_pred_def)
[PROOF STATE]
proof (state)
this:
rel_pred2_witness C C' (F, G) P = G P'
rel_pred2_witness C C' (F, G) Q = G Q'
rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x) = G (\<lambda>x. P' x \<and> Q' x)

goal (2 subgoals):
 1. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 2. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
show "?wit (\<lambda>x. P x \<and> Q x)" if "?wit P" "?wit Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
[PROOF STEP]
using that P Q PQ
[PROOF STATE]
proof (prove)
using this:
rel_pred2_witness C C' (F, G) P
rel_pred2_witness C C' (F, G) Q
rel_pred2_witness C C' (F, G) P = G P'
rel_pred2_witness C C' (F, G) Q = G Q'
rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x) = G (\<lambda>x. P' x \<and> Q' x)

goal (1 subgoal):
 1. rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
[PROOF STEP]
by(auto intro: is_filter.conj[OF G])
[PROOF STATE]
proof (state)
this:
\<lbrakk>rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)

goal (1 subgoal):
 1. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
assume "\<forall>x. P x \<longrightarrow> Q x"
[PROOF STATE]
proof (state)
this:
\<forall>x. P x \<longrightarrow> Q x

goal (1 subgoal):
 1. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
with P' Q' \<open>right_total C'\<close>
[PROOF STATE]
proof (chain)
picking this:
(C' ===> (=)) P P'
(C' ===> (=)) Q Q'
right_total C'
\<forall>x. P x \<longrightarrow> Q x
[PROOF STEP]
have "\<forall>x. P' x \<longrightarrow> Q' x"
[PROOF STATE]
proof (prove)
using this:
(C' ===> (=)) P P'
(C' ===> (=)) Q Q'
right_total C'
\<forall>x. P x \<longrightarrow> Q x

goal (1 subgoal):
 1. \<forall>x. P' x \<longrightarrow> Q' x
[PROOF STEP]
by(metis (full_types) apply_rsp' right_total_def)
[PROOF STATE]
proof (state)
this:
\<forall>x. P' x \<longrightarrow> Q' x

goal (1 subgoal):
 1. \<lbrakk>right_total C'; left_unique C'; rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>x. P' x \<longrightarrow> Q' x
[PROOF STEP]
show "?wit Q" if "?wit P"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. P' x \<longrightarrow> Q' x

goal (1 subgoal):
 1. rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
using P Q that
[PROOF STATE]
proof (prove)
using this:
\<forall>x. P' x \<longrightarrow> Q' x
rel_pred2_witness C C' (F, G) P = G P'
rel_pred2_witness C C' (F, G) Q = G Q'
rel_pred2_witness C C' (F, G) P

goal (1 subgoal):
 1. rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
by(simp add: is_filter.mono[OF G])
[PROOF STATE]
proof (state)
this:
rel_pred2_witness C C' (F, G) P \<Longrightarrow> rel_pred2_witness C C' (F, G) Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(rel_pred2_witness C C' (F, G) P \<longrightarrow> rel_pred2_witness C C' (F, G) Q \<longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)) \<and> (rel_pred2_witness C C' (F, G) P \<longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<longrightarrow> rel_pred2_witness C C' (F, G) Q)

goal (2 subgoals):
 1. \<And>P Q. \<lbrakk>rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
 2. \<And>P Q. \<lbrakk>\<forall>x. P x \<longrightarrow> Q x; rel_pred2_witness C C' (F, G) P\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
show "?wit (\<lambda>x. P x \<and> Q x)" if P: "?wit P" and Q: "?wit Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
[PROOF STEP]
using * that
[PROOF STATE]
proof (prove)
using this:
(rel_pred2_witness C C' (F, G) P \<longrightarrow> rel_pred2_witness C C' (F, G) Q \<longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)) \<and> (rel_pred2_witness C C' (F, G) P \<longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<longrightarrow> rel_pred2_witness C C' (F, G) Q)
rel_pred2_witness C C' (F, G) P
rel_pred2_witness C C' (F, G) Q

goal (1 subgoal):
 1. rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>rel_pred2_witness C C' (F, G) P; rel_pred2_witness C C' (F, G) Q\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)

goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>\<forall>x. P x \<longrightarrow> Q x; rel_pred2_witness C C' (F, G) P\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
show "?wit Q" if P: "?wit P" and imp: "\<forall>x. P x \<longrightarrow> Q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
using * that
[PROOF STATE]
proof (prove)
using this:
(rel_pred2_witness C C' (F, G) P \<longrightarrow> rel_pred2_witness C C' (F, G) Q \<longrightarrow> rel_pred2_witness C C' (F, G) (\<lambda>x. P x \<and> Q x)) \<and> (rel_pred2_witness C C' (F, G) P \<longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<longrightarrow> rel_pred2_witness C C' (F, G) Q)
rel_pred2_witness C C' (F, G) P
\<forall>x. P x \<longrightarrow> Q x

goal (1 subgoal):
 1. rel_pred2_witness C C' (F, G) Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>rel_pred2_witness C C' (F, G) P; \<forall>x. P x \<longrightarrow> Q x\<rbrakk> \<Longrightarrow> rel_pred2_witness C C' (F, G) Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma raw_filtermap_apply: "raw_filtermap f F = (\<lambda>P. F (\<lambda>x. P (f x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. raw_filtermap f F = (\<lambda>P. F (\<lambda>x. P (f x)))
[PROOF STEP]
unfolding raw_filtermap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((f ---> id) ---> id) F = (\<lambda>P. F (\<lambda>x. P (f x)))
[PROOF STEP]
by (simp add: map_fun_def comp_def)


[STATEMENT]
lemma "filtermap f = Abs_filter \<circ> raw_filtermap f \<circ> Rep_filter"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filtermap f = Abs_filter \<circ> raw_filtermap f \<circ> Rep_filter
[PROOF STEP]
unfolding filtermap_def eventually_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>F. Abs_filter (\<lambda>P. Rep_filter F (\<lambda>x. P (f x)))) = Abs_filter \<circ> raw_filtermap f \<circ> Rep_filter
[PROOF STEP]
by (simp add: fun_eq_iff raw_filtermap_apply)


[STATEMENT]
lemma "is_filter (raw_filtermap fst Z')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_filter (raw_filtermap fst (\<lambda>P. Collect P \<in> Z))
[PROOF STEP]
unfolding Z_def raw_filtermap_apply
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_filter (\<lambda>P. {x. P (fst x)} \<in> {{(False, False), (False, True)}, {(False, False), (True, False)}, {(False, False), (False, True), (True, False), (True, True)}})
[PROOF STEP]
apply (rule is_filter.intro)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. {x. True} \<in> {{(False, False), (False, True)}, {(False, False), (True, False)}, {(False, False), (False, True), (True, False), (True, True)}}
 2. \<And>P Q. \<lbrakk>{x. P (fst x)} \<in> {{(False, False), (False, True)}, {(False, False), (True, False)}, {(False, False), (False, True), (True, False), (True, True)}}; {x. Q (fst x)} \<in> {{(False, False), (False, True)}, {(False, False), (True, False)}, {(False, False), (False, True), (True, False), (True, True)}}\<rbrakk> \<Longrightarrow> {x. P (fst x) \<and> Q (fst x)} \<in> {{(False, False), (False, True)}, {(False, False), (True, False)}, {(False, False), (False, True), (True, False), (True, True)}}
 3. \<And>P Q. \<lbrakk>\<forall>x. P x \<longrightarrow> Q x; {x. P (fst x)} \<in> {{(False, False), (False, True)}, {(False, False), (True, False)}, {(False, False), (False, True), (True, False), (True, True)}}\<rbrakk> \<Longrightarrow> {x. Q (fst x)} \<in> {{(False, False), (False, True)}, {(False, False), (True, False)}, {(False, False), (False, True), (True, False), (True, True)}}
[PROOF STEP]
apply (simp add: set_eq_iff; smt)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "is_filter (raw_filtermap snd Z')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_filter (raw_filtermap snd (\<lambda>P. Collect P \<in> Z))
[PROOF STEP]
unfolding Z_def raw_filtermap_apply
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_filter (\<lambda>P. {x. P (snd x)} \<in> {{(False, False), (False, True)}, {(False, False), (True, False)}, {(False, False), (False, True), (True, False), (True, True)}})
[PROOF STEP]
apply (rule is_filter.intro)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. {x. True} \<in> {{(False, False), (False, True)}, {(False, False), (True, False)}, {(False, False), (False, True), (True, False), (True, True)}}
 2. \<And>P Q. \<lbrakk>{x. P (snd x)} \<in> {{(False, False), (False, True)}, {(False, False), (True, False)}, {(False, False), (False, True), (True, False), (True, True)}}; {x. Q (snd x)} \<in> {{(False, False), (False, True)}, {(False, False), (True, False)}, {(False, False), (False, True), (True, False), (True, True)}}\<rbrakk> \<Longrightarrow> {x. P (snd x) \<and> Q (snd x)} \<in> {{(False, False), (False, True)}, {(False, False), (True, False)}, {(False, False), (False, True), (True, False), (True, True)}}
 3. \<And>P Q. \<lbrakk>\<forall>x. P x \<longrightarrow> Q x; {x. P (snd x)} \<in> {{(False, False), (False, True)}, {(False, False), (True, False)}, {(False, False), (False, True), (True, False), (True, True)}}\<rbrakk> \<Longrightarrow> {x. Q (snd x)} \<in> {{(False, False), (False, True)}, {(False, False), (True, False)}, {(False, False), (False, True), (True, False), (True, True)}}
[PROOF STEP]
apply (simp add: set_eq_iff; smt)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma equivp_aeseq_eq: "equivp aeseq_eq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equivp aeseq_eq
[PROOF STEP]
proof(rule equivpI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. reflp aeseq_eq
 2. symp aeseq_eq
 3. transp aeseq_eq
[PROOF STEP]
show "reflp aeseq_eq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflp aeseq_eq
[PROOF STEP]
by(simp add: reflp_def aeseq_eq.simps)
[PROOF STATE]
proof (state)
this:
reflp aeseq_eq

goal (2 subgoals):
 1. symp aeseq_eq
 2. transp aeseq_eq
[PROOF STEP]
show "symp aeseq_eq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symp aeseq_eq
[PROOF STEP]
by(simp add: symp_def aeseq_eq.simps eq_commute)
[PROOF STATE]
proof (state)
this:
symp aeseq_eq

goal (1 subgoal):
 1. transp aeseq_eq
[PROOF STEP]
have "finite {n. f n \<noteq> h n}" if "finite {n. f n \<noteq> g n}" "finite {n. g n \<noteq> h n}"
    for f g h :: "nat \<Rightarrow> 'b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {n. f n \<noteq> h n}
[PROOF STEP]
using finite_subset[of "{n. f n \<noteq> h n}" "{n. f n \<noteq> g n} \<union> {n. g n \<noteq> h n}"] that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>{n. f n \<noteq> h n} \<subseteq> {n. f n \<noteq> g n} \<union> {n. g n \<noteq> h n}; finite ({n. f n \<noteq> g n} \<union> {n. g n \<noteq> h n})\<rbrakk> \<Longrightarrow> finite {n. f n \<noteq> h n}
finite {n. f n \<noteq> g n}
finite {n. g n \<noteq> h n}

goal (1 subgoal):
 1. finite {n. f n \<noteq> h n}
[PROOF STEP]
by(fastforce intro: finite_subset)
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite {n. ?f3 n \<noteq> ?g3 n}; finite {n. ?g3 n \<noteq> ?h3 n}\<rbrakk> \<Longrightarrow> finite {n. ?f3 n \<noteq> ?h3 n}

goal (1 subgoal):
 1. transp aeseq_eq
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>finite {n. ?f3 n \<noteq> ?g3 n}; finite {n. ?g3 n \<noteq> ?h3 n}\<rbrakk> \<Longrightarrow> finite {n. ?f3 n \<noteq> ?h3 n}
[PROOF STEP]
show "transp aeseq_eq"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {n. ?f3 n \<noteq> ?g3 n}; finite {n. ?g3 n \<noteq> ?h3 n}\<rbrakk> \<Longrightarrow> finite {n. ?f3 n \<noteq> ?h3 n}

goal (1 subgoal):
 1. transp aeseq_eq
[PROOF STEP]
by(auto simp add: transp_def aeseq_eq.simps)
[PROOF STATE]
proof (state)
this:
transp aeseq_eq

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_aeseq_id: "map_aeseq id x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_aeseq id x = x
[PROOF STEP]
by transfer(simp add: equivp_reflp[OF equivp_aeseq_eq])


[STATEMENT]
lemma map_aeseq_comp: "map_aeseq f (map_aeseq g x) = map_aeseq (f \<circ> g) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_aeseq f (map_aeseq g x) = map_aeseq (f \<circ> g) x
[PROOF STEP]
by transfer(simp add: o_assoc equivp_reflp[OF equivp_aeseq_eq])


[STATEMENT]
lemma rel_aeseq_mono: "R \<le> S \<Longrightarrow> rel_aeseq R \<le> rel_aeseq S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<le> S \<Longrightarrow> rel_aeseq R \<le> rel_aeseq S
[PROOF STEP]
by(rule predicate2I; transfer; auto intro: finite_subset[rotated])


[STATEMENT]
lemma rel_aeseq_eq: "rel_aeseq (=) = (=)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_aeseq (=) = (=)
[PROOF STEP]
by(intro ext; transfer; simp add: aeseq_eq.simps)


[STATEMENT]
lemma rel_aeseq_conversep: "rel_aeseq R\<inverse>\<inverse> = (rel_aeseq R)\<inverse>\<inverse>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_aeseq R\<inverse>\<inverse> = (rel_aeseq R)\<inverse>\<inverse>
[PROOF STEP]
by(simp add: fun_eq_iff; transfer; simp)


[STATEMENT]
lemma map_aeseq_parametric: includes lifting_syntax shows
  "((A ===> B) ===> rel_aeseq A ===> rel_aeseq B) map_aeseq map_aeseq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> B) ===> rel_aeseq A ===> rel_aeseq B) map_aeseq map_aeseq
[PROOF STEP]
by(intro rel_funI; transfer; auto elim: finite_subset[rotated] dest: rel_funD)


[STATEMENT]
lemma rel_aeseq_distr: "rel_aeseq (R OO S) = rel_aeseq R OO rel_aeseq S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_aeseq (R OO S) = rel_aeseq R OO rel_aeseq S
[PROOF STEP]
apply(intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. rel_aeseq (R OO S) x xa = (rel_aeseq R OO rel_aeseq S) x xa
[PROOF STEP]
apply(transfer fixing: R S)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. finite {n. \<not> (R OO S) (x n) (xa n)} = ((\<lambda>f g. finite {n. \<not> R (f n) (g n)}) OO (\<lambda>f g. finite {n. \<not> S (f n) (g n)})) x xa
[PROOF STEP]
apply(safe)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. finite {n. \<not> (R OO S) (x n) (xa n)} \<Longrightarrow> ((\<lambda>f g. finite {n. \<not> R (f n) (g n)}) OO (\<lambda>f g. finite {n. \<not> S (f n) (g n)})) x xa
 2. \<And>x xa b. \<lbrakk>finite {n. \<not> R (x n) (b n)}; finite {n. \<not> S (b n) (xa n)}\<rbrakk> \<Longrightarrow> finite {n. \<not> (R OO S) (x n) (xa n)}
[PROOF STEP]
subgoal for f h
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {n. \<not> (R OO S) (f n) (h n)} \<Longrightarrow> ((\<lambda>f g. finite {n. \<not> R (f n) (g n)}) OO (\<lambda>f g. finite {n. \<not> S (f n) (g n)})) f h
[PROOF STEP]
apply(rule relcomppI[where b="\<lambda>n. SOME z. R (f n) z \<and> S z (h n)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite {n. \<not> (R OO S) (f n) (h n)} \<Longrightarrow> finite {n. \<not> R (f n) (SOME z. R (f n) z \<and> S z (h n))}
 2. finite {n. \<not> (R OO S) (f n) (h n)} \<Longrightarrow> finite {n. \<not> S (SOME z. R (f n) z \<and> S z (h n)) (h n)}
[PROOF STEP]
apply(auto elim!: finite_subset[rotated] intro: someI2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa b. \<lbrakk>finite {n. \<not> R (x n) (b n)}; finite {n. \<not> S (b n) (xa n)}\<rbrakk> \<Longrightarrow> finite {n. \<not> (R OO S) (x n) (xa n)}
[PROOF STEP]
subgoal for f h g
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite {n. \<not> R (f n) (g n)}; finite {n. \<not> S (g n) (h n)}\<rbrakk> \<Longrightarrow> finite {n. \<not> (R OO S) (f n) (h n)}
[PROOF STEP]
apply(rule finite_subset[where B="{n. \<not> R (f n) (g n)} \<union> {n. \<not> S (g n) (h n)}"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite {n. \<not> R (f n) (g n)}; finite {n. \<not> S (g n) (h n)}\<rbrakk> \<Longrightarrow> {n. \<not> (R OO S) (f n) (h n)} \<subseteq> {n. \<not> R (f n) (g n)} \<union> {n. \<not> S (g n) (h n)}
 2. \<lbrakk>finite {n. \<not> R (f n) (g n)}; finite {n. \<not> S (g n) (h n)}\<rbrakk> \<Longrightarrow> finite ({n. \<not> R (f n) (g n)} \<union> {n. \<not> S (g n) (h n)})
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma closed_segment_imp_Re_Im:
  fixes x::complex
  assumes "x\<in>closed_segment lb ub"
  shows "Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x \<and> Re x \<le> Re ub"
        "Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x \<and> Im x \<le> Im ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x \<and> Re x \<le> Re ub) &&& (Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x \<and> Im x \<le> Im ub)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x \<and> Re x \<le> Re ub
 2. Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x \<and> Im x \<le> Im ub
[PROOF STEP]
obtain u where x_u:"x=(1 - u) *\<^sub>R lb + u *\<^sub>R ub " and "0 \<le> u" "u \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u. \<lbrakk>x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub; 0 \<le> u; u \<le> 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> closed_segment lb ub

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub; 0 \<le> u; u \<le> 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding closed_segment_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {(1 - u) *\<^sub>R lb + u *\<^sub>R ub |u. 0 \<le> u \<and> u \<le> 1}

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub; 0 \<le> u; u \<le> 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub
0 \<le> u
u \<le> 1

goal (2 subgoals):
 1. Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x \<and> Re x \<le> Re ub
 2. Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x \<and> Im x \<le> Im ub
[PROOF STEP]
have "Re lb \<le> Re x" when "Re lb \<le> Re ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re lb \<le> Re x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Re lb \<le> Re x
[PROOF STEP]
have "Re x = Re ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re x = Re ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)
[PROOF STEP]
using x_u
[PROOF STATE]
proof (prove)
using this:
x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub

goal (1 subgoal):
 1. Re x = Re ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Re x = Re ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)

goal (1 subgoal):
 1. Re lb \<le> Re x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Re x = Re ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)

goal (1 subgoal):
 1. Re lb \<le> Re x
[PROOF STEP]
have "... = Re (lb + u *\<^sub>R (ub - lb))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re ((1 - u) *\<^sub>R lb + u *\<^sub>R ub) = Re (lb + u *\<^sub>R (ub - lb))
[PROOF STEP]
by (auto simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
Re ((1 - u) *\<^sub>R lb + u *\<^sub>R ub) = Re (lb + u *\<^sub>R (ub - lb))

goal (1 subgoal):
 1. Re lb \<le> Re x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Re ((1 - u) *\<^sub>R lb + u *\<^sub>R ub) = Re (lb + u *\<^sub>R (ub - lb))

goal (1 subgoal):
 1. Re lb \<le> Re x
[PROOF STEP]
have "... = Re lb + u * (Re ub - Re lb)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re (lb + u *\<^sub>R (ub - lb)) = Re lb + u * (Re ub - Re lb)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Re (lb + u *\<^sub>R (ub - lb)) = Re lb + u * (Re ub - Re lb)

goal (1 subgoal):
 1. Re lb \<le> Re x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Re (lb + u *\<^sub>R (ub - lb)) = Re lb + u * (Re ub - Re lb)

goal (1 subgoal):
 1. Re lb \<le> Re x
[PROOF STEP]
have "... \<ge> Re lb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re lb \<le> Re lb + u * (Re ub - Re lb)
[PROOF STEP]
using \<open>u\<ge>0\<close> \<open>Re lb \<le> Re ub\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> u
Re lb \<le> Re ub

goal (1 subgoal):
 1. Re lb \<le> Re lb + u * (Re ub - Re lb)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Re lb \<le> Re lb + u * (Re ub - Re lb)

goal (1 subgoal):
 1. Re lb \<le> Re x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Re lb \<le> Re x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Re lb \<le> Re x

goal (1 subgoal):
 1. Re lb \<le> Re x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Re lb \<le> Re x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x

goal (2 subgoals):
 1. Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x \<and> Re x \<le> Re ub
 2. Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x \<and> Im x \<le> Im ub
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x

goal (2 subgoals):
 1. Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x \<and> Re x \<le> Re ub
 2. Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x \<and> Im x \<le> Im ub
[PROOF STEP]
have "Im lb \<le> Im x" when "Im lb \<le> Im ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im lb \<le> Im x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Im lb \<le> Im x
[PROOF STEP]
have "Im x = Im ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im x = Im ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)
[PROOF STEP]
using x_u
[PROOF STATE]
proof (prove)
using this:
x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub

goal (1 subgoal):
 1. Im x = Im ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Im x = Im ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)

goal (1 subgoal):
 1. Im lb \<le> Im x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Im x = Im ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)

goal (1 subgoal):
 1. Im lb \<le> Im x
[PROOF STEP]
have "... = Im (lb + u *\<^sub>R (ub - lb))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im ((1 - u) *\<^sub>R lb + u *\<^sub>R ub) = Im (lb + u *\<^sub>R (ub - lb))
[PROOF STEP]
by (auto simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
Im ((1 - u) *\<^sub>R lb + u *\<^sub>R ub) = Im (lb + u *\<^sub>R (ub - lb))

goal (1 subgoal):
 1. Im lb \<le> Im x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Im ((1 - u) *\<^sub>R lb + u *\<^sub>R ub) = Im (lb + u *\<^sub>R (ub - lb))

goal (1 subgoal):
 1. Im lb \<le> Im x
[PROOF STEP]
have "... = Im lb + u * (Im ub - Im lb)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im (lb + u *\<^sub>R (ub - lb)) = Im lb + u * (Im ub - Im lb)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Im (lb + u *\<^sub>R (ub - lb)) = Im lb + u * (Im ub - Im lb)

goal (1 subgoal):
 1. Im lb \<le> Im x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Im (lb + u *\<^sub>R (ub - lb)) = Im lb + u * (Im ub - Im lb)

goal (1 subgoal):
 1. Im lb \<le> Im x
[PROOF STEP]
have "... \<ge> Im lb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im lb \<le> Im lb + u * (Im ub - Im lb)
[PROOF STEP]
using \<open>u\<ge>0\<close> \<open>Im lb \<le> Im ub\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> u
Im lb \<le> Im ub

goal (1 subgoal):
 1. Im lb \<le> Im lb + u * (Im ub - Im lb)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Im lb \<le> Im lb + u * (Im ub - Im lb)

goal (1 subgoal):
 1. Im lb \<le> Im x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Im lb \<le> Im x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Im lb \<le> Im x

goal (1 subgoal):
 1. Im lb \<le> Im x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Im lb \<le> Im x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x

goal (2 subgoals):
 1. Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x \<and> Re x \<le> Re ub
 2. Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x \<and> Im x \<le> Im ub
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x

goal (2 subgoals):
 1. Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x \<and> Re x \<le> Re ub
 2. Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x \<and> Im x \<le> Im ub
[PROOF STEP]
have "Re x \<le> Re ub" when "Re lb \<le> Re ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re x \<le> Re ub
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Re x \<le> Re ub
[PROOF STEP]
have "Re x = Re ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re x = Re ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)
[PROOF STEP]
using x_u
[PROOF STATE]
proof (prove)
using this:
x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub

goal (1 subgoal):
 1. Re x = Re ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Re x = Re ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)

goal (1 subgoal):
 1. Re x \<le> Re ub
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Re x = Re ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)

goal (1 subgoal):
 1. Re x \<le> Re ub
[PROOF STEP]
have "... = (1 - u) * Re lb + u * Re ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re ((1 - u) *\<^sub>R lb + u *\<^sub>R ub) = (1 - u) * Re lb + u * Re ub
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Re ((1 - u) *\<^sub>R lb + u *\<^sub>R ub) = (1 - u) * Re lb + u * Re ub

goal (1 subgoal):
 1. Re x \<le> Re ub
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Re ((1 - u) *\<^sub>R lb + u *\<^sub>R ub) = (1 - u) * Re lb + u * Re ub

goal (1 subgoal):
 1. Re x \<le> Re ub
[PROOF STEP]
have "... \<le> (1 - u) * Re ub + u * Re ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - u) * Re lb + u * Re ub \<le> (1 - u) * Re ub + u * Re ub
[PROOF STEP]
using \<open>u\<le>1\<close> \<open>Re lb \<le> Re ub\<close>
[PROOF STATE]
proof (prove)
using this:
u \<le> 1
Re lb \<le> Re ub

goal (1 subgoal):
 1. (1 - u) * Re lb + u * Re ub \<le> (1 - u) * Re ub + u * Re ub
[PROOF STEP]
by (auto simp add: mult_left_mono)
[PROOF STATE]
proof (state)
this:
(1 - u) * Re lb + u * Re ub \<le> (1 - u) * Re ub + u * Re ub

goal (1 subgoal):
 1. Re x \<le> Re ub
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1 - u) * Re lb + u * Re ub \<le> (1 - u) * Re ub + u * Re ub

goal (1 subgoal):
 1. Re x \<le> Re ub
[PROOF STEP]
have "... = Re ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - u) * Re ub + u * Re ub = Re ub
[PROOF STEP]
by (auto simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
(1 - u) * Re ub + u * Re ub = Re ub

goal (1 subgoal):
 1. Re x \<le> Re ub
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Re x \<le> Re ub
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Re x \<le> Re ub

goal (1 subgoal):
 1. Re x \<le> Re ub
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Re x \<le> Re ub

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Re lb \<le> Re ub \<Longrightarrow> Re x \<le> Re ub

goal (2 subgoals):
 1. Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x \<and> Re x \<le> Re ub
 2. Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x \<and> Im x \<le> Im ub
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Re lb \<le> Re ub \<Longrightarrow> Re x \<le> Re ub

goal (2 subgoals):
 1. Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x \<and> Re x \<le> Re ub
 2. Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x \<and> Im x \<le> Im ub
[PROOF STEP]
have "Im x \<le> Im ub" when "Im lb \<le> Im ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im x \<le> Im ub
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Im x \<le> Im ub
[PROOF STEP]
have "Im x = Im ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im x = Im ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)
[PROOF STEP]
using x_u
[PROOF STATE]
proof (prove)
using this:
x = (1 - u) *\<^sub>R lb + u *\<^sub>R ub

goal (1 subgoal):
 1. Im x = Im ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Im x = Im ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)

goal (1 subgoal):
 1. Im x \<le> Im ub
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Im x = Im ((1 - u) *\<^sub>R lb + u *\<^sub>R ub)

goal (1 subgoal):
 1. Im x \<le> Im ub
[PROOF STEP]
have "... = (1 - u) * Im lb + u * Im ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im ((1 - u) *\<^sub>R lb + u *\<^sub>R ub) = (1 - u) * Im lb + u * Im ub
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Im ((1 - u) *\<^sub>R lb + u *\<^sub>R ub) = (1 - u) * Im lb + u * Im ub

goal (1 subgoal):
 1. Im x \<le> Im ub
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Im ((1 - u) *\<^sub>R lb + u *\<^sub>R ub) = (1 - u) * Im lb + u * Im ub

goal (1 subgoal):
 1. Im x \<le> Im ub
[PROOF STEP]
have "... \<le> (1 - u) * Im ub + u * Im ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - u) * Im lb + u * Im ub \<le> (1 - u) * Im ub + u * Im ub
[PROOF STEP]
using \<open>u\<le>1\<close> \<open>Im lb \<le> Im ub\<close>
[PROOF STATE]
proof (prove)
using this:
u \<le> 1
Im lb \<le> Im ub

goal (1 subgoal):
 1. (1 - u) * Im lb + u * Im ub \<le> (1 - u) * Im ub + u * Im ub
[PROOF STEP]
by (auto simp add: mult_left_mono)
[PROOF STATE]
proof (state)
this:
(1 - u) * Im lb + u * Im ub \<le> (1 - u) * Im ub + u * Im ub

goal (1 subgoal):
 1. Im x \<le> Im ub
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1 - u) * Im lb + u * Im ub \<le> (1 - u) * Im ub + u * Im ub

goal (1 subgoal):
 1. Im x \<le> Im ub
[PROOF STEP]
have "... = Im ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - u) * Im ub + u * Im ub = Im ub
[PROOF STEP]
by (auto simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
(1 - u) * Im ub + u * Im ub = Im ub

goal (1 subgoal):
 1. Im x \<le> Im ub
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Im x \<le> Im ub
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Im x \<le> Im ub

goal (1 subgoal):
 1. Im x \<le> Im ub
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Im x \<le> Im ub

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Im lb \<le> Im ub \<Longrightarrow> Im x \<le> Im ub

goal (2 subgoals):
 1. Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x \<and> Re x \<le> Re ub
 2. Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x \<and> Im x \<le> Im ub
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x
Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x
Re lb \<le> Re ub \<Longrightarrow> Re x \<le> Re ub
Im lb \<le> Im ub \<Longrightarrow> Im x \<le> Im ub
[PROOF STEP]
show
      "Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x \<and> Re x \<le> Re ub"
      "Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x \<and> Im x \<le> Im ub"
[PROOF STATE]
proof (prove)
using this:
Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x
Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x
Re lb \<le> Re ub \<Longrightarrow> Re x \<le> Re ub
Im lb \<le> Im ub \<Longrightarrow> Im x \<le> Im ub

goal (1 subgoal):
 1. (Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x \<and> Re x \<le> Re ub) &&& (Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x \<and> Im x \<le> Im ub)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Re lb \<le> Re ub \<Longrightarrow> Re lb \<le> Re x \<and> Re x \<le> Re ub
Im lb \<le> Im ub \<Longrightarrow> Im lb \<le> Im x \<and> Im x \<le> Im ub

goal:
No subgoals!
[PROOF STEP]
qed