[STATEMENT]
lemma tensor_from_vec_simp[simp]: "tensor_from_vec (dims A) (vec A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_from_vec (dims A) (vec A) = A
[PROOF STEP]
by (simp add: Rep_tensor_inverse Tensor.vec_def dims_def tensor_from_vec_def)


[STATEMENT]
lemma length_vec: "length (vec A) = prod_list (dims A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (vec A) = prod_list (dims A)
[PROOF STEP]
by (metis (mono_tags, lifting) Rep_tensor Tensor.vec_def dims_def mem_Collect_eq)


[STATEMENT]
lemma tensor_eqI[intro]:
assumes "dims A = dims B" and "vec A = vec B"
shows "A=B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = B
[PROOF STEP]
by (metis assms tensor_from_vec_simp)


[STATEMENT]
lemma valid_index_length: "is \<lhd> ds \<Longrightarrow> length is = length ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is \<lhd> ds \<Longrightarrow> length is = length ds
[PROOF STEP]
by (induction rule:valid_index.induct; auto)


[STATEMENT]
lemma valid_index_lt: "is \<lhd> ds \<Longrightarrow> m<length ds \<Longrightarrow> is!m < ds!m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is \<lhd> ds; m < length ds\<rbrakk> \<Longrightarrow> is ! m < ds ! m
[PROOF STEP]
proof (induction arbitrary:m rule:valid_index.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m. m < length [] \<Longrightarrow> [] ! m < [] ! m
 2. \<And>is ds i d m. \<lbrakk>is \<lhd> ds; \<And>m. m < length ds \<Longrightarrow> is ! m < ds ! m; i < d; m < length (d # ds)\<rbrakk> \<Longrightarrow> (i # is) ! m < (d # ds) ! m
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
m < length []

goal (2 subgoals):
 1. \<And>m. m < length [] \<Longrightarrow> [] ! m < [] ! m
 2. \<And>is ds i d m. \<lbrakk>is \<lhd> ds; \<And>m. m < length ds \<Longrightarrow> is ! m < ds ! m; i < d; m < length (d # ds)\<rbrakk> \<Longrightarrow> (i # is) ! m < (d # ds) ! m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m < length []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
m < length []

goal (1 subgoal):
 1. [] ! m < [] ! m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[] ! m < [] ! m

goal (1 subgoal):
 1. \<And>is ds i d m. \<lbrakk>is \<lhd> ds; \<And>m. m < length ds \<Longrightarrow> is ! m < ds ! m; i < d; m < length (d # ds)\<rbrakk> \<Longrightarrow> (i # is) ! m < (d # ds) ! m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>is ds i d m. \<lbrakk>is \<lhd> ds; \<And>m. m < length ds \<Longrightarrow> is ! m < ds ! m; i < d; m < length (d # ds)\<rbrakk> \<Longrightarrow> (i # is) ! m < (d # ds) ! m
[PROOF STEP]
case Cons
[PROOF STATE]
proof (state)
this:
is_ \<lhd> ds_
i_ < d_
?m < length ds_ \<Longrightarrow> is_ ! ?m < ds_ ! ?m
m < length (d_ # ds_)

goal (1 subgoal):
 1. \<And>is ds i d m. \<lbrakk>is \<lhd> ds; \<And>m. m < length ds \<Longrightarrow> is ! m < ds ! m; i < d; m < length (d # ds)\<rbrakk> \<Longrightarrow> (i # is) ! m < (d # ds) ! m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_ \<lhd> ds_
i_ < d_
?m < length ds_ \<Longrightarrow> is_ ! ?m < ds_ ! ?m
m < length (d_ # ds_)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_ \<lhd> ds_
i_ < d_
?m < length ds_ \<Longrightarrow> is_ ! ?m < ds_ ! ?m
m < length (d_ # ds_)

goal (1 subgoal):
 1. (i_ # is_) ! m < (d_ # ds_) ! m
[PROOF STEP]
by (metis gr0_conv_Suc length_Cons linorder_neqE_nat not_less_eq nth_Cons' nth_Cons_Suc)
[PROOF STATE]
proof (state)
this:
(i_ # is_) ! m < (d_ # ds_) ! m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_indexI:
assumes "length is = length ds" and "\<And>m. m<length ds \<Longrightarrow> is!m < ds!m"
shows "is \<lhd> ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is \<lhd> ds
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length is = length ds
?m < length ds \<Longrightarrow> is ! ?m < ds ! ?m

goal (1 subgoal):
 1. is \<lhd> ds
[PROOF STEP]
proof (induction "is" arbitrary:ds)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ds. \<lbrakk>length [] = length ds; \<And>m. m < length ds \<Longrightarrow> [] ! m < ds ! m\<rbrakk> \<Longrightarrow> [] \<lhd> ds
 2. \<And>a is ds. \<lbrakk>\<And>ds. \<lbrakk>length is = length ds; \<And>m. m < length ds \<Longrightarrow> is ! m < ds ! m\<rbrakk> \<Longrightarrow> is \<lhd> ds; length (a # is) = length ds; \<And>m. m < length ds \<Longrightarrow> (a # is) ! m < ds ! m\<rbrakk> \<Longrightarrow> a # is \<lhd> ds
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
length [] = length ds
?m < length ds \<Longrightarrow> [] ! ?m < ds ! ?m

goal (2 subgoals):
 1. \<And>ds. \<lbrakk>length [] = length ds; \<And>m. m < length ds \<Longrightarrow> [] ! m < ds ! m\<rbrakk> \<Longrightarrow> [] \<lhd> ds
 2. \<And>a is ds. \<lbrakk>\<And>ds. \<lbrakk>length is = length ds; \<And>m. m < length ds \<Longrightarrow> is ! m < ds ! m\<rbrakk> \<Longrightarrow> is \<lhd> ds; length (a # is) = length ds; \<And>m. m < length ds \<Longrightarrow> (a # is) ! m < ds ! m\<rbrakk> \<Longrightarrow> a # is \<lhd> ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length [] = length ds
?m < length ds \<Longrightarrow> [] ! ?m < ds ! ?m
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length [] = length ds
?m < length ds \<Longrightarrow> [] ! ?m < ds ! ?m

goal (1 subgoal):
 1. [] \<lhd> ds
[PROOF STEP]
by (metis length_0_conv valid_index.simps)
[PROOF STATE]
proof (state)
this:
[] \<lhd> ds

goal (1 subgoal):
 1. \<And>a is ds. \<lbrakk>\<And>ds. \<lbrakk>length is = length ds; \<And>m. m < length ds \<Longrightarrow> is ! m < ds ! m\<rbrakk> \<Longrightarrow> is \<lhd> ds; length (a # is) = length ds; \<And>m. m < length ds \<Longrightarrow> (a # is) ! m < ds ! m\<rbrakk> \<Longrightarrow> a # is \<lhd> ds
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a is ds. \<lbrakk>\<And>ds. \<lbrakk>length is = length ds; \<And>m. m < length ds \<Longrightarrow> is ! m < ds ! m\<rbrakk> \<Longrightarrow> is \<lhd> ds; length (a # is) = length ds; \<And>m. m < length ds \<Longrightarrow> (a # is) ! m < ds ! m\<rbrakk> \<Longrightarrow> a # is \<lhd> ds
[PROOF STEP]
case (Cons a "is" ds)
[PROOF STATE]
proof (state)
this:
\<lbrakk>length is = length ?ds; \<And>m. m < length ?ds \<Longrightarrow> is ! m < ?ds ! m\<rbrakk> \<Longrightarrow> is \<lhd> ?ds
length (a # is) = length ds
?m < length ds \<Longrightarrow> (a # is) ! ?m < ds ! ?m

goal (1 subgoal):
 1. \<And>a is ds. \<lbrakk>\<And>ds. \<lbrakk>length is = length ds; \<And>m. m < length ds \<Longrightarrow> is ! m < ds ! m\<rbrakk> \<Longrightarrow> is \<lhd> ds; length (a # is) = length ds; \<And>m. m < length ds \<Longrightarrow> (a # is) ! m < ds ! m\<rbrakk> \<Longrightarrow> a # is \<lhd> ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>length is = length ?ds; \<And>m. m < length ?ds \<Longrightarrow> is ! m < ?ds ! m\<rbrakk> \<Longrightarrow> is \<lhd> ?ds
length (a # is) = length ds
?m < length ds \<Longrightarrow> (a # is) ! ?m < ds ! ?m
[PROOF STEP]
obtain d ds' where "ds = d # ds'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length is = length ?ds; \<And>m. m < length ?ds \<Longrightarrow> is ! m < ?ds ! m\<rbrakk> \<Longrightarrow> is \<lhd> ?ds
length (a # is) = length ds
?m < length ds \<Longrightarrow> (a # is) ! ?m < ds ! ?m

goal (1 subgoal):
 1. (\<And>d ds'. ds = d # ds' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis length_Suc_conv)
[PROOF STATE]
proof (state)
this:
ds = d # ds'

goal (1 subgoal):
 1. \<And>a is ds. \<lbrakk>\<And>ds. \<lbrakk>length is = length ds; \<And>m. m < length ds \<Longrightarrow> is ! m < ds ! m\<rbrakk> \<Longrightarrow> is \<lhd> ds; length (a # is) = length ds; \<And>m. m < length ds \<Longrightarrow> (a # is) ! m < ds ! m\<rbrakk> \<Longrightarrow> a # is \<lhd> ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ds = d # ds'
[PROOF STEP]
have "is \<lhd> ds'"
[PROOF STATE]
proof (prove)
using this:
ds = d # ds'

goal (1 subgoal):
 1. is \<lhd> ds'
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
ds = d # ds'
\<lbrakk>length is = length ?ds; \<And>m. m < length ?ds \<Longrightarrow> is ! m < ?ds ! m\<rbrakk> \<Longrightarrow> is \<lhd> ?ds
length (a # is) = length ds
?m < length ds \<Longrightarrow> (a # is) ! ?m < ds ! ?m

goal (1 subgoal):
 1. is \<lhd> ds'
[PROOF STEP]
by (metis length_Cons less_irrefl linorder_neqE_nat not_less_eq nth_Cons_Suc)
[PROOF STATE]
proof (state)
this:
is \<lhd> ds'

goal (1 subgoal):
 1. \<And>a is ds. \<lbrakk>\<And>ds. \<lbrakk>length is = length ds; \<And>m. m < length ds \<Longrightarrow> is ! m < ds ! m\<rbrakk> \<Longrightarrow> is \<lhd> ds; length (a # is) = length ds; \<And>m. m < length ds \<Longrightarrow> (a # is) ! m < ds ! m\<rbrakk> \<Longrightarrow> a # is \<lhd> ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is \<lhd> ds'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is \<lhd> ds'

goal (1 subgoal):
 1. a # is \<lhd> ds
[PROOF STEP]
using Cons.prems(2) \<open>ds = d # ds'\<close> valid_index.Cons
[PROOF STATE]
proof (prove)
using this:
is \<lhd> ds'
?m < length ds \<Longrightarrow> (a # is) ! ?m < ds ! ?m
ds = d # ds'
\<lbrakk>?is \<lhd> ?ds; ?i < ?d\<rbrakk> \<Longrightarrow> ?i # ?is \<lhd> ?d # ?ds

goal (1 subgoal):
 1. a # is \<lhd> ds
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
a # is \<lhd> ds

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_index_append:
assumes is1_valid:"is1 \<lhd> ds1" and is2_valid:"is2 \<lhd> ds2"
shows "is1 @ is2 \<lhd> ds1 @ ds2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is1 @ is2 \<lhd> ds1 @ ds2
[PROOF STEP]
apply (rule valid_indexI[of "is1 @ is2" "ds1 @ ds2"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (is1 @ is2) = length (ds1 @ ds2)
 2. \<And>m. m < length (ds1 @ ds2) \<Longrightarrow> (is1 @ is2) ! m < (ds1 @ ds2) ! m
[PROOF STEP]
unfolding nth_append
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (is1 @ is2) = length (ds1 @ ds2)
 2. \<And>m. m < length (ds1 @ ds2) \<Longrightarrow> (if m < length is1 then is1 ! m else is2 ! (m - length is1)) < (if m < length ds1 then ds1 ! m else ds2 ! (m - length ds1))
[PROOF STEP]
using valid_index_lt[OF is2_valid] valid_index_lt[OF is1_valid] valid_index_length[OF is1_valid] valid_index_length[OF is2_valid] length_append
[PROOF STATE]
proof (prove)
using this:
?m < length ds2 \<Longrightarrow> is2 ! ?m < ds2 ! ?m
?m < length ds1 \<Longrightarrow> is1 ! ?m < ds1 ! ?m
length is1 = length ds1
length is2 = length ds2
length (?xs @ ?ys) = length ?xs + length ?ys

goal (2 subgoals):
 1. length (is1 @ is2) = length (ds1 @ ds2)
 2. \<And>m. m < length (ds1 @ ds2) \<Longrightarrow> (if m < length is1 then is1 ! m else is2 ! (m - length is1)) < (if m < length ds1 then ds1 ! m else ds2 ! (m - length ds1))
[PROOF STEP]
by (auto simp add: \<open>length is1 = length ds1\<close>)


[STATEMENT]
lemma valid_index_list_all2_iff: "is \<lhd> ds \<longleftrightarrow> list_all2 (<) is ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is \<lhd> ds) = list_all2 (<) is ds
[PROOF STEP]
by (metis list_all2_conv_all_nth list_all2_nthD valid_indexI valid_index_length valid_index_lt)


[STATEMENT]
lemma concat_parts_leq:
assumes "a * d \<le> length v"
shows "concat (map (fixed_length_sublist v d) [0..<a]) = take (a*d) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a * d \<le> length v

goal (1 subgoal):
 1. concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v
[PROOF STEP]
proof (induction a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 * d \<le> length v \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<0]) = take (0 * d) v
 2. \<And>a. \<lbrakk>a * d \<le> length v \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v; Suc a * d \<le> length v\<rbrakk> \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<Suc a]) = take (Suc a * d) v
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 * d \<le> length v

goal (2 subgoals):
 1. 0 * d \<le> length v \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<0]) = take (0 * d) v
 2. \<And>a. \<lbrakk>a * d \<le> length v \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v; Suc a * d \<le> length v\<rbrakk> \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<Suc a]) = take (Suc a * d) v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 * d \<le> length v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 * d \<le> length v

goal (1 subgoal):
 1. concat (map (fixed_length_sublist v d) [0..<0]) = take (0 * d) v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
concat (map (fixed_length_sublist v d) [0..<0]) = take (0 * d) v

goal (1 subgoal):
 1. \<And>a. \<lbrakk>a * d \<le> length v \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v; Suc a * d \<le> length v\<rbrakk> \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<Suc a]) = take (Suc a * d) v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>a * d \<le> length v \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v; Suc a * d \<le> length v\<rbrakk> \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<Suc a]) = take (Suc a * d) v
[PROOF STEP]
case (Suc a)
[PROOF STATE]
proof (state)
this:
a * d \<le> length v \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v
Suc a * d \<le> length v

goal (1 subgoal):
 1. \<And>a. \<lbrakk>a * d \<le> length v \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v; Suc a * d \<le> length v\<rbrakk> \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<Suc a]) = take (Suc a * d) v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a * d \<le> length v \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v
Suc a * d \<le> length v
[PROOF STEP]
have "concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v"
[PROOF STATE]
proof (prove)
using this:
a * d \<le> length v \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v
Suc a * d \<le> length v

goal (1 subgoal):
 1. concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v

goal (1 subgoal):
 1. \<And>a. \<lbrakk>a * d \<le> length v \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v; Suc a * d \<le> length v\<rbrakk> \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<Suc a]) = take (Suc a * d) v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v
[PROOF STEP]
have "concat (map (fixed_length_sublist v d) [0..<Suc a]) =
        take (a * d) v @ fixed_length_sublist v d a"
[PROOF STATE]
proof (prove)
using this:
concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v

goal (1 subgoal):
 1. concat (map (fixed_length_sublist v d) [0..<Suc a]) = take (a * d) v @ fixed_length_sublist v d a
[PROOF STEP]
using fixed_length_sublist_def
[PROOF STATE]
proof (prove)
using this:
concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v
fixed_length_sublist ?xs ?l ?i = take ?l (drop (?l * ?i) ?xs)

goal (1 subgoal):
 1. concat (map (fixed_length_sublist v d) [0..<Suc a]) = take (a * d) v @ fixed_length_sublist v d a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
concat (map (fixed_length_sublist v d) [0..<Suc a]) = take (a * d) v @ fixed_length_sublist v d a

goal (1 subgoal):
 1. \<And>a. \<lbrakk>a * d \<le> length v \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v; Suc a * d \<le> length v\<rbrakk> \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<Suc a]) = take (Suc a * d) v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
concat (map (fixed_length_sublist v d) [0..<Suc a]) = take (a * d) v @ fixed_length_sublist v d a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
concat (map (fixed_length_sublist v d) [0..<Suc a]) = take (a * d) v @ fixed_length_sublist v d a

goal (1 subgoal):
 1. concat (map (fixed_length_sublist v d) [0..<Suc a]) = take (Suc a * d) v
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
concat (map (fixed_length_sublist v d) [0..<Suc a]) = take (a * d) v @ fixed_length_sublist v d a
a * d \<le> length v \<Longrightarrow> concat (map (fixed_length_sublist v d) [0..<a]) = take (a * d) v
Suc a * d \<le> length v

goal (1 subgoal):
 1. concat (map (fixed_length_sublist v d) [0..<Suc a]) = take (Suc a * d) v
[PROOF STEP]
by (metis add.commute mult.commute mult_Suc take_add fixed_length_sublist_def)
[PROOF STATE]
proof (state)
this:
concat (map (fixed_length_sublist v d) [0..<Suc a]) = take (Suc a * d) v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma concat_parts_eq:
assumes "a * d = length v"
shows "concat (map (fixed_length_sublist v d) [0..<a]) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concat (map (fixed_length_sublist v d) [0..<a]) = v
[PROOF STEP]
by (simp add: concat_parts_leq assms)


[STATEMENT]
lemma tensor_lookup_base:
assumes "length v = prod_list ds"
and "\<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds v is = e is"
shows "tensor_vec_from_lookup ds e = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_vec_from_lookup ds e = v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length v = prod_list ds
?is \<lhd> ds \<Longrightarrow> lookup_base ds v ?is = e ?is

goal (1 subgoal):
 1. tensor_vec_from_lookup ds e = v
[PROOF STEP]
proof (induction ds arbitrary:v e)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v e. \<lbrakk>length v = prod_list []; \<And>is. is \<lhd> [] \<Longrightarrow> lookup_base [] v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup [] e = v
 2. \<And>a ds v e. \<lbrakk>\<And>v e. \<lbrakk>length v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds e = v; length v = prod_list (a # ds); \<And>is. is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup (a # ds) e = v
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
length v = prod_list []
?is \<lhd> [] \<Longrightarrow> lookup_base [] v ?is = e ?is

goal (2 subgoals):
 1. \<And>v e. \<lbrakk>length v = prod_list []; \<And>is. is \<lhd> [] \<Longrightarrow> lookup_base [] v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup [] e = v
 2. \<And>a ds v e. \<lbrakk>\<And>v e. \<lbrakk>length v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds e = v; length v = prod_list (a # ds); \<And>is. is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup (a # ds) e = v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length v = prod_list []
?is \<lhd> [] \<Longrightarrow> lookup_base [] v ?is = e ?is
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length v = prod_list []
?is \<lhd> [] \<Longrightarrow> lookup_base [] v ?is = e ?is

goal (1 subgoal):
 1. tensor_vec_from_lookup [] e = v
[PROOF STEP]
unfolding tensor_vec_from_lookup.simps
[PROOF STATE]
proof (prove)
using this:
length v = prod_list []
?is \<lhd> [] \<Longrightarrow> lookup_base [] v ?is = e ?is

goal (1 subgoal):
 1. [e []] = v
[PROOF STEP]
by (metis One_nat_def Tensor.lookup_base_Nil length_0_conv length_Suc_conv list.sel(1) prod_list.Nil valid_index.Nil)
[PROOF STATE]
proof (state)
this:
tensor_vec_from_lookup [] e = v

goal (1 subgoal):
 1. \<And>a ds v e. \<lbrakk>\<And>v e. \<lbrakk>length v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds e = v; length v = prod_list (a # ds); \<And>is. is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup (a # ds) e = v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ds v e. \<lbrakk>\<And>v e. \<lbrakk>length v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds e = v; length v = prod_list (a # ds); \<And>is. is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup (a # ds) e = v
[PROOF STEP]
case (Cons a ds)
[PROOF STATE]
proof (state)
this:
\<lbrakk>length ?v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds ?v is = ?e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds ?e = ?v
length v = prod_list (a # ds)
?is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v ?is = e ?is

goal (1 subgoal):
 1. \<And>a ds v e. \<lbrakk>\<And>v e. \<lbrakk>length v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds e = v; length v = prod_list (a # ds); \<And>is. is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup (a # ds) e = v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>length ?v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds ?v is = ?e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds ?e = ?v
length v = prod_list (a # ds)
?is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v ?is = e ?is
[PROOF STEP]
have "a * prod_list ds = length v"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length ?v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds ?v is = ?e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds ?e = ?v
length v = prod_list (a # ds)
?is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v ?is = e ?is

goal (1 subgoal):
 1. a * prod_list ds = length v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a * prod_list ds = length v

goal (1 subgoal):
 1. \<And>a ds v e. \<lbrakk>\<And>v e. \<lbrakk>length v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds e = v; length v = prod_list (a # ds); \<And>is. is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup (a # ds) e = v
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
a * prod_list ds = length v

goal (1 subgoal):
 1. \<And>a ds v e. \<lbrakk>\<And>v e. \<lbrakk>length v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds e = v; length v = prod_list (a # ds); \<And>is. is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup (a # ds) e = v
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ds v e. \<lbrakk>\<And>v e. \<lbrakk>length v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds e = v; length v = prod_list (a # ds); \<And>is. is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup (a # ds) e = v
[PROOF STEP]
assume "i<a"
[PROOF STATE]
proof (state)
this:
i < a

goal (1 subgoal):
 1. \<And>a ds v e. \<lbrakk>\<And>v e. \<lbrakk>length v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds e = v; length v = prod_list (a # ds); \<And>is. is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup (a # ds) e = v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < a
[PROOF STEP]
have "prod_list ds * (i+1) \<le> length v"
[PROOF STATE]
proof (prove)
using this:
i < a

goal (1 subgoal):
 1. prod_list ds * (i + 1) \<le> length v
[PROOF STEP]
using \<open>a * prod_list ds = length v\<close>
[PROOF STATE]
proof (prove)
using this:
i < a
a * prod_list ds = length v

goal (1 subgoal):
 1. prod_list ds * (i + 1) \<le> length v
[PROOF STEP]
using discrete mult.commute mult_le_mono1
[PROOF STATE]
proof (prove)
using this:
i < a
a * prod_list ds = length v
(?a < ?b) = (?a + (1::?'a) \<le> ?b)
?a * ?b = ?b * ?a
?i \<le> ?j \<Longrightarrow> ?i * ?k \<le> ?j * ?k

goal (1 subgoal):
 1. prod_list ds * (i + 1) \<le> length v
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
prod_list ds * (i + 1) \<le> length v

goal (1 subgoal):
 1. \<And>a ds v e. \<lbrakk>\<And>v e. \<lbrakk>length v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds e = v; length v = prod_list (a # ds); \<And>is. is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup (a # ds) e = v
[PROOF STEP]
have "\<And>is'. is' \<lhd> ds \<Longrightarrow> e (i # is') = lookup_base ds (fixed_length_sublist v (prod_list ds) i) is'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>is'. is' \<lhd> ds \<Longrightarrow> e (i # is') = lookup_base ds (fixed_length_sublist v (prod_list ds) i) is'
[PROOF STEP]
using \<open>i<a\<close>
[PROOF STATE]
proof (prove)
using this:
i < a

goal (1 subgoal):
 1. \<And>is'. is' \<lhd> ds \<Longrightarrow> e (i # is') = lookup_base ds (fixed_length_sublist v (prod_list ds) i) is'
[PROOF STEP]
by (metis Cons.prems(2) Tensor.lookup_base_Cons valid_index.simps)
[PROOF STATE]
proof (state)
this:
?is' \<lhd> ds \<Longrightarrow> e (i # ?is') = lookup_base ds (fixed_length_sublist v (prod_list ds) i) ?is'

goal (1 subgoal):
 1. \<And>a ds v e. \<lbrakk>\<And>v e. \<lbrakk>length v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds e = v; length v = prod_list (a # ds); \<And>is. is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup (a # ds) e = v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?is' \<lhd> ds \<Longrightarrow> e (i # ?is') = lookup_base ds (fixed_length_sublist v (prod_list ds) i) ?is'
[PROOF STEP]
have "tensor_vec_from_lookup ds (\<lambda>is'. e (i # is')) = fixed_length_sublist v (prod_list ds) i"
[PROOF STATE]
proof (prove)
using this:
?is' \<lhd> ds \<Longrightarrow> e (i # ?is') = lookup_base ds (fixed_length_sublist v (prod_list ds) i) ?is'

goal (1 subgoal):
 1. tensor_vec_from_lookup ds (\<lambda>is'. e (i # is')) = fixed_length_sublist v (prod_list ds) i
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
?is' \<lhd> ds \<Longrightarrow> e (i # ?is') = lookup_base ds (fixed_length_sublist v (prod_list ds) i) ?is'
\<lbrakk>length ?v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds ?v is = ?e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds ?e = ?v
length v = prod_list (a # ds)
?is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v ?is = e ?is

goal (1 subgoal):
 1. tensor_vec_from_lookup ds (\<lambda>is'. e (i # is')) = fixed_length_sublist v (prod_list ds) i
[PROOF STEP]
using \<open>prod_list ds * (i + 1) \<le> length v\<close>
[PROOF STATE]
proof (prove)
using this:
?is' \<lhd> ds \<Longrightarrow> e (i # ?is') = lookup_base ds (fixed_length_sublist v (prod_list ds) i) ?is'
\<lbrakk>length ?v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds ?v is = ?e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds ?e = ?v
length v = prod_list (a # ds)
?is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v ?is = e ?is
prod_list ds * (i + 1) \<le> length v

goal (1 subgoal):
 1. tensor_vec_from_lookup ds (\<lambda>is'. e (i # is')) = fixed_length_sublist v (prod_list ds) i
[PROOF STEP]
by (simp add: Cons.IH fixed_length_sublist_def)
[PROOF STATE]
proof (state)
this:
tensor_vec_from_lookup ds (\<lambda>is'. e (i # is')) = fixed_length_sublist v (prod_list ds) i

goal (1 subgoal):
 1. \<And>a ds v e. \<lbrakk>\<And>v e. \<lbrakk>length v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds e = v; length v = prod_list (a # ds); \<And>is. is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup (a # ds) e = v
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i2 < a \<Longrightarrow> tensor_vec_from_lookup ds (\<lambda>is'. e (?i2 # is')) = fixed_length_sublist v (prod_list ds) ?i2

goal (1 subgoal):
 1. \<And>a ds v e. \<lbrakk>\<And>v e. \<lbrakk>length v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds e = v; length v = prod_list (a # ds); \<And>is. is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v is = e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup (a # ds) e = v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i2 < a \<Longrightarrow> tensor_vec_from_lookup ds (\<lambda>is'. e (?i2 # is')) = fixed_length_sublist v (prod_list ds) ?i2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?i2 < a \<Longrightarrow> tensor_vec_from_lookup ds (\<lambda>is'. e (?i2 # is')) = fixed_length_sublist v (prod_list ds) ?i2

goal (1 subgoal):
 1. tensor_vec_from_lookup (a # ds) e = v
[PROOF STEP]
unfolding tensor_vec_from_lookup_Cons lookup_base_Cons
[PROOF STATE]
proof (prove)
using this:
?i2 < a \<Longrightarrow> tensor_vec_from_lookup ds (\<lambda>is'. e (?i2 # is')) = fixed_length_sublist v (prod_list ds) ?i2

goal (1 subgoal):
 1. concat (map (\<lambda>i. tensor_vec_from_lookup ds (\<lambda>is. e (i # is))) [0..<a]) = v
[PROOF STEP]
using   concat_parts_eq[OF \<open>a * prod_list ds = length v\<close>]
     atLeastLessThan_iff map_eq_conv set_upt Cons
[PROOF STATE]
proof (prove)
using this:
?i2 < a \<Longrightarrow> tensor_vec_from_lookup ds (\<lambda>is'. e (?i2 # is')) = fixed_length_sublist v (prod_list ds) ?i2
concat (map (fixed_length_sublist v (prod_list ds)) [0..<a]) = v
(?i \<in> {?l..<?u}) = (?l \<le> ?i \<and> ?i < ?u)
(map ?f ?xs = map ?g ?xs) = (\<forall>x\<in>set ?xs. ?f x = ?g x)
set [?i..<?j] = {?i..<?j}
\<lbrakk>length ?v = prod_list ds; \<And>is. is \<lhd> ds \<Longrightarrow> lookup_base ds ?v is = ?e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ds ?e = ?v
length v = prod_list (a # ds)
?is \<lhd> a # ds \<Longrightarrow> lookup_base (a # ds) v ?is = e ?is

goal (1 subgoal):
 1. concat (map (\<lambda>i. tensor_vec_from_lookup ds (\<lambda>is. e (i # is))) [0..<a]) = v
[PROOF STEP]
by (metis (no_types, lifting))
[PROOF STATE]
proof (state)
this:
tensor_vec_from_lookup (a # ds) e = v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tensor_lookup:
assumes "\<And>is. is \<lhd> dims A \<Longrightarrow> lookup A is = e is"
shows "tensor_from_lookup (dims A) e = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_from_lookup (dims A) e = A
[PROOF STEP]
using tensor_lookup_base lookup_def length_vec tensor_from_lookup_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length ?v = prod_list ?ds; \<And>is. is \<lhd> ?ds \<Longrightarrow> lookup_base ?ds ?v is = ?e is\<rbrakk> \<Longrightarrow> tensor_vec_from_lookup ?ds ?e = ?v
lookup ?A = lookup_base (dims ?A) (vec ?A)
length (vec ?A) = prod_list (dims ?A)
tensor_from_lookup ?ds ?e = tensor_from_vec ?ds (tensor_vec_from_lookup ?ds ?e)

goal (1 subgoal):
 1. tensor_from_lookup (dims A) e = A
[PROOF STEP]
by (metis assms tensor_from_vec_simp)


[STATEMENT]
lemma concat_equal_length:
assumes "\<And>xs. xs\<in>set xss \<Longrightarrow> length xs = l"
shows "length (concat xss) = length xss*l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (concat xss) = length xss * l
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?xs \<in> set xss \<Longrightarrow> length ?xs = l

goal (1 subgoal):
 1. length (concat xss) = length xss * l
[PROOF STEP]
by (induction xss;auto)


[STATEMENT]
lemma concat_equal_length_map:
assumes "\<And>i. i<a \<Longrightarrow> length (f i) = d"
shows "length (concat (map (\<lambda>i. f i) [0..<a])) = a*d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (concat (map f [0..<a])) = a * d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?i < a \<Longrightarrow> length (f ?i) = d

goal (1 subgoal):
 1. length (concat (map f [0..<a])) = a * d
[PROOF STEP]
by (induction a;auto)


[STATEMENT]
lemma concat_parts:
assumes "\<And>xs. xs\<in>set xss \<Longrightarrow> length xs = d" and "i<length xss"
shows "fixed_length_sublist (concat xss) d i = xss ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fixed_length_sublist (concat xss) d i = xss ! i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?xs \<in> set xss \<Longrightarrow> length ?xs = d
i < length xss

goal (1 subgoal):
 1. fixed_length_sublist (concat xss) d i = xss ! i
[PROOF STEP]
proof (induction xss arbitrary:i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>\<And>xs. xs \<in> set [] \<Longrightarrow> length xs = d; i < length []\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat []) d i = [] ! i
 2. \<And>a xss i. \<lbrakk>\<And>i. \<lbrakk>\<And>xs. xs \<in> set xss \<Longrightarrow> length xs = d; i < length xss\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat xss) d i = xss ! i; \<And>xs. xs \<in> set (a # xss) \<Longrightarrow> length xs = d; i < length (a # xss)\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (a # xss)) d i = (a # xss) ! i
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
?xs \<in> set [] \<Longrightarrow> length ?xs = d
i < length []

goal (2 subgoals):
 1. \<And>i. \<lbrakk>\<And>xs. xs \<in> set [] \<Longrightarrow> length xs = d; i < length []\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat []) d i = [] ! i
 2. \<And>a xss i. \<lbrakk>\<And>i. \<lbrakk>\<And>xs. xs \<in> set xss \<Longrightarrow> length xs = d; i < length xss\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat xss) d i = xss ! i; \<And>xs. xs \<in> set (a # xss) \<Longrightarrow> length xs = d; i < length (a # xss)\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (a # xss)) d i = (a # xss) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?xs \<in> set [] \<Longrightarrow> length ?xs = d
i < length []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?xs \<in> set [] \<Longrightarrow> length ?xs = d
i < length []

goal (1 subgoal):
 1. fixed_length_sublist (concat []) d i = [] ! i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fixed_length_sublist (concat []) d i = [] ! i

goal (1 subgoal):
 1. \<And>a xss i. \<lbrakk>\<And>i. \<lbrakk>\<And>xs. xs \<in> set xss \<Longrightarrow> length xs = d; i < length xss\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat xss) d i = xss ! i; \<And>xs. xs \<in> set (a # xss) \<Longrightarrow> length xs = d; i < length (a # xss)\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (a # xss)) d i = (a # xss) ! i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xss i. \<lbrakk>\<And>i. \<lbrakk>\<And>xs. xs \<in> set xss \<Longrightarrow> length xs = d; i < length xss\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat xss) d i = xss ! i; \<And>xs. xs \<in> set (a # xss) \<Longrightarrow> length xs = d; i < length (a # xss)\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (a # xss)) d i = (a # xss) ! i
[PROOF STEP]
case (Cons xs xss)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>xs. xs \<in> set xss \<Longrightarrow> length xs = d; ?i < length xss\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat xss) d ?i = xss ! ?i
?xs \<in> set (xs # xss) \<Longrightarrow> length ?xs = d
i < length (xs # xss)

goal (1 subgoal):
 1. \<And>a xss i. \<lbrakk>\<And>i. \<lbrakk>\<And>xs. xs \<in> set xss \<Longrightarrow> length xs = d; i < length xss\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat xss) d i = xss ! i; \<And>xs. xs \<in> set (a # xss) \<Longrightarrow> length xs = d; i < length (a # xss)\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (a # xss)) d i = (a # xss) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>xs. xs \<in> set xss \<Longrightarrow> length xs = d; ?i < length xss\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat xss) d ?i = xss ! ?i
?xs \<in> set (xs # xss) \<Longrightarrow> length ?xs = d
i < length (xs # xss)
[PROOF STEP]
have "length (concat xss) = length xss * d"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>xs. xs \<in> set xss \<Longrightarrow> length xs = d; ?i < length xss\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat xss) d ?i = xss ! ?i
?xs \<in> set (xs # xss) \<Longrightarrow> length ?xs = d
i < length (xs # xss)

goal (1 subgoal):
 1. length (concat xss) = length xss * d
[PROOF STEP]
by (simp add: Cons.prems(1) concat_equal_length)
[PROOF STATE]
proof (state)
this:
length (concat xss) = length xss * d

goal (1 subgoal):
 1. \<And>a xss i. \<lbrakk>\<And>i. \<lbrakk>\<And>xs. xs \<in> set xss \<Longrightarrow> length xs = d; i < length xss\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat xss) d i = xss ! i; \<And>xs. xs \<in> set (a # xss) \<Longrightarrow> length xs = d; i < length (a # xss)\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (a # xss)) d i = (a # xss) ! i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fixed_length_sublist (concat (xs # xss)) d i = (xs # xss) ! i
[PROOF STEP]
proof (cases i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = 0 \<Longrightarrow> fixed_length_sublist (concat (xs # xss)) d i = (xs # xss) ! i
 2. \<And>nat. i = Suc nat \<Longrightarrow> fixed_length_sublist (concat (xs # xss)) d i = (xs # xss) ! i
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
i = 0

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> fixed_length_sublist (concat (xs # xss)) d i = (xs # xss) ! i
 2. \<And>nat. i = Suc nat \<Longrightarrow> fixed_length_sublist (concat (xs # xss)) d i = (xs # xss) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = 0
[PROOF STEP]
have "fixed_length_sublist (concat (xs # xss)) d i = xs"
[PROOF STATE]
proof (prove)
using this:
i = 0

goal (1 subgoal):
 1. fixed_length_sublist (concat (xs # xss)) d i = xs
[PROOF STEP]
unfolding fixed_length_sublist_def
[PROOF STATE]
proof (prove)
using this:
i = 0

goal (1 subgoal):
 1. take d (drop (d * i) (concat (xs # xss))) = xs
[PROOF STEP]
by (simp add: Cons.prems(1))
[PROOF STATE]
proof (state)
this:
fixed_length_sublist (concat (xs # xss)) d i = xs

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> fixed_length_sublist (concat (xs # xss)) d i = (xs # xss) ! i
 2. \<And>nat. i = Suc nat \<Longrightarrow> fixed_length_sublist (concat (xs # xss)) d i = (xs # xss) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fixed_length_sublist (concat (xs # xss)) d i = xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fixed_length_sublist (concat (xs # xss)) d i = xs

goal (1 subgoal):
 1. fixed_length_sublist (concat (xs # xss)) d i = (xs # xss) ! i
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
fixed_length_sublist (concat (xs # xss)) d i = xs
i = 0

goal (1 subgoal):
 1. fixed_length_sublist (concat (xs # xss)) d i = (xs # xss) ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fixed_length_sublist (concat (xs # xss)) d i = (xs # xss) ! i

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> fixed_length_sublist (concat (xs # xss)) d i = (xs # xss) ! i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> fixed_length_sublist (concat (xs # xss)) d i = (xs # xss) ! i
[PROOF STEP]
case (Suc i')
[PROOF STATE]
proof (state)
this:
i = Suc i'

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> fixed_length_sublist (concat (xs # xss)) d i = (xs # xss) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = Suc i'
[PROOF STEP]
have "fixed_length_sublist (concat xss) d i' = xss ! i'"
[PROOF STATE]
proof (prove)
using this:
i = Suc i'

goal (1 subgoal):
 1. fixed_length_sublist (concat xss) d i' = xss ! i'
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
i = Suc i'
\<lbrakk>\<And>xs. xs \<in> set xss \<Longrightarrow> length xs = d; ?i < length xss\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat xss) d ?i = xss ! ?i
?xs \<in> set (xs # xss) \<Longrightarrow> length ?xs = d
i < length (xs # xss)

goal (1 subgoal):
 1. fixed_length_sublist (concat xss) d i' = xss ! i'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fixed_length_sublist (concat xss) d i' = xss ! i'

goal (1 subgoal):
 1. \<And>nat. i = Suc nat \<Longrightarrow> fixed_length_sublist (concat (xs # xss)) d i = (xs # xss) ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fixed_length_sublist (concat xss) d i' = xss ! i'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fixed_length_sublist (concat xss) d i' = xss ! i'

goal (1 subgoal):
 1. fixed_length_sublist (concat (xs # xss)) d i = (xs # xss) ! i
[PROOF STEP]
unfolding fixed_length_sublist_def
[PROOF STATE]
proof (prove)
using this:
take d (drop (d * i') (concat xss)) = xss ! i'

goal (1 subgoal):
 1. take d (drop (d * i) (concat (xs # xss))) = (xs # xss) ! i
[PROOF STEP]
using Suc Cons.prems(1)
[PROOF STATE]
proof (prove)
using this:
take d (drop (d * i') (concat xss)) = xss ! i'
i = Suc i'
?xs \<in> set (xs # xss) \<Longrightarrow> length ?xs = d

goal (1 subgoal):
 1. take d (drop (d * i) (concat (xs # xss))) = (xs # xss) ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fixed_length_sublist (concat (xs # xss)) d i = (xs # xss) ! i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fixed_length_sublist (concat (xs # xss)) d i = (xs # xss) ! i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma concat_parts':
assumes "\<And>i. i<a \<Longrightarrow> length (f i) = d"
and "i<a"
shows "fixed_length_sublist (concat (map (\<lambda>i. f i) [0..<a])) d i = f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fixed_length_sublist (concat (map f [0..<a])) d i = f i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?i < a \<Longrightarrow> length (f ?i) = d
i < a

goal (1 subgoal):
 1. fixed_length_sublist (concat (map f [0..<a])) d i = f i
[PROOF STEP]
proof (induction a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>i. i < 0 \<Longrightarrow> length (f i) = d; i < 0\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<0])) d i = f i
 2. \<And>a. \<lbrakk>\<lbrakk>\<And>i. i < a \<Longrightarrow> length (f i) = d; i < a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<a])) d i = f i; \<And>i. i < Suc a \<Longrightarrow> length (f i) = d; i < Suc a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
?i < 0 \<Longrightarrow> length (f ?i) = d
i < 0

goal (2 subgoals):
 1. \<lbrakk>\<And>i. i < 0 \<Longrightarrow> length (f i) = d; i < 0\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<0])) d i = f i
 2. \<And>a. \<lbrakk>\<lbrakk>\<And>i. i < a \<Longrightarrow> length (f i) = d; i < a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<a])) d i = f i; \<And>i. i < Suc a \<Longrightarrow> length (f i) = d; i < Suc a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i < 0 \<Longrightarrow> length (f ?i) = d
i < 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?i < 0 \<Longrightarrow> length (f ?i) = d
i < 0

goal (1 subgoal):
 1. fixed_length_sublist (concat (map f [0..<0])) d i = f i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fixed_length_sublist (concat (map f [0..<0])) d i = f i

goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrakk>\<And>i. i < a \<Longrightarrow> length (f i) = d; i < a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<a])) d i = f i; \<And>i. i < Suc a \<Longrightarrow> length (f i) = d; i < Suc a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrakk>\<And>i. i < a \<Longrightarrow> length (f i) = d; i < a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<a])) d i = f i; \<And>i. i < Suc a \<Longrightarrow> length (f i) = d; i < Suc a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
case (Suc a)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>i. i < a \<Longrightarrow> length (f i) = d; i < a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<a])) d i = f i
?i < Suc a \<Longrightarrow> length (f ?i) = d
i < Suc a

goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrakk>\<And>i. i < a \<Longrightarrow> length (f i) = d; i < a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<a])) d i = f i; \<And>i. i < Suc a \<Longrightarrow> length (f i) = d; i < Suc a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>i. i < a \<Longrightarrow> length (f i) = d; i < a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<a])) d i = f i
?i < Suc a \<Longrightarrow> length (f ?i) = d
i < Suc a
[PROOF STEP]
have "(\<And>i. i < a \<Longrightarrow> length (f i) = d)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>i. i < a \<Longrightarrow> length (f i) = d; i < a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<a])) d i = f i
?i < Suc a \<Longrightarrow> length (f ?i) = d
i < Suc a

goal (1 subgoal):
 1. \<And>i. i < a \<Longrightarrow> length (f i) = d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i < a \<Longrightarrow> length (f ?i) = d

goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrakk>\<And>i. i < a \<Longrightarrow> length (f i) = d; i < a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<a])) d i = f i; \<And>i. i < Suc a \<Longrightarrow> length (f i) = d; i < Suc a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i < a \<Longrightarrow> length (f ?i) = d
[PROOF STEP]
have "length (concat (map f [0..<a])) = a*d"
[PROOF STATE]
proof (prove)
using this:
?i < a \<Longrightarrow> length (f ?i) = d

goal (1 subgoal):
 1. length (concat (map f [0..<a])) = a * d
[PROOF STEP]
using concat_equal_length_map
[PROOF STATE]
proof (prove)
using this:
?i < a \<Longrightarrow> length (f ?i) = d
(\<And>i. i < ?a \<Longrightarrow> length (?f i) = ?d) \<Longrightarrow> length (concat (map ?f [0..<?a])) = ?a * ?d

goal (1 subgoal):
 1. length (concat (map f [0..<a])) = a * d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (concat (map f [0..<a])) = a * d

goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrakk>\<And>i. i < a \<Longrightarrow> length (f i) = d; i < a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<a])) d i = f i; \<And>i. i < Suc a \<Longrightarrow> length (f i) = d; i < Suc a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
proof (cases "i=a")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = a \<Longrightarrow> fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
 2. i \<noteq> a \<Longrightarrow> fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
assume "i=a"
[PROOF STATE]
proof (state)
this:
i = a

goal (2 subgoals):
 1. i = a \<Longrightarrow> fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
 2. i \<noteq> a \<Longrightarrow> fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = a
[PROOF STEP]
have "fixed_length_sublist (concat (map f [0..<Suc a])) d i = f a"
[PROOF STATE]
proof (prove)
using this:
i = a

goal (1 subgoal):
 1. fixed_length_sublist (concat (map f [0..<Suc a])) d i = f a
[PROOF STEP]
by (simp add: Suc.prems(1) \<open>length (concat (map f [0..<a])) = a * d\<close> fixed_length_sublist_def)
[PROOF STATE]
proof (state)
this:
fixed_length_sublist (concat (map f [0..<Suc a])) d i = f a

goal (2 subgoals):
 1. i = a \<Longrightarrow> fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
 2. i \<noteq> a \<Longrightarrow> fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fixed_length_sublist (concat (map f [0..<Suc a])) d i = f a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fixed_length_sublist (concat (map f [0..<Suc a])) d i = f a

goal (1 subgoal):
 1. fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
using \<open>i=a\<close>
[PROOF STATE]
proof (prove)
using this:
fixed_length_sublist (concat (map f [0..<Suc a])) d i = f a
i = a

goal (1 subgoal):
 1. fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i

goal (1 subgoal):
 1. i \<noteq> a \<Longrightarrow> fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> a \<Longrightarrow> fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
assume "i\<noteq>a"
[PROOF STATE]
proof (state)
this:
i \<noteq> a

goal (1 subgoal):
 1. i \<noteq> a \<Longrightarrow> fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<noteq> a
[PROOF STEP]
have "fixed_length_sublist (concat (map f [0..<a])) d i = f i"
      "concat (map f [0..<Suc a]) = concat (map f [0..<a]) @ f a"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> a

goal (1 subgoal):
 1. fixed_length_sublist (concat (map f [0..<a])) d i = f i &&& concat (map f [0..<Suc a]) = concat (map f [0..<a]) @ f a
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
i \<noteq> a
\<lbrakk>\<And>i. i < a \<Longrightarrow> length (f i) = d; i < a\<rbrakk> \<Longrightarrow> fixed_length_sublist (concat (map f [0..<a])) d i = f i
?i < Suc a \<Longrightarrow> length (f ?i) = d
i < Suc a

goal (1 subgoal):
 1. fixed_length_sublist (concat (map f [0..<a])) d i = f i &&& concat (map f [0..<Suc a]) = concat (map f [0..<a]) @ f a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fixed_length_sublist (concat (map f [0..<a])) d i = f i
concat (map f [0..<Suc a]) = concat (map f [0..<a]) @ f a

goal (1 subgoal):
 1. i \<noteq> a \<Longrightarrow> fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i
[PROOF STEP]
unfolding \<open>concat (map f [0..<Suc a]) = concat (map f [0..<a]) @ f a\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fixed_length_sublist (concat (map f [0..<a]) @ f a) d i = f i
[PROOF STEP]
unfolding fixed_length_sublist_def drop_append
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take d (drop (d * i) (concat (map f [0..<a])) @ drop (d * i - length (concat (map f [0..<a]))) (f a)) = f i
[PROOF STEP]
using  \<open>length (concat (map f [0..<a])) = a * d\<close>  \<open>fixed_length_sublist (concat (map f [0..<a])) d i = f i\<close>
[PROOF STATE]
proof (prove)
using this:
length (concat (map f [0..<a])) = a * d
fixed_length_sublist (concat (map f [0..<a])) d i = f i

goal (1 subgoal):
 1. take d (drop (d * i) (concat (map f [0..<a])) @ drop (d * i - length (concat (map f [0..<a]))) (f a)) = f i
[PROOF STEP]
using append_assoc append_eq_conv_conj append_take_drop_id assms(1) assms(2)  fixed_length_sublist_def
[PROOF STATE]
proof (prove)
using this:
length (concat (map f [0..<a])) = a * d
fixed_length_sublist (concat (map f [0..<a])) d i = f i
(?xs @ ?ys) @ ?zs = ?xs @ ?ys @ ?zs
(?xs @ ?ys = ?zs) = (?xs = take (length ?xs) ?zs \<and> ?ys = drop (length ?xs) ?zs)
take ?n ?xs @ drop ?n ?xs = ?xs
?i < a \<Longrightarrow> length (f ?i) = d
i < a
fixed_length_sublist ?xs ?l ?i = take ?l (drop (?l * ?i) ?xs)

goal (1 subgoal):
 1. take d (drop (d * i) (concat (map f [0..<a])) @ drop (d * i - length (concat (map f [0..<a]))) (f a)) = f i
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fixed_length_sublist (concat (map f [0..<Suc a])) d i = f i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_tensor_vec_from_lookup:
"length (tensor_vec_from_lookup ds e) = prod_list ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (tensor_vec_from_lookup ds e) = prod_list ds
[PROOF STEP]
by (induction ds arbitrary:e; auto simp add: concat_equal_length_map)


[STATEMENT]
lemma lookup_tensor_vec:
assumes "is\<lhd>ds"
shows "lookup_base ds (tensor_vec_from_lookup ds e) is = e is"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup_base ds (tensor_vec_from_lookup ds e) is = e is
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is \<lhd> ds

goal (1 subgoal):
 1. lookup_base ds (tensor_vec_from_lookup ds e) is = e is
[PROOF STEP]
proof (induction arbitrary:e rule:valid_index.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>e. lookup_base [] (tensor_vec_from_lookup [] e) [] = e []
 2. \<And>is ds i d e. \<lbrakk>is \<lhd> ds; \<And>e. lookup_base ds (tensor_vec_from_lookup ds e) is = e is; i < d\<rbrakk> \<Longrightarrow> lookup_base (d # ds) (tensor_vec_from_lookup (d # ds) e) (i # is) = e (i # is)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>e. lookup_base [] (tensor_vec_from_lookup [] e) [] = e []
 2. \<And>is ds i d e. \<lbrakk>is \<lhd> ds; \<And>e. lookup_base ds (tensor_vec_from_lookup ds e) is = e is; i < d\<rbrakk> \<Longrightarrow> lookup_base (d # ds) (tensor_vec_from_lookup (d # ds) e) (i # is) = e (i # is)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup_base [] (tensor_vec_from_lookup [] e) [] = e []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lookup_base [] (tensor_vec_from_lookup [] e) [] = e []

goal (1 subgoal):
 1. \<And>is ds i d e. \<lbrakk>is \<lhd> ds; \<And>e. lookup_base ds (tensor_vec_from_lookup ds e) is = e is; i < d\<rbrakk> \<Longrightarrow> lookup_base (d # ds) (tensor_vec_from_lookup (d # ds) e) (i # is) = e (i # is)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>is ds i d e. \<lbrakk>is \<lhd> ds; \<And>e. lookup_base ds (tensor_vec_from_lookup ds e) is = e is; i < d\<rbrakk> \<Longrightarrow> lookup_base (d # ds) (tensor_vec_from_lookup (d # ds) e) (i # is) = e (i # is)
[PROOF STEP]
case (Cons "is" ds i d e)
[PROOF STATE]
proof (state)
this:
is \<lhd> ds
i < d
lookup_base ds (tensor_vec_from_lookup ds ?e) is = ?e is

goal (1 subgoal):
 1. \<And>is ds i d e. \<lbrakk>is \<lhd> ds; \<And>e. lookup_base ds (tensor_vec_from_lookup ds e) is = e is; i < d\<rbrakk> \<Longrightarrow> lookup_base (d # ds) (tensor_vec_from_lookup (d # ds) e) (i # is) = e (i # is)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is \<lhd> ds
i < d
lookup_base ds (tensor_vec_from_lookup ds ?e) is = ?e is
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is \<lhd> ds
i < d
lookup_base ds (tensor_vec_from_lookup ds ?e) is = ?e is

goal (1 subgoal):
 1. lookup_base (d # ds) (tensor_vec_from_lookup (d # ds) e) (i # is) = e (i # is)
[PROOF STEP]
unfolding tensor_vec_from_lookup_Cons lookup_base_Cons
[PROOF STATE]
proof (prove)
using this:
is \<lhd> ds
i < d
lookup_base ds (tensor_vec_from_lookup ds ?e) is = ?e is

goal (1 subgoal):
 1. lookup_base ds (fixed_length_sublist (concat (map (\<lambda>i. tensor_vec_from_lookup ds (\<lambda>is. e (i # is))) [0..<d])) (prod_list ds) i) is = e (i # is)
[PROOF STEP]
by (simp add: length_tensor_vec_from_lookup concat_parts'[of d "\<lambda>i. tensor_vec_from_lookup ds (\<lambda>is. e (i # is))" "prod_list ds" i] \<open>i < d\<close>)
[PROOF STATE]
proof (state)
this:
lookup_base (d # ds) (tensor_vec_from_lookup (d # ds) e) (i # is) = e (i # is)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lookup_tensor_from_lookup:
assumes "is\<lhd>ds"
shows "lookup (tensor_from_lookup ds e) is = e is"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (tensor_from_lookup ds e) is = e is
[PROOF STEP]
unfolding lookup_def tensor_from_lookup_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup_base (dims (tensor_from_vec ds (tensor_vec_from_lookup ds e))) (vec (tensor_from_vec ds (tensor_vec_from_lookup ds e))) is = e is
[PROOF STEP]
by (simp add: lookup_tensor_vec assms length_tensor_vec_from_lookup)


[STATEMENT]
lemma dims_tensor_from_lookup: "dims (tensor_from_lookup ds e) = ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dims (tensor_from_lookup ds e) = ds
[PROOF STEP]
unfolding tensor_from_lookup_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dims (tensor_from_vec ds (tensor_vec_from_lookup ds e)) = ds
[PROOF STEP]
by (simp add: length_tensor_vec_from_lookup)


[STATEMENT]
lemma tensor_lookup_cong:
assumes "tensor_from_lookup ds e\<^sub>1 = tensor_from_lookup ds e\<^sub>2"
and "is\<lhd>ds"
shows "e\<^sub>1 is = e\<^sub>2 is"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e\<^sub>1 is = e\<^sub>2 is
[PROOF STEP]
using assms lookup_tensor_from_lookup
[PROOF STATE]
proof (prove)
using this:
tensor_from_lookup ds e\<^sub>1 = tensor_from_lookup ds e\<^sub>2
is \<lhd> ds
?is \<lhd> ?ds \<Longrightarrow> lookup (tensor_from_lookup ?ds ?e) ?is = ?e ?is

goal (1 subgoal):
 1. e\<^sub>1 is = e\<^sub>2 is
[PROOF STEP]
by metis


[STATEMENT]
lemma tensor_from_lookup_eqI:
assumes "\<And>is. is\<lhd>ds \<Longrightarrow> e\<^sub>1 is = e\<^sub>2 is"
shows "tensor_from_lookup ds e\<^sub>1 = tensor_from_lookup ds e\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tensor_from_lookup ds e\<^sub>1 = tensor_from_lookup ds e\<^sub>2
[PROOF STEP]
by (metis assms lookup_tensor_vec length_tensor_vec_from_lookup tensor_lookup_base tensor_from_lookup_def)


[STATEMENT]
lemma tensor_lookup_eqI:
assumes "dims A = dims B" and "\<And>is. is\<lhd>(dims A) \<Longrightarrow> lookup A is = lookup B is"
shows "A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = B
[PROOF STEP]
by (metis assms(1) assms(2) tensor_lookup)


[STATEMENT]
lemma card_even[simp]: "card {a \<in> Collect even. a < 2 * n} = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {a \<in> Collect even. a < 2 * n} = n
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. card {a \<in> Collect even. a < 2 * 0} = 0
 2. \<And>n. card {a \<in> Collect even. a < 2 * n} = n \<Longrightarrow> card {a \<in> Collect even. a < 2 * Suc n} = Suc n
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. card {a \<in> Collect even. a < 2 * 0} = 0
 2. \<And>n. card {a \<in> Collect even. a < 2 * n} = n \<Longrightarrow> card {a \<in> Collect even. a < 2 * Suc n} = Suc n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {a \<in> Collect even. a < 2 * 0} = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {a \<in> Collect even. a < 2 * 0} = 0

goal (1 subgoal):
 1. \<And>n. card {a \<in> Collect even. a < 2 * n} = n \<Longrightarrow> card {a \<in> Collect even. a < 2 * Suc n} = Suc n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. card {a \<in> Collect even. a < 2 * n} = n \<Longrightarrow> card {a \<in> Collect even. a < 2 * Suc n} = Suc n
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
card {a \<in> Collect even. a < 2 * n} = n

goal (1 subgoal):
 1. \<And>n. card {a \<in> Collect even. a < 2 * n} = n \<Longrightarrow> card {a \<in> Collect even. a < 2 * Suc n} = Suc n
[PROOF STEP]
have "{a \<in> Collect even. a < 2 * Suc n} = insert (2*n) {a \<in> Collect even. a < 2 * n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a \<in> Collect even. a < 2 * Suc n} = insert (2 * n) {a \<in> Collect even. a < 2 * n}
[PROOF STEP]
using le_eq_less_or_eq less_Suc_eq_le subset_antisym
[PROOF STATE]
proof (prove)
using this:
(?m \<le> ?n) = (?m < ?n \<or> ?m = ?n)
(?m < Suc ?n) = (?m \<le> ?n)
\<lbrakk>?A \<subseteq> ?B; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> ?A = ?B

goal (1 subgoal):
 1. {a \<in> Collect even. a < 2 * Suc n} = insert (2 * n) {a \<in> Collect even. a < 2 * n}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{a \<in> Collect even. a < 2 * Suc n} = insert (2 * n) {a \<in> Collect even. a < 2 * n}

goal (1 subgoal):
 1. \<And>n. card {a \<in> Collect even. a < 2 * n} = n \<Longrightarrow> card {a \<in> Collect even. a < 2 * Suc n} = Suc n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {a \<in> Collect even. a < 2 * Suc n} = Suc n
[PROOF STEP]
unfolding \<open>{a \<in> Collect even. a < 2 * Suc n} = insert (2*n) {a \<in> Collect even. a < 2 * n}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (insert (2 * n) {a \<in> Collect even. a < 2 * n}) = Suc n
[PROOF STEP]
using Suc card_insert_disjoint[of "{a \<in> Collect even. a < 2 * n}" "2*n"]
[PROOF STATE]
proof (prove)
using this:
card {a \<in> Collect even. a < 2 * n} = n
\<lbrakk>finite {a \<in> Collect even. a < 2 * n}; 2 * n \<notin> {a \<in> Collect even. a < 2 * n}\<rbrakk> \<Longrightarrow> card (insert (2 * n) {a \<in> Collect even. a < 2 * n}) = Suc (card {a \<in> Collect even. a < 2 * n})

goal (1 subgoal):
 1. card (insert (2 * n) {a \<in> Collect even. a < 2 * n}) = Suc n
[PROOF STEP]
by (simp add: finite_M_bounded_by_nat less_not_refl2)
[PROOF STATE]
proof (state)
this:
card {a \<in> Collect even. a < 2 * Suc n} = Suc n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_odd[simp]: "card {a \<in> Collect odd. a < 2 * n} = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {a \<in> {a. odd a}. a < 2 * n} = n
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. card {a \<in> {a. odd a}. a < 2 * 0} = 0
 2. \<And>n. card {a \<in> {a. odd a}. a < 2 * n} = n \<Longrightarrow> card {a \<in> {a. odd a}. a < 2 * Suc n} = Suc n
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

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

goal (1 subgoal):
 1. \<And>n. card {a \<in> {a. odd a}. a < 2 * n} = n \<Longrightarrow> card {a \<in> {a. odd a}. a < 2 * Suc n} = Suc n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. card {a \<in> {a. odd a}. a < 2 * n} = n \<Longrightarrow> card {a \<in> {a. odd a}. a < 2 * Suc n} = Suc n
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
card {a \<in> {a. odd a}. a < 2 * n} = n

goal (1 subgoal):
 1. \<And>n. card {a \<in> {a. odd a}. a < 2 * n} = n \<Longrightarrow> card {a \<in> {a. odd a}. a < 2 * Suc n} = Suc n
[PROOF STEP]
have "{a \<in> Collect odd. a < 2 * Suc n} = insert (2*n+1) {a \<in> Collect odd. a < 2 * n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a \<in> {a. odd a}. a < 2 * Suc n} = insert (2 * n + 1) {a \<in> {a. odd a}. a < 2 * n}
[PROOF STEP]
using le_eq_less_or_eq less_Suc_eq_le subset_antisym
[PROOF STATE]
proof (prove)
using this:
(?m \<le> ?n) = (?m < ?n \<or> ?m = ?n)
(?m < Suc ?n) = (?m \<le> ?n)
\<lbrakk>?A \<subseteq> ?B; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> ?A = ?B

goal (1 subgoal):
 1. {a \<in> {a. odd a}. a < 2 * Suc n} = insert (2 * n + 1) {a \<in> {a. odd a}. a < 2 * n}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{a \<in> {a. odd a}. a < 2 * Suc n} = insert (2 * n + 1) {a \<in> {a. odd a}. a < 2 * n}

goal (1 subgoal):
 1. \<And>n. card {a \<in> {a. odd a}. a < 2 * n} = n \<Longrightarrow> card {a \<in> {a. odd a}. a < 2 * Suc n} = Suc n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {a \<in> {a. odd a}. a < 2 * Suc n} = Suc n
[PROOF STEP]
unfolding \<open>{a \<in> Collect odd. a < 2 * Suc n} = insert (2*n+1) {a \<in> Collect odd. a < 2 * n}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (insert (2 * n + 1) {a \<in> {a. odd a}. a < 2 * n}) = Suc n
[PROOF STEP]
using Suc card_insert_disjoint[of "{a \<in> Collect even. a < 2 * n}" "2*n"]
[PROOF STATE]
proof (prove)
using this:
card {a \<in> {a. odd a}. a < 2 * n} = n
\<lbrakk>finite {a \<in> Collect even. a < 2 * n}; 2 * n \<notin> {a \<in> Collect even. a < 2 * n}\<rbrakk> \<Longrightarrow> card (insert (2 * n) {a \<in> Collect even. a < 2 * n}) = Suc (card {a \<in> Collect even. a < 2 * n})

goal (1 subgoal):
 1. card (insert (2 * n + 1) {a \<in> {a. odd a}. a < 2 * n}) = Suc n
[PROOF STEP]
by (simp add: finite_M_bounded_by_nat less_not_refl2)
[PROOF STATE]
proof (state)
this:
card {a \<in> {a. odd a}. a < 2 * Suc n} = Suc n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma varSort_lt_var_INNER:
"|UNIV :: 'varSort set| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |UNIV| <o |UNIV|
[PROOF STEP]
using varSort_lt_var
[PROOF STATE]
proof (prove)
using this:
varSort_lt_var undefined undefined

goal (1 subgoal):
 1. |UNIV| <o |UNIV|
[PROOF STEP]
unfolding varSort_lt_var_def
[PROOF STATE]
proof (prove)
using this:
|UNIV| <o |UNIV|

goal (1 subgoal):
 1. |UNIV| <o |UNIV|
[PROOF STEP]
by simp


[STATEMENT]
lemma varSort_le_Var:
"|UNIV :: 'varSort set| \<le>o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |UNIV| \<le>o |UNIV|
[PROOF STEP]
using varSort_lt_var_INNER ordLess_imp_ordLeq
[PROOF STATE]
proof (prove)
using this:
|UNIV| <o |UNIV|
?r <o ?r' \<Longrightarrow> ?r \<le>o ?r'

goal (1 subgoal):
 1. |UNIV| \<le>o |UNIV|
[PROOF STEP]
by auto


[STATEMENT]
theorem var_infinite_INNER: "infinite (UNIV :: 'var set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite UNIV
[PROOF STEP]
using var_infinite
[PROOF STATE]
proof (prove)
using this:
var_infinite undefined

goal (1 subgoal):
 1. infinite UNIV
[PROOF STEP]
unfolding var_infinite_def
[PROOF STATE]
proof (prove)
using this:
infinite UNIV

goal (1 subgoal):
 1. infinite UNIV
[PROOF STEP]
by simp


[STATEMENT]
theorem var_regular_INNER: "regular |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regular |UNIV|
[PROOF STEP]
using var_regular
[PROOF STATE]
proof (prove)
using this:
var_regular undefined

goal (1 subgoal):
 1. regular |UNIV|
[PROOF STEP]
unfolding var_regular_def
[PROOF STATE]
proof (prove)
using this:
regular |UNIV|

goal (1 subgoal):
 1. regular |UNIV|
[PROOF STEP]
by simp


[STATEMENT]
theorem infinite_var_regular_INNER:
"infinite (UNIV :: 'var set) \<and> regular |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite UNIV \<and> regular |UNIV|
[PROOF STEP]
by (simp add: var_infinite_INNER var_regular_INNER)


[STATEMENT]
theorem finite_ordLess_var:
"( |S| <o |UNIV :: 'var set| \<or> finite S) = ( |S| <o |UNIV :: 'var set| )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (|S| <o |UNIV| \<or> finite S) = (|S| <o |UNIV|)
[PROOF STEP]
by (auto simp add: var_infinite_INNER finite_ordLess_infinite2)


[STATEMENT]
lemma qSwapAll_preserves_qGoodAll1:
fixes X::"('index,'bindex,'varSort,'var,'opSym)qTerm" and
      A::"('index,'bindex,'varSort,'var,'opSym)qAbs" and zs x y
shows
"(qGood X \<longrightarrow> qGood (X #[[x \<and> y]]_zs)) \<and>
 (qGoodAbs A \<longrightarrow> qGoodAbs (A $[[x \<and> y]]_zs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qGood X \<longrightarrow> qGood (X #[[x \<and> y]]_zs)) \<and> (qGoodAbs A \<longrightarrow> qGoodAbs (A $[[x \<and> y]]_zs))
[PROOF STEP]
apply(rule qTerm_induct[of _ _ X A])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xs xa. qGood (qVar xs xa) \<longrightarrow> qGood (qVar xs xa #[[x \<and> y]]_zs)
 2. \<And>delta inp binp. \<lbrakk>liftAll (\<lambda>a. qGood a \<longrightarrow> qGood (a #[[x \<and> y]]_zs)) inp; liftAll (\<lambda>a. qGoodAbs a \<longrightarrow> qGoodAbs (a $[[x \<and> y]]_zs)) binp\<rbrakk> \<Longrightarrow> qGood (qOp delta inp binp) \<longrightarrow> qGood (qOp delta inp binp #[[x \<and> y]]_zs)
 3. \<And>xs xa X. \<lbrakk>\<And>Y. (X, Y) \<in> qSwapped \<Longrightarrow> qGood Y \<longrightarrow> qGood (Y #[[x \<and> y]]_zs); \<And>Y. qSkel Y = qSkel X \<Longrightarrow> qGood Y \<longrightarrow> qGood (Y #[[x \<and> y]]_zs)\<rbrakk> \<Longrightarrow> qGoodAbs (qAbs xs xa X) \<longrightarrow> qGoodAbs (qAbs xs xa X $[[x \<and> y]]_zs)
[PROOF STEP]
apply(simp_all add: sw_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>inp binp. \<lbrakk>liftAll (\<lambda>a. qGood a \<longrightarrow> qGood (a #[[x \<and> y]]_zs)) inp; liftAll (\<lambda>a. qGoodAbs a \<longrightarrow> qGoodAbs (a $[[x \<and> y]]_zs)) binp\<rbrakk> \<Longrightarrow> liftAll qGood inp \<and> liftAll qGoodAbs binp \<and> |{i. \<exists>y. inp i = Some y}| <o |UNIV| \<and> |{i. \<exists>y. binp i = Some y}| <o |UNIV| \<longrightarrow> liftAll qGood (lift (qSwap zs x y) inp) \<and> liftAll qGoodAbs (lift (qSwapAbs zs x y) binp) \<and> |{i. \<exists>ya. lift (qSwap zs x y) inp i = Some ya}| <o |UNIV| \<and> |{i. \<exists>ya. lift (qSwapAbs zs x y) binp i = Some ya}| <o |UNIV|
[PROOF STEP]
unfolding lift_def liftAll_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs)\<rbrakk> \<Longrightarrow> (\<forall>i v. inp i = Some v \<longrightarrow> qGood v) \<and> (\<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v) \<and> |{i. \<exists>y. inp i = Some y}| <o |UNIV| \<and> |{i. \<exists>y. binp i = Some y}| <o |UNIV| \<longrightarrow> (\<forall>i v. (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v #[[x \<and> y]]_zs)) = Some v \<longrightarrow> qGood v) \<and> (\<forall>i v. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some v \<longrightarrow> qGoodAbs v) \<and> |{i. \<exists>ya. (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v #[[x \<and> y]]_zs)) = Some ya}| <o |UNIV| \<and> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>inp binp i v. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|; (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v #[[x \<and> y]]_zs)) = Some v\<rbrakk> \<Longrightarrow> qGood v
 2. \<And>inp binp i v. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|; (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some v\<rbrakk> \<Longrightarrow> qGoodAbs v
 3. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v #[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
 4. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
apply(case_tac "inp i", auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>inp binp i v. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|; (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some v\<rbrakk> \<Longrightarrow> qGoodAbs v
 2. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v #[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
 3. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
apply(case_tac "binp i", auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v #[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
 2. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v #[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
 2. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
fix inp::"('index,('index,'bindex,'varSort,'var,'opSym)qTerm)input" and zs xs x y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v #[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
 2. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
let ?K1 = "{i. \<exists>X. inp i = Some X}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v #[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
 2. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
let ?K2 = "{i. \<exists>X. (case inp i of None \<Rightarrow> None | Some X \<Rightarrow> Some (X #[[x \<and> y]]_zs))
                     = Some X}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v #[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
 2. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
assume "|?K1| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (state)
this:
|{i. \<exists>X. inp i = Some X}| <o |UNIV|

goal (2 subgoals):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v #[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
 2. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
|{i. \<exists>X. inp i = Some X}| <o |UNIV|

goal (2 subgoals):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v #[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
 2. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
have "?K1 = ?K2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. \<exists>X. inp i = Some X} = {i. \<exists>X. (case inp i of None \<Rightarrow> None | Some X \<Rightarrow> Some (X #[[x \<and> y]]_zs)) = Some X}
[PROOF STEP]
by(auto, case_tac "inp x", auto)
[PROOF STATE]
proof (state)
this:
{i. \<exists>X. inp i = Some X} = {i. \<exists>X. (case inp i of None \<Rightarrow> None | Some X \<Rightarrow> Some (X #[[x \<and> y]]_zs)) = Some X}

goal (2 subgoals):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v #[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
 2. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
|{i. \<exists>X. inp i = Some X}| <o |UNIV|
{i. \<exists>X. inp i = Some X} = {i. \<exists>X. (case inp i of None \<Rightarrow> None | Some X \<Rightarrow> Some (X #[[x \<and> y]]_zs)) = Some X}
[PROOF STEP]
show "|?K2| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
|{i. \<exists>X. inp i = Some X}| <o |UNIV|
{i. \<exists>X. inp i = Some X} = {i. \<exists>X. (case inp i of None \<Rightarrow> None | Some X \<Rightarrow> Some (X #[[x \<and> y]]_zs)) = Some X}

goal (1 subgoal):
 1. |{i. \<exists>X. (case inp i of None \<Rightarrow> None | Some X \<Rightarrow> Some (X #[[x \<and> y]]_zs)) = Some X}| <o |UNIV|
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
|{i. \<exists>X. (case inp i of None \<Rightarrow> None | Some X \<Rightarrow> Some (X #[[x \<and> y]]_zs)) = Some X}| <o |UNIV|

goal (1 subgoal):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
fix binp::"('bindex,('index,'bindex,'varSort,'var,'opSym)qAbs)input" and zs xs x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
let ?K1 = "{i. \<exists>A. binp i = Some A}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
let ?K2 = "{i. \<exists>A. (case binp i of None \<Rightarrow> None | Some A \<Rightarrow> Some (A $[[x \<and> y]]_zs))
                     = Some A}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
assume "|?K1| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (state)
this:
|{i. \<exists>A. binp i = Some A}| <o |UNIV|

goal (1 subgoal):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
|{i. \<exists>A. binp i = Some A}| <o |UNIV|

goal (1 subgoal):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
have "?K1 = ?K2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. \<exists>A. binp i = Some A} = {i. \<exists>A. (case binp i of None \<Rightarrow> None | Some A \<Rightarrow> Some (A $[[x \<and> y]]_zs)) = Some A}
[PROOF STEP]
by(auto, case_tac "binp x", auto)
[PROOF STATE]
proof (state)
this:
{i. \<exists>A. binp i = Some A} = {i. \<exists>A. (case binp i of None \<Rightarrow> None | Some A \<Rightarrow> Some (A $[[x \<and> y]]_zs)) = Some A}

goal (1 subgoal):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> qGood (v #[[x \<and> y]]_zs); \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs (v $[[x \<and> y]]_zs); \<forall>i v. inp i = Some v \<longrightarrow> qGood v; \<forall>i v. binp i = Some v \<longrightarrow> qGoodAbs v; |{i. \<exists>y. inp i = Some y}| <o |UNIV|; |{i. \<exists>y. binp i = Some y}| <o |UNIV|\<rbrakk> \<Longrightarrow> |{i. \<exists>ya. (case binp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (v $[[x \<and> y]]_zs)) = Some ya}| <o |UNIV|
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
|{i. \<exists>A. binp i = Some A}| <o |UNIV|
{i. \<exists>A. binp i = Some A} = {i. \<exists>A. (case binp i of None \<Rightarrow> None | Some A \<Rightarrow> Some (A $[[x \<and> y]]_zs)) = Some A}
[PROOF STEP]
show "|?K2| <o |UNIV :: 'var set|"
[PROOF STATE]
proof (prove)
using this:
|{i. \<exists>A. binp i = Some A}| <o |UNIV|
{i. \<exists>A. binp i = Some A} = {i. \<exists>A. (case binp i of None \<Rightarrow> None | Some A \<Rightarrow> Some (A $[[x \<and> y]]_zs)) = Some A}

goal (1 subgoal):
 1. |{i. \<exists>A. (case binp i of None \<Rightarrow> None | Some A \<Rightarrow> Some (A $[[x \<and> y]]_zs)) = Some A}| <o |UNIV|
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
|{i. \<exists>A. (case binp i of None \<Rightarrow> None | Some A \<Rightarrow> Some (A $[[x \<and> y]]_zs)) = Some A}| <o |UNIV|

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma qSwap_preserves_qGood2:
assumes "qGood(X #[[x \<and> y]]_zs)"
shows "qGood X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood X
[PROOF STEP]
by (metis assms qSwap_involutive qSwap_preserves_qGood1)


[STATEMENT]
lemma qSwapAbs_preserves_qGoodAbs2:
assumes "qGoodAbs(A $[[x \<and> y]]_zs)"
shows "qGoodAbs A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGoodAbs A
[PROOF STEP]
by (metis assms qSwapAbs_preserves_qGoodAbs1 qSwapAll_involutive)


[STATEMENT]
lemma qSwap_preserves_qGood: "(qGood (X #[[x \<and> y]]_zs)) = (qGood X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood (X #[[x \<and> y]]_zs) = qGood X
[PROOF STEP]
using qSwap_preserves_qGood1 qSwap_preserves_qGood2
[PROOF STATE]
proof (prove)
using this:
qGood ?X \<Longrightarrow> qGood (?X #[[?x \<and> ?y]]_?zs)
qGood (?X #[[?x \<and> ?y]]_?zs) \<Longrightarrow> qGood ?X

goal (1 subgoal):
 1. qGood (X #[[x \<and> y]]_zs) = qGood X
[PROOF STEP]
by blast


[STATEMENT]
lemma qSwapAbs_preserves_qGoodAbs:
"(qGoodAbs (A $[[x \<and> y]]_zs)) = (qGoodAbs A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGoodAbs (A $[[x \<and> y]]_zs) = qGoodAbs A
[PROOF STEP]
using qSwapAbs_preserves_qGoodAbs1 qSwapAbs_preserves_qGoodAbs2
[PROOF STATE]
proof (prove)
using this:
qGoodAbs ?A \<Longrightarrow> qGoodAbs (?A $[[?x \<and> ?y]]_?zs)
qGoodAbs (?A $[[?x \<and> ?y]]_?zs) \<Longrightarrow> qGoodAbs ?A

goal (1 subgoal):
 1. qGoodAbs (A $[[x \<and> y]]_zs) = qGoodAbs A
[PROOF STEP]
by blast


[STATEMENT]
lemma qSwap_twice_preserves_qGood:
"(qGood ((X #[[x \<and> y]]_zs) #[[x' \<and> y']]_zs')) = (qGood X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qGood (X #[[x \<and> y]]_zs #[[x' \<and> y']]_zs') = qGood X
[PROOF STEP]
by (simp add: qSwap_preserves_qGood)


[STATEMENT]
lemma qSwapped_preserves_qGood:
"(X,Y) \<in> qSwapped \<Longrightarrow> qGood Y = qGood X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X, Y) \<in> qSwapped \<Longrightarrow> qGood Y = qGood X
[PROOF STEP]
apply (induct rule: qSwapped.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>X. qGood X = qGood X
 2. \<And>X Y Z. \<lbrakk>(X, Y) \<in> qSwapped; qGood Y = qGood X; (Y, Z) \<in> qSwapped; qGood Z = qGood Y\<rbrakk> \<Longrightarrow> qGood Z = qGood X
 3. \<And>X Y x y zs. \<lbrakk>(X, Y) \<in> qSwapped; qGood Y = qGood X\<rbrakk> \<Longrightarrow> qGood (Y #[[x \<and> y]]_zs) = qGood X
[PROOF STEP]
using qSwap_preserves_qGood
[PROOF STATE]
proof (prove)
using this:
qGood (?X #[[?x \<and> ?y]]_?zs) = qGood ?X

goal (3 subgoals):
 1. \<And>X. qGood X = qGood X
 2. \<And>X Y Z. \<lbrakk>(X, Y) \<in> qSwapped; qGood Y = qGood X; (Y, Z) \<in> qSwapped; qGood Z = qGood Y\<rbrakk> \<Longrightarrow> qGood Z = qGood X
 3. \<And>X Y x y zs. \<lbrakk>(X, Y) \<in> qSwapped; qGood Y = qGood X\<rbrakk> \<Longrightarrow> qGood (Y #[[x \<and> y]]_zs) = qGood X
[PROOF STEP]
by auto


[STATEMENT]
lemma qGood_qTerm_templateInduct[case_names Rel Var Op Abs]:
fixes X::"('index,'bindex,'varSort,'var,'opSym)qTerm"
and A::"('index,'bindex,'varSort,'var,'opSym)qAbs" and phi phiAbs rel
assumes
REL: "\<And> X Y. \<lbrakk>qGood X; (X,Y) \<in> rel\<rbrakk> \<Longrightarrow> qGood Y \<and> qSkel Y = qSkel X" and
Var: "\<And> xs x. phi (qVar xs x)" and
Op: "\<And> delta inp binp. \<lbrakk>|{i. inp i \<noteq> None}| <o |UNIV :: 'var set|;
                        |{i. binp i \<noteq> None}| <o |UNIV :: 'var set|;
                        liftAll (\<lambda>X. qGood X \<and> phi X) inp;
                        liftAll (\<lambda>A. qGoodAbs A \<and> phiAbs A) binp\<rbrakk>
                   \<Longrightarrow> phi (qOp delta inp binp)" and
Abs: "\<And> xs x X. \<lbrakk>qGood X; \<And> Y. (X,Y) \<in> rel \<Longrightarrow> phi Y\<rbrakk>
                 \<Longrightarrow> phiAbs (qAbs xs x X)"
shows
"(qGood X \<longrightarrow> phi X) \<and> (qGoodAbs A \<longrightarrow> phiAbs A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qGood X \<longrightarrow> phi X) \<and> (qGoodAbs A \<longrightarrow> phiAbs A)
[PROOF STEP]
apply(induct rule: qTerm_templateInduct[of "{(X,Y). qGood X \<and> (X,Y) \<in> rel}"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>X Y. (X, Y) \<in> {(X, Y). qGood X \<and> (X, Y) \<in> rel} \<Longrightarrow> qSkel Y = qSkel X
 2. \<And>xs x. qGood (qVar xs x) \<longrightarrow> phi (qVar xs x)
 3. \<And>delta inp binp. \<lbrakk>liftAll (\<lambda>a. qGood a \<longrightarrow> phi a) inp; liftAll (\<lambda>a. qGoodAbs a \<longrightarrow> phiAbs a) binp\<rbrakk> \<Longrightarrow> qGood (qOp delta inp binp) \<longrightarrow> phi (qOp delta inp binp)
 4. \<And>xs x X. (\<And>Y. (X, Y) \<in> {(X, Y). qGood X \<and> (X, Y) \<in> rel} \<Longrightarrow> qGood Y \<longrightarrow> phi Y) \<Longrightarrow> qGoodAbs (qAbs xs x X) \<longrightarrow> phiAbs (qAbs xs x X)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>qGood ?X11; (?X11, ?Y11) \<in> rel\<rbrakk> \<Longrightarrow> qGood ?Y11 \<and> qSkel ?Y11 = qSkel ?X11
phi (qVar ?xs11 ?x11)
\<lbrakk>|{i. ?inp11 i \<noteq> None}| <o |UNIV|; |{i. ?binp11 i \<noteq> None}| <o |UNIV|; liftAll (\<lambda>X. qGood X \<and> phi X) ?inp11; liftAll (\<lambda>A. qGoodAbs A \<and> phiAbs A) ?binp11\<rbrakk> \<Longrightarrow> phi (qOp ?delta11 ?inp11 ?binp11)
\<lbrakk>qGood ?X11; \<And>Y. (?X11, Y) \<in> rel \<Longrightarrow> phi Y\<rbrakk> \<Longrightarrow> phiAbs (qAbs ?xs11 ?x11 ?X11)

goal (4 subgoals):
 1. \<And>X Y. (X, Y) \<in> {(X, Y). qGood X \<and> (X, Y) \<in> rel} \<Longrightarrow> qSkel Y = qSkel X
 2. \<And>xs x. qGood (qVar xs x) \<longrightarrow> phi (qVar xs x)
 3. \<And>delta inp binp. \<lbrakk>liftAll (\<lambda>a. qGood a \<longrightarrow> phi a) inp; liftAll (\<lambda>a. qGoodAbs a \<longrightarrow> phiAbs a) binp\<rbrakk> \<Longrightarrow> qGood (qOp delta inp binp) \<longrightarrow> phi (qOp delta inp binp)
 4. \<And>xs x X. (\<And>Y. (X, Y) \<in> {(X, Y). qGood X \<and> (X, Y) \<in> rel} \<Longrightarrow> qGood Y \<longrightarrow> phi Y) \<Longrightarrow> qGoodAbs (qAbs xs x X) \<longrightarrow> phiAbs (qAbs xs x X)
[PROOF STEP]
by (simp_all add: liftAll_def)