[STATEMENT]
lemma eval_v_weakening_x:
  fixes c::v
  assumes  "i' \<lbrakk> c \<rbrakk> ~ s" and "atom x \<sharp> c" and "i = i' (x \<mapsto> s')"
  shows "i \<lbrakk> c \<rbrakk> ~ s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<lbrakk> c \<rbrakk> ~ s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i' \<lbrakk> c \<rbrakk> ~ s
atom x \<sharp> c
i = i'(x \<mapsto> s')

goal (1 subgoal):
 1. i \<lbrakk> c \<rbrakk> ~ s
[PROOF STEP]
proof(induct rule: eval_v.induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>ia l. \<lbrakk>atom x \<sharp> [ l ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ \<lbrakk> l \<rbrakk>
 2. \<And>sv ia xa. \<lbrakk>Some sv = ia xa; atom x \<sharp> [ xa ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ sv
 3. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2
 4. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s
 5. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
case (eval_v_litI i l)
[PROOF STATE]
proof (state)
this:
atom x \<sharp> [ l ]\<^sup>v
i = i(x \<mapsto> s')

goal (5 subgoals):
 1. \<And>ia l. \<lbrakk>atom x \<sharp> [ l ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ \<lbrakk> l \<rbrakk>
 2. \<And>sv ia xa. \<lbrakk>Some sv = ia xa; atom x \<sharp> [ xa ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ sv
 3. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2
 4. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s
 5. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atom x \<sharp> [ l ]\<^sup>v
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> [ l ]\<^sup>v
i = i(x \<mapsto> s')

goal (1 subgoal):
 1. i \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ \<lbrakk> l \<rbrakk>
[PROOF STEP]
using eval_v.intros
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> [ l ]\<^sup>v
i = i(x \<mapsto> s')
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>
Some ?sv = ?i ?x \<Longrightarrow> ?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ SPair ?s1.0 ?s2.0
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ SCons ?tyid ?dc ?s
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ SConsp ?tyid ?dc ?b ?s

goal (1 subgoal):
 1. i \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ \<lbrakk> l \<rbrakk>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ l ]\<^sup>v \<rbrakk> ~ \<lbrakk> l \<rbrakk>

goal (4 subgoals):
 1. \<And>sv ia xa. \<lbrakk>Some sv = ia xa; atom x \<sharp> [ xa ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ sv
 2. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2
 3. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s
 4. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>sv ia xa. \<lbrakk>Some sv = ia xa; atom x \<sharp> [ xa ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ sv
 2. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2
 3. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s
 4. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
case (eval_v_varI sv i1 x1)
[PROOF STATE]
proof (state)
this:
Some sv = i1 x1
atom x \<sharp> [ x1 ]\<^sup>v
i = i1(x \<mapsto> s')

goal (4 subgoals):
 1. \<And>sv ia xa. \<lbrakk>Some sv = ia xa; atom x \<sharp> [ xa ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ sv
 2. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2
 3. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s
 4. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
hence "x \<noteq> x1"
[PROOF STATE]
proof (prove)
using this:
Some sv = i1 x1
atom x \<sharp> [ x1 ]\<^sup>v
i = i1(x \<mapsto> s')

goal (1 subgoal):
 1. x \<noteq> x1
[PROOF STEP]
using v.fresh fresh_at_base
[PROOF STATE]
proof (prove)
using this:
Some sv = i1 x1
atom x \<sharp> [ x1 ]\<^sup>v
i = i1(x \<mapsto> s')
?a \<sharp> [ ?l ]\<^sup>v = ?a \<sharp> ?l
?a \<sharp> [ ?x ]\<^sup>v = ?a \<sharp> ?x
?a \<sharp> [ ?v1.0 , ?v2.0 ]\<^sup>v = (?a \<sharp> ?v1.0 \<and> ?a \<sharp> ?v2.0)
?a \<sharp> V_cons ?list1.0 ?list2.0 ?v = (?a \<sharp> ?list1.0 \<and> ?a \<sharp> ?list2.0 \<and> ?a \<sharp> ?v)
?a \<sharp> V_consp ?list1.0 ?list2.0 ?b ?v = (?a \<sharp> ?list1.0 \<and> ?a \<sharp> ?list2.0 \<and> ?a \<sharp> ?b \<and> ?a \<sharp> ?v)
sort_of ?a \<noteq> sort_of (atom ?b) \<Longrightarrow> ?a \<sharp> ?b
?a \<sharp> ?b = (?a \<noteq> atom ?b)

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

goal (4 subgoals):
 1. \<And>sv ia xa. \<lbrakk>Some sv = ia xa; atom x \<sharp> [ xa ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ sv
 2. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2
 3. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s
 4. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
hence "i x1 = Some sv"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> x1

goal (1 subgoal):
 1. i x1 = Some sv
[PROOF STEP]
using eval_v_varI
[PROOF STATE]
proof (prove)
using this:
x \<noteq> x1
Some sv = i1 x1
atom x \<sharp> [ x1 ]\<^sup>v
i = i1(x \<mapsto> s')

goal (1 subgoal):
 1. i x1 = Some sv
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i x1 = Some sv

goal (4 subgoals):
 1. \<And>sv ia xa. \<lbrakk>Some sv = ia xa; atom x \<sharp> [ xa ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ sv
 2. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2
 3. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s
 4. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i x1 = Some sv
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i x1 = Some sv

goal (1 subgoal):
 1. i \<lbrakk> [ x1 ]\<^sup>v \<rbrakk> ~ sv
[PROOF STEP]
using eval_v.intros
[PROOF STATE]
proof (prove)
using this:
i x1 = Some sv
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>
Some ?sv = ?i ?x \<Longrightarrow> ?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ SPair ?s1.0 ?s2.0
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ SCons ?tyid ?dc ?s
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ SConsp ?tyid ?dc ?b ?s

goal (1 subgoal):
 1. i \<lbrakk> [ x1 ]\<^sup>v \<rbrakk> ~ sv
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ x1 ]\<^sup>v \<rbrakk> ~ sv

goal (3 subgoals):
 1. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2
 2. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s
 3. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2
 2. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s
 3. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
case (eval_v_pairI i v1 s1 v2 s2)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1 \<rbrakk> ~ s1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1
i \<lbrakk> v2 \<rbrakk> ~ s2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2
atom x \<sharp> [ v1 , v2 ]\<^sup>v
i = i(x \<mapsto> s')

goal (3 subgoals):
 1. \<And>ia v1 s1 v2 s2. \<lbrakk>ia \<lbrakk> v1 \<rbrakk> ~ s1 ; \<lbrakk>atom x \<sharp> v1; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1 ; ia \<lbrakk> v2 \<rbrakk> ~ s2 ; \<lbrakk>atom x \<sharp> v2; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2 ; atom x \<sharp> [ v1 , v2 ]\<^sup>v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2
 2. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s
 3. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v1 \<rbrakk> ~ s1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1
i \<lbrakk> v2 \<rbrakk> ~ s2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2
atom x \<sharp> [ v1 , v2 ]\<^sup>v
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1
i \<lbrakk> v2 \<rbrakk> ~ s2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2
atom x \<sharp> [ v1 , v2 ]\<^sup>v
i = i(x \<mapsto> s')

goal (1 subgoal):
 1. i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2
[PROOF STEP]
using eval_v.intros
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1 \<rbrakk> ~ s1
\<lbrakk>atom x \<sharp> v1; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v1 \<rbrakk> ~ s1
i \<lbrakk> v2 \<rbrakk> ~ s2
\<lbrakk>atom x \<sharp> v2; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v2 \<rbrakk> ~ s2
atom x \<sharp> [ v1 , v2 ]\<^sup>v
i = i(x \<mapsto> s')
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>
Some ?sv = ?i ?x \<Longrightarrow> ?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ SPair ?s1.0 ?s2.0
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ SCons ?tyid ?dc ?s
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ SConsp ?tyid ?dc ?b ?s

goal (1 subgoal):
 1. i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ SPair s1 s2

goal (2 subgoals):
 1. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s
 2. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s
 2. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
case (eval_v_consI i v s tyid dc)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ s
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s
atom x \<sharp> V_cons tyid dc v
i = i(x \<mapsto> s')

goal (2 subgoals):
 1. \<And>ia v s tyid dc. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_cons tyid dc v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s
 2. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v \<rbrakk> ~ s
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s
atom x \<sharp> V_cons tyid dc v
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s
atom x \<sharp> V_cons tyid dc v
i = i(x \<mapsto> s')

goal (1 subgoal):
 1. i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s
[PROOF STEP]
using eval_v.intros
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s
atom x \<sharp> V_cons tyid dc v
i = i(x \<mapsto> s')
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>
Some ?sv = ?i ?x \<Longrightarrow> ?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ SPair ?s1.0 ?s2.0
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ SCons ?tyid ?dc ?s
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ SConsp ?tyid ?dc ?b ?s

goal (1 subgoal):
 1. i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> V_cons tyid dc v \<rbrakk> ~ SCons tyid dc s

goal (1 subgoal):
 1. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
case (eval_v_conspI i v s tyid dc b)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ s
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s
atom x \<sharp> V_consp tyid dc b v
i = i(x \<mapsto> s')

goal (1 subgoal):
 1. \<And>ia v s tyid dc b. \<lbrakk>ia \<lbrakk> v \<rbrakk> ~ s ; \<lbrakk>atom x \<sharp> v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s ; atom x \<sharp> V_consp tyid dc b v; i = ia(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v \<rbrakk> ~ s
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s
atom x \<sharp> V_consp tyid dc b v
i = i(x \<mapsto> s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s
atom x \<sharp> V_consp tyid dc b v
i = i(x \<mapsto> s')

goal (1 subgoal):
 1. i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
using eval_v.intros
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
\<lbrakk>atom x \<sharp> v; i = i(x \<mapsto> s')\<rbrakk> \<Longrightarrow> i \<lbrakk> v \<rbrakk> ~ s
atom x \<sharp> V_consp tyid dc b v
i = i(x \<mapsto> s')
?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ \<lbrakk> ?l \<rbrakk>
Some ?sv = ?i ?x \<Longrightarrow> ?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ SPair ?s1.0 ?s2.0
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ SCons ?tyid ?dc ?s
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ SConsp ?tyid ?dc ?b ?s

goal (1 subgoal):
 1. i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<lbrakk> V_consp tyid dc b v \<rbrakk> ~ SConsp tyid dc b s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma op_ntsmcf_components[smc_op_simps]:
  shows "op_ntsmcf \<NN>\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>"
    and "op_ntsmcf \<NN>\<lparr>NTDom\<rparr> = op_smcf (\<NN>\<lparr>NTCod\<rparr>)"
    and "op_ntsmcf \<NN>\<lparr>NTCod\<rparr> = op_smcf (\<NN>\<lparr>NTDom\<rparr>)"
    and "op_ntsmcf \<NN>\<lparr>NTDGDom\<rparr> = op_smc (\<NN>\<lparr>NTDGDom\<rparr>)"
    and "op_ntsmcf \<NN>\<lparr>NTDGCod\<rparr> = op_smc (\<NN>\<lparr>NTDGCod\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (op_ntsmcf \<NN>\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr> &&& op_ntsmcf \<NN>\<lparr>NTDom\<rparr> = op_smcf (\<NN>\<lparr>NTCod\<rparr>)) &&& op_ntsmcf \<NN>\<lparr>NTCod\<rparr> = op_smcf (\<NN>\<lparr>NTDom\<rparr>) &&& op_ntsmcf \<NN>\<lparr>NTDGDom\<rparr> = op_smc (\<NN>\<lparr>NTDGDom\<rparr>) &&& op_ntsmcf \<NN>\<lparr>NTDGCod\<rparr> = op_smc (\<NN>\<lparr>NTDGCod\<rparr>)
[PROOF STEP]
unfolding op_ntsmcf_def nt_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, op_smcf (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), op_smcf (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = \<NN>\<lparr>[]\<^sub>\<circ>\<rparr> &&& [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, op_smcf (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), op_smcf (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = op_smcf (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>)) &&& [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, op_smcf (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), op_smcf (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = op_smcf (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>) &&& [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, op_smcf (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), op_smcf (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = op_smc (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>) &&& [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, op_smcf (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), op_smcf (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), op_smc (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr> = op_smc (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)
[PROOF STEP]
by (auto simp: nat_omega_simps)


[STATEMENT]
lemma two_step_less_D:
  "0 < two_step r \<Longrightarrow> two_step r = Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < two_step r \<Longrightarrow> two_step r = Suc 0
[PROOF STEP]
by(auto simp add: two_step_def)


[STATEMENT]
lemma even_card':
  assumes "even(card A)" "x\<in>A"
  shows "\<exists>y\<in>A. y\<noteq>x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>A. y \<noteq> x
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>y\<in>A. y \<noteq> x) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (\<exists>y\<in>A. y \<noteq> x)"
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>y\<in>A. y \<noteq> x)

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>A. y \<noteq> x) \<Longrightarrow> False
[PROOF STEP]
hence "\<forall>y\<in>A. y=x"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>y\<in>A. y \<noteq> x)

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

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>A. y \<noteq> x) \<Longrightarrow> False
[PROOF STEP]
hence "A={x}"
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>A. y = x

goal (1 subgoal):
 1. A = {x}
[PROOF STEP]
by (metis all_not_in_conv assms(2) insertI2 mk_disjoint_insert)
[PROOF STATE]
proof (state)
this:
A = {x}

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>A. y \<noteq> x) \<Longrightarrow> False
[PROOF STEP]
hence "card(A)=1"
[PROOF STATE]
proof (prove)
using this:
A = {x}

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

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>A. y \<noteq> x) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
card A = 1

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>even(card A)\<close>
[PROOF STATE]
proof (prove)
using this:
card A = 1
even (card A)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proper_it'I:
    "\<lbrakk>\<And>s. proper_it (it s) (it' s)\<rbrakk> \<Longrightarrow> proper_it' it it'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. proper_it (it s) (it' s)) \<Longrightarrow> proper_it' it it'
[PROOF STEP]
unfolding proper_it'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. proper_it (it s) (it' s)) \<Longrightarrow> \<forall>s. proper_it (it s) (it' s)
[PROOF STEP]
by blast


[STATEMENT]
lemma vec_tensor_prod_2_bis [simp]:
  assumes "v \<in> state_qbit 1" and "w \<in> state_qbit 1"
  shows "v \<otimes> w = Matrix.vec 4 (\<lambda>i. if i = 0 then v $ 0 * w $ 0 else
                                      if i = 3 then v $ 1 * w $ 1 else
                                          if i = 1 then v $ 0 * w $ 1 else v $ 1 * w $ 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<otimes> w = Matrix.vec 4 (\<lambda>i. if i = 0 then v $ 0 * w $ 0 else if i = 3 then v $ 1 * w $ 1 else if i = 1 then v $ 0 * w $ 1 else v $ 1 * w $ 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < dim_vec (Matrix.vec 4 (\<lambda>i. if i = 0 then v $ 0 * w $ 0 else if i = 3 then v $ 1 * w $ 1 else if i = 1 then v $ 0 * w $ 1 else v $ 1 * w $ 0)) \<Longrightarrow> (v \<otimes> w) $ i = Matrix.vec 4 (\<lambda>i. if i = 0 then v $ 0 * w $ 0 else if i = 3 then v $ 1 * w $ 1 else if i = 1 then v $ 0 * w $ 1 else v $ 1 * w $ 0) $ i
 2. dim_vec (v \<otimes> w) = dim_vec (Matrix.vec 4 (\<lambda>i. if i = 0 then v $ 0 * w $ 0 else if i = 3 then v $ 1 * w $ 1 else if i = 1 then v $ 0 * w $ 1 else v $ 1 * w $ 0))
[PROOF STEP]
define u where "u = Matrix.vec 4 (\<lambda>i. if i = 0 then v $ 0 * w $ 0 else
                                          if i = 3 then v $ 1 * w $ 1 else
                                            if i = 1 then v $ 0 * w $ 1 else v $ 1 * w $ 0)"
[PROOF STATE]
proof (state)
this:
u = Matrix.vec 4 (\<lambda>i. if i = 0 then v $ 0 * w $ 0 else if i = 3 then v $ 1 * w $ 1 else if i = 1 then v $ 0 * w $ 1 else v $ 1 * w $ 0)

goal (2 subgoals):
 1. \<And>i. i < dim_vec (Matrix.vec 4 (\<lambda>i. if i = 0 then v $ 0 * w $ 0 else if i = 3 then v $ 1 * w $ 1 else if i = 1 then v $ 0 * w $ 1 else v $ 1 * w $ 0)) \<Longrightarrow> (v \<otimes> w) $ i = Matrix.vec 4 (\<lambda>i. if i = 0 then v $ 0 * w $ 0 else if i = 3 then v $ 1 * w $ 1 else if i = 1 then v $ 0 * w $ 1 else v $ 1 * w $ 0) $ i
 2. dim_vec (v \<otimes> w) = dim_vec (Matrix.vec 4 (\<lambda>i. if i = 0 then v $ 0 * w $ 0 else if i = 3 then v $ 1 * w $ 1 else if i = 1 then v $ 0 * w $ 1 else v $ 1 * w $ 0))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u = Matrix.vec 4 (\<lambda>i. if i = 0 then v $ 0 * w $ 0 else if i = 3 then v $ 1 * w $ 1 else if i = 1 then v $ 0 * w $ 1 else v $ 1 * w $ 0)
[PROOF STEP]
show f2:"dim_vec (v \<otimes> w) = dim_vec u"
[PROOF STATE]
proof (prove)
using this:
u = Matrix.vec 4 (\<lambda>i. if i = 0 then v $ 0 * w $ 0 else if i = 3 then v $ 1 * w $ 1 else if i = 1 then v $ 0 * w $ 1 else v $ 1 * w $ 0)

goal (1 subgoal):
 1. dim_vec (v \<otimes> w) = dim_vec u
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u = Matrix.vec 4 (\<lambda>i. if i = 0 then v $ 0 * w $ 0 else if i = 3 then v $ 1 * w $ 1 else if i = 1 then v $ 0 * w $ 1 else v $ 1 * w $ 0)
v \<in> state_qbit 1
w \<in> state_qbit 1

goal (1 subgoal):
 1. dim_vec (v \<otimes> w) = dim_vec u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_vec (v \<otimes> w) = dim_vec u

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.vec 4 (\<lambda>i. if i = 0 then v $ 0 * w $ 0 else if i = 3 then v $ 1 * w $ 1 else if i = 1 then v $ 0 * w $ 1 else v $ 1 * w $ 0)) \<Longrightarrow> (v \<otimes> w) $ i = Matrix.vec 4 (\<lambda>i. if i = 0 then v $ 0 * w $ 0 else if i = 3 then v $ 1 * w $ 1 else if i = 1 then v $ 0 * w $ 1 else v $ 1 * w $ 0) $ i
[PROOF STEP]
show "\<And>i. i < dim_vec u \<Longrightarrow> (v \<otimes> w) $ i = u $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < dim_vec u \<Longrightarrow> (v \<otimes> w) $ i = u $ i
[PROOF STEP]
apply (auto simp: u_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (v \<otimes> w) $ Suc 0 = v $ 0 * w $ Suc 0
 2. (v \<otimes> w) $ 3 = v $ Suc 0 * w $ Suc 0
 3. (v \<otimes> w) $ 0 = v $ 0 * w $ 0
 4. \<And>i. \<lbrakk>i < 4; i \<noteq> Suc 0; i \<noteq> 3; 0 < i\<rbrakk> \<Longrightarrow> (v \<otimes> w) $ i = v $ Suc 0 * w $ 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v \<in> state_qbit 1
w \<in> state_qbit 1

goal (4 subgoals):
 1. (v \<otimes> w) $ Suc 0 = v $ 0 * w $ Suc 0
 2. (v \<otimes> w) $ 3 = v $ Suc 0 * w $ Suc 0
 3. (v \<otimes> w) $ 0 = v $ 0 * w $ 0
 4. \<And>i. \<lbrakk>i < 4; i \<noteq> Suc 0; i \<noteq> 3; 0 < i\<rbrakk> \<Longrightarrow> (v \<otimes> w) $ i = v $ Suc 0 * w $ 0
[PROOF STEP]
apply auto[3]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa A Aa. \<lbrakk>v = module.lincomb (module_cpx_vec 2) a A; w = module.lincomb (module_cpx_vec 2) aa Aa; finite A; finite Aa; A \<subseteq> unit_vectors 2; \<parallel>module.lincomb (module_cpx_vec 2) a A\<parallel> = 1; Aa \<subseteq> unit_vectors 2; \<parallel>module.lincomb (module_cpx_vec 2) aa Aa\<parallel> = 1\<rbrakk> \<Longrightarrow> vCons (module.lincomb (module_cpx_vec 2) a A $ 0 * module.lincomb (module_cpx_vec 2) aa Aa $ 0) (vCons (module.lincomb (module_cpx_vec 2) a A $ 0 * module.lincomb (module_cpx_vec 2) aa Aa $ Suc 0) (vCons (module.lincomb (module_cpx_vec 2) a A $ Suc 0 * module.lincomb (module_cpx_vec 2) aa Aa $ 0) (vCons (module.lincomb (module_cpx_vec 2) a A $ Suc 0 * module.lincomb (module_cpx_vec 2) aa Aa $ Suc 0) vNil))) $ 3 = module.lincomb (module_cpx_vec 2) a A $ Suc 0 * module.lincomb (module_cpx_vec 2) aa Aa $ Suc 0
 2. \<And>i. \<lbrakk>i < 4; i \<noteq> Suc 0; i \<noteq> 3; 0 < i\<rbrakk> \<Longrightarrow> (v \<otimes> w) $ i = v $ Suc 0 * w $ 0
[PROOF STEP]
apply (simp add: numeral_3_eq_3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < 4; i \<noteq> Suc 0; i \<noteq> 3; 0 < i\<rbrakk> \<Longrightarrow> (v \<otimes> w) $ i = v $ Suc 0 * w $ 0
[PROOF STEP]
using u_def vec_of_list_index vec_tensor_prod_2 index_is_2
[PROOF STATE]
proof (prove)
using this:
u = Matrix.vec 4 (\<lambda>i. if i = 0 then v $ 0 * w $ 0 else if i = 3 then v $ 1 * w $ 1 else if i = 1 then v $ 0 * w $ 1 else v $ 1 * w $ 0)
vec_of_list ?xs $ ?j = ?xs ! ?j
\<lbrakk>?v \<in> state_qbit 1; ?w \<in> state_qbit 1\<rbrakk> \<Longrightarrow> ?v \<otimes> ?w = vec_of_list [?v $ 0 * ?w $ 0, ?v $ 0 * ?w $ 1, ?v $ 1 * ?w $ 0, ?v $ 1 * ?w $ 1]
\<forall>i. i \<noteq> Suc 0 \<longrightarrow> i \<noteq> 3 \<longrightarrow> 0 < i \<longrightarrow> i < 4 \<longrightarrow> i = 2

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < 4; i \<noteq> Suc 0; i \<noteq> 3; 0 < i\<rbrakk> \<Longrightarrow> (v \<otimes> w) $ i = v $ Suc 0 * w $ 0
[PROOF STEP]
by (metis (no_types, lifting) One_nat_def assms nth_Cons_0 nth_Cons_Suc numeral_2_eq_2)
[PROOF STATE]
proof (state)
this:
?i < dim_vec u \<Longrightarrow> (v \<otimes> w) $ ?i = u $ ?i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dim_row_of_one_mat_less_pow:
  assumes "gate m G1" and "gate n G2" and "i < dim_row (1\<^sub>m(dim_col G1 * dim_col G2))"
  shows "i < 2^(m+n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < 2 ^ (m + n)
[PROOF STEP]
using assms gate_def
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
gate ?n ?A \<equiv> dim_row ?A = 2 ^ ?n \<and> square_mat ?A \<and> unitary ?A

goal (1 subgoal):
 1. i < 2 ^ (m + n)
[PROOF STEP]
by (simp add: power_add)


[STATEMENT]
lemma (in is_tdghm) is_tdghm_op'[dg_op_intros]:
  assumes "\<GG>' = op_dghm \<GG>"
    and "\<FF>' = op_dghm \<FF>"
    and "\<AA>' = op_dg \<AA>"
    and "\<BB>' = op_dg \<BB>"
  shows "op_tdghm \<NN> : \<GG>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>' : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_tdghm \<NN> : \<GG>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>' : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_tdghm \<NN> : op_dghm \<GG> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg \<BB>
[PROOF STEP]
by (rule is_tdghm_op)


[STATEMENT]
lemma word_eq_rbl_eq: "x = y \<longleftrightarrow> rev (to_bl x) = rev (to_bl y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x = y) = (rev (to_bl x) = rev (to_bl y))
[PROOF STEP]
by simp


[STATEMENT]
lemma shiftr1_bl:
  \<open>shiftr1 w = of_bl (butlast (to_bl w))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shiftr1 w = of_bl (butlast (to_bl w))
[PROOF STEP]
proof (rule bit_word_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
assume \<open>n < LENGTH('a)\<close>
[PROOF STATE]
proof (state)
this:
n < LENGTH('a)

goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
show \<open>bit (shiftr1 w) n \<longleftrightarrow> bit (of_bl (butlast (to_bl w)) :: 'a word) n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
proof (cases \<open>n = LENGTH('a) - 1\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
 2. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = LENGTH('a) - 1

goal (2 subgoals):
 1. n = LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
 2. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = LENGTH('a) - 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = LENGTH('a) - 1

goal (1 subgoal):
 1. bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
by (simp add: bit_shiftr1_iff bit_of_bl_iff)
[PROOF STATE]
proof (state)
this:
bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n

goal (1 subgoal):
 1. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> LENGTH('a) - 1

goal (1 subgoal):
 1. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
with \<open>n < LENGTH('a)\<close>
[PROOF STATE]
proof (chain)
picking this:
n < LENGTH('a)
n \<noteq> LENGTH('a) - 1
[PROOF STEP]
have \<open>n < LENGTH('a) - 1\<close>
[PROOF STATE]
proof (prove)
using this:
n < LENGTH('a)
n \<noteq> LENGTH('a) - 1

goal (1 subgoal):
 1. n < LENGTH('a) - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n < LENGTH('a) - 1

goal (1 subgoal):
 1. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
with \<open>n < LENGTH('a)\<close>
[PROOF STATE]
proof (chain)
picking this:
n < LENGTH('a)
n < LENGTH('a) - 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n < LENGTH('a)
n < LENGTH('a) - 1

goal (1 subgoal):
 1. bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
by (simp add: bit_shiftr1_iff bit_of_bl_iff rev_nth nth_butlast
        word_size to_bl_nth)
[PROOF STATE]
proof (state)
this:
bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f_carrier[dest]: "i < m \<Longrightarrow> fs ! i \<in> carrier_vec n"
  and fs_carrier [simp]: "set fs \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i < length fs \<Longrightarrow> fs ! i \<in> carrier_vec n) &&& set fs \<subseteq> carrier_vec n
[PROOF STEP]
using lin_indep gs.f_carrier gs.gso_carrier
[PROOF STATE]
proof (prove)
using this:
gs.lin_indpt_list (map of_int_hom.vec_hom fs)
?i < length (map of_int_hom.vec_hom fs) \<Longrightarrow> map of_int_hom.vec_hom fs ! ?i \<in> carrier_vec n
?i < length (map of_int_hom.vec_hom fs) \<Longrightarrow> gs.gso ?i \<in> carrier_vec n

goal (1 subgoal):
 1. (i < length fs \<Longrightarrow> fs ! i \<in> carrier_vec n) &&& set fs \<subseteq> carrier_vec n
[PROOF STEP]
unfolding gs.lin_indpt_list_def
[PROOF STATE]
proof (prove)
using this:
set (map of_int_hom.vec_hom fs) \<subseteq> carrier_vec n \<and> distinct (map of_int_hom.vec_hom fs) \<and> gs.lin_indpt (set (map of_int_hom.vec_hom fs))
?i < length (map of_int_hom.vec_hom fs) \<Longrightarrow> map of_int_hom.vec_hom fs ! ?i \<in> carrier_vec n
?i < length (map of_int_hom.vec_hom fs) \<Longrightarrow> gs.gso ?i \<in> carrier_vec n

goal (1 subgoal):
 1. (i < length fs \<Longrightarrow> fs ! i \<in> carrier_vec n) &&& set fs \<subseteq> carrier_vec n
[PROOF STEP]
by auto


[STATEMENT]
lemma cinner_basis_enum_of_vec:
  defines "n \<equiv> length (canonical_basis :: 'a::onb_enum list)"
  assumes [simp]: "dim_vec x = n" "dim_vec y = n"
  shows  "(basis_enum_of_vec x :: 'a) \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
have \<open>(basis_enum_of_vec x :: 'a) \<bullet>\<^sub>C basis_enum_of_vec y
    = (\<Sum>i<n. x$i *\<^sub>C canonical_basis ! i :: 'a) \<bullet>\<^sub>C (\<Sum>i<n. y$i *\<^sub>C canonical_basis ! i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = (\<Sum>i<n. x $ i *\<^sub>C canonical_basis ! i) \<bullet>\<^sub>C (\<Sum>i<n. y $ i *\<^sub>C canonical_basis ! i)
[PROOF STEP]
by (auto simp: basis_enum_of_vec_def sum_list_sum_nth atLeast0LessThan simp flip: n_def)
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = (\<Sum>i<n. x $ i *\<^sub>C canonical_basis ! i) \<bullet>\<^sub>C (\<Sum>i<n. y $ i *\<^sub>C canonical_basis ! i)

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = (\<Sum>i<n. x $ i *\<^sub>C canonical_basis ! i) \<bullet>\<^sub>C (\<Sum>i<n. y $ i *\<^sub>C canonical_basis ! i)

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
have \<open>\<dots> = (\<Sum>i<n. \<Sum>j<n. cnj (x$i) *\<^sub>C y$j *\<^sub>C ((canonical_basis ! i :: 'a) \<bullet>\<^sub>C (canonical_basis ! j)))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<n. x $ i *\<^sub>C canonical_basis ! i) \<bullet>\<^sub>C (\<Sum>i<n. y $ i *\<^sub>C canonical_basis ! i) = (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! i \<bullet>\<^sub>C canonical_basis ! j))
[PROOF STEP]
apply (subst cinner_sum_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>xa<n. x $ xa *\<^sub>C canonical_basis ! xa \<bullet>\<^sub>C (\<Sum>i<n. y $ i *\<^sub>C canonical_basis ! i)) = (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! i \<bullet>\<^sub>C canonical_basis ! j))
[PROOF STEP]
apply (subst cinner_sum_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>xa<n. \<Sum>ya<n. x $ xa *\<^sub>C canonical_basis ! xa \<bullet>\<^sub>C y $ ya *\<^sub>C canonical_basis ! ya) = (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! i \<bullet>\<^sub>C canonical_basis ! j))
[PROOF STEP]
by (auto simp: mult_ac)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. x $ i *\<^sub>C canonical_basis ! i) \<bullet>\<^sub>C (\<Sum>i<n. y $ i *\<^sub>C canonical_basis ! i) = (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! i \<bullet>\<^sub>C canonical_basis ! j))

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. x $ i *\<^sub>C canonical_basis ! i) \<bullet>\<^sub>C (\<Sum>i<n. y $ i *\<^sub>C canonical_basis ! i) = (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! i \<bullet>\<^sub>C canonical_basis ! j))

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
have \<open>\<dots> = (\<Sum>i<n. \<Sum>j<n. cnj (x$i) *\<^sub>C y$j *\<^sub>C (if i=j then 1 else 0))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! i \<bullet>\<^sub>C canonical_basis ! j)) = (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (if i = j then 1 else 0))
[PROOF STEP]
apply (rule sum.cong[OF refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {..<n} \<Longrightarrow> (\<Sum>j<n. cnj (x $ xa) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! xa \<bullet>\<^sub>C canonical_basis ! j)) = (\<Sum>j<n. cnj (x $ xa) *\<^sub>C y $ j *\<^sub>C (if xa = j then 1 else 0))
[PROOF STEP]
apply (rule sum.cong[OF refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa. \<lbrakk>xa \<in> {..<n}; xaa \<in> {..<n}\<rbrakk> \<Longrightarrow> cnj (x $ xa) *\<^sub>C y $ xaa *\<^sub>C (canonical_basis ! xa \<bullet>\<^sub>C canonical_basis ! xaa) = cnj (x $ xa) *\<^sub>C y $ xaa *\<^sub>C (if xa = xaa then 1 else 0)
[PROOF STEP]
by (auto simp: cinner_canonical_basis n_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! i \<bullet>\<^sub>C canonical_basis ! j)) = (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (if i = j then 1 else 0))

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! i \<bullet>\<^sub>C canonical_basis ! j)) = (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (if i = j then 1 else 0))

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
have \<open>\<dots> = (\<Sum>i<n. cnj (x$i) *\<^sub>C y$i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (if i = j then 1 else 0)) = (\<Sum>i<n. cnj (x $ i) *\<^sub>C y $ i)
[PROOF STEP]
apply (rule sum.cong[OF refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {..<n} \<Longrightarrow> (\<Sum>j<n. cnj (x $ xa) *\<^sub>C y $ j *\<^sub>C (if xa = j then 1 else 0)) = cnj (x $ xa) *\<^sub>C y $ xa
[PROOF STEP]
apply (subst sum_single)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> {..<n} \<Longrightarrow> finite {..<n}
 2. \<And>xa j. \<lbrakk>xa \<in> {..<n}; j \<noteq> ?i3 xa; j \<in> {..<n}\<rbrakk> \<Longrightarrow> cnj (x $ xa) *\<^sub>C y $ j *\<^sub>C (if xa = j then 1 else 0) = 0
 3. \<And>xa. xa \<in> {..<n} \<Longrightarrow> (if ?i3 xa \<in> {..<n} then cnj (x $ xa) *\<^sub>C y $ ?i3 xa *\<^sub>C (if xa = ?i3 xa then 1 else 0) else 0) = cnj (x $ xa) *\<^sub>C y $ xa
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (if i = j then 1 else 0)) = (\<Sum>i<n. cnj (x $ i) *\<^sub>C y $ i)

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (if i = j then 1 else 0)) = (\<Sum>i<n. cnj (x $ i) *\<^sub>C y $ i)

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
have \<open>\<dots> = y \<bullet>c x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<n. cnj (x $ i) *\<^sub>C y $ i) = y \<bullet>c x
[PROOF STEP]
by (smt (z3) assms(2) complex_scaleC_def conjugate_complex_def dim_vec_conjugate lessThan_atLeast0 lessThan_iff mult.commute scalar_prod_def sum.cong vec_index_conjugate)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. cnj (x $ i) *\<^sub>C y $ i) = y \<bullet>c x

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma imp_nfoldli_simps[simp,code]:
  "imp_nfoldli [] c f s = return s"
  "imp_nfoldli (x#ls) c f s = (do {
    b \<leftarrow> c s;
    if b then do {
      s'\<leftarrow>f x s;
      imp_nfoldli ls c f s'
    } else return s
  })"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_nfoldli [] c f s = return s &&& imp_nfoldli (x # ls) c f s = c s \<bind> (\<lambda>b. if b then f x s \<bind> imp_nfoldli ls c f else return s)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. imp_nfoldli [] c f s = return s
 2. imp_nfoldli (x # ls) c f s = c s \<bind> (\<lambda>b. if b then f x s \<bind> imp_nfoldli ls c f else return s)
[PROOF STEP]
unfolding imp_nfoldli_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) ([], s) = return s
 2. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (x # ls, s) = c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)
[PROOF STEP]
apply (subst heap.mono_body_fixp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. monotone heap.le_fun Heap_ord (\<lambda>fa. case x of ([], s) \<Rightarrow> return s | (x # ls, s) \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. fa (ls, s')) else return s))
 2. (case ([], s) of ([], s) \<Rightarrow> return s | (x # ls, s) \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)) = return s
 3. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (x # ls, s) = c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)
[PROOF STEP]
apply pf_mono
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (case ([], s) of ([], s) \<Rightarrow> return s | (x # ls, s) \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)) = return s
 2. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (x # ls, s) = c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (x # ls, s) = c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)
[PROOF STEP]
apply (subst heap.mono_body_fixp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. monotone heap.le_fun Heap_ord (\<lambda>fa. case x of ([], s) \<Rightarrow> return s | (x # ls, s) \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. fa (ls, s')) else return s))
 2. (case (x # ls, s) of ([], s) \<Rightarrow> return s | (x # ls, s) \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)) = c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)
[PROOF STEP]
apply pf_mono
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (x # ls, s) of ([], s) \<Rightarrow> return s | (x # ls, s) \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)) = c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_final_dstate_imp_not_weighted_RP: "is_final_dstate St \<Longrightarrow> \<not> wstate_of_dstate St \<leadsto>\<^sub>w St'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_final_dstate St \<Longrightarrow> \<not> wstate_of_dstate St \<leadsto>\<^sub>w St'
[PROOF STEP]
using wrp.final_weighted_RP
[PROOF STATE]
proof (prove)
using this:
\<not> ({#}, {#}, ?Q, ?n) \<leadsto>\<^sub>w ?St

goal (1 subgoal):
 1. is_final_dstate St \<Longrightarrow> \<not> wstate_of_dstate St \<leadsto>\<^sub>w St'
[PROOF STEP]
by (cases St) (auto intro: wrp.final_weighted_RP simp: is_final_dstate.simps)