[STATEMENT]
lemma ptensor_encode1_encode2:
  "partial_state.encode1 dims0 vars1' = partial_state.encode2 dims0 vars2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode1 dims0 vars1' = partial_state.encode2 dims0 vars2'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partial_state.encode1 dims0 vars1' = partial_state.encode2 dims0 vars2'
[PROOF STEP]
have "partial_state.encode1 dims0 vars1' i
    = digit_decode (partial_state.dims1 dims0 vars1') (nths (digit_encode dims0 i) ({0..<length dims0} \<inter> vars1'))" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode1 dims0 vars1' i = digit_decode (partial_state.dims1 dims0 vars1') (nths (digit_encode dims0 i) ({0..<length dims0} \<inter> vars1'))
[PROOF STEP]
using partial_state.encode1_alter
[PROOF STATE]
proof (prove)
using this:
{0..<length ?dims} \<subseteq> ?A \<Longrightarrow> partial_state.encode1 ?dims ?vars ?i = digit_decode (partial_state.dims1 ?dims ?vars) (nths (digit_encode ?dims ?i) (?A \<inter> ?vars))

goal (1 subgoal):
 1. partial_state.encode1 dims0 vars1' i = digit_decode (partial_state.dims1 dims0 vars1') (nths (digit_encode dims0 i) ({0..<length dims0} \<inter> vars1'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.encode1 dims0 vars1' ?i = digit_decode (partial_state.dims1 dims0 vars1') (nths (digit_encode dims0 ?i) ({0..<length dims0} \<inter> vars1'))

goal (1 subgoal):
 1. partial_state.encode1 dims0 vars1' = partial_state.encode2 dims0 vars2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
partial_state.encode1 dims0 vars1' ?i = digit_decode (partial_state.dims1 dims0 vars1') (nths (digit_encode dims0 ?i) ({0..<length dims0} \<inter> vars1'))

goal (1 subgoal):
 1. partial_state.encode1 dims0 vars1' = partial_state.encode2 dims0 vars2'
[PROOF STEP]
have "partial_state.encode2 dims0 vars2' i
    = digit_decode (partial_state.dims2 dims0 vars2') (nths (digit_encode dims0 i) ({0..<length dims0} - vars2'))" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode2 dims0 vars2' i = digit_decode (partial_state.dims2 dims0 vars2') (nths (digit_encode dims0 i) ({0..<length dims0} - vars2'))
[PROOF STEP]
using partial_state.encode2_alter
[PROOF STATE]
proof (prove)
using this:
{0..<length ?dims} \<subseteq> ?A \<Longrightarrow> partial_state.encode2 ?dims ?vars ?i = digit_decode (partial_state.dims2 ?dims ?vars) (nths (digit_encode ?dims ?i) (?A - ?vars))

goal (1 subgoal):
 1. partial_state.encode2 dims0 vars2' i = digit_decode (partial_state.dims2 dims0 vars2') (nths (digit_encode dims0 i) ({0..<length dims0} - vars2'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.encode2 dims0 vars2' ?i = digit_decode (partial_state.dims2 dims0 vars2') (nths (digit_encode dims0 ?i) ({0..<length dims0} - vars2'))

goal (1 subgoal):
 1. partial_state.encode1 dims0 vars1' = partial_state.encode2 dims0 vars2'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
partial_state.encode2 dims0 vars2' ?i = digit_decode (partial_state.dims2 dims0 vars2') (nths (digit_encode dims0 ?i) ({0..<length dims0} - vars2'))

goal (1 subgoal):
 1. partial_state.encode1 dims0 vars1' = partial_state.encode2 dims0 vars2'
[PROOF STEP]
have "partial_state.dims1 dims0 vars1' = partial_state.dims2 dims0 vars2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.dims1 dims0 vars1' = partial_state.dims2 dims0 vars2'
[PROOF STEP]
unfolding partial_state.dims1_def partial_state.dims2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths dims0 vars1' = nths dims0 (- vars2')
[PROOF STEP]
using nths_vars1' nths_vars1'_comp
[PROOF STATE]
proof (prove)
using this:
nths dims0 vars1' = dims1
nths dims0 (- vars2') = dims1

goal (1 subgoal):
 1. nths dims0 vars1' = nths dims0 (- vars2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.dims1 dims0 vars1' = partial_state.dims2 dims0 vars2'

goal (1 subgoal):
 1. partial_state.encode1 dims0 vars1' = partial_state.encode2 dims0 vars2'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
partial_state.encode1 dims0 vars1' ?i = digit_decode (partial_state.dims1 dims0 vars1') (nths (digit_encode dims0 ?i) ({0..<length dims0} \<inter> vars1'))
partial_state.encode2 dims0 vars2' ?i = digit_decode (partial_state.dims2 dims0 vars2') (nths (digit_encode dims0 ?i) ({0..<length dims0} - vars2'))
partial_state.dims1 dims0 vars1' = partial_state.dims2 dims0 vars2'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
partial_state.encode1 dims0 vars1' ?i = digit_decode (partial_state.dims1 dims0 vars1') (nths (digit_encode dims0 ?i) ({0..<length dims0} \<inter> vars1'))
partial_state.encode2 dims0 vars2' ?i = digit_decode (partial_state.dims2 dims0 vars2') (nths (digit_encode dims0 ?i) ({0..<length dims0} - vars2'))
partial_state.dims1 dims0 vars1' = partial_state.dims2 dims0 vars2'

goal (1 subgoal):
 1. partial_state.encode1 dims0 vars1' = partial_state.encode2 dims0 vars2'
[PROOF STEP]
using length_dims0_minus_vars2'_is_vars1'
[PROOF STATE]
proof (prove)
using this:
partial_state.encode1 dims0 vars1' ?i = digit_decode (partial_state.dims1 dims0 vars1') (nths (digit_encode dims0 ?i) ({0..<length dims0} \<inter> vars1'))
partial_state.encode2 dims0 vars2' ?i = digit_decode (partial_state.dims2 dims0 vars2') (nths (digit_encode dims0 ?i) ({0..<length dims0} - vars2'))
partial_state.dims1 dims0 vars1' = partial_state.dims2 dims0 vars2'
{0..<length dims0} - vars2' = {0..<length dims0} \<inter> vars1'

goal (1 subgoal):
 1. partial_state.encode1 dims0 vars1' = partial_state.encode2 dims0 vars2'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.encode1 dims0 vars1' = partial_state.encode2 dims0 vars2'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ptensor_encode2_encode1:
  "partial_state.encode1 dims0 vars2' = partial_state.encode2 dims0 vars1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode1 dims0 vars2' = partial_state.encode2 dims0 vars1'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partial_state.encode1 dims0 vars2' = partial_state.encode2 dims0 vars1'
[PROOF STEP]
have "partial_state.encode1 dims0 vars2' i
    = digit_decode (partial_state.dims1 dims0 vars2') (nths (digit_encode dims0 i) ({0..<length dims0} \<inter> vars2'))" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode1 dims0 vars2' i = digit_decode (partial_state.dims1 dims0 vars2') (nths (digit_encode dims0 i) ({0..<length dims0} \<inter> vars2'))
[PROOF STEP]
using partial_state.encode1_alter
[PROOF STATE]
proof (prove)
using this:
{0..<length ?dims} \<subseteq> ?A \<Longrightarrow> partial_state.encode1 ?dims ?vars ?i = digit_decode (partial_state.dims1 ?dims ?vars) (nths (digit_encode ?dims ?i) (?A \<inter> ?vars))

goal (1 subgoal):
 1. partial_state.encode1 dims0 vars2' i = digit_decode (partial_state.dims1 dims0 vars2') (nths (digit_encode dims0 i) ({0..<length dims0} \<inter> vars2'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.encode1 dims0 vars2' ?i = digit_decode (partial_state.dims1 dims0 vars2') (nths (digit_encode dims0 ?i) ({0..<length dims0} \<inter> vars2'))

goal (1 subgoal):
 1. partial_state.encode1 dims0 vars2' = partial_state.encode2 dims0 vars1'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
partial_state.encode1 dims0 vars2' ?i = digit_decode (partial_state.dims1 dims0 vars2') (nths (digit_encode dims0 ?i) ({0..<length dims0} \<inter> vars2'))

goal (1 subgoal):
 1. partial_state.encode1 dims0 vars2' = partial_state.encode2 dims0 vars1'
[PROOF STEP]
have "partial_state.encode2 dims0 vars1' i
    = digit_decode (partial_state.dims2 dims0 vars1') (nths (digit_encode dims0 i) ({0..<length dims0} - vars1'))" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode2 dims0 vars1' i = digit_decode (partial_state.dims2 dims0 vars1') (nths (digit_encode dims0 i) ({0..<length dims0} - vars1'))
[PROOF STEP]
using partial_state.encode2_alter
[PROOF STATE]
proof (prove)
using this:
{0..<length ?dims} \<subseteq> ?A \<Longrightarrow> partial_state.encode2 ?dims ?vars ?i = digit_decode (partial_state.dims2 ?dims ?vars) (nths (digit_encode ?dims ?i) (?A - ?vars))

goal (1 subgoal):
 1. partial_state.encode2 dims0 vars1' i = digit_decode (partial_state.dims2 dims0 vars1') (nths (digit_encode dims0 i) ({0..<length dims0} - vars1'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.encode2 dims0 vars1' ?i = digit_decode (partial_state.dims2 dims0 vars1') (nths (digit_encode dims0 ?i) ({0..<length dims0} - vars1'))

goal (1 subgoal):
 1. partial_state.encode1 dims0 vars2' = partial_state.encode2 dims0 vars1'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
partial_state.encode2 dims0 vars1' ?i = digit_decode (partial_state.dims2 dims0 vars1') (nths (digit_encode dims0 ?i) ({0..<length dims0} - vars1'))

goal (1 subgoal):
 1. partial_state.encode1 dims0 vars2' = partial_state.encode2 dims0 vars1'
[PROOF STEP]
have "partial_state.dims1 dims0 vars2' = partial_state.dims2 dims0 vars1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.dims1 dims0 vars2' = partial_state.dims2 dims0 vars1'
[PROOF STEP]
unfolding partial_state.dims1_def partial_state.dims2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths dims0 vars2' = nths dims0 (- vars1')
[PROOF STEP]
using nths_vars2' nths_vars2'_comp
[PROOF STATE]
proof (prove)
using this:
nths dims0 (- vars1') = dims2
nths dims0 vars2' = dims2

goal (1 subgoal):
 1. nths dims0 vars2' = nths dims0 (- vars1')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.dims1 dims0 vars2' = partial_state.dims2 dims0 vars1'

goal (1 subgoal):
 1. partial_state.encode1 dims0 vars2' = partial_state.encode2 dims0 vars1'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
partial_state.encode1 dims0 vars2' ?i = digit_decode (partial_state.dims1 dims0 vars2') (nths (digit_encode dims0 ?i) ({0..<length dims0} \<inter> vars2'))
partial_state.encode2 dims0 vars1' ?i = digit_decode (partial_state.dims2 dims0 vars1') (nths (digit_encode dims0 ?i) ({0..<length dims0} - vars1'))
partial_state.dims1 dims0 vars2' = partial_state.dims2 dims0 vars1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
partial_state.encode1 dims0 vars2' ?i = digit_decode (partial_state.dims1 dims0 vars2') (nths (digit_encode dims0 ?i) ({0..<length dims0} \<inter> vars2'))
partial_state.encode2 dims0 vars1' ?i = digit_decode (partial_state.dims2 dims0 vars1') (nths (digit_encode dims0 ?i) ({0..<length dims0} - vars1'))
partial_state.dims1 dims0 vars2' = partial_state.dims2 dims0 vars1'

goal (1 subgoal):
 1. partial_state.encode1 dims0 vars2' = partial_state.encode2 dims0 vars1'
[PROOF STEP]
using length_dims0_minus_vars1'_is_vars2'
[PROOF STATE]
proof (prove)
using this:
partial_state.encode1 dims0 vars2' ?i = digit_decode (partial_state.dims1 dims0 vars2') (nths (digit_encode dims0 ?i) ({0..<length dims0} \<inter> vars2'))
partial_state.encode2 dims0 vars1' ?i = digit_decode (partial_state.dims2 dims0 vars1') (nths (digit_encode dims0 ?i) ({0..<length dims0} - vars1'))
partial_state.dims1 dims0 vars2' = partial_state.dims2 dims0 vars1'
{0..<length dims0} - vars1' = {0..<length dims0} \<inter> vars2'

goal (1 subgoal):
 1. partial_state.encode1 dims0 vars2' = partial_state.encode2 dims0 vars1'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_state.encode1 dims0 vars2' = partial_state.encode2 dims0 vars1'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ptensor_vec_dim [simp]:
  "dim_vec (ptensor_vec v1 v2) = d0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (ptensor_vec v1 v2) = d0
[PROOF STEP]
by (simp add: ptensor_vec_def partial_state.tensor_vec_dim state_sig.d_def d0_def)


[STATEMENT]
lemma ptensor_vec_carrier:
  "ptensor_vec v1 v2 \<in> carrier_vec d0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ptensor_vec v1 v2 \<in> carrier_vec d0
[PROOF STEP]
by (simp add: carrier_dim_vec)


[STATEMENT]
lemma ptensor_vec_add:
  fixes v1 v2 v3 :: "'a::comm_ring vec"
  assumes "v1 \<in> carrier_vec d1"
    and "v2 \<in> carrier_vec d1"
    and "v3 \<in> carrier_vec d2"
  shows "ptensor_vec (v1 + v2) v3 = ptensor_vec v1 v3 + ptensor_vec v2 v3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ptensor_vec (v1 + v2) v3 = ptensor_vec v1 v3 + ptensor_vec v2 v3
[PROOF STEP]
unfolding ptensor_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.tensor_vec dims0 vars1' (v1 + v2) v3 = partial_state.tensor_vec dims0 vars1' v1 v3 + partial_state.tensor_vec dims0 vars1' v2 v3
[PROOF STEP]
apply (rule partial_state.tensor_vec_add1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. v1 \<in> carrier_vec (partial_state.d1 dims0 vars1')
 2. v2 \<in> carrier_vec (partial_state.d1 dims0 vars1')
 3. v3 \<in> carrier_vec (partial_state.d2 dims0 vars1')
[PROOF STEP]
unfolding partial_state.d1_def partial_state.d2_def
    partial_state.dims1_def partial_state.dims2_def nths_vars1' nths_vars2'
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. v1 \<in> carrier_vec (prod_list dims1)
 2. v2 \<in> carrier_vec (prod_list dims1)
 3. v3 \<in> carrier_vec (prod_list dims2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v1 \<in> carrier_vec d1
v2 \<in> carrier_vec d1
v3 \<in> carrier_vec d2

goal (3 subgoals):
 1. v1 \<in> carrier_vec (prod_list dims1)
 2. v2 \<in> carrier_vec (prod_list dims1)
 3. v3 \<in> carrier_vec (prod_list dims2)
[PROOF STEP]
unfolding d1_def d2_def
[PROOF STATE]
proof (prove)
using this:
v1 \<in> carrier_vec (prod_list dims1)
v2 \<in> carrier_vec (prod_list dims1)
v3 \<in> carrier_vec (prod_list dims2)

goal (3 subgoals):
 1. v1 \<in> carrier_vec (prod_list dims1)
 2. v2 \<in> carrier_vec (prod_list dims1)
 3. v3 \<in> carrier_vec (prod_list dims2)
[PROOF STEP]
by auto


[STATEMENT]
lemma ptensor_mat_dim_row [simp]:
  "dim_row (ptensor_mat m1 m2) = d0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (ptensor_mat m1 m2) = d0
[PROOF STEP]
by (simp add: ptensor_mat_def partial_state.tensor_mat_dim_row d0_def state_sig.d_def)


[STATEMENT]
lemma ptensor_mat_dim_col [simp]:
  "dim_col (ptensor_mat m1 m2) = d0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (ptensor_mat m1 m2) = d0
[PROOF STEP]
by (simp add: ptensor_mat_def partial_state.tensor_mat_dim_col d0_def state_sig.d_def)


[STATEMENT]
lemma ptensor_mat_carrier:
  "ptensor_mat m1 m2 \<in> carrier_mat d0 d0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ptensor_mat m1 m2 \<in> carrier_mat d0 d0
[PROOF STEP]
by (simp add: carrier_matI)


[STATEMENT]
lemma ptensor_mat_add:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d1 d1"
    and "m3 \<in> carrier_mat d2 d2"
  shows "ptensor_mat (m1 + m2) m3 = ptensor_mat m1 m3 + ptensor_mat m2 m3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ptensor_mat (m1 + m2) m3 = ptensor_mat m1 m3 + ptensor_mat m2 m3
[PROOF STEP]
unfolding ptensor_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat dims0 vars1' (m1 + m2) m3 = tensor_mat dims0 vars1' m1 m3 + tensor_mat dims0 vars1' m2 m3
[PROOF STEP]
apply (rule partial_state.tensor_mat_add1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. m1 \<in> carrier_mat (partial_state.d1 dims0 vars1') (partial_state.d1 dims0 vars1')
 2. m2 \<in> carrier_mat (partial_state.d1 dims0 vars1') (partial_state.d1 dims0 vars1')
 3. m3 \<in> carrier_mat (partial_state.d2 dims0 vars1') (partial_state.d2 dims0 vars1')
[PROOF STEP]
unfolding partial_state.d1_def partial_state.d2_def
    partial_state.dims1_def partial_state.dims2_def nths_vars1'
    nths_vars2'
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. m1 \<in> carrier_mat (prod_list dims1) (prod_list dims1)
 2. m2 \<in> carrier_mat (prod_list dims1) (prod_list dims1)
 3. m3 \<in> carrier_mat (prod_list dims2) (prod_list dims2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d1 d1
m3 \<in> carrier_mat d2 d2

goal (3 subgoals):
 1. m1 \<in> carrier_mat (prod_list dims1) (prod_list dims1)
 2. m2 \<in> carrier_mat (prod_list dims1) (prod_list dims1)
 3. m3 \<in> carrier_mat (prod_list dims2) (prod_list dims2)
[PROOF STEP]
unfolding d1_def d2_def
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat (prod_list dims1) (prod_list dims1)
m2 \<in> carrier_mat (prod_list dims1) (prod_list dims1)
m3 \<in> carrier_mat (prod_list dims2) (prod_list dims2)

goal (3 subgoals):
 1. m1 \<in> carrier_mat (prod_list dims1) (prod_list dims1)
 2. m2 \<in> carrier_mat (prod_list dims1) (prod_list dims1)
 3. m3 \<in> carrier_mat (prod_list dims2) (prod_list dims2)
[PROOF STEP]
by auto


[STATEMENT]
lemma ptensor_mat_trace:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d2 d2"
  shows "trace (ptensor_mat m1 m2) = trace m1 * trace m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (ptensor_mat m1 m2) = trace m1 * trace m2
[PROOF STEP]
unfolding ptensor_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (tensor_mat dims0 vars1' m1 m2) = trace m1 * trace m2
[PROOF STEP]
apply (rule partial_state.tensor_mat_trace)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. m1 \<in> carrier_mat (partial_state.d1 dims0 vars1') (partial_state.d1 dims0 vars1')
 2. m2 \<in> carrier_mat (partial_state.d2 dims0 vars1') (partial_state.d2 dims0 vars1')
[PROOF STEP]
unfolding partial_state.d1_def partial_state.d2_def
    partial_state.dims1_def partial_state.dims2_def nths_vars1' nths_vars2'
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. m1 \<in> carrier_mat (prod_list dims1) (prod_list dims1)
 2. m2 \<in> carrier_mat (prod_list dims2) (prod_list dims2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2

goal (2 subgoals):
 1. m1 \<in> carrier_mat (prod_list dims1) (prod_list dims1)
 2. m2 \<in> carrier_mat (prod_list dims2) (prod_list dims2)
[PROOF STEP]
unfolding d1_def d2_def
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat (prod_list dims1) (prod_list dims1)
m2 \<in> carrier_mat (prod_list dims2) (prod_list dims2)

goal (2 subgoals):
 1. m1 \<in> carrier_mat (prod_list dims1) (prod_list dims1)
 2. m2 \<in> carrier_mat (prod_list dims2) (prod_list dims2)
[PROOF STEP]
by auto


[STATEMENT]
lemma ptensor_mat_id:
  "ptensor_mat (1\<^sub>m d1) (1\<^sub>m d2) = 1\<^sub>m d0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ptensor_mat (1\<^sub>m d1) (1\<^sub>m d2) = 1\<^sub>m d0
[PROOF STEP]
unfolding ptensor_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat dims0 vars1' (1\<^sub>m d1) (1\<^sub>m d2) = 1\<^sub>m d0
[PROOF STEP]
by (metis d0_def d1_def d2_def nths_vars1' nths_vars2'
      partial_state.d1_def partial_state.d2_def partial_state.dims1_def
      partial_state.dims2_def partial_state.tensor_mat_id state_sig.d_def)


[STATEMENT]
lemma ptensor_mat_mult:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d1 d1"
    and "m3 \<in> carrier_mat d2 d2"
    and "m4 \<in> carrier_mat d2 d2"
  shows "ptensor_mat (m1 * m2) (m3 * m4) = ptensor_mat m1 m3 * ptensor_mat m2 m4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ptensor_mat (m1 * m2) (m3 * m4) = ptensor_mat m1 m3 * ptensor_mat m2 m4
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ptensor_mat (m1 * m2) (m3 * m4) = ptensor_mat m1 m3 * ptensor_mat m2 m4
[PROOF STEP]
interpret st: partial_state dims0 vars1'
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ptensor_mat (m1 * m2) (m3 * m4) = ptensor_mat m1 m3 * ptensor_mat m2 m4
[PROOF STEP]
have "st.d1 = d1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. st.d1 = d1
[PROOF STEP]
unfolding st.d1_def st.dims1_def d1_def nths_vars1'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list dims1 = prod_list dims1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
st.d1 = d1

goal (1 subgoal):
 1. ptensor_mat (m1 * m2) (m3 * m4) = ptensor_mat m1 m3 * ptensor_mat m2 m4
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
st.d1 = d1

goal (1 subgoal):
 1. ptensor_mat (m1 * m2) (m3 * m4) = ptensor_mat m1 m3 * ptensor_mat m2 m4
[PROOF STEP]
have "st.d2 = d2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. st.d2 = d2
[PROOF STEP]
unfolding st.d2_def st.dims2_def d2_def nths_vars2'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list dims2 = prod_list dims2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
st.d2 = d2

goal (1 subgoal):
 1. ptensor_mat (m1 * m2) (m3 * m4) = ptensor_mat m1 m3 * ptensor_mat m2 m4
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
st.d1 = d1
st.d2 = d2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
st.d1 = d1
st.d2 = d2

goal (1 subgoal):
 1. ptensor_mat (m1 * m2) (m3 * m4) = ptensor_mat m1 m3 * ptensor_mat m2 m4
[PROOF STEP]
unfolding ptensor_mat_def
[PROOF STATE]
proof (prove)
using this:
st.d1 = d1
st.d2 = d2

goal (1 subgoal):
 1. st.tensor_mat (m1 * m2) (m3 * m4) = st.tensor_mat m1 m3 * st.tensor_mat m2 m4
[PROOF STEP]
using st.tensor_mat_mult assms
[PROOF STATE]
proof (prove)
using this:
st.d1 = d1
st.d2 = d2
\<lbrakk>?m1.0 \<in> carrier_mat st.d1 st.d1; ?m2.0 \<in> carrier_mat st.d1 st.d1; ?m3.0 \<in> carrier_mat st.d2 st.d2; ?m4.0 \<in> carrier_mat st.d2 st.d2\<rbrakk> \<Longrightarrow> st.tensor_mat (?m1.0 * ?m2.0) (?m3.0 * ?m4.0) = st.tensor_mat ?m1.0 ?m3.0 * st.tensor_mat ?m2.0 ?m4.0
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d1 d1
m3 \<in> carrier_mat d2 d2
m4 \<in> carrier_mat d2 d2

goal (1 subgoal):
 1. st.tensor_mat (m1 * m2) (m3 * m4) = st.tensor_mat m1 m3 * st.tensor_mat m2 m4
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ptensor_mat (m1 * m2) (m3 * m4) = ptensor_mat m1 m3 * ptensor_mat m2 m4

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ptensor_mat_mult_vec:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "v1 \<in> carrier_vec d1"
    and "m2 \<in> carrier_mat d2 d2"
    and "v2 \<in> carrier_vec d2"
  shows "ptensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) = ptensor_mat m1 m2 *\<^sub>v ptensor_vec v1 v2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ptensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) = ptensor_mat m1 m2 *\<^sub>v ptensor_vec v1 v2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ptensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) = ptensor_mat m1 m2 *\<^sub>v ptensor_vec v1 v2
[PROOF STEP]
interpret st: partial_state dims0 vars1'
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ptensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) = ptensor_mat m1 m2 *\<^sub>v ptensor_vec v1 v2
[PROOF STEP]
have "st.d1 = d1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. st.d1 = d1
[PROOF STEP]
unfolding st.d1_def st.dims1_def d1_def nths_vars1'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list dims1 = prod_list dims1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
st.d1 = d1

goal (1 subgoal):
 1. ptensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) = ptensor_mat m1 m2 *\<^sub>v ptensor_vec v1 v2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
st.d1 = d1

goal (1 subgoal):
 1. ptensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) = ptensor_mat m1 m2 *\<^sub>v ptensor_vec v1 v2
[PROOF STEP]
have "st.d2 = d2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. st.d2 = d2
[PROOF STEP]
unfolding st.d2_def st.dims2_def d2_def nths_vars2'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list dims2 = prod_list dims2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
st.d2 = d2

goal (1 subgoal):
 1. ptensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) = ptensor_mat m1 m2 *\<^sub>v ptensor_vec v1 v2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
st.d1 = d1
st.d2 = d2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
st.d1 = d1
st.d2 = d2

goal (1 subgoal):
 1. ptensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) = ptensor_mat m1 m2 *\<^sub>v ptensor_vec v1 v2
[PROOF STEP]
unfolding ptensor_mat_def ptensor_vec_def
[PROOF STATE]
proof (prove)
using this:
st.d1 = d1
st.d2 = d2

goal (1 subgoal):
 1. st.tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) = st.tensor_mat m1 m2 *\<^sub>v st.tensor_vec v1 v2
[PROOF STEP]
using st.tensor_mat_mult_vec assms
[PROOF STATE]
proof (prove)
using this:
st.d1 = d1
st.d2 = d2
\<lbrakk>?m1.0 \<in> carrier_mat st.d1 st.d1; ?m2.0 \<in> carrier_mat st.d2 st.d2; ?v1.0 \<in> carrier_vec st.d1; ?v2.0 \<in> carrier_vec st.d2\<rbrakk> \<Longrightarrow> st.tensor_vec (?m1.0 *\<^sub>v ?v1.0) (?m2.0 *\<^sub>v ?v2.0) = st.tensor_mat ?m1.0 ?m2.0 *\<^sub>v st.tensor_vec ?v1.0 ?v2.0
m1 \<in> carrier_mat d1 d1
v1 \<in> carrier_vec d1
m2 \<in> carrier_mat d2 d2
v2 \<in> carrier_vec d2

goal (1 subgoal):
 1. st.tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) = st.tensor_mat m1 m2 *\<^sub>v st.tensor_vec v1 v2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ptensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) = ptensor_mat m1 m2 *\<^sub>v ptensor_vec v1 v2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pmat_extension_carrier:
  "pmat_extension m \<in> carrier_mat d0 d0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmat_extension m \<in> carrier_mat d0 d0
[PROOF STEP]
by (simp add: pmat_extension_def ptensor_mat_carrier)


[STATEMENT]
lemma pmat_extension_add:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d1 d1"
  shows "pmat_extension (m1 + m2) = pmat_extension m1 + pmat_extension m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmat_extension (m1 + m2) = pmat_extension m1 + pmat_extension m2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d1 d1

goal (1 subgoal):
 1. pmat_extension (m1 + m2) = pmat_extension m1 + pmat_extension m2
[PROOF STEP]
by (simp add: pmat_extension_def ptensor_mat_add)


[STATEMENT]
lemma pmat_extension_trace:
  assumes "m \<in> carrier_mat d1 d1"
  shows "trace (pmat_extension m) = d2 * trace m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (pmat_extension m) = int d2 * trace m
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m \<in> carrier_mat d1 d1

goal (1 subgoal):
 1. trace (pmat_extension m) = int d2 * trace m
[PROOF STEP]
by (simp add: pmat_extension_def ptensor_mat_trace)


[STATEMENT]
lemma pmat_extension_id:
  "pmat_extension (1\<^sub>m d1) = 1\<^sub>m d0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmat_extension (1\<^sub>m d1) = 1\<^sub>m d0
[PROOF STEP]
by (simp add: pmat_extension_def ptensor_mat_id)


[STATEMENT]
lemma pmat_extension_mult:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d1 d1"
  shows "pmat_extension (m1 * m2) = pmat_extension m1 * pmat_extension m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmat_extension (m1 * m2) = pmat_extension m1 * pmat_extension m2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d1 d1

goal (1 subgoal):
 1. pmat_extension (m1 * m2) = pmat_extension m1 * pmat_extension m2
[PROOF STEP]
by (simp add: pmat_extension_def ptensor_mat_mult[symmetric])


[STATEMENT]
lemma ptensor_mat_comm:
  fixes m1 m2 :: "complex mat"
  assumes "vars1 \<inter> vars2 = {}"
  shows "ptensor_mat dims vars1 vars2 m1 m2 = ptensor_mat dims vars2 vars1 m2 m1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state2.ptensor_mat dims vars1 vars2 m1 m2 = partial_state2.ptensor_mat dims vars2 vars1 m2 m1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partial_state2.ptensor_mat dims vars1 vars2 m1 m2 = partial_state2.ptensor_mat dims vars2 vars1 m2 m1
[PROOF STEP]
interpret st1: partial_state2 dims vars1 vars2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state2 vars1 vars2
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars1 \<inter> vars2 = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vars1 \<inter> vars2 = {}

goal (1 subgoal):
 1. vars1 \<inter> vars2 = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. st1.ptensor_mat m1 m2 = partial_state2.ptensor_mat dims vars2 vars1 m2 m1
[PROOF STEP]
interpret st2: partial_state2 dims vars2 vars1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state2 vars2 vars1
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars2 \<inter> vars1 = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vars1 \<inter> vars2 = {}

goal (1 subgoal):
 1. vars2 \<inter> vars1 = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. st1.ptensor_mat m1 m2 = st2.ptensor_mat m2 m1
[PROOF STEP]
have eq1: "partial_state.encode1 st1.dims0 st1.vars1' = partial_state.encode2 st2.dims0 st2.vars1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode1 st1.dims0 st1.vars1' = partial_state.encode2 st2.dims0 st2.vars1'
[PROOF STEP]
apply (subst st1.ptensor_encode1_encode2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode2 st1.dims0 st1.vars2' = partial_state.encode2 st2.dims0 st2.vars1'
[PROOF STEP]
unfolding st1.dims0_def st1.vars0_def st1.vars2'_def st2.dims0_def st2.vars0_def st2.vars1'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode2 (nths dims (vars1 \<union> vars2)) (ind_in_set (vars1 \<union> vars2) ` vars2) = partial_state.encode2 (nths dims (vars2 \<union> vars1)) (ind_in_set (vars2 \<union> vars1) ` vars2)
[PROOF STEP]
by (subgoal_tac "vars1 \<union> vars2 = vars2 \<union> vars1", auto)
[PROOF STATE]
proof (state)
this:
partial_state.encode1 st1.dims0 st1.vars1' = partial_state.encode2 st2.dims0 st2.vars1'

goal (1 subgoal):
 1. st1.ptensor_mat m1 m2 = st2.ptensor_mat m2 m1
[PROOF STEP]
have eq2: "partial_state.encode2 st1.dims0 st1.vars1' = partial_state.encode1 st2.dims0 st2.vars1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode2 st1.dims0 st1.vars1' = partial_state.encode1 st2.dims0 st2.vars1'
[PROOF STEP]
apply (subst st1.ptensor_encode2_encode1[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode1 st1.dims0 st1.vars2' = partial_state.encode1 st2.dims0 st2.vars1'
[PROOF STEP]
unfolding st1.dims0_def st1.vars0_def st1.vars2'_def st2.dims0_def st2.vars0_def st2.vars1'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_state.encode1 (nths dims (vars1 \<union> vars2)) (ind_in_set (vars1 \<union> vars2) ` vars2) = partial_state.encode1 (nths dims (vars2 \<union> vars1)) (ind_in_set (vars2 \<union> vars1) ` vars2)
[PROOF STEP]
by (subgoal_tac "vars1 \<union> vars2 = vars2 \<union> vars1", auto)
[PROOF STATE]
proof (state)
this:
partial_state.encode2 st1.dims0 st1.vars1' = partial_state.encode1 st2.dims0 st2.vars1'

goal (1 subgoal):
 1. st1.ptensor_mat m1 m2 = st2.ptensor_mat m2 m1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. st1.ptensor_mat m1 m2 = st2.ptensor_mat m2 m1
[PROOF STEP]
unfolding st1.ptensor_mat_def st2.ptensor_mat_def partial_state.tensor_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (state_sig.d st1.dims0) (state_sig.d st1.dims0) (\<lambda>(i, j). m1 $$ (partial_state.encode1 st1.dims0 st1.vars1' i, partial_state.encode1 st1.dims0 st1.vars1' j) * m2 $$ (partial_state.encode2 st1.dims0 st1.vars1' i, partial_state.encode2 st1.dims0 st1.vars1' j)) = mat (state_sig.d st2.dims0) (state_sig.d st2.dims0) (\<lambda>(i, j). m2 $$ (partial_state.encode1 st2.dims0 st2.vars1' i, partial_state.encode1 st2.dims0 st2.vars1' j) * m1 $$ (partial_state.encode2 st2.dims0 st2.vars1' i, partial_state.encode2 st2.dims0 st2.vars1' j))
[PROOF STEP]
apply (rule cong_mat, auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. state_sig.d st1.dims0 = state_sig.d st2.dims0
 2. state_sig.d st1.dims0 = state_sig.d st2.dims0
 3. \<And>i j. \<lbrakk>i < state_sig.d st1.dims0; j < state_sig.d st1.dims0\<rbrakk> \<Longrightarrow> m1 $$ (partial_state.encode1 st1.dims0 st1.vars1' i, partial_state.encode1 st1.dims0 st1.vars1' j) * m2 $$ (partial_state.encode2 st1.dims0 st1.vars1' i, partial_state.encode2 st1.dims0 st1.vars1' j) = m2 $$ (partial_state.encode1 st2.dims0 st2.vars1' i, partial_state.encode1 st2.dims0 st2.vars1' j) * m1 $$ (partial_state.encode2 st2.dims0 st2.vars1' i, partial_state.encode2 st2.dims0 st2.vars1' j)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_sig.d st1.dims0 = state_sig.d st2.dims0
[PROOF STEP]
unfolding st1.dims0_def st1.vars0_def st2.dims0_def st2.vars0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_sig.d (nths dims (vars1 \<union> vars2)) = state_sig.d (nths dims (vars2 \<union> vars1))
[PROOF STEP]
by (subgoal_tac "vars1 \<union> vars2 = vars2 \<union> vars1", auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. state_sig.d st1.dims0 = state_sig.d st2.dims0
 2. \<And>i j. \<lbrakk>i < state_sig.d st1.dims0; j < state_sig.d st1.dims0\<rbrakk> \<Longrightarrow> m1 $$ (partial_state.encode1 st1.dims0 st1.vars1' i, partial_state.encode1 st1.dims0 st1.vars1' j) * m2 $$ (partial_state.encode2 st1.dims0 st1.vars1' i, partial_state.encode2 st1.dims0 st1.vars1' j) = m2 $$ (partial_state.encode1 st2.dims0 st2.vars1' i, partial_state.encode1 st2.dims0 st2.vars1' j) * m1 $$ (partial_state.encode2 st2.dims0 st2.vars1' i, partial_state.encode2 st2.dims0 st2.vars1' j)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_sig.d st1.dims0 = state_sig.d st2.dims0
[PROOF STEP]
unfolding st1.dims0_def st1.vars0_def st2.dims0_def st2.vars0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_sig.d (nths dims (vars1 \<union> vars2)) = state_sig.d (nths dims (vars2 \<union> vars1))
[PROOF STEP]
by (subgoal_tac "vars1 \<union> vars2 = vars2 \<union> vars1", auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < state_sig.d st1.dims0; j < state_sig.d st1.dims0\<rbrakk> \<Longrightarrow> m1 $$ (partial_state.encode1 st1.dims0 st1.vars1' i, partial_state.encode1 st1.dims0 st1.vars1' j) * m2 $$ (partial_state.encode2 st1.dims0 st1.vars1' i, partial_state.encode2 st1.dims0 st1.vars1' j) = m2 $$ (partial_state.encode1 st2.dims0 st2.vars1' i, partial_state.encode1 st2.dims0 st2.vars1' j) * m1 $$ (partial_state.encode2 st2.dims0 st2.vars1' i, partial_state.encode2 st2.dims0 st2.vars1' j)
[PROOF STEP]
using eq1 eq2
[PROOF STATE]
proof (prove)
using this:
partial_state.encode1 st1.dims0 st1.vars1' = partial_state.encode2 st2.dims0 st2.vars1'
partial_state.encode2 st1.dims0 st1.vars1' = partial_state.encode1 st2.dims0 st2.vars1'

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < state_sig.d st1.dims0; j < state_sig.d st1.dims0\<rbrakk> \<Longrightarrow> m1 $$ (partial_state.encode1 st1.dims0 st1.vars1' i, partial_state.encode1 st1.dims0 st1.vars1' j) * m2 $$ (partial_state.encode2 st1.dims0 st1.vars1' i, partial_state.encode2 st1.dims0 st1.vars1' j) = m2 $$ (partial_state.encode1 st2.dims0 st2.vars1' i, partial_state.encode1 st2.dims0 st2.vars1' j) * m1 $$ (partial_state.encode2 st2.dims0 st2.vars1' i, partial_state.encode2 st2.dims0 st2.vars1' j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
st1.ptensor_mat m1 m2 = st2.ptensor_mat m2 m1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ind_in_set_inj:
  fixes a b :: nat and A :: "nat set"
  assumes "a \<in> A" "b \<in> A" "ind_in_set A a = ind_in_set A b"
  shows "a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
have "ind_in_set A a < ind_in_set A b" if "a < b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A a < ind_in_set A b
[PROOF STEP]
by (rule ind_in_set_mono[OF assms(1) assms(2) that])
[PROOF STATE]
proof (state)
this:
a < b \<Longrightarrow> ind_in_set A a < ind_in_set A b

goal (1 subgoal):
 1. a = b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a < b \<Longrightarrow> ind_in_set A a < ind_in_set A b

goal (1 subgoal):
 1. a = b
[PROOF STEP]
have "ind_in_set A b < ind_in_set A a" if "b < a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A b < ind_in_set A a
[PROOF STEP]
by (rule ind_in_set_mono[OF assms(2) assms(1) that])
[PROOF STATE]
proof (state)
this:
b < a \<Longrightarrow> ind_in_set A b < ind_in_set A a

goal (1 subgoal):
 1. a = b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a < b \<Longrightarrow> ind_in_set A a < ind_in_set A b
b < a \<Longrightarrow> ind_in_set A b < ind_in_set A a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a < b \<Longrightarrow> ind_in_set A a < ind_in_set A b
b < a \<Longrightarrow> ind_in_set A b < ind_in_set A a

goal (1 subgoal):
 1. a = b
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
a < b \<Longrightarrow> ind_in_set A a < ind_in_set A b
b < a \<Longrightarrow> ind_in_set A b < ind_in_set A a
ind_in_set A a = ind_in_set A b

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ind_in_set_mono2:
  fixes a b :: nat and A :: "nat set"
  assumes "a \<in> A" "b \<in> A" "ind_in_set A a < ind_in_set A b"
  shows "a < b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < b
[PROOF STEP]
using ind_in_set_mono ind_in_set_inj
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<in> ?A; ?b \<in> ?A; ?a < ?b\<rbrakk> \<Longrightarrow> ind_in_set ?A ?a < ind_in_set ?A ?b
\<lbrakk>?a \<in> ?A; ?b \<in> ?A; ind_in_set ?A ?a = ind_in_set ?A ?b\<rbrakk> \<Longrightarrow> ?a = ?b

goal (1 subgoal):
 1. a < b
[PROOF STEP]
by (metis assms not_less_iff_gr_or_eq)


[STATEMENT]
lemma ind_in_set_bij_betw:
  fixes A B :: "nat set"
  assumes "B \<subseteq> A" "c \<in> B"
  shows "bij_betw (ind_in_set A) {i \<in> B. i < c} {i \<in> ind_in_set A ` B. i < ind_in_set A c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (ind_in_set A) {i \<in> B. i < c} {i \<in> ind_in_set A ` B. i < ind_in_set A c}
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (ind_in_set A) {i \<in> B. i < c} \<and> ind_in_set A ` {i \<in> B. i < c} = {i \<in> ind_in_set A ` B. i < ind_in_set A c}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. inj_on (ind_in_set A) {i \<in> B. i < c}
 2. \<And>xa. \<lbrakk>xa \<in> B; xa < c\<rbrakk> \<Longrightarrow> ind_in_set A xa < ind_in_set A c
 3. \<And>xa. \<lbrakk>ind_in_set A xa < ind_in_set A c; xa \<in> B\<rbrakk> \<Longrightarrow> ind_in_set A xa \<in> ind_in_set A ` {i \<in> B. i < c}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. inj_on (ind_in_set A) {i \<in> B. i < c}
 2. \<And>xa. \<lbrakk>xa \<in> B; xa < c\<rbrakk> \<Longrightarrow> ind_in_set A xa < ind_in_set A c
 3. \<And>xa. \<lbrakk>ind_in_set A xa < ind_in_set A c; xa \<in> B\<rbrakk> \<Longrightarrow> ind_in_set A xa \<in> ind_in_set A ` {i \<in> B. i < c}
[PROOF STEP]
show "inj_on (ind_in_set A) {i \<in> B. i < c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (ind_in_set A) {i \<in> B. i < c}
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{i \<in> B. i < c}. \<forall>y\<in>{i \<in> B. i < c}. ind_in_set A x = ind_in_set A y \<longrightarrow> x = y
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> B; x < c; y \<in> B; y < c; ind_in_set A x = ind_in_set A y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
using assms(1) ind_in_set_inj
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> A
\<lbrakk>?a \<in> ?A; ?b \<in> ?A; ind_in_set ?A ?a = ind_in_set ?A ?b\<rbrakk> \<Longrightarrow> ?a = ?b

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> B; x < c; y \<in> B; y < c; ind_in_set A x = ind_in_set A y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inj_on (ind_in_set A) {i \<in> B. i < c}

goal (2 subgoals):
 1. \<And>xa. \<lbrakk>xa \<in> B; xa < c\<rbrakk> \<Longrightarrow> ind_in_set A xa < ind_in_set A c
 2. \<And>xa. \<lbrakk>ind_in_set A xa < ind_in_set A c; xa \<in> B\<rbrakk> \<Longrightarrow> ind_in_set A xa \<in> ind_in_set A ` {i \<in> B. i < c}
[PROOF STEP]
show "ind_in_set A x < ind_in_set A c" if "x \<in> B" "x < c" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A x < ind_in_set A c
[PROOF STEP]
by (meson assms that ind_in_set_mono subsetCE)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> B; ?x < c\<rbrakk> \<Longrightarrow> ind_in_set A ?x < ind_in_set A c

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>ind_in_set A xa < ind_in_set A c; xa \<in> B\<rbrakk> \<Longrightarrow> ind_in_set A xa \<in> ind_in_set A ` {i \<in> B. i < c}
[PROOF STEP]
show "ind_in_set A x \<in> ind_in_set A ` {i \<in> B. i < c}" if "ind_in_set A x < ind_in_set A c" "x \<in> B" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A x \<in> ind_in_set A ` {i \<in> B. i < c}
[PROOF STEP]
using that ind_in_set_mono2 assms
[PROOF STATE]
proof (prove)
using this:
ind_in_set A x < ind_in_set A c
x \<in> B
\<lbrakk>?a \<in> ?A; ?b \<in> ?A; ind_in_set ?A ?a < ind_in_set ?A ?b\<rbrakk> \<Longrightarrow> ?a < ?b
B \<subseteq> A
c \<in> B

goal (1 subgoal):
 1. ind_in_set A x \<in> ind_in_set A ` {i \<in> B. i < c}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>ind_in_set A ?x < ind_in_set A c; ?x \<in> B\<rbrakk> \<Longrightarrow> ind_in_set A ?x \<in> ind_in_set A ` {i \<in> B. i < c}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ind_in_set_assoc:
  fixes A B C :: "nat set"
  assumes "C \<subseteq> B" "B \<subseteq> A"
  shows "ind_in_set (ind_in_set A ` B) ` (ind_in_set A ` C) = ind_in_set B ` C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C = ind_in_set B ` C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C = ind_in_set B ` C
[PROOF STEP]
have "x \<in> ind_in_set (ind_in_set A ` B) ` (ind_in_set A ` C)" if x: "x \<in> ind_in_set B ` C" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C
[PROOF STEP]
obtain c where c: "c \<in> C" and x_eq: "x = card {i \<in> B. i < c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<in> C; x = card {i \<in> B. i < c}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x \<in> ind_in_set B ` C

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<in> C; x = card {i \<in> B. i < c}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: ind_in_set_def)
[PROOF STATE]
proof (state)
this:
c \<in> C
x = card {i \<in> B. i < c}

goal (1 subgoal):
 1. x \<in> ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C
[PROOF STEP]
have "card {i \<in> B. i < c} = card {i \<in> ind_in_set A ` B. i < ind_in_set A c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i \<in> B. i < c} = card {i \<in> ind_in_set A ` B. i < ind_in_set A c}
[PROOF STEP]
apply (rule bij_betw_same_card)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw ?f {i \<in> B. i < c} {i \<in> ind_in_set A ` B. i < ind_in_set A c}
[PROOF STEP]
using c assms
[PROOF STATE]
proof (prove)
using this:
c \<in> C
C \<subseteq> B
B \<subseteq> A

goal (1 subgoal):
 1. bij_betw ?f {i \<in> B. i < c} {i \<in> ind_in_set A ` B. i < ind_in_set A c}
[PROOF STEP]
by (auto intro: ind_in_set_bij_betw)
[PROOF STATE]
proof (state)
this:
card {i \<in> B. i < c} = card {i \<in> ind_in_set A ` B. i < ind_in_set A c}

goal (1 subgoal):
 1. x \<in> ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card {i \<in> B. i < c} = card {i \<in> ind_in_set A ` B. i < ind_in_set A c}
[PROOF STEP]
have "ind_in_set (ind_in_set A ` B) (ind_in_set A c) = x"
[PROOF STATE]
proof (prove)
using this:
card {i \<in> B. i < c} = card {i \<in> ind_in_set A ` B. i < ind_in_set A c}

goal (1 subgoal):
 1. ind_in_set (ind_in_set A ` B) (ind_in_set A c) = x
[PROOF STEP]
apply (subst ind_in_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i \<in> B. i < c} = card {i \<in> ind_in_set A ` B. i < ind_in_set A c} \<Longrightarrow> card {i \<in> ind_in_set A ` B. i < ind_in_set A c} = x
[PROOF STEP]
using x_eq
[PROOF STATE]
proof (prove)
using this:
x = card {i \<in> B. i < c}

goal (1 subgoal):
 1. card {i \<in> B. i < c} = card {i \<in> ind_in_set A ` B. i < ind_in_set A c} \<Longrightarrow> card {i \<in> ind_in_set A ` B. i < ind_in_set A c} = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ind_in_set (ind_in_set A ` B) (ind_in_set A c) = x

goal (1 subgoal):
 1. x \<in> ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ind_in_set (ind_in_set A ` B) (ind_in_set A c) = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ind_in_set (ind_in_set A ` B) (ind_in_set A c) = x

goal (1 subgoal):
 1. x \<in> ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C
[PROOF STEP]
using \<open>c \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
ind_in_set (ind_in_set A ` B) (ind_in_set A c) = x
c \<in> C

goal (1 subgoal):
 1. x \<in> ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> ind_in_set B ` C \<Longrightarrow> ?x \<in> ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C

goal (1 subgoal):
 1. ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C = ind_in_set B ` C
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x \<in> ind_in_set B ` C \<Longrightarrow> ?x \<in> ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C

goal (1 subgoal):
 1. ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C = ind_in_set B ` C
[PROOF STEP]
have "x \<in> ind_in_set B ` C" if x: "x \<in> ind_in_set (ind_in_set A ` B) ` (ind_in_set A ` C)" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> ind_in_set B ` C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> ind_in_set B ` C
[PROOF STEP]
obtain c where c: "c \<in> C" and x_eq: "x = card {i \<in> ind_in_set A ` B. i < ind_in_set A c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<in> C; x = card {i \<in> ind_in_set A ` B. i < ind_in_set A c}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x \<in> ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<in> C; x = card {i \<in> ind_in_set A ` B. i < ind_in_set A c}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: ind_in_set_def)
[PROOF STATE]
proof (state)
this:
c \<in> C
x = card {i \<in> ind_in_set A ` B. i < ind_in_set A c}

goal (1 subgoal):
 1. x \<in> ind_in_set B ` C
[PROOF STEP]
have "card {i \<in> B. i < c} = card {i \<in> ind_in_set A ` B. i < ind_in_set A c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i \<in> B. i < c} = card {i \<in> ind_in_set A ` B. i < ind_in_set A c}
[PROOF STEP]
apply (rule bij_betw_same_card)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw ?f {i \<in> B. i < c} {i \<in> ind_in_set A ` B. i < ind_in_set A c}
[PROOF STEP]
using c assms
[PROOF STATE]
proof (prove)
using this:
c \<in> C
C \<subseteq> B
B \<subseteq> A

goal (1 subgoal):
 1. bij_betw ?f {i \<in> B. i < c} {i \<in> ind_in_set A ` B. i < ind_in_set A c}
[PROOF STEP]
by (auto intro: ind_in_set_bij_betw)
[PROOF STATE]
proof (state)
this:
card {i \<in> B. i < c} = card {i \<in> ind_in_set A ` B. i < ind_in_set A c}

goal (1 subgoal):
 1. x \<in> ind_in_set B ` C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card {i \<in> B. i < c} = card {i \<in> ind_in_set A ` B. i < ind_in_set A c}
[PROOF STEP]
have "ind_in_set B c = x"
[PROOF STATE]
proof (prove)
using this:
card {i \<in> B. i < c} = card {i \<in> ind_in_set A ` B. i < ind_in_set A c}

goal (1 subgoal):
 1. ind_in_set B c = x
[PROOF STEP]
apply (subst ind_in_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i \<in> B. i < c} = card {i \<in> ind_in_set A ` B. i < ind_in_set A c} \<Longrightarrow> card {i \<in> B. i < c} = x
[PROOF STEP]
using x_eq
[PROOF STATE]
proof (prove)
using this:
x = card {i \<in> ind_in_set A ` B. i < ind_in_set A c}

goal (1 subgoal):
 1. card {i \<in> B. i < c} = card {i \<in> ind_in_set A ` B. i < ind_in_set A c} \<Longrightarrow> card {i \<in> B. i < c} = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ind_in_set B c = x

goal (1 subgoal):
 1. x \<in> ind_in_set B ` C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ind_in_set B c = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ind_in_set B c = x

goal (1 subgoal):
 1. x \<in> ind_in_set B ` C
[PROOF STEP]
using \<open>c \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
ind_in_set B c = x
c \<in> C

goal (1 subgoal):
 1. x \<in> ind_in_set B ` C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> ind_in_set B ` C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C \<Longrightarrow> ?x \<in> ind_in_set B ` C

goal (1 subgoal):
 1. ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C = ind_in_set B ` C
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?x \<in> ind_in_set B ` C \<Longrightarrow> ?x \<in> ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C
?x \<in> ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C \<Longrightarrow> ?x \<in> ind_in_set B ` C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?x \<in> ind_in_set B ` C \<Longrightarrow> ?x \<in> ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C
?x \<in> ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C \<Longrightarrow> ?x \<in> ind_in_set B ` C

goal (1 subgoal):
 1. ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C = ind_in_set B ` C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C = ind_in_set B ` C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nths_reencode_eq3:
  fixes A B C :: "nat set"
  assumes "C \<subseteq> B" "B \<subseteq> A"
  shows "nths (nths xs (ind_in_set A ` B)) (ind_in_set B ` C) = nths xs (ind_in_set A ` C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths xs (ind_in_set A ` B)) (ind_in_set B ` C) = nths xs (ind_in_set A ` C)
[PROOF STEP]
apply (subst ind_in_set_assoc[OF assms, symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths xs (ind_in_set A ` B)) (ind_in_set (ind_in_set A ` B) ` ind_in_set A ` C) = nths xs (ind_in_set A ` C)
[PROOF STEP]
apply (rule nths_reencode_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A ` C \<subseteq> ind_in_set A ` B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> B
B \<subseteq> A

goal (1 subgoal):
 1. ind_in_set A ` C \<subseteq> ind_in_set A ` B
[PROOF STEP]
by blast


[STATEMENT]
lemma nths_assoc_three_B:
  fixes A B C :: "nat set"
  assumes "A \<inter> B = {}"
    and "(A \<union> B) \<inter> C = {}"
  shows "nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (A \<union> B))) (ind_in_set (A \<union> B) ` B)
       = nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (B \<union> C))) (ind_in_set (B \<union> C) ` B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (A \<union> B))) (ind_in_set (A \<union> B) ` B) = nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (B \<union> C))) (ind_in_set (B \<union> C) ` B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (A \<union> B))) (ind_in_set (A \<union> B) ` B) = nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (B \<union> C))) (ind_in_set (B \<union> C) ` B)
[PROOF STEP]
have "nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (A \<union> B))) (ind_in_set (A \<union> B) ` B) = nths xs (ind_in_set (A \<union> B \<union> C) ` B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (A \<union> B))) (ind_in_set (A \<union> B) ` B) = nths xs (ind_in_set (A \<union> B \<union> C) ` B)
[PROOF STEP]
using nths_assoc_three_A[of B A C xs] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>B \<inter> A = {}; (B \<union> A) \<inter> C = {}\<rbrakk> \<Longrightarrow> nths (nths xs (ind_in_set (B \<union> A \<union> C) ` (B \<union> A))) (ind_in_set (B \<union> A) ` B) = nths xs (ind_in_set (B \<union> A \<union> C) ` B)
A \<inter> B = {}
(A \<union> B) \<inter> C = {}

goal (1 subgoal):
 1. nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (A \<union> B))) (ind_in_set (A \<union> B) ` B) = nths xs (ind_in_set (A \<union> B \<union> C) ` B)
[PROOF STEP]
by (simp add: inf_commute sup_commute)
[PROOF STATE]
proof (state)
this:
nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (A \<union> B))) (ind_in_set (A \<union> B) ` B) = nths xs (ind_in_set (A \<union> B \<union> C) ` B)

goal (1 subgoal):
 1. nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (A \<union> B))) (ind_in_set (A \<union> B) ` B) = nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (B \<union> C))) (ind_in_set (B \<union> C) ` B)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (A \<union> B))) (ind_in_set (A \<union> B) ` B) = nths xs (ind_in_set (A \<union> B \<union> C) ` B)

goal (1 subgoal):
 1. nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (A \<union> B))) (ind_in_set (A \<union> B) ` B) = nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (B \<union> C))) (ind_in_set (B \<union> C) ` B)
[PROOF STEP]
have "nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (B \<union> C))) (ind_in_set (B \<union> C) ` B) = nths xs (ind_in_set (A \<union> B \<union> C) ` B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (B \<union> C))) (ind_in_set (B \<union> C) ` B) = nths xs (ind_in_set (A \<union> B \<union> C) ` B)
[PROOF STEP]
using nths_assoc_three_A[of B C A xs] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>B \<inter> C = {}; (B \<union> C) \<inter> A = {}\<rbrakk> \<Longrightarrow> nths (nths xs (ind_in_set (B \<union> C \<union> A) ` (B \<union> C))) (ind_in_set (B \<union> C) ` B) = nths xs (ind_in_set (B \<union> C \<union> A) ` B)
A \<inter> B = {}
(A \<union> B) \<inter> C = {}

goal (1 subgoal):
 1. nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (B \<union> C))) (ind_in_set (B \<union> C) ` B) = nths xs (ind_in_set (A \<union> B \<union> C) ` B)
[PROOF STEP]
by (smt Un_empty inf_commute inf_sup_distrib2 sup_assoc sup_commute)
[PROOF STATE]
proof (state)
this:
nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (B \<union> C))) (ind_in_set (B \<union> C) ` B) = nths xs (ind_in_set (A \<union> B \<union> C) ` B)

goal (1 subgoal):
 1. nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (A \<union> B))) (ind_in_set (A \<union> B) ` B) = nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (B \<union> C))) (ind_in_set (B \<union> C) ` B)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (A \<union> B))) (ind_in_set (A \<union> B) ` B) = nths xs (ind_in_set (A \<union> B \<union> C) ` B)
nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (B \<union> C))) (ind_in_set (B \<union> C) ` B) = nths xs (ind_in_set (A \<union> B \<union> C) ` B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (A \<union> B))) (ind_in_set (A \<union> B) ` B) = nths xs (ind_in_set (A \<union> B \<union> C) ` B)
nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (B \<union> C))) (ind_in_set (B \<union> C) ` B) = nths xs (ind_in_set (A \<union> B \<union> C) ` B)

goal (1 subgoal):
 1. nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (A \<union> B))) (ind_in_set (A \<union> B) ` B) = nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (B \<union> C))) (ind_in_set (B \<union> C) ` B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (A \<union> B))) (ind_in_set (A \<union> B) ` B) = nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (B \<union> C))) (ind_in_set (B \<union> C) ` B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nths_assoc_three_C:
  fixes A B C :: "nat set"
  assumes "A \<inter> B = {}"
    and "(A \<union> B) \<inter> C = {}"
  shows "nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (B \<union> C))) (ind_in_set (B \<union> C) ` C)
    = nths xs (ind_in_set (A \<union> B \<union> C) ` C) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (B \<union> C))) (ind_in_set (B \<union> C) ` C) = nths xs (ind_in_set (A \<union> B \<union> C) ` C)
[PROOF STEP]
using nths_assoc_three_A[of C B A xs] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>C \<inter> B = {}; (C \<union> B) \<inter> A = {}\<rbrakk> \<Longrightarrow> nths (nths xs (ind_in_set (C \<union> B \<union> A) ` (C \<union> B))) (ind_in_set (C \<union> B) ` C) = nths xs (ind_in_set (C \<union> B \<union> A) ` C)
A \<inter> B = {}
(A \<union> B) \<inter> C = {}

goal (1 subgoal):
 1. nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (B \<union> C))) (ind_in_set (B \<union> C) ` C) = nths xs (ind_in_set (A \<union> B \<union> C) ` C)
[PROOF STEP]
by (smt Un_empty inf_commute inf_sup_distrib2 sup_assoc sup_commute)


[STATEMENT]
lemma valid_index_ind_in_set:
  assumes "is \<lhd> nths dims A" "B \<subseteq> A"
  shows "nths is (ind_in_set A ` B) \<lhd> nths dims B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths is (ind_in_set A ` B) \<lhd> nths dims B
[PROOF STEP]
apply (subst nths_reencode_eq[OF assms(2), symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths is (ind_in_set A ` B) \<lhd> nths (nths dims A) (ind_in_set A ` B)
[PROOF STEP]
apply (rule valid_index_nths)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is \<lhd> nths dims A
[PROOF STEP]
by (rule assms(1))


[STATEMENT]
lemma ind_in_set_id:
  fixes A :: "nat set"
  assumes "finite A"
  shows "ind_in_set A ` A = {0..< card A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A ` A = {0..<card A}
[PROOF STEP]
unfolding ind_in_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. card {i \<in> A. i < x}) ` A = {0..<card A}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa \<in> A \<Longrightarrow> card {i \<in> A. i < xa} < card A
 2. \<And>x. x < card A \<Longrightarrow> x \<in> (\<lambda>x. card {i \<in> A. i < x}) ` A
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa_ \<in> A \<Longrightarrow> card {i \<in> A. i < xa_} < card A
[PROOF STEP]
using assms lt_set_card_lt
[PROOF STATE]
proof (prove)
using this:
finite A
\<lbrakk>finite ?A; ?x \<in> ?A\<rbrakk> \<Longrightarrow> card {y \<in> ?A. y < ?x} < card ?A

goal (1 subgoal):
 1. xa_ \<in> A \<Longrightarrow> card {i \<in> A. i < xa_} < card A
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x < card A \<Longrightarrow> x \<in> (\<lambda>x. card {i \<in> A. i < x}) ` A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x < card A \<Longrightarrow> x \<in> (\<lambda>x. card {i \<in> A. i < x}) ` A
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x < card A \<Longrightarrow> x \<in> (\<lambda>x. card {i \<in> A. i < x}) ` A
[PROOF STEP]
assume x: "x < card A"
[PROOF STATE]
proof (state)
this:
x < card A

goal (1 subgoal):
 1. \<And>x. x < card A \<Longrightarrow> x \<in> (\<lambda>x. card {i \<in> A. i < x}) ` A
[PROOF STEP]
have *: "card {i \<in> A. i < pick A x} = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i \<in> A. i < pick A x} = x
[PROOF STEP]
apply (rule card_pick_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < card A
[PROOF STEP]
by (rule x)
[PROOF STATE]
proof (state)
this:
card {i \<in> A. i < pick A x} = x

goal (1 subgoal):
 1. \<And>x. x < card A \<Longrightarrow> x \<in> (\<lambda>x. card {i \<in> A. i < x}) ` A
[PROOF STEP]
show "x \<in> (\<lambda>x. card {i \<in> A. i < x}) ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> (\<lambda>x. card {i \<in> A. i < x}) ` A
[PROOF STEP]
apply (subst *[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i \<in> A. i < pick A x} \<in> (\<lambda>x. card {i \<in> A. i < x}) ` A
[PROOF STEP]
apply (rule imageI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pick A x \<in> A
[PROOF STEP]
apply (rule pick_in_set_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < card A
[PROOF STEP]
by (rule x)
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>x. card {i \<in> A. i < x}) ` A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nths_complement_ind_in_set:
  fixes A B :: "nat set"
  assumes "A \<inter> B = {}"
    "card (A \<union> B) = length xs"
  shows "nths xs (- ind_in_set (A \<union> B) ` A) = nths xs (ind_in_set (A \<union> B) ` B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths xs (- ind_in_set (A \<union> B) ` A) = nths xs (ind_in_set (A \<union> B) ` B)
[PROOF STEP]
apply (rule nths_split_complement_eq[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ind_in_set (A \<union> B) ` B \<inter> ind_in_set (A \<union> B) ` A = {}
 2. {0..<length xs} \<subseteq> ind_in_set (A \<union> B) ` B \<union> ind_in_set (A \<union> B) ` A
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set (A \<union> B) ` B \<inter> ind_in_set (A \<union> B) ` A = {}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa xb. \<lbrakk>xa \<in> B; ind_in_set (A \<union> B) xa = ind_in_set (A \<union> B) xb; xb \<in> A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using assms(1) ind_in_set_inj
[PROOF STATE]
proof (prove)
using this:
A \<inter> B = {}
\<lbrakk>?a \<in> ?A; ?b \<in> ?A; ind_in_set ?A ?a = ind_in_set ?A ?b\<rbrakk> \<Longrightarrow> ?a = ?b

goal (1 subgoal):
 1. \<And>xa xb. \<lbrakk>xa \<in> B; ind_in_set (A \<union> B) xa = ind_in_set (A \<union> B) xb; xb \<in> A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis disjoint_iff_not_equal subsetCE sup_ge1 sup_ge2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<length xs} \<subseteq> ind_in_set (A \<union> B) ` B \<union> ind_in_set (A \<union> B) ` A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {0..<length xs} \<subseteq> ind_in_set (A \<union> B) ` B \<union> ind_in_set (A \<union> B) ` A
[PROOF STEP]
have *: "ind_in_set (A \<union> B) ` B \<union> ind_in_set (A \<union> B) ` A = ind_in_set (A \<union> B) ` (A \<union> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set (A \<union> B) ` B \<union> ind_in_set (A \<union> B) ` A = ind_in_set (A \<union> B) ` (A \<union> B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ind_in_set (A \<union> B) ` B \<union> ind_in_set (A \<union> B) ` A = ind_in_set (A \<union> B) ` (A \<union> B)

goal (1 subgoal):
 1. {0..<length xs} \<subseteq> ind_in_set (A \<union> B) ` B \<union> ind_in_set (A \<union> B) ` A
[PROOF STEP]
show "{0..<length xs} \<subseteq> ind_in_set (A \<union> B) ` B \<union> ind_in_set (A \<union> B) ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<length xs} \<subseteq> ind_in_set (A \<union> B) ` B \<union> ind_in_set (A \<union> B) ` A
[PROOF STEP]
apply (auto simp add: * assms(2))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x < length xs \<Longrightarrow> x \<in> ind_in_set (A \<union> B) ` (A \<union> B)
[PROOF STEP]
using ind_in_set_id
[PROOF STATE]
proof (prove)
using this:
finite ?A \<Longrightarrow> ind_in_set ?A ` ?A = {0..<card ?A}

goal (1 subgoal):
 1. \<And>x. x < length xs \<Longrightarrow> x \<in> ind_in_set (A \<union> B) ` (A \<union> B)
[PROOF STEP]
by (metis assms(2) atLeastLessThan_iff card.infinite not_le_imp_less not_less_zero)
[PROOF STATE]
proof (state)
this:
{0..<length xs} \<subseteq> ind_in_set (A \<union> B) ` B \<union> ind_in_set (A \<union> B) ` A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ind_in_set_inj':
  fixes A B :: "nat set"
  assumes "B \<subseteq> A"
  shows "inj_on (ind_in_set A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (ind_in_set A) B
[PROOF STEP]
proof (rule inj_onI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> B; y \<in> B; ind_in_set A x = ind_in_set A y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> B; y \<in> B; ind_in_set A x = ind_in_set A y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume x: "x \<in> B" and y: "y \<in> B" and eq: "ind_in_set A x = ind_in_set A y"
[PROOF STATE]
proof (state)
this:
x \<in> B
y \<in> B
ind_in_set A x = ind_in_set A y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> B; y \<in> B; ind_in_set A x = ind_in_set A y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have x': "x \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A
[PROOF STEP]
using x assms
[PROOF STATE]
proof (prove)
using this:
x \<in> B
B \<subseteq> A

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> B; y \<in> B; ind_in_set A x = ind_in_set A y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have y': "y \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> A
[PROOF STEP]
using y assms
[PROOF STATE]
proof (prove)
using this:
y \<in> B
B \<subseteq> A

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> B; y \<in> B; ind_in_set A x = ind_in_set A y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
show "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (rule ind_in_set_inj[OF x' y' eq])
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ind_in_set_less:
  fixes x :: nat and A :: "nat set"
  assumes "finite A" "x \<in> A"
  shows "ind_in_set A x < card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A x < card A
[PROOF STEP]
unfolding ind_in_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i \<in> A. i < x} < card A
[PROOF STEP]
apply (rule psubset_card_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite A
 2. {i \<in> A. i < x} \<subset> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
x \<in> A

goal (2 subgoals):
 1. finite A
 2. {i \<in> A. i < x} \<subset> A
[PROOF STEP]
by auto