[STATEMENT]
lemma nths_prod_list_split:
  fixes A :: "nat set" and xs :: "nat list"
  assumes "B \<subseteq> A"
  shows "prod_list (nths xs A) = (prod_list (nths xs B)) * (prod_list (nths xs (A - B)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list (nths xs A) = prod_list (nths xs B) * prod_list (nths xs (A - B))
[PROOF STEP]
proof (induction xs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. prod_list (nths [] A) = prod_list (nths [] B) * prod_list (nths [] (A - B))
 2. \<And>x xs. prod_list (nths xs A) = prod_list (nths xs B) * prod_list (nths xs (A - B)) \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. prod_list (nths [] A) = prod_list (nths [] B) * prod_list (nths [] (A - B))
 2. \<And>x xs. prod_list (nths xs A) = prod_list (nths xs B) * prod_list (nths xs (A - B)) \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list (nths [] A) = prod_list (nths [] B) * prod_list (nths [] (A - B))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prod_list (nths [] A) = prod_list (nths [] B) * prod_list (nths [] (A - B))

goal (1 subgoal):
 1. \<And>x xs. prod_list (nths xs A) = prod_list (nths xs B) * prod_list (nths xs (A - B)) \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. prod_list (nths xs A) = prod_list (nths xs B) * prod_list (nths xs (A - B)) \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
let ?C = "A - B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. prod_list (nths xs A) = prod_list (nths xs B) * prod_list (nths xs (A - B)) \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
prod_list (nths xs A) = prod_list (nths xs B) * prod_list (nths xs (A - B))

goal (1 subgoal):
 1. \<And>x xs. prod_list (nths xs A) = prod_list (nths xs B) * prod_list (nths xs (A - B)) \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
have SA: "nths (xs @ [x]) A = nths xs A @ nths [x] {j. j + length xs \<in> A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ nths [x] {j. j + length xs \<in> A}
[PROOF STEP]
using nths_append[of xs]
[PROOF STATE]
proof (prove)
using this:
nths (xs @ ?l') ?A = nths xs ?A @ nths ?l' {j. j + length xs \<in> ?A}

goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ nths [x] {j. j + length xs \<in> A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) A = nths xs A @ nths [x] {j. j + length xs \<in> A}

goal (1 subgoal):
 1. \<And>x xs. prod_list (nths xs A) = prod_list (nths xs B) * prod_list (nths xs (A - B)) \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
have SB: "nths (xs @ [x]) B = nths xs B @ nths [x] {j. j + length xs \<in> B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (xs @ [x]) B = nths xs B @ nths [x] {j. j + length xs \<in> B}
[PROOF STEP]
using nths_append[of xs]
[PROOF STATE]
proof (prove)
using this:
nths (xs @ ?l') ?A = nths xs ?A @ nths ?l' {j. j + length xs \<in> ?A}

goal (1 subgoal):
 1. nths (xs @ [x]) B = nths xs B @ nths [x] {j. j + length xs \<in> B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) B = nths xs B @ nths [x] {j. j + length xs \<in> B}

goal (1 subgoal):
 1. \<And>x xs. prod_list (nths xs A) = prod_list (nths xs B) * prod_list (nths xs (A - B)) \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
have SC: "nths (xs @ [x]) ?C = nths xs ?C @ nths [x] {j. j + length xs \<in> ?C}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {j. j + length xs \<in> A - B}
[PROOF STEP]
using nths_append[of xs]
[PROOF STATE]
proof (prove)
using this:
nths (xs @ ?l') ?A = nths xs ?A @ nths ?l' {j. j + length xs \<in> ?A}

goal (1 subgoal):
 1. nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {j. j + length xs \<in> A - B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {j. j + length xs \<in> A - B}

goal (1 subgoal):
 1. \<And>x xs. prod_list (nths xs A) = prod_list (nths xs B) * prod_list (nths xs (A - B)) \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
proof (cases "length xs \<in> A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
 2. length xs \<notin> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length xs \<in> A

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
 2. length xs \<notin> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs \<in> A
[PROOF STEP]
have "nths (xs @ [x]) A = nths xs A @ [x]"
[PROOF STATE]
proof (prove)
using this:
length xs \<in> A

goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ [x]
[PROOF STEP]
using SA
[PROOF STATE]
proof (prove)
using this:
length xs \<in> A
nths (xs @ [x]) A = nths xs A @ nths [x] {j. j + length xs \<in> A}

goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A @ [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) A = nths xs A @ [x]

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
 2. length xs \<notin> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) A = nths xs A @ [x]
[PROOF STEP]
have eqA: "prod_list (nths (xs @ [x]) A) = prod_list (nths xs A) * x"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) A = nths xs A @ [x]

goal (1 subgoal):
 1. prod_list (nths (xs @ [x]) A) = prod_list (nths xs A) * x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prod_list (nths (xs @ [x]) A) = prod_list (nths xs A) * x

goal (2 subgoals):
 1. length xs \<in> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
 2. length xs \<notin> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
proof (cases "length xs \<in> B")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
 2. length xs \<notin> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length xs \<in> B

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
 2. length xs \<notin> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs \<in> B
[PROOF STEP]
have "nths (xs @ [x]) B = nths xs B @ [x]"
[PROOF STATE]
proof (prove)
using this:
length xs \<in> B

goal (1 subgoal):
 1. nths (xs @ [x]) B = nths xs B @ [x]
[PROOF STEP]
using SB
[PROOF STATE]
proof (prove)
using this:
length xs \<in> B
nths (xs @ [x]) B = nths xs B @ nths [x] {j. j + length xs \<in> B}

goal (1 subgoal):
 1. nths (xs @ [x]) B = nths xs B @ [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) B = nths xs B @ [x]

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
 2. length xs \<notin> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) B = nths xs B @ [x]
[PROOF STEP]
have eqB: "prod_list (nths (xs @ [x]) B) = prod_list (nths xs B) * x"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) B = nths xs B @ [x]

goal (1 subgoal):
 1. prod_list (nths (xs @ [x]) B) = prod_list (nths xs B) * x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prod_list (nths (xs @ [x]) B) = prod_list (nths xs B) * x

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
 2. length xs \<notin> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
have "length xs \<notin> ?C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs \<notin> A - B
[PROOF STEP]
using True assms
[PROOF STATE]
proof (prove)
using this:
length xs \<in> B
B \<subseteq> A

goal (1 subgoal):
 1. length xs \<notin> A - B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length xs \<notin> A - B

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
 2. length xs \<notin> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs \<notin> A - B
[PROOF STEP]
have "nths (xs @ [x]) ?C = nths xs ?C"
[PROOF STATE]
proof (prove)
using this:
length xs \<notin> A - B

goal (1 subgoal):
 1. nths (xs @ [x]) (A - B) = nths xs (A - B)
[PROOF STEP]
using SC
[PROOF STATE]
proof (prove)
using this:
length xs \<notin> A - B
nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {j. j + length xs \<in> A - B}

goal (1 subgoal):
 1. nths (xs @ [x]) (A - B) = nths xs (A - B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) (A - B) = nths xs (A - B)

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
 2. length xs \<notin> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) (A - B) = nths xs (A - B)
[PROOF STEP]
have eqC: "prod_list (nths (xs @ [x]) ?C) = prod_list (nths xs ?C)"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) (A - B) = nths xs (A - B)

goal (1 subgoal):
 1. prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B))

goal (2 subgoals):
 1. length xs \<in> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
 2. length xs \<notin> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B))

goal (1 subgoal):
 1. prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
using snoc eqA eqB eqC
[PROOF STATE]
proof (prove)
using this:
prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B))
prod_list (nths xs A) = prod_list (nths xs B) * prod_list (nths xs (A - B))
prod_list (nths (xs @ [x]) A) = prod_list (nths xs A) * x
prod_list (nths (xs @ [x]) B) = prod_list (nths xs B) * x
prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B))

goal (1 subgoal):
 1. prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))

goal (1 subgoal):
 1. length xs \<notin> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length xs \<notin> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
length xs \<notin> B

goal (1 subgoal):
 1. length xs \<notin> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs \<notin> B
[PROOF STEP]
have "nths (xs @ [x]) B = nths xs B"
[PROOF STATE]
proof (prove)
using this:
length xs \<notin> B

goal (1 subgoal):
 1. nths (xs @ [x]) B = nths xs B
[PROOF STEP]
using SB
[PROOF STATE]
proof (prove)
using this:
length xs \<notin> B
nths (xs @ [x]) B = nths xs B @ nths [x] {j. j + length xs \<in> B}

goal (1 subgoal):
 1. nths (xs @ [x]) B = nths xs B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) B = nths xs B

goal (1 subgoal):
 1. length xs \<notin> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) B = nths xs B
[PROOF STEP]
have eqB: "prod_list (nths (xs @ [x]) B) = prod_list (nths xs B)"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) B = nths xs B

goal (1 subgoal):
 1. prod_list (nths (xs @ [x]) B) = prod_list (nths xs B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prod_list (nths (xs @ [x]) B) = prod_list (nths xs B)

goal (1 subgoal):
 1. length xs \<notin> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prod_list (nths (xs @ [x]) B) = prod_list (nths xs B)
[PROOF STEP]
have "length xs \<in> ?C"
[PROOF STATE]
proof (prove)
using this:
prod_list (nths (xs @ [x]) B) = prod_list (nths xs B)

goal (1 subgoal):
 1. length xs \<in> A - B
[PROOF STEP]
using True False assms
[PROOF STATE]
proof (prove)
using this:
prod_list (nths (xs @ [x]) B) = prod_list (nths xs B)
length xs \<in> A
length xs \<notin> B
B \<subseteq> A

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

goal (1 subgoal):
 1. length xs \<notin> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs \<in> A - B
[PROOF STEP]
have "nths (xs @ [x]) ?C = nths xs ?C @ [x]"
[PROOF STATE]
proof (prove)
using this:
length xs \<in> A - B

goal (1 subgoal):
 1. nths (xs @ [x]) (A - B) = nths xs (A - B) @ [x]
[PROOF STEP]
using SC
[PROOF STATE]
proof (prove)
using this:
length xs \<in> A - B
nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {j. j + length xs \<in> A - B}

goal (1 subgoal):
 1. nths (xs @ [x]) (A - B) = nths xs (A - B) @ [x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) (A - B) = nths xs (A - B) @ [x]

goal (1 subgoal):
 1. length xs \<notin> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) (A - B) = nths xs (A - B) @ [x]
[PROOF STEP]
have eqC: "prod_list (nths (xs @ [x]) ?C) = prod_list (nths xs ?C) * x"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) (A - B) = nths xs (A - B) @ [x]

goal (1 subgoal):
 1. prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B)) * x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B)) * x

goal (1 subgoal):
 1. length xs \<notin> B \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B)) * x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B)) * x

goal (1 subgoal):
 1. prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
using snoc eqA eqB eqC
[PROOF STATE]
proof (prove)
using this:
prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B)) * x
prod_list (nths xs A) = prod_list (nths xs B) * prod_list (nths xs (A - B))
prod_list (nths (xs @ [x]) A) = prod_list (nths xs A) * x
prod_list (nths (xs @ [x]) B) = prod_list (nths xs B)
prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B)) * x

goal (1 subgoal):
 1. prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
length xs \<notin> A

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs \<notin> A
[PROOF STEP]
have ninB: "length xs \<notin> B" and ninC: "length xs \<notin> ?C"
[PROOF STATE]
proof (prove)
using this:
length xs \<notin> A

goal (1 subgoal):
 1. length xs \<notin> B &&& length xs \<notin> A - B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xs \<notin> A
B \<subseteq> A

goal (1 subgoal):
 1. length xs \<notin> B &&& length xs \<notin> A - B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length xs \<notin> B
length xs \<notin> A - B

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
have "nths (xs @ [x]) A = nths xs A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A
[PROOF STEP]
using SA False nths_singleton
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) A = nths xs A @ nths [x] {j. j + length xs \<in> A}
length xs \<notin> A
nths [?x] ?A = (if 0 \<in> ?A then [?x] else [])

goal (1 subgoal):
 1. nths (xs @ [x]) A = nths xs A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) A = nths xs A

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) A = nths xs A
[PROOF STEP]
have eqA: "prod_list (nths (xs @ [x]) A) = prod_list (nths xs A)"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) A = nths xs A

goal (1 subgoal):
 1. prod_list (nths (xs @ [x]) A) = prod_list (nths xs A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prod_list (nths (xs @ [x]) A) = prod_list (nths xs A)

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
have "nths (xs @ [x]) B = nths xs B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (xs @ [x]) B = nths xs B
[PROOF STEP]
using SB ninB nths_singleton
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) B = nths xs B @ nths [x] {j. j + length xs \<in> B}
length xs \<notin> B
nths [?x] ?A = (if 0 \<in> ?A then [?x] else [])

goal (1 subgoal):
 1. nths (xs @ [x]) B = nths xs B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) B = nths xs B

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) B = nths xs B
[PROOF STEP]
have eqB: "prod_list (nths (xs @ [x]) B) = prod_list (nths xs B)"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) B = nths xs B

goal (1 subgoal):
 1. prod_list (nths (xs @ [x]) B) = prod_list (nths xs B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prod_list (nths (xs @ [x]) B) = prod_list (nths xs B)

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
have "nths (xs @ [x]) ?C = nths xs ?C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (xs @ [x]) (A - B) = nths xs (A - B)
[PROOF STEP]
using SC ninC nths_singleton
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) (A - B) = nths xs (A - B) @ nths [x] {j. j + length xs \<in> A - B}
length xs \<notin> A - B
nths [?x] ?A = (if 0 \<in> ?A then [?x] else [])

goal (1 subgoal):
 1. nths (xs @ [x]) (A - B) = nths xs (A - B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nths (xs @ [x]) (A - B) = nths xs (A - B)

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nths (xs @ [x]) (A - B) = nths xs (A - B)
[PROOF STEP]
have eqC: "prod_list (nths (xs @ [x]) ?C) = prod_list (nths xs ?C)"
[PROOF STATE]
proof (prove)
using this:
nths (xs @ [x]) (A - B) = nths xs (A - B)

goal (1 subgoal):
 1. prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B))

goal (1 subgoal):
 1. length xs \<notin> A \<Longrightarrow> prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B))

goal (1 subgoal):
 1. prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
using eqA eqB eqC snoc
[PROOF STATE]
proof (prove)
using this:
prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B))
prod_list (nths (xs @ [x]) A) = prod_list (nths xs A)
prod_list (nths (xs @ [x]) B) = prod_list (nths xs B)
prod_list (nths (xs @ [x]) (A - B)) = prod_list (nths xs (A - B))
prod_list (nths xs A) = prod_list (nths xs B) * prod_list (nths xs (A - B))

goal (1 subgoal):
 1. prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prod_list (nths (xs @ [x]) A) = prod_list (nths (xs @ [x]) B) * prod_list (nths (xs @ [x]) (A - B))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma digit_encode_take:
  "take n (digit_encode ds a) = digit_encode (take n ds) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take n (digit_encode ds a) = digit_encode (take n ds) a
[PROOF STEP]
proof (induct n arbitrary: ds a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ds a. take 0 (digit_encode ds a) = digit_encode (take 0 ds) a
 2. \<And>n ds a. (\<And>ds a. take n (digit_encode ds a) = digit_encode (take n ds) a) \<Longrightarrow> take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>ds a. take 0 (digit_encode ds a) = digit_encode (take 0 ds) a
 2. \<And>n ds a. (\<And>ds a. take n (digit_encode ds a) = digit_encode (take n ds) a) \<Longrightarrow> take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take 0 (digit_encode ds a) = digit_encode (take 0 ds) a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
take 0 (digit_encode ds a) = digit_encode (take 0 ds) a

goal (1 subgoal):
 1. \<And>n ds a. (\<And>ds a. take n (digit_encode ds a) = digit_encode (take n ds) a) \<Longrightarrow> take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n ds a. (\<And>ds a. take n (digit_encode ds a) = digit_encode (take n ds) a) \<Longrightarrow> take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
take n (digit_encode ?ds ?a) = digit_encode (take n ?ds) ?a

goal (1 subgoal):
 1. \<And>n ds a. (\<And>ds a. take n (digit_encode ds a) = digit_encode (take n ds) a) \<Longrightarrow> take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
take n (digit_encode ?ds ?a) = digit_encode (take n ?ds) ?a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
take n (digit_encode ?ds ?a) = digit_encode (take n ?ds) ?a

goal (1 subgoal):
 1. take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a
[PROOF STEP]
proof (cases ds)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>ds a. take n (digit_encode ds a) = digit_encode (take n ds) a; ds = []\<rbrakk> \<Longrightarrow> take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a
 2. \<And>a list. \<lbrakk>\<And>ds a. take n (digit_encode ds a) = digit_encode (take n ds) a; ds = a # list\<rbrakk> \<Longrightarrow> take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
ds = []

goal (2 subgoals):
 1. \<lbrakk>\<And>ds a. take n (digit_encode ds a) = digit_encode (take n ds) a; ds = []\<rbrakk> \<Longrightarrow> take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a
 2. \<And>a list. \<lbrakk>\<And>ds a. take n (digit_encode ds a) = digit_encode (take n ds) a; ds = a # list\<rbrakk> \<Longrightarrow> take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ds = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ds = []

goal (1 subgoal):
 1. take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<And>ds a. take n (digit_encode ds a) = digit_encode (take n ds) a; ds = a # list\<rbrakk> \<Longrightarrow> take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<And>ds a. take n (digit_encode ds a) = digit_encode (take n ds) a; ds = a # list\<rbrakk> \<Longrightarrow> take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a
[PROOF STEP]
case (Cons d ds')
[PROOF STATE]
proof (state)
this:
ds = d # ds'

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<And>ds a. take n (digit_encode ds a) = digit_encode (take n ds) a; ds = a # list\<rbrakk> \<Longrightarrow> take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ds = d # ds'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ds = d # ds'

goal (1 subgoal):
 1. take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a
[PROOF STEP]
by (auto simp add: Suc)
[PROOF STATE]
proof (state)
this:
take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
take (Suc n) (digit_encode ds a) = digit_encode (take (Suc n) ds) a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nths_minus_upt_eq_drop:
  "nths l (-{..<n}) = drop n l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths l (- {..<n}) = drop n l
[PROOF STEP]
apply (induct l rule: rev_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. nths [] (- {..<n}) = drop n []
 2. \<And>x xs. nths xs (- {..<n}) = drop n xs \<Longrightarrow> nths (xs @ [x]) (- {..<n}) = drop n (xs @ [x])
[PROOF STEP]
by (auto simp add: nths_append)


[STATEMENT]
lemma digit_encode_drop:
  "drop n (digit_encode ds a) = digit_encode (drop n ds) (a div (prod_list (take n ds)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop n (digit_encode ds a) = digit_encode (drop n ds) (a div prod_list (take n ds))
[PROOF STEP]
proof (induct n arbitrary: ds a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ds a. drop 0 (digit_encode ds a) = digit_encode (drop 0 ds) (a div prod_list (take 0 ds))
 2. \<And>n ds a. (\<And>ds a. drop n (digit_encode ds a) = digit_encode (drop n ds) (a div prod_list (take n ds))) \<Longrightarrow> drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>ds a. drop 0 (digit_encode ds a) = digit_encode (drop 0 ds) (a div prod_list (take 0 ds))
 2. \<And>n ds a. (\<And>ds a. drop n (digit_encode ds a) = digit_encode (drop n ds) (a div prod_list (take n ds))) \<Longrightarrow> drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop 0 (digit_encode ds a) = digit_encode (drop 0 ds) (a div prod_list (take 0 ds))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
drop 0 (digit_encode ds a) = digit_encode (drop 0 ds) (a div prod_list (take 0 ds))

goal (1 subgoal):
 1. \<And>n ds a. (\<And>ds a. drop n (digit_encode ds a) = digit_encode (drop n ds) (a div prod_list (take n ds))) \<Longrightarrow> drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n ds a. (\<And>ds a. drop n (digit_encode ds a) = digit_encode (drop n ds) (a div prod_list (take n ds))) \<Longrightarrow> drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
drop n (digit_encode ?ds ?a) = digit_encode (drop n ?ds) (?a div prod_list (take n ?ds))

goal (1 subgoal):
 1. \<And>n ds a. (\<And>ds a. drop n (digit_encode ds a) = digit_encode (drop n ds) (a div prod_list (take n ds))) \<Longrightarrow> drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
drop n (digit_encode ?ds ?a) = digit_encode (drop n ?ds) (?a div prod_list (take n ?ds))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
drop n (digit_encode ?ds ?a) = digit_encode (drop n ?ds) (?a div prod_list (take n ?ds))

goal (1 subgoal):
 1. drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))
[PROOF STEP]
proof (cases ds)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>ds a. drop n (digit_encode ds a) = digit_encode (drop n ds) (a div prod_list (take n ds)); ds = []\<rbrakk> \<Longrightarrow> drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))
 2. \<And>a list. \<lbrakk>\<And>ds a. drop n (digit_encode ds a) = digit_encode (drop n ds) (a div prod_list (take n ds)); ds = a # list\<rbrakk> \<Longrightarrow> drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
ds = []

goal (2 subgoals):
 1. \<lbrakk>\<And>ds a. drop n (digit_encode ds a) = digit_encode (drop n ds) (a div prod_list (take n ds)); ds = []\<rbrakk> \<Longrightarrow> drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))
 2. \<And>a list. \<lbrakk>\<And>ds a. drop n (digit_encode ds a) = digit_encode (drop n ds) (a div prod_list (take n ds)); ds = a # list\<rbrakk> \<Longrightarrow> drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ds = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ds = []

goal (1 subgoal):
 1. drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<And>ds a. drop n (digit_encode ds a) = digit_encode (drop n ds) (a div prod_list (take n ds)); ds = a # list\<rbrakk> \<Longrightarrow> drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<And>ds a. drop n (digit_encode ds a) = digit_encode (drop n ds) (a div prod_list (take n ds)); ds = a # list\<rbrakk> \<Longrightarrow> drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))
[PROOF STEP]
case (Cons d ds')
[PROOF STATE]
proof (state)
this:
ds = d # ds'

goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<And>ds a. drop n (digit_encode ds a) = digit_encode (drop n ds) (a div prod_list (take n ds)); ds = a # list\<rbrakk> \<Longrightarrow> drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ds = d # ds'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ds = d # ds'

goal (1 subgoal):
 1. drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))
[PROOF STEP]
by (auto simp add: Suc div_mult2_eq)
[PROOF STATE]
proof (state)
this:
drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
drop (Suc n) (digit_encode ds a) = digit_encode (drop (Suc n) ds) (a div prod_list (take (Suc n) ds))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dims1_alter:
  assumes "avars \<subseteq> A"
  shows "dims1 = nths dims (A \<inter> vars)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dims1 = nths dims (A \<inter> vars)
[PROOF STEP]
using nths_intersection_eq assms
[PROOF STATE]
proof (prove)
using this:
{0..<length ?xs} \<subseteq> ?A \<Longrightarrow> nths ?xs ?B = nths ?xs (?A \<inter> ?B)
avars \<subseteq> A

goal (1 subgoal):
 1. dims1 = nths dims (A \<inter> vars)
[PROOF STEP]
unfolding dims1_def
[PROOF STATE]
proof (prove)
using this:
{0..<length ?xs} \<subseteq> ?A \<Longrightarrow> nths ?xs ?B = nths ?xs (?A \<inter> ?B)
avars \<subseteq> A

goal (1 subgoal):
 1. nths dims vars = nths dims (A \<inter> vars)
[PROOF STEP]
by auto


[STATEMENT]
lemma dims2_alter:
  assumes "avars \<subseteq> A"
  shows "dims2 = nths dims (A-vars)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dims2 = nths dims (A - vars)
[PROOF STEP]
using nths_minus_eq assms
[PROOF STATE]
proof (prove)
using this:
{0..<length ?xs} \<subseteq> ?A \<Longrightarrow> nths ?xs (- ?B) = nths ?xs (?A - ?B)
avars \<subseteq> A

goal (1 subgoal):
 1. dims2 = nths dims (A - vars)
[PROOF STEP]
unfolding dims2_def
[PROOF STATE]
proof (prove)
using this:
{0..<length ?xs} \<subseteq> ?A \<Longrightarrow> nths ?xs (- ?B) = nths ?xs (?A - ?B)
avars \<subseteq> A

goal (1 subgoal):
 1. nths dims (- vars) = nths dims (A - vars)
[PROOF STEP]
by auto


[STATEMENT]
lemma encode1_alter:
  assumes "avars \<subseteq> A"
  shows "encode1 i = digit_decode dims1 (nths (digit_encode dims i) (A \<inter> vars))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. encode1 i = digit_decode dims1 (nths (digit_encode dims i) (A \<inter> vars))
[PROOF STEP]
using length_digit_encode[of dims i] nths_intersection_eq[of "digit_encode dims i" A vars] assms
[PROOF STATE]
proof (prove)
using this:
length (digit_encode dims i) = length dims
{0..<length (digit_encode dims i)} \<subseteq> A \<Longrightarrow> nths (digit_encode dims i) vars = nths (digit_encode dims i) (A \<inter> vars)
avars \<subseteq> A

goal (1 subgoal):
 1. encode1 i = digit_decode dims1 (nths (digit_encode dims i) (A \<inter> vars))
[PROOF STEP]
unfolding encode1_def
[PROOF STATE]
proof (prove)
using this:
length (digit_encode dims i) = length dims
{0..<length (digit_encode dims i)} \<subseteq> A \<Longrightarrow> nths (digit_encode dims i) vars = nths (digit_encode dims i) (A \<inter> vars)
avars \<subseteq> A

goal (1 subgoal):
 1. digit_decode dims1 (nths (digit_encode dims i) vars) = digit_decode dims1 (nths (digit_encode dims i) (A \<inter> vars))
[PROOF STEP]
by (subgoal_tac "nths (digit_encode dims i) (vars) = nths (digit_encode dims i) (A \<inter> vars)", auto)


[STATEMENT]
lemma encode2_alter:
  assumes "avars \<subseteq> A"
  shows "encode2 i = digit_decode dims2 (nths (digit_encode dims i) (A-vars))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. encode2 i = digit_decode dims2 (nths (digit_encode dims i) (A - vars))
[PROOF STEP]
using length_digit_encode[of dims i] nths_minus_eq[of "digit_encode dims i" A] assms
[PROOF STATE]
proof (prove)
using this:
length (digit_encode dims i) = length dims
{0..<length (digit_encode dims i)} \<subseteq> A \<Longrightarrow> nths (digit_encode dims i) (- ?B) = nths (digit_encode dims i) (A - ?B)
avars \<subseteq> A

goal (1 subgoal):
 1. encode2 i = digit_decode dims2 (nths (digit_encode dims i) (A - vars))
[PROOF STEP]
unfolding encode2_def
[PROOF STATE]
proof (prove)
using this:
length (digit_encode dims i) = length dims
{0..<length (digit_encode dims i)} \<subseteq> A \<Longrightarrow> nths (digit_encode dims i) (- ?B) = nths (digit_encode dims i) (A - ?B)
avars \<subseteq> A

goal (1 subgoal):
 1. digit_decode dims2 (nths (digit_encode dims i) (- vars)) = digit_decode dims2 (nths (digit_encode dims i) (A - vars))
[PROOF STEP]
by (subgoal_tac "nths (digit_encode dims i) (- vars) = nths (digit_encode dims i) (A - vars)", auto)


[STATEMENT]
lemma encode1_lt [simp]:
  assumes "i < d"
  shows "encode1 i < d1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. encode1 i < d1
[PROOF STEP]
unfolding d1_def encode1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit_decode dims1 (nths (digit_encode dims i) vars) < prod_list dims1
[PROOF STEP]
apply (rule digit_decode_lt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (digit_encode dims i) vars \<lhd> dims1
[PROOF STEP]
using dims1_def assms d_def digit_encode_valid_index valid_index_nths
[PROOF STATE]
proof (prove)
using this:
dims1 = nths dims vars
i < d
d = prod_list dims
?a < prod_list ?ds \<Longrightarrow> digit_encode ?ds ?a \<lhd> ?ds
?is \<lhd> ?ds \<Longrightarrow> nths ?is ?A \<lhd> nths ?ds ?A

goal (1 subgoal):
 1. nths (digit_encode dims i) vars \<lhd> dims1
[PROOF STEP]
by auto


[STATEMENT]
lemma encode2_lt [simp]:
  assumes "i < d"
  shows "encode2 i < d2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. encode2 i < d2
[PROOF STEP]
unfolding d2_def encode2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit_decode dims2 (nths (digit_encode dims i) (- vars)) < prod_list dims2
[PROOF STEP]
apply (rule digit_decode_lt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (digit_encode dims i) (- vars) \<lhd> dims2
[PROOF STEP]
using dims2_def assms d_def digit_encode_valid_index valid_index_nths
[PROOF STATE]
proof (prove)
using this:
dims2 = nths dims (- vars)
i < d
d = prod_list dims
?a < prod_list ?ds \<Longrightarrow> digit_encode ?ds ?a \<lhd> ?ds
?is \<lhd> ?ds \<Longrightarrow> nths ?is ?A \<lhd> nths ?ds ?A

goal (1 subgoal):
 1. nths (digit_encode dims i) (- vars) \<lhd> dims2
[PROOF STEP]
by auto


[STATEMENT]
lemma encode12_inv:
  assumes "k < d"
  shows "encode12 (encode1 k, encode2 k) = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. encode12 (encode1 k, encode2 k) = k
[PROOF STEP]
unfolding encode12.simps encode1_def encode2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit_decode dims (weave vars (digit_encode dims1 (digit_decode dims1 (nths (digit_encode dims k) vars))) (digit_encode dims2 (digit_decode dims2 (nths (digit_encode dims k) (- vars))))) = k
[PROOF STEP]
using assms d_def digit_encode_valid_index dims1_def dims2_def valid_index_nths
[PROOF STATE]
proof (prove)
using this:
k < d
d = prod_list dims
?a < prod_list ?ds \<Longrightarrow> digit_encode ?ds ?a \<lhd> ?ds
dims1 = nths dims vars
dims2 = nths dims (- vars)
?is \<lhd> ?ds \<Longrightarrow> nths ?is ?A \<lhd> nths ?ds ?A

goal (1 subgoal):
 1. digit_decode dims (weave vars (digit_encode dims1 (digit_decode dims1 (nths (digit_encode dims k) vars))) (digit_encode dims2 (digit_decode dims2 (nths (digit_encode dims k) (- vars))))) = k
[PROOF STEP]
by auto


[STATEMENT]
lemma encode12_inv1:
  assumes "i < d1" "j < d2"
  shows "encode1 (encode12 (i, j)) = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. encode1 (encode12 (i, j)) = i
[PROOF STEP]
unfolding encode12.simps encode1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit_decode dims1 (nths (digit_encode dims (digit_decode dims (weave vars (digit_encode dims1 i) (digit_encode dims2 j)))) vars) = i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < d1
j < d2

goal (1 subgoal):
 1. digit_decode dims1 (nths (digit_encode dims (digit_decode dims (weave vars (digit_encode dims1 i) (digit_encode dims2 j)))) vars) = i
[PROOF STEP]
unfolding d1_def d2_def dims1_def dims2_def
[PROOF STATE]
proof (prove)
using this:
i < prod_list (nths dims vars)
j < prod_list (nths dims (- vars))

goal (1 subgoal):
 1. digit_decode (nths dims vars) (nths (digit_encode dims (digit_decode dims (weave vars (digit_encode (nths dims vars) i) (digit_encode (nths dims (- vars)) j)))) vars) = i
[PROOF STEP]
by (metis digit_decode_encode_lt digit_encode_decode digit_encode_valid_index valid_index_weave(1,2))


[STATEMENT]
lemma encode12_inv2:
  assumes "i < d1" "j < d2"
  shows "encode2 (encode12 (i, j)) = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. encode2 (encode12 (i, j)) = j
[PROOF STEP]
unfolding encode12.simps encode2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digit_decode dims2 (nths (digit_encode dims (digit_decode dims (weave vars (digit_encode dims1 i) (digit_encode dims2 j)))) (- vars)) = j
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < d1
j < d2

goal (1 subgoal):
 1. digit_decode dims2 (nths (digit_encode dims (digit_decode dims (weave vars (digit_encode dims1 i) (digit_encode dims2 j)))) (- vars)) = j
[PROOF STEP]
unfolding d1_def d2_def dims1_def dims2_def
[PROOF STATE]
proof (prove)
using this:
i < prod_list (nths dims vars)
j < prod_list (nths dims (- vars))

goal (1 subgoal):
 1. digit_decode (nths dims (- vars)) (nths (digit_encode dims (digit_decode dims (weave vars (digit_encode (nths dims vars) i) (digit_encode (nths dims (- vars)) j)))) (- vars)) = j
[PROOF STEP]
by (metis digit_decode_encode_lt digit_encode_decode digit_encode_valid_index valid_index_weave(1,3))


[STATEMENT]
lemma encode12_lt:
  assumes "i < d1" "j < d2"
  shows "encode12 (i, j) < d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. encode12 (i, j) < d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < d1
j < d2

goal (1 subgoal):
 1. encode12 (i, j) < d
[PROOF STEP]
unfolding encode12.simps d_def d1_def d2_def dims1_def dims2_def
[PROOF STATE]
proof (prove)
using this:
i < prod_list (nths dims vars)
j < prod_list (nths dims (- vars))

goal (1 subgoal):
 1. digit_decode dims (weave vars (digit_encode (nths dims vars) i) (digit_encode (nths dims (- vars)) j)) < prod_list dims
[PROOF STEP]
by (simp add: digit_decode_lt digit_encode_valid_index valid_index_weave(1))


[STATEMENT]
lemma sum_encode: "(\<Sum>i = 0..<d1. \<Sum>j = 0..<d2. f i j) = sum (\<lambda>k. f (encode1 k) (encode2 k)) {0..<d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<d1. sum (f i) {0..<d2}) = (\<Sum>k = 0..<d. f (encode1 k) (encode2 k))
[PROOF STEP]
apply (subst sum.cartesian_product)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(x, y)\<in>{0..<d1} \<times> {0..<d2}. f x y) = (\<Sum>k = 0..<d. f (encode1 k) (encode2 k))
[PROOF STEP]
apply (rule sum.reindex_bij_witness[where i="\<lambda>k. (encode1 k, encode2 k)" and j=encode12])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a. a \<in> {0..<d1} \<times> {0..<d2} \<Longrightarrow> (encode1 (encode12 a), encode2 (encode12 a)) = a
 2. \<And>a. a \<in> {0..<d1} \<times> {0..<d2} \<Longrightarrow> encode12 a \<in> {0..<d}
 3. \<And>b. b \<in> {0..<d} \<Longrightarrow> encode12 (encode1 b, encode2 b) = b
 4. \<And>b. b \<in> {0..<d} \<Longrightarrow> (encode1 b, encode2 b) \<in> {0..<d1} \<times> {0..<d2}
 5. \<And>a. a \<in> {0..<d1} \<times> {0..<d2} \<Longrightarrow> f (encode1 (encode12 a)) (encode2 (encode12 a)) = (case a of (x, xa) \<Rightarrow> f x xa)
[PROOF STEP]
by (auto simp: encode12_inv1 encode12_inv2 encode12_inv encode12_lt)


[STATEMENT]
lemma tensor_vec_dim [simp]:
  "dim_vec (tensor_vec v1 v2) = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (tensor_vec v1 v2) = d
[PROOF STEP]
unfolding tensor_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (Matrix.vec d (\<lambda>i. v1 $ encode1 i * v2 $ encode2 i)) = d
[PROOF STEP]
by auto


[STATEMENT]
lemma tensor_vec_carrier:
  "tensor_vec v1 v2 \<in> carrier_vec d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_vec v1 v2 \<in> carrier_vec d
[PROOF STEP]
unfolding tensor_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix.vec d (\<lambda>i. v1 $ encode1 i * v2 $ encode2 i) \<in> carrier_vec d
[PROOF STEP]
by auto


[STATEMENT]
lemma tensor_vec_eval:
  assumes "i < d"
  shows "tensor_vec v1 v2 $ i = v1 $ encode1 i * v2 $ encode2 i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_vec v1 v2 $ i = v1 $ encode1 i * v2 $ encode2 i
[PROOF STEP]
unfolding tensor_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix.vec d (\<lambda>i. v1 $ encode1 i * v2 $ encode2 i) $ i = v1 $ encode1 i * v2 $ encode2 i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < d

goal (1 subgoal):
 1. Matrix.vec d (\<lambda>i. v1 $ encode1 i * v2 $ encode2 i) $ i = v1 $ encode1 i * v2 $ encode2 i
[PROOF STEP]
by simp


[STATEMENT]
lemma tensor_vec_add1:
  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 "tensor_vec (v1 + v2) v3 = tensor_vec v1 v3 + tensor_vec v2 v3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_vec (v1 + v2) v3 = tensor_vec v1 v3 + tensor_vec v2 v3
[PROOF STEP]
apply (rule eq_vecI, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> tensor_vec (v1 + v2) v3 $ i = tensor_vec v1 v3 $ i + tensor_vec v2 v3 $ i
[PROOF STEP]
unfolding tensor_vec_eval
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> (v1 + v2) $ encode1 i * v3 $ encode2 i = v1 $ encode1 i * v3 $ encode2 i + v2 $ encode1 i * v3 $ encode2 i
[PROOF STEP]
using assms(2) comm_semiring_class.distrib
[PROOF STATE]
proof (prove)
using this:
v2 \<in> carrier_vec d1
(?a + ?b) * ?c = ?a * ?c + ?b * ?c

goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> (v1 + v2) $ encode1 i * v3 $ encode2 i = v1 $ encode1 i * v3 $ encode2 i + v2 $ encode1 i * v3 $ encode2 i
[PROOF STEP]
by force


[STATEMENT]
lemma tensor_vec_add2:
  fixes v1 v2 v3 :: "'a::comm_ring vec"
  assumes "v1 \<in> carrier_vec d1"
    and "v2 \<in> carrier_vec d2"
    and "v3 \<in> carrier_vec d2"
  shows "tensor_vec v1 (v2 + v3) = tensor_vec v1 v2 + tensor_vec v1 v3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_vec v1 (v2 + v3) = tensor_vec v1 v2 + tensor_vec v1 v3
[PROOF STEP]
apply (rule eq_vecI, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> tensor_vec v1 (v2 + v3) $ i = tensor_vec v1 v2 $ i + tensor_vec v1 v3 $ i
[PROOF STEP]
unfolding tensor_vec_eval
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> v1 $ encode1 i * (v2 + v3) $ encode2 i = v1 $ encode1 i * v2 $ encode2 i + v1 $ encode1 i * v3 $ encode2 i
[PROOF STEP]
using assms(3) semiring_class.distrib_left
[PROOF STATE]
proof (prove)
using this:
v3 \<in> carrier_vec d2
?a * (?b + ?c) = ?a * ?b + ?a * ?c

goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> v1 $ encode1 i * (v2 + v3) $ encode2 i = v1 $ encode1 i * v2 $ encode2 i + v1 $ encode1 i * v3 $ encode2 i
[PROOF STEP]
by force


[STATEMENT]
lemma tensor_mat_dim_row [simp]:
  "dim_row (tensor_mat m1 m2) = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (tensor_mat m1 m2) = d
[PROOF STEP]
unfolding tensor_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (mat d d (\<lambda>(i, j). m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j))) = d
[PROOF STEP]
by auto


[STATEMENT]
lemma tensor_mat_dim_col [simp]:
  "dim_col (tensor_mat m1 m2) = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (tensor_mat m1 m2) = d
[PROOF STEP]
unfolding tensor_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (mat d d (\<lambda>(i, j). m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j))) = d
[PROOF STEP]
by auto


[STATEMENT]
lemma tensor_mat_carrier:
  "tensor_mat m1 m2 \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat m1 m2 \<in> carrier_mat d d
[PROOF STEP]
unfolding tensor_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat d d (\<lambda>(i, j). m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j)) \<in> carrier_mat d d
[PROOF STEP]
by auto


[STATEMENT]
lemma tensor_mat_eval:
  assumes "i < d" "j < d"
  shows "tensor_mat m1 m2 $$ (i, j) = m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat m1 m2 $$ (i, j) = m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j)
[PROOF STEP]
unfolding tensor_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat d d (\<lambda>(i, j). m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j)) $$ (i, j) = m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < d
j < d

goal (1 subgoal):
 1. mat d d (\<lambda>(i, j). m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j)) $$ (i, j) = m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j)
[PROOF STEP]
by simp


[STATEMENT]
lemma tensor_mat_zero1:
  shows "tensor_mat (0\<^sub>m d1 d1) m1 = 0\<^sub>m d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (0\<^sub>m d1 d1) m1 = 0\<^sub>m d d
[PROOF STEP]
apply (rule eq_matI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (0\<^sub>m d d); j < dim_col (0\<^sub>m d d)\<rbrakk> \<Longrightarrow> tensor_mat (0\<^sub>m d1 d1) m1 $$ (i, j) = 0\<^sub>m d d $$ (i, j)
 2. dim_row (tensor_mat (0\<^sub>m d1 d1) m1) = dim_row (0\<^sub>m d d)
 3. dim_col (tensor_mat (0\<^sub>m d1 d1) m1) = dim_col (0\<^sub>m d d)
[PROOF STEP]
by (auto simp add: tensor_mat_eval)


[STATEMENT]
lemma tensor_mat_zero2:
  shows "tensor_mat m1 (0\<^sub>m d2 d2) = 0\<^sub>m d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat m1 (0\<^sub>m d2 d2) = 0\<^sub>m d d
[PROOF STEP]
apply (rule eq_matI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (0\<^sub>m d d); j < dim_col (0\<^sub>m d d)\<rbrakk> \<Longrightarrow> tensor_mat m1 (0\<^sub>m d2 d2) $$ (i, j) = 0\<^sub>m d d $$ (i, j)
 2. dim_row (tensor_mat m1 (0\<^sub>m d2 d2)) = dim_row (0\<^sub>m d d)
 3. dim_col (tensor_mat m1 (0\<^sub>m d2 d2)) = dim_col (0\<^sub>m d d)
[PROOF STEP]
by (auto simp add: tensor_mat_eval)


[STATEMENT]
lemma tensor_mat_add1:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d1 d1"
    and "m3 \<in> carrier_mat d2 d2"
  shows "tensor_mat (m1 + m2) m3 = tensor_mat m1 m3 + tensor_mat m2 m3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (m1 + m2) m3 = tensor_mat m1 m3 + tensor_mat m2 m3
[PROOF STEP]
apply (rule eq_matI, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (m1 + m2) m3 $$ (i, j) = tensor_mat m1 m3 $$ (i, j) + tensor_mat m2 m3 $$ (i, j)
[PROOF STEP]
unfolding tensor_mat_eval
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> (m1 + m2) $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j) = m1 $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j) + m2 $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j)
[PROOF STEP]
using assms(2) comm_semiring_class.distrib
[PROOF STATE]
proof (prove)
using this:
m2 \<in> carrier_mat d1 d1
(?a + ?b) * ?c = ?a * ?c + ?b * ?c

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> (m1 + m2) $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j) = m1 $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j) + m2 $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j)
[PROOF STEP]
by force


[STATEMENT]
lemma tensor_mat_add2:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d2 d2"
    and "m3 \<in> carrier_mat d2 d2"
  shows "tensor_mat m1 (m2 + m3) = tensor_mat m1 m2 + tensor_mat m1 m3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat m1 (m2 + m3) = tensor_mat m1 m2 + tensor_mat m1 m3
[PROOF STEP]
apply (rule eq_matI, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat m1 (m2 + m3) $$ (i, j) = tensor_mat m1 m2 $$ (i, j) + tensor_mat m1 m3 $$ (i, j)
[PROOF STEP]
unfolding tensor_mat_eval
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> m1 $$ (encode1 i, encode1 j) * (m2 + m3) $$ (encode2 i, encode2 j) = m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j) + m1 $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j)
[PROOF STEP]
using assms(3) semiring_class.distrib_left
[PROOF STATE]
proof (prove)
using this:
m3 \<in> carrier_mat d2 d2
?a * (?b + ?c) = ?a * ?b + ?a * ?c

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> m1 $$ (encode1 i, encode1 j) * (m2 + m3) $$ (encode2 i, encode2 j) = m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j) + m1 $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j)
[PROOF STEP]
by force


[STATEMENT]
lemma tensor_mat_minus1:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d1 d1"
    and "m3 \<in> carrier_mat d2 d2"
  shows "tensor_mat (m1 - m2) m3 = tensor_mat m1 m3 - tensor_mat m2 m3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (m1 - m2) m3 = tensor_mat m1 m3 - tensor_mat m2 m3
[PROOF STEP]
apply (rule eq_matI, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (m1 - m2) m3 $$ (i, j) = tensor_mat m1 m3 $$ (i, j) - tensor_mat m2 m3 $$ (i, j)
[PROOF STEP]
unfolding tensor_mat_eval
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> (m1 - m2) $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j) = m1 $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j) - m2 $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j)
[PROOF STEP]
apply (subst index_minus_mat)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> encode1 i < dim_row m2
 2. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> encode1 j < dim_col m2
 3. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> (m1 $$ (encode1 i, encode1 j) - m2 $$ (encode1 i, encode1 j)) * m3 $$ (encode2 i, encode2 j) = m1 $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j) - m2 $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i_ < d; j_ < d\<rbrakk> \<Longrightarrow> encode1 i_ < dim_row m2
[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 (1 subgoal):
 1. \<lbrakk>i_ < d; j_ < d\<rbrakk> \<Longrightarrow> encode1 i_ < dim_row m2
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> encode1 j < dim_col m2
 2. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> (m1 $$ (encode1 i, encode1 j) - m2 $$ (encode1 i, encode1 j)) * m3 $$ (encode2 i, encode2 j) = m1 $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j) - m2 $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i_ < d; j_ < d\<rbrakk> \<Longrightarrow> encode1 j_ < dim_col m2
[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 (1 subgoal):
 1. \<lbrakk>i_ < d; j_ < d\<rbrakk> \<Longrightarrow> encode1 j_ < dim_col m2
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> (m1 $$ (encode1 i, encode1 j) - m2 $$ (encode1 i, encode1 j)) * m3 $$ (encode2 i, encode2 j) = m1 $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j) - m2 $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j)
[PROOF STEP]
using assms(2) ring_class.left_diff_distrib
[PROOF STATE]
proof (prove)
using this:
m2 \<in> carrier_mat d1 d1
(?a - ?b) * ?c = ?a * ?c - ?b * ?c

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> (m1 $$ (encode1 i, encode1 j) - m2 $$ (encode1 i, encode1 j)) * m3 $$ (encode2 i, encode2 j) = m1 $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j) - m2 $$ (encode1 i, encode1 j) * m3 $$ (encode2 i, encode2 j)
[PROOF STEP]
by force


[STATEMENT]
lemma tensor_mat_matrix_sum2:
  assumes "m1 \<in> carrier_mat d1 d1"
  shows "(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2)
    \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n)
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>k. k < 0 \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) 0 = tensor_mat m1 (matrix_sum d2 f 0)
 2. \<And>n. \<lbrakk>(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n); \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d2 d2\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (matrix_sum d2 f (Suc n))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
?k2 < 0 \<Longrightarrow> f ?k2 \<in> carrier_mat d2 d2

goal (2 subgoals):
 1. (\<And>k. k < 0 \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) 0 = tensor_mat m1 (matrix_sum d2 f 0)
 2. \<And>n. \<lbrakk>(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n); \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d2 d2\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (matrix_sum d2 f (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k2 < 0 \<Longrightarrow> f ?k2 \<in> carrier_mat d2 d2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?k2 < 0 \<Longrightarrow> f ?k2 \<in> carrier_mat d2 d2

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) 0 = tensor_mat m1 (matrix_sum d2 f 0)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>m d d = tensor_mat m1 (0\<^sub>m d2 d2)
[PROOF STEP]
using tensor_mat_zero2[of m1]
[PROOF STATE]
proof (prove)
using this:
tensor_mat m1 (0\<^sub>m d2 d2) = 0\<^sub>m d d

goal (1 subgoal):
 1. 0\<^sub>m d d = tensor_mat m1 (0\<^sub>m d2 d2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) 0 = tensor_mat m1 (matrix_sum d2 f 0)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n); \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d2 d2\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (matrix_sum d2 f (Suc n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n); \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d2 d2\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (matrix_sum d2 f (Suc n))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n)
?k2 < Suc n \<Longrightarrow> f ?k2 \<in> carrier_mat d2 d2

goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n); \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d2 d2\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (matrix_sum d2 f (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n)
?k2 < Suc n \<Longrightarrow> f ?k2 \<in> carrier_mat d2 d2
[PROOF STEP]
have "k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2" for k
[PROOF STATE]
proof (prove)
using this:
(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n)
?k2 < Suc n \<Longrightarrow> f ?k2 \<in> carrier_mat d2 d2

goal (1 subgoal):
 1. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k2 < n \<Longrightarrow> f ?k2 \<in> carrier_mat d2 d2

goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n); \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d2 d2\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (matrix_sum d2 f (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k2 < n \<Longrightarrow> f ?k2 \<in> carrier_mat d2 d2
[PROOF STEP]
have ds: "matrix_sum d2 f n \<in> carrier_mat d2 d2"
[PROOF STATE]
proof (prove)
using this:
?k2 < n \<Longrightarrow> f ?k2 \<in> carrier_mat d2 d2

goal (1 subgoal):
 1. matrix_sum d2 f n \<in> carrier_mat d2 d2
[PROOF STEP]
using matrix_sum_dim
[PROOF STATE]
proof (prove)
using this:
?k2 < n \<Longrightarrow> f ?k2 \<in> carrier_mat d2 d2
(\<And>k. k < ?n \<Longrightarrow> ?f k \<in> carrier_mat ?d ?d) \<Longrightarrow> matrix_sum ?d ?f ?n \<in> carrier_mat ?d ?d

goal (1 subgoal):
 1. matrix_sum d2 f n \<in> carrier_mat d2 d2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d2 f n \<in> carrier_mat d2 d2

goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n); \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d2 d2\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (matrix_sum d2 f (Suc n))
[PROOF STEP]
have dn: "f n \<in> carrier_mat d2 d2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f n \<in> carrier_mat d2 d2
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n)
?k2 < Suc n \<Longrightarrow> f ?k2 \<in> carrier_mat d2 d2

goal (1 subgoal):
 1. f n \<in> carrier_mat d2 d2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f n \<in> carrier_mat d2 d2

goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n); \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d2 d2\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (matrix_sum d2 f (Suc n))
[PROOF STEP]
have "matrix_sum d2 f (Suc n) = f n + matrix_sum d2 f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_sum d2 f (Suc n) = f n + matrix_sum d2 f n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
matrix_sum d2 f (Suc n) = f n + matrix_sum d2 f n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n); \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d2 d2\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (matrix_sum d2 f (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matrix_sum d2 f (Suc n) = f n + matrix_sum d2 f n
[PROOF STEP]
have eq: "tensor_mat m1 (matrix_sum d2 f (Suc n))
    = tensor_mat m1 (f n) + tensor_mat m1 (matrix_sum d2 f n)"
[PROOF STATE]
proof (prove)
using this:
matrix_sum d2 f (Suc n) = f n + matrix_sum d2 f n

goal (1 subgoal):
 1. tensor_mat m1 (matrix_sum d2 f (Suc n)) = tensor_mat m1 (f n) + tensor_mat m1 (matrix_sum d2 f n)
[PROOF STEP]
using tensor_mat_add2 dn ds assms
[PROOF STATE]
proof (prove)
using this:
matrix_sum d2 f (Suc n) = f n + matrix_sum d2 f n
\<lbrakk>?m1.0 \<in> carrier_mat d1 d1; ?m2.0 \<in> carrier_mat d2 d2; ?m3.0 \<in> carrier_mat d2 d2\<rbrakk> \<Longrightarrow> tensor_mat ?m1.0 (?m2.0 + ?m3.0) = tensor_mat ?m1.0 ?m2.0 + tensor_mat ?m1.0 ?m3.0
f n \<in> carrier_mat d2 d2
matrix_sum d2 f n \<in> carrier_mat d2 d2
m1 \<in> carrier_mat d1 d1

goal (1 subgoal):
 1. tensor_mat m1 (matrix_sum d2 f (Suc n)) = tensor_mat m1 (f n) + tensor_mat m1 (matrix_sum d2 f n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tensor_mat m1 (matrix_sum d2 f (Suc n)) = tensor_mat m1 (f n) + tensor_mat m1 (matrix_sum d2 f n)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n); \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d2 d2\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (matrix_sum d2 f (Suc n))
[PROOF STEP]
have "matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n)
    = tensor_mat m1 (f n) + matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (f n) + matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (f n) + matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n); \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d2 d2\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (matrix_sum d2 f (Suc n))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (f n) + matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n); \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d2 d2\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (matrix_sum d2 f (Suc n))
[PROOF STEP]
have "\<dots> = tensor_mat m1 (f n) + tensor_mat m1 (matrix_sum d2 f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat m1 (f n) + matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (f n) + tensor_mat m1 (matrix_sum d2 f n)
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n)
?k2 < Suc n \<Longrightarrow> f ?k2 \<in> carrier_mat d2 d2

goal (1 subgoal):
 1. tensor_mat m1 (f n) + matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (f n) + tensor_mat m1 (matrix_sum d2 f n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tensor_mat m1 (f n) + matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (f n) + tensor_mat m1 (matrix_sum d2 f n)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>(\<And>k. k < n \<Longrightarrow> f k \<in> carrier_mat d2 d2) \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) n = tensor_mat m1 (matrix_sum d2 f n); \<And>k. k < Suc n \<Longrightarrow> f k \<in> carrier_mat d2 d2\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (matrix_sum d2 f (Suc n))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (f n) + tensor_mat m1 (matrix_sum d2 f n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (f n) + tensor_mat m1 (matrix_sum d2 f n)

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (matrix_sum d2 f (Suc n))
[PROOF STEP]
using eq
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (f n) + tensor_mat m1 (matrix_sum d2 f n)
tensor_mat m1 (matrix_sum d2 f (Suc n)) = tensor_mat m1 (f n) + tensor_mat m1 (matrix_sum d2 f n)

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (matrix_sum d2 f (Suc n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. tensor_mat m1 (f k)) (Suc n) = tensor_mat m1 (matrix_sum d2 f (Suc n))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tensor_mat_scale1:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d2 d2"
  shows "tensor_mat (a \<cdot>\<^sub>m m1) m2 = a \<cdot>\<^sub>m tensor_mat m1 m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (a \<cdot>\<^sub>m m1) m2 = a \<cdot>\<^sub>m tensor_mat m1 m2
[PROOF STEP]
apply (rule eq_matI, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat (a \<cdot>\<^sub>m m1) m2 $$ (i, j) = a * tensor_mat m1 m2 $$ (i, j)
[PROOF STEP]
unfolding tensor_mat_eval
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> (a \<cdot>\<^sub>m m1) $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j) = a * (m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j))
[PROOF STEP]
using assms comm_semiring_class.distrib
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
(?a + ?b) * ?c = ?a * ?c + ?b * ?c

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> (a \<cdot>\<^sub>m m1) $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j) = a * (m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j))
[PROOF STEP]
by force


[STATEMENT]
lemma tensor_mat_scale2:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d2 d2"
  shows "tensor_mat m1 (a \<cdot>\<^sub>m m2) = a \<cdot>\<^sub>m tensor_mat m1 m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat m1 (a \<cdot>\<^sub>m m2) = a \<cdot>\<^sub>m tensor_mat m1 m2
[PROOF STEP]
apply (rule eq_matI, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> tensor_mat m1 (a \<cdot>\<^sub>m m2) $$ (i, j) = a * tensor_mat m1 m2 $$ (i, j)
[PROOF STEP]
unfolding tensor_mat_eval
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> m1 $$ (encode1 i, encode1 j) * (a \<cdot>\<^sub>m m2) $$ (encode2 i, encode2 j) = a * (m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j))
[PROOF STEP]
using assms comm_semiring_class.distrib
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
(?a + ?b) * ?c = ?a * ?c + ?b * ?c

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d\<rbrakk> \<Longrightarrow> m1 $$ (encode1 i, encode1 j) * (a \<cdot>\<^sub>m m2) $$ (encode2 i, encode2 j) = a * (m1 $$ (encode1 i, encode1 j) * m2 $$ (encode2 i, encode2 j))
[PROOF STEP]
by force


[STATEMENT]
lemma tensor_mat_trace:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d2 d2"
  shows "trace (tensor_mat m1 m2) = trace m1 * trace m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (tensor_mat m1 m2) = trace m1 * trace m2
[PROOF STEP]
apply (auto simp add: tensor_mat_carrier trace_def tensor_mat_eval)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<d. m1 $$ (encode1 i, encode1 i) * m2 $$ (encode2 i, encode2 i)) = (\<Sum>i = 0..<dim_row m1. m1 $$ (i, i)) * (\<Sum>i = 0..<dim_row m2. m2 $$ (i, i))
[PROOF STEP]
apply (subst Groups_Big.sum_product)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<d. m1 $$ (encode1 i, encode1 i) * m2 $$ (encode2 i, encode2 i)) = (\<Sum>i = 0..<dim_row m1. \<Sum>j = 0..<dim_row m2. m1 $$ (i, i) * m2 $$ (j, j))
[PROOF STEP]
apply (subst sum_encode[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<d1. \<Sum>j = 0..<d2. m1 $$ (i, i) * m2 $$ (j, j)) = (\<Sum>i = 0..<dim_row m1. \<Sum>j = 0..<dim_row m2. m1 $$ (i, i) * m2 $$ (j, j))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2

goal (1 subgoal):
 1. (\<Sum>i = 0..<d1. \<Sum>j = 0..<d2. m1 $$ (i, i) * m2 $$ (j, j)) = (\<Sum>i = 0..<dim_row m1. \<Sum>j = 0..<dim_row m2. m1 $$ (i, i) * m2 $$ (j, j))
[PROOF STEP]
by auto


[STATEMENT]
lemma tensor_mat_id:
  "tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) = 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) = 1\<^sub>m d
[PROOF STEP]
proof (rule eq_matI, auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>j. j < d \<Longrightarrow> tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) $$ (j, j) = (1::'a)
 2. \<And>i j. \<lbrakk>i < d; j < d; i \<noteq> j\<rbrakk> \<Longrightarrow> tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) $$ (i, j) = (0::'a)
[PROOF STEP]
show "tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) $$ (i, i) = 1" if "i < d" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) $$ (i, i) = (1::'b)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i < d

goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) $$ (i, i) = (1::'b)
[PROOF STEP]
by (simp add: tensor_mat_eval)
[PROOF STATE]
proof (state)
this:
?i3 < d \<Longrightarrow> tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) $$ (?i3, ?i3) = (1::?'b4)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d; i \<noteq> j\<rbrakk> \<Longrightarrow> tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) $$ (i, j) = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < d; j < d; i \<noteq> j\<rbrakk> \<Longrightarrow> tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) $$ (i, j) = (0::'a)
[PROOF STEP]
show "tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) $$ (i, j) = 0" if "i < d" "j < d" "i \<noteq> j" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) $$ (i, j) = (0::'b)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i < d
j < d
i \<noteq> j

goal (1 subgoal):
 1. tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) $$ (i, j) = (0::'b)
[PROOF STEP]
apply (simp add: tensor_mat_eval)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < d; j < d; i \<noteq> j\<rbrakk> \<Longrightarrow> encode1 i = encode1 j \<longrightarrow> encode2 i \<noteq> encode2 j
[PROOF STEP]
by (metis encode12_inv)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i3 < d; ?j3 < d; ?i3 \<noteq> ?j3\<rbrakk> \<Longrightarrow> tensor_mat (1\<^sub>m d1) (1\<^sub>m d2) $$ (?i3, ?j3) = (0::?'b4)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tensor_mat_mult_vec:
  assumes "m1 \<in> carrier_mat d1 d1"
    and "m2 \<in> carrier_mat d2 d2"
    and "v1 \<in> carrier_vec d1"
    and "v2 \<in> carrier_vec d2"
  shows "tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) = tensor_mat m1 m2 *\<^sub>v tensor_vec v1 v2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) = tensor_mat m1 m2 *\<^sub>v tensor_vec v1 v2
[PROOF STEP]
proof (rule eq_vecI, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2
[PROOF STEP]
fix i j :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2
[PROOF STEP]
assume i: "i < d"
[PROOF STATE]
proof (state)
this:
i < d

goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2
[PROOF STEP]
let ?i1 = "encode1 i" and ?i2 = "encode2 i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2
[PROOF STEP]
have "tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = (m1 *\<^sub>v v1) $ ?i1 * (m2 *\<^sub>v v2) $ ?i2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = (m1 *\<^sub>v v1) $ encode1 i * (m2 *\<^sub>v v2) $ encode2 i
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < d

goal (1 subgoal):
 1. tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = (m1 *\<^sub>v v1) $ encode1 i * (m2 *\<^sub>v v2) $ encode2 i
[PROOF STEP]
by (simp add: tensor_vec_eval)
[PROOF STATE]
proof (state)
this:
tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = (m1 *\<^sub>v v1) $ encode1 i * (m2 *\<^sub>v v2) $ encode2 i

goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = (m1 *\<^sub>v v1) $ encode1 i * (m2 *\<^sub>v v2) $ encode2 i

goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2
[PROOF STEP]
have "\<dots> = (row m1 ?i1 \<bullet> v1) * (row m2 ?i2 \<bullet> v2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (m1 *\<^sub>v v1) $ encode1 i * (m2 *\<^sub>v v2) $ encode2 i = row m1 (encode1 i) \<bullet> v1 * (row m2 (encode2 i) \<bullet> v2)
[PROOF STEP]
using assms i
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
v1 \<in> carrier_vec d1
v2 \<in> carrier_vec d2
i < d

goal (1 subgoal):
 1. (m1 *\<^sub>v v1) $ encode1 i * (m2 *\<^sub>v v2) $ encode2 i = row m1 (encode1 i) \<bullet> v1 * (row m2 (encode2 i) \<bullet> v2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(m1 *\<^sub>v v1) $ encode1 i * (m2 *\<^sub>v v2) $ encode2 i = row m1 (encode1 i) \<bullet> v1 * (row m2 (encode2 i) \<bullet> v2)

goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(m1 *\<^sub>v v1) $ encode1 i * (m2 *\<^sub>v v2) $ encode2 i = row m1 (encode1 i) \<bullet> v1 * (row m2 (encode2 i) \<bullet> v2)

goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2
[PROOF STEP]
have "\<dots> = (\<Sum>i = 0..<d1. m1 $$ (?i1, i) * v1 $ i) * (\<Sum>j = 0..<d2. m2 $$ (?i2, j) * v2 $ j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row m1 (encode1 i) \<bullet> v1 * (row m2 (encode2 i) \<bullet> v2) = (\<Sum>ia = 0..<d1. m1 $$ (encode1 i, ia) * v1 $ ia) * (\<Sum>j = 0..<d2. m2 $$ (encode2 i, j) * v2 $ j)
[PROOF STEP]
using assms i
[PROOF STATE]
proof (prove)
using this:
m1 \<in> carrier_mat d1 d1
m2 \<in> carrier_mat d2 d2
v1 \<in> carrier_vec d1
v2 \<in> carrier_vec d2
i < d

goal (1 subgoal):
 1. row m1 (encode1 i) \<bullet> v1 * (row m2 (encode2 i) \<bullet> v2) = (\<Sum>ia = 0..<d1. m1 $$ (encode1 i, ia) * v1 $ ia) * (\<Sum>j = 0..<d2. m2 $$ (encode2 i, j) * v2 $ j)
[PROOF STEP]
by (simp add: scalar_prod_def)
[PROOF STATE]
proof (state)
this:
row m1 (encode1 i) \<bullet> v1 * (row m2 (encode2 i) \<bullet> v2) = (\<Sum>ia = 0..<d1. m1 $$ (encode1 i, ia) * v1 $ ia) * (\<Sum>j = 0..<d2. m2 $$ (encode2 i, j) * v2 $ j)

goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
row m1 (encode1 i) \<bullet> v1 * (row m2 (encode2 i) \<bullet> v2) = (\<Sum>ia = 0..<d1. m1 $$ (encode1 i, ia) * v1 $ ia) * (\<Sum>j = 0..<d2. m2 $$ (encode2 i, j) * v2 $ j)

goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2
[PROOF STEP]
have "\<dots> = (\<Sum>i = 0..<d1. \<Sum>j = 0..<d2. (m1 $$ (?i1, i) * v1 $ i) * (m2 $$ (?i2, j) * v2 $ j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<d1. m1 $$ (encode1 i, ia) * v1 $ ia) * (\<Sum>j = 0..<d2. m2 $$ (encode2 i, j) * v2 $ j) = (\<Sum>ia = 0..<d1. \<Sum>j = 0..<d2. m1 $$ (encode1 i, ia) * v1 $ ia * (m2 $$ (encode2 i, j) * v2 $ j))
[PROOF STEP]
by (rule Groups_Big.sum_product)
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<d1. m1 $$ (encode1 i, ia) * v1 $ ia) * (\<Sum>j = 0..<d2. m2 $$ (encode2 i, j) * v2 $ j) = (\<Sum>ia = 0..<d1. \<Sum>j = 0..<d2. m1 $$ (encode1 i, ia) * v1 $ ia * (m2 $$ (encode2 i, j) * v2 $ j))

goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<d1. m1 $$ (encode1 i, ia) * v1 $ ia) * (\<Sum>j = 0..<d2. m2 $$ (encode2 i, j) * v2 $ j) = (\<Sum>ia = 0..<d1. \<Sum>j = 0..<d2. m1 $$ (encode1 i, ia) * v1 $ ia * (m2 $$ (encode2 i, j) * v2 $ j))

goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2
[PROOF STEP]
have "\<dots> = (\<Sum>i = 0..<d. (m1 $$ (?i1, encode1 i) * v1 $ (encode1 i)) * (m2 $$ (?i2, encode2 i) * v2 $ (encode2 i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<d1. \<Sum>j = 0..<d2. m1 $$ (encode1 i, ia) * v1 $ ia * (m2 $$ (encode2 i, j) * v2 $ j)) = (\<Sum>ia = 0..<d. m1 $$ (encode1 i, encode1 ia) * v1 $ encode1 ia * (m2 $$ (encode2 i, encode2 ia) * v2 $ encode2 ia))
[PROOF STEP]
by (rule sum_encode)
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<d1. \<Sum>j = 0..<d2. m1 $$ (encode1 i, ia) * v1 $ ia * (m2 $$ (encode2 i, j) * v2 $ j)) = (\<Sum>ia = 0..<d. m1 $$ (encode1 i, encode1 ia) * v1 $ encode1 ia * (m2 $$ (encode2 i, encode2 ia) * v2 $ encode2 ia))

goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<d1. \<Sum>j = 0..<d2. m1 $$ (encode1 i, ia) * v1 $ ia * (m2 $$ (encode2 i, j) * v2 $ j)) = (\<Sum>ia = 0..<d. m1 $$ (encode1 i, encode1 ia) * v1 $ encode1 ia * (m2 $$ (encode2 i, encode2 ia) * v2 $ encode2 ia))

goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2
[PROOF STEP]
have "\<dots> = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<d. m1 $$ (encode1 i, encode1 ia) * v1 $ encode1 ia * (m2 $$ (encode2 i, encode2 ia) * v2 $ encode2 ia)) = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2
[PROOF STEP]
apply (simp add: scalar_prod_def tensor_mat_eval tensor_vec_eval i)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<d. m1 $$ (encode1 i, encode1 ia) * v1 $ encode1 ia * (m2 $$ (encode2 i, encode2 ia) * v2 $ encode2 ia)) = (\<Sum>ia = 0..<d. m1 $$ (encode1 i, encode1 ia) * m2 $$ (encode2 i, encode2 ia) * (v1 $ encode1 ia * v2 $ encode2 ia))
[PROOF STEP]
by (rule sum.cong, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>ia = 0..<d. m1 $$ (encode1 i, encode1 ia) * v1 $ encode1 ia * (m2 $$ (encode2 i, encode2 ia) * v2 $ encode2 ia)) = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2

goal (1 subgoal):
 1. \<And>i. i < d \<Longrightarrow> tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2
[PROOF STEP]
show "tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2"
[PROOF STATE]
proof (prove)
using this:
tensor_vec (m1 *\<^sub>v v1) (m2 *\<^sub>v v2) $ i = row (tensor_mat m1 m2) i \<bullet> tensor_vec v1 v2

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

goal:
No subgoals!
[PROOF STEP]
qed