[STATEMENT]
lemma loxodromic_attracting_fixed_point:
  assumes "loxodromic_isometry f"
  shows "attracting_fixed_point f \<in> Gromov_boundary"
        "Gromov_extension f (attracting_fixed_point f) = attracting_fixed_point f"
        "additive_strength f (attracting_fixed_point f) < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. attracting_fixed_point f \<in> Gromov_boundary &&& Gromov_extension f (attracting_fixed_point f) = attracting_fixed_point f &&& additive_strength f (attracting_fixed_point f) < 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. attracting_fixed_point f \<in> Gromov_boundary
 2. Gromov_extension f (attracting_fixed_point f) = attracting_fixed_point f
 3. additive_strength f (attracting_fixed_point f) < 0
[PROOF STEP]
obtain xi where xi: "xi \<in> Gromov_boundary" "Gromov_extension f xi = xi" "additive_strength f xi \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xi. \<lbrakk>xi \<in> Gromov_boundary; Gromov_extension f xi = xi; additive_strength f xi \<le> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using isometry_not_elliptic_has_attracting_fixed_point loxodromic_isometryD[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>isometry ?f; \<not> elliptic_isometry ?f\<rbrakk> \<Longrightarrow> \<exists>xi\<in>Gromov_boundary. Gromov_extension ?f xi = xi \<and> additive_strength ?f xi \<le> 0
isometry f
\<not> bounded {(f ^^ n) ?x |n. True}
0 < stable_translation_length f
\<not> elliptic_isometry f

goal (1 subgoal):
 1. (\<And>xi. \<lbrakk>xi \<in> Gromov_boundary; Gromov_extension f xi = xi; additive_strength f xi \<le> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xi \<in> Gromov_boundary
Gromov_extension f xi = xi
additive_strength f xi \<le> 0

goal (3 subgoals):
 1. attracting_fixed_point f \<in> Gromov_boundary
 2. Gromov_extension f (attracting_fixed_point f) = attracting_fixed_point f
 3. additive_strength f (attracting_fixed_point f) < 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xi \<in> Gromov_boundary
Gromov_extension f xi = xi
additive_strength f xi \<le> 0

goal (3 subgoals):
 1. attracting_fixed_point f \<in> Gromov_boundary
 2. Gromov_extension f (attracting_fixed_point f) = attracting_fixed_point f
 3. additive_strength f (attracting_fixed_point f) < 0
[PROOF STEP]
have "additive_strength f xi < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. additive_strength f xi < 0
[PROOF STEP]
using stable_translation_length_eq_additive_strength[OF loxodromic_isometryD(1)[OF assms] xi(2)]
    loxodromic_isometryD(3)[OF assms] xi(3)
[PROOF STATE]
proof (prove)
using this:
stable_translation_length f = \<bar>additive_strength f xi\<bar>
0 < stable_translation_length f
additive_strength f xi \<le> 0

goal (1 subgoal):
 1. additive_strength f xi < 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
additive_strength f xi < 0

goal (3 subgoals):
 1. attracting_fixed_point f \<in> Gromov_boundary
 2. Gromov_extension f (attracting_fixed_point f) = attracting_fixed_point f
 3. additive_strength f (attracting_fixed_point f) < 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xi \<in> Gromov_boundary
Gromov_extension f xi = xi
additive_strength f xi \<le> 0
additive_strength f xi < 0
[PROOF STEP]
have A: "\<exists>xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi < 0"
[PROOF STATE]
proof (prove)
using this:
xi \<in> Gromov_boundary
Gromov_extension f xi = xi
additive_strength f xi \<le> 0
additive_strength f xi < 0

goal (1 subgoal):
 1. \<exists>xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi < 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi < 0

goal (3 subgoals):
 1. attracting_fixed_point f \<in> Gromov_boundary
 2. Gromov_extension f (attracting_fixed_point f) = attracting_fixed_point f
 3. additive_strength f (attracting_fixed_point f) < 0
[PROOF STEP]
show "attracting_fixed_point f \<in> Gromov_boundary"
       "Gromov_extension f (attracting_fixed_point f) = attracting_fixed_point f"
       "additive_strength f (attracting_fixed_point f) < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. attracting_fixed_point f \<in> Gromov_boundary &&& Gromov_extension f (attracting_fixed_point f) = attracting_fixed_point f &&& additive_strength f (attracting_fixed_point f) < 0
[PROOF STEP]
unfolding attracting_fixed_point_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi < 0) \<in> Gromov_boundary &&& Gromov_extension f (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi < 0) = (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi < 0) &&& additive_strength f (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi < 0) < 0
[PROOF STEP]
using someI_ex[OF A]
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> Gromov_boundary \<and> Gromov_extension f x = x \<and> additive_strength f x < 0) \<in> Gromov_boundary \<and> Gromov_extension f (SOME x. x \<in> Gromov_boundary \<and> Gromov_extension f x = x \<and> additive_strength f x < 0) = (SOME x. x \<in> Gromov_boundary \<and> Gromov_extension f x = x \<and> additive_strength f x < 0) \<and> additive_strength f (SOME x. x \<in> Gromov_boundary \<and> Gromov_extension f x = x \<and> additive_strength f x < 0) < 0

goal (1 subgoal):
 1. (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi < 0) \<in> Gromov_boundary &&& Gromov_extension f (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi < 0) = (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi < 0) &&& additive_strength f (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi < 0) < 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
attracting_fixed_point f \<in> Gromov_boundary
Gromov_extension f (attracting_fixed_point f) = attracting_fixed_point f
additive_strength f (attracting_fixed_point f) < 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma loxodromic_repelling_fixed_point:
  assumes "loxodromic_isometry f"
  shows "repelling_fixed_point f \<in> Gromov_boundary"
        "Gromov_extension f (repelling_fixed_point f) = repelling_fixed_point f"
        "additive_strength f (repelling_fixed_point f) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. repelling_fixed_point f \<in> Gromov_boundary &&& Gromov_extension f (repelling_fixed_point f) = repelling_fixed_point f &&& 0 < additive_strength f (repelling_fixed_point f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. repelling_fixed_point f \<in> Gromov_boundary
 2. Gromov_extension f (repelling_fixed_point f) = repelling_fixed_point f
 3. 0 < additive_strength f (repelling_fixed_point f)
[PROOF STEP]
obtain xi where xi: "xi \<in> Gromov_boundary" "Gromov_extension f xi = xi" "additive_strength f xi \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xi. \<lbrakk>xi \<in> Gromov_boundary; Gromov_extension f xi = xi; 0 \<le> additive_strength f xi\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using isometry_not_elliptic_has_repelling_fixed_point loxodromic_isometryD[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>isometry ?f; \<not> elliptic_isometry ?f\<rbrakk> \<Longrightarrow> \<exists>xi\<in>Gromov_boundary. Gromov_extension ?f xi = xi \<and> 0 \<le> additive_strength ?f xi
isometry f
\<not> bounded {(f ^^ n) ?x |n. True}
0 < stable_translation_length f
\<not> elliptic_isometry f

goal (1 subgoal):
 1. (\<And>xi. \<lbrakk>xi \<in> Gromov_boundary; Gromov_extension f xi = xi; 0 \<le> additive_strength f xi\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xi \<in> Gromov_boundary
Gromov_extension f xi = xi
0 \<le> additive_strength f xi

goal (3 subgoals):
 1. repelling_fixed_point f \<in> Gromov_boundary
 2. Gromov_extension f (repelling_fixed_point f) = repelling_fixed_point f
 3. 0 < additive_strength f (repelling_fixed_point f)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xi \<in> Gromov_boundary
Gromov_extension f xi = xi
0 \<le> additive_strength f xi

goal (3 subgoals):
 1. repelling_fixed_point f \<in> Gromov_boundary
 2. Gromov_extension f (repelling_fixed_point f) = repelling_fixed_point f
 3. 0 < additive_strength f (repelling_fixed_point f)
[PROOF STEP]
have "additive_strength f xi > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < additive_strength f xi
[PROOF STEP]
using stable_translation_length_eq_additive_strength[OF loxodromic_isometryD(1)[OF assms] xi(2)]
    loxodromic_isometryD(3)[OF assms] xi(3)
[PROOF STATE]
proof (prove)
using this:
stable_translation_length f = \<bar>additive_strength f xi\<bar>
0 < stable_translation_length f
0 \<le> additive_strength f xi

goal (1 subgoal):
 1. 0 < additive_strength f xi
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < additive_strength f xi

goal (3 subgoals):
 1. repelling_fixed_point f \<in> Gromov_boundary
 2. Gromov_extension f (repelling_fixed_point f) = repelling_fixed_point f
 3. 0 < additive_strength f (repelling_fixed_point f)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xi \<in> Gromov_boundary
Gromov_extension f xi = xi
0 \<le> additive_strength f xi
0 < additive_strength f xi
[PROOF STEP]
have A: "\<exists>xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> additive_strength f xi > 0"
[PROOF STATE]
proof (prove)
using this:
xi \<in> Gromov_boundary
Gromov_extension f xi = xi
0 \<le> additive_strength f xi
0 < additive_strength f xi

goal (1 subgoal):
 1. \<exists>xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> 0 < additive_strength f xi
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> 0 < additive_strength f xi

goal (3 subgoals):
 1. repelling_fixed_point f \<in> Gromov_boundary
 2. Gromov_extension f (repelling_fixed_point f) = repelling_fixed_point f
 3. 0 < additive_strength f (repelling_fixed_point f)
[PROOF STEP]
show "repelling_fixed_point f \<in> Gromov_boundary"
       "Gromov_extension f (repelling_fixed_point f) = repelling_fixed_point f"
       "additive_strength f (repelling_fixed_point f) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. repelling_fixed_point f \<in> Gromov_boundary &&& Gromov_extension f (repelling_fixed_point f) = repelling_fixed_point f &&& 0 < additive_strength f (repelling_fixed_point f)
[PROOF STEP]
unfolding repelling_fixed_point_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> 0 < additive_strength f xi) \<in> Gromov_boundary &&& Gromov_extension f (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> 0 < additive_strength f xi) = (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> 0 < additive_strength f xi) &&& 0 < additive_strength f (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> 0 < additive_strength f xi)
[PROOF STEP]
using someI_ex[OF A]
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> Gromov_boundary \<and> Gromov_extension f x = x \<and> 0 < additive_strength f x) \<in> Gromov_boundary \<and> Gromov_extension f (SOME x. x \<in> Gromov_boundary \<and> Gromov_extension f x = x \<and> 0 < additive_strength f x) = (SOME x. x \<in> Gromov_boundary \<and> Gromov_extension f x = x \<and> 0 < additive_strength f x) \<and> 0 < additive_strength f (SOME x. x \<in> Gromov_boundary \<and> Gromov_extension f x = x \<and> 0 < additive_strength f x)

goal (1 subgoal):
 1. (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> 0 < additive_strength f xi) \<in> Gromov_boundary &&& Gromov_extension f (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> 0 < additive_strength f xi) = (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> 0 < additive_strength f xi) &&& 0 < additive_strength f (SOME xi. xi \<in> Gromov_boundary \<and> Gromov_extension f xi = xi \<and> 0 < additive_strength f xi)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
repelling_fixed_point f \<in> Gromov_boundary
Gromov_extension f (repelling_fixed_point f) = repelling_fixed_point f
0 < additive_strength f (repelling_fixed_point f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma attracting_fixed_point_neq_repelling_fixed_point:
  assumes "loxodromic_isometry f"
  shows "attracting_fixed_point f \<noteq> repelling_fixed_point f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. attracting_fixed_point f \<noteq> repelling_fixed_point f
[PROOF STEP]
using loxodromic_repelling_fixed_point[OF assms] loxodromic_attracting_fixed_point[OF assms]
[PROOF STATE]
proof (prove)
using this:
repelling_fixed_point f \<in> Gromov_boundary
Gromov_extension f (repelling_fixed_point f) = repelling_fixed_point f
0 < additive_strength f (repelling_fixed_point f)
attracting_fixed_point f \<in> Gromov_boundary
Gromov_extension f (attracting_fixed_point f) = attracting_fixed_point f
additive_strength f (attracting_fixed_point f) < 0

goal (1 subgoal):
 1. attracting_fixed_point f \<noteq> repelling_fixed_point f
[PROOF STEP]
by auto


[STATEMENT]
lemma loxodromic_attracting_fixed_point_attracts:
  assumes "loxodromic_isometry f"
          "xi \<noteq> repelling_fixed_point f"
  shows "(\<lambda>n. ((Gromov_extension f)^^n) xi) \<longlonglongrightarrow> attracting_fixed_point f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. (Gromov_extension f ^^ n) xi) \<longlonglongrightarrow> attracting_fixed_point f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. (Gromov_extension f ^^ n) xi) \<longlonglongrightarrow> attracting_fixed_point f
[PROOF STEP]
have "(\<lambda>n. extended_Gromov_product_at basepoint (((Gromov_extension f)^^n) xi) (attracting_fixed_point f)) \<longlonglongrightarrow> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. extended_Gromov_product_at basepoint ((Gromov_extension f ^^ n) xi) (attracting_fixed_point f)) \<longlonglongrightarrow> \<infinity>
[PROOF STEP]
unfolding Lim_PInfty
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>B. \<exists>N. \<forall>n\<ge>N. ereal B \<le> extended_Gromov_product_at basepoint ((Gromov_extension f ^^ n) xi) (attracting_fixed_point f)
[PROOF STEP]
using loxodromic_attracting_fixed_point_attracts_uniformly[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
\<exists>N. \<forall>n\<ge>N. \<forall>x. extended_Gromov_product_at basepoint x (repelling_fixed_point f) \<le> ereal ?K \<longrightarrow> ereal ?M \<le> extended_Gromov_product_at basepoint ((Gromov_extension f ^^ n) x) (attracting_fixed_point f)

goal (1 subgoal):
 1. \<forall>B. \<exists>N. \<forall>n\<ge>N. ereal B \<le> extended_Gromov_product_at basepoint ((Gromov_extension f ^^ n) xi) (attracting_fixed_point f)
[PROOF STEP]
by auto (metis Gromov_boundary_extended_product_PInf assms(2) dual_order.refl real_le_ereal_iff real_of_ereal_le_0 zero_ereal_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. extended_Gromov_product_at basepoint ((Gromov_extension f ^^ n) xi) (attracting_fixed_point f)) \<longlonglongrightarrow> \<infinity>

goal (1 subgoal):
 1. (\<lambda>n. (Gromov_extension f ^^ n) xi) \<longlonglongrightarrow> attracting_fixed_point f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. extended_Gromov_product_at basepoint ((Gromov_extension f ^^ n) xi) (attracting_fixed_point f)) \<longlonglongrightarrow> \<infinity>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. extended_Gromov_product_at basepoint ((Gromov_extension f ^^ n) xi) (attracting_fixed_point f)) \<longlonglongrightarrow> \<infinity>

goal (1 subgoal):
 1. (\<lambda>n. (Gromov_extension f ^^ n) xi) \<longlonglongrightarrow> attracting_fixed_point f
[PROOF STEP]
unfolding Gromov_completion_boundary_limit[OF loxodromic_attracting_fixed_point(1)[OF assms(1)]]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. extended_Gromov_product_at basepoint ((Gromov_extension f ^^ n) xi) (attracting_fixed_point f)) \<longlonglongrightarrow> \<infinity>

goal (1 subgoal):
 1. (\<lambda>n. extended_Gromov_product_at basepoint ((Gromov_extension f ^^ n) xi) (attracting_fixed_point f)) \<longlonglongrightarrow> \<infinity>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (Gromov_extension f ^^ n) xi) \<longlonglongrightarrow> attracting_fixed_point f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem loxodromic_unique_fixed_points:
  assumes "loxodromic_isometry f"
  shows "Gromov_extension f xi = xi \<longleftrightarrow> xi = attracting_fixed_point f \<or> xi = repelling_fixed_point f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Gromov_extension f xi = xi) = (xi = attracting_fixed_point f \<or> xi = repelling_fixed_point f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (Gromov_extension f xi = xi) = (xi = attracting_fixed_point f \<or> xi = repelling_fixed_point f)
[PROOF STEP]
have "xi = attracting_fixed_point f" if H: "Gromov_extension f xi = xi" "xi \<noteq> repelling_fixed_point f" for xi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xi = attracting_fixed_point f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xi = attracting_fixed_point f
[PROOF STEP]
have "((Gromov_extension f)^^n) xi = xi" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Gromov_extension f ^^ n) xi = xi
[PROOF STEP]
apply (induction n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (Gromov_extension f ^^ 0) xi = xi
 2. \<And>n. (Gromov_extension f ^^ n) xi = xi \<Longrightarrow> (Gromov_extension f ^^ Suc n) xi = xi
[PROOF STEP]
using H(1)
[PROOF STATE]
proof (prove)
using this:
Gromov_extension f xi = xi

goal (2 subgoals):
 1. (Gromov_extension f ^^ 0) xi = xi
 2. \<And>n. (Gromov_extension f ^^ n) xi = xi \<Longrightarrow> (Gromov_extension f ^^ Suc n) xi = xi
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Gromov_extension f ^^ ?n) xi = xi

goal (1 subgoal):
 1. xi = attracting_fixed_point f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(Gromov_extension f ^^ ?n) xi = xi
[PROOF STEP]
have "(\<lambda>n. ((Gromov_extension f)^^n) xi) \<longlonglongrightarrow> xi"
[PROOF STATE]
proof (prove)
using this:
(Gromov_extension f ^^ ?n) xi = xi

goal (1 subgoal):
 1. (\<lambda>n. (Gromov_extension f ^^ n) xi) \<longlonglongrightarrow> xi
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (Gromov_extension f ^^ n) xi) \<longlonglongrightarrow> xi

goal (1 subgoal):
 1. xi = attracting_fixed_point f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. (Gromov_extension f ^^ n) xi) \<longlonglongrightarrow> xi
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (Gromov_extension f ^^ n) xi) \<longlonglongrightarrow> xi

goal (1 subgoal):
 1. xi = attracting_fixed_point f
[PROOF STEP]
using loxodromic_attracting_fixed_point_attracts[OF assms H(2)] LIMSEQ_unique
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (Gromov_extension f ^^ n) xi) \<longlonglongrightarrow> xi
(\<lambda>n. (Gromov_extension f ^^ n) xi) \<longlonglongrightarrow> attracting_fixed_point f
\<lbrakk>?X \<longlonglongrightarrow> ?a; ?X \<longlonglongrightarrow> ?b\<rbrakk> \<Longrightarrow> ?a = ?b

goal (1 subgoal):
 1. xi = attracting_fixed_point f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xi = attracting_fixed_point f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>Gromov_extension f ?xi = ?xi; ?xi \<noteq> repelling_fixed_point f\<rbrakk> \<Longrightarrow> ?xi = attracting_fixed_point f

goal (1 subgoal):
 1. (Gromov_extension f xi = xi) = (xi = attracting_fixed_point f \<or> xi = repelling_fixed_point f)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Gromov_extension f ?xi = ?xi; ?xi \<noteq> repelling_fixed_point f\<rbrakk> \<Longrightarrow> ?xi = attracting_fixed_point f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Gromov_extension f ?xi = ?xi; ?xi \<noteq> repelling_fixed_point f\<rbrakk> \<Longrightarrow> ?xi = attracting_fixed_point f

goal (1 subgoal):
 1. (Gromov_extension f xi = xi) = (xi = attracting_fixed_point f \<or> xi = repelling_fixed_point f)
[PROOF STEP]
using loxodromic_attracting_fixed_point(2)[OF assms] loxodromic_repelling_fixed_point(2)[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Gromov_extension f ?xi = ?xi; ?xi \<noteq> repelling_fixed_point f\<rbrakk> \<Longrightarrow> ?xi = attracting_fixed_point f
Gromov_extension f (attracting_fixed_point f) = attracting_fixed_point f
Gromov_extension f (repelling_fixed_point f) = repelling_fixed_point f

goal (1 subgoal):
 1. (Gromov_extension f xi = xi) = (xi = attracting_fixed_point f \<or> xi = repelling_fixed_point f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Gromov_extension f xi = xi) = (xi = attracting_fixed_point f \<or> xi = repelling_fixed_point f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bounded_byI[intro]:
  "\<lbrakk> \<And>x. P x \<le> b \<rbrakk> \<Longrightarrow> bounded_by b P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. P x \<le> b) \<Longrightarrow> bounded_by b P
[PROOF STEP]
by (simp add:bounded_by_def)


[STATEMENT]
lemma bounded_byI2[intro]:
  "P \<le> (\<lambda>s. b) \<Longrightarrow> bounded_by b P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<le> (\<lambda>s. b) \<Longrightarrow> bounded_by b P
[PROOF STEP]
by (blast dest:le_funD)


[STATEMENT]
lemma bounded_byD[dest]:
  "bounded_by b P \<Longrightarrow> P x \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by b P \<Longrightarrow> P x \<le> b
[PROOF STEP]
by (simp add:bounded_by_def)


[STATEMENT]
lemma bounded_byD2[dest]:
  "bounded_by b P \<Longrightarrow> P \<le> (\<lambda>s. b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by b P \<Longrightarrow> P \<le> (\<lambda>s. b)
[PROOF STEP]
by (blast intro:le_funI)


[STATEMENT]
lemma bounded_bdd_above[intro]:
  assumes bP: "bounded P"
  shows "bdd_above (range P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above (range P)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> range P \<Longrightarrow> x \<le> ?M
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> range P \<Longrightarrow> x \<le> ?M
[PROOF STEP]
assume "x \<in> range P"
[PROOF STATE]
proof (state)
this:
x \<in> range P

goal (1 subgoal):
 1. \<And>x. x \<in> range P \<Longrightarrow> x \<le> ?M
[PROOF STEP]
with bP
[PROOF STATE]
proof (chain)
picking this:
Expectations.bounded P
x \<in> range P
[PROOF STEP]
show "x \<le> Inf {b. bounded_by b P}"
[PROOF STATE]
proof (prove)
using this:
Expectations.bounded P
x \<in> range P

goal (1 subgoal):
 1. x \<le> Inf {b. bounded_by b P}
[PROOF STEP]
unfolding bounded_def
[PROOF STATE]
proof (prove)
using this:
\<exists>b. bounded_by b P
x \<in> range P

goal (1 subgoal):
 1. x \<le> Inf {b. bounded_by b P}
[PROOF STEP]
by(auto intro:cInf_greatest)
[PROOF STATE]
proof (state)
this:
x \<le> Inf {b. bounded_by b P}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bound_of_least[intro]:
  assumes bP: "bounded_by b P"
  shows "bound_of P \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bound_of P \<le> b
[PROOF STEP]
unfolding bound_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup (range P) \<le> b
[PROOF STEP]
using bP
[PROOF STATE]
proof (prove)
using this:
bounded_by b P

goal (1 subgoal):
 1. Sup (range P) \<le> b
[PROOF STEP]
by(intro cSup_least, auto)


[STATEMENT]
lemma bounded_by_bound_of[intro!]:
  fixes P::"'a \<Rightarrow> real"
  assumes bP: "bounded P"
  shows "bounded_by (bound_of P) P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by (bound_of P) P
[PROOF STEP]
unfolding bound_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by (Sup (range P)) P
[PROOF STEP]
using bP
[PROOF STATE]
proof (prove)
using this:
Expectations.bounded P

goal (1 subgoal):
 1. bounded_by (Sup (range P)) P
[PROOF STEP]
by(intro bounded_byI cSup_upper bounded_bdd_above, auto)


[STATEMENT]
lemma bound_of_greater[intro]:
  "bounded P \<Longrightarrow> P x \<le> bound_of P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Expectations.bounded P \<Longrightarrow> P x \<le> bound_of P
[PROOF STEP]
by (blast intro:bounded_byD)


[STATEMENT]
lemma bounded_by_mono:
  "\<lbrakk> bounded_by a P; a \<le> b \<rbrakk> \<Longrightarrow> bounded_by b P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bounded_by a P; a \<le> b\<rbrakk> \<Longrightarrow> bounded_by b P
[PROOF STEP]
unfolding bounded_by_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. P x \<le> a; a \<le> b\<rbrakk> \<Longrightarrow> \<forall>x. P x \<le> b
[PROOF STEP]
by(blast intro:order_trans)


[STATEMENT]
lemma bounded_by_imp_bounded[intro]:
  "bounded_by b P \<Longrightarrow> bounded P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by b P \<Longrightarrow> Expectations.bounded P
[PROOF STEP]
unfolding bounded_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by b P \<Longrightarrow> \<exists>b. bounded_by b P
[PROOF STEP]
by(blast)


[STATEMENT]
lemma bounded_by_bound_of_alt:
  "\<lbrakk> bounded P; bound_of P = a \<rbrakk> \<Longrightarrow> bounded_by a P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Expectations.bounded P; bound_of P = a\<rbrakk> \<Longrightarrow> bounded_by a P
[PROOF STEP]
by (blast)


[STATEMENT]
lemma bounded_const[simp]:
  "bounded (\<lambda>x. c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Expectations.bounded (\<lambda>x. c)
[PROOF STEP]
by (blast)


[STATEMENT]
lemma bounded_by_const[intro]:
  "c \<le> b \<Longrightarrow> bounded_by b (\<lambda>x. c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<le> b \<Longrightarrow> bounded_by b (\<lambda>x. c)
[PROOF STEP]
by (blast)


[STATEMENT]
lemma bounded_by_mono_alt[intro]:
  "\<lbrakk> bounded_by b Q; P \<le> Q \<rbrakk> \<Longrightarrow> bounded_by b P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bounded_by b Q; P \<le> Q\<rbrakk> \<Longrightarrow> bounded_by b P
[PROOF STEP]
by (blast intro:order_trans dest:le_funD)


[STATEMENT]
lemma bound_of_const[simp, intro]:
  "bound_of (\<lambda>x. c) = (c::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bound_of (\<lambda>x. c) = c
[PROOF STEP]
unfolding bound_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SUP x. c) = c
[PROOF STEP]
by(intro antisym cSup_least cSup_upper bounded_bdd_above bounded_const, auto)


[STATEMENT]
lemma bound_of_leI:
  assumes "\<And>x. P x \<le> (c::real)"
  shows "bound_of P \<le> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bound_of P \<le> c
[PROOF STEP]
unfolding bound_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup (range P) \<le> c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P ?x \<le> c

goal (1 subgoal):
 1. Sup (range P) \<le> c
[PROOF STEP]
by(intro cSup_least, auto)


[STATEMENT]
lemma bound_of_mono[intro]:
  "\<lbrakk> P \<le> Q; bounded P; bounded Q \<rbrakk> \<Longrightarrow> bound_of P \<le> bound_of Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<le> Q; Expectations.bounded P; Expectations.bounded Q\<rbrakk> \<Longrightarrow> bound_of P \<le> bound_of Q
[PROOF STEP]
by (blast intro:order_trans dest:le_funD)


[STATEMENT]
lemma bounded_by_o[intro,simp]:
  "\<And>b. bounded_by b P \<Longrightarrow> bounded_by b (P o f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. bounded_by b P \<Longrightarrow> bounded_by b (P \<circ> f)
[PROOF STEP]
unfolding o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. bounded_by b P \<Longrightarrow> bounded_by b (\<lambda>x. P (f x))
[PROOF STEP]
by(blast)


[STATEMENT]
lemma le_bound_of[intro]:
  "\<And>x. bounded f \<Longrightarrow> f x \<le> bound_of f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. Expectations.bounded f \<Longrightarrow> f x \<le> bound_of f
[PROOF STEP]
by(blast)


[STATEMENT]
lemma nnegI[intro]:
  "\<lbrakk> \<And>x. 0 \<le> P x \<rbrakk> \<Longrightarrow> nneg P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. (0::'b) \<le> P x) \<Longrightarrow> nneg P
[PROOF STEP]
by (simp add:nneg_def)


[STATEMENT]
lemma nnegI2[intro]:
  "(\<lambda>s. 0) \<le> P \<Longrightarrow> nneg P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. 0::'b) \<le> P \<Longrightarrow> nneg P
[PROOF STEP]
by (blast dest:le_funD)


[STATEMENT]
lemma nnegD[dest]:
  "nneg P \<Longrightarrow> 0 \<le> P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nneg P \<Longrightarrow> (0::'b) \<le> P x
[PROOF STEP]
by (simp add:nneg_def)


[STATEMENT]
lemma nnegD2[dest]:
  "nneg P \<Longrightarrow> (\<lambda>s. 0) \<le> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nneg P \<Longrightarrow> (\<lambda>s. 0::'b) \<le> P
[PROOF STEP]
by (blast intro:le_funI)


[STATEMENT]
lemma nneg_bdd_below[intro]:
  "nneg P \<Longrightarrow> bdd_below (range P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nneg P \<Longrightarrow> bdd_below (range P)
[PROOF STEP]
by(auto)


[STATEMENT]
lemma nneg_const[iff]:
  "nneg (\<lambda>x. c) \<longleftrightarrow> 0 \<le> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nneg (\<lambda>x. c) = ((0::'b) \<le> c)
[PROOF STEP]
by (simp add:nneg_def)


[STATEMENT]
lemma nneg_o[intro,simp]:
  "nneg P \<Longrightarrow> nneg (P o f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nneg P \<Longrightarrow> nneg (P \<circ> f)
[PROOF STEP]
by (force)


[STATEMENT]
lemma nneg_bound_nneg[intro]:
  "\<lbrakk> bounded P; nneg P \<rbrakk> \<Longrightarrow> 0 \<le> bound_of P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Expectations.bounded P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> bound_of P
[PROOF STEP]
by (blast intro:order_trans)


[STATEMENT]
lemma nneg_bounded_by_nneg[dest]:
  "\<lbrakk> bounded_by b P; nneg P \<rbrakk> \<Longrightarrow> 0 \<le> (b::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> b
[PROOF STEP]
by (blast intro:order_trans)


[STATEMENT]
lemma bounded_by_nneg[dest]:
  fixes P::"'s \<Rightarrow> real"
  shows "\<lbrakk> bounded_by b P; nneg P \<rbrakk> \<Longrightarrow> 0 \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> 0 \<le> b
[PROOF STEP]
by (blast intro:order_trans)


[STATEMENT]
lemma soundI:
  "\<lbrakk> bounded P; nneg P \<rbrakk> \<Longrightarrow> sound P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Expectations.bounded P; nneg P\<rbrakk> \<Longrightarrow> sound P
[PROOF STEP]
by (simp add:sound_def)


[STATEMENT]
lemma soundI2[intro]:
  "\<lbrakk> bounded_by b P; nneg P \<rbrakk> \<Longrightarrow> sound P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bounded_by b P; nneg P\<rbrakk> \<Longrightarrow> sound P
[PROOF STEP]
by(blast intro:soundI)


[STATEMENT]
lemma sound_bounded[dest]:
  "sound P \<Longrightarrow> bounded P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound P \<Longrightarrow> Expectations.bounded P
[PROOF STEP]
by (simp add:sound_def)


[STATEMENT]
lemma sound_nneg[dest]:
  "sound P \<Longrightarrow> nneg P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound P \<Longrightarrow> nneg P
[PROOF STEP]
by (simp add:sound_def)


[STATEMENT]
lemma bound_of_sound[intro]:
  assumes sP: "sound P"
  shows "0 \<le> bound_of P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> bound_of P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sound P

goal (1 subgoal):
 1. 0 \<le> bound_of P
[PROOF STEP]
by(auto)


[STATEMENT]
lemma sound_sum[simp,intro]:
  assumes sP: "sound P" and sQ: "sound Q"
  shows "sound (\<lambda>s. P s + Q s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound (\<lambda>s. P s + Q s)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bounded_by ?b (\<lambda>s. P s + Q s)
 2. nneg (\<lambda>s. P s + Q s)
[PROOF STEP]
from sP
[PROOF STATE]
proof (chain)
picking this:
sound P
[PROOF STEP]
have "\<And>s. P s \<le> bound_of P"
[PROOF STATE]
proof (prove)
using this:
sound P

goal (1 subgoal):
 1. \<And>s. P s \<le> bound_of P
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
P ?s \<le> bound_of P

goal (2 subgoals):
 1. bounded_by ?b (\<lambda>s. P s + Q s)
 2. nneg (\<lambda>s. P s + Q s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P ?s \<le> bound_of P

goal (2 subgoals):
 1. bounded_by ?b (\<lambda>s. P s + Q s)
 2. nneg (\<lambda>s. P s + Q s)
[PROOF STEP]
from sQ
[PROOF STATE]
proof (chain)
picking this:
sound Q
[PROOF STEP]
have "\<And>s. Q s \<le> bound_of Q"
[PROOF STATE]
proof (prove)
using this:
sound Q

goal (1 subgoal):
 1. \<And>s. Q s \<le> bound_of Q
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
Q ?s \<le> bound_of Q

goal (2 subgoals):
 1. bounded_by ?b (\<lambda>s. P s + Q s)
 2. nneg (\<lambda>s. P s + Q s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P ?s \<le> bound_of P
Q ?s \<le> bound_of Q
[PROOF STEP]
have "\<And>s. P s + Q s \<le> bound_of P + bound_of Q"
[PROOF STATE]
proof (prove)
using this:
P ?s \<le> bound_of P
Q ?s \<le> bound_of Q

goal (1 subgoal):
 1. \<And>s. P s + Q s \<le> bound_of P + bound_of Q
[PROOF STEP]
by(rule add_mono)
[PROOF STATE]
proof (state)
this:
P ?s + Q ?s \<le> bound_of P + bound_of Q

goal (2 subgoals):
 1. bounded_by ?b (\<lambda>s. P s + Q s)
 2. nneg (\<lambda>s. P s + Q s)
[PROOF STEP]
thus "bounded_by (bound_of P + bound_of Q) (\<lambda>s. P s + Q s)"
[PROOF STATE]
proof (prove)
using this:
P ?s + Q ?s \<le> bound_of P + bound_of Q

goal (1 subgoal):
 1. bounded_by (bound_of P + bound_of Q) (\<lambda>s. P s + Q s)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
bounded_by (bound_of P + bound_of Q) (\<lambda>s. P s + Q s)

goal (1 subgoal):
 1. nneg (\<lambda>s. P s + Q s)
[PROOF STEP]
from sP
[PROOF STATE]
proof (chain)
picking this:
sound P
[PROOF STEP]
have "\<And>s. 0 \<le> P s"
[PROOF STATE]
proof (prove)
using this:
sound P

goal (1 subgoal):
 1. \<And>s. 0 \<le> P s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
0 \<le> P ?s

goal (1 subgoal):
 1. nneg (\<lambda>s. P s + Q s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> P ?s

goal (1 subgoal):
 1. nneg (\<lambda>s. P s + Q s)
[PROOF STEP]
from sQ
[PROOF STATE]
proof (chain)
picking this:
sound Q
[PROOF STEP]
have "\<And>s. 0 \<le> Q s"
[PROOF STATE]
proof (prove)
using this:
sound Q

goal (1 subgoal):
 1. \<And>s. 0 \<le> Q s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
0 \<le> Q ?s

goal (1 subgoal):
 1. nneg (\<lambda>s. P s + Q s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 \<le> P ?s
0 \<le> Q ?s
[PROOF STEP]
have "\<And>s. 0 \<le> P s + Q s"
[PROOF STATE]
proof (prove)
using this:
0 \<le> P ?s
0 \<le> Q ?s

goal (1 subgoal):
 1. \<And>s. 0 \<le> P s + Q s
[PROOF STEP]
by(simp add:add_mono)
[PROOF STATE]
proof (state)
this:
0 \<le> P ?s + Q ?s

goal (1 subgoal):
 1. nneg (\<lambda>s. P s + Q s)
[PROOF STEP]
thus "nneg (\<lambda>s. P s + Q s)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> P ?s + Q ?s

goal (1 subgoal):
 1. nneg (\<lambda>s. P s + Q s)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
nneg (\<lambda>s. P s + Q s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_sound:
  assumes sP: "sound P" and sQ: "sound Q"
  shows "sound (\<lambda>s. P s * Q s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound (\<lambda>s. P s * Q s)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bounded_by ?b (\<lambda>s. P s * Q s)
 2. nneg (\<lambda>s. P s * Q s)
[PROOF STEP]
from sP
[PROOF STATE]
proof (chain)
picking this:
sound P
[PROOF STEP]
have "\<And>s. P s \<le> bound_of P"
[PROOF STATE]
proof (prove)
using this:
sound P

goal (1 subgoal):
 1. \<And>s. P s \<le> bound_of P
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
P ?s \<le> bound_of P

goal (2 subgoals):
 1. bounded_by ?b (\<lambda>s. P s * Q s)
 2. nneg (\<lambda>s. P s * Q s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P ?s \<le> bound_of P

goal (2 subgoals):
 1. bounded_by ?b (\<lambda>s. P s * Q s)
 2. nneg (\<lambda>s. P s * Q s)
[PROOF STEP]
from sQ
[PROOF STATE]
proof (chain)
picking this:
sound Q
[PROOF STEP]
have "\<And>s. Q s \<le> bound_of Q"
[PROOF STATE]
proof (prove)
using this:
sound Q

goal (1 subgoal):
 1. \<And>s. Q s \<le> bound_of Q
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
Q ?s \<le> bound_of Q

goal (2 subgoals):
 1. bounded_by ?b (\<lambda>s. P s * Q s)
 2. nneg (\<lambda>s. P s * Q s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P ?s \<le> bound_of P
Q ?s \<le> bound_of Q
[PROOF STEP]
have "\<And>s. P s * Q s \<le> bound_of P * bound_of Q"
[PROOF STATE]
proof (prove)
using this:
P ?s \<le> bound_of P
Q ?s \<le> bound_of Q

goal (1 subgoal):
 1. \<And>s. P s * Q s \<le> bound_of P * bound_of Q
[PROOF STEP]
using sP and sQ
[PROOF STATE]
proof (prove)
using this:
P ?s \<le> bound_of P
Q ?s \<le> bound_of Q
sound P
sound Q

goal (1 subgoal):
 1. \<And>s. P s * Q s \<le> bound_of P * bound_of Q
[PROOF STEP]
by(blast intro:mult_mono)
[PROOF STATE]
proof (state)
this:
P ?s * Q ?s \<le> bound_of P * bound_of Q

goal (2 subgoals):
 1. bounded_by ?b (\<lambda>s. P s * Q s)
 2. nneg (\<lambda>s. P s * Q s)
[PROOF STEP]
thus "bounded_by (bound_of P * bound_of Q) (\<lambda>s. P s * Q s)"
[PROOF STATE]
proof (prove)
using this:
P ?s * Q ?s \<le> bound_of P * bound_of Q

goal (1 subgoal):
 1. bounded_by (bound_of P * bound_of Q) (\<lambda>s. P s * Q s)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
bounded_by (bound_of P * bound_of Q) (\<lambda>s. P s * Q s)

goal (1 subgoal):
 1. nneg (\<lambda>s. P s * Q s)
[PROOF STEP]
from sP and sQ
[PROOF STATE]
proof (chain)
picking this:
sound P
sound Q
[PROOF STEP]
show "nneg (\<lambda>s. P s * Q s)"
[PROOF STATE]
proof (prove)
using this:
sound P
sound Q

goal (1 subgoal):
 1. nneg (\<lambda>s. P s * Q s)
[PROOF STEP]
by(blast intro:mult_nonneg_nonneg)
[PROOF STATE]
proof (state)
this:
nneg (\<lambda>s. P s * Q s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma div_sound:
  assumes sP: "sound P" and cpos: "0 < c"
  shows "sound (\<lambda>s. P s / c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound (\<lambda>s. P s / c)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bounded_by ?b (\<lambda>s. P s / c)
 2. nneg (\<lambda>s. P s / c)
[PROOF STEP]
from sP and cpos
[PROOF STATE]
proof (chain)
picking this:
sound P
0 < c
[PROOF STEP]
have "\<And>s. P s / c \<le> bound_of P / c"
[PROOF STATE]
proof (prove)
using this:
sound P
0 < c

goal (1 subgoal):
 1. \<And>s. P s / c \<le> bound_of P / c
[PROOF STEP]
by(blast intro:divide_right_mono less_imp_le)
[PROOF STATE]
proof (state)
this:
P ?s / c \<le> bound_of P / c

goal (2 subgoals):
 1. bounded_by ?b (\<lambda>s. P s / c)
 2. nneg (\<lambda>s. P s / c)
[PROOF STEP]
thus "bounded_by (bound_of P / c) (\<lambda>s. P s / c)"
[PROOF STATE]
proof (prove)
using this:
P ?s / c \<le> bound_of P / c

goal (1 subgoal):
 1. bounded_by (bound_of P / c) (\<lambda>s. P s / c)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
bounded_by (bound_of P / c) (\<lambda>s. P s / c)

goal (1 subgoal):
 1. nneg (\<lambda>s. P s / c)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
sound P
0 < c
[PROOF STEP]
show "nneg (\<lambda>s. P s / c)"
[PROOF STATE]
proof (prove)
using this:
sound P
0 < c

goal (1 subgoal):
 1. nneg (\<lambda>s. P s / c)
[PROOF STEP]
by(blast intro:divide_nonneg_pos)
[PROOF STATE]
proof (state)
this:
nneg (\<lambda>s. P s / c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tminus_sound:
  assumes sP: "sound P" and nnc: "0 \<le> c"
  shows "sound (\<lambda>s. P s \<ominus> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound (\<lambda>s. P s \<ominus> c)
[PROOF STEP]
proof(rule soundI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Expectations.bounded (\<lambda>s. P s \<ominus> c)
 2. nneg (\<lambda>s. P s \<ominus> c)
[PROOF STEP]
from sP
[PROOF STATE]
proof (chain)
picking this:
sound P
[PROOF STEP]
have "\<And>s. P s \<le> bound_of P"
[PROOF STATE]
proof (prove)
using this:
sound P

goal (1 subgoal):
 1. \<And>s. P s \<le> bound_of P
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
P ?s \<le> bound_of P

goal (2 subgoals):
 1. Expectations.bounded (\<lambda>s. P s \<ominus> c)
 2. nneg (\<lambda>s. P s \<ominus> c)
[PROOF STEP]
with nnc
[PROOF STATE]
proof (chain)
picking this:
0 \<le> c
P ?s \<le> bound_of P
[PROOF STEP]
have "\<And>s. P s \<ominus> c \<le> bound_of P \<ominus> c"
[PROOF STATE]
proof (prove)
using this:
0 \<le> c
P ?s \<le> bound_of P

goal (1 subgoal):
 1. \<And>s. P s \<ominus> c \<le> bound_of P \<ominus> c
[PROOF STEP]
by(blast intro:tminus_left_mono)
[PROOF STATE]
proof (state)
this:
P ?s \<ominus> c \<le> bound_of P \<ominus> c

goal (2 subgoals):
 1. Expectations.bounded (\<lambda>s. P s \<ominus> c)
 2. nneg (\<lambda>s. P s \<ominus> c)
[PROOF STEP]
thus "bounded (\<lambda>s. P s \<ominus> c)"
[PROOF STATE]
proof (prove)
using this:
P ?s \<ominus> c \<le> bound_of P \<ominus> c

goal (1 subgoal):
 1. Expectations.bounded (\<lambda>s. P s \<ominus> c)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
Expectations.bounded (\<lambda>s. P s \<ominus> c)

goal (1 subgoal):
 1. nneg (\<lambda>s. P s \<ominus> c)
[PROOF STEP]
show "nneg (\<lambda>s. P s \<ominus> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nneg (\<lambda>s. P s \<ominus> c)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
nneg (\<lambda>s. P s \<ominus> c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma const_sound:
  "0 \<le> c \<Longrightarrow> sound (\<lambda>s. c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> c \<Longrightarrow> sound (\<lambda>s. c)
[PROOF STEP]
by (blast)


[STATEMENT]
lemma sound_o[intro,simp]:
  "sound P \<Longrightarrow> sound (P o f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound P \<Longrightarrow> sound (P \<circ> f)
[PROOF STEP]
unfolding o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound P \<Longrightarrow> sound (\<lambda>x. P (f x))
[PROOF STEP]
by(blast)


[STATEMENT]
lemma sc_bounded_by[intro,simp]:
  "\<lbrakk> sound P; 0 \<le> c \<rbrakk> \<Longrightarrow> bounded_by (c * bound_of P) (\<lambda>x. c * P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> bounded_by (c * bound_of P) (\<lambda>x. c * P x)
[PROOF STEP]
by(blast intro!:mult_left_mono)


[STATEMENT]
lemma sc_bounded[intro,simp]:
  assumes sP:  "sound P" and pos: "0 \<le> c"
  shows "bounded (\<lambda>x. c * P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Expectations.bounded (\<lambda>x. c * P x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sound P
0 \<le> c

goal (1 subgoal):
 1. Expectations.bounded (\<lambda>x. c * P x)
[PROOF STEP]
by(blast)


[STATEMENT]
lemma sc_bound[simp]:
  assumes sP: "sound P"
      and cnn: "0 \<le> c"
  shows "c * bound_of P = bound_of (\<lambda>x. c * P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * bound_of P = bound_of (\<lambda>x. c * P x)
[PROOF STEP]
proof(cases "c = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c = 0 \<Longrightarrow> c * bound_of P = bound_of (\<lambda>x. c * P x)
 2. c \<noteq> 0 \<Longrightarrow> c * bound_of P = bound_of (\<lambda>x. c * P x)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
c = 0

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> c * bound_of P = bound_of (\<lambda>x. c * P x)
 2. c \<noteq> 0 \<Longrightarrow> c * bound_of P = bound_of (\<lambda>x. c * P x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0

goal (1 subgoal):
 1. c * bound_of P = bound_of (\<lambda>x. c * P x)
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
c * bound_of P = bound_of (\<lambda>x. c * P x)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> c * bound_of P = bound_of (\<lambda>x. c * P x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> c * bound_of P = bound_of (\<lambda>x. c * P x)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
c \<noteq> 0

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> c * bound_of P = bound_of (\<lambda>x. c * P x)
[PROOF STEP]
with cnn
[PROOF STATE]
proof (chain)
picking this:
0 \<le> c
c \<noteq> 0
[PROOF STEP]
have cpos: "0 < c"
[PROOF STATE]
proof (prove)
using this:
0 \<le> c
c \<noteq> 0

goal (1 subgoal):
 1. 0 < c
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
0 < c

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> c * bound_of P = bound_of (\<lambda>x. c * P x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * bound_of P = bound_of (\<lambda>x. c * P x)
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c * bound_of P \<le> bound_of (\<lambda>x. c * P x)
 2. bound_of (\<lambda>x. c * P x) \<le> c * bound_of P
[PROOF STEP]
from sP and cnn
[PROOF STATE]
proof (chain)
picking this:
sound P
0 \<le> c
[PROOF STEP]
have "bounded (\<lambda>x. c * P x)"
[PROOF STATE]
proof (prove)
using this:
sound P
0 \<le> c

goal (1 subgoal):
 1. Expectations.bounded (\<lambda>x. c * P x)
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
Expectations.bounded (\<lambda>x. c * P x)

goal (2 subgoals):
 1. c * bound_of P \<le> bound_of (\<lambda>x. c * P x)
 2. bound_of (\<lambda>x. c * P x) \<le> c * bound_of P
[PROOF STEP]
hence "\<And>x. c * P x \<le> bound_of (\<lambda>x. c * P x)"
[PROOF STATE]
proof (prove)
using this:
Expectations.bounded (\<lambda>x. c * P x)

goal (1 subgoal):
 1. \<And>x. c * P x \<le> bound_of (\<lambda>x. c * P x)
[PROOF STEP]
by(rule le_bound_of)
[PROOF STATE]
proof (state)
this:
c * P ?x \<le> bound_of (\<lambda>x. c * P x)

goal (2 subgoals):
 1. c * bound_of P \<le> bound_of (\<lambda>x. c * P x)
 2. bound_of (\<lambda>x. c * P x) \<le> c * bound_of P
[PROOF STEP]
with cpos
[PROOF STATE]
proof (chain)
picking this:
0 < c
c * P ?x \<le> bound_of (\<lambda>x. c * P x)
[PROOF STEP]
have "\<And>x. P x \<le> inverse c * bound_of (\<lambda>x. c * P x)"
[PROOF STATE]
proof (prove)
using this:
0 < c
c * P ?x \<le> bound_of (\<lambda>x. c * P x)

goal (1 subgoal):
 1. \<And>x. P x \<le> inverse c * bound_of (\<lambda>x. c * P x)
[PROOF STEP]
by(force intro:mult_div_mono_right)
[PROOF STATE]
proof (state)
this:
P ?x \<le> inverse c * bound_of (\<lambda>x. c * P x)

goal (2 subgoals):
 1. c * bound_of P \<le> bound_of (\<lambda>x. c * P x)
 2. bound_of (\<lambda>x. c * P x) \<le> c * bound_of P
[PROOF STEP]
hence "bound_of P \<le> inverse c * bound_of (\<lambda>x. c * P x)"
[PROOF STATE]
proof (prove)
using this:
P ?x \<le> inverse c * bound_of (\<lambda>x. c * P x)

goal (1 subgoal):
 1. bound_of P \<le> inverse c * bound_of (\<lambda>x. c * P x)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
bound_of P \<le> inverse c * bound_of (\<lambda>x. c * P x)

goal (2 subgoals):
 1. c * bound_of P \<le> bound_of (\<lambda>x. c * P x)
 2. bound_of (\<lambda>x. c * P x) \<le> c * bound_of P
[PROOF STEP]
with cpos
[PROOF STATE]
proof (chain)
picking this:
0 < c
bound_of P \<le> inverse c * bound_of (\<lambda>x. c * P x)
[PROOF STEP]
show "c * bound_of P \<le> bound_of (\<lambda>x. c * P x)"
[PROOF STATE]
proof (prove)
using this:
0 < c
bound_of P \<le> inverse c * bound_of (\<lambda>x. c * P x)

goal (1 subgoal):
 1. c * bound_of P \<le> bound_of (\<lambda>x. c * P x)
[PROOF STEP]
by(force intro:mult_div_mono_left)
[PROOF STATE]
proof (state)
this:
c * bound_of P \<le> bound_of (\<lambda>x. c * P x)

goal (1 subgoal):
 1. bound_of (\<lambda>x. c * P x) \<le> c * bound_of P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bound_of (\<lambda>x. c * P x) \<le> c * bound_of P
[PROOF STEP]
from sP and cpos
[PROOF STATE]
proof (chain)
picking this:
sound P
0 < c
[PROOF STEP]
have "\<And>x. c * P x \<le> c * bound_of P"
[PROOF STATE]
proof (prove)
using this:
sound P
0 < c

goal (1 subgoal):
 1. \<And>x. c * P x \<le> c * bound_of P
[PROOF STEP]
by(blast intro:mult_left_mono less_imp_le)
[PROOF STATE]
proof (state)
this:
c * P ?x \<le> c * bound_of P

goal (1 subgoal):
 1. bound_of (\<lambda>x. c * P x) \<le> c * bound_of P
[PROOF STEP]
thus "bound_of (\<lambda>x. c * P x) \<le> c * bound_of P"
[PROOF STATE]
proof (prove)
using this:
c * P ?x \<le> c * bound_of P

goal (1 subgoal):
 1. bound_of (\<lambda>x. c * P x) \<le> c * bound_of P
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
bound_of (\<lambda>x. c * P x) \<le> c * bound_of P

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c * bound_of P = bound_of (\<lambda>x. c * P x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sc_sound:
  "\<lbrakk> sound P; 0 \<le> c \<rbrakk> \<Longrightarrow> sound (\<lambda>s. c * P s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sound P; 0 \<le> c\<rbrakk> \<Longrightarrow> sound (\<lambda>s. c * P s)
[PROOF STEP]
by (blast intro:mult_nonneg_nonneg)


[STATEMENT]
lemma bounded_by_mult:
  assumes sP: "sound P" and bP: "bounded_by a P"
      and sQ: "sound Q" and bQ: "bounded_by b Q"
  shows "bounded_by (a * b) (\<lambda>s. P s * Q s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by (a * b) (\<lambda>s. P s * Q s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sound P
bounded_by a P
sound Q
bounded_by b Q

goal (1 subgoal):
 1. bounded_by (a * b) (\<lambda>s. P s * Q s)
[PROOF STEP]
by(intro bounded_byI, auto intro:mult_mono)


[STATEMENT]
lemma bounded_by_add:
  fixes P::"'s \<Rightarrow> real" and Q
  assumes bP: "bounded_by a P"
      and bQ: "bounded_by b Q"
  shows "bounded_by (a + b) (\<lambda>s. P s + Q s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by (a + b) (\<lambda>s. P s + Q s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bounded_by a P
bounded_by b Q

goal (1 subgoal):
 1. bounded_by (a + b) (\<lambda>s. P s + Q s)
[PROOF STEP]
by(intro bounded_byI, auto intro:add_mono)


[STATEMENT]
lemma sound_unit[intro!,simp]:
  "sound (\<lambda>s. 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound (\<lambda>s. 1)
[PROOF STEP]
by(auto)


[STATEMENT]
lemma unit_mult[intro]:
  assumes sP: "sound P" and bP: "bounded_by 1 P"
      and sQ: "sound Q" and bQ: "bounded_by 1 Q"
  shows "bounded_by 1 (\<lambda>s. P s * Q s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by 1 (\<lambda>s. P s * Q s)
[PROOF STEP]
proof(rule bounded_byI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. P x * Q x \<le> 1
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. P x * Q x \<le> 1
[PROOF STEP]
have "P s * Q s \<le> 1 * 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P s * Q s \<le> 1 * 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sound P
bounded_by 1 P
sound Q
bounded_by 1 Q

goal (1 subgoal):
 1. P s * Q s \<le> 1 * 1
[PROOF STEP]
by(blast dest:bounded_by_mult)
[PROOF STATE]
proof (state)
this:
P s * Q s \<le> 1 * 1

goal (1 subgoal):
 1. \<And>x. P x * Q x \<le> 1
[PROOF STEP]
thus "P s * Q s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
P s * Q s \<le> 1 * 1

goal (1 subgoal):
 1. P s * Q s \<le> 1
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
P s * Q s \<le> 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_sound:
  assumes sP: "\<forall>x\<in>S. sound (P x)"
  shows "sound (\<lambda>s. \<Sum>x\<in>S. P x s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound (\<lambda>s. \<Sum>x\<in>S. P x s)
[PROOF STEP]
proof(rule soundI2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bounded_by ?b (\<lambda>s. \<Sum>x\<in>S. P x s)
 2. nneg (\<lambda>s. \<Sum>x\<in>S. P x s)
[PROOF STEP]
from sP
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>S. sound (P x)
[PROOF STEP]
show "bounded_by (\<Sum>x\<in>S. bound_of (P x)) (\<lambda>s. \<Sum>x\<in>S. P x s)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. sound (P x)

goal (1 subgoal):
 1. bounded_by (\<Sum>x\<in>S. bound_of (P x)) (\<lambda>s. \<Sum>x\<in>S. P x s)
[PROOF STEP]
by(auto intro!:sum_mono)
[PROOF STATE]
proof (state)
this:
bounded_by (\<Sum>x\<in>S. bound_of (P x)) (\<lambda>s. \<Sum>x\<in>S. P x s)

goal (1 subgoal):
 1. nneg (\<lambda>s. \<Sum>x\<in>S. P x s)
[PROOF STEP]
from sP
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>S. sound (P x)
[PROOF STEP]
show "nneg (\<lambda>s. \<Sum>x\<in>S. P x s)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. sound (P x)

goal (1 subgoal):
 1. nneg (\<lambda>s. \<Sum>x\<in>S. P x s)
[PROOF STEP]
by(auto intro!:sum_nonneg)
[PROOF STATE]
proof (state)
this:
nneg (\<lambda>s. \<Sum>x\<in>S. P x s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unitaryI[intro]:
  "\<lbrakk> sound P; bounded_by 1 P \<rbrakk> \<Longrightarrow> unitary P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sound P; bounded_by 1 P\<rbrakk> \<Longrightarrow> unitary P
[PROOF STEP]
by(simp add:unitary_def)


[STATEMENT]
lemma unitaryI2:
  "\<lbrakk> nneg P; bounded_by 1 P \<rbrakk> \<Longrightarrow> unitary P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nneg P; bounded_by 1 P\<rbrakk> \<Longrightarrow> unitary P
[PROOF STEP]
by(auto)


[STATEMENT]
lemma unitary_sound[dest]:
  "unitary P \<Longrightarrow> sound P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary P \<Longrightarrow> sound P
[PROOF STEP]
by(simp add:unitary_def)


[STATEMENT]
lemma unitary_bound[dest]:
  "unitary P \<Longrightarrow> bounded_by 1 P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary P \<Longrightarrow> bounded_by 1 P
[PROOF STEP]
by(simp add:unitary_def)


[STATEMENT]
lemma embed_bool_nneg[simp,intro]:
  "nneg \<guillemotleft>P\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nneg \<guillemotleft> P \<guillemotright>
[PROOF STEP]
unfolding embed_bool_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nneg (\<lambda>s. if P s then 1 else 0)
[PROOF STEP]
by(force)


[STATEMENT]
lemma embed_bool_bounded_by_1[simp,intro]:
  "bounded_by 1 \<guillemotleft>P\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by 1 \<guillemotleft> P \<guillemotright>
[PROOF STEP]
unfolding embed_bool_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by 1 (\<lambda>s. if P s then 1 else 0)
[PROOF STEP]
by(force)


[STATEMENT]
lemma embed_bool_bounded[simp,intro]:
  "bounded \<guillemotleft>P\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Expectations.bounded \<guillemotleft> P \<guillemotright>
[PROOF STEP]
by (blast)


[STATEMENT]
lemma embed_bool_idem:
  "\<guillemotleft>P\<guillemotright> s * \<guillemotleft>P\<guillemotright> s = \<guillemotleft>P\<guillemotright> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> P \<guillemotright> s * \<guillemotleft> P \<guillemotright> s = \<guillemotleft> P \<guillemotright> s
[PROOF STEP]
by (simp add:embed_bool_def)


[STATEMENT]
lemma eval_embed_true[simp]:
  "P s \<Longrightarrow> \<guillemotleft>P\<guillemotright> s = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P s \<Longrightarrow> \<guillemotleft> P \<guillemotright> s = 1
[PROOF STEP]
by (simp add:embed_bool_def)


[STATEMENT]
lemma eval_embed_false[simp]:
  "\<not>P s \<Longrightarrow> \<guillemotleft>P\<guillemotright> s = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> P s \<Longrightarrow> \<guillemotleft> P \<guillemotright> s = 0
[PROOF STEP]
by (simp add:embed_bool_def)


[STATEMENT]
lemma embed_ge_0[simp,intro]:
  "0 \<le> \<guillemotleft>G\<guillemotright> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> \<guillemotleft> G \<guillemotright> s
[PROOF STEP]
by (simp add:embed_bool_def)


[STATEMENT]
lemma embed_le_1[simp,intro]:
  "\<guillemotleft>G\<guillemotright> s \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> s \<le> 1
[PROOF STEP]
by(simp add:embed_bool_def)


[STATEMENT]
lemma embed_le_1_alt[simp,intro]:
  "0 \<le> 1 - \<guillemotleft>G\<guillemotright> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> 1 - \<guillemotleft> G \<guillemotright> s
[PROOF STEP]
by(subst add_le_cancel_right[where c="\<guillemotleft>G\<guillemotright> s", symmetric], simp)


[STATEMENT]
lemma expect_1_I:
  "P x \<Longrightarrow> 1 \<le> \<guillemotleft>P\<guillemotright> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P x \<Longrightarrow> 1 \<le> \<guillemotleft> P \<guillemotright> x
[PROOF STEP]
by(simp)


[STATEMENT]
lemma standard_sound[intro,simp]:
  "sound \<guillemotleft>P\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound \<guillemotleft> P \<guillemotright>
[PROOF STEP]
by(blast)


[STATEMENT]
lemma embed_o[simp]:
  "\<guillemotleft>P\<guillemotright> o f = \<guillemotleft>P o f\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> P \<guillemotright> \<circ> f = \<guillemotleft> P \<circ> f \<guillemotright>
[PROOF STEP]
unfolding embed_bool_def o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if P (f x) then 1 else 0) = (\<lambda>s. if P (f s) then 1 else 0)
[PROOF STEP]
by(simp)


[STATEMENT]
lemma negateI:
  "\<not> P s \<Longrightarrow> \<N> P s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> P s \<Longrightarrow> \<N> P s
[PROOF STEP]
by (simp add:negate_def)


[STATEMENT]
lemma embed_split:
  "f s = \<guillemotleft>P\<guillemotright> s * f s + \<guillemotleft>\<N> P\<guillemotright> s * f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f s = \<guillemotleft> P \<guillemotright> s * f s + \<guillemotleft> \<N> P \<guillemotright> s * f s
[PROOF STEP]
by (simp add:negate_def embed_bool_def)


[STATEMENT]
lemma negate_embed:
  "\<guillemotleft>\<N> P\<guillemotright> s = 1 - \<guillemotleft>P\<guillemotright> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> \<N> P \<guillemotright> s = 1 - \<guillemotleft> P \<guillemotright> s
[PROOF STEP]
by (simp add:embed_bool_def negate_def)


[STATEMENT]
lemma eval_nembed_true[simp]:
  "P s \<Longrightarrow> \<guillemotleft>\<N> P\<guillemotright> s = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P s \<Longrightarrow> \<guillemotleft> \<N> P \<guillemotright> s = 0
[PROOF STEP]
by (simp add:embed_bool_def negate_def)


[STATEMENT]
lemma eval_nembed_false[simp]:
  "\<not>P s \<Longrightarrow> \<guillemotleft>\<N> P\<guillemotright> s = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> P s \<Longrightarrow> \<guillemotleft> \<N> P \<guillemotright> s = 1
[PROOF STEP]
by (simp add:embed_bool_def negate_def)


[STATEMENT]
lemma negate_Not[simp]:
  "\<N> Not = (\<lambda>x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<N> Not = (\<lambda>x. x)
[PROOF STEP]
by(simp add:negate_def)


[STATEMENT]
lemma negate_negate[simp]:
  "\<N> (\<N> P) = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<N> (\<N> P) = P
[PROOF STEP]
by(simp add:negate_def)


[STATEMENT]
lemma embed_bool_cancel:
  "\<guillemotleft>G\<guillemotright> s * \<guillemotleft>\<N> G\<guillemotright> s = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> G \<guillemotright> s * \<guillemotleft> \<N> G \<guillemotright> s = 0
[PROOF STEP]
by(cases "G s", simp_all)


[STATEMENT]
lemma entailsI[intro]:
  "\<lbrakk>\<And>s. P s \<le> Q s\<rbrakk> \<Longrightarrow> P \<tturnstile> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<le> Q s) \<Longrightarrow> P \<tturnstile> Q
[PROOF STEP]
by(simp add:le_funI)


[STATEMENT]
lemma entailsD[dest]:
  "P \<tturnstile> Q \<Longrightarrow> P s \<le> Q s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<tturnstile> Q \<Longrightarrow> P s \<le> Q s
[PROOF STEP]
by(simp add:le_funD)


[STATEMENT]
lemma eq_entails[intro]:
  "P = Q \<Longrightarrow> P \<tturnstile> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P = Q \<Longrightarrow> P \<tturnstile> Q
[PROOF STEP]
by(blast)


[STATEMENT]
lemma entails_trans[trans]:
  "\<lbrakk> P \<tturnstile> Q; Q \<tturnstile> R \<rbrakk> \<Longrightarrow> P \<tturnstile> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<tturnstile> Q; Q \<tturnstile> R\<rbrakk> \<Longrightarrow> P \<tturnstile> R
[PROOF STEP]
by(blast intro:order_trans)


[STATEMENT]
lemma implies_entails:
  "\<lbrakk> \<And>s. P s \<Longrightarrow> Q s \<rbrakk> \<Longrightarrow> \<guillemotleft>P\<guillemotright> \<tturnstile> \<guillemotleft>Q\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> Q s) \<Longrightarrow> \<guillemotleft> P \<guillemotright> \<tturnstile> \<guillemotleft> Q \<guillemotright>
[PROOF STEP]
by(rule entailsI, case_tac "P s", simp_all)


[STATEMENT]
lemma entails_implies:
  "\<And>s. \<lbrakk> \<guillemotleft>P\<guillemotright> \<tturnstile> \<guillemotleft>Q\<guillemotright>; P s \<rbrakk> \<Longrightarrow> Q s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<guillemotleft> P \<guillemotright> \<tturnstile> \<guillemotleft> Q \<guillemotright>; P s\<rbrakk> \<Longrightarrow> Q s
[PROOF STEP]
by(rule ccontr, drule_tac s=s in entailsD, simp)


[STATEMENT]
lemma pconj_lzero[intro,simp]:
  "b \<le> 1 \<Longrightarrow> 0 .& b = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<le> 1 \<Longrightarrow> 0 .& b = 0
[PROOF STEP]
by(simp add:pconj_def tminus_def)


[STATEMENT]
lemma pconj_rzero[intro,simp]:
  "b \<le> 1 \<Longrightarrow> b .& 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<le> 1 \<Longrightarrow> b .& 0 = 0
[PROOF STEP]
by(simp add:pconj_def tminus_def)


[STATEMENT]
lemma pconj_lone[intro,simp]:
  "0 \<le> b \<Longrightarrow> 1 .& b = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> b \<Longrightarrow> 1 .& b = b
[PROOF STEP]
by(simp add:pconj_def tminus_def)


[STATEMENT]
lemma pconj_rone[intro,simp]:
  "0 \<le> b \<Longrightarrow> b .& 1 = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> b \<Longrightarrow> b .& 1 = b
[PROOF STEP]
by(simp add:pconj_def tminus_def)


[STATEMENT]
lemma pconj_bconj:
  "\<guillemotleft>a\<guillemotright> s .& \<guillemotleft>b\<guillemotright> s = \<guillemotleft>\<lambda>s. a s \<and> b s\<guillemotright> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> a \<guillemotright> s .& \<guillemotleft> b \<guillemotright> s = \<guillemotleft> \<lambda>s. a s \<and> b s \<guillemotright> s
[PROOF STEP]
unfolding embed_bool_def pconj_def tminus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max ((if a s then 1 else 0) + (if b s then 1 else 0) - 1) 0 = (if a s \<and> b s then 1 else 0)
[PROOF STEP]
by(force)


[STATEMENT]
lemma pconj_comm[ac_simps]:
  "a .& b = b .& a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a .& b = b .& a
[PROOF STEP]
by(simp add:pconj_def ac_simps)


[STATEMENT]
lemma pconj_assoc:
  "\<lbrakk> 0 \<le> a; a \<le> 1; 0 \<le> b; b \<le> 1; 0 \<le> c; c \<le> 1 \<rbrakk> \<Longrightarrow>
   a .& (b .& c) = (a .& b) .& c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; a \<le> 1; 0 \<le> b; b \<le> 1; 0 \<le> c; c \<le> 1\<rbrakk> \<Longrightarrow> a .& (b .& c) = a .& b .& c
[PROOF STEP]
unfolding pconj_def tminus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; a \<le> 1; 0 \<le> b; b \<le> 1; 0 \<le> c; c \<le> 1\<rbrakk> \<Longrightarrow> max (a + max (b + c - 1) 0 - 1) 0 = max (max (a + b - 1) 0 + c - 1) 0
[PROOF STEP]
by(simp)


[STATEMENT]
lemma pconj_mono:
  "\<lbrakk> a \<le> b; c \<le> d \<rbrakk> \<Longrightarrow> a .& c \<le> b .& d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; c \<le> d\<rbrakk> \<Longrightarrow> a .& c \<le> b .& d
[PROOF STEP]
unfolding pconj_def tminus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; c \<le> d\<rbrakk> \<Longrightarrow> max (a + c - 1) 0 \<le> max (b + d - 1) 0
[PROOF STEP]
by(simp)


[STATEMENT]
lemma pconj_nneg[intro,simp]:
  "0 \<le> a .& b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> a .& b
[PROOF STEP]
unfolding pconj_def tminus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> max (a + b - 1) 0
[PROOF STEP]
by(auto)


[STATEMENT]
lemma min_pconj:
  "(min a b) .& (min c d) \<le> min (a .& c) (b .& d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min a b .& min c d \<le> min (a .& c) (b .& d)
[PROOF STEP]
by(cases "a \<le> b",
     (cases "c \<le> d",
      simp_all add:min.absorb1 min.absorb2 pconj_mono)[],
     (cases "c \<le> d",
      simp_all add:min.absorb1 min.absorb2 pconj_mono))


[STATEMENT]
lemma pconj_less_one[simp]:
  "a + b < 1 \<Longrightarrow> a .& b = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + b < 1 \<Longrightarrow> a .& b = 0
[PROOF STEP]
unfolding pconj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + b < 1 \<Longrightarrow> a + b \<ominus> 1 = 0
[PROOF STEP]
by(simp)


[STATEMENT]
lemma pconj_ge_one[simp]:
  "1 \<le> a + b \<Longrightarrow> a .& b = a + b - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> a + b \<Longrightarrow> a .& b = a + b - 1
[PROOF STEP]
unfolding pconj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> a + b \<Longrightarrow> a + b \<ominus> 1 = a + b - 1
[PROOF STEP]
by(simp)


[STATEMENT]
lemma pconj_idem[simp]:
  "\<guillemotleft>P\<guillemotright> s .& \<guillemotleft>P\<guillemotright> s = \<guillemotleft>P\<guillemotright> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> P \<guillemotright> s .& \<guillemotleft> P \<guillemotright> s = \<guillemotleft> P \<guillemotright> s
[PROOF STEP]
unfolding pconj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> P \<guillemotright> s + \<guillemotleft> P \<guillemotright> s \<ominus> 1 = \<guillemotleft> P \<guillemotright> s
[PROOF STEP]
by(cases "P s", simp_all)


[STATEMENT]
lemma exp_conj_mono_left:
  "P \<tturnstile> Q \<Longrightarrow> P && R \<tturnstile> Q && R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<tturnstile> Q \<Longrightarrow> P && R \<tturnstile> Q && R
[PROOF STEP]
unfolding exp_conj_def pconj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<tturnstile> Q \<Longrightarrow> \<lambda>s. P s + R s \<ominus> 1 \<tturnstile> \<lambda>s. Q s + R s \<ominus> 1
[PROOF STEP]
by(auto intro:tminus_left_mono add_right_mono)


[STATEMENT]
lemma exp_conj_mono_right:
  "Q \<tturnstile> R \<Longrightarrow> P && Q \<tturnstile> P && R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<tturnstile> R \<Longrightarrow> P && Q \<tturnstile> P && R
[PROOF STEP]
unfolding exp_conj_def pconj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<tturnstile> R \<Longrightarrow> \<lambda>s. P s + Q s \<ominus> 1 \<tturnstile> \<lambda>s. P s + R s \<ominus> 1
[PROOF STEP]
by(auto intro:tminus_left_mono add_left_mono)


[STATEMENT]
lemma exp_conj_comm[ac_simps]:
  "a && b = b && a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a && b = b && a
[PROOF STEP]
by(simp add:exp_conj_def ac_simps)


[STATEMENT]
lemma exp_conj_bounded_by[intro,simp]:
  assumes bP: "bounded_by 1 P"
      and bQ: "bounded_by 1 Q"
  shows "bounded_by 1 (P && Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by 1 (P && Q)
[PROOF STEP]
proof(rule bounded_byI, unfold exp_conj_def pconj_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. P x + Q x \<ominus> 1 \<le> 1
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. P x + Q x \<ominus> 1 \<le> 1
[PROOF STEP]
from bP
[PROOF STATE]
proof (chain)
picking this:
bounded_by 1 P
[PROOF STEP]
have "P x \<le> 1"
[PROOF STATE]
proof (prove)
using this:
bounded_by 1 P

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

goal (1 subgoal):
 1. \<And>x. P x + Q x \<ominus> 1 \<le> 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P x \<le> 1

goal (1 subgoal):
 1. \<And>x. P x + Q x \<ominus> 1 \<le> 1
[PROOF STEP]
from bQ
[PROOF STATE]
proof (chain)
picking this:
bounded_by 1 Q
[PROOF STEP]
have "Q x \<le> 1"
[PROOF STATE]
proof (prove)
using this:
bounded_by 1 Q

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

goal (1 subgoal):
 1. \<And>x. P x + Q x \<ominus> 1 \<le> 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P x \<le> 1
Q x \<le> 1
[PROOF STEP]
have "P x + Q x \<le> 2"
[PROOF STATE]
proof (prove)
using this:
P x \<le> 1
Q x \<le> 1

goal (1 subgoal):
 1. P x + Q x \<le> 2
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
P x + Q x \<le> 2

goal (1 subgoal):
 1. \<And>x. P x + Q x \<ominus> 1 \<le> 1
[PROOF STEP]
thus "P x + Q x \<ominus> 1 \<le> 1"
[PROOF STATE]
proof (prove)
using this:
P x + Q x \<le> 2

goal (1 subgoal):
 1. P x + Q x \<ominus> 1 \<le> 1
[PROOF STEP]
unfolding tminus_def
[PROOF STATE]
proof (prove)
using this:
P x + Q x \<le> 2

goal (1 subgoal):
 1. max (P x + Q x - 1) 0 \<le> 1
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
P x + Q x \<ominus> 1 \<le> 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exp_conj_o_distrib[simp]:
  "(P && Q) o f = (P o f) && (Q o f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P && Q \<circ> f = (P \<circ> f) && (Q \<circ> f)
[PROOF STEP]
unfolding exp_conj_def o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. P (f x) .& Q (f x)) = (\<lambda>s. P (f s) .& Q (f s))
[PROOF STEP]
by(simp)


[STATEMENT]
lemma exp_conj_assoc:
  assumes "unitary P" and "unitary Q" and "unitary R"
  shows "P && (Q && R) = (P && Q) && R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P && (Q && R) = P && Q && R
[PROOF STEP]
unfolding exp_conj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. P s .& (Q s .& R s)) = (\<lambda>s. P s .& Q s .& R s)
[PROOF STEP]
proof(rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. P s .& (Q s .& R s) = P s .& Q s .& R s
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. P s .& (Q s .& R s) = P s .& Q s .& R s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
unitary P
unitary Q
unitary R
[PROOF STEP]
have "0 \<le> P s"
[PROOF STATE]
proof (prove)
using this:
unitary P
unitary Q
unitary R

goal (1 subgoal):
 1. 0 \<le> P s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
0 \<le> P s

goal (1 subgoal):
 1. \<And>s. P s .& (Q s .& R s) = P s .& Q s .& R s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> P s

goal (1 subgoal):
 1. \<And>s. P s .& (Q s .& R s) = P s .& Q s .& R s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
unitary P
unitary Q
unitary R
[PROOF STEP]
have "0 \<le> Q s"
[PROOF STATE]
proof (prove)
using this:
unitary P
unitary Q
unitary R

goal (1 subgoal):
 1. 0 \<le> Q s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
0 \<le> Q s

goal (1 subgoal):
 1. \<And>s. P s .& (Q s .& R s) = P s .& Q s .& R s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> Q s

goal (1 subgoal):
 1. \<And>s. P s .& (Q s .& R s) = P s .& Q s .& R s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
unitary P
unitary Q
unitary R
[PROOF STEP]
have "0 \<le> R s"
[PROOF STATE]
proof (prove)
using this:
unitary P
unitary Q
unitary R

goal (1 subgoal):
 1. 0 \<le> R s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
0 \<le> R s

goal (1 subgoal):
 1. \<And>s. P s .& (Q s .& R s) = P s .& Q s .& R s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> R s

goal (1 subgoal):
 1. \<And>s. P s .& (Q s .& R s) = P s .& Q s .& R s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
unitary P
unitary Q
unitary R
[PROOF STEP]
have "P s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
unitary P
unitary Q
unitary R

goal (1 subgoal):
 1. P s \<le> 1
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
P s \<le> 1

goal (1 subgoal):
 1. \<And>s. P s .& (Q s .& R s) = P s .& Q s .& R s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P s \<le> 1

goal (1 subgoal):
 1. \<And>s. P s .& (Q s .& R s) = P s .& Q s .& R s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
unitary P
unitary Q
unitary R
[PROOF STEP]
have "Q s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
unitary P
unitary Q
unitary R

goal (1 subgoal):
 1. Q s \<le> 1
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
Q s \<le> 1

goal (1 subgoal):
 1. \<And>s. P s .& (Q s .& R s) = P s .& Q s .& R s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Q s \<le> 1

goal (1 subgoal):
 1. \<And>s. P s .& (Q s .& R s) = P s .& Q s .& R s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
unitary P
unitary Q
unitary R
[PROOF STEP]
have "R s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
unitary P
unitary Q
unitary R

goal (1 subgoal):
 1. R s \<le> 1
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
R s \<le> 1

goal (1 subgoal):
 1. \<And>s. P s .& (Q s .& R s) = P s .& Q s .& R s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 \<le> P s
0 \<le> Q s
0 \<le> R s
P s \<le> 1
Q s \<le> 1
R s \<le> 1
[PROOF STEP]
show "P s .& (Q s .& R s) = (P s .& Q s) .& R s"
[PROOF STATE]
proof (prove)
using this:
0 \<le> P s
0 \<le> Q s
0 \<le> R s
P s \<le> 1
Q s \<le> 1
R s \<le> 1

goal (1 subgoal):
 1. P s .& (Q s .& R s) = P s .& Q s .& R s
[PROOF STEP]
by(simp add:pconj_assoc)
[PROOF STATE]
proof (state)
this:
P s .& (Q s .& R s) = P s .& Q s .& R s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exp_conj_top_left[simp]:
  "sound P \<Longrightarrow> \<guillemotleft>\<lambda>_. True\<guillemotright> && P = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound P \<Longrightarrow> \<guillemotleft> \<lambda>_. True \<guillemotright> && P = P
[PROOF STEP]
unfolding exp_conj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound P \<Longrightarrow> (\<lambda>s. \<guillemotleft> \<lambda>_. True \<guillemotright> s .& P s) = P
[PROOF STEP]
by(force)


[STATEMENT]
lemma exp_conj_top_right[simp]:
  "sound P \<Longrightarrow> P && \<guillemotleft>\<lambda>_. True\<guillemotright> = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound P \<Longrightarrow> P && \<guillemotleft> \<lambda>_. True \<guillemotright> = P
[PROOF STEP]
unfolding exp_conj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound P \<Longrightarrow> (\<lambda>s. P s .& \<guillemotleft> \<lambda>_. True \<guillemotright> s) = P
[PROOF STEP]
by(force)


[STATEMENT]
lemma exp_conj_idem[simp]:
  "\<guillemotleft>P\<guillemotright> && \<guillemotleft>P\<guillemotright> = \<guillemotleft>P\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> P \<guillemotright> && \<guillemotleft> P \<guillemotright> = \<guillemotleft> P \<guillemotright>
[PROOF STEP]
unfolding exp_conj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<guillemotleft> P \<guillemotright> s .& \<guillemotleft> P \<guillemotright> s) = \<guillemotleft> P \<guillemotright>
[PROOF STEP]
by(rule ext, cases "P s", simp_all)


[STATEMENT]
lemma exp_conj_nneg[intro,simp]:
  "(\<lambda>s. 0) \<le> P && Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lambda>s. 0 \<tturnstile> P && Q
[PROOF STEP]
unfolding exp_conj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lambda>s. 0 \<tturnstile> \<lambda>s. P s .& Q s
[PROOF STEP]
by(blast intro:le_funI)


[STATEMENT]
lemma exp_conj_sound[intro,simp]:
  assumes s_P: "sound P"
      and s_Q: "sound Q"
  shows "sound (P && Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound (P && Q)
[PROOF STEP]
unfolding exp_conj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound (\<lambda>s. P s .& Q s)
[PROOF STEP]
proof(rule soundI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Expectations.bounded (\<lambda>s. P s .& Q s)
 2. nneg (\<lambda>s. P s .& Q s)
[PROOF STEP]
from s_P and s_Q
[PROOF STATE]
proof (chain)
picking this:
sound P
sound Q
[PROOF STEP]
have "\<And>s. 0 \<le> P s + Q s"
[PROOF STATE]
proof (prove)
using this:
sound P
sound Q

goal (1 subgoal):
 1. \<And>s. 0 \<le> P s + Q s
[PROOF STEP]
by(blast intro:add_nonneg_nonneg)
[PROOF STATE]
proof (state)
this:
0 \<le> P ?s + Q ?s

goal (2 subgoals):
 1. Expectations.bounded (\<lambda>s. P s .& Q s)
 2. nneg (\<lambda>s. P s .& Q s)
[PROOF STEP]
hence "\<And>s. P s .& Q s \<le> P s + Q s"
[PROOF STATE]
proof (prove)
using this:
0 \<le> P ?s + Q ?s

goal (1 subgoal):
 1. \<And>s. P s .& Q s \<le> P s + Q s
[PROOF STEP]
unfolding pconj_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> P ?s + Q ?s

goal (1 subgoal):
 1. \<And>s. P s + Q s \<ominus> 1 \<le> P s + Q s
[PROOF STEP]
by(force intro:tminus_less)
[PROOF STATE]
proof (state)
this:
P ?s .& Q ?s \<le> P ?s + Q ?s

goal (2 subgoals):
 1. Expectations.bounded (\<lambda>s. P s .& Q s)
 2. nneg (\<lambda>s. P s .& Q s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
P ?s .& Q ?s \<le> P ?s + Q ?s

goal (2 subgoals):
 1. Expectations.bounded (\<lambda>s. P s .& Q s)
 2. nneg (\<lambda>s. P s .& Q s)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
sound P
sound Q
[PROOF STEP]
have "\<And>s. ... s \<le> bound_of P + bound_of Q"
[PROOF STATE]
proof (prove)
using this:
sound P
sound Q

goal (1 subgoal):
 1. \<And>s. P s + Q s \<le> bound_of P + bound_of Q
[PROOF STEP]
by(blast intro:add_mono)
[PROOF STATE]
proof (state)
this:
P ?s + Q ?s \<le> bound_of P + bound_of Q

goal (2 subgoals):
 1. Expectations.bounded (\<lambda>s. P s .& Q s)
 2. nneg (\<lambda>s. P s .& Q s)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
P ?s1 .& Q ?s1 \<le> bound_of P + bound_of Q
[PROOF STEP]
have "bounded_by (bound_of P + bound_of Q) (\<lambda>s. P s .& Q s)"
[PROOF STATE]
proof (prove)
using this:
P ?s1 .& Q ?s1 \<le> bound_of P + bound_of Q

goal (1 subgoal):
 1. bounded_by (bound_of P + bound_of Q) (\<lambda>s. P s .& Q s)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
bounded_by (bound_of P + bound_of Q) (\<lambda>s. P s .& Q s)

goal (2 subgoals):
 1. Expectations.bounded (\<lambda>s. P s .& Q s)
 2. nneg (\<lambda>s. P s .& Q s)
[PROOF STEP]
thus "bounded (\<lambda>s. P s .& Q s)"
[PROOF STATE]
proof (prove)
using this:
bounded_by (bound_of P + bound_of Q) (\<lambda>s. P s .& Q s)

goal (1 subgoal):
 1. Expectations.bounded (\<lambda>s. P s .& Q s)
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
Expectations.bounded (\<lambda>s. P s .& Q s)

goal (1 subgoal):
 1. nneg (\<lambda>s. P s .& Q s)
[PROOF STEP]
show "nneg (\<lambda>s. P s .& Q s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nneg (\<lambda>s. P s .& Q s)
[PROOF STEP]
unfolding pconj_def tminus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nneg (\<lambda>s. max (P s + Q s - 1) 0)
[PROOF STEP]
by(force)
[PROOF STATE]
proof (state)
this:
nneg (\<lambda>s. P s .& Q s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exp_conj_rzero[simp]:
  "bounded_by 1 P \<Longrightarrow> P && (\<lambda>s. 0) = (\<lambda>s. 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by 1 P \<Longrightarrow> P && (\<lambda>s. 0) = (\<lambda>s. 0)
[PROOF STEP]
unfolding exp_conj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_by 1 P \<Longrightarrow> (\<lambda>s. P s .& 0) = (\<lambda>s. 0)
[PROOF STEP]
by(force)


[STATEMENT]
lemma exp_conj_1_right[simp]:
  assumes nn: "nneg A"
  shows "A && (\<lambda>_. 1) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A && (\<lambda>_. 1) = A
[PROOF STEP]
unfolding exp_conj_def pconj_def tminus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. max (A s + 1 - 1) 0) = A
[PROOF STEP]
proof(rule ext, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. max (A s) 0 = A s
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. max (A s) 0 = A s
[PROOF STEP]
from nn
[PROOF STATE]
proof (chain)
picking this:
nneg A
[PROOF STEP]
have "0 \<le> A s"
[PROOF STATE]
proof (prove)
using this:
nneg A

goal (1 subgoal):
 1. 0 \<le> A s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
0 \<le> A s

goal (1 subgoal):
 1. \<And>s. max (A s) 0 = A s
[PROOF STEP]
thus "max (A s) 0 = A s"
[PROOF STATE]
proof (prove)
using this:
0 \<le> A s

goal (1 subgoal):
 1. max (A s) 0 = A s
[PROOF STEP]
by(force)
[PROOF STATE]
proof (state)
this:
max (A s) 0 = A s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exp_conj_std_split:
  "\<guillemotleft>\<lambda>s. P s \<and> Q s\<guillemotright> = \<guillemotleft>P\<guillemotright> && \<guillemotleft>Q\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft> \<lambda>s. P s \<and> Q s \<guillemotright> = \<guillemotleft> P \<guillemotright> && \<guillemotleft> Q \<guillemotright>
[PROOF STEP]
unfolding exp_conj_def embed_bool_def pconj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. if P s \<and> Q s then 1 else 0) = (\<lambda>s. (if P s then 1 else 0) + (if Q s then 1 else 0) \<ominus> 1)
[PROOF STEP]
by(auto)


[STATEMENT]
lemma entails_frame:
  assumes ePR: "P \<tturnstile> R"
      and eQS: "Q \<tturnstile> S"
  shows "P && Q \<tturnstile> R && S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P && Q \<tturnstile> R && S
[PROOF STEP]
proof(rule le_funI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (P && Q) x \<le> (R && S) x
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (P && Q) x \<le> (R && S) x
[PROOF STEP]
from ePR
[PROOF STATE]
proof (chain)
picking this:
P \<tturnstile> R
[PROOF STEP]
have "P s \<le> R s"
[PROOF STATE]
proof (prove)
using this:
P \<tturnstile> R

goal (1 subgoal):
 1. P s \<le> R s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
P s \<le> R s

goal (1 subgoal):
 1. \<And>x. (P && Q) x \<le> (R && S) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P s \<le> R s

goal (1 subgoal):
 1. \<And>x. (P && Q) x \<le> (R && S) x
[PROOF STEP]
from eQS
[PROOF STATE]
proof (chain)
picking this:
Q \<tturnstile> S
[PROOF STEP]
have "Q s \<le> S s"
[PROOF STATE]
proof (prove)
using this:
Q \<tturnstile> S

goal (1 subgoal):
 1. Q s \<le> S s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
Q s \<le> S s

goal (1 subgoal):
 1. \<And>x. (P && Q) x \<le> (R && S) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P s \<le> R s
Q s \<le> S s
[PROOF STEP]
have "P s + Q s \<le> R s + S s"
[PROOF STATE]
proof (prove)
using this:
P s \<le> R s
Q s \<le> S s

goal (1 subgoal):
 1. P s + Q s \<le> R s + S s
[PROOF STEP]
by(rule add_mono)
[PROOF STATE]
proof (state)
this:
P s + Q s \<le> R s + S s

goal (1 subgoal):
 1. \<And>x. (P && Q) x \<le> (R && S) x
[PROOF STEP]
hence "P s + Q s \<ominus> 1 \<le> R s + S s \<ominus> 1"
[PROOF STATE]
proof (prove)
using this:
P s + Q s \<le> R s + S s

goal (1 subgoal):
 1. P s + Q s \<ominus> 1 \<le> R s + S s \<ominus> 1
[PROOF STEP]
by(rule tminus_left_mono)
[PROOF STATE]
proof (state)
this:
P s + Q s \<ominus> 1 \<le> R s + S s \<ominus> 1

goal (1 subgoal):
 1. \<And>x. (P && Q) x \<le> (R && S) x
[PROOF STEP]
thus "(P && Q) s \<le> (R && S) s"
[PROOF STATE]
proof (prove)
using this:
P s + Q s \<ominus> 1 \<le> R s + S s \<ominus> 1

goal (1 subgoal):
 1. (P && Q) s \<le> (R && S) s
[PROOF STEP]
unfolding exp_conj_def pconj_def
[PROOF STATE]
proof (prove)
using this:
P s + Q s \<ominus> 1 \<le> R s + S s \<ominus> 1

goal (1 subgoal):
 1. P s + Q s \<ominus> 1 \<le> R s + S s \<ominus> 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(P && Q) s \<le> (R && S) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pentails_cases:
  assumes PQe: "\<And>x. P x \<tturnstile> Q x"
      and exhaust: "\<And>s. \<exists>x. P (x s) s = 1"
      and framed: "\<And>x. P x && R \<tturnstile> Q x && S"
      and sR: "sound R" and sS: "sound S"
      and bQ: "\<And>x. bounded_by 1 (Q x)"
  shows "R \<tturnstile> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<tturnstile> S
[PROOF STEP]
proof(rule le_funI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. R x \<le> S x
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. R x \<le> S x
[PROOF STEP]
from exhaust
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. P (x ?s) ?s = 1
[PROOF STEP]
obtain x where P_xs: "P x s = 1"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. P (x ?s) ?s = 1

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

goal (1 subgoal):
 1. \<And>x. R x \<le> S x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P x s = 1

goal (1 subgoal):
 1. \<And>x. R x \<le> S x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
P x s = 1

goal (1 subgoal):
 1. \<And>x. R x \<le> S x
[PROOF STEP]
hence "1 = P x s"
[PROOF STATE]
proof (prove)
using this:
P x s = 1

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

goal (1 subgoal):
 1. \<And>x. R x \<le> S x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 = P x s

goal (1 subgoal):
 1. \<And>x. R x \<le> S x
[PROOF STEP]
from PQe
[PROOF STATE]
proof (chain)
picking this:
P ?x \<tturnstile> Q ?x
[PROOF STEP]
have "P x s \<le> Q x s"
[PROOF STATE]
proof (prove)
using this:
P ?x \<tturnstile> Q ?x

goal (1 subgoal):
 1. P x s \<le> Q x s
[PROOF STEP]
by(blast dest:le_funD)
[PROOF STATE]
proof (state)
this:
P x s \<le> Q x s

goal (1 subgoal):
 1. \<And>x. R x \<le> S x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 \<le> Q x s
[PROOF STEP]
have "Q x s = 1"
[PROOF STATE]
proof (prove)
using this:
1 \<le> Q x s

goal (1 subgoal):
 1. Q x s = 1
[PROOF STEP]
using bQ
[PROOF STATE]
proof (prove)
using this:
1 \<le> Q x s
bounded_by 1 (Q ?x)

goal (1 subgoal):
 1. Q x s = 1
[PROOF STEP]
by(blast intro:antisym)
[PROOF STATE]
proof (state)
this:
Q x s = 1

goal (1 subgoal):
 1. \<And>x. R x \<le> S x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Q x s = 1

goal (1 subgoal):
 1. \<And>x. R x \<le> S x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Q x s = 1

goal (1 subgoal):
 1. \<And>x. R x \<le> S x
[PROOF STEP]
note le_funD[OF framed[where x=x], where x=s]
[PROOF STATE]
proof (state)
this:
(P x && R) s \<le> (Q x && S) s

goal (1 subgoal):
 1. \<And>x. R x \<le> S x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(P x && R) s \<le> (Q x && S) s

goal (1 subgoal):
 1. \<And>x. R x \<le> S x
[PROOF STEP]
from sR
[PROOF STATE]
proof (chain)
picking this:
sound R
[PROOF STEP]
have "0 \<le> R s"
[PROOF STATE]
proof (prove)
using this:
sound R

goal (1 subgoal):
 1. 0 \<le> R s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
0 \<le> R s

goal (1 subgoal):
 1. \<And>x. R x \<le> S x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> R s

goal (1 subgoal):
 1. \<And>x. R x \<le> S x
[PROOF STEP]
from sS
[PROOF STATE]
proof (chain)
picking this:
sound S
[PROOF STEP]
have "0 \<le> S s"
[PROOF STATE]
proof (prove)
using this:
sound S

goal (1 subgoal):
 1. 0 \<le> S s
[PROOF STEP]
by(blast)
[PROOF STATE]
proof (state)
this:
0 \<le> S s

goal (1 subgoal):
 1. \<And>x. R x \<le> S x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P x s = 1
Q x s = 1
(P x && R) s \<le> (Q x && S) s
0 \<le> R s
0 \<le> S s
[PROOF STEP]
show "R s \<le> S s"
[PROOF STATE]
proof (prove)
using this:
P x s = 1
Q x s = 1
(P x && R) s \<le> (Q x && S) s
0 \<le> R s
0 \<le> S s

goal (1 subgoal):
 1. R s \<le> S s
[PROOF STEP]
by(simp add:exp_conj_def)
[PROOF STATE]
proof (state)
this:
R s \<le> S s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unitary_bot[iff]:
  "unitary (\<lambda>s. 0::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary (\<lambda>s. 0)
[PROOF STEP]
by(auto)


[STATEMENT]
lemma unitary_top[iff]:
  "unitary (\<lambda>s. 1::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary (\<lambda>s. 1)
[PROOF STEP]
by(auto)


[STATEMENT]
lemma unitary_embed[iff]:
  "unitary \<guillemotleft>P\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary \<guillemotleft> P \<guillemotright>
[PROOF STEP]
by(auto)


[STATEMENT]
lemma unitary_const[iff]:
  "\<lbrakk> 0 \<le> c; c \<le> 1 \<rbrakk> \<Longrightarrow> unitary (\<lambda>s. c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> c; c \<le> 1\<rbrakk> \<Longrightarrow> unitary (\<lambda>s. c)
[PROOF STEP]
by(auto)


[STATEMENT]
lemma unitary_mult:
  assumes uA: "unitary A" and uB: "unitary B"
  shows "unitary (\<lambda>s. A s * B s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary (\<lambda>s. A s * B s)
[PROOF STEP]
proof(intro unitaryI2 nnegI bounded_byI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. 0 \<le> A x * B x
 2. \<And>x. A x * B x \<le> 1
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. 0 \<le> A x * B x
 2. \<And>x. A x * B x \<le> 1
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
unitary A
unitary B
[PROOF STEP]
have nnA: "0 \<le> A s" and nnB: "0 \<le> B s"
[PROOF STATE]
proof (prove)
using this:
unitary A
unitary B

goal (1 subgoal):
 1. 0 \<le> A s &&& 0 \<le> B s
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
0 \<le> A s
0 \<le> B s

goal (2 subgoals):
 1. \<And>x. 0 \<le> A x * B x
 2. \<And>x. A x * B x \<le> 1
[PROOF STEP]
thus "0 \<le> A s * B s"
[PROOF STATE]
proof (prove)
using this:
0 \<le> A s
0 \<le> B s

goal (1 subgoal):
 1. 0 \<le> A s * B s
[PROOF STEP]
by(rule mult_nonneg_nonneg)
[PROOF STATE]
proof (state)
this:
0 \<le> A s * B s

goal (1 subgoal):
 1. \<And>x. A x * B x \<le> 1
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
unitary A
unitary B
[PROOF STEP]
have "A s \<le> 1" and "B s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
unitary A
unitary B

goal (1 subgoal):
 1. A s \<le> 1 &&& B s \<le> 1
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
A s \<le> 1
B s \<le> 1

goal (1 subgoal):
 1. \<And>x. A x * B x \<le> 1
[PROOF STEP]
with nnB
[PROOF STATE]
proof (chain)
picking this:
0 \<le> B s
A s \<le> 1
B s \<le> 1
[PROOF STEP]
have "A s * B s \<le> 1 * 1"
[PROOF STATE]
proof (prove)
using this:
0 \<le> B s
A s \<le> 1
B s \<le> 1

goal (1 subgoal):
 1. A s * B s \<le> 1 * 1
[PROOF STEP]
by(intro mult_mono, auto)
[PROOF STATE]
proof (state)
this:
A s * B s \<le> 1 * 1

goal (1 subgoal):
 1. \<And>x. A x * B x \<le> 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A s * B s \<le> 1 * 1

goal (1 subgoal):
 1. \<And>x. A x * B x \<le> 1
[PROOF STEP]
have "... = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 * 1 = 1
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
1 * 1 = 1

goal (1 subgoal):
 1. \<And>x. A x * B x \<le> 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A s * B s \<le> 1
[PROOF STEP]
show "A s * B s \<le> 1"
[PROOF STATE]
proof (prove)
using this:
A s * B s \<le> 1

goal (1 subgoal):
 1. A s * B s \<le> 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A s * B s \<le> 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exp_conj_unitary:
  "\<lbrakk> unitary P; unitary Q \<rbrakk> \<Longrightarrow> unitary (P && Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unitary P; unitary Q\<rbrakk> \<Longrightarrow> unitary (P && Q)
[PROOF STEP]
by(intro unitaryI2 nnegI2, auto)


[STATEMENT]
lemma unitary_comp[simp]:
  "unitary P \<Longrightarrow> unitary (P o f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary P \<Longrightarrow> unitary (P \<circ> f)
[PROOF STEP]
by(intro unitaryI2 nnegI bounded_byI, auto simp:o_def)


[STATEMENT]
lemma singleTauChain:
  fixes P  :: pi
  and   P' :: pi

  assumes "P \<longmapsto>\<tau> \<prec> P'"

  shows "P \<Longrightarrow>\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> \<tau> \<prec> P'

goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
by(simp add: r_into_rtrancl)


[STATEMENT]
lemma tauChainAddTau[dest]:
  fixes P   :: pi
  and   P'  :: pi
  and   P'' :: pi

  shows "P \<Longrightarrow>\<^sub>\<tau> P' \<Longrightarrow> P' \<longmapsto>\<tau> \<prec> P'' \<Longrightarrow> P \<Longrightarrow>\<^sub>\<tau> P''"
  and "P \<longmapsto>\<tau> \<prec> P' \<Longrightarrow> P' \<Longrightarrow>\<^sub>\<tau> P'' \<Longrightarrow> P \<Longrightarrow>\<^sub>\<tau> P''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto> \<tau> \<prec> P''\<rbrakk> \<Longrightarrow> P \<Longrightarrow>\<^sub>\<tau> P'') &&& (\<lbrakk>P \<longmapsto> \<tau> \<prec> P'; P' \<Longrightarrow>\<^sub>\<tau> P''\<rbrakk> \<Longrightarrow> P \<Longrightarrow>\<^sub>\<tau> P'')
[PROOF STEP]
by(auto dest: singleTauChain)


[STATEMENT]
lemma tauChainInduct[consumes 1, case_names id ih]:
  fixes P  :: pi
  and   P' :: pi

  assumes "P \<Longrightarrow>\<^sub>\<tau> P'"
  and     "F P"
  and     "\<And>P' P''. \<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P'; P' \<longmapsto>\<tau> \<prec> P''; F P'\<rbrakk> \<Longrightarrow> F P''"

  shows "F P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sub>\<tau> P'
F P
\<lbrakk>P \<Longrightarrow>\<^sub>\<tau> ?P'; ?P' \<longmapsto> \<tau> \<prec> ?P''; F ?P'\<rbrakk> \<Longrightarrow> F ?P''

goal (1 subgoal):
 1. F P'
[PROOF STEP]
by(drule_tac rtrancl_induct) auto