[STATEMENT]
lemma finite_subset[trans]: "A \<subseteq> B \<Longrightarrow> finite B \<Longrightarrow> finite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> B; finite B\<rbrakk> \<Longrightarrow> finite A
[PROOF STEP]
using finite_subset
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> B; finite B\<rbrakk> \<Longrightarrow> finite A
[PROOF STEP]
by this


[STATEMENT]
lemma lowner_lub_form:
  "lowner_is_lub (mat dim dim (\<lambda> (i, j). (lim (\<lambda> n. (f n) $$ (i, j)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
from inc_partial_density_operator_converge
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?i \<in> {0..<dim}; ?j \<in> {0..<dim}\<rbrakk> \<Longrightarrow> convergent (\<lambda>n. f n $$ (?i, ?j))
[PROOF STEP]
have conf: "\<forall> i \<in> {0 ..<dim}.  \<forall> j \<in> {0 ..<dim}. convergent (\<lambda> n. f n $$ (i, j))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<in> {0..<dim}; ?j \<in> {0..<dim}\<rbrakk> \<Longrightarrow> convergent (\<lambda>n. f n $$ (?i, ?j))

goal (1 subgoal):
 1. \<forall>i\<in>{0..<dim}. \<forall>j\<in>{0..<dim}. convergent (\<lambda>n. f n $$ (i, j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{0..<dim}. \<forall>j\<in>{0..<dim}. convergent (\<lambda>n. f n $$ (i, j))

goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
let ?A = "mat dim dim (\<lambda> (i, j). (lim (\<lambda> n. (f n) $$ (i, j))))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
have dim_A: "?A \<in> carrier_mat dim dim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<in> carrier_mat dim dim
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<in> carrier_mat dim dim

goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
have lim_A: "(\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)"
    if i: "i < dim" and j: "j < dim" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)
[PROOF STEP]
from i j
[PROOF STATE]
proof (chain)
picking this:
i < dim
j < dim
[PROOF STEP]
have ij: "mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j) = lim (\<lambda>n. f n $$ (i, j))"
[PROOF STATE]
proof (prove)
using this:
i < dim
j < dim

goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j) = lim (\<lambda>n. f n $$ (i, j))
[PROOF STEP]
by (metis case_prod_conv index_mat(1))
[PROOF STATE]
proof (state)
this:
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j) = lim (\<lambda>n. f n $$ (i, j))

goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)
[PROOF STEP]
have "convergent (\<lambda>n. f n $$ (i, j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergent (\<lambda>n. f n $$ (i, j))
[PROOF STEP]
using conf i j
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{0..<dim}. \<forall>j\<in>{0..<dim}. convergent (\<lambda>n. f n $$ (i, j))
i < dim
j < dim

goal (1 subgoal):
 1. convergent (\<lambda>n. f n $$ (i, j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
convergent (\<lambda>n. f n $$ (i, j))

goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
convergent (\<lambda>n. f n $$ (i, j))
[PROOF STEP]
have "(\<lambda>n. f n $$ (i, j))  \<longlonglongrightarrow> lim (\<lambda>n. f n $$ (i, j)) "
[PROOF STATE]
proof (prove)
using this:
convergent (\<lambda>n. f n $$ (i, j))

goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> lim (\<lambda>n. f n $$ (i, j))
[PROOF STEP]
using convergent_LIMSEQ_iff
[PROOF STATE]
proof (prove)
using this:
convergent (\<lambda>n. f n $$ (i, j))
convergent ?X = ?X \<longlonglongrightarrow> lim ?X

goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> lim (\<lambda>n. f n $$ (i, j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> lim (\<lambda>n. f n $$ (i, j))

goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> lim (\<lambda>n. f n $$ (i, j))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> lim (\<lambda>n. f n $$ (i, j))

goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)
[PROOF STEP]
using ij
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> lim (\<lambda>n. f n $$ (i, j))
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j) = lim (\<lambda>n. f n $$ (i, j))

goal (1 subgoal):
 1. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < dim; ?j < dim\<rbrakk> \<Longrightarrow> (\<lambda>n. f n $$ (?i, ?j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (?i, ?j)

goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
from dim dim_A lim_A
[PROOF STATE]
proof (chain)
picking this:
f ?n \<in> carrier_mat dim dim
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<in> carrier_mat dim dim
\<lbrakk>?i < dim; ?j < dim\<rbrakk> \<Longrightarrow> (\<lambda>n. f n $$ (?i, ?j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (?i, ?j)
[PROOF STEP]
have lim_mat_A: "limit_mat f ?A dim"
[PROOF STATE]
proof (prove)
using this:
f ?n \<in> carrier_mat dim dim
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<in> carrier_mat dim dim
\<lbrakk>?i < dim; ?j < dim\<rbrakk> \<Longrightarrow> (\<lambda>n. f n $$ (?i, ?j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (?i, ?j)

goal (1 subgoal):
 1. limit_mat f (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim
[PROOF STEP]
unfolding limit_mat_def
[PROOF STATE]
proof (prove)
using this:
f ?n \<in> carrier_mat dim dim
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<in> carrier_mat dim dim
\<lbrakk>?i < dim; ?j < dim\<rbrakk> \<Longrightarrow> (\<lambda>n. f n $$ (?i, ?j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (?i, ?j)

goal (1 subgoal):
 1. \<forall>n. f n \<in> carrier_mat dim dim \<and> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<in> carrier_mat dim dim \<and> (\<forall>i<dim. \<forall>j<dim. (\<lambda>n. f n $$ (i, j)) \<longlonglongrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) $$ (i, j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
limit_mat f (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim

goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
have is_ub: "f n \<le>\<^sub>L ?A" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
have "\<forall> m \<ge> n. positive (f m - f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m\<ge>n. positive (f m - f n)
[PROOF STEP]
using lowner_le_transitive
[PROOF STATE]
proof (prove)
using this:
?m \<le> ?n \<Longrightarrow> positive (f ?n - f ?m)

goal (1 subgoal):
 1. \<forall>m\<ge>n. positive (f m - f n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>m\<ge>n. positive (f m - f n)

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<ge>n. positive (f m - f n)
[PROOF STEP]
have le: "\<forall> m \<ge> n. f n \<le>\<^sub>L f m "
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>n. positive (f m - f n)

goal (1 subgoal):
 1. \<forall>m\<ge>n. f n \<le>\<^sub>L f m
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>n. positive (f m - f n)

goal (1 subgoal):
 1. \<forall>m\<ge>n. dim_row (f n) = dim_row (f m) \<and> dim_col (f n) = dim_col (f m) \<and> positive (f m - f n)
[PROOF STEP]
using dim
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>n. positive (f m - f n)
f ?n \<in> carrier_mat dim dim

goal (1 subgoal):
 1. \<forall>m\<ge>n. dim_row (f n) = dim_row (f m) \<and> dim_col (f n) = dim_col (f m) \<and> positive (f m - f n)
[PROOF STEP]
by (metis carrier_matD(1) carrier_matD(2))
[PROOF STATE]
proof (state)
this:
\<forall>m\<ge>n. f n \<le>\<^sub>L f m

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
have dimn: "f n \<in> carrier_mat dim dim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n \<in> carrier_mat dim dim
[PROOF STEP]
using dim
[PROOF STATE]
proof (prove)
using this:
f ?n \<in> carrier_mat dim dim

goal (1 subgoal):
 1. f n \<in> carrier_mat dim dim
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f n \<in> carrier_mat dim dim

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f n \<in> carrier_mat dim dim
[PROOF STEP]
have limAf: "limit_mat (mat_seq_minus f (f n)) (?A - f n) dim"
[PROOF STATE]
proof (prove)
using this:
f n \<in> carrier_mat dim dim

goal (1 subgoal):
 1. limit_mat (mat_seq_minus f (f n)) (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n) dim
[PROOF STEP]
using minus_mat_limit lim_mat_A
[PROOF STATE]
proof (prove)
using this:
f n \<in> carrier_mat dim dim
\<lbrakk>?B \<in> carrier_mat ?m ?m; limit_mat ?X ?A ?m\<rbrakk> \<Longrightarrow> limit_mat (mat_seq_minus ?X ?B) (?A - ?B) ?m
limit_mat f (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim

goal (1 subgoal):
 1. limit_mat (mat_seq_minus f (f n)) (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n) dim
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
limit_mat (mat_seq_minus f (f n)) (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n) dim

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
have " \<forall>m\<ge>n. positive (f m - f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m\<ge>n. positive (f m - f n)
[PROOF STEP]
using lowner_le_transitive
[PROOF STATE]
proof (prove)
using this:
?m \<le> ?n \<Longrightarrow> positive (f ?n - f ?m)

goal (1 subgoal):
 1. \<forall>m\<ge>n. positive (f m - f n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>m\<ge>n. positive (f m - f n)

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<ge>n. positive (f m - f n)
[PROOF STEP]
have "\<exists>k. \<forall>m\<ge>k. positive (f m - f n)"
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<ge>n. positive (f m - f n)

goal (1 subgoal):
 1. \<exists>k. \<forall>m\<ge>k. positive (f m - f n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>m\<ge>k. positive (f m - f n)

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. \<forall>m\<ge>k. positive (f m - f n)
[PROOF STEP]
have posAf: "\<exists> k. \<forall> m \<ge> k. positive ((mat_seq_minus f (f n)) m)"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. \<forall>m\<ge>k. positive (f m - f n)

goal (1 subgoal):
 1. \<exists>k. \<forall>m\<ge>k. positive (mat_seq_minus f (f n) m)
[PROOF STEP]
unfolding mat_seq_minus_def
[PROOF STATE]
proof (prove)
using this:
\<exists>k. \<forall>m\<ge>k. positive (f m - f n)

goal (1 subgoal):
 1. \<exists>k. \<forall>m\<ge>k. positive (f m - f n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>m\<ge>k. positive (mat_seq_minus f (f n) m)

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
from limAf posAf
[PROOF STATE]
proof (chain)
picking this:
limit_mat (mat_seq_minus f (f n)) (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n) dim
\<exists>k. \<forall>m\<ge>k. positive (mat_seq_minus f (f n) m)
[PROOF STEP]
have "positive (?A - f n)"
[PROOF STATE]
proof (prove)
using this:
limit_mat (mat_seq_minus f (f n)) (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n) dim
\<exists>k. \<forall>m\<ge>k. positive (mat_seq_minus f (f n) m)

goal (1 subgoal):
 1. positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)
[PROOF STEP]
using pos_mat_lim_is_pos_aux
[PROOF STATE]
proof (prove)
using this:
limit_mat (mat_seq_minus f (f n)) (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n) dim
\<exists>k. \<forall>m\<ge>k. positive (mat_seq_minus f (f n) m)
\<lbrakk>limit_mat ?X ?A ?m; \<exists>k. \<forall>n\<ge>k. positive (?X n)\<rbrakk> \<Longrightarrow> positive ?A

goal (1 subgoal):
 1. positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)
[PROOF STEP]
have "f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))"
[PROOF STATE]
proof (prove)
using this:
positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)

goal (1 subgoal):
 1. dim_row (f n) = dim_row (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) \<and> dim_col (f n) = dim_col (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) \<and> positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)
[PROOF STEP]
using dim
[PROOF STATE]
proof (prove)
using this:
positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)
f ?n \<in> carrier_mat dim dim

goal (1 subgoal):
 1. dim_row (f n) = dim_row (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) \<and> dim_col (f n) = dim_col (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) \<and> positive (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) - f n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))

goal (1 subgoal):
 1. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f ?n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))

goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
have is_lub: "?A \<le>\<^sub>L M'" if ub: "\<forall>n. f n \<le>\<^sub>L M'" for M'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
have dim_M: "M' \<in> carrier_mat dim dim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M' \<in> carrier_mat dim dim
[PROOF STEP]
using ub
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f n \<le>\<^sub>L M'

goal (1 subgoal):
 1. M' \<in> carrier_mat dim dim
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. dim_row (f n) = dim_row M' \<and> dim_col (f n) = dim_col M' \<and> positive (M' - f n)

goal (1 subgoal):
 1. M' \<in> carrier_mat dim dim
[PROOF STEP]
using dim
[PROOF STATE]
proof (prove)
using this:
\<forall>n. dim_row (f n) = dim_row M' \<and> dim_col (f n) = dim_col M' \<and> positive (M' - f n)
f ?n \<in> carrier_mat dim dim

goal (1 subgoal):
 1. M' \<in> carrier_mat dim dim
[PROOF STEP]
by (metis carrier_matD(1) carrier_matD(2) carrier_mat_triv)
[PROOF STATE]
proof (state)
this:
M' \<in> carrier_mat dim dim

goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
from ub
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. f n \<le>\<^sub>L M'
[PROOF STEP]
have posAf: "\<forall> n. positive (minus_mat_seq M' f n)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f n \<le>\<^sub>L M'

goal (1 subgoal):
 1. \<forall>n. positive (minus_mat_seq M' f n)
[PROOF STEP]
unfolding minus_mat_seq_def lowner_le_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. dim_row (f n) = dim_row M' \<and> dim_col (f n) = dim_col M' \<and> positive (M' - f n)

goal (1 subgoal):
 1. \<forall>n. positive (M' - f n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. positive (minus_mat_seq M' f n)

goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
have limAf: "limit_mat (minus_mat_seq M' f) (M' - ?A) dim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. limit_mat (minus_mat_seq M' f) (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim
[PROOF STEP]
using mat_minus_limit dim_A lim_mat_A
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> carrier_mat ?m ?m; limit_mat ?X ?A ?m\<rbrakk> \<Longrightarrow> limit_mat (minus_mat_seq ?B ?X) (?B - ?A) ?m
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<in> carrier_mat dim dim
limit_mat f (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim

goal (1 subgoal):
 1. limit_mat (minus_mat_seq M' f) (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
limit_mat (minus_mat_seq M' f) (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim

goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
from posAf limAf
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. positive (minus_mat_seq M' f n)
limit_mat (minus_mat_seq M' f) (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim
[PROOF STEP]
have  "positive (M' - ?A)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. positive (minus_mat_seq M' f n)
limit_mat (minus_mat_seq M' f) (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim

goal (1 subgoal):
 1. positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
using pos_mat_lim_is_pos_aux
[PROOF STATE]
proof (prove)
using this:
\<forall>n. positive (minus_mat_seq M' f n)
limit_mat (minus_mat_seq M' f) (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) dim
\<lbrakk>limit_mat ?X ?A ?m; \<exists>k. \<forall>n\<ge>k. positive (?X n)\<rbrakk> \<Longrightarrow> positive ?A

goal (1 subgoal):
 1. positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))

goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
have "?A \<le>\<^sub>L M'"
[PROOF STATE]
proof (prove)
using this:
positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))

goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
unfolding lowner_le_def
[PROOF STATE]
proof (prove)
using this:
positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))

goal (1 subgoal):
 1. dim_row (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) = dim_row M' \<and> dim_col (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) = dim_col M' \<and> positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
using dim dim_A dim_M
[PROOF STATE]
proof (prove)
using this:
positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
f ?n \<in> carrier_mat dim dim
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<in> carrier_mat dim dim
M' \<in> carrier_mat dim dim

goal (1 subgoal):
 1. dim_row (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) = dim_row M' \<and> dim_col (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) = dim_col M' \<and> positive (M' - mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'

goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'

goal (1 subgoal):
 1. mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n. f n \<le>\<^sub>L ?M' \<Longrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L ?M'

goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
from is_ub is_lub
[PROOF STATE]
proof (chain)
picking this:
f ?n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
\<forall>n. f n \<le>\<^sub>L ?M' \<Longrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L ?M'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f ?n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
\<forall>n. f n \<le>\<^sub>L ?M' \<Longrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L ?M'

goal (1 subgoal):
 1. local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))
[PROOF STEP]
unfolding lowner_is_lub_def
[PROOF STATE]
proof (prove)
using this:
f ?n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))
\<forall>n. f n \<le>\<^sub>L ?M' \<Longrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L ?M'

goal (1 subgoal):
 1. (\<forall>n. f n \<le>\<^sub>L mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j)))) \<and> (\<forall>M'. (\<forall>n. f n \<le>\<^sub>L M') \<longrightarrow> mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))) \<le>\<^sub>L M')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.lowner_is_lub (mat dim dim (\<lambda>(i, j). lim (\<lambda>n. f n $$ (i, j))))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_Err_eq: "(x \<noteq> Err) = (\<exists>a. x = OK a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<noteq> Err) = (\<exists>a. x = OK a)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<noteq> Err) = (\<exists>a. x = OK a)
[PROOF STEP]
by (cases x) auto


[STATEMENT]
lemma eq_order_le:
  "\<lbrakk> x=y; order r A; x \<in>A ; y \<in> A \<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^sub>r y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = y; order r A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> y
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = y; order r A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> y
[PROOF STEP]
apply (unfold order_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = y; (\<forall>x\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> x) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^esub> x \<longrightarrow> x = y) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> y \<and> y \<sqsubseteq>\<^bsub>r\<^esub> z \<longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> z); x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> y
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bad_guards:
  "\<exists>i. can_take_transition t1 i r \<and> \<not> can_take_transition t2 i r \<Longrightarrow>
   \<not> subsumes t2 r t1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. can_take_transition t1 i r \<and> \<not> can_take_transition t2 i r \<Longrightarrow> \<not> subsumes t2 r t1
[PROOF STEP]
by (simp add: subsumes_def)


[STATEMENT]
lemma triangle_set_power_set_ss: "triangle_set \<subseteq> Pow V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triangle_set \<subseteq> Pow V
[PROOF STEP]
by (auto simp add: triangle_set_def triangle_in_graph_def wellformed_alt_fst wellformed_alt_snd)


[STATEMENT]
lemma omega_mult_star_2:
  "x\<^sup>\<omega> * y\<^sup>\<star> = x\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<omega> * y\<^sup>\<star> = x\<^sup>\<omega>
[PROOF STEP]
by (meson order.antisym le_supE star.circ_back_loop_prefixpoint omega_sub_vector)


[STATEMENT]
lemma class_add_relevant_entries:
 "\<not> is_class P C
  \<Longrightarrow> set (relevant_entries P i pc xt) \<subseteq> set (relevant_entries (class_add P (C, cdec)) i pc xt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_class P C \<Longrightarrow> set (relevant_entries P i pc xt) \<subseteq> set (relevant_entries (class_add P (C, cdec)) i pc xt)
[PROOF STEP]
by(clarsimp simp: relevant_entries_def class_add_is_relevant_entry)


[STATEMENT]
lemma fresh_vsubstEnv_updEnv[simp]:
assumes rho: "goodEnv rho"
and *: "freshEnv ys y rho"
shows "(rho &[y1 // y]_ys) = (rho [y \<leftarrow> Var ys y1]_ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rho &[y1 // y]_ys = rho [y \<leftarrow> Var ys y1]_ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
goodEnv rho
freshEnv ys y rho

goal (1 subgoal):
 1. rho &[y1 // y]_ys = rho [y \<leftarrow> Var ys y1]_ys
[PROOF STEP]
unfolding vsubstEnv_def
[PROOF STATE]
proof (prove)
using this:
goodEnv rho
freshEnv ys y rho

goal (1 subgoal):
 1. rho &[Var ys y1 / y]_ys = rho [y \<leftarrow> Var ys y1]_ys
[PROOF STEP]
by simp


[STATEMENT]
lemma sscan_shift[simp]: "sscan f (xs @- ys) a = scan f xs a @- sscan f ys (fold f xs a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sscan f (xs @- ys) a = scan f xs a @- sscan f ys (fold f xs a)
[PROOF STEP]
by (induct xs arbitrary: a) (auto)


[STATEMENT]
lemma abs_complex_real[simp]: "abs x \<in> \<real>" for x :: complex
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x\<bar> \<in> \<real>
[PROOF STEP]
by (simp add: abs_complex_def)


[STATEMENT]
lemma ROI_init:
  assumes "CNV_ANNOT a a' R"
  assumes "(c,a')\<in>R"
  shows "(c,a)\<in>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c, a) \<in> R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
CNV_ANNOT a a' R
(c, a') \<in> R

goal (1 subgoal):
 1. (c, a) \<in> R
[PROOF STEP]
by simp


[STATEMENT]
lemma at_res1:"\<Turnstile>(re(c)) \<^bold>\<rightarrow> (\<^bold>\<forall>d. \<^bold>@d re(c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ts v. 0 < \<parallel>ext v\<parallel> \<and> len v ts c = ext v \<and> restrict v (res ts) c = lan v \<and> |lan v| = 1 \<longrightarrow> (\<forall>x v'. v = x > v' \<longrightarrow> 0 < \<parallel>ext v'\<parallel> \<and> len v' ts c = ext v' \<and> restrict v' (res ts) c = lan v' \<and> |lan v'| = 1)
[PROOF STEP]
by (metis (no_types, lifting) perfect_sensors.switch_length_stable
      restriction.switch_restrict_stable view.switch_def)


[STATEMENT]
lemma cosh_dist_perp_divide:
  assumes "M_perp l m" and "a \<in> hyp2" and "b \<in> hyp2" and "c \<in> hyp2"
  and "proj2_incident a l" and "proj2_incident b l" and "proj2_incident b m"
  and "proj2_incident c m"
  shows "cosh_dist b c = cosh_dist a c / cosh_dist b a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cosh_dist b c = cosh_dist a c / cosh_dist b a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cosh_dist b c = cosh_dist a c / cosh_dist b a
[PROOF STEP]
from \<open>b \<in> hyp2\<close> and \<open>a \<in> hyp2\<close>
[PROOF STATE]
proof (chain)
picking this:
b \<in> hyp2
a \<in> hyp2
[PROOF STEP]
have "cosh_dist b a > 0"
[PROOF STATE]
proof (prove)
using this:
b \<in> hyp2
a \<in> hyp2

goal (1 subgoal):
 1. 0 < cosh_dist b a
[PROOF STEP]
by (rule cosh_dist_positive)
[PROOF STATE]
proof (state)
this:
0 < cosh_dist b a

goal (1 subgoal):
 1. cosh_dist b c = cosh_dist a c / cosh_dist b a
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
M_perp l m
a \<in> hyp2
b \<in> hyp2
c \<in> hyp2
proj2_incident a l
proj2_incident b l
proj2_incident b m
proj2_incident c m
[PROOF STEP]
have "cosh_dist a c = cosh_dist b a * cosh_dist b c"
[PROOF STATE]
proof (prove)
using this:
M_perp l m
a \<in> hyp2
b \<in> hyp2
c \<in> hyp2
proj2_incident a l
proj2_incident b l
proj2_incident b m
proj2_incident c m

goal (1 subgoal):
 1. cosh_dist a c = cosh_dist b a * cosh_dist b c
[PROOF STEP]
by (rule cosh_dist_perp)
[PROOF STATE]
proof (state)
this:
cosh_dist a c = cosh_dist b a * cosh_dist b c

goal (1 subgoal):
 1. cosh_dist b c = cosh_dist a c / cosh_dist b a
[PROOF STEP]
with \<open>cosh_dist b a > 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < cosh_dist b a
cosh_dist a c = cosh_dist b a * cosh_dist b c
[PROOF STEP]
show "cosh_dist b c = cosh_dist a c / cosh_dist b a"
[PROOF STATE]
proof (prove)
using this:
0 < cosh_dist b a
cosh_dist a c = cosh_dist b a * cosh_dist b c

goal (1 subgoal):
 1. cosh_dist b c = cosh_dist a c / cosh_dist b a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cosh_dist b c = cosh_dist a c / cosh_dist b a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem hyp2_axiom11:
  "\<forall> X Y. (\<exists> a. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y)
  \<longrightarrow> (\<exists> b. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X Y. (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
proof (rule allI)+
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X Y. (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
fix X Y :: "hyp2 set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X Y. (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
show "(\<exists> a. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y)
    \<longrightarrow> (\<exists> b. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
 2. \<not> ?P \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
assume "X = {} \<or> Y = {}"
[PROOF STATE]
proof (state)
this:
X = {} \<or> Y = {}

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
 2. \<not> ?P \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
thus "(\<exists> a. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y)
      \<longrightarrow> (\<exists> b. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)"
[PROOF STATE]
proof (prove)
using this:
X = {} \<or> Y = {}

goal (1 subgoal):
 1. (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)

goal (1 subgoal):
 1. \<not> (X = {} \<or> Y = {}) \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (X = {} \<or> Y = {}) \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
assume "\<not> (X = {} \<or> Y = {})"
[PROOF STATE]
proof (state)
this:
\<not> (X = {} \<or> Y = {})

goal (1 subgoal):
 1. \<not> (X = {} \<or> Y = {}) \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
hence "X \<noteq> {}" and "Y \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
\<not> (X = {} \<or> Y = {})

goal (1 subgoal):
 1. X \<noteq> {} &&& Y \<noteq> {}
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
X \<noteq> {}
Y \<noteq> {}

goal (1 subgoal):
 1. \<not> (X = {} \<or> Y = {}) \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<noteq> {}
Y \<noteq> {}
[PROOF STEP]
obtain w and z where "w \<in> X" and "z \<in> Y"
[PROOF STATE]
proof (prove)
using this:
X \<noteq> {}
Y \<noteq> {}

goal (1 subgoal):
 1. (\<And>w z. \<lbrakk>w \<in> X; z \<in> Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<in> X
z \<in> Y

goal (1 subgoal):
 1. \<not> (X = {} \<or> Y = {}) \<Longrightarrow> (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
show "(\<exists> a. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y)
      \<longrightarrow> (\<exists> b. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
assume "\<exists> a. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y"
[PROOF STATE]
proof (state)
this:
\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y

goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y
[PROOF STEP]
obtain a where "\<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y"
[PROOF STATE]
proof (prove)
using this:
\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y

goal (1 subgoal):
 1. (\<And>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y

goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
let ?cX = "hyp2_rep ` X"
        and ?cY = "hyp2_rep ` Y"
        and ?ca = "hyp2_rep a"
        and ?cw = "hyp2_rep w"
        and ?cz = "hyp2_rep z"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
from \<open>\<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y
[PROOF STEP]
have "\<forall> cx cy. cx \<in> ?cX \<and> cy \<in> ?cY \<longrightarrow> B\<^sub>\<real> ?ca cx cy"
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y

goal (1 subgoal):
 1. \<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> hyp2_rep a cx cy
[PROOF STEP]
by (unfold real_hyp2_B_def) auto
[PROOF STATE]
proof (state)
this:
\<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> hyp2_rep a cx cy

goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
with real_euclid.A11' [of ?cX ?cY ?ca]
[PROOF STATE]
proof (chain)
picking this:
\<forall>x y. x \<in> hyp2_rep ` X \<and> y \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> hyp2_rep a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> hyp2_rep ` X \<and> y \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> x b y
\<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> hyp2_rep a cx cy
[PROOF STEP]
obtain cb where "\<forall> cx cy. cx \<in> ?cX \<and> cy \<in> ?cY \<longrightarrow> B\<^sub>\<real> cx cb cy"
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. x \<in> hyp2_rep ` X \<and> y \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> hyp2_rep a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> hyp2_rep ` X \<and> y \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> x b y
\<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> hyp2_rep a cx cy

goal (1 subgoal):
 1. (\<And>cb. \<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> cx cb cy \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> cx cb cy

goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
with \<open>w \<in> X\<close> and \<open>z \<in> Y\<close>
[PROOF STATE]
proof (chain)
picking this:
w \<in> X
z \<in> Y
\<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> cx cb cy
[PROOF STEP]
have "B\<^sub>\<real> ?cw cb ?cz"
[PROOF STATE]
proof (prove)
using this:
w \<in> X
z \<in> Y
\<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> cx cb cy

goal (1 subgoal):
 1. B\<^sub>\<real> hyp2_rep w cb hyp2_rep z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
B\<^sub>\<real> hyp2_rep w cb hyp2_rep z

goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
hence "hyp2_rep (hyp2_abs cb) = cb" (is "hyp2_rep ?b = cb")
[PROOF STATE]
proof (prove)
using this:
B\<^sub>\<real> hyp2_rep w cb hyp2_rep z

goal (1 subgoal):
 1. hyp2_rep (hyp2_abs cb) = cb
[PROOF STEP]
by (rule between_inverse)
[PROOF STATE]
proof (state)
this:
hyp2_rep (hyp2_abs cb) = cb

goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
with \<open>\<forall> cx cy. cx \<in> ?cX \<and> cy \<in> ?cY \<longrightarrow> B\<^sub>\<real> cx cb cy\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> cx cb cy
hyp2_rep (hyp2_abs cb) = cb
[PROOF STEP]
have "\<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x ?b y"
[PROOF STATE]
proof (prove)
using this:
\<forall>cx cy. cx \<in> hyp2_rep ` X \<and> cy \<in> hyp2_rep ` Y \<longrightarrow> B\<^sub>\<real> cx cb cy
hyp2_rep (hyp2_abs cb) = cb

goal (1 subgoal):
 1. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x hyp2_abs cb y
[PROOF STEP]
by (unfold real_hyp2_B_def) simp
[PROOF STATE]
proof (state)
this:
\<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x hyp2_abs cb y

goal (1 subgoal):
 1. \<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y \<Longrightarrow> \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
thus "\<exists> b. \<forall> x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y"
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x hyp2_abs cb y

goal (1 subgoal):
 1. \<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y
[PROOF STEP]
by (rule exI)
[PROOF STATE]
proof (state)
this:
\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>a. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K a x y) \<longrightarrow> (\<exists>b. \<forall>x y. x \<in> X \<and> y \<in> Y \<longrightarrow> B\<^sub>K x b y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ang_vec_opposite_opposite:
  assumes "z1 \<noteq> 0" and "z2 \<noteq> 0"
  shows "\<angle> (-z1) (-z2) = \<angle> z1 z2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<angle> z1 z2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<angle> z1 z2
[PROOF STEP]
have "\<angle> (-z1) (-z2) = \<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft>
[PROOF STEP]
using ang_vec_opposite1[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
\<angle> (- z1) ?z2.0 = \<downharpoonright>\<angle> z1 ?z2.0 - pi\<downharpoonleft>

goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft>
[PROOF STEP]
using ang_vec_opposite2[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
\<angle> (- z1) ?z2.0 = \<downharpoonright>\<angle> z1 ?z2.0 - pi\<downharpoonleft>
\<angle> ?z1.0 (- z2) = \<downharpoonright>\<angle> ?z1.0 z2 + pi\<downharpoonleft>

goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft>
[PROOF STEP]
using canon_ang_id[of pi, symmetric]
[PROOF STATE]
proof (prove)
using this:
\<angle> (- z1) ?z2.0 = \<downharpoonright>\<angle> z1 ?z2.0 - pi\<downharpoonleft>
\<angle> ?z1.0 (- z2) = \<downharpoonright>\<angle> ?z1.0 z2 + pi\<downharpoonleft>
- pi < pi \<and> pi \<le> pi \<Longrightarrow> pi = \<downharpoonright>pi\<downharpoonleft>

goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft>
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<angle> (- z1) (- z2) = \<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft>

goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<angle> z1 z2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<angle> (- z1) (- z2) = \<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft>

goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<angle> z1 z2
[PROOF STEP]
have "... = \<downharpoonright>\<angle> z1 z2\<downharpoonleft>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft> = \<downharpoonright>\<angle> z1 z2\<downharpoonleft>
[PROOF STEP]
by (subst canon_ang_diff[symmetric], simp)
[PROOF STATE]
proof (state)
this:
\<downharpoonright>\<downharpoonright>\<angle> z1 z2 + pi\<downharpoonleft> - \<downharpoonright>pi\<downharpoonleft>\<downharpoonleft> = \<downharpoonright>\<angle> z1 z2\<downharpoonleft>

goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<angle> z1 z2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<angle> (- z1) (- z2) = \<downharpoonright>\<angle> z1 z2\<downharpoonleft>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<angle> (- z1) (- z2) = \<downharpoonright>\<angle> z1 z2\<downharpoonleft>

goal (1 subgoal):
 1. \<angle> (- z1) (- z2) = \<angle> z1 z2
[PROOF STEP]
by (metis ang_vec_def canon_ang(1) canon_ang(2) canon_ang_id)
[PROOF STATE]
proof (state)
this:
\<angle> (- z1) (- z2) = \<angle> z1 z2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unat_ucast_10_32 :
  fixes x :: "10 word"
  shows "unat (ucast x :: word32) = unat x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (UCAST(10 \<rightarrow> 32) x) = unat x
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma check_tableau_normalized: "\<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<diamond> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow> \<triangle> (\<T> (check s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<diamond> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow> \<triangle> (\<T> (check s))
[PROOF STEP]
using check_tableau
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> \<U> ?s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s ?s; \<diamond> ?s; \<triangle> (\<T> ?s); \<nabla> ?s\<rbrakk> \<Longrightarrow> let s' = check ?s in ?v \<Turnstile>\<^sub>t \<T> ?s = ?v \<Turnstile>\<^sub>t \<T> s' \<and> \<triangle> (\<T> s') \<and> \<nabla> s' \<and> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s' \<and> \<diamond> s'

goal (1 subgoal):
 1. \<lbrakk>\<not> \<U> s; \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s; \<diamond> s; \<triangle> (\<T> s); \<nabla> s\<rbrakk> \<Longrightarrow> \<triangle> (\<T> (check s))
[PROOF STEP]
by (simp add: Let_def)


[STATEMENT]
lemma succ_valuation_satisfies:
  assumes "s \<succ> s'" "\<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s"
  shows "\<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'
[PROOF STEP]
from \<open>s \<succ> s'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<triangle> (\<T> s) \<and> \<diamond> s \<and> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s \<and> \<nabla> s \<and> s \<succ>\<^sub>x s' \<and> \<B>\<^sub>i s' = \<B>\<^sub>i s \<and> \<U>\<^sub>c s' = \<U>\<^sub>c s
[PROOF STEP]
obtain x\<^sub>i x\<^sub>j b where
    "\<triangle> (\<T> s)" "\<nabla> s"
    "min_lvar_not_in_bounds s = Some x\<^sub>i"
    "min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j"
    "b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i)"
    "s' = pivot_and_update x\<^sub>i x\<^sub>j b s"
[PROOF STATE]
proof (prove)
using this:
\<triangle> (\<T> s) \<and> \<diamond> s \<and> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s \<and> \<nabla> s \<and> s \<succ>\<^sub>x s' \<and> \<B>\<^sub>i s' = \<B>\<^sub>i s \<and> \<U>\<^sub>c s' = \<U>\<^sub>c s

goal (1 subgoal):
 1. (\<And>x\<^sub>i x\<^sub>j b. \<lbrakk>\<triangle> (\<T> s); \<nabla> s; min_lvar_not_in_bounds s = Some x\<^sub>i; min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j; b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i); s' = pivot_and_update x\<^sub>i x\<^sub>j b s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding gt_state_def
[PROOF STATE]
proof (prove)
using this:
\<triangle> (\<T> s) \<and> \<diamond> s \<and> \<Turnstile>\<^sub>n\<^sub>o\<^sub>l\<^sub>h\<^sub>s s \<and> \<nabla> s \<and> (\<exists>x\<^sub>i x\<^sub>j l\<^sub>i. let dir = if \<langle>\<V> s\<rangle> x\<^sub>i <\<^sub>l\<^sub>b \<B>\<^sub>l s x\<^sub>i then Positive else Negative in gt_state' dir s s' x\<^sub>i x\<^sub>j l\<^sub>i) \<and> \<B>\<^sub>i s' = \<B>\<^sub>i s \<and> \<U>\<^sub>c s' = \<U>\<^sub>c s

goal (1 subgoal):
 1. (\<And>x\<^sub>i x\<^sub>j b. \<lbrakk>\<triangle> (\<T> s); \<nabla> s; min_lvar_not_in_bounds s = Some x\<^sub>i; min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j; b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i); s' = pivot_and_update x\<^sub>i x\<^sub>j b s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: Let_def split: if_splits)
[PROOF STATE]
proof (state)
this:
\<triangle> (\<T> s)
\<nabla> s
min_lvar_not_in_bounds s = Some x\<^sub>i
min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j
b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i)
s' = pivot_and_update x\<^sub>i x\<^sub>j b s

goal (1 subgoal):
 1. \<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<triangle> (\<T> s)
\<nabla> s
min_lvar_not_in_bounds s = Some x\<^sub>i
min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j
b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i)
s' = pivot_and_update x\<^sub>i x\<^sub>j b s
[PROOF STEP]
have
    "x\<^sub>i \<in> lvars (\<T> s)"
    "x\<^sub>j \<in> rvars_of_lvar (\<T> s) x\<^sub>i"
[PROOF STATE]
proof (prove)
using this:
\<triangle> (\<T> s)
\<nabla> s
min_lvar_not_in_bounds s = Some x\<^sub>i
min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j
b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i)
s' = pivot_and_update x\<^sub>i x\<^sub>j b s

goal (1 subgoal):
 1. x\<^sub>i \<in> lvars (\<T> s) &&& x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
[PROOF STEP]
using min_lvar_not_in_bounds_lvars[of s x\<^sub>i]
[PROOF STATE]
proof (prove)
using this:
\<triangle> (\<T> s)
\<nabla> s
min_lvar_not_in_bounds s = Some x\<^sub>i
min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j
b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i)
s' = pivot_and_update x\<^sub>i x\<^sub>j b s
min_lvar_not_in_bounds s = Some x\<^sub>i \<longrightarrow> x\<^sub>i \<in> lvars (\<T> s)

goal (1 subgoal):
 1. x\<^sub>i \<in> lvars (\<T> s) &&& x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
[PROOF STEP]
using min_rvar_incdec_eq_Some_rvars[of Positive s "eq_for_lvar (\<T> s) x\<^sub>i" x\<^sub>j]
[PROOF STATE]
proof (prove)
using this:
\<triangle> (\<T> s)
\<nabla> s
min_lvar_not_in_bounds s = Some x\<^sub>i
min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j
b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i)
s' = pivot_and_update x\<^sub>i x\<^sub>j b s
min_lvar_not_in_bounds s = Some x\<^sub>i \<longrightarrow> x\<^sub>i \<in> lvars (\<T> s)
min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<Longrightarrow> x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)

goal (1 subgoal):
 1. x\<^sub>i \<in> lvars (\<T> s) &&& x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
[PROOF STEP]
using min_rvar_incdec_eq_Some_rvars[of Negative s "eq_for_lvar (\<T> s) x\<^sub>i" x\<^sub>j] \<open>\<triangle> (\<T> s)\<close>
[PROOF STATE]
proof (prove)
using this:
\<triangle> (\<T> s)
\<nabla> s
min_lvar_not_in_bounds s = Some x\<^sub>i
min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<or> min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j
b = the (\<B>\<^sub>l s x\<^sub>i) \<or> b = the (\<B>\<^sub>u s x\<^sub>i)
s' = pivot_and_update x\<^sub>i x\<^sub>j b s
min_lvar_not_in_bounds s = Some x\<^sub>i \<longrightarrow> x\<^sub>i \<in> lvars (\<T> s)
min_rvar_incdec Positive s x\<^sub>i = Inr x\<^sub>j \<Longrightarrow> x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
min_rvar_incdec Negative s x\<^sub>i = Inr x\<^sub>j \<Longrightarrow> x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
\<triangle> (\<T> s)

goal (1 subgoal):
 1. x\<^sub>i \<in> lvars (\<T> s) &&& x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
[PROOF STEP]
by (auto simp add: normalized_tableau_def)
[PROOF STATE]
proof (state)
this:
x\<^sub>i \<in> lvars (\<T> s)
x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)

goal (1 subgoal):
 1. \<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>i \<in> lvars (\<T> s)
x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x\<^sub>i \<in> lvars (\<T> s)
x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)

goal (1 subgoal):
 1. \<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'
[PROOF STEP]
using pivotandupdate_satisfies_tableau[of s x\<^sub>i x\<^sub>j b]
[PROOF STATE]
proof (prove)
using this:
x\<^sub>i \<in> lvars (\<T> s)
x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)\<rbrakk> \<Longrightarrow> \<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s \<longrightarrow> \<langle>\<V> (pivot_and_update x\<^sub>i x\<^sub>j b s)\<rangle> \<Turnstile>\<^sub>t \<T> s

goal (1 subgoal):
 1. \<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'
[PROOF STEP]
using pivotandupdate_tableau_equiv[of s x\<^sub>i x\<^sub>j ]
[PROOF STATE]
proof (prove)
using this:
x\<^sub>i \<in> lvars (\<T> s)
x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)\<rbrakk> \<Longrightarrow> \<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s \<longrightarrow> \<langle>\<V> (pivot_and_update x\<^sub>i x\<^sub>j b s)\<rangle> \<Turnstile>\<^sub>t \<T> s
\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)\<rbrakk> \<Longrightarrow> ?v \<Turnstile>\<^sub>t \<T> s = ?v \<Turnstile>\<^sub>t \<T> (pivot_and_update x\<^sub>i x\<^sub>j ?c s)

goal (1 subgoal):
 1. \<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'
[PROOF STEP]
using \<open>\<triangle> (\<T> s)\<close> \<open>\<nabla> s\<close> \<open>\<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s\<close> \<open>s' = pivot_and_update x\<^sub>i x\<^sub>j b s\<close>
[PROOF STATE]
proof (prove)
using this:
x\<^sub>i \<in> lvars (\<T> s)
x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)
\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)\<rbrakk> \<Longrightarrow> \<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s \<longrightarrow> \<langle>\<V> (pivot_and_update x\<^sub>i x\<^sub>j b s)\<rangle> \<Turnstile>\<^sub>t \<T> s
\<lbrakk>\<triangle> (\<T> s); \<nabla> s; x\<^sub>i \<in> lvars (\<T> s); x\<^sub>j \<in> rvars_eq (eq_for_lvar (\<T> s) x\<^sub>i)\<rbrakk> \<Longrightarrow> ?v \<Turnstile>\<^sub>t \<T> s = ?v \<Turnstile>\<^sub>t \<T> (pivot_and_update x\<^sub>i x\<^sub>j ?c s)
\<triangle> (\<T> s)
\<nabla> s
\<langle>\<V> s\<rangle> \<Turnstile>\<^sub>t \<T> s
s' = pivot_and_update x\<^sub>i x\<^sub>j b s

goal (1 subgoal):
 1. \<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>\<V> s'\<rangle> \<Turnstile>\<^sub>t \<T> s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma surj_Sup_pres_inj:
  fixes f :: "'a::complete_lattice_with_dual \<Rightarrow> 'b::complete_lattice_with_dual"
  assumes "surj f"
  and "Sup_pres f"
  shows "inj (radj f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (radj f)
[PROOF STEP]
by (metis assms comp_eq_dest_lhs id_apply injI surj_Sup_pres_id)


[STATEMENT]
lemma resultant_const[simp]:
  fixes a :: "'a :: comm_ring_1"
  shows "resultant [:a:] q = a ^ (degree q)"
    and "resultant p [:a:] = a ^ (degree p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resultant [:a:] q = a ^ degree q &&& resultant p [:a:] = a ^ degree p
[PROOF STEP]
unfolding resultant_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (sylvester_mat [:a:] q) = a ^ degree q &&& det (sylvester_mat p [:a:]) = a ^ degree p
[PROOF STEP]
unfolding sylvester_mat_const
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (a \<cdot>\<^sub>m 1\<^sub>m (degree q)) = a ^ degree q &&& det (a \<cdot>\<^sub>m 1\<^sub>m (degree p)) = a ^ degree p
[PROOF STEP]
by simp_all


[STATEMENT]
lemma filtermap_list_all[simp]: "filtermap pred func tr = map func tr \<longleftrightarrow> list_all pred tr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Filtermap.filtermap pred func tr = map func tr) = list_all pred tr
[PROOF STEP]
proof(induction tr)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (Filtermap.filtermap pred func [] = map func []) = list_all pred []
 2. \<And>a tr. (Filtermap.filtermap pred func tr = map func tr) = list_all pred tr \<Longrightarrow> (Filtermap.filtermap pred func (a # tr) = map func (a # tr)) = list_all pred (a # tr)
[PROOF STEP]
case (Cons trn tr)
[PROOF STATE]
proof (state)
this:
(Filtermap.filtermap pred func tr = map func tr) = list_all pred tr

goal (2 subgoals):
 1. (Filtermap.filtermap pred func [] = map func []) = list_all pred []
 2. \<And>a tr. (Filtermap.filtermap pred func tr = map func tr) = list_all pred tr \<Longrightarrow> (Filtermap.filtermap pred func (a # tr) = map func (a # tr)) = list_all pred (a # tr)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(Filtermap.filtermap pred func tr = map func tr) = list_all pred tr

goal (1 subgoal):
 1. (Filtermap.filtermap pred func (trn # tr) = map func (trn # tr)) = list_all pred (trn # tr)
[PROOF STEP]
apply (cases "pred trn")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(Filtermap.filtermap pred func tr = map func tr) = list_all pred tr; pred trn\<rbrakk> \<Longrightarrow> (Filtermap.filtermap pred func (trn # tr) = map func (trn # tr)) = list_all pred (trn # tr)
 2. \<lbrakk>(Filtermap.filtermap pred func tr = map func tr) = list_all pred tr; \<not> pred trn\<rbrakk> \<Longrightarrow> (Filtermap.filtermap pred func (trn # tr) = map func (trn # tr)) = list_all pred (trn # tr)
[PROOF STEP]
by (simp_all) (metis impossible_Cons length_filtermap length_map)
[PROOF STATE]
proof (state)
this:
(Filtermap.filtermap pred func (trn # tr) = map func (trn # tr)) = list_all pred (trn # tr)

goal (1 subgoal):
 1. (Filtermap.filtermap pred func [] = map func []) = list_all pred []
[PROOF STEP]
qed auto


[STATEMENT]
lemma "\<lfloor>(\<lambda>X. \<^bold>\<diamond>\<^bold>\<exists>X) \<^bold>\<down>(P::\<up>\<langle>\<up>\<zero>\<rangle>) \<^bold>\<rightarrow> \<^bold>\<diamond>((\<lambda>X. \<^bold>\<exists>X) \<^bold>\<down>P)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<^bold>\<diamond>\<lparr>mexistsB P w\<rparr> \<^bold>\<rightarrow> \<^bold>\<diamond>mexistsB P) w)\<rfloor>
[PROOF STEP]
nitpick[card 't=1, card i=2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>(\<lambda>w. (\<^bold>\<diamond>\<lparr>mexistsB P w\<rparr> \<^bold>\<rightarrow> \<^bold>\<diamond>mexistsB P) w)\<rfloor>
[PROOF STEP]
oops \<comment> \<open>countersatisfiable\<close>


[STATEMENT]
lemma cindexE_cong:
  assumes "finite s" and fg_eq:"\<And>x. \<lbrakk>a<x;x<b;x\<notin>s\<rbrakk> \<Longrightarrow> f x = g x"
  shows "cindexE a b f = cindexE a b g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindexE a b f = cindexE a b g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cindexE a b f = cindexE a b g
[PROOF STEP]
define left where
      "left=(\<lambda>f. (\<Sum>x | jumpF f (at_left x) \<noteq> 0 \<and> a < x \<and> x \<le> b. jumpF f (at_left x)))"
[PROOF STATE]
proof (state)
this:
left = (\<lambda>f. \<Sum>x | jumpF f (at_left x) \<noteq> 0 \<and> a < x \<and> x \<le> b. jumpF f (at_left x))

goal (1 subgoal):
 1. cindexE a b f = cindexE a b g
[PROOF STEP]
define right where
      "right=(\<lambda>f. (\<Sum>x | jumpF f (at_right x) \<noteq> 0 \<and> a \<le> x \<and> x < b. jumpF f (at_right x)))"
[PROOF STATE]
proof (state)
this:
right = (\<lambda>f. \<Sum>x | jumpF f (at_right x) \<noteq> 0 \<and> a \<le> x \<and> x < b. jumpF f (at_right x))

goal (1 subgoal):
 1. cindexE a b f = cindexE a b g
[PROOF STEP]
have "left f = left g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left f = left g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. left f = left g
[PROOF STEP]
have "jumpF f (at_left x) = jumpF g (at_left x)" when "a<x" "x\<le>b" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. jumpF f (at_left x) = jumpF g (at_left x)
[PROOF STEP]
proof (rule jumpF_cong)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. at_left x = at_left x
 2. \<forall>\<^sub>F x in at_left x. f x = g x
[PROOF STEP]
define cs where "cs \<equiv> {y\<in>s. a<y \<and> y<x}"
[PROOF STATE]
proof (state)
this:
cs \<equiv> {y \<in> s. a < y \<and> y < x}

goal (2 subgoals):
 1. at_left x = at_left x
 2. \<forall>\<^sub>F x in at_left x. f x = g x
[PROOF STEP]
define c where "c\<equiv> (if cs = {} then (x+a)/2 else Max cs)"
[PROOF STATE]
proof (state)
this:
c \<equiv> if cs = {} then (x + a) / 2 else Max cs

goal (2 subgoals):
 1. at_left x = at_left x
 2. \<forall>\<^sub>F x in at_left x. f x = g x
[PROOF STEP]
have "finite cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite cs
[PROOF STEP]
unfolding cs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {y \<in> s. a < y \<and> y < x}
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
finite s

goal (1 subgoal):
 1. finite {y \<in> s. a < y \<and> y < x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite cs

goal (2 subgoals):
 1. at_left x = at_left x
 2. \<forall>\<^sub>F x in at_left x. f x = g x
[PROOF STEP]
have "c<x \<and> (\<forall>y. c<y \<and> y<x \<longrightarrow> f y=g y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
proof (cases "cs={}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs = {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
cs = {}

goal (2 subgoals):
 1. cs = {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cs = {}
[PROOF STEP]
have "\<forall>y. c<y \<and> y<x \<longrightarrow> y \<notin> s"
[PROOF STATE]
proof (prove)
using this:
cs = {}

goal (1 subgoal):
 1. \<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s
[PROOF STEP]
unfolding cs_def c_def
[PROOF STATE]
proof (prove)
using this:
{y \<in> s. a < y \<and> y < x} = {}

goal (1 subgoal):
 1. \<forall>y. (if {y \<in> s. a < y \<and> y < x} = {} then (x + a) / 2 else Max {y \<in> s. a < y \<and> y < x}) < y \<and> y < x \<longrightarrow> y \<notin> s
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s

goal (2 subgoals):
 1. cs = {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s

goal (2 subgoals):
 1. cs = {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
have "c=(x+a)/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c = (x + a) / 2
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
cs = {}

goal (1 subgoal):
 1. c = (x + a) / 2
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
cs = {}

goal (1 subgoal):
 1. (if cs = {} then (x + a) / 2 else Max cs) = (x + a) / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c = (x + a) / 2

goal (2 subgoals):
 1. cs = {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s
c = (x + a) / 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s
c = (x + a) / 2

goal (1 subgoal):
 1. c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
using fg_eq
[PROOF STATE]
proof (prove)
using this:
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s
c = (x + a) / 2
\<lbrakk>a < ?x; ?x < b; ?x \<notin> s\<rbrakk> \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s
c = (x + a) / 2
\<lbrakk>a < ?x; ?x < b; ?x \<notin> s\<rbrakk> \<Longrightarrow> f ?x = g ?x
a < x
x \<le> b

goal (1 subgoal):
 1. c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
cs \<noteq> {}

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cs \<noteq> {}
[PROOF STEP]
have "c\<in>cs"
[PROOF STATE]
proof (prove)
using this:
cs \<noteq> {}

goal (1 subgoal):
 1. c \<in> cs
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
cs \<noteq> {}

goal (1 subgoal):
 1. (if cs = {} then (x + a) / 2 else Max cs) \<in> cs
[PROOF STEP]
using False \<open>finite cs\<close>
[PROOF STATE]
proof (prove)
using this:
cs \<noteq> {}
cs \<noteq> {}
finite cs

goal (1 subgoal):
 1. (if cs = {} then (x + a) / 2 else Max cs) \<in> cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<in> cs

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c \<in> cs

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
have "\<forall>y. c<y \<and> y<x \<longrightarrow> y \<notin> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s) "
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s)

goal (1 subgoal):
 1. \<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s)
[PROOF STEP]
obtain y' where "c<y'" "y'<x" "y'\<in>s"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s)

goal (1 subgoal):
 1. (\<And>y'. \<lbrakk>c < y'; y' < x; y' \<in> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c < y'
y' < x
y' \<in> s

goal (1 subgoal):
 1. \<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c < y'
y' < x
y' \<in> s
[PROOF STEP]
have "y'\<in>cs"
[PROOF STATE]
proof (prove)
using this:
c < y'
y' < x
y' \<in> s

goal (1 subgoal):
 1. y' \<in> cs
[PROOF STEP]
using \<open>c\<in>cs\<close>
[PROOF STATE]
proof (prove)
using this:
c < y'
y' < x
y' \<in> s
c \<in> cs

goal (1 subgoal):
 1. y' \<in> cs
[PROOF STEP]
unfolding cs_def
[PROOF STATE]
proof (prove)
using this:
c < y'
y' < x
y' \<in> s
c \<in> {y \<in> s. a < y \<and> y < x}

goal (1 subgoal):
 1. y' \<in> {y \<in> s. a < y \<and> y < x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y' \<in> cs

goal (1 subgoal):
 1. \<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y' \<in> cs
[PROOF STEP]
have "y'\<le>c"
[PROOF STATE]
proof (prove)
using this:
y' \<in> cs

goal (1 subgoal):
 1. y' \<le> c
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
y' \<in> cs

goal (1 subgoal):
 1. y' \<le> (if cs = {} then (x + a) / 2 else Max cs)
[PROOF STEP]
using False \<open>finite cs\<close>
[PROOF STATE]
proof (prove)
using this:
y' \<in> cs
cs \<noteq> {}
finite cs

goal (1 subgoal):
 1. y' \<le> (if cs = {} then (x + a) / 2 else Max cs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y' \<le> c

goal (1 subgoal):
 1. \<not> (\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y' \<le> c
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
y' \<le> c

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>c<y'\<close>
[PROOF STATE]
proof (prove)
using this:
y' \<le> c
c < y'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c \<in> cs
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c \<in> cs
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s

goal (1 subgoal):
 1. c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
unfolding cs_def
[PROOF STATE]
proof (prove)
using this:
c \<in> {y \<in> s. a < y \<and> y < x}
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s

goal (1 subgoal):
 1. c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
c \<in> {y \<in> s. a < y \<and> y < x}
\<forall>y. c < y \<and> y < x \<longrightarrow> y \<notin> s
a < x
x \<le> b

goal (1 subgoal):
 1. c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
by (auto intro!:fg_eq)
[PROOF STATE]
proof (state)
this:
c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)

goal (2 subgoals):
 1. at_left x = at_left x
 2. \<forall>\<^sub>F x in at_left x. f x = g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)
[PROOF STEP]
show "\<forall>\<^sub>F x in at_left x. f x = g x"
[PROOF STATE]
proof (prove)
using this:
c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_left x. f x = g x
[PROOF STEP]
unfolding eventually_at_left
[PROOF STATE]
proof (prove)
using this:
c < x \<and> (\<forall>y. c < y \<and> y < x \<longrightarrow> f y = g y)

goal (1 subgoal):
 1. \<exists>b<x. \<forall>y>b. y < x \<longrightarrow> f y = g y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at_left x. f x = g x

goal (1 subgoal):
 1. at_left x = at_left x
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>a < ?x; ?x \<le> b\<rbrakk> \<Longrightarrow> jumpF f (at_left ?x) = jumpF g (at_left ?x)

goal (1 subgoal):
 1. left f = left g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a < ?x; ?x \<le> b\<rbrakk> \<Longrightarrow> jumpF f (at_left ?x) = jumpF g (at_left ?x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a < ?x; ?x \<le> b\<rbrakk> \<Longrightarrow> jumpF f (at_left ?x) = jumpF g (at_left ?x)

goal (1 subgoal):
 1. left f = left g
[PROOF STEP]
unfolding left_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a < ?x; ?x \<le> b\<rbrakk> \<Longrightarrow> jumpF f (at_left ?x) = jumpF g (at_left ?x)

goal (1 subgoal):
 1. (\<Sum>x | jumpF f (at_left x) \<noteq> 0 \<and> a < x \<and> x \<le> b. jumpF f (at_left x)) = (\<Sum>x | jumpF g (at_left x) \<noteq> 0 \<and> a < x \<and> x \<le> b. jumpF g (at_left x))
[PROOF STEP]
by (auto intro: sum.cong)
[PROOF STATE]
proof (state)
this:
left f = left g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
left f = left g

goal (1 subgoal):
 1. cindexE a b f = cindexE a b g
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
left f = left g

goal (1 subgoal):
 1. cindexE a b f = cindexE a b g
[PROOF STEP]
have "right f = right g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. right f = right g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. right f = right g
[PROOF STEP]
have "jumpF f (at_right x) = jumpF g (at_right x)" when "a\<le>x" "x<b" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. jumpF f (at_right x) = jumpF g (at_right x)
[PROOF STEP]
proof (rule jumpF_cong)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. at_right x = at_right x
 2. \<forall>\<^sub>F x in at_right x. f x = g x
[PROOF STEP]
define cs where "cs \<equiv> {y\<in>s. x<y \<and> y<b}"
[PROOF STATE]
proof (state)
this:
cs \<equiv> {y \<in> s. x < y \<and> y < b}

goal (2 subgoals):
 1. at_right x = at_right x
 2. \<forall>\<^sub>F x in at_right x. f x = g x
[PROOF STEP]
define c where "c\<equiv> (if cs = {} then (x+b)/2 else Min cs)"
[PROOF STATE]
proof (state)
this:
c \<equiv> if cs = {} then (x + b) / 2 else Min cs

goal (2 subgoals):
 1. at_right x = at_right x
 2. \<forall>\<^sub>F x in at_right x. f x = g x
[PROOF STEP]
have "finite cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite cs
[PROOF STEP]
unfolding cs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {y \<in> s. x < y \<and> y < b}
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
finite s

goal (1 subgoal):
 1. finite {y \<in> s. x < y \<and> y < b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite cs

goal (2 subgoals):
 1. at_right x = at_right x
 2. \<forall>\<^sub>F x in at_right x. f x = g x
[PROOF STEP]
have "x<c \<and> (\<forall>y. x<y \<and> y<c \<longrightarrow> f y=g y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
proof (cases "cs={}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs = {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
cs = {}

goal (2 subgoals):
 1. cs = {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cs = {}
[PROOF STEP]
have "\<forall>y. x<y \<and> y<c \<longrightarrow> y \<notin> s"
[PROOF STATE]
proof (prove)
using this:
cs = {}

goal (1 subgoal):
 1. \<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s
[PROOF STEP]
unfolding cs_def c_def
[PROOF STATE]
proof (prove)
using this:
{y \<in> s. x < y \<and> y < b} = {}

goal (1 subgoal):
 1. \<forall>y. x < y \<and> y < (if {y \<in> s. x < y \<and> y < b} = {} then (x + b) / 2 else Min {y \<in> s. x < y \<and> y < b}) \<longrightarrow> y \<notin> s
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s

goal (2 subgoals):
 1. cs = {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s

goal (2 subgoals):
 1. cs = {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
have "c=(x+b)/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c = (x + b) / 2
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
cs = {}

goal (1 subgoal):
 1. c = (x + b) / 2
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
cs = {}

goal (1 subgoal):
 1. (if cs = {} then (x + b) / 2 else Min cs) = (x + b) / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c = (x + b) / 2

goal (2 subgoals):
 1. cs = {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
 2. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s
c = (x + b) / 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s
c = (x + b) / 2

goal (1 subgoal):
 1. x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
using fg_eq
[PROOF STATE]
proof (prove)
using this:
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s
c = (x + b) / 2
\<lbrakk>a < ?x; ?x < b; ?x \<notin> s\<rbrakk> \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s
c = (x + b) / 2
\<lbrakk>a < ?x; ?x < b; ?x \<notin> s\<rbrakk> \<Longrightarrow> f ?x = g ?x
a \<le> x
x < b

goal (1 subgoal):
 1. x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
cs \<noteq> {}

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cs \<noteq> {}
[PROOF STEP]
have "c\<in>cs"
[PROOF STATE]
proof (prove)
using this:
cs \<noteq> {}

goal (1 subgoal):
 1. c \<in> cs
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
cs \<noteq> {}

goal (1 subgoal):
 1. (if cs = {} then (x + b) / 2 else Min cs) \<in> cs
[PROOF STEP]
using False \<open>finite cs\<close>
[PROOF STATE]
proof (prove)
using this:
cs \<noteq> {}
cs \<noteq> {}
finite cs

goal (1 subgoal):
 1. (if cs = {} then (x + b) / 2 else Min cs) \<in> cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<in> cs

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c \<in> cs

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
have "\<forall>y. x<y \<and> y<c \<longrightarrow> y \<notin> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s) "
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s)

goal (1 subgoal):
 1. \<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s)
[PROOF STEP]
obtain y' where "x<y'" "y'<c" "y'\<in>s"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s)

goal (1 subgoal):
 1. (\<And>y'. \<lbrakk>x < y'; y' < c; y' \<in> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < y'
y' < c
y' \<in> s

goal (1 subgoal):
 1. \<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < y'
y' < c
y' \<in> s
[PROOF STEP]
have "y'\<in>cs"
[PROOF STATE]
proof (prove)
using this:
x < y'
y' < c
y' \<in> s

goal (1 subgoal):
 1. y' \<in> cs
[PROOF STEP]
using \<open>c\<in>cs\<close>
[PROOF STATE]
proof (prove)
using this:
x < y'
y' < c
y' \<in> s
c \<in> cs

goal (1 subgoal):
 1. y' \<in> cs
[PROOF STEP]
unfolding cs_def
[PROOF STATE]
proof (prove)
using this:
x < y'
y' < c
y' \<in> s
c \<in> {y \<in> s. x < y \<and> y < b}

goal (1 subgoal):
 1. y' \<in> {y \<in> s. x < y \<and> y < b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y' \<in> cs

goal (1 subgoal):
 1. \<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y' \<in> cs
[PROOF STEP]
have "y'\<ge>c"
[PROOF STATE]
proof (prove)
using this:
y' \<in> cs

goal (1 subgoal):
 1. c \<le> y'
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
y' \<in> cs

goal (1 subgoal):
 1. (if cs = {} then (x + b) / 2 else Min cs) \<le> y'
[PROOF STEP]
using False \<open>finite cs\<close>
[PROOF STATE]
proof (prove)
using this:
y' \<in> cs
cs \<noteq> {}
finite cs

goal (1 subgoal):
 1. (if cs = {} then (x + b) / 2 else Min cs) \<le> y'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<le> y'

goal (1 subgoal):
 1. \<not> (\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c \<le> y'
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
c \<le> y'

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>c>y'\<close>
[PROOF STATE]
proof (prove)
using this:
c \<le> y'
y' < c

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s

goal (1 subgoal):
 1. cs \<noteq> {} \<Longrightarrow> x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c \<in> cs
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c \<in> cs
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s

goal (1 subgoal):
 1. x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
unfolding cs_def
[PROOF STATE]
proof (prove)
using this:
c \<in> {y \<in> s. x < y \<and> y < b}
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s

goal (1 subgoal):
 1. x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
c \<in> {y \<in> s. x < y \<and> y < b}
\<forall>y. x < y \<and> y < c \<longrightarrow> y \<notin> s
a \<le> x
x < b

goal (1 subgoal):
 1. x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
by (auto intro!:fg_eq)
[PROOF STATE]
proof (state)
this:
x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)

goal (2 subgoals):
 1. at_right x = at_right x
 2. \<forall>\<^sub>F x in at_right x. f x = g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)
[PROOF STEP]
show "\<forall>\<^sub>F x in at_right x. f x = g x"
[PROOF STATE]
proof (prove)
using this:
x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_right x. f x = g x
[PROOF STEP]
unfolding eventually_at_right
[PROOF STATE]
proof (prove)
using this:
x < c \<and> (\<forall>y. x < y \<and> y < c \<longrightarrow> f y = g y)

goal (1 subgoal):
 1. \<exists>b>x. \<forall>y>x. y < b \<longrightarrow> f y = g y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at_right x. f x = g x

goal (1 subgoal):
 1. at_right x = at_right x
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>a \<le> ?x; ?x < b\<rbrakk> \<Longrightarrow> jumpF f (at_right ?x) = jumpF g (at_right ?x)

goal (1 subgoal):
 1. right f = right g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a \<le> ?x; ?x < b\<rbrakk> \<Longrightarrow> jumpF f (at_right ?x) = jumpF g (at_right ?x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<le> ?x; ?x < b\<rbrakk> \<Longrightarrow> jumpF f (at_right ?x) = jumpF g (at_right ?x)

goal (1 subgoal):
 1. right f = right g
[PROOF STEP]
unfolding right_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<le> ?x; ?x < b\<rbrakk> \<Longrightarrow> jumpF f (at_right ?x) = jumpF g (at_right ?x)

goal (1 subgoal):
 1. (\<Sum>x | jumpF f (at_right x) \<noteq> 0 \<and> a \<le> x \<and> x < b. jumpF f (at_right x)) = (\<Sum>x | jumpF g (at_right x) \<noteq> 0 \<and> a \<le> x \<and> x < b. jumpF g (at_right x))
[PROOF STEP]
by (auto intro: sum.cong)
[PROOF STATE]
proof (state)
this:
right f = right g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
right f = right g

goal (1 subgoal):
 1. cindexE a b f = cindexE a b g
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
left f = left g
right f = right g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
left f = left g
right f = right g

goal (1 subgoal):
 1. cindexE a b f = cindexE a b g
[PROOF STEP]
unfolding cindexE_def left_def right_def
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x | jumpF f (at_left x) \<noteq> 0 \<and> a < x \<and> x \<le> b. jumpF f (at_left x)) = (\<Sum>x | jumpF g (at_left x) \<noteq> 0 \<and> a < x \<and> x \<le> b. jumpF g (at_left x))
(\<Sum>x | jumpF f (at_right x) \<noteq> 0 \<and> a \<le> x \<and> x < b. jumpF f (at_right x)) = (\<Sum>x | jumpF g (at_right x) \<noteq> 0 \<and> a \<le> x \<and> x < b. jumpF g (at_right x))

goal (1 subgoal):
 1. (\<Sum>x | jumpF f (at_right x) \<noteq> 0 \<and> a \<le> x \<and> x < b. jumpF f (at_right x)) - (\<Sum>x | jumpF f (at_left x) \<noteq> 0 \<and> a < x \<and> x \<le> b. jumpF f (at_left x)) = (\<Sum>x | jumpF g (at_right x) \<noteq> 0 \<and> a \<le> x \<and> x < b. jumpF g (at_right x)) - (\<Sum>x | jumpF g (at_left x) \<noteq> 0 \<and> a < x \<and> x \<le> b. jumpF g (at_left x))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
cindexE a b f = cindexE a b g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tmin_le_tmax[intro, simp]: "tmin \<le> tmax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tmin \<le> tmax
[PROOF STEP]
using nonempty_set tmin tmax
[PROOF STATE]
proof (prove)
using this:
T \<noteq> {}
?t \<in> T \<Longrightarrow> tmin \<le> ?t
tmin \<in> T
?t \<in> T \<Longrightarrow> ?t \<le> tmax
tmax \<in> T

goal (1 subgoal):
 1. tmin \<le> tmax
[PROOF STEP]
by auto


[STATEMENT]
lemma (in Network) am_s_is_incoming:
  assumes "is_adj_map am"
  shows "E``{s} = set (am s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E `` {s} = set (am s)
[PROOF STEP]
using assms no_incoming_s
[PROOF STATE]
proof (prove)
using this:
is_adj_map am
\<forall>u. (u, s) \<notin> E

goal (1 subgoal):
 1. E `` {s} = set (am s)
[PROOF STEP]
unfolding is_adj_map_def
[PROOF STATE]
proof (prove)
using this:
\<forall>u. distinct (am u) \<and> set (am u) = E `` {u} \<union> E\<inverse> `` {u}
\<forall>u. (u, s) \<notin> E

goal (1 subgoal):
 1. E `` {s} = set (am s)
[PROOF STEP]
by auto


[STATEMENT]
lemma unity_periodic_arithmetic_mult:
  "periodic_arithmetic (\<lambda>n. unity_root k (m * int n)) k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. periodic_arithmetic (\<lambda>n. unity_root k (m * int n)) k
[PROOF STEP]
unfolding periodic_arithmetic_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. unity_root k (m * int (n + k)) = unity_root k (m * int n)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. unity_root k (m * int (n + k)) = unity_root k (m * int n)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. unity_root k (m * int (n + k)) = unity_root k (m * int n)
[PROOF STEP]
have "unity_root k (m * int (n + k)) =
        unity_root k (m*n + m*k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unity_root k (m * int (n + k)) = unity_root k (m * int n + m * int k)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
unity_root k (m * int (n + k)) = unity_root k (m * int n + m * int k)

goal (1 subgoal):
 1. \<And>n. unity_root k (m * int (n + k)) = unity_root k (m * int n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
unity_root k (m * int (n + k)) = unity_root k (m * int n + m * int k)

goal (1 subgoal):
 1. \<And>n. unity_root k (m * int (n + k)) = unity_root k (m * int n)
[PROOF STEP]
have "\<dots> = unity_root k (m*n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unity_root k (m * int n + m * int k) = unity_root k (m * int n)
[PROOF STEP]
using unity_root_mod[of k "m * int n"] unity_root_mod[of k "m * int n + m * int k"]
          mod_mult_self3
[PROOF STATE]
proof (prove)
using this:
unity_root k (m * int n mod int k) = unity_root k (m * int n)
unity_root k ((m * int n + m * int k) mod int k) = unity_root k (m * int n + m * int k)
(?c * ?b + ?a) mod ?b = ?a mod ?b

goal (1 subgoal):
 1. unity_root k (m * int n + m * int k) = unity_root k (m * int n)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
unity_root k (m * int n + m * int k) = unity_root k (m * int n)

goal (1 subgoal):
 1. \<And>n. unity_root k (m * int (n + k)) = unity_root k (m * int n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
unity_root k (m * int (n + k)) = unity_root k (m * int n)
[PROOF STEP]
show "unity_root k (m * int (n + k)) =
             unity_root k (m * int n)"
[PROOF STATE]
proof (prove)
using this:
unity_root k (m * int (n + k)) = unity_root k (m * int n)

goal (1 subgoal):
 1. unity_root k (m * int (n + k)) = unity_root k (m * int n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
unity_root k (m * int (n + k)) = unity_root k (m * int n)

goal:
No subgoals!
[PROOF STEP]
qed