[STATEMENT]
lemma cspan_range_ket_finite[simp]: "cspan (range ket :: 'a::finite ell2 set) = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cspan (range ket) = UNIV
[PROOF STEP]
by (metis closed_cspan_range_ket closure_finite_cspan finite_class.finite_UNIV finite_imageI)


[STATEMENT]
lemma canonical_basis_length_ell2[code_unfold, simp]:
  "length (canonical_basis ::'a::enum ell2 list) = CARD('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length canonical_basis = CARD('a)
[PROOF STEP]
unfolding canonical_basis_ell2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map ket enum_class.enum) = CARD('a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length enum_class.enum = CARD('a)
[PROOF STEP]
using card_UNIV_length_enum
[PROOF STATE]
proof (prove)
using this:
CARD(?'a) = length enum_class.enum

goal (1 subgoal):
 1. length enum_class.enum = CARD('a)
[PROOF STEP]
by metis


[STATEMENT]
lemma ket_canonical_basis: "ket x = canonical_basis ! enum_idx x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ket x = canonical_basis ! enum_idx x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ket x = canonical_basis ! enum_idx x
[PROOF STEP]
have "x = (enum_class.enum::'a list) ! enum_idx x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = enum_class.enum ! enum_idx x
[PROOF STEP]
using enum_idx_correct[where i = x]
[PROOF STATE]
proof (prove)
using this:
enum_class.enum ! enum_idx x = x

goal (1 subgoal):
 1. x = enum_class.enum ! enum_idx x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = enum_class.enum ! enum_idx x

goal (1 subgoal):
 1. ket x = canonical_basis ! enum_idx x
[PROOF STEP]
hence p1: "ket x = ket ((enum_class.enum::'a list) ! enum_idx x)"
[PROOF STATE]
proof (prove)
using this:
x = enum_class.enum ! enum_idx x

goal (1 subgoal):
 1. ket x = ket (enum_class.enum ! enum_idx x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ket x = ket (enum_class.enum ! enum_idx x)

goal (1 subgoal):
 1. ket x = canonical_basis ! enum_idx x
[PROOF STEP]
have "enum_idx x < length (enum_class.enum::'a list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enum_idx x < length enum_class.enum
[PROOF STEP]
using enum_idx_bound[where x = x]
[PROOF STATE]
proof (prove)
using this:
enum_idx x < length enum_class.enum

goal (1 subgoal):
 1. enum_idx x < length enum_class.enum
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
enum_idx x < length enum_class.enum

goal (1 subgoal):
 1. ket x = canonical_basis ! enum_idx x
[PROOF STEP]
hence "(map ket (enum_class.enum::'a list)) ! enum_idx x
        = ket ((enum_class.enum::'a list) ! enum_idx x)"
[PROOF STATE]
proof (prove)
using this:
enum_idx x < length enum_class.enum

goal (1 subgoal):
 1. map ket enum_class.enum ! enum_idx x = ket (enum_class.enum ! enum_idx x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map ket enum_class.enum ! enum_idx x = ket (enum_class.enum ! enum_idx x)

goal (1 subgoal):
 1. ket x = canonical_basis ! enum_idx x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
map ket enum_class.enum ! enum_idx x = ket (enum_class.enum ! enum_idx x)

goal (1 subgoal):
 1. ket x = canonical_basis ! enum_idx x
[PROOF STEP]
unfolding canonical_basis_ell2_def
[PROOF STATE]
proof (prove)
using this:
map ket enum_class.enum ! enum_idx x = ket (enum_class.enum ! enum_idx x)

goal (1 subgoal):
 1. ket x = map ket enum_class.enum ! enum_idx x
[PROOF STEP]
using p1
[PROOF STATE]
proof (prove)
using this:
map ket enum_class.enum ! enum_idx x = ket (enum_class.enum ! enum_idx x)
ket x = ket (enum_class.enum ! enum_idx x)

goal (1 subgoal):
 1. ket x = map ket enum_class.enum ! enum_idx x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ket x = canonical_basis ! enum_idx x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma clinear_equal_ket:
  fixes f g :: \<open>'a::finite ell2 \<Rightarrow> _\<close>
  assumes \<open>clinear f\<close>
  assumes \<open>clinear g\<close>
  assumes \<open>\<And>i. f (ket i) = g (ket i)\<close>
  shows \<open>f = g\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = g
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. f x = g x
[PROOF STEP]
apply (rule complex_vector.linear_eq_on_span[where f=f and g=g and B=\<open>range ket\<close>])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. clinear f
 2. \<And>x. clinear g
 3. \<And>x xa. xa \<in> range ket \<Longrightarrow> f xa = g xa
 4. \<And>x. x \<in> cspan (range ket)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
clinear f
clinear g
f (ket ?i) = g (ket ?i)

goal (4 subgoals):
 1. \<And>x. clinear f
 2. \<And>x. clinear g
 3. \<And>x xa. xa \<in> range ket \<Longrightarrow> f xa = g xa
 4. \<And>x. x \<in> cspan (range ket)
[PROOF STEP]
by auto


[STATEMENT]
lemma equal_ket:
  fixes A B :: \<open>('a ell2, 'b::complex_normed_vector) cblinfun\<close>
  assumes \<open>\<And> x. A *\<^sub>V ket x = B *\<^sub>V ket x\<close>
  shows \<open>A = B\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = B
[PROOF STEP]
apply (rule cblinfun_eq_gen_eqI[where G=\<open>range ket\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> range ket \<Longrightarrow> A *\<^sub>V x = B *\<^sub>V x
 2. ccspan (range ket) = \<top>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A *\<^sub>V ket ?x = B *\<^sub>V ket ?x

goal (2 subgoals):
 1. \<And>x. x \<in> range ket \<Longrightarrow> A *\<^sub>V x = B *\<^sub>V x
 2. ccspan (range ket) = \<top>
[PROOF STEP]
by auto


[STATEMENT]
lemma antilinear_equal_ket:
  fixes f g :: \<open>'a::finite ell2 \<Rightarrow> _\<close>
  assumes \<open>antilinear f\<close>
  assumes \<open>antilinear g\<close>
  assumes \<open>\<And>i. f (ket i) = g (ket i)\<close>
  shows \<open>f = g\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f = g
[PROOF STEP]
have [simp]: \<open>clinear (f \<circ> from_conjugate_space)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear (f \<circ> from_conjugate_space)
[PROOF STEP]
apply (rule antilinear_o_antilinear)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. antilinear from_conjugate_space
 2. antilinear f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
antilinear f
antilinear g
f (ket ?i) = g (ket ?i)

goal (2 subgoals):
 1. antilinear from_conjugate_space
 2. antilinear f
[PROOF STEP]
by (simp_all add: antilinear_from_conjugate_space)
[PROOF STATE]
proof (state)
this:
clinear (f \<circ> from_conjugate_space)

goal (1 subgoal):
 1. f = g
[PROOF STEP]
have [simp]: \<open>clinear (g \<circ> from_conjugate_space)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear (g \<circ> from_conjugate_space)
[PROOF STEP]
apply (rule antilinear_o_antilinear)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. antilinear from_conjugate_space
 2. antilinear g
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
antilinear f
antilinear g
f (ket ?i) = g (ket ?i)

goal (2 subgoals):
 1. antilinear from_conjugate_space
 2. antilinear g
[PROOF STEP]
by (simp_all add: antilinear_from_conjugate_space)
[PROOF STATE]
proof (state)
this:
clinear (g \<circ> from_conjugate_space)

goal (1 subgoal):
 1. f = g
[PROOF STEP]
have [simp]: \<open>cspan (to_conjugate_space ` (range ket :: 'a ell2 set)) = UNIV\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cspan (to_conjugate_space ` range ket) = UNIV
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cspan (to_conjugate_space ` range ket) = UNIV

goal (1 subgoal):
 1. f = g
[PROOF STEP]
have "f o from_conjugate_space = g o from_conjugate_space"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<circ> from_conjugate_space = g \<circ> from_conjugate_space
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (f \<circ> from_conjugate_space) x = (g \<circ> from_conjugate_space) x
[PROOF STEP]
apply (rule complex_vector.linear_eq_on_span[where f="f o from_conjugate_space" and g="g o from_conjugate_space" and B=\<open>to_conjugate_space ` range ket\<close>])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. clinear (f \<circ> from_conjugate_space)
 2. \<And>x. clinear (g \<circ> from_conjugate_space)
 3. \<And>x xa. xa \<in> to_conjugate_space ` range ket \<Longrightarrow> (f \<circ> from_conjugate_space) xa = (g \<circ> from_conjugate_space) xa
 4. \<And>x. x \<in> cspan (to_conjugate_space ` range ket)
[PROOF STEP]
apply (simp, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. xa \<in> to_conjugate_space ` range ket \<Longrightarrow> (f \<circ> from_conjugate_space) xa = (g \<circ> from_conjugate_space) xa
 2. \<And>x. x \<in> cspan (to_conjugate_space ` range ket)
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
f (ket ?i) = g (ket ?i)

goal (2 subgoals):
 1. \<And>x xa. xa \<in> to_conjugate_space ` range ket \<Longrightarrow> (f \<circ> from_conjugate_space) xa = (g \<circ> from_conjugate_space) xa
 2. \<And>x. x \<in> cspan (to_conjugate_space ` range ket)
[PROOF STEP]
by (auto simp: to_conjugate_space_inverse)
[PROOF STATE]
proof (state)
this:
f \<circ> from_conjugate_space = g \<circ> from_conjugate_space

goal (1 subgoal):
 1. f = g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<circ> from_conjugate_space = g \<circ> from_conjugate_space
[PROOF STEP]
show "f = g"
[PROOF STATE]
proof (prove)
using this:
f \<circ> from_conjugate_space = g \<circ> from_conjugate_space

goal (1 subgoal):
 1. f = g
[PROOF STEP]
by (smt (verit) UNIV_I from_conjugate_space_inverse surj_def surj_fun_eq to_conjugate_space_inject)
[PROOF STATE]
proof (state)
this:
f = g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cinner_ket_adjointI:
  fixes F::"'a ell2 \<Rightarrow>\<^sub>C\<^sub>L _" and G::"'b ell2 \<Rightarrow>\<^sub>C\<^sub>L_"
  assumes "\<And> i j. (F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)"
  shows "F = G*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F = G*
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. F = G*
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(F *\<^sub>V ket ?i) \<bullet>\<^sub>C ket ?j = ket ?i \<bullet>\<^sub>C (G *\<^sub>V ket ?j)
[PROOF STEP]
have \<open>(F *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (G *\<^sub>V y)\<close> if \<open>x \<in> range ket\<close> and \<open>y \<in> range ket\<close> for x y
[PROOF STATE]
proof (prove)
using this:
(F *\<^sub>V ket ?i) \<bullet>\<^sub>C ket ?j = ket ?i \<bullet>\<^sub>C (G *\<^sub>V ket ?j)

goal (1 subgoal):
 1. (F *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (G *\<^sub>V y)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
(F *\<^sub>V ket ?i) \<bullet>\<^sub>C ket ?j = ket ?i \<bullet>\<^sub>C (G *\<^sub>V ket ?j)
x \<in> range ket
y \<in> range ket

goal (1 subgoal):
 1. (F *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (G *\<^sub>V y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> range ket; ?y \<in> range ket\<rbrakk> \<Longrightarrow> (F *\<^sub>V ?x) \<bullet>\<^sub>C ?y = ?x \<bullet>\<^sub>C (G *\<^sub>V ?y)

goal (1 subgoal):
 1. F = G*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x \<in> range ket; ?y \<in> range ket\<rbrakk> \<Longrightarrow> (F *\<^sub>V ?x) \<bullet>\<^sub>C ?y = ?x \<bullet>\<^sub>C (G *\<^sub>V ?y)
[PROOF STEP]
have \<open>(F *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (G *\<^sub>V y)\<close> if \<open>x \<in> range ket\<close> for x y
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> range ket; ?y \<in> range ket\<rbrakk> \<Longrightarrow> (F *\<^sub>V ?x) \<bullet>\<^sub>C ?y = ?x \<bullet>\<^sub>C (G *\<^sub>V ?y)

goal (1 subgoal):
 1. (F *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (G *\<^sub>V y)
[PROOF STEP]
apply (rule bounded_clinear_eq_on[where G=\<open>range ket\<close> and t=y, rotated 2])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>xa. xa \<in> range ket \<Longrightarrow> x \<in> range ket
 2. \<And>x. x \<in> range ket \<Longrightarrow> x \<in> range ket
 3. y \<in> closure (cspan (range ket))
 4. bounded_clinear ((\<bullet>\<^sub>C) (F *\<^sub>V x))
 5. bounded_clinear (\<lambda>xa. x \<bullet>\<^sub>C (G *\<^sub>V xa))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> range ket

goal (5 subgoals):
 1. \<And>xa. xa \<in> range ket \<Longrightarrow> x \<in> range ket
 2. \<And>x. x \<in> range ket \<Longrightarrow> x \<in> range ket
 3. y \<in> closure (cspan (range ket))
 4. bounded_clinear ((\<bullet>\<^sub>C) (F *\<^sub>V x))
 5. bounded_clinear (\<lambda>xa. x \<bullet>\<^sub>C (G *\<^sub>V xa))
[PROOF STEP]
by (auto intro!: bounded_linear_intros)
[PROOF STATE]
proof (state)
this:
?x \<in> range ket \<Longrightarrow> (F *\<^sub>V ?x) \<bullet>\<^sub>C ?y = ?x \<bullet>\<^sub>C (G *\<^sub>V ?y)

goal (1 subgoal):
 1. F = G*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> range ket \<Longrightarrow> (F *\<^sub>V ?x) \<bullet>\<^sub>C ?y = ?x \<bullet>\<^sub>C (G *\<^sub>V ?y)
[PROOF STEP]
have \<open>(F *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (G *\<^sub>V y)\<close> for x y
[PROOF STATE]
proof (prove)
using this:
?x \<in> range ket \<Longrightarrow> (F *\<^sub>V ?x) \<bullet>\<^sub>C ?y = ?x \<bullet>\<^sub>C (G *\<^sub>V ?y)

goal (1 subgoal):
 1. (F *\<^sub>V x) \<bullet>\<^sub>C y = x \<bullet>\<^sub>C (G *\<^sub>V y)
[PROOF STEP]
apply (rule bounded_antilinear_eq_on[where G=\<open>range ket\<close> and t=x, rotated 2])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. x \<in> range ket \<Longrightarrow> x \<in> range ket
 2. x \<in> closure (cspan (range ket))
 3. bounded_antilinear (\<lambda>x. (F *\<^sub>V x) \<bullet>\<^sub>C y)
 4. bounded_antilinear (\<lambda>x. x \<bullet>\<^sub>C (G *\<^sub>V y))
[PROOF STEP]
by (auto intro!: bounded_linear_intros)
[PROOF STATE]
proof (state)
this:
(F *\<^sub>V ?x) \<bullet>\<^sub>C ?y = ?x \<bullet>\<^sub>C (G *\<^sub>V ?y)

goal (1 subgoal):
 1. F = G*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(F *\<^sub>V ?x) \<bullet>\<^sub>C ?y = ?x \<bullet>\<^sub>C (G *\<^sub>V ?y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(F *\<^sub>V ?x) \<bullet>\<^sub>C ?y = ?x \<bullet>\<^sub>C (G *\<^sub>V ?y)

goal (1 subgoal):
 1. F = G*
[PROOF STEP]
by (rule adjoint_eqI)
[PROOF STATE]
proof (state)
this:
F = G*

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ket_nonzero[simp]: "ket i \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ket i \<noteq> 0
[PROOF STEP]
using norm_ket[of i]
[PROOF STATE]
proof (prove)
using this:
norm (ket i) = 1

goal (1 subgoal):
 1. ket i \<noteq> 0
[PROOF STEP]
by force


[STATEMENT]
lemma cindependent_ket:
  "cindependent (range (ket::'a\<Rightarrow>_))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindependent (range ket)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cindependent (range ket)
[PROOF STEP]
define S where "S = range (ket::'a\<Rightarrow>_)"
[PROOF STATE]
proof (state)
this:
S = range ket

goal (1 subgoal):
 1. cindependent (range ket)
[PROOF STEP]
have "is_ortho_set S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_ortho_set S
[PROOF STEP]
unfolding S_def is_ortho_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>range ket. \<forall>y\<in>range ket. x \<noteq> y \<longrightarrow> is_orthogonal x y) \<and> 0 \<notin> range ket
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_ortho_set S

goal (1 subgoal):
 1. cindependent (range ket)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_ortho_set S

goal (1 subgoal):
 1. cindependent (range ket)
[PROOF STEP]
have "0 \<notin> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> S
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> range ket
[PROOF STEP]
using ket_nonzero
[PROOF STATE]
proof (prove)
using this:
ket ?i \<noteq> 0

goal (1 subgoal):
 1. 0 \<notin> range ket
[PROOF STEP]
by (simp add: image_iff)
[PROOF STATE]
proof (state)
this:
0 \<notin> S

goal (1 subgoal):
 1. cindependent (range ket)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_ortho_set S
0 \<notin> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_ortho_set S
0 \<notin> S

goal (1 subgoal):
 1. cindependent (range ket)
[PROOF STEP]
using is_ortho_set_cindependent[where A = S]
[PROOF STATE]
proof (prove)
using this:
is_ortho_set S
0 \<notin> S
is_ortho_set S \<Longrightarrow> cindependent S

goal (1 subgoal):
 1. cindependent (range ket)
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
using this:
is_ortho_set (range ket)
0 \<notin> range ket
is_ortho_set (range ket) \<Longrightarrow> cindependent (range ket)

goal (1 subgoal):
 1. cindependent (range ket)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cindependent (range ket)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cdim_UNIV_ell2[simp]: \<open>cdim (UNIV::'a::finite ell2 set) = CARD('a)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cdim UNIV = CARD('a)
[PROOF STEP]
apply (subst cspan_range_ket_finite[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cdim (cspan (range ket)) = CARD('a)
[PROOF STEP]
by (metis card_image cindependent_ket complex_vector.dim_span_eq_card_independent inj_ket)


[STATEMENT]
lemma is_ortho_set_ket[simp]: \<open>is_ortho_set (range ket)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_ortho_set (range ket)
[PROOF STEP]
using is_ortho_set_def
[PROOF STATE]
proof (prove)
using this:
is_ortho_set ?S = ((\<forall>x\<in>?S. \<forall>y\<in>?S. x \<noteq> y \<longrightarrow> is_orthogonal x y) \<and> (0::?'a) \<notin> ?S)

goal (1 subgoal):
 1. is_ortho_set (range ket)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma bounded_clinear_equal_ket:
  fixes f g :: \<open>'a ell2 \<Rightarrow> _\<close>
  assumes \<open>bounded_clinear f\<close>
  assumes \<open>bounded_clinear g\<close>
  assumes \<open>\<And>i. f (ket i) = g (ket i)\<close>
  shows \<open>f = g\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = g
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. f x = g x
[PROOF STEP]
apply (rule bounded_clinear_eq_on[of f g \<open>range ket\<close>])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. bounded_clinear f
 2. \<And>x. bounded_clinear g
 3. \<And>x xa. xa \<in> range ket \<Longrightarrow> f xa = g xa
 4. \<And>x. x \<in> closure (cspan (range ket))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bounded_clinear f
bounded_clinear g
f (ket ?i) = g (ket ?i)

goal (4 subgoals):
 1. \<And>x. bounded_clinear f
 2. \<And>x. bounded_clinear g
 3. \<And>x xa. xa \<in> range ket \<Longrightarrow> f xa = g xa
 4. \<And>x. x \<in> closure (cspan (range ket))
[PROOF STEP]
by auto


[STATEMENT]
lemma bounded_antilinear_equal_ket:
  fixes f g :: \<open>'a ell2 \<Rightarrow> _\<close>
  assumes \<open>bounded_antilinear f\<close>
  assumes \<open>bounded_antilinear g\<close>
  assumes \<open>\<And>i. f (ket i) = g (ket i)\<close>
  shows \<open>f = g\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = g
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. f x = g x
[PROOF STEP]
apply (rule bounded_antilinear_eq_on[of f g \<open>range ket\<close>])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. bounded_antilinear f
 2. \<And>x. bounded_antilinear g
 3. \<And>x xa. xa \<in> range ket \<Longrightarrow> f xa = g xa
 4. \<And>x. x \<in> closure (cspan (range ket))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bounded_antilinear f
bounded_antilinear g
f (ket ?i) = g (ket ?i)

goal (4 subgoals):
 1. \<And>x. bounded_antilinear f
 2. \<And>x. bounded_antilinear g
 3. \<And>x xa. xa \<in> range ket \<Longrightarrow> f xa = g xa
 4. \<And>x. x \<in> closure (cspan (range ket))
[PROOF STEP]
by auto


[STATEMENT]
lemma is_onb_ket[simp]: \<open>is_onb (range ket)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_onb (range ket)
[PROOF STEP]
by (auto simp: is_onb_def)


[STATEMENT]
lemma ell2_sum_ket: \<open>\<psi> = (\<Sum>i\<in>UNIV. Rep_ell2 \<psi> i *\<^sub>C ket i)\<close> for \<psi> :: \<open>_::finite ell2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> = (\<Sum>i\<in>UNIV. Rep_ell2 \<psi> i *\<^sub>C ket i)
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<psi>. has_ell2_norm \<psi> \<Longrightarrow> \<psi> = (\<lambda>x. \<Sum>y\<in>UNIV. \<psi> y * (if y = x then 1 else 0))
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<psi> x. has_ell2_norm \<psi> \<Longrightarrow> \<psi> x = (\<Sum>y\<in>UNIV. \<psi> y * (if y = x then 1 else 0))
[PROOF STEP]
apply (subst sum_single)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>\<psi> x. has_ell2_norm \<psi> \<Longrightarrow> finite UNIV
 2. \<And>\<psi> x j. \<lbrakk>has_ell2_norm \<psi>; j \<noteq> ?i46 \<psi> x; j \<in> UNIV\<rbrakk> \<Longrightarrow> \<psi> j * (if j = x then 1 else 0) = 0
 3. \<And>\<psi> x. has_ell2_norm \<psi> \<Longrightarrow> \<psi> x = (if ?i46 \<psi> x \<in> UNIV then \<psi> (?i46 \<psi> x) * (if ?i46 \<psi> x = x then 1 else 0) else 0)
[PROOF STEP]
by auto


[STATEMENT]
lemma cspan_butterfly_ket: \<open>cspan {butterfly (ket i) (ket j)| (i::'b::finite) (j::'a::finite). True} = UNIV\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cspan {butterfly (ket i) (ket j) |i j. True} = UNIV
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cspan {butterfly (ket i) (ket j) |i j. True} = UNIV
[PROOF STEP]
have *: \<open>{butterfly (ket i) (ket j)| (i::'b::finite) (j::'a::finite). True} = {butterfly a b |a b. a \<in> range ket \<and> b \<in> range ket}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {butterfly (ket i) (ket j) |i j. True} = {butterfly a b |a b. a \<in> range ket \<and> b \<in> range ket}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{butterfly (ket i) (ket j) |i j. True} = {butterfly a b |a b. a \<in> range ket \<and> b \<in> range ket}

goal (1 subgoal):
 1. cspan {butterfly (ket i) (ket j) |i j. True} = UNIV
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cspan {butterfly (ket i) (ket j) |i j. True} = UNIV
[PROOF STEP]
apply (subst *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cspan {butterfly a b |a b. a \<in> range ket \<and> b \<in> range ket} = UNIV
[PROOF STEP]
apply (rule cspan_butterfly_UNIV)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. cspan (range ket) = UNIV
 2. cspan (range ket) = UNIV
 3. is_ortho_set (range ket)
 4. \<And>b. b \<in> range ket \<Longrightarrow> norm b = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cspan {butterfly (ket i) (ket j) |i j. True} = UNIV

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cindependent_butterfly_ket: \<open>cindependent {butterfly (ket i) (ket j)| (i::'b) (j::'a). True}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindependent {butterfly (ket i) (ket j) |i j. True}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cindependent {butterfly (ket i) (ket j) |i j. True}
[PROOF STEP]
have *: \<open>{butterfly (ket i) (ket j)| (i::'b) (j::'a). True} = {butterfly a b |a b. a \<in> range ket \<and> b \<in> range ket}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {butterfly (ket i) (ket j) |i j. True} = {butterfly a b |a b. a \<in> range ket \<and> b \<in> range ket}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{butterfly (ket i) (ket j) |i j. True} = {butterfly a b |a b. a \<in> range ket \<and> b \<in> range ket}

goal (1 subgoal):
 1. cindependent {butterfly (ket i) (ket j) |i j. True}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindependent {butterfly (ket i) (ket j) |i j. True}
[PROOF STEP]
apply (subst *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindependent {butterfly a b |a b. a \<in> range ket \<and> b \<in> range ket}
[PROOF STEP]
apply (rule cindependent_butterfly)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. is_ortho_set (range ket)
 2. is_ortho_set (range ket)
 3. \<And>a. a \<in> range ket \<Longrightarrow> norm a = 1
 4. \<And>b. b \<in> range ket \<Longrightarrow> norm b = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cindependent {butterfly (ket i) (ket j) |i j. True}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_butterfly_ket[simp]: \<open>(\<Sum>(i::'a::finite)\<in>UNIV. butterfly (ket i) (ket i)) = id_cblinfun\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>UNIV. selfbutter (ket i)) = id_cblinfun
[PROOF STEP]
apply (rule equal_ket)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<Sum>i\<in>UNIV. selfbutter (ket i)) *\<^sub>V ket x = id_cblinfun *\<^sub>V ket x
[PROOF STEP]
apply (subst complex_vector.linear_sum[where f=\<open>\<lambda>y. y *\<^sub>V ket _\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. clinear (\<lambda>y. y *\<^sub>V ket x)
 2. \<And>x. (\<Sum>a\<in>UNIV. selfbutter (ket a) *\<^sub>V ket x) = id_cblinfun *\<^sub>V ket x
[PROOF STEP]
apply (auto simp add: scaleC_cblinfun.rep_eq cblinfun.add_left clinearI butterfly_def cblinfun_compose_image cinner_ket)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<Sum>a\<in>UNIV. (if a = x then 1 else 0) *\<^sub>C ket a) = ket x
[PROOF STEP]
apply (subst sum.mono_neutral_cong_right[where S=\<open>{_}\<close>])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. finite UNIV
 2. \<And>x. {?uu7 x} \<subseteq> UNIV
 3. \<And>x. \<forall>i\<in>UNIV - {?uu7 x}. (if i = x then 1 else 0) *\<^sub>C ket i = 0
 4. \<And>x xa. xa \<in> {?uu7 x} \<Longrightarrow> (if xa = x then 1 else 0) *\<^sub>C ket xa = ?h7 x xa
 5. \<And>x. sum (?h7 x) {?uu7 x} = ket x
[PROOF STEP]
by auto


[STATEMENT]
lemma ket_CARD_1_is_1: \<open>ket x = 1\<close> for x :: \<open>'a::CARD_1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ket x = 1
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<lambda>y. if x = y then 1 else 0) = (\<lambda>_. 1)
[PROOF STEP]
by simp


[STATEMENT]
lemma classical_operator_existsI:
  assumes "\<And>x. B *\<^sub>V (ket x) = (case \<pi> x of Some i \<Rightarrow> ket i | None \<Rightarrow> 0)"
  shows "classical_operator_exists \<pi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator_exists \<pi>
[PROOF STEP]
unfolding classical_operator_exists_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cblinfun_extension_exists (range ket) (\<lambda>t. case \<pi> (inv ket t) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x)
[PROOF STEP]
apply (rule cblinfun_extension_existsI[of _ B])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> range ket \<Longrightarrow> B *\<^sub>V x = (case \<pi> (inv ket x) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
B *\<^sub>V ket ?x = (case \<pi> ?x of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i)

goal (1 subgoal):
 1. \<And>x. x \<in> range ket \<Longrightarrow> B *\<^sub>V x = (case \<pi> (inv ket x) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x)
[PROOF STEP]
by (auto simp: inv_f_f[OF inj_ket])


[STATEMENT]
lemma
  assumes "inj_map \<pi>"
  shows classical_operator_exists_inj: "classical_operator_exists \<pi>"
    and classical_operator_norm_inj: \<open>norm (classical_operator \<pi>) \<le> 1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator_exists \<pi> &&& norm (classical_operator \<pi>) \<le> 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. classical_operator_exists \<pi>
 2. norm (classical_operator \<pi>) \<le> 1
[PROOF STEP]
have \<open>is_orthogonal (case \<pi> x of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x')
                      (case \<pi> y of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')\<close>
    if \<open>x \<noteq> y\<close> for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_orthogonal (case \<pi> x of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> y of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')
[PROOF STEP]
apply (cases \<open>\<pi> x\<close>; cases \<open>\<pi> y\<close>)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<pi> x = None; \<pi> y = None\<rbrakk> \<Longrightarrow> is_orthogonal (case \<pi> x of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> y of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')
 2. \<And>a. \<lbrakk>\<pi> x = None; \<pi> y = Some a\<rbrakk> \<Longrightarrow> is_orthogonal (case \<pi> x of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> y of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')
 3. \<And>a. \<lbrakk>\<pi> x = Some a; \<pi> y = None\<rbrakk> \<Longrightarrow> is_orthogonal (case \<pi> x of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> y of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')
 4. \<And>a aa. \<lbrakk>\<pi> x = Some a; \<pi> y = Some aa\<rbrakk> \<Longrightarrow> is_orthogonal (case \<pi> x of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> y of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')
[PROOF STEP]
using that assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
inj_map \<pi>

goal (4 subgoals):
 1. \<lbrakk>\<pi> x = None; \<pi> y = None\<rbrakk> \<Longrightarrow> is_orthogonal (case \<pi> x of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> y of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')
 2. \<And>a. \<lbrakk>\<pi> x = None; \<pi> y = Some a\<rbrakk> \<Longrightarrow> is_orthogonal (case \<pi> x of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> y of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')
 3. \<And>a. \<lbrakk>\<pi> x = Some a; \<pi> y = None\<rbrakk> \<Longrightarrow> is_orthogonal (case \<pi> x of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> y of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')
 4. \<And>a aa. \<lbrakk>\<pi> x = Some a; \<pi> y = Some aa\<rbrakk> \<Longrightarrow> is_orthogonal (case \<pi> x of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> y of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')
[PROOF STEP]
by (auto simp add: inj_map_def)
[PROOF STATE]
proof (state)
this:
?x \<noteq> ?y \<Longrightarrow> is_orthogonal (case \<pi> ?x of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> ?y of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')

goal (2 subgoals):
 1. classical_operator_exists \<pi>
 2. norm (classical_operator \<pi>) \<le> 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<noteq> ?y \<Longrightarrow> is_orthogonal (case \<pi> ?x of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> ?y of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')
[PROOF STEP]
have 1: \<open>is_orthogonal (case \<pi> (inv ket x) of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x')
                      (case \<pi> (inv ket y) of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')\<close>
    if \<open>x \<in> range ket\<close> and \<open>y \<in> range ket\<close> and \<open>x \<noteq> y\<close> for x y
[PROOF STATE]
proof (prove)
using this:
?x \<noteq> ?y \<Longrightarrow> is_orthogonal (case \<pi> ?x of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> ?y of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')

goal (1 subgoal):
 1. is_orthogonal (case \<pi> (inv ket x) of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> (inv ket y) of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?x \<noteq> ?y \<Longrightarrow> is_orthogonal (case \<pi> ?x of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> ?y of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')
x \<in> range ket
y \<in> range ket
x \<noteq> y

goal (1 subgoal):
 1. is_orthogonal (case \<pi> (inv ket x) of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> (inv ket y) of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> range ket; ?y \<in> range ket; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> is_orthogonal (case \<pi> (inv ket ?x) of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> (inv ket ?y) of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')

goal (2 subgoals):
 1. classical_operator_exists \<pi>
 2. norm (classical_operator \<pi>) \<le> 1
[PROOF STEP]
have \<open>norm (case \<pi> x of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) \<le> 1 * norm (ket x)\<close> for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (case \<pi> x of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) \<le> 1 * norm (ket x)
[PROOF STEP]
apply (cases \<open>\<pi> x\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<pi> x = None \<Longrightarrow> norm (case \<pi> x of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) \<le> 1 * norm (ket x)
 2. \<And>a. \<pi> x = Some a \<Longrightarrow> norm (case \<pi> x of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) \<le> 1 * norm (ket x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
norm (case \<pi> ?x of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) \<le> 1 * norm (ket ?x)

goal (2 subgoals):
 1. classical_operator_exists \<pi>
 2. norm (classical_operator \<pi>) \<le> 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
norm (case \<pi> ?x of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) \<le> 1 * norm (ket ?x)
[PROOF STEP]
have 2: \<open>norm (case \<pi> (inv ket x) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) \<le> 1 * norm x\<close>
    if \<open>x \<in> range ket\<close> for x
[PROOF STATE]
proof (prove)
using this:
norm (case \<pi> ?x of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) \<le> 1 * norm (ket ?x)

goal (1 subgoal):
 1. norm (case \<pi> (inv ket x) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) \<le> 1 * norm x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
norm (case \<pi> ?x of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) \<le> 1 * norm (ket ?x)
x \<in> range ket

goal (1 subgoal):
 1. norm (case \<pi> (inv ket x) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) \<le> 1 * norm x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> range ket \<Longrightarrow> norm (case \<pi> (inv ket ?x) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) \<le> 1 * norm ?x

goal (2 subgoals):
 1. classical_operator_exists \<pi>
 2. norm (classical_operator \<pi>) \<le> 1
[PROOF STEP]
show \<open>classical_operator_exists \<pi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator_exists \<pi>
[PROOF STEP]
unfolding classical_operator_exists_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cblinfun_extension_exists (range ket) (\<lambda>t. case \<pi> (inv ket t) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x)
[PROOF STEP]
using _ _ 1 2
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
PROP ?psi \<Longrightarrow> PROP ?psi
\<lbrakk>?x \<in> range ket; ?y \<in> range ket; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> is_orthogonal (case \<pi> (inv ket ?x) of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> (inv ket ?y) of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')
?x \<in> range ket \<Longrightarrow> norm (case \<pi> (inv ket ?x) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) \<le> 1 * norm ?x

goal (1 subgoal):
 1. cblinfun_extension_exists (range ket) (\<lambda>t. case \<pi> (inv ket t) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x)
[PROOF STEP]
apply (rule cblinfun_extension_exists_ortho)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. is_ortho_set (range ket)
 2. closure (cspan (range ket)) = UNIV
 3. \<And>t y. \<lbrakk>t \<in> range ket; y \<in> range ket; t \<noteq> y\<rbrakk> \<Longrightarrow> t \<in> range ket
 4. \<And>t y. \<lbrakk>t \<in> range ket; y \<in> range ket; t \<noteq> y\<rbrakk> \<Longrightarrow> y \<in> range ket
 5. \<And>t y. \<lbrakk>t \<in> range ket; y \<in> range ket; t \<noteq> y\<rbrakk> \<Longrightarrow> t \<noteq> y
 6. \<And>t. t \<in> range ket \<Longrightarrow> t \<in> range ket
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
classical_operator_exists \<pi>

goal (1 subgoal):
 1. norm (classical_operator \<pi>) \<le> 1
[PROOF STEP]
show \<open>norm (classical_operator \<pi>) \<le> 1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (classical_operator \<pi>) \<le> 1
[PROOF STEP]
unfolding classical_operator_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (cblinfun_extension (range ket) (\<lambda>t. case \<pi> (inv ket t) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x)) \<le> 1
[PROOF STEP]
using _ _ 1 2
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
PROP ?psi \<Longrightarrow> PROP ?psi
\<lbrakk>?x \<in> range ket; ?y \<in> range ket; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> is_orthogonal (case \<pi> (inv ket ?x) of None \<Rightarrow> 0 | Some x' \<Rightarrow> ket x') (case \<pi> (inv ket ?y) of None \<Rightarrow> 0 | Some y' \<Rightarrow> ket y')
?x \<in> range ket \<Longrightarrow> norm (case \<pi> (inv ket ?x) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) \<le> 1 * norm ?x

goal (1 subgoal):
 1. norm (cblinfun_extension (range ket) (\<lambda>t. case \<pi> (inv ket t) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x)) \<le> 1
[PROOF STEP]
apply (rule cblinfun_extension_exists_ortho_norm)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. is_ortho_set (range ket)
 2. closure (cspan (range ket)) = UNIV
 3. \<And>t y. \<lbrakk>t \<in> range ket; y \<in> range ket; t \<noteq> y\<rbrakk> \<Longrightarrow> t \<in> range ket
 4. \<And>t y. \<lbrakk>t \<in> range ket; y \<in> range ket; t \<noteq> y\<rbrakk> \<Longrightarrow> y \<in> range ket
 5. \<And>t y. \<lbrakk>t \<in> range ket; y \<in> range ket; t \<noteq> y\<rbrakk> \<Longrightarrow> t \<noteq> y
 6. \<And>t. t \<in> range ket \<Longrightarrow> t \<in> range ket
 7. 0 \<le> 1
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
norm (classical_operator \<pi>) \<le> 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma classical_operator_exists_finite[simp]: "classical_operator_exists (\<pi> :: _::finite \<Rightarrow> _)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator_exists \<pi>
[PROOF STEP]
unfolding classical_operator_exists_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cblinfun_extension_exists (range ket) (\<lambda>t. case \<pi> (inv ket t) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x)
[PROOF STEP]
apply (rule cblinfun_extension_exists_finite_dim)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. cindependent (range ket)
 2. cspan (range ket) = UNIV
[PROOF STEP]
using cindependent_ket
[PROOF STATE]
proof (prove)
using this:
cindependent (range ket)

goal (2 subgoals):
 1. cindependent (range ket)
 2. cspan (range ket) = UNIV
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cspan (range ket) = UNIV
[PROOF STEP]
using finite_class.finite_UNIV finite_imageI closed_cspan_range_ket closure_finite_cspan
[PROOF STATE]
proof (prove)
using this:
finite UNIV
finite ?F \<Longrightarrow> finite (?h ` ?F)
closure (cspan (range ket)) = UNIV
finite ?T \<Longrightarrow> closure (cspan ?T) = cspan ?T

goal (1 subgoal):
 1. cspan (range ket) = UNIV
[PROOF STEP]
by blast


[STATEMENT]
lemma classical_operator_ket:
  assumes "classical_operator_exists \<pi>"
  shows "(classical_operator \<pi>) *\<^sub>V (ket x) = (case \<pi> x of Some i \<Rightarrow> ket i | None \<Rightarrow> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator \<pi> *\<^sub>V ket x = (case \<pi> x of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i)
[PROOF STEP]
unfolding classical_operator_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Let (\<lambda>t. case \<pi> (inv ket t) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) (cblinfun_extension (range ket)) *\<^sub>V ket x = (case \<pi> x of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i)
[PROOF STEP]
using f_inv_into_f ket_injective rangeI
[PROOF STATE]
proof (prove)
using this:
?y \<in> ?f ` ?A \<Longrightarrow> ?f (inv_into ?A ?f ?y) = ?y
(ket ?i = ket ?j) = (?i = ?j)
?f ?x \<in> range ?f

goal (1 subgoal):
 1. Let (\<lambda>t. case \<pi> (inv ket t) of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) (cblinfun_extension (range ket)) *\<^sub>V ket x = (case \<pi> x of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i)
[PROOF STEP]
by (metis assms cblinfun_extension_apply classical_operator_exists_def)


[STATEMENT]
lemma classical_operator_ket_finite:
  "(classical_operator \<pi>) *\<^sub>V (ket (x::'a::finite)) = (case \<pi> x of Some i \<Rightarrow> ket i | None \<Rightarrow> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator \<pi> *\<^sub>V ket x = (case \<pi> x of None \<Rightarrow> 0 | Some i \<Rightarrow> ket i)
[PROOF STEP]
by (rule classical_operator_ket, simp)


[STATEMENT]
lemma classical_operator_adjoint[simp]:
  fixes \<pi> :: "'a \<Rightarrow> 'b option"
  assumes a1: "inj_map \<pi>"
  shows  "(classical_operator \<pi>)* = classical_operator (inv_map \<pi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator \<pi>* = classical_operator (inv_map \<pi>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. classical_operator \<pi>* = classical_operator (inv_map \<pi>)
[PROOF STEP]
define F where "F = classical_operator (inv_map \<pi>)"
[PROOF STATE]
proof (state)
this:
F = classical_operator (inv_map \<pi>)

goal (1 subgoal):
 1. classical_operator \<pi>* = classical_operator (inv_map \<pi>)
[PROOF STEP]
define G where "G = classical_operator \<pi>"
[PROOF STATE]
proof (state)
this:
G = classical_operator \<pi>

goal (1 subgoal):
 1. classical_operator \<pi>* = classical_operator (inv_map \<pi>)
[PROOF STEP]
have "(F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)
[PROOF STEP]
have w1: "(classical_operator (inv_map \<pi>)) *\<^sub>V (ket i)
     = (case inv_map \<pi> i of Some k \<Rightarrow> ket k | None \<Rightarrow> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator (inv_map \<pi>) *\<^sub>V ket i = (case inv_map \<pi> i of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k)
[PROOF STEP]
by (simp add: classical_operator_ket classical_operator_exists_inj)
[PROOF STATE]
proof (state)
this:
classical_operator (inv_map \<pi>) *\<^sub>V ket i = (case inv_map \<pi> i of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k)

goal (1 subgoal):
 1. (F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)
[PROOF STEP]
have w2: "(classical_operator \<pi>) *\<^sub>V (ket j)
     = (case \<pi> j of Some k \<Rightarrow> ket k | None \<Rightarrow> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator \<pi> *\<^sub>V ket j = (case \<pi> j of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k)
[PROOF STEP]
by (simp add: assms classical_operator_ket classical_operator_exists_inj)
[PROOF STATE]
proof (state)
this:
classical_operator \<pi> *\<^sub>V ket j = (case \<pi> j of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k)

goal (1 subgoal):
 1. (F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)
[PROOF STEP]
have "(F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = (classical_operator (inv_map \<pi>) *\<^sub>V ket i) \<bullet>\<^sub>C ket j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = (classical_operator (inv_map \<pi>) *\<^sub>V ket i) \<bullet>\<^sub>C ket j
[PROOF STEP]
unfolding F_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (classical_operator (inv_map \<pi>) *\<^sub>V ket i) \<bullet>\<^sub>C ket j = (classical_operator (inv_map \<pi>) *\<^sub>V ket i) \<bullet>\<^sub>C ket j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = (classical_operator (inv_map \<pi>) *\<^sub>V ket i) \<bullet>\<^sub>C ket j

goal (1 subgoal):
 1. (F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = (classical_operator (inv_map \<pi>) *\<^sub>V ket i) \<bullet>\<^sub>C ket j

goal (1 subgoal):
 1. (F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)
[PROOF STEP]
have "\<dots> = ((case inv_map \<pi> i of Some k \<Rightarrow> ket k | None \<Rightarrow> 0) \<bullet>\<^sub>C ket j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (classical_operator (inv_map \<pi>) *\<^sub>V ket i) \<bullet>\<^sub>C ket j = (case inv_map \<pi> i of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k) \<bullet>\<^sub>C ket j
[PROOF STEP]
using w1
[PROOF STATE]
proof (prove)
using this:
classical_operator (inv_map \<pi>) *\<^sub>V ket i = (case inv_map \<pi> i of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k)

goal (1 subgoal):
 1. (classical_operator (inv_map \<pi>) *\<^sub>V ket i) \<bullet>\<^sub>C ket j = (case inv_map \<pi> i of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k) \<bullet>\<^sub>C ket j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(classical_operator (inv_map \<pi>) *\<^sub>V ket i) \<bullet>\<^sub>C ket j = (case inv_map \<pi> i of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k) \<bullet>\<^sub>C ket j

goal (1 subgoal):
 1. (F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(classical_operator (inv_map \<pi>) *\<^sub>V ket i) \<bullet>\<^sub>C ket j = (case inv_map \<pi> i of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k) \<bullet>\<^sub>C ket j

goal (1 subgoal):
 1. (F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)
[PROOF STEP]
have "\<dots> = (ket i \<bullet>\<^sub>C (case \<pi> j of Some k \<Rightarrow> ket k | None \<Rightarrow> 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case inv_map \<pi> i of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k)
[PROOF STEP]
proof(induction "inv_map \<pi> i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. None = inv_map \<pi> i \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
 2. \<And>option. Some option = inv_map \<pi> i \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
None = inv_map \<pi> i

goal (2 subgoals):
 1. None = inv_map \<pi> i \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
 2. \<And>option. Some option = inv_map \<pi> i \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
hence pi1: "None = inv_map \<pi> i"
[PROOF STATE]
proof (prove)
using this:
None = inv_map \<pi> i

goal (1 subgoal):
 1. None = inv_map \<pi> i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
None = inv_map \<pi> i

goal (2 subgoals):
 1. None = inv_map \<pi> i \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
 2. \<And>option. Some option = inv_map \<pi> i \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
proof (induction "\<pi> j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. None = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
 2. \<And>option. Some option = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
None = \<pi> j

goal (2 subgoals):
 1. None = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
 2. \<And>option. Some option = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
None = \<pi> j

goal (1 subgoal):
 1. (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
using pi1
[PROOF STATE]
proof (prove)
using this:
None = \<pi> j
None = inv_map \<pi> i

goal (1 subgoal):
 1. (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)

goal (1 subgoal):
 1. \<And>option. Some option = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>option. Some option = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
case (Some c)
[PROOF STATE]
proof (state)
this:
Some c = \<pi> j

goal (1 subgoal):
 1. \<And>option. Some option = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
have "c \<noteq> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<noteq> i
[PROOF STEP]
proof(rule classical)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> c \<noteq> i \<Longrightarrow> c \<noteq> i
[PROOF STEP]
assume "\<not>(c \<noteq> i)"
[PROOF STATE]
proof (state)
this:
\<not> c \<noteq> i

goal (1 subgoal):
 1. \<not> c \<noteq> i \<Longrightarrow> c \<noteq> i
[PROOF STEP]
hence "c = i"
[PROOF STATE]
proof (prove)
using this:
\<not> c \<noteq> i

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

goal (1 subgoal):
 1. \<not> c \<noteq> i \<Longrightarrow> c \<noteq> i
[PROOF STEP]
hence "inv_map \<pi> c = inv_map \<pi> i"
[PROOF STATE]
proof (prove)
using this:
c = i

goal (1 subgoal):
 1. inv_map \<pi> c = inv_map \<pi> i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inv_map \<pi> c = inv_map \<pi> i

goal (1 subgoal):
 1. \<not> c \<noteq> i \<Longrightarrow> c \<noteq> i
[PROOF STEP]
hence "inv_map \<pi> c = None"
[PROOF STATE]
proof (prove)
using this:
inv_map \<pi> c = inv_map \<pi> i

goal (1 subgoal):
 1. inv_map \<pi> c = None
[PROOF STEP]
by (simp add: pi1)
[PROOF STATE]
proof (state)
this:
inv_map \<pi> c = None

goal (1 subgoal):
 1. \<not> c \<noteq> i \<Longrightarrow> c \<noteq> i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inv_map \<pi> c = None

goal (1 subgoal):
 1. \<not> c \<noteq> i \<Longrightarrow> c \<noteq> i
[PROOF STEP]
have "inv_map \<pi> c = Some j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_map \<pi> c = Some j
[PROOF STEP]
using Some.hyps
[PROOF STATE]
proof (prove)
using this:
Some c = \<pi> j

goal (1 subgoal):
 1. inv_map \<pi> c = Some j
[PROOF STEP]
unfolding inv_map_def
[PROOF STATE]
proof (prove)
using this:
Some c = \<pi> j

goal (1 subgoal):
 1. (if Some c \<in> range \<pi> then Some (inv \<pi> (Some c)) else None) = Some j
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some c = \<pi> j \<Longrightarrow> inv \<pi> (\<pi> j) = j
[PROOF STEP]
by (metis a1 f_inv_into_f inj_map_def option.distinct(1) rangeI)
[PROOF STATE]
proof (state)
this:
inv_map \<pi> c = Some j

goal (1 subgoal):
 1. \<not> c \<noteq> i \<Longrightarrow> c \<noteq> i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inv_map \<pi> c = None
inv_map \<pi> c = Some j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv_map \<pi> c = None
inv_map \<pi> c = Some j

goal (1 subgoal):
 1. c \<noteq> i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c \<noteq> i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c \<noteq> i

goal (1 subgoal):
 1. \<And>option. Some option = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
c \<noteq> i

goal (1 subgoal):
 1. (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
by (metis None.hyps Some.hyps cinner_zero_left orthogonal_ket option.simps(4)
              option.simps(5))
[PROOF STATE]
proof (state)
this:
(case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)

goal (1 subgoal):
 1. \<And>option. Some option = inv_map \<pi> i \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>option. Some option = inv_map \<pi> i \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
case (Some d)
[PROOF STATE]
proof (state)
this:
Some d = inv_map \<pi> i

goal (1 subgoal):
 1. \<And>option. Some option = inv_map \<pi> i \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
hence s1: "Some d = inv_map \<pi> i"
[PROOF STATE]
proof (prove)
using this:
Some d = inv_map \<pi> i

goal (1 subgoal):
 1. Some d = inv_map \<pi> i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Some d = inv_map \<pi> i

goal (1 subgoal):
 1. \<And>option. Some option = inv_map \<pi> i \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
show "(case inv_map \<pi> i of None \<Rightarrow> 0| Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j
           = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
proof(induction "\<pi> j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. None = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
 2. \<And>option. Some option = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
None = \<pi> j

goal (2 subgoals):
 1. None = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
 2. \<And>option. Some option = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
have "d \<noteq> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<noteq> j
[PROOF STEP]
proof(rule classical)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> d \<noteq> j \<Longrightarrow> d \<noteq> j
[PROOF STEP]
assume "\<not>(d \<noteq> j)"
[PROOF STATE]
proof (state)
this:
\<not> d \<noteq> j

goal (1 subgoal):
 1. \<not> d \<noteq> j \<Longrightarrow> d \<noteq> j
[PROOF STEP]
hence "d = j"
[PROOF STATE]
proof (prove)
using this:
\<not> d \<noteq> j

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

goal (1 subgoal):
 1. \<not> d \<noteq> j \<Longrightarrow> d \<noteq> j
[PROOF STEP]
hence "\<pi> d = \<pi> j"
[PROOF STATE]
proof (prove)
using this:
d = j

goal (1 subgoal):
 1. \<pi> d = \<pi> j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> d = \<pi> j

goal (1 subgoal):
 1. \<not> d \<noteq> j \<Longrightarrow> d \<noteq> j
[PROOF STEP]
hence "\<pi> d = None"
[PROOF STATE]
proof (prove)
using this:
\<pi> d = \<pi> j

goal (1 subgoal):
 1. \<pi> d = None
[PROOF STEP]
by (simp add: None.hyps)
[PROOF STATE]
proof (state)
this:
\<pi> d = None

goal (1 subgoal):
 1. \<not> d \<noteq> j \<Longrightarrow> d \<noteq> j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi> d = None

goal (1 subgoal):
 1. \<not> d \<noteq> j \<Longrightarrow> d \<noteq> j
[PROOF STEP]
have "\<pi> d = Some i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> d = Some i
[PROOF STEP]
using Some.hyps
[PROOF STATE]
proof (prove)
using this:
Some d = inv_map \<pi> i

goal (1 subgoal):
 1. \<pi> d = Some i
[PROOF STEP]
unfolding inv_map_def
[PROOF STATE]
proof (prove)
using this:
Some d = (if Some i \<in> range \<pi> then Some (inv \<pi> (Some i)) else None)

goal (1 subgoal):
 1. \<pi> d = Some i
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some d = (if Some i \<in> range \<pi> then Some (inv \<pi> (Some i)) else None) \<Longrightarrow> \<pi> d = Some i
[PROOF STEP]
by (metis f_inv_into_f option.distinct(1) option.inject)
[PROOF STATE]
proof (state)
this:
\<pi> d = Some i

goal (1 subgoal):
 1. \<not> d \<noteq> j \<Longrightarrow> d \<noteq> j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pi> d = None
\<pi> d = Some i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pi> d = None
\<pi> d = Some i

goal (1 subgoal):
 1. d \<noteq> j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d \<noteq> j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
d \<noteq> j

goal (2 subgoals):
 1. None = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
 2. \<And>option. Some option = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
d \<noteq> j

goal (1 subgoal):
 1. (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
by (metis None.hyps Some.hyps cinner_zero_right orthogonal_ket option.case_eq_if
              option.simps(5))
[PROOF STATE]
proof (state)
this:
(case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)

goal (1 subgoal):
 1. \<And>option. Some option = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>option. Some option = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
case (Some c)
[PROOF STATE]
proof (state)
this:
Some c = \<pi> j

goal (1 subgoal):
 1. \<And>option. Some option = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
hence s2: "\<pi> j = Some c"
[PROOF STATE]
proof (prove)
using this:
Some c = \<pi> j

goal (1 subgoal):
 1. \<pi> j = Some c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> j = Some c

goal (1 subgoal):
 1. \<And>option. Some option = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
have "(ket d \<bullet>\<^sub>C ket j) = (ket i \<bullet>\<^sub>C ket c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
[PROOF STEP]
proof(cases "\<pi> j = Some i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<pi> j = Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
 2. \<pi> j \<noteq> Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<pi> j = Some i

goal (2 subgoals):
 1. \<pi> j = Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
 2. \<pi> j \<noteq> Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
[PROOF STEP]
hence ij: "Some j = inv_map \<pi> i"
[PROOF STATE]
proof (prove)
using this:
\<pi> j = Some i

goal (1 subgoal):
 1. Some j = inv_map \<pi> i
[PROOF STEP]
unfolding inv_map_def
[PROOF STATE]
proof (prove)
using this:
\<pi> j = Some i

goal (1 subgoal):
 1. Some j = (if Some i \<in> range \<pi> then Some (inv \<pi> (Some i)) else None)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<pi> j = \<pi> x; Some i = \<pi> x\<rbrakk> \<Longrightarrow> j = inv \<pi> (\<pi> x)
 2. \<pi> j = Some i \<Longrightarrow> Some i \<in> range \<pi>
[PROOF STEP]
apply (metis a1 f_inv_into_f inj_map_def option.discI range_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> j = Some i \<Longrightarrow> Some i \<in> range \<pi>
[PROOF STEP]
by (metis range_eqI)
[PROOF STATE]
proof (state)
this:
Some j = inv_map \<pi> i

goal (2 subgoals):
 1. \<pi> j = Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
 2. \<pi> j \<noteq> Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
[PROOF STEP]
have "i = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = c
[PROOF STEP]
using True s2
[PROOF STATE]
proof (prove)
using this:
\<pi> j = Some i
\<pi> j = Some c

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

goal (2 subgoals):
 1. \<pi> j = Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
 2. \<pi> j \<noteq> Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i = c

goal (2 subgoals):
 1. \<pi> j = Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
 2. \<pi> j \<noteq> Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
[PROOF STEP]
have "j = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j = d
[PROOF STEP]
by (metis option.inject s1 ij)
[PROOF STATE]
proof (state)
this:
j = d

goal (2 subgoals):
 1. \<pi> j = Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
 2. \<pi> j \<noteq> Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i = c
j = d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = c
j = d

goal (1 subgoal):
 1. ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
[PROOF STEP]
by (simp add: cinner_ket_same)
[PROOF STATE]
proof (state)
this:
ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c

goal (1 subgoal):
 1. \<pi> j \<noteq> Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> j \<noteq> Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<pi> j \<noteq> Some i

goal (1 subgoal):
 1. \<pi> j \<noteq> Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi> j \<noteq> Some i

goal (1 subgoal):
 1. \<pi> j \<noteq> Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
[PROOF STEP]
have "\<pi> d = Some i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> d = Some i
[PROOF STEP]
using s1
[PROOF STATE]
proof (prove)
using this:
Some d = inv_map \<pi> i

goal (1 subgoal):
 1. \<pi> d = Some i
[PROOF STEP]
unfolding inv_map_def
[PROOF STATE]
proof (prove)
using this:
Some d = (if Some i \<in> range \<pi> then Some (inv \<pi> (Some i)) else None)

goal (1 subgoal):
 1. \<pi> d = Some i
[PROOF STEP]
by (metis f_inv_into_f option.distinct(1) option.inject)
[PROOF STATE]
proof (state)
this:
\<pi> d = Some i

goal (1 subgoal):
 1. \<pi> j \<noteq> Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pi> j \<noteq> Some i
\<pi> d = Some i
[PROOF STEP]
have "j \<noteq> d"
[PROOF STATE]
proof (prove)
using this:
\<pi> j \<noteq> Some i
\<pi> d = Some i

goal (1 subgoal):
 1. j \<noteq> d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j \<noteq> d

goal (1 subgoal):
 1. \<pi> j \<noteq> Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j \<noteq> d

goal (1 subgoal):
 1. \<pi> j \<noteq> Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
[PROOF STEP]
have "i \<noteq> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<noteq> c
[PROOF STEP]
using False s2
[PROOF STATE]
proof (prove)
using this:
\<pi> j \<noteq> Some i
\<pi> j = Some c

goal (1 subgoal):
 1. i \<noteq> c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<noteq> c

goal (1 subgoal):
 1. \<pi> j \<noteq> Some i \<Longrightarrow> ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j \<noteq> d
i \<noteq> c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
j \<noteq> d
i \<noteq> c

goal (1 subgoal):
 1. ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c
[PROOF STEP]
by (metis orthogonal_ket)
[PROOF STATE]
proof (state)
this:
ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c

goal (1 subgoal):
 1. \<And>option. Some option = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
hence "(case Some d of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j
             = ket i \<bullet>\<^sub>C (case Some c of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)"
[PROOF STATE]
proof (prove)
using this:
ket d \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C ket c

goal (1 subgoal):
 1. (case Some d of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case Some c of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(case Some d of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case Some c of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)

goal (1 subgoal):
 1. \<And>option. Some option = \<pi> j \<Longrightarrow> (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
thus "(case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j
             = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)"
[PROOF STATE]
proof (prove)
using this:
(case Some d of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case Some c of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)

goal (1 subgoal):
 1. (case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)
[PROOF STEP]
by (simp add: Some.hyps s1)
[PROOF STATE]
proof (state)
this:
(case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(case inv_map \<pi> i of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some a \<Rightarrow> ket a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(case inv_map \<pi> i of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k)

goal (1 subgoal):
 1. (F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(case inv_map \<pi> i of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k)

goal (1 subgoal):
 1. (F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)
[PROOF STEP]
have "\<dots> = ket i \<bullet>\<^sub>C (classical_operator \<pi> *\<^sub>V ket j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k) = ket i \<bullet>\<^sub>C (classical_operator \<pi> *\<^sub>V ket j)
[PROOF STEP]
by (simp add: w2)
[PROOF STATE]
proof (state)
this:
ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k) = ket i \<bullet>\<^sub>C (classical_operator \<pi> *\<^sub>V ket j)

goal (1 subgoal):
 1. (F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ket i \<bullet>\<^sub>C (case \<pi> j of None \<Rightarrow> 0 | Some k \<Rightarrow> ket k) = ket i \<bullet>\<^sub>C (classical_operator \<pi> *\<^sub>V ket j)

goal (1 subgoal):
 1. (F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)
[PROOF STEP]
have "\<dots> = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C (classical_operator \<pi> *\<^sub>V ket j) = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)
[PROOF STEP]
unfolding G_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ket i \<bullet>\<^sub>C (classical_operator \<pi> *\<^sub>V ket j) = ket i \<bullet>\<^sub>C (classical_operator \<pi> *\<^sub>V ket j)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ket i \<bullet>\<^sub>C (classical_operator \<pi> *\<^sub>V ket j) = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)

goal (1 subgoal):
 1. (F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)

goal (1 subgoal):
 1. (F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (G *\<^sub>V ket j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(F *\<^sub>V ket ?i) \<bullet>\<^sub>C ket ?j = ket ?i \<bullet>\<^sub>C (G *\<^sub>V ket ?j)

goal (1 subgoal):
 1. classical_operator \<pi>* = classical_operator (inv_map \<pi>)
[PROOF STEP]
hence "G* = F"
[PROOF STATE]
proof (prove)
using this:
(F *\<^sub>V ket ?i) \<bullet>\<^sub>C ket ?j = ket ?i \<bullet>\<^sub>C (G *\<^sub>V ket ?j)

goal (1 subgoal):
 1. G* = F
[PROOF STEP]
using cinner_ket_adjointI
[PROOF STATE]
proof (prove)
using this:
(F *\<^sub>V ket ?i) \<bullet>\<^sub>C ket ?j = ket ?i \<bullet>\<^sub>C (G *\<^sub>V ket ?j)
(\<And>i j. (?F *\<^sub>V ket i) \<bullet>\<^sub>C ket j = ket i \<bullet>\<^sub>C (?G *\<^sub>V ket j)) \<Longrightarrow> ?F = ?G*

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

goal (1 subgoal):
 1. classical_operator \<pi>* = classical_operator (inv_map \<pi>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
G* = F

goal (1 subgoal):
 1. classical_operator \<pi>* = classical_operator (inv_map \<pi>)
[PROOF STEP]
unfolding G_def F_def
[PROOF STATE]
proof (prove)
using this:
classical_operator \<pi>* = classical_operator (inv_map \<pi>)

goal (1 subgoal):
 1. classical_operator \<pi>* = classical_operator (inv_map \<pi>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
classical_operator \<pi>* = classical_operator (inv_map \<pi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma classical_operator_Some[simp]: "classical_operator (Some::'a\<Rightarrow>_) = id_cblinfun"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator Some = id_cblinfun
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. classical_operator Some = id_cblinfun
[PROOF STEP]
have "(classical_operator Some) *\<^sub>V (ket i)  = id_cblinfun *\<^sub>V (ket i)"
    for i::'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator Some *\<^sub>V ket i = id_cblinfun *\<^sub>V ket i
[PROOF STEP]
apply (subst classical_operator_ket)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. classical_operator_exists Some
 2. (case Some i of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) = id_cblinfun *\<^sub>V ket i
[PROOF STEP]
apply (rule classical_operator_exists_inj)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. inj_map Some
 2. (case Some i of None \<Rightarrow> 0 | Some x \<Rightarrow> ket x) = id_cblinfun *\<^sub>V ket i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
classical_operator Some *\<^sub>V ket ?i = id_cblinfun *\<^sub>V ket ?i

goal (1 subgoal):
 1. classical_operator Some = id_cblinfun
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
classical_operator Some *\<^sub>V ket ?i = id_cblinfun *\<^sub>V ket ?i

goal (1 subgoal):
 1. classical_operator Some = id_cblinfun
[PROOF STEP]
using equal_ket[where A = "classical_operator (Some::'a \<Rightarrow> _ option)"
        and B = "id_cblinfun::'a ell2 \<Rightarrow>\<^sub>C\<^sub>L _"]
[PROOF STATE]
proof (prove)
using this:
classical_operator Some *\<^sub>V ket ?i = id_cblinfun *\<^sub>V ket ?i
(\<And>x. classical_operator Some *\<^sub>V ket x = id_cblinfun *\<^sub>V ket x) \<Longrightarrow> classical_operator Some = id_cblinfun

goal (1 subgoal):
 1. classical_operator Some = id_cblinfun
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
classical_operator Some = id_cblinfun

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isometry_classical_operator[simp]:
  fixes \<pi>::"'a \<Rightarrow> 'b"
  assumes a1: "inj \<pi>"
  shows "isometry (classical_operator (Some o \<pi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry (classical_operator (Some \<circ> \<pi>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. isometry (classical_operator (Some \<circ> \<pi>))
[PROOF STEP]
have b0: "inj_map (Some \<circ> \<pi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_map (Some \<circ> \<pi>)
[PROOF STEP]
by (simp add: a1)
[PROOF STATE]
proof (state)
this:
inj_map (Some \<circ> \<pi>)

goal (1 subgoal):
 1. isometry (classical_operator (Some \<circ> \<pi>))
[PROOF STEP]
have b0': "inj_map (inv_map (Some \<circ> \<pi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_map (inv_map (Some \<circ> \<pi>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inj_map (inv_map (Some \<circ> \<pi>))

goal (1 subgoal):
 1. isometry (classical_operator (Some \<circ> \<pi>))
[PROOF STEP]
have b1: "inv_map (Some \<circ> \<pi>) \<circ>\<^sub>m (Some \<circ> \<pi>) = Some"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_map (Some \<circ> \<pi>) \<circ>\<^sub>m (Some \<circ> \<pi>) = Some
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (inv_map (Some \<circ> \<pi>) \<circ>\<^sub>m (Some \<circ> \<pi>)) x = Some x
[PROOF STEP]
unfolding inv_map_def o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. ((\<lambda>y. if Some y \<in> range (\<lambda>x. Some (\<pi> x)) then Some (inv (\<lambda>x. Some (\<pi> x)) (Some y)) else None) \<circ>\<^sub>m (\<lambda>x. Some (\<pi> x))) x = Some x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
inj \<pi>

goal (1 subgoal):
 1. \<And>x. ((\<lambda>y. if Some y \<in> range (\<lambda>x. Some (\<pi> x)) then Some (inv (\<lambda>x. Some (\<pi> x)) (Some y)) else None) \<circ>\<^sub>m (\<lambda>x. Some (\<pi> x))) x = Some x
[PROOF STEP]
unfolding inj_def inv_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. \<pi> x = \<pi> y \<longrightarrow> x = y

goal (1 subgoal):
 1. \<And>x. ((\<lambda>y. if Some y \<in> range (\<lambda>x. Some (\<pi> x)) then Some (SOME x. Some (\<pi> x) = Some y) else None) \<circ>\<^sub>m (\<lambda>x. Some (\<pi> x))) x = Some x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_map (Some \<circ> \<pi>) \<circ>\<^sub>m (Some \<circ> \<pi>) = Some

goal (1 subgoal):
 1. isometry (classical_operator (Some \<circ> \<pi>))
[PROOF STEP]
have b3: "classical_operator (inv_map (Some \<circ> \<pi>)) o\<^sub>C\<^sub>L
            classical_operator (Some \<circ> \<pi>) = classical_operator (inv_map (Some \<circ> \<pi>) \<circ>\<^sub>m (Some \<circ> \<pi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator (inv_map (Some \<circ> \<pi>)) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = classical_operator (inv_map (Some \<circ> \<pi>) \<circ>\<^sub>m (Some \<circ> \<pi>))
[PROOF STEP]
by (metis b0 b0' b1 classical_operator_Some classical_operator_exists_inj
        classical_operator_mult)
[PROOF STATE]
proof (state)
this:
classical_operator (inv_map (Some \<circ> \<pi>)) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = classical_operator (inv_map (Some \<circ> \<pi>) \<circ>\<^sub>m (Some \<circ> \<pi>))

goal (1 subgoal):
 1. isometry (classical_operator (Some \<circ> \<pi>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry (classical_operator (Some \<circ> \<pi>))
[PROOF STEP]
unfolding isometry_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>)* o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = id_cblinfun
[PROOF STEP]
apply (subst classical_operator_adjoint)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. inj_map (Some \<circ> \<pi>)
 2. classical_operator (inv_map (Some \<circ> \<pi>)) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = id_cblinfun
[PROOF STEP]
using b0
[PROOF STATE]
proof (prove)
using this:
inj_map (Some \<circ> \<pi>)

goal (2 subgoals):
 1. inj_map (Some \<circ> \<pi>)
 2. classical_operator (inv_map (Some \<circ> \<pi>)) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = id_cblinfun
[PROOF STEP]
by (auto simp add: b1 b3)
[PROOF STATE]
proof (state)
this:
isometry (classical_operator (Some \<circ> \<pi>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unitary_classical_operator[simp]:
  fixes \<pi>::"'a \<Rightarrow> 'b"
  assumes a1: "bij \<pi>"
  shows "unitary (classical_operator (Some o \<pi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary (classical_operator (Some \<circ> \<pi>))
[PROOF STEP]
proof (unfold unitary_def, rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. classical_operator (Some \<circ> \<pi>)* o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = id_cblinfun
 2. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun
[PROOF STEP]
have "inj \<pi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj \<pi>
[PROOF STEP]
using a1 bij_betw_imp_inj_on
[PROOF STATE]
proof (prove)
using this:
bij \<pi>
bij_betw ?f ?A ?B \<Longrightarrow> inj_on ?f ?A

goal (1 subgoal):
 1. inj \<pi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj \<pi>

goal (2 subgoals):
 1. classical_operator (Some \<circ> \<pi>)* o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = id_cblinfun
 2. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun
[PROOF STEP]
hence "isometry (classical_operator (Some o \<pi>))"
[PROOF STATE]
proof (prove)
using this:
inj \<pi>

goal (1 subgoal):
 1. isometry (classical_operator (Some \<circ> \<pi>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
isometry (classical_operator (Some \<circ> \<pi>))

goal (2 subgoals):
 1. classical_operator (Some \<circ> \<pi>)* o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = id_cblinfun
 2. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun
[PROOF STEP]
hence "classical_operator (Some \<circ> \<pi>)* o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = id_cblinfun"
[PROOF STATE]
proof (prove)
using this:
isometry (classical_operator (Some \<circ> \<pi>))

goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>)* o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = id_cblinfun
[PROOF STEP]
unfolding isometry_def
[PROOF STATE]
proof (prove)
using this:
classical_operator (Some \<circ> \<pi>)* o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = id_cblinfun

goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>)* o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = id_cblinfun
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
classical_operator (Some \<circ> \<pi>)* o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = id_cblinfun

goal (2 subgoals):
 1. classical_operator (Some \<circ> \<pi>)* o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = id_cblinfun
 2. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun
[PROOF STEP]
thus \<open>classical_operator (Some \<circ> \<pi>)* o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = id_cblinfun\<close>
[PROOF STATE]
proof (prove)
using this:
classical_operator (Some \<circ> \<pi>)* o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = id_cblinfun

goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>)* o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = id_cblinfun
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
classical_operator (Some \<circ> \<pi>)* o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>) = id_cblinfun

goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun
[PROOF STEP]
have "inj \<pi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj \<pi>
[PROOF STEP]
by (simp add: assms bij_is_inj)
[PROOF STATE]
proof (state)
this:
inj \<pi>

goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun
[PROOF STEP]
have comp: "Some \<circ> \<pi> \<circ>\<^sub>m inv_map (Some \<circ> \<pi>) = Some"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some \<circ> \<pi> \<circ>\<^sub>m inv_map (Some \<circ> \<pi>) = Some
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (Some \<circ> \<pi> \<circ>\<^sub>m inv_map (Some \<circ> \<pi>)) x = Some x
[PROOF STEP]
unfolding inv_map_def o_def map_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (case if Some x \<in> range (\<lambda>x. Some (\<pi> x)) then Some (inv (\<lambda>x. Some (\<pi> x)) (Some x)) else None of None \<Rightarrow> None | Some x \<Rightarrow> Some (\<pi> x)) = Some x
[PROOF STEP]
unfolding inv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (case if Some x \<in> range (\<lambda>x. Some (\<pi> x)) then Some (SOME xa. Some (\<pi> xa) = Some x) else None of None \<Rightarrow> None | Some x \<Rightarrow> Some (\<pi> x)) = Some x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<pi> (SOME x. \<pi> x = \<pi> xa) = \<pi> xa
 2. \<And>x. Some x \<in> range (\<lambda>x. Some (\<pi> x))
[PROOF STEP]
apply (metis \<open>inj \<pi>\<close> inv_def inv_f_f)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. Some x \<in> range (\<lambda>x. Some (\<pi> x))
[PROOF STEP]
using bij_def image_iff range_eqI
[PROOF STATE]
proof (prove)
using this:
bij ?f = (inj ?f \<and> surj ?f)
(?z \<in> ?f ` ?A) = (\<exists>x\<in>?A. ?z = ?f x)
?b = ?f ?x \<Longrightarrow> ?b \<in> range ?f

goal (1 subgoal):
 1. \<And>x. Some x \<in> range (\<lambda>x. Some (\<pi> x))
[PROOF STEP]
by (metis a1)
[PROOF STATE]
proof (state)
this:
Some \<circ> \<pi> \<circ>\<^sub>m inv_map (Some \<circ> \<pi>) = Some

goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun
[PROOF STEP]
have "classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)*
      = classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (inv_map (Some \<circ> \<pi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (inv_map (Some \<circ> \<pi>))
[PROOF STEP]
by (simp add: \<open>inj \<pi>\<close>)
[PROOF STATE]
proof (state)
this:
classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (inv_map (Some \<circ> \<pi>))

goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (inv_map (Some \<circ> \<pi>))

goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun
[PROOF STEP]
have "\<dots> = classical_operator ((Some \<circ> \<pi>) \<circ>\<^sub>m (inv_map (Some \<circ> \<pi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (inv_map (Some \<circ> \<pi>)) = classical_operator (Some \<circ> \<pi> \<circ>\<^sub>m inv_map (Some \<circ> \<pi>))
[PROOF STEP]
by (simp add: \<open>inj \<pi>\<close> classical_operator_exists_inj)
[PROOF STATE]
proof (state)
this:
classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (inv_map (Some \<circ> \<pi>)) = classical_operator (Some \<circ> \<pi> \<circ>\<^sub>m inv_map (Some \<circ> \<pi>))

goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (inv_map (Some \<circ> \<pi>)) = classical_operator (Some \<circ> \<pi> \<circ>\<^sub>m inv_map (Some \<circ> \<pi>))

goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun
[PROOF STEP]
have "\<dots> = classical_operator (Some::'b\<Rightarrow>_)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi> \<circ>\<^sub>m inv_map (Some \<circ> \<pi>)) = classical_operator Some
[PROOF STEP]
using comp
[PROOF STATE]
proof (prove)
using this:
Some \<circ> \<pi> \<circ>\<^sub>m inv_map (Some \<circ> \<pi>) = Some

goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi> \<circ>\<^sub>m inv_map (Some \<circ> \<pi>)) = classical_operator Some
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
classical_operator (Some \<circ> \<pi> \<circ>\<^sub>m inv_map (Some \<circ> \<pi>)) = classical_operator Some

goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
classical_operator (Some \<circ> \<pi> \<circ>\<^sub>m inv_map (Some \<circ> \<pi>)) = classical_operator Some

goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun
[PROOF STEP]
have "\<dots> = (id_cblinfun:: 'b ell2 \<Rightarrow>\<^sub>C\<^sub>L _)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. classical_operator Some = id_cblinfun
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
classical_operator Some = id_cblinfun

goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun
[PROOF STEP]
show "classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun"
[PROOF STATE]
proof (prove)
using this:
classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun

goal (1 subgoal):
 1. classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
classical_operator (Some \<circ> \<pi>) o\<^sub>C\<^sub>L classical_operator (Some \<circ> \<pi>)* = id_cblinfun

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma AX01: "AX0 \<subseteq> AX1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AX0 \<subseteq> AX1
[PROOF STEP]
by (simp add: AX1.intros(1) subsetI)


[STATEMENT]
lemma AX1_away: "AX1 \<union> \<Gamma> = AX0 \<union> (\<Gamma> \<union> AX1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AX1 \<union> \<Gamma> = AX0 \<union> (\<Gamma> \<union> AX1)
[PROOF STEP]
using AX01
[PROOF STATE]
proof (prove)
using this:
AX0 \<subseteq> AX1

goal (1 subgoal):
 1. AX1 \<union> \<Gamma> = AX0 \<union> (\<Gamma> \<union> AX1)
[PROOF STEP]
by blast


[STATEMENT]
lemma Deduction1: "F \<triangleright> (AX1 \<union> \<Gamma> ) \<turnstile>\<^sub>H \<bottom> \<longleftrightarrow> (AX1 \<union> \<Gamma>) \<turnstile>\<^sub>H (F \<^bold>\<rightarrow> \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (F \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>) = (AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<bottom>)
[PROOF STEP]
unfolding AX1_away
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (F \<triangleright> AX0 \<union> (\<Gamma> \<union> AX1) \<turnstile>\<^sub>H \<bottom>) = (AX0 \<union> (\<Gamma> \<union> AX1) \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<bottom>)
[PROOF STEP]
by (metis Deduction_theorem HC.simps HC_mono Un_commute Un_insert_left insertI1 subset_insertI)