[STATEMENT]
lemma c_out_cf'_eq': "valid_tree t \<Longrightarrow> c_out cf' sf t = c_out cf sf t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_tree t \<Longrightarrow> c_out cf' sf t = c_out cf sf t
[PROOF STEP]
by (simp add: c_out_cf'_eq matching_rels_def valid_tree_def)


[STATEMENT]
lemma joinTree_card'_pos[intro]: "pos_rel_cards cf' t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pos_rel_cards cf' t
[PROOF STEP]
by (induction t) (auto simp: pos_cards' pos_rel_cards_def)


[STATEMENT]
lemma match_reasonable_cards'[intro]: "reasonable_cards cf' match_sel t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reasonable_cards cf' match_sel t
[PROOF STEP]
using pos_sel_reason_impl_reason
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>pos_rel_cards ?cf ?t; sel_reasonable ?sel\<rbrakk> \<Longrightarrow> reasonable_cards ?cf ?sel ?t

goal (1 subgoal):
 1. reasonable_cards cf' match_sel t
[PROOF STEP]
by blast


[STATEMENT]
lemma sel_r_gt0: "r \<in> verts G \<Longrightarrow> sel_r r x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> verts G \<Longrightarrow> 0 < sel_r r x
[PROOF STEP]
using directed_tree.contr_sel_gt0[OF directed_tree_r]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?root \<in> verts G; sel_reasonable ?sf\<rbrakk> \<Longrightarrow> 0 < directed_tree.contr_sel (dir_tree_r ?root) ?sf ?x

goal (1 subgoal):
 1. r \<in> verts G \<Longrightarrow> 0 < sel_r r x
[PROOF STEP]
by blast


[STATEMENT]
lemma sel_r_le1: "r \<in> verts G \<Longrightarrow> sel_r r x \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> verts G \<Longrightarrow> sel_r r x \<le> 1
[PROOF STEP]
using directed_tree.contr_sel_le1[OF directed_tree_r]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?root \<in> verts G; sel_reasonable ?sf\<rbrakk> \<Longrightarrow> directed_tree.contr_sel (dir_tree_r ?root) ?sf ?x \<le> 1

goal (1 subgoal):
 1. r \<in> verts G \<Longrightarrow> sel_r r x \<le> 1
[PROOF STEP]
by blast


[STATEMENT]
lemma sel_r_eq_ldeep_s_if_dst_fwd_verts:
  "\<lbrakk>r \<in> verts G; distinct xs; directed_tree.forward (dir_tree_r r) xs; set xs = verts G\<rbrakk>
    \<Longrightarrow> sel_r r = ldeep_s match_sel (rev xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> verts G; distinct xs; directed_tree.forward (dir_tree_r r) xs; set xs = verts G\<rbrakk> \<Longrightarrow> sel_r r = ldeep_s match_sel (rev xs)
[PROOF STEP]
using directed_tree.contr_sel_eq_ldeep_s_if_tree_dst_fwd_verts'[OF directed_tree_r]
    verts_dir_tree_r_eq
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?root \<in> verts G; directed_tree.tree_sel (dir_tree_r ?root) ?sel; distinct ?xs; directed_tree.forward (dir_tree_r ?root) ?xs; set ?xs = verts (dir_tree_r ?root)\<rbrakk> \<Longrightarrow> directed_tree.contr_sel (dir_tree_r ?root) ?sel = ldeep_s ?sel (rev ?xs)
?r \<in> verts G \<Longrightarrow> verts (dir_tree_r ?r) = verts G

goal (1 subgoal):
 1. \<lbrakk>r \<in> verts G; distinct xs; directed_tree.forward (dir_tree_r r) xs; set xs = verts G\<rbrakk> \<Longrightarrow> sel_r r = ldeep_s match_sel (rev xs)
[PROOF STEP]
by blast


[STATEMENT]
lemma sel_r_eq_ldeep_s_if_valid_fwd:
  "\<lbrakk>r \<in> verts G; valid_tree t; directed_tree.forward (dir_tree_r r) (inorder t)\<rbrakk>
    \<Longrightarrow> sel_r r = ldeep_s match_sel (revorder t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> verts G; valid_tree t; directed_tree.forward (dir_tree_r r) (inorder t)\<rbrakk> \<Longrightarrow> sel_r r = ldeep_s match_sel (revorder t)
[PROOF STEP]
unfolding valid_tree_def distinct_relations_def inorder_eq_set[symmetric] revorder_eq_rev_inorder
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> verts G; set (inorder t) = verts G \<and> distinct (inorder t); directed_tree.forward (dir_tree_r r) (inorder t)\<rbrakk> \<Longrightarrow> sel_r r = ldeep_s match_sel (rev (inorder t))
[PROOF STEP]
using sel_r_eq_ldeep_s_if_dst_fwd_verts
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?r \<in> verts G; distinct ?xs; directed_tree.forward (dir_tree_r ?r) ?xs; set ?xs = verts G\<rbrakk> \<Longrightarrow> sel_r ?r = ldeep_s match_sel (rev ?xs)

goal (1 subgoal):
 1. \<lbrakk>r \<in> verts G; set (inorder t) = verts G \<and> distinct (inorder t); directed_tree.forward (dir_tree_r r) (inorder t)\<rbrakk> \<Longrightarrow> sel_r r = ldeep_s match_sel (rev (inorder t))
[PROOF STEP]
by blast


[STATEMENT]
lemma sel_r_eq_ldeep_s_if_valid_no_cross:
  "\<lbrakk>valid_tree t; no_cross_products t; left_deep t\<rbrakk>
    \<Longrightarrow> sel_r (first_node t) = ldeep_s match_sel (revorder t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_tree t; no_cross_products t; left_deep t\<rbrakk> \<Longrightarrow> sel_r (first_node t) = ldeep_s match_sel (revorder t)
[PROOF STEP]
using sel_r_eq_ldeep_s_if_valid_fwd forward_if_ldeep_no_cross'
    valid_tree_def first_node_in_verts_if_valid
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?r \<in> verts G; valid_tree ?t; directed_tree.forward (dir_tree_r ?r) (inorder ?t)\<rbrakk> \<Longrightarrow> sel_r ?r = ldeep_s match_sel (revorder ?t)
\<lbrakk>first_node ?t \<in> verts G; distinct_relations ?t; left_deep ?t; no_cross_products ?t\<rbrakk> \<Longrightarrow> directed_tree.forward (dir_tree_r (first_node ?t)) (inorder ?t)
valid_tree ?t = (relations ?t = verts G \<and> distinct_relations ?t)
valid_tree ?t \<Longrightarrow> first_node ?t \<in> verts G

goal (1 subgoal):
 1. \<lbrakk>valid_tree t; no_cross_products t; left_deep t\<rbrakk> \<Longrightarrow> sel_r (first_node t) = ldeep_s match_sel (revorder t)
[PROOF STEP]
by blast


[STATEMENT]
lemma c_list_ldeep_s_eq_c_list_r_if_valid_no_cross:
  "\<lbrakk>valid_tree t; no_cross_products t; left_deep t\<rbrakk>
    \<Longrightarrow> c_list (ldeep_s match_sel (revorder t)) cf' h (first_node t) xs
      = c_list_r h (first_node t) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_tree t; no_cross_products t; left_deep t\<rbrakk> \<Longrightarrow> c_list (ldeep_s match_sel (revorder t)) cf' h (first_node t) xs = c_list_r h (first_node t) xs
[PROOF STEP]
using sel_r_eq_ldeep_s_if_valid_no_cross c_list_r_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>valid_tree ?t; no_cross_products ?t; left_deep ?t\<rbrakk> \<Longrightarrow> sel_r (first_node ?t) = ldeep_s match_sel (revorder ?t)
c_list_r ?h ?r = c_list (sel_r ?r) cf' ?h ?r

goal (1 subgoal):
 1. \<lbrakk>valid_tree t; no_cross_products t; left_deep t\<rbrakk> \<Longrightarrow> c_list (ldeep_s match_sel (revorder t)) cf' h (first_node t) xs = c_list_r h (first_node t) xs
[PROOF STEP]
by simp


[STATEMENT]
lemma c_IKKBZ_list_correct_if_simple_h:
  assumes "valid_tree t" and "no_cross_products t" and "left_deep t"
  shows "c_list_r (\<lambda>x. h x (cf' x)) (first_node t) (revorder t) = c_IKKBZ h cf match_sel t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_list_r (\<lambda>x. h x (cf' x)) (first_node t) (revorder t) = c_IKKBZ h cf match_sel t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c_list_r (\<lambda>x. h x (cf' x)) (first_node t) (revorder t) = c_IKKBZ h cf match_sel t
[PROOF STEP]
have "(\<lambda>t. c_IKKBZ h cf' match_sel t) t
      = c_list (ldeep_s match_sel (revorder t)) cf' (\<lambda>x. h x (cf' x)) (first_node t) (revorder t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_IKKBZ h cf' match_sel t = c_list (ldeep_s match_sel (revorder t)) cf' (\<lambda>x. h x (cf' x)) (first_node t) (revorder t)
[PROOF STEP]
using c_IKKBZ_eq_c_list assms(1,3) valid_tree_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct_relations ?t; reasonable_cards ?cf ?f ?t; left_deep ?t; \<forall>x\<in>relations ?t. ?h1.0 x (?cf x) = ?h2.0 x\<rbrakk> \<Longrightarrow> c_IKKBZ ?h1.0 ?cf ?f ?t = c_list (ldeep_s ?f (revorder ?t)) ?cf ?h2.0 (first_node ?t) (revorder ?t)
valid_tree t
left_deep t
valid_tree ?t = (relations ?t = verts G \<and> distinct_relations ?t)

goal (1 subgoal):
 1. c_IKKBZ h cf' match_sel t = c_list (ldeep_s match_sel (revorder t)) cf' (\<lambda>x. h x (cf' x)) (first_node t) (revorder t)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
c_IKKBZ h cf' match_sel t = c_list (ldeep_s match_sel (revorder t)) cf' (\<lambda>x. h x (cf' x)) (first_node t) (revorder t)

goal (1 subgoal):
 1. c_list_r (\<lambda>x. h x (cf' x)) (first_node t) (revorder t) = c_IKKBZ h cf match_sel t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c_IKKBZ h cf' match_sel t = c_list (ldeep_s match_sel (revorder t)) cf' (\<lambda>x. h x (cf' x)) (first_node t) (revorder t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c_IKKBZ h cf' match_sel t = c_list (ldeep_s match_sel (revorder t)) cf' (\<lambda>x. h x (cf' x)) (first_node t) (revorder t)

goal (1 subgoal):
 1. c_list_r (\<lambda>x. h x (cf' x)) (first_node t) (revorder t) = c_IKKBZ h cf match_sel t
[PROOF STEP]
using c_list_ldeep_s_eq_c_list_r_if_valid_no_cross assms
[PROOF STATE]
proof (prove)
using this:
c_IKKBZ h cf' match_sel t = c_list (ldeep_s match_sel (revorder t)) cf' (\<lambda>x. h x (cf' x)) (first_node t) (revorder t)
\<lbrakk>valid_tree ?t; no_cross_products ?t; left_deep ?t\<rbrakk> \<Longrightarrow> c_list (ldeep_s match_sel (revorder ?t)) cf' ?h (first_node ?t) ?xs = c_list_r ?h (first_node ?t) ?xs
valid_tree t
no_cross_products t
left_deep t

goal (1 subgoal):
 1. c_list_r (\<lambda>x. h x (cf' x)) (first_node t) (revorder t) = c_IKKBZ h cf match_sel t
[PROOF STEP]
by (simp add: c_IKKBZ_cf'_eq')
[PROOF STATE]
proof (state)
this:
c_list_r (\<lambda>x. h x (cf' x)) (first_node t) (revorder t) = c_IKKBZ h cf match_sel t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ikkbz_query_graph_if_simple_h:
  defines "cost \<equiv> c_IKKBZ h cf match_sel"
  defines "h' \<equiv> (\<lambda>x. h x (cf' x))"
  shows "ikkbz_query_graph bfs sel cf G cmp cost (c_list_r h') (rank_r h')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ikkbz_query_graph bfs sel cf G cmp cost (c_list_r h') (rank_r h')
[PROOF STEP]
unfolding ikkbz_query_graph_def ikkbz_query_graph_axioms_def assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmp_tree_query_graph bfs sel cf G cmp \<and> (\<forall>r. r \<in> verts G \<longrightarrow> asi (rank_r (\<lambda>x. h x (cf' x)) r) r (c_list_r (\<lambda>x. h x (cf' x)) r)) \<and> (\<forall>t. valid_tree t \<longrightarrow> no_cross_products t \<longrightarrow> left_deep t \<longrightarrow> c_list_r (\<lambda>x. h x (cf' x)) (first_node t) (revorder t) = c_IKKBZ h cf match_sel t)
[PROOF STEP]
by (auto simp: cmp_tree_query_graph_axioms c_list_asi c_IKKBZ_list_correct_if_simple_h h_pos)


[STATEMENT]
theorem ikkbz_simple_h_optimal:
  "\<lbrakk>valid_tree t; no_cross_products t; left_deep t\<rbrakk>
    \<Longrightarrow> c_IKKBZ h cf match_sel (create_ldeep ikkbz) \<le> c_IKKBZ h cf match_sel t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_tree t; no_cross_products t; left_deep t\<rbrakk> \<Longrightarrow> cost_l ikkbz \<le> c_IKKBZ h cf match_sel t
[PROOF STEP]
by (rule ikkbz_optimal_tree)


[STATEMENT]
lemma id_cf'_gt0: "\<forall>x. id (cf' x) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. 0 < id (cf' x)
[PROOF STEP]
by auto


[STATEMENT]
lemma c_out_eq_c_list_cf':
  fixes t
  defines "xs \<equiv> revorder t"
  defines "h \<equiv> (\<lambda>a. ldeep_s match_sel xs a * cf' a)"
  assumes "distinct_relations t" and "left_deep t"
  shows "c_list (ldeep_s match_sel xs) cf' h (first_node t) xs = c_out cf' match_sel t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_list (ldeep_s match_sel xs) cf' h (first_node t) xs = c_out cf' match_sel t
[PROOF STEP]
using c_out_eq_c_list assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct_relations ?t; reasonable_cards ?cf ?f ?t; left_deep ?t\<rbrakk> \<Longrightarrow> c_list (ldeep_s ?f (revorder ?t)) ?cf (\<lambda>a. ldeep_s ?f (revorder ?t) a * ?cf a) (first_node ?t) (revorder ?t) = c_out ?cf ?f ?t
xs \<equiv> revorder t
h \<equiv> \<lambda>a. ldeep_s match_sel xs a * cf' a
distinct_relations t
left_deep t

goal (1 subgoal):
 1. c_list (ldeep_s match_sel xs) cf' h (first_node t) xs = c_out cf' match_sel t
[PROOF STEP]
by blast


[STATEMENT]
lemma c_out_list_correct_cf':
  fixes t
  defines "h \<equiv> (\<lambda>a. sel_r (first_node t) a * cf' a)"
  assumes "valid_tree t" and "no_cross_products t" and "left_deep t"
  shows "c_list_r h (first_node t) (revorder t) = c_out cf' match_sel t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_list_r h (first_node t) (revorder t) = c_out cf' match_sel t
[PROOF STEP]
using c_out_eq_c_list_cf' assms sel_r_eq_ldeep_s_if_valid_no_cross
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct_relations ?t; left_deep ?t\<rbrakk> \<Longrightarrow> c_list (ldeep_s match_sel (revorder ?t)) cf' (\<lambda>a. ldeep_s match_sel (revorder ?t) a * cf' a) (first_node ?t) (revorder ?t) = c_out cf' match_sel ?t
h \<equiv> \<lambda>a. sel_r (first_node t) a * cf' a
valid_tree t
no_cross_products t
left_deep t
\<lbrakk>valid_tree ?t; no_cross_products ?t; left_deep ?t\<rbrakk> \<Longrightarrow> sel_r (first_node ?t) = ldeep_s match_sel (revorder ?t)

goal (1 subgoal):
 1. c_list_r h (first_node t) (revorder t) = c_out cf' match_sel t
[PROOF STEP]
by (fastforce simp: valid_tree_def c_list_ldeep_s_eq_c_list_r_if_valid_no_cross)


[STATEMENT]
lemma c_out_list_correct_cf:
  fixes t
  defines "h \<equiv> (\<lambda>a. sel_r (first_node t) a * cf' a)"
  assumes "valid_tree t" and "no_cross_products t" and "left_deep t"
  shows "c_list_r h (first_node t) (revorder t) = c_out cf match_sel t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_list_r h (first_node t) (revorder t) = c_out cf match_sel t
[PROOF STEP]
using c_out_list_correct_cf' c_out_cf'_eq' assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>valid_tree ?t; no_cross_products ?t; left_deep ?t\<rbrakk> \<Longrightarrow> c_list_r (\<lambda>a. sel_r (first_node ?t) a * cf' a) (first_node ?t) (revorder ?t) = c_out cf' match_sel ?t
valid_tree ?t \<Longrightarrow> c_out cf' ?sf ?t = c_out cf ?sf ?t
h \<equiv> \<lambda>a. sel_r (first_node t) a * cf' a
valid_tree t
no_cross_products t
left_deep t

goal (1 subgoal):
 1. c_list_r h (first_node t) (revorder t) = c_out cf match_sel t
[PROOF STEP]
by simp


[STATEMENT]
lemma c_out_list_correct:
  "\<lbrakk>valid_tree t; no_cross_products t; left_deep t\<rbrakk>
    \<Longrightarrow> c_out_list_r (first_node t) (revorder t) = c_out cf match_sel t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_tree t; no_cross_products t; left_deep t\<rbrakk> \<Longrightarrow> c_out_list_r (first_node t) (revorder t) = c_out cf match_sel t
[PROOF STEP]
using c_out_list_correct_cf c_out_list_r_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>valid_tree ?t; no_cross_products ?t; left_deep ?t\<rbrakk> \<Longrightarrow> c_list_r (\<lambda>a. sel_r (first_node ?t) a * cf' a) (first_node ?t) (revorder ?t) = c_out cf match_sel ?t
c_out_list_r ?r = c_list_r (\<lambda>a. sel_r ?r a * cf' a) ?r

goal (1 subgoal):
 1. \<lbrakk>valid_tree t; no_cross_products t; left_deep t\<rbrakk> \<Longrightarrow> c_out_list_r (first_node t) (revorder t) = c_out cf match_sel t
[PROOF STEP]
by simp


[STATEMENT]
lemma c_out_h_gt0: "r \<in> verts G \<Longrightarrow> (\<lambda>a. sel_r r a * cf' a) x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> verts G \<Longrightarrow> 0 < sel_r r x * cf' x
[PROOF STEP]
using sel_r_gt0
[PROOF STATE]
proof (prove)
using this:
?r \<in> verts G \<Longrightarrow> 0 < sel_r ?r ?x

goal (1 subgoal):
 1. r \<in> verts G \<Longrightarrow> 0 < sel_r r x * cf' x
[PROOF STEP]
by (simp add: pos_cards')


[STATEMENT]
lemma c_out_r_asi: "r \<in> verts G \<Longrightarrow> asi (c_out_rank_r r) r (c_out_list_r r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> verts G \<Longrightarrow> asi (c_out_rank_r r) r (c_out_list_r r)
[PROOF STEP]
using c_out_h_gt0
[PROOF STATE]
proof (prove)
using this:
?r \<in> verts G \<Longrightarrow> 0 < sel_r ?r ?x * cf' ?x

goal (1 subgoal):
 1. r \<in> verts G \<Longrightarrow> asi (c_out_rank_r r) r (c_out_list_r r)
[PROOF STEP]
by (simp add: c_list_asi c_out_list_r_def c_out_rank_r_def)


[STATEMENT]
theorem ikkbz_query_graph_c_out:
  "ikkbz_query_graph bfs sel cf G cmp (c_out cf match_sel) c_out_list_r c_out_rank_r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ikkbz_query_graph bfs sel cf G cmp (c_out cf match_sel) c_out_list_r c_out_rank_r
[PROOF STEP]
unfolding ikkbz_query_graph_def ikkbz_query_graph_axioms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmp_tree_query_graph bfs sel cf G cmp \<and> (\<forall>r. r \<in> verts G \<longrightarrow> asi (c_out_rank_r r) r (c_out_list_r r)) \<and> (\<forall>t. valid_tree t \<longrightarrow> no_cross_products t \<longrightarrow> left_deep t \<longrightarrow> c_out_list_r (first_node t) (revorder t) = c_out cf match_sel t)
[PROOF STEP]
by (auto simp: cmp_tree_query_graph_axioms c_out_r_asi c_out_list_correct)


[STATEMENT]
lemma cmp_hd_eq_if_equiv: "compare cmp (v1,e1) (v2,e2) = Equiv \<Longrightarrow> hd v1 = hd v2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compare cmp (v1, e1) (v2, e2) = Equiv \<Longrightarrow> hd v1 = hd v2
[PROOF STEP]
by(auto simp: cmp.rep_eq split: if_splits)


[STATEMENT]
lemma cmp_sets_not_dsjnt_if_equiv:
  "\<lbrakk>v1 \<noteq> []; v2 \<noteq> []; compare cmp (v1,e1) (v2,e2) = Equiv\<rbrakk> \<Longrightarrow> set v1 \<inter> set v2 \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v1 \<noteq> []; v2 \<noteq> []; compare cmp (v1, e1) (v2, e2) = Equiv\<rbrakk> \<Longrightarrow> set v1 \<inter> set v2 \<noteq> {}
[PROOF STEP]
using cmp_hd_eq_if_equiv disjoint_iff_not_equal hd_in_set[of v1]
[PROOF STATE]
proof (prove)
using this:
compare cmp (?v1.0, ?e1.0) (?v2.0, ?e2.0) = Equiv \<Longrightarrow> hd ?v1.0 = hd ?v2.0
(?A \<inter> ?B = {}) = (\<forall>x\<in>?A. \<forall>y\<in>?B. x \<noteq> y)
v1 \<noteq> [] \<Longrightarrow> hd v1 \<in> set v1

goal (1 subgoal):
 1. \<lbrakk>v1 \<noteq> []; v2 \<noteq> []; compare cmp (v1, e1) (v2, e2) = Equiv\<rbrakk> \<Longrightarrow> set v1 \<inter> set v2 \<noteq> {}
[PROOF STEP]
by auto


[STATEMENT]
lemma cmp_tree_qg: "cmp_tree_query_graph bfs sel cf G cmp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmp_tree_query_graph bfs sel cf G cmp
[PROOF STEP]
by standard (simp add: cmp_sets_not_dsjnt_if_equiv)


[STATEMENT]
lemma cmp_arcs_eq_if_equiv: "compare cmp (v1,e1) (v2,e2) = Equiv \<Longrightarrow> e1 = e2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compare cmp (v1, e1) (v2, e2) = Equiv \<Longrightarrow> e1 = e2
[PROOF STEP]
by(auto simp: cmp.rep_eq split: if_splits)


[STATEMENT]
lemma cmp_tree_qg: "cmp_tree_query_graph bfs sel cf G cmp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmp_tree_query_graph bfs sel cf G cmp
[PROOF STEP]
by standard (simp add: cmp_arcs_eq_if_equiv)


[STATEMENT]
lemma cnj_0[simp]: "cnj 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (0::'a) = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cnj_class.cnj (0::'a) = (0::'a)
[PROOF STEP]
have "cnj 0 = cnj (0 + 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (0::'a) = cnj_class.cnj ((0::'a) + (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (0::'a) = cnj_class.cnj ((0::'a) + (0::'a))

goal (1 subgoal):
 1. cnj_class.cnj (0::'a) = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (0::'a) = cnj_class.cnj ((0::'a) + (0::'a))

goal (1 subgoal):
 1. cnj_class.cnj (0::'a) = (0::'a)
[PROOF STEP]
have "... = cnj 0 + cnj 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj ((0::'a) + (0::'a)) = cnj_class.cnj (0::'a) + cnj_class.cnj (0::'a)
[PROOF STEP]
unfolding cnj_add
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (0::'a) + cnj_class.cnj (0::'a) = cnj_class.cnj (0::'a) + cnj_class.cnj (0::'a)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
cnj_class.cnj ((0::'a) + (0::'a)) = cnj_class.cnj (0::'a) + cnj_class.cnj (0::'a)

goal (1 subgoal):
 1. cnj_class.cnj (0::'a) = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cnj_class.cnj ((0::'a) + (0::'a)) = cnj_class.cnj (0::'a) + cnj_class.cnj (0::'a)

goal (1 subgoal):
 1. cnj_class.cnj (0::'a) = (0::'a)
[PROOF STEP]
have "... = 2 * (cnj 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (0::'a) + cnj_class.cnj (0::'a) = (2::'a) * cnj_class.cnj (0::'a)
[PROOF STEP]
by (simp add: local.mult_2)
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (0::'a) + cnj_class.cnj (0::'a) = (2::'a) * cnj_class.cnj (0::'a)

goal (1 subgoal):
 1. cnj_class.cnj (0::'a) = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cnj_class.cnj (0::'a) = (2::'a) * cnj_class.cnj (0::'a)
[PROOF STEP]
have "cnj 0 = 2 * cnj 0"
[PROOF STATE]
proof (prove)
using this:
cnj_class.cnj (0::'a) = (2::'a) * cnj_class.cnj (0::'a)

goal (1 subgoal):
 1. cnj_class.cnj (0::'a) = (2::'a) * cnj_class.cnj (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (0::'a) = (2::'a) * cnj_class.cnj (0::'a)

goal (1 subgoal):
 1. cnj_class.cnj (0::'a) = (0::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cnj_class.cnj (0::'a) = (2::'a) * cnj_class.cnj (0::'a)

goal (1 subgoal):
 1. cnj_class.cnj (0::'a) = (0::'a)
[PROOF STEP]
by (auto simp add: two_not_one)
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (0::'a) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cnj_0_eq[simp]: "(cnj a = 0) = (a = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cnj_class.cnj a = (0::'a)) = (a = (0::'a))
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (0::'a) = cnj_class.cnj a \<Longrightarrow> a = cnj_class.cnj a
[PROOF STEP]
assume cnj_rw: "0 = cnj a"
[PROOF STATE]
proof (state)
this:
(0::'a) = cnj_class.cnj a

goal (1 subgoal):
 1. (0::'a) = cnj_class.cnj a \<Longrightarrow> a = cnj_class.cnj a
[PROOF STEP]
have "cnj (cnj a) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (cnj_class.cnj a) = a
[PROOF STEP]
using cnj_idem
[PROOF STATE]
proof (prove)
using this:
cnj_class.cnj (cnj_class.cnj ?a) = ?a

goal (1 subgoal):
 1. cnj_class.cnj (cnj_class.cnj a) = a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (cnj_class.cnj a) = a

goal (1 subgoal):
 1. (0::'a) = cnj_class.cnj a \<Longrightarrow> a = cnj_class.cnj a
[PROOF STEP]
hence "cnj 0 = a"
[PROOF STATE]
proof (prove)
using this:
cnj_class.cnj (cnj_class.cnj a) = a

goal (1 subgoal):
 1. cnj_class.cnj (0::'a) = a
[PROOF STEP]
unfolding cnj_rw
[PROOF STATE]
proof (prove)
using this:
cnj_class.cnj (cnj_class.cnj a) = a

goal (1 subgoal):
 1. cnj_class.cnj (cnj_class.cnj a) = a
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (0::'a) = a

goal (1 subgoal):
 1. (0::'a) = cnj_class.cnj a \<Longrightarrow> a = cnj_class.cnj a
[PROOF STEP]
hence "a = 0"
[PROOF STATE]
proof (prove)
using this:
cnj_class.cnj (0::'a) = a

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

goal (1 subgoal):
 1. (0::'a) = cnj_class.cnj a \<Longrightarrow> a = cnj_class.cnj a
[PROOF STEP]
thus "a = cnj a"
[PROOF STATE]
proof (prove)
using this:
a = (0::'a)

goal (1 subgoal):
 1. a = cnj_class.cnj a
[PROOF STEP]
using cnj_rw
[PROOF STATE]
proof (prove)
using this:
a = (0::'a)
(0::'a) = cnj_class.cnj a

goal (1 subgoal):
 1. a = cnj_class.cnj a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a = cnj_class.cnj a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma a_cnj_a_0: "(a*cnj a = 0) = (a = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a * cnj_class.cnj a = (0::'a)) = (a = (0::'a))
[PROOF STEP]
by simp


[STATEMENT]
lemma cnj_sum: "cnj (\<Sum>xa\<in>A. ((f xa))) = (\<Sum>xa\<in>A. cnj (f xa))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (sum f A) = (\<Sum>xa\<in>A. cnj_class.cnj (f xa))
[PROOF STEP]
by (cases "finite A", induct set: finite, auto simp add: cnj_add)


[STATEMENT]
lemma real_minus: "real_of (a - b) = real_of a - real_of b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (a - b) = real_of a - real_of b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of (a - b) = real_of a - real_of b
[PROOF STEP]
have "real_of (a - b) = real_of (a + - b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (a - b) = real_of (a + - b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real_of (a - b) = real_of (a + - b)

goal (1 subgoal):
 1. real_of (a - b) = real_of a - real_of b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of (a - b) = real_of (a + - b)

goal (1 subgoal):
 1. real_of (a - b) = real_of a - real_of b
[PROOF STEP]
have "... = real_of a + real_of (- b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (a + - b) = real_of a + real_of (- b)
[PROOF STEP]
unfolding real_add
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of a + real_of (- b) = real_of a + real_of (- b)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
real_of (a + - b) = real_of a + real_of (- b)

goal (1 subgoal):
 1. real_of (a - b) = real_of a - real_of b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of (a + - b) = real_of a + real_of (- b)

goal (1 subgoal):
 1. real_of (a - b) = real_of a - real_of b
[PROOF STEP]
have "... = real_of a + - real_of b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of a + real_of (- b) = real_of a + - real_of b
[PROOF STEP]
unfolding real_uminus
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of a + - real_of b = real_of a + - real_of b
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
real_of a + real_of (- b) = real_of a + - real_of b

goal (1 subgoal):
 1. real_of (a - b) = real_of a - real_of b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of a + real_of (- b) = real_of a + - real_of b

goal (1 subgoal):
 1. real_of (a - b) = real_of a - real_of b
[PROOF STEP]
have "... = real_of a - real_of b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of a + - real_of b = real_of a - real_of b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real_of a + - real_of b = real_of a - real_of b

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

goal (1 subgoal):
 1. real_of (a - b) = real_of a - real_of b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
real_of (a - b) = real_of a - real_of b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma real_0[simp]: "real_of 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (0::'a) = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of (0::'a) = 0
[PROOF STEP]
have "real_of 0 = real_of (0+0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (0::'a) = real_of ((0::'a) + (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of (0::'a) = real_of ((0::'a) + (0::'a))

goal (1 subgoal):
 1. real_of (0::'a) = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of (0::'a) = real_of ((0::'a) + (0::'a))

goal (1 subgoal):
 1. real_of (0::'a) = 0
[PROOF STEP]
have "... = real_of 0 + real_of 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of ((0::'a) + (0::'a)) = real_of (0::'a) + real_of (0::'a)
[PROOF STEP]
unfolding real_add
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (0::'a) + real_of (0::'a) = real_of (0::'a) + real_of (0::'a)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
real_of ((0::'a) + (0::'a)) = real_of (0::'a) + real_of (0::'a)

goal (1 subgoal):
 1. real_of (0::'a) = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of ((0::'a) + (0::'a)) = real_of (0::'a) + real_of (0::'a)

goal (1 subgoal):
 1. real_of (0::'a) = 0
[PROOF STEP]
have "... = 2*(real_of 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (0::'a) + real_of (0::'a) = 2 * real_of (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of (0::'a) + real_of (0::'a) = 2 * real_of (0::'a)

goal (1 subgoal):
 1. real_of (0::'a) = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real_of (0::'a) = 2 * real_of (0::'a)
[PROOF STEP]
have "real_of 0 = 2* real_of 0"
[PROOF STATE]
proof (prove)
using this:
real_of (0::'a) = 2 * real_of (0::'a)

goal (1 subgoal):
 1. real_of (0::'a) = 2 * real_of (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
real_of (0::'a) = 2 * real_of (0::'a)

goal (1 subgoal):
 1. real_of (0::'a) = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
real_of (0::'a) = 2 * real_of (0::'a)

goal (1 subgoal):
 1. real_of (0::'a) = 0
[PROOF STEP]
by (auto simp add: two_not_one)
[PROOF STATE]
proof (state)
this:
real_of (0::'a) = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma real_sum:
  "real_of (sum (\<lambda>i. f i) A) = sum (\<lambda>i. real_of (f i)) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (sum f A) = (\<Sum>i\<in>A. real_of (f i))
[PROOF STEP]
proof (cases "finite A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite A \<Longrightarrow> real_of (sum f A) = (\<Sum>i\<in>A. real_of (f i))
 2. infinite A \<Longrightarrow> real_of (sum f A) = (\<Sum>i\<in>A. real_of (f i))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
infinite A

goal (2 subgoals):
 1. finite A \<Longrightarrow> real_of (sum f A) = (\<Sum>i\<in>A. real_of (f i))
 2. infinite A \<Longrightarrow> real_of (sum f A) = (\<Sum>i\<in>A. real_of (f i))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
infinite A

goal (1 subgoal):
 1. real_of (sum f A) = (\<Sum>i\<in>A. real_of (f i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of (sum f A) = (\<Sum>i\<in>A. real_of (f i))

goal (1 subgoal):
 1. finite A \<Longrightarrow> real_of (sum f A) = (\<Sum>i\<in>A. real_of (f i))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite A \<Longrightarrow> real_of (sum f A) = (\<Sum>i\<in>A. real_of (f i))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
finite A

goal (1 subgoal):
 1. finite A \<Longrightarrow> real_of (sum f A) = (\<Sum>i\<in>A. real_of (f i))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. real_of (sum f A) = (\<Sum>i\<in>A. real_of (f i))
[PROOF STEP]
by (induct, auto simp add: real_add)
[PROOF STATE]
proof (state)
this:
real_of (sum f A) = (\<Sum>i\<in>A. real_of (f i))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inner_zero_left [simp]: "inner 0 x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner (0::'b) x = (0::'a)
[PROOF STEP]
using inner_add_left [of 0 0 x]
[PROOF STATE]
proof (prove)
using this:
inner ((0::'b) + (0::'b)) x = inner (0::'b) x + inner (0::'b) x

goal (1 subgoal):
 1. inner (0::'b) x = (0::'a)
[PROOF STEP]
by (auto simp add: two_not_one)


[STATEMENT]
lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner (- x) y = - inner x y
[PROOF STEP]
using inner_add_left [of x "- x" y]
[PROOF STATE]
proof (prove)
using this:
inner (x + - x) y = inner x y + inner (- x) y

goal (1 subgoal):
 1. inner (- x) y = - inner x y
[PROOF STEP]
using add_eq_0_iff
[PROOF STATE]
proof (prove)
using this:
inner (x + - x) y = inner x y + inner (- x) y
(?a + ?b = (0::?'a)) = (?b = - ?a)

goal (1 subgoal):
 1. inner (- x) y = - inner x y
[PROOF STEP]
by force


[STATEMENT]
lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner (x - y) z = inner x z - inner y z
[PROOF STEP]
using inner_add_left [of x "- y" z]
[PROOF STATE]
proof (prove)
using this:
inner (x + - y) z = inner x z + inner (- y) z

goal (1 subgoal):
 1. inner (x - y) z = inner x z - inner y z
[PROOF STEP]
by simp


[STATEMENT]
lemma inner_sum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner (sum f A) y = (\<Sum>x\<in>A. inner (f x) y)
[PROOF STEP]
by (cases "finite A", induct set: finite, simp_all add: inner_add_left)


[STATEMENT]
lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner x (y + z) = inner x y + inner x z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inner x (y + z) = inner x y + inner x z
[PROOF STEP]
have "inner x (y + z) = cnj (inner (y + z) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner x (y + z) = cnj_class.cnj (inner (y + z) x)
[PROOF STEP]
using inner_commute
[PROOF STATE]
proof (prove)
using this:
inner ?x ?y = cnj_class.cnj (inner ?y ?x)

goal (1 subgoal):
 1. inner x (y + z) = cnj_class.cnj (inner (y + z) x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inner x (y + z) = cnj_class.cnj (inner (y + z) x)

goal (1 subgoal):
 1. inner x (y + z) = inner x y + inner x z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inner x (y + z) = cnj_class.cnj (inner (y + z) x)

goal (1 subgoal):
 1. inner x (y + z) = inner x y + inner x z
[PROOF STEP]
have "... = cnj ((inner y x) +(inner z x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (inner (y + z) x) = cnj_class.cnj (inner y x + inner z x)
[PROOF STEP]
using inner_add_left
[PROOF STATE]
proof (prove)
using this:
inner (?x + ?y) ?z = inner ?x ?z + inner ?y ?z

goal (1 subgoal):
 1. cnj_class.cnj (inner (y + z) x) = cnj_class.cnj (inner y x + inner z x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (inner (y + z) x) = cnj_class.cnj (inner y x + inner z x)

goal (1 subgoal):
 1. inner x (y + z) = inner x y + inner x z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (inner (y + z) x) = cnj_class.cnj (inner y x + inner z x)

goal (1 subgoal):
 1. inner x (y + z) = inner x y + inner x z
[PROOF STEP]
have "... = cnj (inner y x) + cnj (inner z x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (inner y x + inner z x) = cnj_class.cnj (inner y x) + cnj_class.cnj (inner z x)
[PROOF STEP]
using cnj_add
[PROOF STATE]
proof (prove)
using this:
cnj_class.cnj (?a + ?b) = cnj_class.cnj ?a + cnj_class.cnj ?b

goal (1 subgoal):
 1. cnj_class.cnj (inner y x + inner z x) = cnj_class.cnj (inner y x) + cnj_class.cnj (inner z x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (inner y x + inner z x) = cnj_class.cnj (inner y x) + cnj_class.cnj (inner z x)

goal (1 subgoal):
 1. inner x (y + z) = inner x y + inner x z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (inner y x + inner z x) = cnj_class.cnj (inner y x) + cnj_class.cnj (inner z x)

goal (1 subgoal):
 1. inner x (y + z) = inner x y + inner x z
[PROOF STEP]
have "... = inner x y + inner x z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (inner y x) + cnj_class.cnj (inner z x) = inner x y + inner x z
[PROOF STEP]
using inner_commute[of x y]
[PROOF STATE]
proof (prove)
using this:
inner x y = cnj_class.cnj (inner y x)

goal (1 subgoal):
 1. cnj_class.cnj (inner y x) + cnj_class.cnj (inner z x) = inner x y + inner x z
[PROOF STEP]
using inner_commute[of x z]
[PROOF STATE]
proof (prove)
using this:
inner x y = cnj_class.cnj (inner y x)
inner x z = cnj_class.cnj (inner z x)

goal (1 subgoal):
 1. cnj_class.cnj (inner y x) + cnj_class.cnj (inner z x) = inner x y + inner x z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (inner y x) + cnj_class.cnj (inner z x) = inner x y + inner x z

goal (1 subgoal):
 1. inner x (y + z) = inner x y + inner x z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
inner x (y + z) = inner x y + inner x z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inner x (y + z) = inner x y + inner x z

goal (1 subgoal):
 1. inner x (y + z) = inner x y + inner x z
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
inner x (y + z) = inner x y + inner x z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inner_scaleR_right [simp]: "inner x (scale r y) = (cnj r) * (inner x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner x (scale r y) = cnj_class.cnj r * inner x y
[PROOF STEP]
using inner_scaleR_left [of r y x]
[PROOF STATE]
proof (prove)
using this:
inner (scale r y) x = r * inner y x

goal (1 subgoal):
 1. inner x (scale r y) = cnj_class.cnj r * inner x y
[PROOF STEP]
by (metis (no_types) cnj_mult local.inner_commute)


[STATEMENT]
lemma inner_zero_right [simp]: "inner x 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner x (0::'b) = (0::'a)
[PROOF STEP]
using inner_zero_left [of x]
[PROOF STATE]
proof (prove)
using this:
inner (0::'b) x = (0::'a)

goal (1 subgoal):
 1. inner x (0::'b) = (0::'a)
[PROOF STEP]
by (metis local.inner_commute local.inner_eq_zero_iff)


[STATEMENT]
lemma inner_minus_right [simp]: "inner x (- y) = - inner x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner x (- y) = - inner x y
[PROOF STEP]
using inner_minus_left [of y x]
[PROOF STATE]
proof (prove)
using this:
inner (- y) x = - inner y x

goal (1 subgoal):
 1. inner x (- y) = - inner x y
[PROOF STEP]
by (metis (no_types) add_eq_0_iff local.inner_add_right local.inner_zero_right)


[STATEMENT]
lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner x (y - z) = inner x y - inner x z
[PROOF STEP]
using inner_diff_left [of y z x]
[PROOF STATE]
proof (prove)
using this:
inner (y - z) x = inner y x - inner z x

goal (1 subgoal):
 1. inner x (y - z) = inner x y - inner x z
[PROOF STEP]
by (metis add_uminus_conv_diff local.inner_add_right local.inner_minus_right)


[STATEMENT]
lemma inner_sum_right: "inner x (\<Sum>y\<in>A. f y) = (\<Sum>y\<in>A. inner x (f y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner x (sum f A) = (\<Sum>y\<in>A. inner x (f y))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inner x (sum f A) = (\<Sum>y\<in>A. inner x (f y))
[PROOF STEP]
have "inner x (\<Sum>y\<in>A. f y) = cnj (inner (\<Sum>y\<in>A. f y) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner x (sum f A) = cnj_class.cnj (inner (sum f A) x)
[PROOF STEP]
using inner_commute
[PROOF STATE]
proof (prove)
using this:
inner ?x ?y = cnj_class.cnj (inner ?y ?x)

goal (1 subgoal):
 1. inner x (sum f A) = cnj_class.cnj (inner (sum f A) x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inner x (sum f A) = cnj_class.cnj (inner (sum f A) x)

goal (1 subgoal):
 1. inner x (sum f A) = (\<Sum>y\<in>A. inner x (f y))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inner x (sum f A) = cnj_class.cnj (inner (sum f A) x)

goal (1 subgoal):
 1. inner x (sum f A) = (\<Sum>y\<in>A. inner x (f y))
[PROOF STEP]
have "... = cnj (\<Sum>xa\<in>A. inner (f xa) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (inner (sum f A) x) = cnj_class.cnj (\<Sum>xa\<in>A. inner (f xa) x)
[PROOF STEP]
unfolding inner_sum_left [of f A x]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (\<Sum>xa\<in>A. inner (f xa) x) = cnj_class.cnj (\<Sum>xa\<in>A. inner (f xa) x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (inner (sum f A) x) = cnj_class.cnj (\<Sum>xa\<in>A. inner (f xa) x)

goal (1 subgoal):
 1. inner x (sum f A) = (\<Sum>y\<in>A. inner x (f y))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (inner (sum f A) x) = cnj_class.cnj (\<Sum>xa\<in>A. inner (f xa) x)

goal (1 subgoal):
 1. inner x (sum f A) = (\<Sum>y\<in>A. inner x (f y))
[PROOF STEP]
have "... = (\<Sum>xa\<in>A. cnj (inner (f xa) x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (\<Sum>xa\<in>A. inner (f xa) x) = (\<Sum>xa\<in>A. cnj_class.cnj (inner (f xa) x))
[PROOF STEP]
unfolding cnj_sum
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>xa\<in>A. cnj_class.cnj (inner (f xa) x)) = (\<Sum>xa\<in>A. cnj_class.cnj (inner (f xa) x))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (\<Sum>xa\<in>A. inner (f xa) x) = (\<Sum>xa\<in>A. cnj_class.cnj (inner (f xa) x))

goal (1 subgoal):
 1. inner x (sum f A) = (\<Sum>y\<in>A. inner x (f y))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (\<Sum>xa\<in>A. inner (f xa) x) = (\<Sum>xa\<in>A. cnj_class.cnj (inner (f xa) x))

goal (1 subgoal):
 1. inner x (sum f A) = (\<Sum>y\<in>A. inner x (f y))
[PROOF STEP]
have "... = (\<Sum>xa\<in>A. inner x (f xa))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>xa\<in>A. cnj_class.cnj (inner (f xa) x)) = (\<Sum>xa\<in>A. inner x (f xa))
[PROOF STEP]
by (rule sum.cong, simp, metis inner_commute)
[PROOF STATE]
proof (state)
this:
(\<Sum>xa\<in>A. cnj_class.cnj (inner (f xa) x)) = (\<Sum>xa\<in>A. inner x (f xa))

goal (1 subgoal):
 1. inner x (sum f A) = (\<Sum>y\<in>A. inner x (f y))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
inner x (sum f A) = (\<Sum>xa\<in>A. inner x (f xa))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inner x (sum f A) = (\<Sum>xa\<in>A. inner x (f xa))

goal (1 subgoal):
 1. inner x (sum f A) = (\<Sum>y\<in>A. inner x (f y))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
inner x (sum f A) = (\<Sum>y\<in>A. inner x (f y))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma aux_Cauchy:
shows "0 \<le> real_of (inner x x + (cnj a) * (inner x y) + a * ((cnj (inner x y)) + (cnj a) * (inner y y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> real_of (inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> real_of (inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y))
[PROOF STEP]
have "(inner (x+scale a y) (x+scale a y)) = (inner (x+scale a y) x) + (inner (x+scale a y) (scale a y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner (x + scale a y) (x + scale a y) = inner (x + scale a y) x + inner (x + scale a y) (scale a y)
[PROOF STEP]
unfolding inner_add_right
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner (x + scale a y) x + inner (x + scale a y) (scale a y) = inner (x + scale a y) x + inner (x + scale a y) (scale a y)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
inner (x + scale a y) (x + scale a y) = inner (x + scale a y) x + inner (x + scale a y) (scale a y)

goal (1 subgoal):
 1. 0 \<le> real_of (inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inner (x + scale a y) (x + scale a y) = inner (x + scale a y) x + inner (x + scale a y) (scale a y)

goal (1 subgoal):
 1. 0 \<le> real_of (inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y))
[PROOF STEP]
have "... = inner x x + (cnj a) * (inner x y) + a * ((cnj (inner x y)) + (cnj a) * (inner y y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner (x + scale a y) x + inner (x + scale a y) (scale a y) = inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y)
[PROOF STEP]
unfolding inner_add_left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner x x + inner (scale a y) x + (inner x (scale a y) + inner (scale a y) (scale a y)) = inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y)
[PROOF STEP]
unfolding inner_scaleR_left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner x x + a * inner y x + (inner x (scale a y) + a * inner y (scale a y)) = inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y)
[PROOF STEP]
unfolding inner_scaleR_right
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner x x + a * inner y x + (cnj_class.cnj a * inner x y + a * (cnj_class.cnj a * inner y y)) = inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y)
[PROOF STEP]
unfolding inner_commute[of y x]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner x x + a * cnj_class.cnj (inner x y) + (cnj_class.cnj a * inner x y + a * (cnj_class.cnj a * inner y y)) = inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y)
[PROOF STEP]
unfolding distrib_left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner x x + a * cnj_class.cnj (inner x y) + (cnj_class.cnj a * inner x y + a * (cnj_class.cnj a * inner y y)) = inner x x + cnj_class.cnj a * inner x y + (a * cnj_class.cnj (inner x y) + a * (cnj_class.cnj a * inner y y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inner (x + scale a y) x + inner (x + scale a y) (scale a y) = inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y)

goal (1 subgoal):
 1. 0 \<le> real_of (inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
inner (x + scale a y) (x + scale a y) = inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inner (x + scale a y) (x + scale a y) = inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y)

goal (1 subgoal):
 1. 0 \<le> real_of (inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y))
[PROOF STEP]
by (metis inner_ge_zero)
[PROOF STATE]
proof (state)
this:
0 \<le> real_of (inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma real_inner_inner: "real_of (inner x x * inner y y) = real_of (inner x x) * real_of (inner y y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (inner x x * inner y y) = real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
by (metis real_scalar_mult real_scalar_mult2)


[STATEMENT]
lemma Cauchy_Schwarz_ineq:
  "real_of (cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
define cnj_a where "cnj_a = - cnj (inner x y)/ (inner y y)"
[PROOF STATE]
proof (state)
this:
cnj_a = - cnj_class.cnj (inner x y) / inner y y

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
define a where "a = cnj (cnj_a)"
[PROOF STATE]
proof (state)
this:
a = cnj_class.cnj cnj_a

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
have cnj_rw: "(cnj a) = cnj_a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj a = cnj_a
[PROOF STEP]
unfolding a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (cnj_class.cnj cnj_a) = cnj_a
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
cnj_class.cnj a = cnj_a

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
have rw_0: "(cnj (inner x y)) + (cnj a) * (inner y y) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y = (0::'a)
[PROOF STEP]
unfolding cnj_rw cnj_a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (inner x y) + - cnj_class.cnj (inner x y) / inner y y * inner y y = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y = (0::'a)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
have "0 \<le> real_of (inner x x + (cnj a) * (inner x y) + a * ((cnj (inner x y)) + (cnj a) * (inner y y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> real_of (inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y))
[PROOF STEP]
using aux_Cauchy
[PROOF STATE]
proof (prove)
using this:
0 \<le> real_of (inner ?x ?x + cnj_class.cnj ?a * inner ?x ?y + ?a * (cnj_class.cnj (inner ?x ?y) + cnj_class.cnj ?a * inner ?y ?y))

goal (1 subgoal):
 1. 0 \<le> real_of (inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> real_of (inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y))

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 \<le> real_of (inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y))

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
have "... = real_of (inner x x + (cnj a) * (inner x y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y)) = real_of (inner x x + cnj_class.cnj a * inner x y)
[PROOF STEP]
unfolding rw_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (inner x x + cnj_class.cnj a * inner x y + a * (0::'a)) = real_of (inner x x + cnj_class.cnj a * inner x y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of (inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y)) = real_of (inner x x + cnj_class.cnj a * inner x y)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of (inner x x + cnj_class.cnj a * inner x y + a * (cnj_class.cnj (inner x y) + cnj_class.cnj a * inner y y)) = real_of (inner x x + cnj_class.cnj a * inner x y)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
have "... = real_of (inner x x - cnj (inner x y) * inner x y / inner y y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (inner x x + cnj_class.cnj a * inner x y) = real_of (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)
[PROOF STEP]
unfolding cnj_rw cnj_a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (inner x x + - cnj_class.cnj (inner x y) / inner y y * inner x y) = real_of (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of (inner x x + cnj_class.cnj a * inner x y) = real_of (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 \<le> real_of (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)
[PROOF STEP]
have " 0 \<le> real_of (inner x x - cnj (inner x y) * inner x y / inner y y) "
[PROOF STATE]
proof (prove)
using this:
0 \<le> real_of (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)

goal (1 subgoal):
 1. 0 \<le> real_of (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
0 \<le> real_of (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
hence "0 \<le> real_of (inner y y)  * real_of (inner x x - cnj (inner x y) * inner x y / inner y y)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> real_of (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)

goal (1 subgoal):
 1. 0 \<le> real_of (inner y y) * real_of (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> real_of (inner y y) * real_of (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 \<le> real_of (inner y y) * real_of (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
have "... = real_of (real_of (inner y y)*\<^sub>R(inner x x - cnj (inner x y) * inner x y / inner y y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (inner y y) * real_of (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y) = real_of (real_of (inner y y) *\<^sub>R (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y))
[PROOF STEP]
unfolding real_scalar_mult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (inner y y) * real_of (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y) = real_of (inner y y) * real_of (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
real_of (inner y y) * real_of (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y) = real_of (real_of (inner y y) *\<^sub>R (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y))

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of (inner y y) * real_of (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y) = real_of (real_of (inner y y) *\<^sub>R (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y))

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
have "... = real_of ((inner y y) * (inner x x - cnj (inner x y) * inner x y / inner y y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (real_of (inner y y) *\<^sub>R (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)) = real_of (inner y y * (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y))
[PROOF STEP]
unfolding real_scalar_mult2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (inner y y * (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)) = real_of (inner y y * (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
real_of (real_of (inner y y) *\<^sub>R (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)) = real_of (inner y y * (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y))

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of (real_of (inner y y) *\<^sub>R (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)) = real_of (inner y y * (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y))

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
have "... = real_of ((inner x x - cnj (inner x y) * inner x y / inner y y)*(inner y y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (inner y y * (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)) = real_of ((inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y) * inner y y)
[PROOF STEP]
by (simp add: mult.commute)
[PROOF STATE]
proof (state)
this:
real_of (inner y y * (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)) = real_of ((inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y) * inner y y)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of (inner y y * (inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y)) = real_of ((inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y) * inner y y)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
have "... = real_of (((inner x x)*(inner y y) - cnj (inner x y) * inner x y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of ((inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y) * inner y y) = real_of (inner x x * inner y y - cnj_class.cnj (inner x y) * inner x y)
[PROOF STEP]
by (simp add: left_diff_distrib)
[PROOF STATE]
proof (state)
this:
real_of ((inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y) * inner y y) = real_of (inner x x * inner y y - cnj_class.cnj (inner x y) * inner x y)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of ((inner x x - cnj_class.cnj (inner x y) * inner x y / inner y y) * inner y y) = real_of (inner x x * inner y y - cnj_class.cnj (inner x y) * inner x y)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
have "... = real_of ((inner x x)*(inner y y)) - real_of (cnj (inner x y) * inner x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (inner x x * inner y y - cnj_class.cnj (inner x y) * inner x y) = real_of (inner x x * inner y y) - real_of (cnj_class.cnj (inner x y) * inner x y)
[PROOF STEP]
unfolding real_minus
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (inner x x * inner y y) - real_of (cnj_class.cnj (inner x y) * inner x y) = real_of (inner x x * inner y y) - real_of (cnj_class.cnj (inner x y) * inner x y)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
real_of (inner x x * inner y y - cnj_class.cnj (inner x y) * inner x y) = real_of (inner x x * inner y y) - real_of (cnj_class.cnj (inner x y) * inner x y)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 \<le> real_of (inner x x * inner y y) - real_of (cnj_class.cnj (inner x y) * inner x y)
[PROOF STEP]
have "real_of (cnj (inner x y) * inner x y) \<le> real_of ((inner x x)*(inner y y))"
[PROOF STATE]
proof (prove)
using this:
0 \<le> real_of (inner x x * inner y y) - real_of (cnj_class.cnj (inner x y) * inner x y)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x * inner y y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x * inner y y)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x * inner y y)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
unfolding real_inner_inner
[PROOF STATE]
proof (prove)
using this:
real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inner_cnj_ge_zero[simp]: "real_of ((inner x y) * cnj (inner x y)) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> real_of (inner x y * cnj_class.cnj (inner x y))
[PROOF STEP]
using real_a_cnj_ge_0
[PROOF STATE]
proof (prove)
using this:
0 \<le> real_of (?a * cnj_class.cnj ?a)

goal (1 subgoal):
 1. 0 \<le> real_of (inner x y * cnj_class.cnj (inner x y))
[PROOF STEP]
by auto


[STATEMENT]
lemma power2_norm_eq_inner: "(norm x)\<^sup>2 = real_of (inner x x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (norm x)\<^sup>2 = real_of (inner x x)
[PROOF STEP]
by (simp add: norm_def)


[STATEMENT]
lemma Cauchy_Schwarz_ineq2:
  "sqrt (real_of (cnj (inner x y) * inner x y)) \<le> norm x * norm y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (real_of (cnj_class.cnj (inner x y) * inner x y)) \<le> norm x * norm y
[PROOF STEP]
proof (rule power2_le_imp_le)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (sqrt (real_of (cnj_class.cnj (inner x y) * inner x y)))\<^sup>2 \<le> (norm x * norm y)\<^sup>2
 2. 0 \<le> norm x * norm y
[PROOF STEP]
have eq: "0 \<le> real_of (cnj (inner x y) * inner x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> real_of (cnj_class.cnj (inner x y) * inner x y)
[PROOF STEP]
by (simp add: mult.commute)
[PROOF STATE]
proof (state)
this:
0 \<le> real_of (cnj_class.cnj (inner x y) * inner x y)

goal (2 subgoals):
 1. (sqrt (real_of (cnj_class.cnj (inner x y) * inner x y)))\<^sup>2 \<le> (norm x * norm y)\<^sup>2
 2. 0 \<le> norm x * norm y
[PROOF STEP]
have "real_of (cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
using Cauchy_Schwarz_ineq
[PROOF STATE]
proof (prove)
using this:
real_of (cnj_class.cnj (inner ?x ?y) * inner ?x ?y) \<le> real_of (inner ?x ?x) * real_of (inner ?y ?y)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)

goal (2 subgoals):
 1. (sqrt (real_of (cnj_class.cnj (inner x y) * inner x y)))\<^sup>2 \<le> (norm x * norm y)\<^sup>2
 2. 0 \<le> norm x * norm y
[PROOF STEP]
thus "(sqrt (real_of (cnj (inner x y) * inner x y)))\<^sup>2 \<le> (norm x * norm y)\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)

goal (1 subgoal):
 1. (sqrt (real_of (cnj_class.cnj (inner x y) * inner x y)))\<^sup>2 \<le> (norm x * norm y)\<^sup>2
[PROOF STEP]
unfolding power_mult_distrib
[PROOF STATE]
proof (prove)
using this:
real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)

goal (1 subgoal):
 1. (sqrt (real_of (cnj_class.cnj (inner x y) * inner x y)))\<^sup>2 \<le> (norm x)\<^sup>2 * (norm y)\<^sup>2
[PROOF STEP]
unfolding power2_norm_eq_inner
[PROOF STATE]
proof (prove)
using this:
real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)

goal (1 subgoal):
 1. (sqrt (real_of (cnj_class.cnj (inner x y) * inner x y)))\<^sup>2 \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
unfolding real_sqrt_pow2[OF eq]
[PROOF STATE]
proof (prove)
using this:
real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)

goal (1 subgoal):
 1. real_of (cnj_class.cnj (inner x y) * inner x y) \<le> real_of (inner x x) * real_of (inner y y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(sqrt (real_of (cnj_class.cnj (inner x y) * inner x y)))\<^sup>2 \<le> (norm x * norm y)\<^sup>2

goal (1 subgoal):
 1. 0 \<le> norm x * norm y
[PROOF STEP]
show "0 \<le> norm x * norm y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> norm x * norm y
[PROOF STEP]
unfolding norm_eq_sqrt_inner
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> sqrt (real_of (inner x x)) * sqrt (real_of (inner y y))
[PROOF STEP]
by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero)
[PROOF STATE]
proof (state)
this:
0 \<le> norm x * norm y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma orthogonal_clauses:
  "orthogonal a 0"
  "orthogonal a x \<Longrightarrow> orthogonal a (scale c x)"
  "orthogonal a x \<Longrightarrow> orthogonal a (- x)"
  "orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x + y)"
  "orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x - y)"
  "orthogonal 0 a"
  "orthogonal x a \<Longrightarrow> orthogonal (scale c x) a"
  "orthogonal x a \<Longrightarrow> orthogonal (- x) a"
  "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a"
  "orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x - y) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((orthogonal a (0::'b) &&& (orthogonal a x \<Longrightarrow> orthogonal a (scale c x))) &&& (orthogonal a x \<Longrightarrow> orthogonal a (- x)) &&& (\<lbrakk>orthogonal a x; orthogonal a y\<rbrakk> \<Longrightarrow> orthogonal a (x + y)) &&& (\<lbrakk>orthogonal a x; orthogonal a y\<rbrakk> \<Longrightarrow> orthogonal a (x - y))) &&& (orthogonal (0::'b) a &&& (orthogonal x a \<Longrightarrow> orthogonal (scale c x) a)) &&& (orthogonal x a \<Longrightarrow> orthogonal (- x) a) &&& (\<lbrakk>orthogonal x a; orthogonal y a\<rbrakk> \<Longrightarrow> orthogonal (x + y) a) &&& (\<lbrakk>orthogonal x a; orthogonal y a\<rbrakk> \<Longrightarrow> orthogonal (x - y) a)
[PROOF STEP]
unfolding orthogonal_def inner_add inner_diff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((inner a (0::'b) = (0::'a) &&& (inner a x = (0::'a) \<Longrightarrow> inner a (scale c x) = (0::'a))) &&& (inner a x = (0::'a) \<Longrightarrow> inner a (- x) = (0::'a)) &&& (\<lbrakk>inner a x = (0::'a); inner a y = (0::'a)\<rbrakk> \<Longrightarrow> inner a x + inner a y = (0::'a)) &&& (\<lbrakk>inner a x = (0::'a); inner a y = (0::'a)\<rbrakk> \<Longrightarrow> inner a x - inner a y = (0::'a))) &&& (inner (0::'b) a = (0::'a) &&& (inner x a = (0::'a) \<Longrightarrow> inner (scale c x) a = (0::'a))) &&& (inner x a = (0::'a) \<Longrightarrow> inner (- x) a = (0::'a)) &&& (\<lbrakk>inner x a = (0::'a); inner y a = (0::'a)\<rbrakk> \<Longrightarrow> inner x a + inner y a = (0::'a)) &&& (\<lbrakk>inner x a = (0::'a); inner y a = (0::'a)\<rbrakk> \<Longrightarrow> inner x a - inner y a = (0::'a))
[PROOF STEP]
by auto


[STATEMENT]
lemma inner_commute_zero: "(inner xa x = 0) = (inner x xa = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inner xa x = (0::'a)) = (inner x xa = (0::'a))
[PROOF STEP]
by (metis cnj_0 local.inner_commute)


[STATEMENT]
lemma vector_sub_project_orthogonal:
  "inner b (x - scale (inner x b / (inner b b)) b) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner b (x - scale (inner x b / inner b b) b) = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inner b (x - scale (inner x b / inner b b) b) = (0::'a)
[PROOF STEP]
have f1: "\<And>b a ba. inner b (scale a ba) = cnj (a * inner ba b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. inner b (scale a ba) = cnj_class.cnj (a * inner ba b)
[PROOF STEP]
by (metis local.inner_commute local.inner_scaleR_left)
[PROOF STATE]
proof (state)
this:
inner ?b (scale ?a ?ba) = cnj_class.cnj (?a * inner ?ba ?b)

goal (1 subgoal):
 1. inner b (x - scale (inner x b / inner b b) b) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
inner ?b (scale ?a ?ba) = cnj_class.cnj (?a * inner ?ba ?b)

goal (1 subgoal):
 1. inner b (x - scale (inner x b / inner b b) b) = (0::'a)
[PROOF STEP]
assume "b \<noteq> 0"
[PROOF STATE]
proof (state)
this:
b \<noteq> (0::'b)

goal (1 subgoal):
 1. inner b (x - scale (inner x b / inner b b) b) = (0::'a)
[PROOF STEP]
hence "cnj (inner x b) = inner b x \<and> inner b b \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
b \<noteq> (0::'b)

goal (1 subgoal):
 1. cnj_class.cnj (inner x b) = inner b x \<and> inner b b \<noteq> (0::'a)
[PROOF STEP]
by (metis (no_types) local.inner_commute local.inner_eq_zero_iff)
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (inner x b) = inner b x \<and> inner b b \<noteq> (0::'a)

goal (1 subgoal):
 1. inner b (x - scale (inner x b / inner b b) b) = (0::'a)
[PROOF STEP]
hence "inner b (x - scale (inner x b / inner b b) b) = 0"
[PROOF STATE]
proof (prove)
using this:
cnj_class.cnj (inner x b) = inner b x \<and> inner b b \<noteq> (0::'a)

goal (1 subgoal):
 1. inner b (x - scale (inner x b / inner b b) b) = (0::'a)
[PROOF STEP]
using f1 local.inner_diff_right
[PROOF STATE]
proof (prove)
using this:
cnj_class.cnj (inner x b) = inner b x \<and> inner b b \<noteq> (0::'a)
inner ?b (scale ?a ?ba) = cnj_class.cnj (?a * inner ?ba ?b)
inner ?x (?y - ?z) = inner ?x ?y - inner ?x ?z

goal (1 subgoal):
 1. inner b (x - scale (inner x b / inner b b) b) = (0::'a)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
inner b (x - scale (inner x b / inner b b) b) = (0::'a)

goal (1 subgoal):
 1. inner b (x - scale (inner x b / inner b b) b) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
b \<noteq> (0::'b) \<Longrightarrow> inner b (x - scale (inner x b / inner b b) b) = (0::'a)

goal (1 subgoal):
 1. inner b (x - scale (inner x b / inner b b) b) = (0::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<noteq> (0::'b) \<Longrightarrow> inner b (x - scale (inner x b / inner b b) b) = (0::'a)

goal (1 subgoal):
 1. inner b (x - scale (inner x b / inner b b) b) = (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
inner b (x - scale (inner x b / inner b b) b) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. orthogonal x y = orthogonal y x
[PROOF STEP]
unfolding orthogonal_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inner x y = (0::'a)) = (inner y x = (0::'a))
[PROOF STEP]
using inner_commute_zero
[PROOF STATE]
proof (prove)
using this:
(inner ?xa ?x = (0::'a)) = (inner ?x ?xa = (0::'a))

goal (1 subgoal):
 1. (inner x y = (0::'a)) = (inner y x = (0::'a))
[PROOF STEP]
by auto


[STATEMENT]
lemma pairwise_orthogonal_insert:
  assumes "pairwise orthogonal S"
  and "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y"
  shows "pairwise orthogonal (insert x S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pairwise orthogonal (insert x S)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
pairwise orthogonal S
?y \<in> S \<Longrightarrow> orthogonal x ?y

goal (1 subgoal):
 1. pairwise orthogonal (insert x S)
[PROOF STEP]
unfolding pairwise_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. \<forall>y\<in>S. x \<noteq> y \<longrightarrow> orthogonal x y
?y \<in> S \<Longrightarrow> orthogonal x ?y

goal (1 subgoal):
 1. \<forall>xa\<in>insert x S. \<forall>y\<in>insert x S. xa \<noteq> y \<longrightarrow> orthogonal xa y
[PROOF STEP]
by (auto simp add: orthogonal_commute)


[STATEMENT]
lemma sum_0_all:
  assumes a: "\<forall>a\<in>A. f a \<ge> (0 :: real)"
  and s0: "sum f A = 0" and f: "finite A"
  shows "\<forall>a\<in>A. f a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>A. f a = 0
[PROOF STEP]
using a f s0 sum_nonneg_eq_0_iff
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>A. 0 \<le> f a
finite A
sum f A = 0
\<lbrakk>finite ?A; \<And>x. x \<in> ?A \<Longrightarrow> (0::?'a) \<le> ?f x\<rbrakk> \<Longrightarrow> (sum ?f ?A = (0::?'a)) = (\<forall>x\<in>?A. ?f x = (0::?'a))

goal (1 subgoal):
 1. \<forall>a\<in>A. f a = 0
[PROOF STEP]
by blast


[STATEMENT]
lemma inner_ge_zero [simp]: "0 \<le> real_of (inner x x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> real_of (inner x x)
[PROOF STEP]
by (auto simp add: inner_vec_def real_sum sum_nonneg)


[STATEMENT]
lemma real_scalar_mult2: "real_of (inner x x) *\<^sub>R A = inner x x * A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (inner x x) *\<^sub>R A = inner x x * A
[PROOF STEP]
by (auto simp add: inner_vec_def)
  (metis (mono_tags, lifting) Finite_Cartesian_Product.sum_cong_aux
  real_scalar_mult2 real_sum scaleR_left.sum scale_sum_left)


[STATEMENT]
lemma i1: "inner x y = cnj (inner y x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner x y = cnj_class.cnj (inner y x)
[PROOF STEP]
by (auto simp add: inner_vec_def cnj_sum cnj_mult mult.commute)
   (meson local.inner_commute)


[STATEMENT]
lemma i2: "inner (x + y) z = inner x z + inner y z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner (x + y) z = inner x z + inner y z
[PROOF STEP]
using local.inner_left_distrib sum.distrib inner_vec_def
[PROOF STATE]
proof (prove)
using this:
inner_field (?x + ?y) ?z = inner_field ?x ?z + inner_field ?y ?z
(\<Sum>x\<in>?A. ?g x + ?h x) = sum ?g ?A + sum ?h ?A
inner ?x ?y = (\<Sum>i\<in>UNIV. inner_field (?x $ i) (?y $ i))

goal (1 subgoal):
 1. inner (x + y) z = inner x z + inner y z
[PROOF STEP]
by force


[STATEMENT]
lemma i3: "inner (r *s x) y = r * inner x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner (r *s x) y = r * inner x y
[PROOF STEP]
by (auto simp add: inner_vec_def scale_sum_right)


[STATEMENT]
lemma i4: assumes "inner x x = 0"
shows "x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = 0
[PROOF STEP]
proof (unfold vec_eq_iff, clarify, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. x $ i = (0::'a)
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. x $ i = (0::'a)
[PROOF STEP]
have "0 = real_of (\<Sum>i\<in>UNIV. inner_field (x $ i) (x $ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = real_of (\<Sum>i\<in>UNIV. inner_field (x $ i) (x $ i))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
inner x x = (0::'a)

goal (1 subgoal):
 1. 0 = real_of (\<Sum>i\<in>UNIV. inner_field (x $ i) (x $ i))
[PROOF STEP]
by (simp add: inner_vec_def)
[PROOF STATE]
proof (state)
this:
0 = real_of (\<Sum>i\<in>UNIV. inner_field (x $ i) (x $ i))

goal (1 subgoal):
 1. \<And>i. x $ i = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 = real_of (\<Sum>i\<in>UNIV. inner_field (x $ i) (x $ i))

goal (1 subgoal):
 1. \<And>i. x $ i = (0::'a)
[PROOF STEP]
have "... = (\<Sum>i\<in>UNIV. real_of (inner_field (x $ i) (x $ i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of (\<Sum>i\<in>UNIV. inner_field (x $ i) (x $ i)) = (\<Sum>i\<in>UNIV. real_of (inner_field (x $ i) (x $ i)))
[PROOF STEP]
using real_sum
[PROOF STATE]
proof (prove)
using this:
real_of (sum ?f ?A) = (\<Sum>i\<in>?A. real_of (?f i))

goal (1 subgoal):
 1. real_of (\<Sum>i\<in>UNIV. inner_field (x $ i) (x $ i)) = (\<Sum>i\<in>UNIV. real_of (inner_field (x $ i) (x $ i)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of (\<Sum>i\<in>UNIV. inner_field (x $ i) (x $ i)) = (\<Sum>i\<in>UNIV. real_of (inner_field (x $ i) (x $ i)))

goal (1 subgoal):
 1. \<And>i. x $ i = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 = (\<Sum>i\<in>UNIV. real_of (inner_field (x $ i) (x $ i)))
[PROOF STEP]
have "0 = (\<Sum>i\<in>UNIV. real_of (inner_field (x $ i) (x $ i)))"
[PROOF STATE]
proof (prove)
using this:
0 = (\<Sum>i\<in>UNIV. real_of (inner_field (x $ i) (x $ i)))

goal (1 subgoal):
 1. 0 = (\<Sum>i\<in>UNIV. real_of (inner_field (x $ i) (x $ i)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
0 = (\<Sum>i\<in>UNIV. real_of (inner_field (x $ i) (x $ i)))

goal (1 subgoal):
 1. \<And>i. x $ i = (0::'a)
[PROOF STEP]
hence "real_of (inner_field (x $ a) (x $ a)) = 0"
[PROOF STATE]
proof (prove)
using this:
0 = (\<Sum>i\<in>UNIV. real_of (inner_field (x $ i) (x $ i)))

goal (1 subgoal):
 1. real_of (inner_field (x $ a) (x $ a)) = 0
[PROOF STEP]
using sum_0_all F.inner_ge_zero
[PROOF STATE]
proof (prove)
using this:
0 = (\<Sum>i\<in>UNIV. real_of (inner_field (x $ i) (x $ i)))
\<lbrakk>\<forall>a\<in>?A. 0 \<le> ?f a; sum ?f ?A = 0; finite ?A\<rbrakk> \<Longrightarrow> \<forall>a\<in>?A. ?f a = 0
0 \<le> real_of (inner_field ?x ?x)

goal (1 subgoal):
 1. real_of (inner_field (x $ a) (x $ a)) = 0
[PROOF STEP]
by (metis (no_types, lifting) finite iso_tuple_UNIV_I)
[PROOF STATE]
proof (state)
this:
real_of (inner_field (x $ a) (x $ a)) = 0

goal (1 subgoal):
 1. \<And>i. x $ i = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real_of (inner_field (x $ a) (x $ a)) = 0
[PROOF STEP]
show "x $ a = 0"
[PROOF STATE]
proof (prove)
using this:
real_of (inner_field (x $ a) (x $ a)) = 0

goal (1 subgoal):
 1. x $ a = (0::'a)
[PROOF STEP]
by (metis F.inner_eq_zero_iff F.inner_gt_zero_iff real_0)
[PROOF STATE]
proof (state)
this:
x $ a = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inner_0_0[simp]: "inner 0 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner 0 0 = (0::'a)
[PROOF STEP]
unfolding inner_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>UNIV. inner_field (0 $ i) (0 $ i)) = (0::'a)
[PROOF STEP]
by auto


[STATEMENT]
lemma dot_lmul_matrix: "inner_rows (x v* A) y = inner_cols x ((\<chi> i j. cnj (A $ i $ j)) *v y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner_rows (x v* A) y = inner_cols x ((\<chi>i j. cnj_class.cnj (A $ i $ j)) *v y)
[PROOF STEP]
apply (simp add: COLS.inner_vec_def ROWS.inner_vec_def matrix_vector_mult_def
       vector_matrix_mult_def sum_distrib_right cnj_sum ac_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>UNIV. cnj_class.cnj (y $ i) * (\<Sum>ia\<in>UNIV. x $ ia * A $ ia $ i)) = (\<Sum>i\<in>UNIV. x $ i * (\<Sum>j\<in>UNIV. cnj_class.cnj (y $ j * cnj_class.cnj (A $ i $ j))))
[PROOF STEP]
proof (unfold sum_distrib_left, subst sum.swap, rule sum.cong, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> UNIV \<Longrightarrow> (\<Sum>i\<in>UNIV. cnj_class.cnj (y $ i) * (x $ xa * A $ xa $ i)) = (\<Sum>n\<in>UNIV. x $ xa * cnj_class.cnj (y $ n * cnj_class.cnj (A $ xa $ n)))
[PROOF STEP]
fix xa::'cols
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> UNIV \<Longrightarrow> (\<Sum>i\<in>UNIV. cnj_class.cnj (y $ i) * (x $ xa * A $ xa $ i)) = (\<Sum>n\<in>UNIV. x $ xa * cnj_class.cnj (y $ n * cnj_class.cnj (A $ xa $ n)))
[PROOF STEP]
show "(\<Sum>i\<in>UNIV. cnj (y $ i) * (x $ xa * A $ xa $ i))
    = (\<Sum>n\<in>UNIV. x $ xa * cnj (y $ n * cnj (A $ xa $ n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>UNIV. cnj_class.cnj (y $ i) * (x $ xa * A $ xa $ i)) = (\<Sum>n\<in>UNIV. x $ xa * cnj_class.cnj (y $ n * cnj_class.cnj (A $ xa $ n)))
[PROOF STEP]
proof (rule sum.cong, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xb. xb \<in> UNIV \<Longrightarrow> cnj_class.cnj (y $ xb) * (x $ xa * A $ xa $ xb) = x $ xa * cnj_class.cnj (y $ xb * cnj_class.cnj (A $ xa $ xb))
[PROOF STEP]
fix xb:: 'rows
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xb. xb \<in> UNIV \<Longrightarrow> cnj_class.cnj (y $ xb) * (x $ xa * A $ xa $ xb) = x $ xa * cnj_class.cnj (y $ xb * cnj_class.cnj (A $ xa $ xb))
[PROOF STEP]
show "cnj_class.cnj (y $ xb) * (x $ xa * A $ xa $ xb)
      = x $ xa * cnj_class.cnj (y $ xb * cnj_class.cnj (A $ xa $ xb))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (y $ xb) * (x $ xa * A $ xa $ xb) = x $ xa * cnj_class.cnj (y $ xb * cnj_class.cnj (A $ xa $ xb))
[PROOF STEP]
unfolding cnj_mult cnj_idem
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (y $ xb) * (x $ xa * A $ xa $ xb) = x $ xa * (cnj_class.cnj (y $ xb) * A $ xa $ xb)
[PROOF STEP]
unfolding mult.assoc
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (y $ xb) * (x $ xa * A $ xa $ xb) = x $ xa * (cnj_class.cnj (y $ xb) * A $ xa $ xb)
[PROOF STEP]
unfolding mult.commute[of "A $ xa $ xb"]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj_class.cnj (y $ xb) * (x $ xa * A $ xa $ xb) = x $ xa * (cnj_class.cnj (y $ xb) * A $ xa $ xb)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cnj_class.cnj (y $ xb) * (x $ xa * A $ xa $ xb) = x $ xa * cnj_class.cnj (y $ xb * cnj_class.cnj (A $ xa $ xb))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>UNIV. cnj_class.cnj (y $ i) * (x $ xa * A $ xa $ i)) = (\<Sum>n\<in>UNIV. x $ xa * cnj_class.cnj (y $ n * cnj_class.cnj (A $ xa $ n)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subspace_orthogonal_complement: "subspace (orthogonal_complement W)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.subspace (orthogonal_complement W)
[PROOF STEP]
unfolding subspace_def orthogonal_complement_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'b) \<in> {x. \<forall>y\<in>W. orthogonal y x} \<and> (\<forall>x\<in>{x. \<forall>y\<in>W. orthogonal y x}. \<forall>y\<in>{x. \<forall>y\<in>W. orthogonal y x}. x + y \<in> {x. \<forall>y\<in>W. orthogonal y x}) \<and> (\<forall>c. \<forall>x\<in>{x. \<forall>y\<in>W. orthogonal y x}. scale c x \<in> {x. \<forall>y\<in>W. orthogonal y x})
[PROOF STEP]
by (auto simp add: orthogonal_def local.inner_right_distrib)


[STATEMENT]
lemma orthogonal_complement_mono:
  assumes A_in_B: "A \<subseteq> B"
  shows "orthogonal_complement B \<subseteq> orthogonal_complement A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. orthogonal_complement B \<subseteq> orthogonal_complement A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> orthogonal_complement B \<Longrightarrow> x \<in> orthogonal_complement A
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> orthogonal_complement B \<Longrightarrow> x \<in> orthogonal_complement A
[PROOF STEP]
assume x: "x \<in> orthogonal_complement B"
[PROOF STATE]
proof (state)
this:
x \<in> orthogonal_complement B

goal (1 subgoal):
 1. \<And>x. x \<in> orthogonal_complement B \<Longrightarrow> x \<in> orthogonal_complement A
[PROOF STEP]
show "x \<in> orthogonal_complement A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> orthogonal_complement A
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x \<in> orthogonal_complement B

goal (1 subgoal):
 1. x \<in> orthogonal_complement A
[PROOF STEP]
unfolding orthogonal_complement_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {x. \<forall>y\<in>B. orthogonal y x}

goal (1 subgoal):
 1. x \<in> {x. \<forall>y\<in>A. orthogonal y x}
[PROOF STEP]
by (simp add: orthogonal_def, metis A_in_B in_mono)
[PROOF STATE]
proof (state)
this:
x \<in> orthogonal_complement A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma B_in_orthogonal_complement_of_orthogonal_complement:
  shows "B \<subseteq> orthogonal_complement (orthogonal_complement B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<subseteq> orthogonal_complement (orthogonal_complement B)
[PROOF STEP]
by (auto simp add: orthogonal_complement_def orthogonal_def inner_commute_zero)


[STATEMENT]
lemma vector_sub_project_orthogonal_proj:
  shows "inner b (x - proj x b) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner b (x - proj x b) = (0::'a)
[PROOF STEP]
using vector_sub_project_orthogonal
[PROOF STATE]
proof (prove)
using this:
inner ?b (?x - scale (inner ?x ?b / inner ?b ?b) ?b) = (0::'a)

goal (1 subgoal):
 1. inner b (x - proj x b) = (0::'a)
[PROOF STEP]
unfolding proj_def
[PROOF STATE]
proof (prove)
using this:
inner ?b (?x - scale (inner ?x ?b / inner ?b ?b) ?b) = (0::'a)

goal (1 subgoal):
 1. inner b (x - scale (inner x b / inner b b) b) = (0::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma orthogonal_proj_set:
  assumes yC: "y\<in>C" and C: "finite C" and p: "pairwise orthogonal C"
  shows "orthogonal (a - proj_onto a C) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. orthogonal (a - proj_onto a C) y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. orthogonal (a - proj_onto a C) y
[PROOF STEP]
have Cy: "C = insert y (C - {y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C = insert y (C - {y})
[PROOF STEP]
using yC
[PROOF STATE]
proof (prove)
using this:
y \<in> C

goal (1 subgoal):
 1. C = insert y (C - {y})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C = insert y (C - {y})

goal (1 subgoal):
 1. orthogonal (a - proj_onto a C) y
[PROOF STEP]
have fth: "finite (C - {y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (C - {y})
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
finite C

goal (1 subgoal):
 1. finite (C - {y})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (C - {y})

goal (1 subgoal):
 1. orthogonal (a - proj_onto a C) y
[PROOF STEP]
show "orthogonal (a - proj_onto a C) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. orthogonal (a - proj_onto a C) y
[PROOF STEP]
unfolding orthogonal_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner (a - proj_onto a C) y = (0::'a)
[PROOF STEP]
unfolding proj_onto_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner (a - sum (proj a) C) y = (0::'a)
[PROOF STEP]
unfolding proj_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner (a - (\<Sum>u\<in>C. scale (inner a u / inner u u) u)) y = (0::'a)
[PROOF STEP]
unfolding inner_diff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner a y - inner (\<Sum>u\<in>C. scale (inner a u / inner u u) u) y = (0::'a)
[PROOF STEP]
unfolding inner_sum_left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner a y - (\<Sum>x\<in>C. inner (scale (inner a x / inner x x) x) y) = (0::'a)
[PROOF STEP]
unfolding right_minus_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner a y = (\<Sum>x\<in>C. inner (scale (inner a x / inner x x) x) y)
[PROOF STEP]
unfolding sum.remove[OF C yC]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner a y = inner (scale (inner a y / inner y y) y) y + (\<Sum>x\<in>C - {y}. inner (scale (inner a x / inner x x) x) y)
[PROOF STEP]
apply (clarsimp simp add: inner_commute[of y a])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<noteq> (0::'b) \<Longrightarrow> (\<Sum>x\<in>C - {y}. inner a x * inner x y / inner x x) = (0::'a)
[PROOF STEP]
apply (rule sum.neutral)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<noteq> (0::'b) \<Longrightarrow> \<forall>x\<in>C - {y}. inner a x * inner x y / inner x x = (0::'a)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>y \<noteq> (0::'b); x \<in> C; x \<noteq> y; inner a x \<noteq> (0::'a); x \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> inner x y = (0::'a)
[PROOF STEP]
apply (rule p[unfolded pairwise_def orthogonal_def, rule_format])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>y \<noteq> (0::'b); x \<in> C; x \<noteq> y; inner a x \<noteq> (0::'a); x \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> x \<in> C
 2. \<And>x. \<lbrakk>y \<noteq> (0::'b); x \<in> C; x \<noteq> y; inner a x \<noteq> (0::'a); x \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> y \<in> C
 3. \<And>x. \<lbrakk>y \<noteq> (0::'b); x \<in> C; x \<noteq> y; inner a x \<noteq> (0::'a); x \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> x \<noteq> y
[PROOF STEP]
using yC
[PROOF STATE]
proof (prove)
using this:
y \<in> C

goal (3 subgoals):
 1. \<And>x. \<lbrakk>y \<noteq> (0::'b); x \<in> C; x \<noteq> y; inner a x \<noteq> (0::'a); x \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> x \<in> C
 2. \<And>x. \<lbrakk>y \<noteq> (0::'b); x \<in> C; x \<noteq> y; inner a x \<noteq> (0::'a); x \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> y \<in> C
 3. \<And>x. \<lbrakk>y \<noteq> (0::'b); x \<in> C; x \<noteq> y; inner a x \<noteq> (0::'a); x \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> x \<noteq> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
orthogonal (a - proj_onto a C) y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pairwise_orthogonal_proj_set:
  assumes C: "finite C" and p: "pairwise orthogonal C"
  shows "pairwise orthogonal (insert (a - proj_onto a C) C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pairwise orthogonal (insert (a - proj_onto a C) C)
[PROOF STEP]
by (rule pairwise_orthogonal_insert[OF p], auto simp add: orthogonal_proj_set C p)


[STATEMENT]
lemma orthogonal_real_eq: "RV_inner.orthogonal = real_inner_class.orthogonal"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RV_inner.orthogonal = real_inner_class.orthogonal
[PROOF STEP]
unfolding RV_inner.orthogonal_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x y. x \<bullet> y = 0) = real_inner_class.orthogonal
[PROOF STEP]
unfolding real_inner_class.orthogonal_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x y. x \<bullet> y = 0) = (\<lambda>x y. x \<bullet> y = 0)
[PROOF STEP]
..


[STATEMENT]
lemma cnj_cnj_matrix[simp]: "(\<chi> i j. cnj ((\<chi> i j. cnj (A $ i $ j)) $ i $ j)) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i j. cnj_class.cnj ((\<chi>i j. cnj_class.cnj (A $ i $ j)) $ i $ j)) = A
[PROOF STEP]
unfolding vec_eq_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i ia. (\<chi>i j. cnj_class.cnj ((\<chi>i j. cnj_class.cnj (A $ i $ j)) $ i $ j)) $ i $ ia = A $ i $ ia
[PROOF STEP]
by auto


[STATEMENT]
lemma cnj_transpose[simp]: "(\<chi> i j. cnj (transpose A $ i $ j)) = transpose (\<chi> i j. cnj (A $ i $ j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i j. cnj_class.cnj (Finite_Cartesian_Product.transpose A $ i $ j)) = Finite_Cartesian_Product.transpose (\<chi>i j. cnj_class.cnj (A $ i $ j))
[PROOF STEP]
unfolding vec_eq_iff transpose_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i ia. (\<chi>i j. cnj_class.cnj ((\<chi>i j. A $ j $ i) $ i $ j)) $ i $ ia = (\<chi>i j. (\<chi>i j. cnj_class.cnj (A $ i $ j)) $ j $ i) $ i $ ia
[PROOF STEP]
by auto


[STATEMENT]
lemma null_space_orthogonal_complement_row_space:
  fixes A::"'a^'cols::{finite, wellorder}^'rows::{finite, wellorder}"
  shows "null_space A = COLS.v.orthogonal_complement (row_space (\<chi> i j. cnj (A $ i $ j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. null_space A = COLS.v.orthogonal_complement (row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. null_space A = COLS.v.orthogonal_complement (row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))
[PROOF STEP]
interpret m: matrix inner_rows inner_cols
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Generalizations2.matrix inner_rows inner_cols
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. null_space A = COLS.v.orthogonal_complement (row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))
[PROOF STEP]
let ?A="(\<chi> i j. cnj (A $ i $ j))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. null_space A = COLS.v.orthogonal_complement (row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. null_space A = COLS.v.orthogonal_complement (row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))
[PROOF STEP]
proof (unfold null_space_def COLS.v.orthogonal_complement_def, auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>A *v x = 0; y \<in> row_space (\<chi>i j. cnj_class.cnj (A $ i $ j))\<rbrakk> \<Longrightarrow> COLS.v.orthogonal y x
 2. \<And>x. \<forall>y\<in>row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)). COLS.v.orthogonal y x \<Longrightarrow> A *v x = 0
[PROOF STEP]
fix x xa
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>A *v x = 0; y \<in> row_space (\<chi>i j. cnj_class.cnj (A $ i $ j))\<rbrakk> \<Longrightarrow> COLS.v.orthogonal y x
 2. \<And>x. \<forall>y\<in>row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)). COLS.v.orthogonal y x \<Longrightarrow> A *v x = 0
[PROOF STEP]
assume Ax: "A *v x = 0" and xa: "xa \<in> row_space (\<chi> i j. cnj (A $ i $ j))"
[PROOF STATE]
proof (state)
this:
A *v x = 0
xa \<in> row_space (\<chi>i j. cnj_class.cnj (A $ i $ j))

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>A *v x = 0; y \<in> row_space (\<chi>i j. cnj_class.cnj (A $ i $ j))\<rbrakk> \<Longrightarrow> COLS.v.orthogonal y x
 2. \<And>x. \<forall>y\<in>row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)). COLS.v.orthogonal y x \<Longrightarrow> A *v x = 0
[PROOF STEP]
obtain y where y: "xa = transpose (\<chi> i j. cnj (A $ i $ j)) *v y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. xa = Finite_Cartesian_Product.transpose (\<chi>i j. cnj_class.cnj (A $ i $ j)) *v y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using xa
[PROOF STATE]
proof (prove)
using this:
xa \<in> row_space (\<chi>i j. cnj_class.cnj (A $ i $ j))

goal (1 subgoal):
 1. (\<And>y. xa = Finite_Cartesian_Product.transpose (\<chi>i j. cnj_class.cnj (A $ i $ j)) *v y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding row_space_eq
[PROOF STATE]
proof (prove)
using this:
xa \<in> {w. \<exists>y. Finite_Cartesian_Product.transpose (\<chi>i j. cnj_class.cnj (A $ i $ j)) *v y = w}

goal (1 subgoal):
 1. (\<And>y. xa = Finite_Cartesian_Product.transpose (\<chi>i j. cnj_class.cnj (A $ i $ j)) *v y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xa = Finite_Cartesian_Product.transpose (\<chi>i j. cnj_class.cnj (A $ i $ j)) *v y

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>A *v x = 0; y \<in> row_space (\<chi>i j. cnj_class.cnj (A $ i $ j))\<rbrakk> \<Longrightarrow> COLS.v.orthogonal y x
 2. \<And>x. \<forall>y\<in>row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)). COLS.v.orthogonal y x \<Longrightarrow> A *v x = 0
[PROOF STEP]
have y2: "y v* (\<chi> i j. cnj (A $ i $ j)) = xa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y v* (\<chi>i j. cnj_class.cnj (A $ i $ j)) = xa
[PROOF STEP]
using transpose_vector y
[PROOF STATE]
proof (prove)
using this:
?x v* ?A = Finite_Cartesian_Product.transpose ?A *v ?x
xa = Finite_Cartesian_Product.transpose (\<chi>i j. cnj_class.cnj (A $ i $ j)) *v y

goal (1 subgoal):
 1. y v* (\<chi>i j. cnj_class.cnj (A $ i $ j)) = xa
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
y v* (\<chi>i j. cnj_class.cnj (A $ i $ j)) = xa

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>A *v x = 0; y \<in> row_space (\<chi>i j. cnj_class.cnj (A $ i $ j))\<rbrakk> \<Longrightarrow> COLS.v.orthogonal y x
 2. \<And>x. \<forall>y\<in>row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)). COLS.v.orthogonal y x \<Longrightarrow> A *v x = 0
[PROOF STEP]
show "COLS.v.orthogonal xa x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. COLS.v.orthogonal xa x
[PROOF STEP]
using m.dot_lmul_matrix[of y ?A x]
[PROOF STATE]
proof (prove)
using this:
inner_cols (y v* (\<chi>i j. cnj_class.cnj (A $ i $ j))) x = inner_rows y ((\<chi>i j. cnj_class.cnj ((\<chi>i j. cnj_class.cnj (A $ i $ j)) $ i $ j)) *v x)

goal (1 subgoal):
 1. COLS.v.orthogonal xa x
[PROOF STEP]
unfolding cnj_cnj_matrix Ax ROWS.v.inner_zero_right
[PROOF STATE]
proof (prove)
using this:
inner_cols (y v* (\<chi>i j. cnj_class.cnj (A $ i $ j))) x = (0::'a)

goal (1 subgoal):
 1. COLS.v.orthogonal xa x
[PROOF STEP]
unfolding y2
[PROOF STATE]
proof (prove)
using this:
inner_cols xa x = (0::'a)

goal (1 subgoal):
 1. COLS.v.orthogonal xa x
[PROOF STEP]
unfolding COLS.v.orthogonal_def
[PROOF STATE]
proof (prove)
using this:
inner_cols xa x = (0::'a)

goal (1 subgoal):
 1. inner_cols xa x = (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
COLS.v.orthogonal xa x

goal (1 subgoal):
 1. \<And>x. \<forall>y\<in>row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)). COLS.v.orthogonal y x \<Longrightarrow> A *v x = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y\<in>row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)). COLS.v.orthogonal y x \<Longrightarrow> A *v x = 0
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y\<in>row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)). COLS.v.orthogonal y x \<Longrightarrow> A *v x = 0
[PROOF STEP]
assume xa: "\<forall>xa\<in>row_space (\<chi> i j. cnj (A $ i $ j)). COLS.v.orthogonal xa x"
[PROOF STATE]
proof (state)
this:
\<forall>xa\<in>row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)). COLS.v.orthogonal xa x

goal (1 subgoal):
 1. \<And>x. \<forall>y\<in>row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)). COLS.v.orthogonal y x \<Longrightarrow> A *v x = 0
[PROOF STEP]
show "A *v x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *v x = 0
[PROOF STEP]
using xa
[PROOF STATE]
proof (prove)
using this:
\<forall>xa\<in>row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)). COLS.v.orthogonal xa x

goal (1 subgoal):
 1. A *v x = 0
[PROOF STEP]
unfolding row_space_eq COLS.v.orthogonal_def
[PROOF STATE]
proof (prove)
using this:
\<forall>xa\<in>{w. \<exists>y. Finite_Cartesian_Product.transpose (\<chi>i j. cnj_class.cnj (A $ i $ j)) *v y = w}. inner_cols xa x = (0::'a)

goal (1 subgoal):
 1. A *v x = 0
[PROOF STEP]
using COLS.v.inner_eq_zero_iff
[PROOF STATE]
proof (prove)
using this:
\<forall>xa\<in>{w. \<exists>y. Finite_Cartesian_Product.transpose (\<chi>i j. cnj_class.cnj (A $ i $ j)) *v y = w}. inner_cols xa x = (0::'a)
(inner_cols ?x ?x = (0::'a)) = (?x = 0)

goal (1 subgoal):
 1. A *v x = 0
[PROOF STEP]
using m.dot_lmul_matrix[of _ ?A]
[PROOF STATE]
proof (prove)
using this:
\<forall>xa\<in>{w. \<exists>y. Finite_Cartesian_Product.transpose (\<chi>i j. cnj_class.cnj (A $ i $ j)) *v y = w}. inner_cols xa x = (0::'a)
(inner_cols ?x ?x = (0::'a)) = (?x = 0)
inner_cols (?x v* (\<chi>i j. cnj_class.cnj (A $ i $ j))) ?y = inner_rows ?x ((\<chi>i j. cnj_class.cnj ((\<chi>i j. cnj_class.cnj (A $ i $ j)) $ i $ j)) *v ?y)

goal (1 subgoal):
 1. A *v x = 0
[PROOF STEP]
unfolding transpose_vector
[PROOF STATE]
proof (prove)
using this:
\<forall>xa\<in>{w. \<exists>y. Finite_Cartesian_Product.transpose (\<chi>i j. cnj_class.cnj (A $ i $ j)) *v y = w}. inner_cols xa x = (0::'a)
(inner_cols ?x ?x = (0::'a)) = (?x = 0)
inner_cols (Finite_Cartesian_Product.transpose (\<chi>i j. cnj_class.cnj (A $ i $ j)) *v ?x) ?y = inner_rows ?x ((\<chi>i j. cnj_class.cnj ((\<chi>i j. cnj_class.cnj (A $ i $ j)) $ i $ j)) *v ?y)

goal (1 subgoal):
 1. A *v x = 0
[PROOF STEP]
by auto
       (metis ROWS.i4 m.cnj_cnj_matrix m.dot_lmul_matrix transpose_vector)
[PROOF STATE]
proof (state)
this:
A *v x = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
null_space A = COLS.v.orthogonal_complement (row_space (\<chi>i j. cnj_class.cnj (A $ i $ j)))

goal:
No subgoals!
[PROOF STEP]
qed