[STATEMENT]
lemma nonneg_power_le:
  assumes "0 \<le> a" and "0 \<le> b" shows "a^n \<le> b^n \<longleftrightarrow> n = 0 \<or> a \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> a
(0::'a) \<le> b

goal (1 subgoal):
 1. (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
[PROOF STEP]
proof (cases rule: nonneg_linorder_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. a < b \<Longrightarrow> (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
 2. a = b \<Longrightarrow> (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
 3. b < a \<Longrightarrow> (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
[PROOF STEP]
case less
[PROOF STATE]
proof (state)
this:
a < b

goal (3 subgoals):
 1. a < b \<Longrightarrow> (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
 2. a = b \<Longrightarrow> (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
 3. b < a \<Longrightarrow> (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
[PROOF STEP]
with power_strict_mono[OF this, of n] assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(0::'a) \<le> a; 0 < n\<rbrakk> \<Longrightarrow> a ^ n < b ^ n
(0::'a) \<le> a
(0::'a) \<le> b
a < b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(0::'a) \<le> a; 0 < n\<rbrakk> \<Longrightarrow> a ^ n < b ^ n
(0::'a) \<le> a
(0::'a) \<le> b
a < b

goal (1 subgoal):
 1. (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
[PROOF STEP]
by (cases n, auto)
[PROOF STATE]
proof (state)
this:
(a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)

goal (2 subgoals):
 1. a = b \<Longrightarrow> (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
 2. b < a \<Longrightarrow> (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = b \<Longrightarrow> (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
 2. b < a \<Longrightarrow> (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
[PROOF STEP]
case eq
[PROOF STATE]
proof (state)
this:
a = b

goal (2 subgoals):
 1. a = b \<Longrightarrow> (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
 2. b < a \<Longrightarrow> (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = b

goal (1 subgoal):
 1. (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)

goal (1 subgoal):
 1. b < a \<Longrightarrow> (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b < a \<Longrightarrow> (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
[PROOF STEP]
case greater
[PROOF STATE]
proof (state)
this:
b < a

goal (1 subgoal):
 1. b < a \<Longrightarrow> (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
[PROOF STEP]
with power_strict_mono[OF this, of n] assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(0::'a) \<le> b; 0 < n\<rbrakk> \<Longrightarrow> b ^ n < a ^ n
(0::'a) \<le> a
(0::'a) \<le> b
b < a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(0::'a) \<le> b; 0 < n\<rbrakk> \<Longrightarrow> b ^ n < a ^ n
(0::'a) \<le> a
(0::'a) \<le> b
b < a

goal (1 subgoal):
 1. (a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)
[PROOF STEP]
by (cases n, auto)
[PROOF STATE]
proof (state)
this:
(a ^ n \<le> b ^ n) = (n = 0 \<or> a \<le> b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abs_cases:
  assumes "a = 0 \<Longrightarrow> thesis" and "\<bar>a\<bar> > 0 \<Longrightarrow> thesis" shows thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a = (0::'a) \<Longrightarrow> thesis
(0::'a) < \<bar>a\<bar> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma abs_linorder_cases[case_names less eq greater]:
  assumes "\<bar>a\<bar> < \<bar>b\<bar> \<Longrightarrow> thesis" and "\<bar>a\<bar> = \<bar>b\<bar> \<Longrightarrow> thesis" and "\<bar>b\<bar> < \<bar>a\<bar> \<Longrightarrow> thesis"
  shows thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
apply (cases rule: nonneg_linorder_cases[of "\<bar>a\<bar>" "\<bar>b\<bar>"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. (0::'a) \<le> \<bar>a\<bar>
 2. (0::'a) \<le> \<bar>b\<bar>
 3. \<bar>a\<bar> < \<bar>b\<bar> \<Longrightarrow> thesis
 4. \<bar>a\<bar> = \<bar>b\<bar> \<Longrightarrow> thesis
 5. \<bar>b\<bar> < \<bar>a\<bar> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<bar>a\<bar> < \<bar>b\<bar> \<Longrightarrow> thesis
\<bar>a\<bar> = \<bar>b\<bar> \<Longrightarrow> thesis
\<bar>b\<bar> < \<bar>a\<bar> \<Longrightarrow> thesis

goal (5 subgoals):
 1. (0::'a) \<le> \<bar>a\<bar>
 2. (0::'a) \<le> \<bar>b\<bar>
 3. \<bar>a\<bar> < \<bar>b\<bar> \<Longrightarrow> thesis
 4. \<bar>a\<bar> = \<bar>b\<bar> \<Longrightarrow> thesis
 5. \<bar>b\<bar> < \<bar>a\<bar> \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma [simp]:
  shows not_le_abs_abs: "\<not> \<bar>a\<bar> \<ge> \<bar>b\<bar> \<longleftrightarrow> \<bar>a\<bar> < \<bar>b\<bar>"
    and not_less_abs_abs: "\<not> \<bar>a\<bar> > \<bar>b\<bar> \<longleftrightarrow> \<bar>a\<bar> \<le> \<bar>b\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> \<bar>b\<bar> \<le> \<bar>a\<bar>) = (\<bar>a\<bar> < \<bar>b\<bar>) &&& (\<not> \<bar>b\<bar> < \<bar>a\<bar>) = (\<bar>a\<bar> \<le> \<bar>b\<bar>)
[PROOF STEP]
by (atomize(full), cases a b rule: abs_linorder_cases, auto simp: less_imp_le)


[STATEMENT]
lemma abs_power_less [simp]: "\<bar>a\<bar>^n < \<bar>b\<bar>^n \<longleftrightarrow> n > 0 \<and> \<bar>a\<bar> < \<bar>b\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<bar>a\<bar> ^ n < \<bar>b\<bar> ^ n) = (0 < n \<and> \<bar>a\<bar> < \<bar>b\<bar>)
[PROOF STEP]
by (subst nonneg_power_less, auto)


[STATEMENT]
lemma abs_power_le [simp]: "\<bar>a\<bar>^n \<le> \<bar>b\<bar>^n \<longleftrightarrow> n = 0 \<or> \<bar>a\<bar> \<le> \<bar>b\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<bar>a\<bar> ^ n \<le> \<bar>b\<bar> ^ n) = (n = 0 \<or> \<bar>a\<bar> \<le> \<bar>b\<bar>)
[PROOF STEP]
by (subst nonneg_power_le, auto)


[STATEMENT]
lemma abs_power_pos [simp]: "\<bar>a\<bar>^n > 0 \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((0::'a) < \<bar>a\<bar> ^ n) = (a \<noteq> (0::'a) \<or> n = 0)
[PROOF STEP]
using power_pos[of "\<bar>a\<bar>"]
[PROOF STATE]
proof (prove)
using this:
(0::'a) < \<bar>a\<bar> \<Longrightarrow> (0::'a) < \<bar>a\<bar> ^ ?n

goal (1 subgoal):
 1. ((0::'a) < \<bar>a\<bar> ^ n) = (a \<noteq> (0::'a) \<or> n = 0)
[PROOF STEP]
by (cases "n", auto)


[STATEMENT]
lemma abs_power_nonneg [intro!]: "\<bar>a\<bar>^n \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> \<bar>a\<bar> ^ n
[PROOF STEP]
by auto


[STATEMENT]
lemma abs_power_eq_0 [simp]: "\<bar>a\<bar>^n = 0 \<longleftrightarrow> a = 0 \<and> n \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<bar>a\<bar> ^ n = (0::'a)) = (a = (0::'a) \<and> n \<noteq> 0)
[PROOF STEP]
apply (induct n, force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. (\<bar>a\<bar> ^ n = (0::'a)) = (a = (0::'a) \<and> n \<noteq> 0) \<Longrightarrow> (\<bar>a\<bar> ^ Suc n = (0::'a)) = (a = (0::'a) \<and> Suc n \<noteq> 0)
[PROOF STEP]
apply (unfold power_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. (\<bar>a\<bar> ^ n = (0::'a)) = (a = (0::'a) \<and> n \<noteq> 0) \<Longrightarrow> (\<bar>a\<bar> * \<bar>a\<bar> ^ n = (0::'a)) = (a = (0::'a) \<and> Suc n \<noteq> 0)
[PROOF STEP]
apply (subst real_mult_eq_0_iff, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.


[STATEMENT]
lemma vec_index_vec_of_list [simp]: "vec_of_list xs $ i = xs ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_list xs $ i = xs ! i
[PROOF STEP]
by transfer (auto simp: mk_vec_def undef_vec_def dest: empty_nth)


[STATEMENT]
lemma vec_of_list_append: "vec_of_list (xs @ ys) = vec_of_list xs @\<^sub>v vec_of_list ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_list (xs @ ys) = vec_of_list xs @\<^sub>v vec_of_list ys
[PROOF STEP]
by (auto simp: nth_append)


[STATEMENT]
lemma linf_norm_vec_of_list:
  "\<parallel>vec_of_list xs\<parallel>\<^sub>\<infinity> = max_list (map abs xs @ [0])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>vec_of_list xs\<parallel>\<^sub>\<infinity> = Missing_Lemmas.max_list (map abs xs @ [0::'a])
[PROOF STEP]
by (simp add: linf_norm_vec_def)


[STATEMENT]
lemma linf_norm_vec_as_Greatest:
  fixes v :: "'a :: ring_1_abs_real_line vec"
  shows "\<parallel>v\<parallel>\<^sub>\<infinity> = (GREATEST a. a \<in> abs ` set (list_of_vec v) \<union> {0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>v\<parallel>\<^sub>\<infinity> = (GREATEST a. a \<in> abs ` set (list_of_vec v) \<union> {0::'a})
[PROOF STEP]
unfolding linf_norm_vec_of_list[of "list_of_vec v", simplified]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Missing_Lemmas.max_list (map abs (list_of_vec v) @ [0::'a]) = (GREATEST a. a \<in> abs ` set (list_of_vec v) \<union> {0::'a})
[PROOF STEP]
by (subst max_list_as_Greatest, auto)


[STATEMENT]
lemma vec_of_poly_pCons:
  assumes "f \<noteq> 0"
  shows "vec_of_poly (pCons a f) = vec_of_poly f @\<^sub>v vec_of_list [a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_poly (pCons a f) = vec_of_poly f @\<^sub>v vec_of_list [a]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<noteq> 0

goal (1 subgoal):
 1. vec_of_poly (pCons a f) = vec_of_poly f @\<^sub>v vec_of_list [a]
[PROOF STEP]
by (auto simp: vec_eq_iff Suc_diff_le)


[STATEMENT]
lemma vec_of_poly_as_vec_of_list:
  assumes "f \<noteq> 0"
  shows "vec_of_poly f = vec_of_list (rev (coeffs f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_poly f = vec_of_list (rev (coeffs f))
[PROOF STEP]
proof (insert assms, induct f)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<noteq> 0 \<Longrightarrow> vec_of_poly 0 = vec_of_list (rev (coeffs 0))
 2. \<And>a f. \<lbrakk>a \<noteq> (0::'a) \<or> f \<noteq> 0; f \<noteq> 0 \<Longrightarrow> vec_of_poly f = vec_of_list (rev (coeffs f)); pCons a f \<noteq> 0\<rbrakk> \<Longrightarrow> vec_of_poly (pCons a f) = vec_of_list (rev (coeffs (pCons a f)))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 \<noteq> 0

goal (2 subgoals):
 1. 0 \<noteq> 0 \<Longrightarrow> vec_of_poly 0 = vec_of_list (rev (coeffs 0))
 2. \<And>a f. \<lbrakk>a \<noteq> (0::'a) \<or> f \<noteq> 0; f \<noteq> 0 \<Longrightarrow> vec_of_poly f = vec_of_list (rev (coeffs f)); pCons a f \<noteq> 0\<rbrakk> \<Longrightarrow> vec_of_poly (pCons a f) = vec_of_list (rev (coeffs (pCons a f)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<noteq> 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 \<noteq> 0

goal (1 subgoal):
 1. vec_of_poly 0 = vec_of_list (rev (coeffs 0))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_of_poly 0 = vec_of_list (rev (coeffs 0))

goal (1 subgoal):
 1. \<And>a f. \<lbrakk>a \<noteq> (0::'a) \<or> f \<noteq> 0; f \<noteq> 0 \<Longrightarrow> vec_of_poly f = vec_of_list (rev (coeffs f)); pCons a f \<noteq> 0\<rbrakk> \<Longrightarrow> vec_of_poly (pCons a f) = vec_of_list (rev (coeffs (pCons a f)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a f. \<lbrakk>a \<noteq> (0::'a) \<or> f \<noteq> 0; f \<noteq> 0 \<Longrightarrow> vec_of_poly f = vec_of_list (rev (coeffs f)); pCons a f \<noteq> 0\<rbrakk> \<Longrightarrow> vec_of_poly (pCons a f) = vec_of_list (rev (coeffs (pCons a f)))
[PROOF STEP]
case (pCons a f)
[PROOF STATE]
proof (state)
this:
a \<noteq> (0::'a) \<or> f \<noteq> 0
f \<noteq> 0 \<Longrightarrow> vec_of_poly f = vec_of_list (rev (coeffs f))
pCons a f \<noteq> 0

goal (1 subgoal):
 1. \<And>a f. \<lbrakk>a \<noteq> (0::'a) \<or> f \<noteq> 0; f \<noteq> 0 \<Longrightarrow> vec_of_poly f = vec_of_list (rev (coeffs f)); pCons a f \<noteq> 0\<rbrakk> \<Longrightarrow> vec_of_poly (pCons a f) = vec_of_list (rev (coeffs (pCons a f)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> (0::'a) \<or> f \<noteq> 0
f \<noteq> 0 \<Longrightarrow> vec_of_poly f = vec_of_list (rev (coeffs f))
pCons a f \<noteq> 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a \<noteq> (0::'a) \<or> f \<noteq> 0
f \<noteq> 0 \<Longrightarrow> vec_of_poly f = vec_of_list (rev (coeffs f))
pCons a f \<noteq> 0

goal (1 subgoal):
 1. vec_of_poly (pCons a f) = vec_of_list (rev (coeffs (pCons a f)))
[PROOF STEP]
by (cases "f = 0", auto simp: vec_of_list_append vec_of_poly_pCons)
[PROOF STATE]
proof (state)
this:
vec_of_poly (pCons a f) = vec_of_list (rev (coeffs (pCons a f)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma linf_norm_vec_of_poly [simp]:
  fixes f :: "'a :: ring_1_abs_real_line poly"
  shows "\<parallel>vec_of_poly f\<parallel>\<^sub>\<infinity> = \<parallel>f\<parallel>\<^sub>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>vec_of_poly f\<parallel>\<^sub>\<infinity> = \<parallel>f\<parallel>\<^sub>\<infinity>
[PROOF STEP]
proof (cases "f = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f = 0 \<Longrightarrow> \<parallel>vec_of_poly f\<parallel>\<^sub>\<infinity> = \<parallel>f\<parallel>\<^sub>\<infinity>
 2. f \<noteq> 0 \<Longrightarrow> \<parallel>vec_of_poly f\<parallel>\<^sub>\<infinity> = \<parallel>f\<parallel>\<^sub>\<infinity>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
f \<noteq> 0

goal (2 subgoals):
 1. f = 0 \<Longrightarrow> \<parallel>vec_of_poly f\<parallel>\<^sub>\<infinity> = \<parallel>f\<parallel>\<^sub>\<infinity>
 2. f \<noteq> 0 \<Longrightarrow> \<parallel>vec_of_poly f\<parallel>\<^sub>\<infinity> = \<parallel>f\<parallel>\<^sub>\<infinity>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<noteq> 0

goal (1 subgoal):
 1. \<parallel>vec_of_poly f\<parallel>\<^sub>\<infinity> = \<parallel>f\<parallel>\<^sub>\<infinity>
[PROOF STEP]
apply (unfold vec_of_poly_as_vec_of_list linf_norm_vec_of_list linf_norm_poly_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> Missing_Lemmas.max_list (map abs (rev (coeffs f)) @ [0::'a]) = Missing_Lemmas.max_list (map abs (coeffs f) @ [0::'a])
[PROOF STEP]
apply (subst (1 2) max_list_as_Greatest, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<parallel>vec_of_poly f\<parallel>\<^sub>\<infinity> = \<parallel>f\<parallel>\<^sub>\<infinity>

goal (1 subgoal):
 1. f = 0 \<Longrightarrow> \<parallel>vec_of_poly f\<parallel>\<^sub>\<infinity> = \<parallel>f\<parallel>\<^sub>\<infinity>
[PROOF STEP]
qed simp


[STATEMENT]
lemma linf_norm_poly_as_Greatest:
  fixes f :: "'a :: ring_1_abs_real_line poly"
  shows "\<parallel>f\<parallel>\<^sub>\<infinity> = (GREATEST a. a \<in> abs ` set (coeffs f) \<union> {0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>f\<parallel>\<^sub>\<infinity> = (GREATEST a. a \<in> abs ` set (coeffs f) \<union> {0::'a})
[PROOF STEP]
using linf_norm_vec_as_Greatest[of "vec_of_poly f"]
[PROOF STATE]
proof (prove)
using this:
\<parallel>vec_of_poly f\<parallel>\<^sub>\<infinity> = (GREATEST a. a \<in> abs ` set (list_of_vec (vec_of_poly f)) \<union> {0::'a})

goal (1 subgoal):
 1. \<parallel>f\<parallel>\<^sub>\<infinity> = (GREATEST a. a \<in> abs ` set (coeffs f) \<union> {0::'a})
[PROOF STEP]
by simp


[STATEMENT]
lemma vec_index_le_linf_norm:
  fixes v :: "'a :: ring_1_abs_real_line vec"
  assumes "i < dim_vec v"
  shows "\<bar>v$i\<bar> \<le> \<parallel>v\<parallel>\<^sub>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>v $ i\<bar> \<le> \<parallel>v\<parallel>\<^sub>\<infinity>
[PROOF STEP]
apply (unfold linf_norm_vec_def, rule le_max_list)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> set (map abs (list_of_vec v) @ [0::'a]); b \<in> set (map abs (list_of_vec v) @ [0::'a])\<rbrakk> \<Longrightarrow> a \<le> b \<or> b \<le> a
 2. \<bar>v $ i\<bar> \<le> ?b
 3. ?b \<in> set (map abs (list_of_vec v) @ [0::'a])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < dim_vec v

goal (3 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> set (map abs (list_of_vec v) @ [0::'a]); b \<in> set (map abs (list_of_vec v) @ [0::'a])\<rbrakk> \<Longrightarrow> a \<le> b \<or> b \<le> a
 2. \<bar>v $ i\<bar> \<le> ?b
 3. ?b \<in> set (map abs (list_of_vec v) @ [0::'a])
[PROOF STEP]
apply (auto simp:  in_set_conv_nth intro!: imageI exI[of _ i])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.


[STATEMENT]
lemma coeff_le_linf_norm:
  fixes f :: "'a :: ring_1_abs_real_line poly"
  shows "\<bar>coeff f i\<bar> \<le> \<parallel>f\<parallel>\<^sub>\<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>coeff f i\<bar> \<le> \<parallel>f\<parallel>\<^sub>\<infinity>
[PROOF STEP]
using vec_index_le_linf_norm[of "degree f - i" "vec_of_poly f"]
[PROOF STATE]
proof (prove)
using this:
degree f - i < dim_vec (vec_of_poly f) \<Longrightarrow> \<bar>vec_of_poly f $ (degree f - i)\<bar> \<le> \<parallel>vec_of_poly f\<parallel>\<^sub>\<infinity>

goal (1 subgoal):
 1. \<bar>coeff f i\<bar> \<le> \<parallel>f\<parallel>\<^sub>\<infinity>
[PROOF STEP]
by (cases "i \<le> degree f", auto simp: coeff_eq_0)


[STATEMENT]
lemma sq_norm_as_sq_abs [simp]: "(sq_norm :: 'a :: conjugatable_ring_1_abs_real_line \<Rightarrow> 'a) = power2 \<circ> abs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sq_norm = power2 \<circ> abs
[PROOF STEP]
by auto


[STATEMENT]
lemma sq_norm_vec_le_linf_norm:
  fixes v :: "'a :: {conjugatable_ring_1_abs_real_line} vec"
  assumes "v \<in> carrier_vec n"
  shows "\<parallel>v\<parallel>\<^sup>2 \<le> of_nat n * \<parallel>v\<parallel>\<^sub>\<infinity>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>v\<parallel>\<^sup>2 \<le> of_nat n * \<parallel>v\<parallel>\<^sub>\<infinity>\<^sup>2
[PROOF STEP]
proof (insert assms, induct rule: carrier_vec_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<parallel>vNil\<parallel>\<^sup>2 \<le> of_nat 0 * \<parallel>vNil\<parallel>\<^sub>\<infinity>\<^sup>2
 2. \<And>n a v. \<lbrakk>v \<in> carrier_vec n; \<parallel>v\<parallel>\<^sup>2 \<le> of_nat n * \<parallel>v\<parallel>\<^sub>\<infinity>\<^sup>2\<rbrakk> \<Longrightarrow> \<parallel>vCons a v\<parallel>\<^sup>2 \<le> of_nat (Suc n) * \<parallel>vCons a v\<parallel>\<^sub>\<infinity>\<^sup>2
[PROOF STEP]
case (Suc n a v)
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec n
\<parallel>v\<parallel>\<^sup>2 \<le> of_nat n * \<parallel>v\<parallel>\<^sub>\<infinity>\<^sup>2

goal (2 subgoals):
 1. \<parallel>vNil\<parallel>\<^sup>2 \<le> of_nat 0 * \<parallel>vNil\<parallel>\<^sub>\<infinity>\<^sup>2
 2. \<And>n a v. \<lbrakk>v \<in> carrier_vec n; \<parallel>v\<parallel>\<^sup>2 \<le> of_nat n * \<parallel>v\<parallel>\<^sub>\<infinity>\<^sup>2\<rbrakk> \<Longrightarrow> \<parallel>vCons a v\<parallel>\<^sup>2 \<le> of_nat (Suc n) * \<parallel>vCons a v\<parallel>\<^sub>\<infinity>\<^sup>2
[PROOF STEP]
have [dest!]: "\<not> \<bar>a\<bar> \<le> \<parallel>v\<parallel>\<^sub>\<infinity> \<Longrightarrow> of_nat n * \<parallel>v\<parallel>\<^sub>\<infinity>\<^sup>2 \<le> of_nat n * \<bar>a\<bar>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<bar>a\<bar> \<le> \<parallel>v\<parallel>\<^sub>\<infinity> \<Longrightarrow> of_nat n * \<parallel>v\<parallel>\<^sub>\<infinity>\<^sup>2 \<le> of_nat n * \<bar>a\<bar>\<^sup>2
[PROOF STEP]
by (rule real_linorder_cases[of "\<bar>a\<bar>" "\<parallel>v\<parallel>\<^sub>\<infinity>"], insert Suc, auto simp: less_le intro!: power_mono mult_left_mono)
[PROOF STATE]
proof (state)
this:
\<not> \<bar>a\<bar> \<le> \<parallel>v\<parallel>\<^sub>\<infinity> \<Longrightarrow> of_nat n * \<parallel>v\<parallel>\<^sub>\<infinity>\<^sup>2 \<le> of_nat n * \<bar>a\<bar>\<^sup>2

goal (2 subgoals):
 1. \<parallel>vNil\<parallel>\<^sup>2 \<le> of_nat 0 * \<parallel>vNil\<parallel>\<^sub>\<infinity>\<^sup>2
 2. \<And>n a v. \<lbrakk>v \<in> carrier_vec n; \<parallel>v\<parallel>\<^sup>2 \<le> of_nat n * \<parallel>v\<parallel>\<^sub>\<infinity>\<^sup>2\<rbrakk> \<Longrightarrow> \<parallel>vCons a v\<parallel>\<^sup>2 \<le> of_nat (Suc n) * \<parallel>vCons a v\<parallel>\<^sub>\<infinity>\<^sup>2
[PROOF STEP]
from Suc
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec n
\<parallel>v\<parallel>\<^sup>2 \<le> of_nat n * \<parallel>v\<parallel>\<^sub>\<infinity>\<^sup>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
\<parallel>v\<parallel>\<^sup>2 \<le> of_nat n * \<parallel>v\<parallel>\<^sub>\<infinity>\<^sup>2

goal (1 subgoal):
 1. \<parallel>vCons a v\<parallel>\<^sup>2 \<le> of_nat (Suc n) * \<parallel>vCons a v\<parallel>\<^sub>\<infinity>\<^sup>2
[PROOF STEP]
by (auto simp: ring_distribs max_def intro!:add_mono power_mono)
[PROOF STATE]
proof (state)
this:
\<parallel>vCons a v\<parallel>\<^sup>2 \<le> of_nat (Suc n) * \<parallel>vCons a v\<parallel>\<^sub>\<infinity>\<^sup>2

goal (1 subgoal):
 1. \<parallel>vNil\<parallel>\<^sup>2 \<le> of_nat 0 * \<parallel>vNil\<parallel>\<^sub>\<infinity>\<^sup>2
[PROOF STEP]
qed simp


[STATEMENT]
lemma sq_norm_poly_le_linf_norm:
  fixes p :: "'a :: {conjugatable_ring_1_abs_real_line} poly"
  shows "\<parallel>p\<parallel>\<^sup>2 \<le> of_nat (degree p + 1) * \<parallel>p\<parallel>\<^sub>\<infinity>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>p\<parallel>\<^sup>2 \<le> of_nat (degree p + 1) * \<parallel>p\<parallel>\<^sub>\<infinity>\<^sup>2
[PROOF STEP]
using sq_norm_vec_le_linf_norm[of "vec_of_poly p" "degree p + 1"]
[PROOF STATE]
proof (prove)
using this:
vec_of_poly p \<in> carrier_vec (degree p + 1) \<Longrightarrow> \<parallel>vec_of_poly p\<parallel>\<^sup>2 \<le> of_nat (degree p + 1) * \<parallel>vec_of_poly p\<parallel>\<^sub>\<infinity>\<^sup>2

goal (1 subgoal):
 1. \<parallel>p\<parallel>\<^sup>2 \<le> of_nat (degree p + 1) * \<parallel>p\<parallel>\<^sub>\<infinity>\<^sup>2
[PROOF STEP]
by (auto simp: carrier_dim_vec)


[STATEMENT]
lemma coeff_le_sq_norm:
  fixes f :: "'a :: {conjugatable_ring_1_abs_real_line} poly"
  shows "\<bar>coeff f i\<bar>\<^sup>2 \<le> \<parallel>f\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>coeff f i\<bar>\<^sup>2 \<le> \<parallel>f\<parallel>\<^sup>2
[PROOF STEP]
proof (induct f arbitrary: i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<bar>coeff 0 i\<bar>\<^sup>2 \<le> \<parallel>0\<parallel>\<^sup>2
 2. \<And>a f i. \<lbrakk>a \<noteq> (0::'a) \<or> f \<noteq> 0; \<And>i. \<bar>coeff f i\<bar>\<^sup>2 \<le> \<parallel>f\<parallel>\<^sup>2\<rbrakk> \<Longrightarrow> \<bar>coeff (pCons a f) i\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2
[PROOF STEP]
case (pCons a f)
[PROOF STATE]
proof (state)
this:
a \<noteq> (0::'a) \<or> f \<noteq> 0
\<bar>coeff f ?i\<bar>\<^sup>2 \<le> \<parallel>f\<parallel>\<^sup>2

goal (2 subgoals):
 1. \<And>i. \<bar>coeff 0 i\<bar>\<^sup>2 \<le> \<parallel>0\<parallel>\<^sup>2
 2. \<And>a f i. \<lbrakk>a \<noteq> (0::'a) \<or> f \<noteq> 0; \<And>i. \<bar>coeff f i\<bar>\<^sup>2 \<le> \<parallel>f\<parallel>\<^sup>2\<rbrakk> \<Longrightarrow> \<bar>coeff (pCons a f) i\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>coeff (pCons a f) i\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2
[PROOF STEP]
proof (cases i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = 0 \<Longrightarrow> \<bar>coeff (pCons a f) i\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2
 2. \<And>nat. i = Suc nat \<Longrightarrow> \<bar>coeff (pCons a f) i\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2
[PROOF STEP]
case (Suc ii)
[PROOF STATE]
proof (state)
this:
i = Suc ii

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> \<bar>coeff (pCons a f) i\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2
 2. \<And>nat. i = Suc nat \<Longrightarrow> \<bar>coeff (pCons a f) i\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2
[PROOF STEP]
note pCons(2)[of ii]
[PROOF STATE]
proof (state)
this:
\<bar>coeff f ii\<bar>\<^sup>2 \<le> \<parallel>f\<parallel>\<^sup>2

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> \<bar>coeff (pCons a f) i\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2
 2. \<And>nat. i = Suc nat \<Longrightarrow> \<bar>coeff (pCons a f) i\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>coeff f ii\<bar>\<^sup>2 \<le> \<parallel>f\<parallel>\<^sup>2

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> \<bar>coeff (pCons a f) i\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2
 2. \<And>nat. i = Suc nat \<Longrightarrow> \<bar>coeff (pCons a f) i\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2
[PROOF STEP]
have "\<parallel>f\<parallel>\<^sup>2 \<le> \<bar>a\<bar>\<^sup>2 + \<parallel>f\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>f\<parallel>\<^sup>2 \<le> \<bar>a\<bar>\<^sup>2 + \<parallel>f\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<parallel>f\<parallel>\<^sup>2 \<le> \<bar>a\<bar>\<^sup>2 + \<parallel>f\<parallel>\<^sup>2

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> \<bar>coeff (pCons a f) i\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2
 2. \<And>nat. i = Suc nat \<Longrightarrow> \<bar>coeff (pCons a f) i\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>coeff f ii\<bar>\<^sup>2 \<le> \<bar>a\<bar>\<^sup>2 + \<parallel>f\<parallel>\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>coeff f ii\<bar>\<^sup>2 \<le> \<bar>a\<bar>\<^sup>2 + \<parallel>f\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<bar>coeff (pCons a f) i\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2
[PROOF STEP]
unfolding Suc
[PROOF STATE]
proof (prove)
using this:
\<bar>coeff f ii\<bar>\<^sup>2 \<le> \<bar>a\<bar>\<^sup>2 + \<parallel>f\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<bar>coeff (pCons a f) (Suc ii)\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>coeff (pCons a f) i\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2

goal (1 subgoal):
 1. i = 0 \<Longrightarrow> \<bar>coeff (pCons a f) i\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<bar>coeff (pCons a f) i\<bar>\<^sup>2 \<le> \<parallel>pCons a f\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<And>i. \<bar>coeff 0 i\<bar>\<^sup>2 \<le> \<parallel>0\<parallel>\<^sup>2
[PROOF STEP]
qed simp


[STATEMENT]
lemma max_norm_witness:
  fixes f :: "'a :: ordered_ring_abs poly"
  shows "\<exists> i. \<parallel>f\<parallel>\<^sub>\<infinity> = \<bar>coeff f i\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. \<parallel>f\<parallel>\<^sub>\<infinity> = \<bar>coeff f i\<bar>
[PROOF STEP]
by (induct f, auto simp add: max_def intro: exI[of _ "Suc _"] exI[of _ 0])


[STATEMENT]
lemma max_norm_le_sq_norm:
  fixes f ::  "'a :: conjugatable_ring_1_abs_real_line poly"
shows "\<parallel>f\<parallel>\<^sub>\<infinity>\<^sup>2 \<le> \<parallel>f\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>f\<parallel>\<^sub>\<infinity>\<^sup>2 \<le> \<parallel>f\<parallel>\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<parallel>f\<parallel>\<^sub>\<infinity>\<^sup>2 \<le> \<parallel>f\<parallel>\<^sup>2
[PROOF STEP]
from max_norm_witness[of f]
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. \<parallel>f\<parallel>\<^sub>\<infinity> = \<bar>coeff f i\<bar>
[PROOF STEP]
obtain i where id: "\<parallel>f\<parallel>\<^sub>\<infinity> = \<bar>coeff f i\<bar>"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. \<parallel>f\<parallel>\<^sub>\<infinity> = \<bar>coeff f i\<bar>

goal (1 subgoal):
 1. (\<And>i. \<parallel>f\<parallel>\<^sub>\<infinity> = \<bar>coeff f i\<bar> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<parallel>f\<parallel>\<^sub>\<infinity> = \<bar>coeff f i\<bar>

goal (1 subgoal):
 1. \<parallel>f\<parallel>\<^sub>\<infinity>\<^sup>2 \<le> \<parallel>f\<parallel>\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>f\<parallel>\<^sub>\<infinity>\<^sup>2 \<le> \<parallel>f\<parallel>\<^sup>2
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>coeff f i\<bar>\<^sup>2 \<le> \<parallel>f\<parallel>\<^sup>2
[PROOF STEP]
using coeff_le_sq_norm[of f i]
[PROOF STATE]
proof (prove)
using this:
\<bar>coeff f i\<bar>\<^sup>2 \<le> \<parallel>f\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<bar>coeff f i\<bar>\<^sup>2 \<le> \<parallel>f\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<parallel>f\<parallel>\<^sub>\<infinity>\<^sup>2 \<le> \<parallel>f\<parallel>\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in conjugatable_ring) conjugate_minus: "conjugate (x - y) = conjugate x - conjugate y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate (x - y) = conjugate x - conjugate y
[PROOF STEP]
by (unfold diff_conv_add_uminus conjugate_dist_add conjugate_neg, rule)


[STATEMENT]
lemma conjugate_1[simp]: "(conjugate 1 :: 'a :: {conjugatable_ring, ring_1}) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate (1::'a) = (1::'a)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. conjugate (1::'a) = (1::'a)
[PROOF STEP]
have "conjugate 1 * 1 = (conjugate 1 :: 'a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate (1::'a) * (1::'a) = conjugate (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
conjugate (1::'a) * (1::'a) = conjugate (1::'a)

goal (1 subgoal):
 1. conjugate (1::'a) = (1::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
conjugate (1::'a) * (1::'a) = conjugate (1::'a)

goal (1 subgoal):
 1. conjugate (1::'a) = (1::'a)
[PROOF STEP]
have "conjugate \<dots> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate (conjugate (1::'a)) = (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
conjugate (conjugate (1::'a)) = (1::'a)

goal (1 subgoal):
 1. conjugate (1::'a) = (1::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
conjugate (conjugate (1::'a) * (1::'a)) = (1::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
conjugate (conjugate (1::'a) * (1::'a)) = (1::'a)

goal (1 subgoal):
 1. conjugate (1::'a) = (1::'a)
[PROOF STEP]
by (unfold conjugate_dist_mul, simp)
[PROOF STATE]
proof (state)
this:
conjugate (1::'a) = (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma conjugate_of_int [simp]:
  "(conjugate (of_int x) :: 'a :: {conjugatable_ring,ring_1}) = of_int x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate (of_int x) = of_int x
[PROOF STEP]
proof (induct x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. conjugate (of_int (int n)) = of_int (int n)
 2. \<And>n. conjugate (of_int (- int (Suc n))) = of_int (- int (Suc n))
[PROOF STEP]
case (nonneg n)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>n. conjugate (of_int (int n)) = of_int (int n)
 2. \<And>n. conjugate (of_int (- int (Suc n))) = of_int (- int (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate (of_int (int n)) = of_int (int n)
[PROOF STEP]
by (induct n, auto simp: conjugate_dist_add)
[PROOF STATE]
proof (state)
this:
conjugate (of_int (int n)) = of_int (int n)

goal (1 subgoal):
 1. \<And>n. conjugate (of_int (- int (Suc n))) = of_int (- int (Suc n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. conjugate (of_int (- int (Suc n))) = of_int (- int (Suc n))
[PROOF STEP]
case (neg n)
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>n. conjugate (of_int (- int (Suc n))) = of_int (- int (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate (of_int (- int (Suc n))) = of_int (- int (Suc n))
[PROOF STEP]
apply (induct n, auto simp: conjugate_minus conjugate_neg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. conjugate (of_nat n) = of_nat n \<Longrightarrow> conjugate (2::'a) = (2::'a)
[PROOF STEP]
by (metis conjugate_1 conjugate_dist_add one_add_one)
[PROOF STATE]
proof (state)
this:
conjugate (of_int (- int (Suc n))) = of_int (- int (Suc n))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sq_norm_of_int: "\<parallel>map_vec of_int v :: 'a :: {conjugatable_ring,ring_1} vec\<parallel>\<^sup>2 = of_int \<parallel>v\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>of_int_hom.vec_hom v\<parallel>\<^sup>2 = of_int \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
unfolding sq_norm_vec_as_cscalar_prod scalar_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<dim_vec (conjugate (of_int_hom.vec_hom v)). of_int_hom.vec_hom v $ i * conjugate (of_int_hom.vec_hom v) $ i) = of_int (\<Sum>i = 0..<dim_vec (conjugate v). v $ i * conjugate v $ i)
[PROOF STEP]
unfolding hom_distribs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<dim_vec (conjugate (of_int_hom.vec_hom v)). of_int_hom.vec_hom v $ i * conjugate (of_int_hom.vec_hom v) $ i) = (\<Sum>x = 0..<dim_vec (conjugate v). of_int (v $ x) * of_int (conjugate v $ x))
[PROOF STEP]
by (rule sum.cong, auto)


[STATEMENT]
lemma norm1_ge_0: "norm1 (f :: 'a :: {abs,ordered_semiring_0,ordered_ab_group_add_abs}poly) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> norm1 f
[PROOF STEP]
unfolding norm1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> sum_list (map abs (coeffs f))
[PROOF STEP]
by (rule sum_list_nonneg, auto)


[STATEMENT]
lemma norm2_norm1_main_equality: fixes f :: "nat \<Rightarrow> 'a :: linordered_idom"
  shows "(\<Sum>i = 0..<n. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<n. f i * f i)
      + (\<Sum>i = 0..<n. \<Sum>j = 0..<n. if i = j then 0 else \<bar>f i\<bar> * \<bar>f j\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<n. f i * f i) + (\<Sum>i = 0..<n. \<Sum>j = 0..<n. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>)
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Sum>i = 0..<0. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<0. f i * f i) + (\<Sum>i = 0..<0. \<Sum>j = 0..<0. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>)
 2. \<And>n. (\<Sum>i = 0..<n. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<n. f i * f i) + (\<Sum>i = 0..<n. \<Sum>j = 0..<n. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>) \<Longrightarrow> (\<Sum>i = 0..<Suc n. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<Suc n. f i * f i) + (\<Sum>i = 0..<Suc n. \<Sum>j = 0..<Suc n. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<n. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<n. f i * f i) + (\<Sum>i = 0..<n. \<Sum>j = 0..<n. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>)

goal (2 subgoals):
 1. (\<Sum>i = 0..<0. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<0. f i * f i) + (\<Sum>i = 0..<0. \<Sum>j = 0..<0. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>)
 2. \<And>n. (\<Sum>i = 0..<n. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<n. f i * f i) + (\<Sum>i = 0..<n. \<Sum>j = 0..<n. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>) \<Longrightarrow> (\<Sum>i = 0..<Suc n. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<Suc n. f i * f i) + (\<Sum>i = 0..<Suc n. \<Sum>j = 0..<Suc n. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>)
[PROOF STEP]
have id: "{0 ..< Suc n} = insert n {0 ..< n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<Suc n} = insert n {0..<n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0..<Suc n} = insert n {0..<n}

goal (2 subgoals):
 1. (\<Sum>i = 0..<0. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<0. f i * f i) + (\<Sum>i = 0..<0. \<Sum>j = 0..<0. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>)
 2. \<And>n. (\<Sum>i = 0..<n. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<n. f i * f i) + (\<Sum>i = 0..<n. \<Sum>j = 0..<n. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>) \<Longrightarrow> (\<Sum>i = 0..<Suc n. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<Suc n. f i * f i) + (\<Sum>i = 0..<Suc n. \<Sum>j = 0..<Suc n. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>)
[PROOF STEP]
have id: "sum f {0 ..< Suc n} = f n + sum f {0 ..< n}" for f :: "nat \<Rightarrow> 'a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {0..<Suc n} = f n + sum f {0..<n}
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f (insert n {0..<n}) = f n + sum f {0..<n}
[PROOF STEP]
by (rule sum.insert, auto)
[PROOF STATE]
proof (state)
this:
sum ?f {0..<Suc n} = ?f n + sum ?f {0..<n}

goal (2 subgoals):
 1. (\<Sum>i = 0..<0. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<0. f i * f i) + (\<Sum>i = 0..<0. \<Sum>j = 0..<0. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>)
 2. \<And>n. (\<Sum>i = 0..<n. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<n. f i * f i) + (\<Sum>i = 0..<n. \<Sum>j = 0..<n. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>) \<Longrightarrow> (\<Sum>i = 0..<Suc n. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<Suc n. f i * f i) + (\<Sum>i = 0..<Suc n. \<Sum>j = 0..<Suc n. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<Suc n. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<Suc n. f i * f i) + (\<Sum>i = 0..<Suc n. \<Sum>j = 0..<Suc n. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>)
[PROOF STEP]
unfolding id power2_sum
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>f n\<bar>\<^sup>2 + (\<Sum>i = 0..<n. \<bar>f i\<bar>)\<^sup>2 + (2::'a) * \<bar>f n\<bar> * (\<Sum>i = 0..<n. \<bar>f i\<bar>) = f n * f n + (\<Sum>i = 0..<n. f i * f i) + ((if n = n then 0::'a else \<bar>f n\<bar> * \<bar>f n\<bar>) + (\<Sum>j = 0..<n. if n = j then 0::'a else \<bar>f n\<bar> * \<bar>f j\<bar>) + (\<Sum>i = 0..<n. (if i = n then 0::'a else \<bar>f i\<bar> * \<bar>f n\<bar>) + (\<Sum>j = 0..<n. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>)))
[PROOF STEP]
unfolding Suc
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>f n\<bar>\<^sup>2 + ((\<Sum>i = 0..<n. f i * f i) + (\<Sum>i = 0..<n. \<Sum>j = 0..<n. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>)) + (2::'a) * \<bar>f n\<bar> * (\<Sum>i = 0..<n. \<bar>f i\<bar>) = f n * f n + (\<Sum>i = 0..<n. f i * f i) + ((if n = n then 0::'a else \<bar>f n\<bar> * \<bar>f n\<bar>) + (\<Sum>j = 0..<n. if n = j then 0::'a else \<bar>f n\<bar> * \<bar>f j\<bar>) + (\<Sum>i = 0..<n. (if i = n then 0::'a else \<bar>f i\<bar> * \<bar>f n\<bar>) + (\<Sum>j = 0..<n. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>)))
[PROOF STEP]
by (auto simp: power2_eq_square sum_distrib_left sum.distrib ac_simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<Suc n. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<Suc n. f i * f i) + (\<Sum>i = 0..<Suc n. \<Sum>j = 0..<Suc n. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>)

goal (1 subgoal):
 1. (\<Sum>i = 0..<0. \<bar>f i\<bar>)\<^sup>2 = (\<Sum>i = 0..<0. f i * f i) + (\<Sum>i = 0..<0. \<Sum>j = 0..<0. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>)
[PROOF STEP]
qed auto


[STATEMENT]
lemma norm2_norm1_main_inequality: fixes f :: "nat \<Rightarrow> 'a :: linordered_idom"
  shows "(\<Sum>i = 0..<n. f i * f i) \<le> (\<Sum>i = 0..<n. \<bar>f i\<bar>)\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n. f i * f i) \<le> (\<Sum>i = 0..<n. \<bar>f i\<bar>)\<^sup>2
[PROOF STEP]
unfolding norm2_norm1_main_equality
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n. f i * f i) \<le> (\<Sum>i = 0..<n. f i * f i) + (\<Sum>i = 0..<n. \<Sum>j = 0..<n. if i = j then 0::'a else \<bar>f i\<bar> * \<bar>f j\<bar>)
[PROOF STEP]
by (auto intro!: sum_nonneg)


[STATEMENT]
lemma norm2_le_norm1_int: "\<parallel>f :: int poly\<parallel>\<^sup>2 \<le> (norm1 f)^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>f\<parallel>\<^sup>2 \<le> (norm1 f)\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<parallel>f\<parallel>\<^sup>2 \<le> (norm1 f)\<^sup>2
[PROOF STEP]
define F where "F = (!) (coeffs f)"
[PROOF STATE]
proof (state)
this:
F = (!) (coeffs f)

goal (1 subgoal):
 1. \<parallel>f\<parallel>\<^sup>2 \<le> (norm1 f)\<^sup>2
[PROOF STEP]
define n where "n = length (coeffs f)"
[PROOF STATE]
proof (state)
this:
n = length (coeffs f)

goal (1 subgoal):
 1. \<parallel>f\<parallel>\<^sup>2 \<le> (norm1 f)\<^sup>2
[PROOF STEP]
have 1: "\<parallel>f\<parallel>\<^sup>2 = (\<Sum>i = 0..<n. F i * F i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>f\<parallel>\<^sup>2 = (\<Sum>i = 0..<n. F i * F i)
[PROOF STEP]
unfolding norm1_def sq_norm_poly_def sum_list_sum_nth F_def n_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((!) (map sq_norm (coeffs f))) {0..<length (map sq_norm (coeffs f))} = (\<Sum>i = 0..<length (coeffs f). coeffs f ! i * coeffs f ! i)
[PROOF STEP]
by (subst sum.cong, auto simp: power2_eq_square)
[PROOF STATE]
proof (state)
this:
\<parallel>f\<parallel>\<^sup>2 = (\<Sum>i = 0..<n. F i * F i)

goal (1 subgoal):
 1. \<parallel>f\<parallel>\<^sup>2 \<le> (norm1 f)\<^sup>2
[PROOF STEP]
have 2: "norm1 f = (\<Sum>i = 0..<n. \<bar>F i\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm1 f = (\<Sum>i = 0..<n. \<bar>F i\<bar>)
[PROOF STEP]
unfolding norm1_def sq_norm_poly_def sum_list_sum_nth F_def n_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((!) (map abs (coeffs f))) {0..<length (map abs (coeffs f))} = (\<Sum>i = 0..<length (coeffs f). \<bar>coeffs f ! i\<bar>)
[PROOF STEP]
by (subst sum.cong, auto)
[PROOF STATE]
proof (state)
this:
norm1 f = (\<Sum>i = 0..<n. \<bar>F i\<bar>)

goal (1 subgoal):
 1. \<parallel>f\<parallel>\<^sup>2 \<le> (norm1 f)\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>f\<parallel>\<^sup>2 \<le> (norm1 f)\<^sup>2
[PROOF STEP]
unfolding 1 2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n. F i * F i) \<le> (\<Sum>i = 0..<n. \<bar>F i\<bar>)\<^sup>2
[PROOF STEP]
by (rule norm2_norm1_main_inequality)
[PROOF STATE]
proof (state)
this:
\<parallel>f\<parallel>\<^sup>2 \<le> (norm1 f)\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sq_norm_smult_vec: "sq_norm ((c :: 'a :: {conjugatable_ring,comm_semiring_0}) \<cdot>\<^sub>v v) = (c * conjugate c) * sq_norm v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>c \<cdot>\<^sub>v v\<parallel>\<^sup>2 = sq_norm_conjugate c * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
unfolding sq_norm_vec_as_cscalar_prod
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c \<cdot>\<^sub>v v) \<bullet>c (c \<cdot>\<^sub>v v) = sq_norm_conjugate c * (v \<bullet>c v)
[PROOF STEP]
by (subst scalar_prod_smult_left, force, unfold conjugate_smult_vec,
    subst scalar_prod_smult_right, force, simp add: ac_simps)


[STATEMENT]
lemma vec_le_sq_norm:
  fixes v :: "'a :: conjugatable_ring_1_abs_real_line vec"
  assumes "v \<in> carrier_vec n" "i < n"
  shows "\<bar>v $ i\<bar>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>v $ i\<bar>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
i < n

goal (1 subgoal):
 1. \<bar>v $ i\<bar>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
proof (induction v arbitrary: i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < 0 \<Longrightarrow> \<bar>vNil $ i\<bar>\<^sup>2 \<le> \<parallel>vNil\<parallel>\<^sup>2
 2. \<And>n a v i. \<lbrakk>v \<in> carrier_vec n; \<And>i. i < n \<Longrightarrow> \<bar>v $ i\<bar>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2; i < Suc n\<rbrakk> \<Longrightarrow> \<bar>vCons a v $ i\<bar>\<^sup>2 \<le> \<parallel>vCons a v\<parallel>\<^sup>2
[PROOF STEP]
case (Suc n a v i)
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec n
?i < n \<Longrightarrow> \<bar>v $ ?i\<bar>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
i < Suc n

goal (2 subgoals):
 1. \<And>i. i < 0 \<Longrightarrow> \<bar>vNil $ i\<bar>\<^sup>2 \<le> \<parallel>vNil\<parallel>\<^sup>2
 2. \<And>n a v i. \<lbrakk>v \<in> carrier_vec n; \<And>i. i < n \<Longrightarrow> \<bar>v $ i\<bar>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2; i < Suc n\<rbrakk> \<Longrightarrow> \<bar>vCons a v $ i\<bar>\<^sup>2 \<le> \<parallel>vCons a v\<parallel>\<^sup>2
[PROOF STEP]
note IH = Suc
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec n
?i < n \<Longrightarrow> \<bar>v $ ?i\<bar>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
i < Suc n

goal (2 subgoals):
 1. \<And>i. i < 0 \<Longrightarrow> \<bar>vNil $ i\<bar>\<^sup>2 \<le> \<parallel>vNil\<parallel>\<^sup>2
 2. \<And>n a v i. \<lbrakk>v \<in> carrier_vec n; \<And>i. i < n \<Longrightarrow> \<bar>v $ i\<bar>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2; i < Suc n\<rbrakk> \<Longrightarrow> \<bar>vCons a v $ i\<bar>\<^sup>2 \<le> \<parallel>vCons a v\<parallel>\<^sup>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>vCons a v $ i\<bar>\<^sup>2 \<le> \<parallel>vCons a v\<parallel>\<^sup>2
[PROOF STEP]
proof (cases i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = 0 \<Longrightarrow> \<bar>vCons a v $ i\<bar>\<^sup>2 \<le> \<parallel>vCons a v\<parallel>\<^sup>2
 2. \<And>nat. i = Suc nat \<Longrightarrow> \<bar>vCons a v $ i\<bar>\<^sup>2 \<le> \<parallel>vCons a v\<parallel>\<^sup>2
[PROOF STEP]
case (Suc ii)
[PROOF STATE]
proof (state)
this:
i = Suc ii

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> \<bar>vCons a v $ i\<bar>\<^sup>2 \<le> \<parallel>vCons a v\<parallel>\<^sup>2
 2. \<And>nat. i = Suc nat \<Longrightarrow> \<bar>vCons a v $ i\<bar>\<^sup>2 \<le> \<parallel>vCons a v\<parallel>\<^sup>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = Suc ii
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = Suc ii

goal (1 subgoal):
 1. \<bar>vCons a v $ i\<bar>\<^sup>2 \<le> \<parallel>vCons a v\<parallel>\<^sup>2
[PROOF STEP]
using IH IH(2)[of ii] le_add_same_cancel2 order_trans
[PROOF STATE]
proof (prove)
using this:
i = Suc ii
v \<in> carrier_vec n
?i < n \<Longrightarrow> \<bar>v $ ?i\<bar>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
i < Suc n
ii < n \<Longrightarrow> \<bar>v $ ii\<bar>\<^sup>2 \<le> \<parallel>v\<parallel>\<^sup>2
(?a \<le> ?b + ?a) = ((0::?'a) \<le> ?b)
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z

goal (1 subgoal):
 1. \<bar>vCons a v $ i\<bar>\<^sup>2 \<le> \<parallel>vCons a v\<parallel>\<^sup>2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<bar>vCons a v $ i\<bar>\<^sup>2 \<le> \<parallel>vCons a v\<parallel>\<^sup>2

goal (1 subgoal):
 1. i = 0 \<Longrightarrow> \<bar>vCons a v $ i\<bar>\<^sup>2 \<le> \<parallel>vCons a v\<parallel>\<^sup>2
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<bar>vCons a v $ i\<bar>\<^sup>2 \<le> \<parallel>vCons a v\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<And>i. i < 0 \<Longrightarrow> \<bar>vNil $ i\<bar>\<^sup>2 \<le> \<parallel>vNil\<parallel>\<^sup>2
[PROOF STEP]
qed auto


[STATEMENT]
lemma scalar_prod_ge_0: "(x :: 'a :: linordered_idom vec) \<bullet> x \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> x \<bullet> x
[PROOF STEP]
unfolding scalar_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> (\<Sum>i = 0..<dim_vec x. x $ i * x $ i)
[PROOF STEP]
by (rule sum_nonneg, auto)


[STATEMENT]
lemma cscalar_prod_is_scalar_prod[simp]: "(x :: 'a :: trivial_conjugatable_ordered_field vec) \<bullet>c y = x \<bullet> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<bullet>c y = x \<bullet> y
[PROOF STEP]
unfolding conjugate_id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<bullet>c y = x \<bullet> y
[PROOF STEP]
by (rule arg_cong[of _ _ "scalar_prod x"], auto)


[STATEMENT]
lemma scalar_prod_Cauchy:
  fixes u v::"'a :: {trivial_conjugatable_linordered_field} Matrix.vec"
  assumes "u \<in> carrier_vec n" "v \<in> carrier_vec n"
  shows "(u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
assume v_0: "v \<noteq> 0\<^sub>v n"
[PROOF STATE]
proof (state)
this:
v \<noteq> 0\<^sub>v n

goal (1 subgoal):
 1. (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
have "0 \<le> (u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v)" for r
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> (u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v)
[PROOF STEP]
by (simp add: scalar_prod_ge_0)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> (u - ?r \<cdot>\<^sub>v v) \<bullet> (u - ?r \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> (u - ?r \<cdot>\<^sub>v v) \<bullet> (u - ?r \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
have "(u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)" for r::'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)
[PROOF STEP]
have "(u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = (u - r \<cdot>\<^sub>v v) \<bullet> u - (u - r \<cdot>\<^sub>v v) \<bullet> (r \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = (u - r \<cdot>\<^sub>v v) \<bullet> u - (u - r \<cdot>\<^sub>v v) \<bullet> (r \<cdot>\<^sub>v v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u \<in> carrier_vec n
v \<in> carrier_vec n

goal (1 subgoal):
 1. (u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = (u - r \<cdot>\<^sub>v v) \<bullet> u - (u - r \<cdot>\<^sub>v v) \<bullet> (r \<cdot>\<^sub>v v)
[PROOF STEP]
by (subst scalar_prod_minus_distrib) auto
[PROOF STATE]
proof (state)
this:
(u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = (u - r \<cdot>\<^sub>v v) \<bullet> u - (u - r \<cdot>\<^sub>v v) \<bullet> (r \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. (u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = (u - r \<cdot>\<^sub>v v) \<bullet> u - (u - r \<cdot>\<^sub>v v) \<bullet> (r \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. (u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)
[PROOF STEP]
have "\<dots> = u \<bullet> u - (r \<cdot>\<^sub>v v) \<bullet> u - r * ((u - r \<cdot>\<^sub>v v) \<bullet> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u - r \<cdot>\<^sub>v v) \<bullet> u - (u - r \<cdot>\<^sub>v v) \<bullet> (r \<cdot>\<^sub>v v) = u \<bullet> u - (r \<cdot>\<^sub>v v) \<bullet> u - r * ((u - r \<cdot>\<^sub>v v) \<bullet> v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u \<in> carrier_vec n
v \<in> carrier_vec n

goal (1 subgoal):
 1. (u - r \<cdot>\<^sub>v v) \<bullet> u - (u - r \<cdot>\<^sub>v v) \<bullet> (r \<cdot>\<^sub>v v) = u \<bullet> u - (r \<cdot>\<^sub>v v) \<bullet> u - r * ((u - r \<cdot>\<^sub>v v) \<bullet> v)
[PROOF STEP]
by (subst minus_scalar_prod_distrib) auto
[PROOF STATE]
proof (state)
this:
(u - r \<cdot>\<^sub>v v) \<bullet> u - (u - r \<cdot>\<^sub>v v) \<bullet> (r \<cdot>\<^sub>v v) = u \<bullet> u - (r \<cdot>\<^sub>v v) \<bullet> u - r * ((u - r \<cdot>\<^sub>v v) \<bullet> v)

goal (1 subgoal):
 1. (u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(u - r \<cdot>\<^sub>v v) \<bullet> u - (u - r \<cdot>\<^sub>v v) \<bullet> (r \<cdot>\<^sub>v v) = u \<bullet> u - (r \<cdot>\<^sub>v v) \<bullet> u - r * ((u - r \<cdot>\<^sub>v v) \<bullet> v)

goal (1 subgoal):
 1. (u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)
[PROOF STEP]
have "\<dots> = u \<bullet> u - r * (v \<bullet> u) - r * (u \<bullet> v - r * (v \<bullet> v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<bullet> u - (r \<cdot>\<^sub>v v) \<bullet> u - r * ((u - r \<cdot>\<^sub>v v) \<bullet> v) = u \<bullet> u - r * (v \<bullet> u) - r * (u \<bullet> v - r * (v \<bullet> v))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u \<in> carrier_vec n
v \<in> carrier_vec n

goal (1 subgoal):
 1. u \<bullet> u - (r \<cdot>\<^sub>v v) \<bullet> u - r * ((u - r \<cdot>\<^sub>v v) \<bullet> v) = u \<bullet> u - r * (v \<bullet> u) - r * (u \<bullet> v - r * (v \<bullet> v))
[PROOF STEP]
by (subst minus_scalar_prod_distrib) auto
[PROOF STATE]
proof (state)
this:
u \<bullet> u - (r \<cdot>\<^sub>v v) \<bullet> u - r * ((u - r \<cdot>\<^sub>v v) \<bullet> v) = u \<bullet> u - r * (v \<bullet> u) - r * (u \<bullet> v - r * (v \<bullet> v))

goal (1 subgoal):
 1. (u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u \<bullet> u - (r \<cdot>\<^sub>v v) \<bullet> u - r * ((u - r \<cdot>\<^sub>v v) \<bullet> v) = u \<bullet> u - r * (v \<bullet> u) - r * (u \<bullet> v - r * (v \<bullet> v))

goal (1 subgoal):
 1. (u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)
[PROOF STEP]
have "\<dots> = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<bullet> u - r * (v \<bullet> u) - r * (u \<bullet> v - r * (v \<bullet> v)) = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)
[PROOF STEP]
using assms comm_scalar_prod
[PROOF STATE]
proof (prove)
using this:
u \<in> carrier_vec n
v \<in> carrier_vec n
\<lbrakk>?v\<^sub>1 \<in> carrier_vec ?n; ?v\<^sub>2 \<in> carrier_vec ?n\<rbrakk> \<Longrightarrow> ?v\<^sub>1 \<bullet> ?v\<^sub>2 = ?v\<^sub>2 \<bullet> ?v\<^sub>1

goal (1 subgoal):
 1. u \<bullet> u - r * (v \<bullet> u) - r * (u \<bullet> v - r * (v \<bullet> v)) = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
u \<bullet> u - r * (v \<bullet> u) - r * (u \<bullet> v - r * (v \<bullet> v)) = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)

goal (1 subgoal):
 1. (u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)

goal (1 subgoal):
 1. (u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(u - r \<cdot>\<^sub>v v) \<bullet> (u - r \<cdot>\<^sub>v v) = u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(u - ?r \<cdot>\<^sub>v v) \<bullet> (u - ?r \<cdot>\<^sub>v v) = u \<bullet> u - ?r * (u \<bullet> v) - ?r * (u \<bullet> v) + ?r * ?r * (v \<bullet> v)

goal (1 subgoal):
 1. (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(u - ?r \<cdot>\<^sub>v v) \<bullet> (u - ?r \<cdot>\<^sub>v v) = u \<bullet> u - ?r * (u \<bullet> v) - ?r * (u \<bullet> v) + ?r * ?r * (v \<bullet> v)

goal (1 subgoal):
 1. (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
have "u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v) = sq_norm u - (u \<bullet> v)\<^sup>2 / sq_norm v"
      if "r = (u \<bullet> v) / (v \<bullet> v)" for r
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<bullet> u - r * (u \<bullet> v) - r * (u \<bullet> v) + r * r * (v \<bullet> v) = \<parallel>u\<parallel>\<^sup>2 - (u \<bullet> v)\<^sup>2 / \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
unfolding that
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<bullet> u - u \<bullet> v / (v \<bullet> v) * (u \<bullet> v) - u \<bullet> v / (v \<bullet> v) * (u \<bullet> v) + u \<bullet> v / (v \<bullet> v) * (u \<bullet> v / (v \<bullet> v)) * (v \<bullet> v) = \<parallel>u\<parallel>\<^sup>2 - (u \<bullet> v)\<^sup>2 / \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
by (auto simp add: sq_norm_vec_as_cscalar_prod power2_eq_square)
[PROOF STATE]
proof (state)
this:
?r = u \<bullet> v / (v \<bullet> v) \<Longrightarrow> u \<bullet> u - ?r * (u \<bullet> v) - ?r * (u \<bullet> v) + ?r * ?r * (v \<bullet> v) = \<parallel>u\<parallel>\<^sup>2 - (u \<bullet> v)\<^sup>2 / \<parallel>v\<parallel>\<^sup>2

goal (1 subgoal):
 1. (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
?r1 = u \<bullet> v / (v \<bullet> v) \<Longrightarrow> (0::'a) \<le> \<parallel>u\<parallel>\<^sup>2 - (u \<bullet> v)\<^sup>2 / \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
have "0 \<le> \<parallel>u\<parallel>\<^sup>2 - (u \<bullet> v)\<^sup>2 / \<parallel>v\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
?r1 = u \<bullet> v / (v \<bullet> v) \<Longrightarrow> (0::'a) \<le> \<parallel>u\<parallel>\<^sup>2 - (u \<bullet> v)\<^sup>2 / \<parallel>v\<parallel>\<^sup>2

goal (1 subgoal):
 1. (0::'a) \<le> \<parallel>u\<parallel>\<^sup>2 - (u \<bullet> v)\<^sup>2 / \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> \<parallel>u\<parallel>\<^sup>2 - (u \<bullet> v)\<^sup>2 / \<parallel>v\<parallel>\<^sup>2

goal (1 subgoal):
 1. (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(0::'a) \<le> \<parallel>u\<parallel>\<^sup>2 - (u \<bullet> v)\<^sup>2 / \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
have "(u \<bullet> v)\<^sup>2 / \<parallel>v\<parallel>\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> \<parallel>u\<parallel>\<^sup>2 - (u \<bullet> v)\<^sup>2 / \<parallel>v\<parallel>\<^sup>2

goal (1 subgoal):
 1. (u \<bullet> v)\<^sup>2 / \<parallel>v\<parallel>\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u \<bullet> v)\<^sup>2 / \<parallel>v\<parallel>\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2

goal (1 subgoal):
 1. (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(u \<bullet> v)\<^sup>2 / \<parallel>v\<parallel>\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2
[PROOF STEP]
have "(u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
(u \<bullet> v)\<^sup>2 / \<parallel>v\<parallel>\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2

goal (1 subgoal):
 1. (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
using pos_divide_le_eq[of "\<parallel>v\<parallel>\<^sup>2"] v_0 assms
[PROOF STATE]
proof (prove)
using this:
(u \<bullet> v)\<^sup>2 / \<parallel>v\<parallel>\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2
(0::'a) < \<parallel>v\<parallel>\<^sup>2 \<Longrightarrow> (?b / \<parallel>v\<parallel>\<^sup>2 \<le> ?a) = (?b \<le> ?a * \<parallel>v\<parallel>\<^sup>2)
v \<noteq> 0\<^sub>v n
u \<in> carrier_vec n
v \<in> carrier_vec n

goal (1 subgoal):
 1. (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
(u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2

goal (1 subgoal):
 1. (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
v \<noteq> 0\<^sub>v n \<Longrightarrow> (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2

goal (1 subgoal):
 1. (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<noteq> 0\<^sub>v n \<Longrightarrow> (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<noteq> 0\<^sub>v n \<Longrightarrow> (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2

goal (1 subgoal):
 1. (u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2
[PROOF STEP]
by (fastforce simp add: assms)
[PROOF STATE]
proof (state)
this:
(u \<bullet> v)\<^sup>2 \<le> \<parallel>u\<parallel>\<^sup>2 * \<parallel>v\<parallel>\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma clock_jview_tInit:
  "clock_jview a (tInit s) = (0, envObs a s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clock_jview a (tInit s) = (0, envObs a s)
[PROOF STEP]
unfolding clock_jview_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (tLength (tInit s), envObs a (tLast (tInit s))) = (0, envObs a s)
[PROOF STEP]
by simp


[STATEMENT]
lemma clock_jview_tStep:
  "clock_jview a (t \<leadsto> s) = (Suc (tLength t), envObs a s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clock_jview a (t \<leadsto> s) = (Suc (tLength t), envObs a s)
[PROOF STEP]
unfolding clock_jview_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (tLength (t \<leadsto> s), envObs a (tLast (t \<leadsto> s))) = (Suc (tLength t), envObs a s)
[PROOF STEP]
by simp


[STATEMENT]
lemma clock_jview_tStepI[intro]:
  "\<lbrakk> tLength t = Suc n; envObs a (tLast t) = obs \<rbrakk>
     \<Longrightarrow> clock_jview a t = (Suc n, obs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tLength t = Suc n; envObs a (tLast t) = obs\<rbrakk> \<Longrightarrow> clock_jview a t = (Suc n, obs)
[PROOF STEP]
unfolding clock_jview_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tLength t = Suc n; envObs a (tLast t) = obs\<rbrakk> \<Longrightarrow> (tLength t, envObs a (tLast t)) = (Suc n, obs)
[PROOF STEP]
by (cases t) simp_all


[STATEMENT]
lemma clock_jview_inv:
  "clock_jview a t = (n, obs) \<Longrightarrow> envObs a (tLast t) = obs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clock_jview a t = (n, obs) \<Longrightarrow> envObs a (tLast t) = obs
[PROOF STEP]
unfolding clock_jview_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (tLength t, envObs a (tLast t)) = (n, obs) \<Longrightarrow> envObs a (tLast t) = obs
[PROOF STEP]
by (cases t) simp_all


[STATEMENT]
lemma clock_jview_eq_inv[iff]:
  "clock_jview a t' = clock_jview a t
    \<longleftrightarrow> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (clock_jview a t' = clock_jview a t) = (tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t))
[PROOF STEP]
by (fastforce simp: clock_jview_def)


[STATEMENT]
lemma clock_sim_range:
  "sim_range Clock.MC clock_simMC clock_sim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_range Clock.MC clock_simMC clock_sim
[PROOF STEP]
by (rule sim_rangeI) (simp_all add: clock_sim_def)


[STATEMENT]
lemma clock_simVal:
  "sim_val Clock.MC clock_simMC clock_sim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_val Clock.MC clock_simMC clock_sim
[PROOF STEP]
by (rule sim_valI) (simp add: clock_simVal_def clock_sim_def)


[STATEMENT]
lemma clock_sim_f:
  "sim_f Clock.MC clock_simMC clock_sim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_f Clock.MC clock_simMC clock_sim
[PROOF STEP]
apply (rule sim_fI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a u v. (u, v) \<in> relations Clock.MC a \<Longrightarrow> (clock_sim u, clock_sim v) \<in> relations clock_simMC a
[PROOF STEP]
apply (simp add: clock_simRels_def clock_sim_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a u v. (u, v) \<in> relations Clock.MC a \<Longrightarrow> tLast u \<in> clock_commonAbs u \<and> tLast v \<in> clock_commonAbs u \<and> envObs a (tLast u) = envObs a (tLast v) \<and> (clock_commonAbs u, tLast v) \<in> (\<lambda>x. (clock_commonAbs x, tLast x)) ` Clock.jkbpC
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a u v. (u, v) \<in> relations Clock.MC a \<Longrightarrow> tLast u \<in> clock_commonAbs u
 2. \<And>a u v. (u, v) \<in> relations Clock.MC a \<Longrightarrow> tLast v \<in> clock_commonAbs u
 3. \<And>a u v. (u, v) \<in> relations Clock.MC a \<Longrightarrow> envObs a (tLast u) = envObs a (tLast v)
 4. \<And>a u v. (u, v) \<in> relations Clock.MC a \<Longrightarrow> (clock_commonAbs u, tLast v) \<in> (\<lambda>x. (clock_commonAbs x, tLast x)) ` Clock.jkbpC
[PROOF STEP]
apply (fastforce intro!: imageI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a u v. (u, v) \<in> relations Clock.MC a \<Longrightarrow> tLast v \<in> clock_commonAbs u
 2. \<And>a u v. (u, v) \<in> relations Clock.MC a \<Longrightarrow> envObs a (tLast u) = envObs a (tLast v)
 3. \<And>a u v. (u, v) \<in> relations Clock.MC a \<Longrightarrow> (clock_commonAbs u, tLast v) \<in> (\<lambda>x. (clock_commonAbs x, tLast x)) ` Clock.jkbpC
[PROOF STEP]
apply (fastforce intro!: imageI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a u v. (u, v) \<in> relations Clock.MC a \<Longrightarrow> envObs a (tLast u) = envObs a (tLast v)
 2. \<And>a u v. (u, v) \<in> relations Clock.MC a \<Longrightarrow> (clock_commonAbs u, tLast v) \<in> (\<lambda>x. (clock_commonAbs x, tLast x)) ` Clock.jkbpC
[PROOF STEP]
apply (fastforce dest: Clock.mkM_simps(2))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a u v. (u, v) \<in> relations Clock.MC a \<Longrightarrow> (clock_commonAbs u, tLast v) \<in> (\<lambda>x. (clock_commonAbs x, tLast x)) ` Clock.jkbpC
[PROOF STEP]
apply (rule_tac x=v in image_eqI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a u v. (u, v) \<in> relations Clock.MC a \<Longrightarrow> (clock_commonAbs u, tLast v) = (clock_commonAbs v, tLast v)
 2. \<And>a u v. (u, v) \<in> relations Clock.MC a \<Longrightarrow> v \<in> Clock.jkbpC
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma clock_sim_r:
  "sim_r Clock.MC clock_simMC clock_sim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_r Clock.MC clock_simMC clock_sim
[PROOF STEP]
apply (rule sim_rI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a u v'. \<lbrakk>u \<in> worlds Clock.MC; (clock_sim u, v') \<in> relations clock_simMC a\<rbrakk> \<Longrightarrow> \<exists>v. (u, v) \<in> relations Clock.MC a \<and> clock_sim v = v'
[PROOF STEP]
apply (clarsimp simp: clock_simRels_def clock_sim_def cong del: image_cong_simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a u t x xa. \<lbrakk>u \<in> Clock.jkbpC; t \<in> Clock.jkbpC; tLast u = tLast x; x \<in> Clock.jkbpCn (tLength u); clock_commonAbs t = clock_commonAbs u; envObs a (tLast x) = envObs a (tLast xa); tLast t = tLast xa; xa \<in> Clock.jkbpCn (tLength u)\<rbrakk> \<Longrightarrow> \<exists>v. (u, v) \<in> relations Clock.MC a \<and> clock_commonAbs v = clock_commonAbs u \<and> tLast v = tLast xa
[PROOF STEP]
apply (rule_tac x=xa in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a u t x xa. \<lbrakk>u \<in> Clock.jkbpC; t \<in> Clock.jkbpC; tLast u = tLast x; x \<in> Clock.jkbpCn (tLength u); clock_commonAbs t = clock_commonAbs u; envObs a (tLast x) = envObs a (tLast xa); tLast t = tLast xa; xa \<in> Clock.jkbpCn (tLength u)\<rbrakk> \<Longrightarrow> (u, xa) \<in> relations Clock.MC a \<and> clock_commonAbs xa = clock_commonAbs u \<and> tLast xa = tLast xa
[PROOF STEP]
unfolding Clock.mkM_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a u t x xa. \<lbrakk>u \<in> Clock.jkbpC; t \<in> Clock.jkbpC; tLast u = tLast x; x \<in> Clock.jkbpCn (tLength u); clock_commonAbs t = clock_commonAbs u; envObs a (tLast x) = envObs a (tLast xa); tLast t = tLast xa; xa \<in> Clock.jkbpCn (tLength u)\<rbrakk> \<Longrightarrow> (u, xa) \<in> relations \<lparr>worlds = Clock.jkbpC, relations = \<lambda>a. rel_ext (\<lambda>(t, t'). {t, t'} \<subseteq> Clock.jkbpC \<and> clock_jview a t = clock_jview a t'), valuation = envVal \<circ> tLast\<rparr> a \<and> clock_commonAbs xa = clock_commonAbs u \<and> tLast xa = tLast xa
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma clock_sim:
  "sim Clock.MC clock_simMC clock_sim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim Clock.MC clock_simMC clock_sim
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim Clock.MC clock_simMC clock_sim
[PROOF STEP]
using clock_sim_range clock_simVal clock_sim_f clock_sim_r
[PROOF STATE]
proof (prove)
using this:
sim_range Clock.MC clock_simMC clock_sim
sim_val Clock.MC clock_simMC clock_sim
sim_f Clock.MC clock_simMC clock_sim
sim_r Clock.MC clock_simMC clock_sim

goal (1 subgoal):
 1. sim Clock.MC clock_simMC clock_sim
[PROOF STEP]
unfolding sim_def
[PROOF STATE]
proof (prove)
using this:
sim_range Clock.MC clock_simMC clock_sim
sim_val Clock.MC clock_simMC clock_sim
sim_f Clock.MC clock_simMC clock_sim
sim_r Clock.MC clock_simMC clock_sim

goal (1 subgoal):
 1. sim_range Clock.MC clock_simMC clock_sim \<and> sim_val Clock.MC clock_simMC clock_sim \<and> sim_f Clock.MC clock_simMC clock_sim \<and> sim_r Clock.MC clock_simMC clock_sim
[PROOF STEP]
by blast


[STATEMENT]
lemma aec_refl[intro, simp]:
  "t \<in> Clock.jkbpC \<Longrightarrow> tLast t \<in> agent_abs a t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> Clock.jkbpC \<Longrightarrow> tLast t \<in> agent_abs a t
[PROOF STEP]
unfolding agent_abs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> Clock.jkbpC \<Longrightarrow> tLast t \<in> rel_ext (\<lambda>uu_. \<exists>t'. uu_ = tLast t' \<and> t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)
[PROOF STEP]
by auto


[STATEMENT]
lemma aec_cec_subset:
  assumes tC: "t \<in> Clock.jkbpC"
      and aec: "ODList.toSet aec = agent_abs a t"
      and cec: "ODList.toSet cec = common_abs t"
  shows "x \<in> ODList.toSet aec \<Longrightarrow> x \<in> ODList.toSet cec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> toSet aec \<Longrightarrow> x \<in> toSet cec
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC
toSet aec = agent_abs a t
toSet cec = common_abs t

goal (1 subgoal):
 1. x \<in> toSet aec \<Longrightarrow> x \<in> toSet cec
[PROOF STEP]
unfolding agent_abs_def common_abs_def
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC
toSet aec = rel_ext (\<lambda>uu_. \<exists>t'. uu_ = tLast t' \<and> t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)
toSet cec = clock_commonAbs t

goal (1 subgoal):
 1. x \<in> toSet aec \<Longrightarrow> x \<in> toSet cec
[PROOF STEP]
by fastforce


[STATEMENT]
lemma clock_simAbs_refl:
  assumes tC: "t \<in> Clock.jkbpC"
      and ec: "clock_simAbs ec = Clock.sim_equiv_class a t"
  shows "clock_sim t \<in> clock_simAbs ec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clock_sim t \<in> clock_simAbs ec
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC
clock_simAbs ec = Clock.sim_equiv_class a t

goal (1 subgoal):
 1. clock_sim t \<in> clock_simAbs ec
[PROOF STEP]
by simp


[STATEMENT]
lemma common_abs:
  assumes tC: "t \<in> Clock.jkbpC"
  assumes ec: "clock_simAbs ec = Clock.sim_equiv_class a t"
  shows "ODList.toSet (fst ec) = common_abs t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toSet (fst ec) = common_abs t
[PROOF STEP]
using tC clock_simAbs_refl[OF tC ec]
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC
clock_sim t \<in> clock_simAbs ec

goal (1 subgoal):
 1. toSet (fst ec) = common_abs t
[PROOF STEP]
unfolding clock_sim_def clock_simAbs_def common_abs_def
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC
(clock_commonAbs t, tLast t) \<in> rel_ext (\<lambda>uu_. \<exists>s. uu_ = (toSet (fst ec), s) \<and> s \<in> toSet (snd ec))

goal (1 subgoal):
 1. toSet (fst ec) = clock_commonAbs t
[PROOF STEP]
by (auto simp: ODList.toSet_def[symmetric])


[STATEMENT]
lemma agent_abs:
  assumes tC: "t \<in> Clock.jkbpC"
  assumes ec: "clock_simAbs ec = Clock.sim_equiv_class a t"
  shows "ODList.toSet (snd ec) = agent_abs a t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toSet (snd ec) = agent_abs a t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC
clock_simAbs ec = Clock.sim_equiv_class a t

goal (1 subgoal):
 1. toSet (snd ec) = agent_abs a t
[PROOF STEP]
unfolding clock_sim_def clock_simAbs_def agent_abs_def
[PROOF STATE]
proof (prove)
using this:
t \<in> Clock.jkbpC
rel_ext (\<lambda>uu_. \<exists>s. uu_ = (toSet (fst ec), s) \<and> s \<in> toSet (snd ec)) = (\<lambda>t. (clock_commonAbs t, tLast t)) ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)

goal (1 subgoal):
 1. toSet (snd ec) = rel_ext (\<lambda>uu_. \<exists>t'. uu_ = tLast t' \<and> t' \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>t \<in> Clock.jkbpC; rel_ext (\<lambda>uu_. \<exists>s. uu_ = (toSet (fst ec), s) \<and> s \<in> toSet (snd ec)) = (\<lambda>x. (clock_commonAbs t, tLast x)) ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); x \<in> toSet (snd ec)\<rbrakk> \<Longrightarrow> \<exists>t'. x = tLast t' \<and> t' \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)
[PROOF STEP]
apply (subgoal_tac "(ODList.toSet (fst ec), x) \<in> {(ODList.toSet (fst ec), s) |s. s \<in> ODList.toSet (snd ec)}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>t \<in> Clock.jkbpC; rel_ext (\<lambda>uu_. \<exists>s. uu_ = (toSet (fst ec), s) \<and> s \<in> toSet (snd ec)) = (\<lambda>x. (clock_commonAbs t, tLast x)) ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); x \<in> toSet (snd ec); (toSet (fst ec), x) \<in> rel_ext (\<lambda>uu_. \<exists>s. uu_ = (toSet (fst ec), s) \<and> s \<in> toSet (snd ec))\<rbrakk> \<Longrightarrow> \<exists>t'. x = tLast t' \<and> t' \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)
 2. \<And>x. \<lbrakk>t \<in> Clock.jkbpC; rel_ext (\<lambda>uu_. \<exists>s. uu_ = (toSet (fst ec), s) \<and> s \<in> toSet (snd ec)) = (\<lambda>x. (clock_commonAbs t, tLast x)) ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); x \<in> toSet (snd ec)\<rbrakk> \<Longrightarrow> (toSet (fst ec), x) \<in> rel_ext (\<lambda>uu_. \<exists>s. uu_ = (toSet (fst ec), s) \<and> s \<in> toSet (snd ec))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
(* FIXME filthy *)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma clock_simAbs_inj_on:
  "inj_on clock_simAbs { x . clock_simAbs x \<in> Clock.jkbpSEC }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on clock_simAbs (rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on clock_simAbs (rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)))
[PROOF STEP]
proof(rule inj_onI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)); y \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)); clock_simAbs x = clock_simAbs y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)); y \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)); clock_simAbs x = clock_simAbs y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume x: "x \<in> { x . clock_simAbs x \<in> Clock.jkbpSEC }"
     and y: "y \<in> { x . clock_simAbs x \<in> Clock.jkbpSEC }"
     and xy: "clock_simAbs x = clock_simAbs y"
[PROOF STATE]
proof (state)
this:
x \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC))
y \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC))
clock_simAbs x = clock_simAbs y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)); y \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)); clock_simAbs x = clock_simAbs y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC))
[PROOF STEP]
obtain a t
    where tC: "t \<in> Clock.jkbpC"
      and ec: "clock_simAbs x = Clock.sim_equiv_class a t"
[PROOF STATE]
proof (prove)
using this:
x \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC))

goal (1 subgoal):
 1. (\<And>t a. \<lbrakk>t \<in> Clock.jkbpC; clock_simAbs x = Clock.sim_equiv_class a t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> Clock.jkbpC
clock_simAbs x = Clock.sim_equiv_class a t

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)); y \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)); clock_simAbs x = clock_simAbs y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from common_abs[OF tC ec] common_abs[OF tC trans[OF xy[symmetric] ec], symmetric]
[PROOF STATE]
proof (chain)
picking this:
toSet (fst x) = common_abs t
common_abs t = toSet (fst y)
[PROOF STEP]
have "fst x = fst y"
[PROOF STATE]
proof (prove)
using this:
toSet (fst x) = common_abs t
common_abs t = toSet (fst y)

goal (1 subgoal):
 1. fst x = fst y
[PROOF STEP]
by (blast intro: injD[OF toSet_inj])
[PROOF STATE]
proof (state)
this:
fst x = fst y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)); y \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)); clock_simAbs x = clock_simAbs y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst x = fst y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)); y \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)); clock_simAbs x = clock_simAbs y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from agent_abs[OF tC ec] agent_abs[OF tC trans[OF xy[symmetric] ec], symmetric]
[PROOF STATE]
proof (chain)
picking this:
toSet (snd x) = agent_abs a t
agent_abs a t = toSet (snd y)
[PROOF STEP]
have "snd x = snd y"
[PROOF STATE]
proof (prove)
using this:
toSet (snd x) = agent_abs a t
agent_abs a t = toSet (snd y)

goal (1 subgoal):
 1. snd x = snd y
[PROOF STEP]
by (blast intro: injD[OF toSet_inj])
[PROOF STATE]
proof (state)
this:
snd x = snd y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)); y \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)); clock_simAbs x = clock_simAbs y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fst x = fst y
snd x = snd y
[PROOF STEP]
show "x = y"
[PROOF STATE]
proof (prove)
using this:
fst x = fst y
snd x = snd y

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (simp add: prod_eqI)
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma clock_repMC_kripke[intro, simp]: "kripke (clock_repMC X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kripke (clock_repMC X)
[PROOF STEP]
by (rule kripkeI) simp


[STATEMENT]
lemma clock_repMC_S5n[intro, simp]: "S5n (clock_repMC X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S5n (clock_repMC X)
[PROOF STEP]
unfolding clock_repRels_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S5n (mkKripke X (\<lambda>a. rel_ext (\<lambda>(s, s'). envObs a s = envObs a s')) envVal)
[PROOF STEP]
by (intro S5nI equivI refl_onI symI transI) auto


[STATEMENT]
lemma jkbpCSt_jkbpCS_subset:
  "clock_jkbpCSt t \<subseteq> clock_sim ` Clock.jkbpC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clock_jkbpCSt t \<subseteq> Clock.jkbpCS
[PROOF STEP]
by auto


[STATEMENT]
lemma jkbpCSt_refl[iff]:
  "t \<in> Clock.jkbpC \<Longrightarrow> clock_sim t \<in> clock_jkbpCSt t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> Clock.jkbpC \<Longrightarrow> clock_sim t \<in> clock_jkbpCSt t
[PROOF STEP]
by blast


[STATEMENT]
lemma fst_clock_sim[iff]:
  "t \<in> Clock.jkbpC \<Longrightarrow> fst (clock_sim t) = tLast ` Clock.jkbpCn (tLength t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> Clock.jkbpC \<Longrightarrow> fst (clock_sim t) = clock_commonAbs t
[PROOF STEP]
by (simp add: clock_sim_def)


[STATEMENT]
lemma clock_repSim_simps[simp]:
  "clock_repSim ` clock_sim ` T = tLast ` T"
  "clock_repSim (clock_sim t) = tLast t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clock_repSim ` clock_sim ` T = tLast ` T &&& clock_repSim (clock_sim t) = tLast t
[PROOF STEP]
unfolding clock_repSim_def clock_sim_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ` (\<lambda>t. (clock_commonAbs t, tLast t)) ` T = tLast ` T &&& snd (clock_commonAbs t, tLast t) = tLast t
[PROOF STEP]
by (auto intro!: image_eqI)


[STATEMENT]
lemma clock_repSim:
  assumes tC: "t \<in> Clock.jkbpC"
  shows "sim (clock_simMCt t)
             ((clock_repMC \<circ> fst) (clock_sim t))
             clock_repSim"
(*<*) (is "sim ?M ?M' ?f")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. sim_range (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
 2. sim_val (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
 3. sim_f (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
 4. sim_r (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
[PROOF STEP]
show "sim_range ?M ?M' ?f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_range (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. worlds ((clock_repMC \<circ> fst) (clock_sim t)) = clock_repSim ` worlds (clock_simMCt t)
 2. \<And>a. relations ((clock_repMC \<circ> fst) (clock_sim t)) a \<subseteq> worlds ((clock_repMC \<circ> fst) (clock_sim t)) \<times> worlds ((clock_repMC \<circ> fst) (clock_sim t))
[PROOF STEP]
show "worlds ?M' = ?f ` worlds ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. worlds ((clock_repMC \<circ> fst) (clock_sim t)) = clock_repSim ` worlds (clock_simMCt t)
[PROOF STEP]
unfolding clock_sim_def clock_repSim_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. worlds ((clock_repMC \<circ> fst) (clock_commonAbs t, tLast t)) = snd ` worlds (mkKripke ((\<lambda>t. (clock_commonAbs t, tLast t)) ` Clock.jkbpCn (tLength t)) clock_simRels clock_simVal)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
worlds ((clock_repMC \<circ> fst) (clock_sim t)) = clock_repSim ` worlds (clock_simMCt t)

goal (1 subgoal):
 1. \<And>a. relations ((clock_repMC \<circ> fst) (clock_sim t)) a \<subseteq> worlds ((clock_repMC \<circ> fst) (clock_sim t)) \<times> worlds ((clock_repMC \<circ> fst) (clock_sim t))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. relations ((clock_repMC \<circ> fst) (clock_sim t)) a \<subseteq> worlds ((clock_repMC \<circ> fst) (clock_sim t)) \<times> worlds ((clock_repMC \<circ> fst) (clock_sim t))
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. relations ((clock_repMC \<circ> fst) (clock_sim t)) a \<subseteq> worlds ((clock_repMC \<circ> fst) (clock_sim t)) \<times> worlds ((clock_repMC \<circ> fst) (clock_sim t))
[PROOF STEP]
show "relations ?M' a \<subseteq> worlds ?M' \<times> worlds ?M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. relations ((clock_repMC \<circ> fst) (clock_sim t)) a \<subseteq> worlds ((clock_repMC \<circ> fst) (clock_sim t)) \<times> worlds ((clock_repMC \<circ> fst) (clock_sim t))
[PROOF STEP]
by (simp add: clock_sim_def clock_repSim_def)
[PROOF STATE]
proof (state)
this:
relations ((clock_repMC \<circ> fst) (clock_sim t)) a \<subseteq> worlds ((clock_repMC \<circ> fst) (clock_sim t)) \<times> worlds ((clock_repMC \<circ> fst) (clock_sim t))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sim_range (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim

goal (3 subgoals):
 1. sim_val (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
 2. sim_f (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
 3. sim_r (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sim_val (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
 2. sim_f (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
 3. sim_r (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
[PROOF STEP]
show "sim_val ?M ?M' ?f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_val (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
[PROOF STEP]
by (rule, simp add: clock_sim_def clock_simVal_def clock_repSim_def split: prod.split)
[PROOF STATE]
proof (state)
this:
sim_val (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim

goal (2 subgoals):
 1. sim_f (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
 2. sim_r (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sim_f (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
 2. sim_r (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
[PROOF STEP]
show "sim_f ?M ?M' ?f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_f (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a u v. (u, v) \<in> relations (clock_simMCt t) a \<Longrightarrow> (clock_repSim u, clock_repSim v) \<in> relations ((clock_repMC \<circ> fst) (clock_sim t)) a
[PROOF STEP]
unfolding clock_repRels_def clock_repSim_def clock_simRels_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a u v. (u, v) \<in> relations (mkKripke (clock_jkbpCSt t) (\<lambda>a. rel_ext (\<lambda>uu_. \<exists>X X' s s'. uu_ = ((X, s), X', s') \<and> X = X' \<and> {s, s'} \<subseteq> X \<and> envObs a s = envObs a s')) clock_simVal) a \<Longrightarrow> (snd u, snd v) \<in> relations (((\<lambda>X. mkKripke X (\<lambda>a. rel_ext (\<lambda>(s, s'). envObs a s = envObs a s')) envVal) \<circ> fst) (clock_sim t)) a
[PROOF STEP]
apply (auto iff: clock_sim_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
sim_f (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim

goal (1 subgoal):
 1. sim_r (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sim_r (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
[PROOF STEP]
show "sim_r ?M ?M' ?f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_r (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a u v'. \<lbrakk>u \<in> worlds (clock_simMCt t); (clock_repSim u, v') \<in> relations ((clock_repMC \<circ> fst) (clock_sim t)) a\<rbrakk> \<Longrightarrow> \<exists>v. (u, v) \<in> relations (clock_simMCt t) a \<and> clock_repSim v = v'
[PROOF STEP]
unfolding clock_repRels_def clock_repSim_def clock_simRels_def clock_sim_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a u v'. \<lbrakk>u \<in> worlds (mkKripke ((\<lambda>t. (clock_commonAbs t, tLast t)) ` Clock.jkbpCn (tLength t)) (\<lambda>a. rel_ext (\<lambda>uu_. \<exists>X X' s s'. uu_ = ((X, s), X', s') \<and> X = X' \<and> {s, s'} \<subseteq> X \<and> envObs a s = envObs a s')) clock_simVal); (snd u, v') \<in> relations (((\<lambda>X. mkKripke X (\<lambda>a. rel_ext (\<lambda>(s, s'). envObs a s = envObs a s')) envVal) \<circ> fst) (clock_commonAbs t, tLast t)) a\<rbrakk> \<Longrightarrow> \<exists>v. (u, v) \<in> relations (mkKripke ((\<lambda>t. (clock_commonAbs t, tLast t)) ` Clock.jkbpCn (tLength t)) (\<lambda>a. rel_ext (\<lambda>uu_. \<exists>X X' s s'. uu_ = ((X, s), X', s') \<and> X = X' \<and> {s, s'} \<subseteq> X \<and> envObs a s = envObs a s')) clock_simVal) a \<and> snd v = v'
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
sim_r (clock_simMCt t) ((clock_repMC \<circ> fst) (clock_sim t)) clock_repSim

goal:
No subgoals!
[PROOF STEP]
qed