[STATEMENT]
lemma preregister_mult_right: \<open>clinear (\<lambda>a. a o\<^sub>C\<^sub>L z)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear (\<lambda>a. a o\<^sub>C\<^sub>L z)
[PROOF STEP]
by (simp add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose clinearI)


[STATEMENT]
lemma preregister_mult_left: \<open>clinear (\<lambda>a. z o\<^sub>C\<^sub>L a)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear ((o\<^sub>C\<^sub>L) z)
[PROOF STEP]
by (meson cbilinear_cblinfun_compose cbilinear_def)


[STATEMENT]
lemma register_of_id: \<open>register F \<Longrightarrow> F id_cblinfun = id_cblinfun\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. register F \<Longrightarrow> F id_cblinfun = id_cblinfun
[PROOF STEP]
by (simp add: register_def)


[STATEMENT]
lemma register_id: \<open>register id\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. register id
[PROOF STEP]
by (simp add: register_def complex_vector.module_hom_id)


[STATEMENT]
lemma register_preregister: "register F \<Longrightarrow> clinear F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. register F \<Longrightarrow> clinear F
[PROOF STEP]
unfolding register_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear F \<and> F id_cblinfun = id_cblinfun \<and> (\<forall>a b. F (a o\<^sub>C\<^sub>L b) = F a o\<^sub>C\<^sub>L F b) \<and> (\<forall>a. F (a*) = F a*) \<Longrightarrow> clinear F
[PROOF STEP]
by simp


[STATEMENT]
lemma register_comp: "register F \<Longrightarrow> register G \<Longrightarrow> register (G \<circ> F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>register F; register G\<rbrakk> \<Longrightarrow> register (G \<circ> F)
[PROOF STEP]
unfolding register_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>clinear F \<and> F id_cblinfun = id_cblinfun \<and> (\<forall>a b. F (a o\<^sub>C\<^sub>L b) = F a o\<^sub>C\<^sub>L F b) \<and> (\<forall>a. F (a*) = F a*); clinear G \<and> G id_cblinfun = id_cblinfun \<and> (\<forall>a b. G (a o\<^sub>C\<^sub>L b) = G a o\<^sub>C\<^sub>L G b) \<and> (\<forall>a. G (a*) = G a*)\<rbrakk> \<Longrightarrow> clinear (G \<circ> F) \<and> (G \<circ> F) id_cblinfun = id_cblinfun \<and> (\<forall>a b. (G \<circ> F) (a o\<^sub>C\<^sub>L b) = (G \<circ> F) a o\<^sub>C\<^sub>L (G \<circ> F) b) \<and> (\<forall>a. (G \<circ> F) (a*) = (G \<circ> F) a*)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>clinear F; clinear G; F id_cblinfun = id_cblinfun; G id_cblinfun = id_cblinfun; \<forall>a b. F (a o\<^sub>C\<^sub>L b) = F a o\<^sub>C\<^sub>L F b; \<forall>a. F (a*) = F a*; \<forall>a b. G (a o\<^sub>C\<^sub>L b) = G a o\<^sub>C\<^sub>L G b; \<forall>a. G (a*) = G a*\<rbrakk> \<Longrightarrow> clinear (G \<circ> F)
[PROOF STEP]
using clinear_compose
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>clinear ?f; clinear ?g\<rbrakk> \<Longrightarrow> clinear (?g \<circ> ?f)

goal (1 subgoal):
 1. \<lbrakk>clinear F; clinear G; F id_cblinfun = id_cblinfun; G id_cblinfun = id_cblinfun; \<forall>a b. F (a o\<^sub>C\<^sub>L b) = F a o\<^sub>C\<^sub>L F b; \<forall>a. F (a*) = F a*; \<forall>a b. G (a o\<^sub>C\<^sub>L b) = G a o\<^sub>C\<^sub>L G b; \<forall>a. G (a*) = G a*\<rbrakk> \<Longrightarrow> clinear (G \<circ> F)
[PROOF STEP]
by blast


[STATEMENT]
lemma register_mult: "register F \<Longrightarrow> cblinfun_compose (F a) (F b) = F (cblinfun_compose a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. register F \<Longrightarrow> F a o\<^sub>C\<^sub>L F b = F (a o\<^sub>C\<^sub>L b)
[PROOF STEP]
unfolding register_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear F \<and> F id_cblinfun = id_cblinfun \<and> (\<forall>a b. F (a o\<^sub>C\<^sub>L b) = F a o\<^sub>C\<^sub>L F b) \<and> (\<forall>a. F (a*) = F a*) \<Longrightarrow> F a o\<^sub>C\<^sub>L F b = F (a o\<^sub>C\<^sub>L b)
[PROOF STEP]
by auto


[STATEMENT]
lemma register_tensor_left: \<open>register (\<lambda>a. tensor_op a id_cblinfun)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. register (\<lambda>a. a \<otimes>\<^sub>o id_cblinfun)
[PROOF STEP]
by (simp add: comp_tensor_op register_def tensor_op_cbilinear tensor_op_adjoint)


[STATEMENT]
lemma register_tensor_right: \<open>register (\<lambda>a. tensor_op id_cblinfun a)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. register ((\<otimes>\<^sub>o) id_cblinfun)
[PROOF STEP]
by (simp add: comp_tensor_op register_def tensor_op_cbilinear tensor_op_adjoint)


[STATEMENT]
lemma cbilinear_F_comp_G[simp]: \<open>clinear F \<Longrightarrow> clinear G \<Longrightarrow> cbilinear (\<lambda>a b. F a o\<^sub>C\<^sub>L G b)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>clinear F; clinear G\<rbrakk> \<Longrightarrow> cbilinear (\<lambda>a b. F a o\<^sub>C\<^sub>L G b)
[PROOF STEP]
unfolding cbilinear_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>clinear F; clinear G\<rbrakk> \<Longrightarrow> (\<forall>y. clinear (\<lambda>x. F x o\<^sub>C\<^sub>L G y)) \<and> (\<forall>x. clinear (\<lambda>b. F x o\<^sub>C\<^sub>L G b))
[PROOF STEP]
by (auto simp add: clinear_iff bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose bounded_cbilinear.add_right)


[STATEMENT]
lemma register_pair_apply:
  assumes [simp]: \<open>register F\<close> \<open>register G\<close>
  assumes \<open>\<And>a b. F a o\<^sub>C\<^sub>L G b = G b o\<^sub>C\<^sub>L F a\<close>
  shows \<open>(register_pair F G) (tensor_op a b) = F a o\<^sub>C\<^sub>L G b\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. register_pair F G (a \<otimes>\<^sub>o b) = F a o\<^sub>C\<^sub>L G b
[PROOF STEP]
unfolding register_pair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if register F \<and> register G \<and> (\<forall>a b. F a o\<^sub>C\<^sub>L G b = G b o\<^sub>C\<^sub>L F a) then tensor_lift (\<lambda>a b. F a o\<^sub>C\<^sub>L G b) else (\<lambda>_. 0)) (a \<otimes>\<^sub>o b) = F a o\<^sub>C\<^sub>L G b
[PROOF STEP]
apply (simp flip: assms(3))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_lift (\<lambda>a b. F a o\<^sub>C\<^sub>L G b) (a \<otimes>\<^sub>o b) = F a o\<^sub>C\<^sub>L G b
[PROOF STEP]
by (metis assms(1) assms(2) cbilinear_F_comp_G register_preregister tensor_lift_correct)


[STATEMENT]
lemma register_pair_is_register:
  fixes F :: \<open>'a::finite update \<Rightarrow> 'c::finite update\<close> and G
  assumes [simp]: \<open>register F\<close> and [simp]: \<open>register G\<close>
  assumes \<open>\<And>a b. F a o\<^sub>C\<^sub>L G b = G b o\<^sub>C\<^sub>L F a\<close>
  shows \<open>register (register_pair F G)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. register (register_pair F G)
[PROOF STEP]
proof (unfold register_def, intro conjI allI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. clinear (register_pair F G)
 2. register_pair F G id_cblinfun = id_cblinfun
 3. \<And>a b. register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b
 4. \<And>a. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
have [simp]: \<open>clinear F\<close> \<open>clinear G\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear F &&& clinear G
[PROOF STEP]
using assms register_def
[PROOF STATE]
proof (prove)
using this:
register F
register G
F ?a o\<^sub>C\<^sub>L G ?b = G ?b o\<^sub>C\<^sub>L F ?a
register ?F = (clinear ?F \<and> ?F id_cblinfun = id_cblinfun \<and> (\<forall>a b. ?F (a o\<^sub>C\<^sub>L b) = ?F a o\<^sub>C\<^sub>L ?F b) \<and> (\<forall>a. ?F (a*) = ?F a*))

goal (1 subgoal):
 1. clinear F &&& clinear G
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
clinear F
clinear G

goal (4 subgoals):
 1. clinear (register_pair F G)
 2. register_pair F G id_cblinfun = id_cblinfun
 3. \<And>a b. register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b
 4. \<And>a. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
have [simp]: \<open>F id_cblinfun = id_cblinfun\<close> \<open>G id_cblinfun = id_cblinfun\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F id_cblinfun = id_cblinfun &&& G id_cblinfun = id_cblinfun
[PROOF STEP]
using assms(1,2) register_def
[PROOF STATE]
proof (prove)
using this:
register F
register G
register ?F = (clinear ?F \<and> ?F id_cblinfun = id_cblinfun \<and> (\<forall>a b. ?F (a o\<^sub>C\<^sub>L b) = ?F a o\<^sub>C\<^sub>L ?F b) \<and> (\<forall>a. ?F (a*) = ?F a*))

goal (1 subgoal):
 1. F id_cblinfun = id_cblinfun &&& G id_cblinfun = id_cblinfun
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
F id_cblinfun = id_cblinfun
G id_cblinfun = id_cblinfun

goal (4 subgoals):
 1. clinear (register_pair F G)
 2. register_pair F G id_cblinfun = id_cblinfun
 3. \<And>a b. register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b
 4. \<And>a. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
show [simp]: \<open>clinear (register_pair F G)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear (register_pair F G)
[PROOF STEP]
unfolding register_pair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear (if register F \<and> register G \<and> (\<forall>a b. F a o\<^sub>C\<^sub>L G b = G b o\<^sub>C\<^sub>L F a) then tensor_lift (\<lambda>a b. F a o\<^sub>C\<^sub>L G b) else (\<lambda>_. 0))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
register F
register G
F ?a o\<^sub>C\<^sub>L G ?b = G ?b o\<^sub>C\<^sub>L F ?a

goal (1 subgoal):
 1. clinear (if register F \<and> register G \<and> (\<forall>a b. F a o\<^sub>C\<^sub>L G b = G b o\<^sub>C\<^sub>L F a) then tensor_lift (\<lambda>a b. F a o\<^sub>C\<^sub>L G b) else (\<lambda>_. 0))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. F a o\<^sub>C\<^sub>L G b = G b o\<^sub>C\<^sub>L F a) \<Longrightarrow> clinear (tensor_lift (\<lambda>a b. G b o\<^sub>C\<^sub>L F a))
[PROOF STEP]
apply (rule tensor_lift_clinear)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. F a o\<^sub>C\<^sub>L G b = G b o\<^sub>C\<^sub>L F a) \<Longrightarrow> cbilinear (\<lambda>a b. G b o\<^sub>C\<^sub>L F a)
[PROOF STEP]
by (simp flip: assms(3))
[PROOF STATE]
proof (state)
this:
clinear (register_pair F G)

goal (3 subgoals):
 1. register_pair F G id_cblinfun = id_cblinfun
 2. \<And>a b. register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b
 3. \<And>a. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
show \<open>register_pair F G id_cblinfun = id_cblinfun\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. register_pair F G id_cblinfun = id_cblinfun
[PROOF STEP]
apply (simp flip: tensor_id)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. register_pair F G (id_cblinfun \<otimes>\<^sub>o id_cblinfun) = id_cblinfun
[PROOF STEP]
apply (subst register_pair_apply)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. register F
 2. register G
 3. \<And>a b. F a o\<^sub>C\<^sub>L G b = G b o\<^sub>C\<^sub>L F a
 4. F id_cblinfun o\<^sub>C\<^sub>L G id_cblinfun = id_cblinfun
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
register F
register G
F ?a o\<^sub>C\<^sub>L G ?b = G ?b o\<^sub>C\<^sub>L F ?a

goal (4 subgoals):
 1. register F
 2. register G
 3. \<And>a b. F a o\<^sub>C\<^sub>L G b = G b o\<^sub>C\<^sub>L F a
 4. F id_cblinfun o\<^sub>C\<^sub>L G id_cblinfun = id_cblinfun
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
register_pair F G id_cblinfun = id_cblinfun

goal (2 subgoals):
 1. \<And>a b. register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b
 2. \<And>a. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
have [simp]: \<open>clinear (\<lambda>y. register_pair F G (x o\<^sub>C\<^sub>L y))\<close> for x :: \<open>('a\<times>'b) update\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear (\<lambda>y. register_pair F G (x o\<^sub>C\<^sub>L y))
[PROOF STEP]
apply (rule clinear_compose[unfolded o_def, where g=\<open>register_pair F G\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. clinear ((o\<^sub>C\<^sub>L) x)
 2. clinear (register_pair F G)
[PROOF STEP]
by (simp_all add: preregister_mult_left bounded_cbilinear.add_right clinearI)
[PROOF STATE]
proof (state)
this:
clinear (\<lambda>y. register_pair F G (?x o\<^sub>C\<^sub>L y))

goal (2 subgoals):
 1. \<And>a b. register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b
 2. \<And>a. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
have [simp]: \<open>clinear (\<lambda>y. x o\<^sub>C\<^sub>L register_pair F G y)\<close> for x :: \<open>'c update\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear (\<lambda>y. x o\<^sub>C\<^sub>L register_pair F G y)
[PROOF STEP]
apply (rule clinear_compose[unfolded o_def, where f=\<open>register_pair F G\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. clinear (register_pair F G)
 2. clinear ((o\<^sub>C\<^sub>L) x)
[PROOF STEP]
by (simp_all add: preregister_mult_left bounded_cbilinear.add_right clinearI)
[PROOF STATE]
proof (state)
this:
clinear (\<lambda>y. ?x o\<^sub>C\<^sub>L register_pair F G y)

goal (2 subgoals):
 1. \<And>a b. register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b
 2. \<And>a. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
have [simp]: \<open>clinear (\<lambda>x. register_pair F G (x o\<^sub>C\<^sub>L y))\<close> for y :: \<open>('a\<times>'b) update\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear (\<lambda>x. register_pair F G (x o\<^sub>C\<^sub>L y))
[PROOF STEP]
apply (rule clinear_compose[unfolded o_def, where g=\<open>register_pair F G\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. clinear (\<lambda>x. x o\<^sub>C\<^sub>L y)
 2. clinear (register_pair F G)
[PROOF STEP]
by (simp_all add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose clinearI)
[PROOF STATE]
proof (state)
this:
clinear (\<lambda>x. register_pair F G (x o\<^sub>C\<^sub>L ?y))

goal (2 subgoals):
 1. \<And>a b. register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b
 2. \<And>a. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
have [simp]: \<open>clinear (\<lambda>x. register_pair F G x o\<^sub>C\<^sub>L y)\<close> for y :: \<open>'c update\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear (\<lambda>x. register_pair F G x o\<^sub>C\<^sub>L y)
[PROOF STEP]
apply (rule clinear_compose[unfolded o_def, where f=\<open>register_pair F G\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. clinear (register_pair F G)
 2. clinear (\<lambda>a. a o\<^sub>C\<^sub>L y)
[PROOF STEP]
by (simp_all add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose clinearI)
[PROOF STATE]
proof (state)
this:
clinear (\<lambda>x. register_pair F G x o\<^sub>C\<^sub>L ?y)

goal (2 subgoals):
 1. \<And>a b. register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b
 2. \<And>a. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
have [simp]: \<open>F (x o\<^sub>C\<^sub>L y) = F x o\<^sub>C\<^sub>L F y\<close> for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F (x o\<^sub>C\<^sub>L y) = F x o\<^sub>C\<^sub>L F y
[PROOF STEP]
by (simp add: register_mult)
[PROOF STATE]
proof (state)
this:
F (?x o\<^sub>C\<^sub>L ?y) = F ?x o\<^sub>C\<^sub>L F ?y

goal (2 subgoals):
 1. \<And>a b. register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b
 2. \<And>a. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
have [simp]: \<open>G (x o\<^sub>C\<^sub>L y) = G x o\<^sub>C\<^sub>L G y\<close> for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G (x o\<^sub>C\<^sub>L y) = G x o\<^sub>C\<^sub>L G y
[PROOF STEP]
by (simp add: register_mult)
[PROOF STATE]
proof (state)
this:
G (?x o\<^sub>C\<^sub>L ?y) = G ?x o\<^sub>C\<^sub>L G ?y

goal (2 subgoals):
 1. \<And>a b. register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b
 2. \<And>a. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
have [simp]: \<open>clinear (\<lambda>a. (register_pair F G (a*))*)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear (\<lambda>a. register_pair F G (a*)*)
[PROOF STEP]
apply (rule antilinear_o_antilinear[unfolded o_def, where f=\<open>adj\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. antilinear adj
 2. antilinear (\<lambda>a. register_pair F G a*)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. antilinear (\<lambda>a. register_pair F G a*)
[PROOF STEP]
apply (rule antilinear_o_clinear[unfolded o_def, where g=\<open>adj\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. clinear (register_pair F G)
 2. antilinear adj
[PROOF STEP]
by (simp_all)
[PROOF STATE]
proof (state)
this:
clinear (\<lambda>a. register_pair F G (a*)*)

goal (2 subgoals):
 1. \<And>a b. register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b
 2. \<And>a. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
have [simp]: \<open>F (a*) = (F a)*\<close> for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F (a*) = F a*
[PROOF STEP]
using assms(1) register_def
[PROOF STATE]
proof (prove)
using this:
register F
register ?F = (clinear ?F \<and> ?F id_cblinfun = id_cblinfun \<and> (\<forall>a b. ?F (a o\<^sub>C\<^sub>L b) = ?F a o\<^sub>C\<^sub>L ?F b) \<and> (\<forall>a. ?F (a*) = ?F a*))

goal (1 subgoal):
 1. F (a*) = F a*
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
F (?a*) = F ?a*

goal (2 subgoals):
 1. \<And>a b. register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b
 2. \<And>a. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
have [simp]: \<open>G (b*) = (G b)*\<close> for b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G (b*) = G b*
[PROOF STEP]
using assms(2) register_def
[PROOF STATE]
proof (prove)
using this:
register G
register ?F = (clinear ?F \<and> ?F id_cblinfun = id_cblinfun \<and> (\<forall>a b. ?F (a o\<^sub>C\<^sub>L b) = ?F a o\<^sub>C\<^sub>L ?F b) \<and> (\<forall>a. ?F (a*) = ?F a*))

goal (1 subgoal):
 1. G (b*) = G b*
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
G (?b*) = G ?b*

goal (2 subgoals):
 1. \<And>a b. register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b
 2. \<And>a. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b
 2. \<And>a. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
show \<open>register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b
[PROOF STEP]
apply (rule tensor_extensionality[THEN fun_cong, where x=b], simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b. register_pair F G (a o\<^sub>C\<^sub>L aa \<otimes>\<^sub>o b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G (aa \<otimes>\<^sub>o b)
[PROOF STEP]
apply (rule tensor_extensionality[THEN fun_cong, where x=a], simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. register_pair F G (aa \<otimes>\<^sub>o ba o\<^sub>C\<^sub>L a \<otimes>\<^sub>o b) = register_pair F G (aa \<otimes>\<^sub>o ba) o\<^sub>C\<^sub>L register_pair F G (a \<otimes>\<^sub>o b)
[PROOF STEP]
apply (simp_all add: comp_tensor_op register_pair_apply assms(3))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. F aa o\<^sub>C\<^sub>L F a o\<^sub>C\<^sub>L (G ba o\<^sub>C\<^sub>L G b) = G ba o\<^sub>C\<^sub>L F aa o\<^sub>C\<^sub>L (G b o\<^sub>C\<^sub>L F a)
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
F ?a o\<^sub>C\<^sub>L G ?b = G ?b o\<^sub>C\<^sub>L F ?a

goal (1 subgoal):
 1. \<And>a b aa ba. F aa o\<^sub>C\<^sub>L F a o\<^sub>C\<^sub>L (G ba o\<^sub>C\<^sub>L G b) = G ba o\<^sub>C\<^sub>L F aa o\<^sub>C\<^sub>L (G b o\<^sub>C\<^sub>L F a)
[PROOF STEP]
by (metis cblinfun_compose_assoc)
[PROOF STATE]
proof (state)
this:
register_pair F G (a o\<^sub>C\<^sub>L b) = register_pair F G a o\<^sub>C\<^sub>L register_pair F G b

goal (1 subgoal):
 1. \<And>a. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
have \<open>(register_pair F G (a*))* = register_pair F G a\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. register_pair F G (a*)* = register_pair F G a
[PROOF STEP]
apply (rule tensor_extensionality[THEN fun_cong, where x=a])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. clinear (\<lambda>a. register_pair F G (a*)*)
 2. clinear (register_pair F G)
 3. \<And>a b. register_pair F G ((a \<otimes>\<^sub>o b)*)* = register_pair F G (a \<otimes>\<^sub>o b)
[PROOF STEP]
by (simp_all add: tensor_op_adjoint register_pair_apply assms(3))
[PROOF STATE]
proof (state)
this:
register_pair F G (a*)* = register_pair F G a

goal (1 subgoal):
 1. \<And>a. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
register_pair F G (a*)* = register_pair F G a
[PROOF STEP]
show \<open>register_pair F G (a*) = register_pair F G a*\<close>
[PROOF STATE]
proof (prove)
using this:
register_pair F G (a*)* = register_pair F G a

goal (1 subgoal):
 1. register_pair F G (a*) = register_pair F G a*
[PROOF STEP]
by (metis double_adj)
[PROOF STATE]
proof (state)
this:
register_pair F G (a*) = register_pair F G a*

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rref_id_implies_invertible:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
assumes Gauss_mat_1: "Gauss_Jordan A = mat 1"
shows "invertible A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invertible A
[PROOF STEP]
obtain P where P: "invertible P" and PA: "Gauss_Jordan A = P ** A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrakk>invertible P; Gauss_Jordan A = P ** A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using invertible_Gauss_Jordan[of A]
[PROOF STATE]
proof (prove)
using this:
\<exists>P. invertible P \<and> Gauss_Jordan A = P ** A

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>invertible P; Gauss_Jordan A = P ** A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
invertible P
Gauss_Jordan A = P ** A

goal (1 subgoal):
 1. invertible A
[PROOF STEP]
have "A = mat 1 ** A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = mat (1::'a) ** A
[PROOF STEP]
unfolding matrix_mul_lid
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = A
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
A = mat (1::'a) ** A

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

goal (1 subgoal):
 1. invertible A
[PROOF STEP]
have "... = (matrix_inv P ** P) ** A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (1::'a) ** A = matrix_inv P ** P ** A
[PROOF STEP]
using P invertible_def matrix_inv_unique
[PROOF STATE]
proof (prove)
using this:
invertible P
invertible ?A = (\<exists>A'. ?A ** A' = mat (1::?'a) \<and> A' ** ?A = mat (1::?'a))
\<lbrakk>?A ** ?B = mat (1::?'a); ?B ** ?A = mat (1::?'a)\<rbrakk> \<Longrightarrow> matrix_inv ?A = ?B

goal (1 subgoal):
 1. mat (1::'a) ** A = matrix_inv P ** P ** A
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
mat (1::'a) ** A = matrix_inv P ** P ** A

goal (1 subgoal):
 1. invertible A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mat (1::'a) ** A = matrix_inv P ** P ** A

goal (1 subgoal):
 1. invertible A
[PROOF STEP]
have "... = (matrix_inv P) ** (P ** A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_inv P ** P ** A = matrix_inv P ** (P ** A)
[PROOF STEP]
by (metis PA assms calculation matrix_eq matrix_vector_mul_assoc matrix_vector_mul_lid)
[PROOF STATE]
proof (state)
this:
matrix_inv P ** P ** A = matrix_inv P ** (P ** A)

goal (1 subgoal):
 1. invertible A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
matrix_inv P ** P ** A = matrix_inv P ** (P ** A)

goal (1 subgoal):
 1. invertible A
[PROOF STEP]
have "... = (matrix_inv P) ** mat 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_inv P ** (P ** A) = matrix_inv P ** mat (1::'a)
[PROOF STEP]
unfolding PA[symmetric] Gauss_mat_1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_inv P ** mat (1::'a) = matrix_inv P ** mat (1::'a)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
matrix_inv P ** (P ** A) = matrix_inv P ** mat (1::'a)

goal (1 subgoal):
 1. invertible A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
matrix_inv P ** (P ** A) = matrix_inv P ** mat (1::'a)

goal (1 subgoal):
 1. invertible A
[PROOF STEP]
have "... = (matrix_inv P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_inv P ** mat (1::'a) = matrix_inv P
[PROOF STEP]
unfolding matrix_mul_rid
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_inv P = matrix_inv P
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
matrix_inv P ** mat (1::'a) = matrix_inv P

goal (1 subgoal):
 1. invertible A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A = matrix_inv P
[PROOF STEP]
have "A = (matrix_inv P)"
[PROOF STATE]
proof (prove)
using this:
A = matrix_inv P

goal (1 subgoal):
 1. A = matrix_inv P
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A = matrix_inv P

goal (1 subgoal):
 1. invertible A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A = matrix_inv P

goal (1 subgoal):
 1. invertible A
[PROOF STEP]
using P
[PROOF STATE]
proof (prove)
using this:
A = matrix_inv P
invertible P

goal (1 subgoal):
 1. invertible A
[PROOF STEP]
unfolding invertible_def
[PROOF STATE]
proof (prove)
using this:
A = matrix_inv P
\<exists>A'. P ** A' = mat (1::'a) \<and> A' ** P = mat (1::'a)

goal (1 subgoal):
 1. \<exists>A'. A ** A' = mat (1::'a) \<and> A' ** A = mat (1::'a)
[PROOF STEP]
using matrix_inv_unique
[PROOF STATE]
proof (prove)
using this:
A = matrix_inv P
\<exists>A'. P ** A' = mat (1::'a) \<and> A' ** P = mat (1::'a)
\<lbrakk>?A ** ?B = mat (1::?'a); ?B ** ?A = mat (1::?'a)\<rbrakk> \<Longrightarrow> matrix_inv ?A = ?B

goal (1 subgoal):
 1. \<exists>A'. A ** A' = mat (1::'a) \<and> A' ** A = mat (1::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
invertible A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma full_rank_implies_invertible:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
assumes rank_n: "rank A = nrows A"
shows "invertible A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible A
[PROOF STEP]
proof (unfold invertible_left_inverse[of A] matrix_left_invertible_ker, clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. A *v x = 0 \<Longrightarrow> x = 0
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. A *v x = 0 \<Longrightarrow> x = 0
[PROOF STEP]
assume Ax: "A *v x = 0"
[PROOF STATE]
proof (state)
this:
A *v x = 0

goal (1 subgoal):
 1. \<And>x. A *v x = 0 \<Longrightarrow> x = 0
[PROOF STEP]
have rank_eq_card_n: "rank A = CARD('n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A = CARD('n)
[PROOF STEP]
using rank_n
[PROOF STATE]
proof (prove)
using this:
rank A = nrows A

goal (1 subgoal):
 1. rank A = CARD('n)
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
rank A = CARD('n)

goal (1 subgoal):
 1. rank A = CARD('n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
rank A = CARD('n)

goal (1 subgoal):
 1. \<And>x. A *v x = 0 \<Longrightarrow> x = 0
[PROOF STEP]
have "vec.dim (null_space A)=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.dim (null_space A) = 0
[PROOF STEP]
unfolding dim_null_space
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_dimensional_vector_space.dimension cart_basis - rank A = 0
[PROOF STEP]
unfolding rank_eq_card_n dimension_vector
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('n) - CARD('n) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vec.dim (null_space A) = 0

goal (1 subgoal):
 1. \<And>x. A *v x = 0 \<Longrightarrow> x = 0
[PROOF STEP]
hence "null_space A = {0}"
[PROOF STATE]
proof (prove)
using this:
vec.dim (null_space A) = 0

goal (1 subgoal):
 1. null_space A = {0}
[PROOF STEP]
using vec.dim_zero_eq
[PROOF STATE]
proof (prove)
using this:
vec.dim (null_space A) = 0
vec.dim ?A = 0 \<Longrightarrow> ?A = {} \<or> ?A = {0}

goal (1 subgoal):
 1. null_space A = {0}
[PROOF STEP]
using Ax null_space_def
[PROOF STATE]
proof (prove)
using this:
vec.dim (null_space A) = 0
vec.dim ?A = 0 \<Longrightarrow> ?A = {} \<or> ?A = {0}
A *v x = 0
null_space ?A = {x. ?A *v x = 0}

goal (1 subgoal):
 1. null_space A = {0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
null_space A = {0}

goal (1 subgoal):
 1. \<And>x. A *v x = 0 \<Longrightarrow> x = 0
[PROOF STEP]
thus "x = 0"
[PROOF STATE]
proof (prove)
using this:
null_space A = {0}

goal (1 subgoal):
 1. x = 0
[PROOF STEP]
unfolding null_space_def
[PROOF STATE]
proof (prove)
using this:
{x. A *v x = 0} = {0}

goal (1 subgoal):
 1. x = 0
[PROOF STEP]
using Ax
[PROOF STATE]
proof (prove)
using this:
{x. A *v x = 0} = {0}
A *v x = 0

goal (1 subgoal):
 1. x = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invertible_implies_full_rank:
  fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
  assumes inv_A: "invertible A"
  shows "rank A = nrows A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A = nrows A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank A = nrows A
[PROOF STEP]
have "(\<forall>x. A *v x = 0 \<longrightarrow> x = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. A *v x = 0 \<longrightarrow> x = 0
[PROOF STEP]
using inv_A
[PROOF STATE]
proof (prove)
using this:
invertible A

goal (1 subgoal):
 1. \<forall>x. A *v x = 0 \<longrightarrow> x = 0
[PROOF STEP]
unfolding  invertible_left_inverse[unfolded matrix_left_invertible_ker]
[PROOF STATE]
proof (prove)
using this:
\<forall>x. A *v x = 0 \<longrightarrow> x = 0

goal (1 subgoal):
 1. \<forall>x. A *v x = 0 \<longrightarrow> x = 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<forall>x. A *v x = 0 \<longrightarrow> x = 0

goal (1 subgoal):
 1. rank A = nrows A
[PROOF STEP]
hence null_space_eq_0: "(null_space A) = {0}"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. A *v x = 0 \<longrightarrow> x = 0

goal (1 subgoal):
 1. null_space A = {0}
[PROOF STEP]
unfolding null_space_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. A *v x = 0 \<longrightarrow> x = 0

goal (1 subgoal):
 1. {x. A *v x = 0} = {0}
[PROOF STEP]
using matrix_vector_mult_0_right
[PROOF STATE]
proof (prove)
using this:
\<forall>x. A *v x = 0 \<longrightarrow> x = 0
?A *v 0 = 0

goal (1 subgoal):
 1. {x. A *v x = 0} = {0}
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
null_space A = {0}

goal (1 subgoal):
 1. rank A = nrows A
[PROOF STEP]
have dim_null_space: "vec.dim (null_space A) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.dim (null_space A) = 0
[PROOF STEP]
unfolding vec.dim_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<exists>b. vec.independent b \<and> vec.span b = vec.span (null_space A) then card (SOME b. vec.independent b \<and> vec.span b = vec.span (null_space A)) else 0) = 0
[PROOF STEP]
by (metis (no_types) null_space_eq_0 vec.dim_def vec.dim_zero_eq')
[PROOF STATE]
proof (state)
this:
vec.dim (null_space A) = 0

goal (1 subgoal):
 1. rank A = nrows A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A = nrows A
[PROOF STEP]
using rank_nullity_theorem_matrices[of A]
[PROOF STATE]
proof (prove)
using this:
ncols A = vec.dim (null_space A) + vec.dim (col_space A)

goal (1 subgoal):
 1. rank A = nrows A
[PROOF STEP]
unfolding dim_null_space rank_eq_dim_col_space nrows_def
[PROOF STATE]
proof (prove)
using this:
ncols A = 0 + vec.dim (col_space A)

goal (1 subgoal):
 1. vec.dim (col_space A) = CARD('n)
[PROOF STEP]
unfolding col_space_eq
[PROOF STATE]
proof (prove)
using this:
ncols A = 0 + vec.dim {y. \<exists>x. A *v x = y}

goal (1 subgoal):
 1. vec.dim {y. \<exists>x. A *v x = y} = CARD('n)
[PROOF STEP]
unfolding ncols_def
[PROOF STATE]
proof (prove)
using this:
CARD('n) = 0 + vec.dim {y. \<exists>x. A *v x = y}

goal (1 subgoal):
 1. vec.dim {y. \<exists>x. A *v x = y} = CARD('n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rank A = nrows A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma id_upt_nrows_mat_1:
assumes "id_upt_k A (nrows A)"
shows "A = mat 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = mat (1::'a)
[PROOF STEP]
unfolding mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = (\<chi>i j. if i = j then 1::'a else (0::'a))
[PROOF STEP]
apply vector
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i ia. (i = ia \<longrightarrow> A $ ia $ ia = (1::'a)) \<and> (i \<noteq> ia \<longrightarrow> A $ i $ ia = (0::'a))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
id_upt_k A (nrows A)

goal (1 subgoal):
 1. \<forall>i ia. (i = ia \<longrightarrow> A $ ia $ ia = (1::'a)) \<and> (i \<noteq> ia \<longrightarrow> A $ i $ ia = (0::'a))
[PROOF STEP]
unfolding id_upt_k_def nrows_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. mod_type_class.to_nat i < CARD('b) \<and> mod_type_class.to_nat j < CARD('b) \<longrightarrow> (i = j \<longrightarrow> A $ i $ j = (1::'a)) \<and> (i \<noteq> j \<longrightarrow> A $ i $ j = (0::'a))

goal (1 subgoal):
 1. \<forall>i ia. (i = ia \<longrightarrow> A $ ia $ ia = (1::'a)) \<and> (i \<noteq> ia \<longrightarrow> A $ i $ ia = (0::'a))
[PROOF STEP]
using to_nat_less_card[where ?'a='b]
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. mod_type_class.to_nat i < CARD('b) \<and> mod_type_class.to_nat j < CARD('b) \<longrightarrow> (i = j \<longrightarrow> A $ i $ j = (1::'a)) \<and> (i \<noteq> j \<longrightarrow> A $ i $ j = (0::'a))
mod_type_class.to_nat ?j < CARD('b)

goal (1 subgoal):
 1. \<forall>i ia. (i = ia \<longrightarrow> A $ ia $ ia = (1::'a)) \<and> (i \<noteq> ia \<longrightarrow> A $ i $ ia = (0::'a))
[PROOF STEP]
by presburger