[STATEMENT]
lemma bs_boxed_var:
  assumes "boxed_i \<Theta> \<Gamma> b' bv i i'"
  shows "Some (b,c) = lookup \<Gamma> x \<Longrightarrow> Some s = i x \<Longrightarrow> Some s' = i' x \<Longrightarrow> boxed_b \<Theta> s b bv b' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some (b, c) = lookup \<Gamma> x; Some s = i x; Some s' = i' x\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'

goal (1 subgoal):
 1. \<lbrakk>Some (b, c) = lookup \<Gamma> x; Some s = i x; Some s' = i' x\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
proof(induct rule: boxed_i.inducts)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Theta> ba bv i. \<lbrakk>Some (b, c) = lookup GNil x; Some s = i x; Some s' = i x\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= ba ] \<setminus> s'
 2. \<And>sa i xa \<Theta> ba bv b' s'a \<Gamma> i' ca. \<lbrakk>Some sa = i xa;  \<Theta>  \<turnstile> sa ~ ba [ bv ::= b' ] \<setminus> s'a ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; \<lbrakk>Some (b, c) = lookup \<Gamma> x; Some s = i x; Some s' = i' x\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; Some (b, c) = lookup ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>) x; Some s = i x; Some s' = (i'(xa \<mapsto> s'a)) x\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
case (boxed_i_GNilI T i)
[PROOF STATE]
proof (state)
this:
Some (b, c) = lookup GNil x
Some s = i_ x
Some s' = i_ x

goal (2 subgoals):
 1. \<And>\<Theta> ba bv i. \<lbrakk>Some (b, c) = lookup GNil x; Some s = i x; Some s' = i x\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= ba ] \<setminus> s'
 2. \<And>sa i xa \<Theta> ba bv b' s'a \<Gamma> i' ca. \<lbrakk>Some sa = i xa;  \<Theta>  \<turnstile> sa ~ ba [ bv ::= b' ] \<setminus> s'a ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; \<lbrakk>Some (b, c) = lookup \<Gamma> x; Some s = i x; Some s' = i' x\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; Some (b, c) = lookup ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>) x; Some s = i x; Some s' = (i'(xa \<mapsto> s'a)) x\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Some (b, c) = lookup GNil x
Some s = i_ x
Some s' = i_ x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Some (b, c) = lookup GNil x
Some s = i_ x
Some s' = i_ x

goal (1 subgoal):
 1.  T  \<turnstile> s ~ b [ bv_ ::= i ] \<setminus> s'
[PROOF STEP]
using lookup.simps
[PROOF STATE]
proof (prove)
using this:
Some (b, c) = lookup GNil x
Some s = i_ x
Some s' = i_ x
lookup GNil ?x = None
lookup ((?x, ?b, ?c) #\<^sub>\<Gamma> ?G) ?y = (if ?x = ?y then Some (?b, ?c) else lookup ?G ?y)

goal (1 subgoal):
 1.  T  \<turnstile> s ~ b [ bv_ ::= i ] \<setminus> s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 T  \<turnstile> s ~ b [ bv_ ::= i ] \<setminus> s'

goal (1 subgoal):
 1. \<And>sa i xa \<Theta> ba bv b' s'a \<Gamma> i' ca. \<lbrakk>Some sa = i xa;  \<Theta>  \<turnstile> sa ~ ba [ bv ::= b' ] \<setminus> s'a ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; \<lbrakk>Some (b, c) = lookup \<Gamma> x; Some s = i x; Some s' = i' x\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; Some (b, c) = lookup ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>) x; Some s = i x; Some s' = (i'(xa \<mapsto> s'a)) x\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>sa i xa \<Theta> ba bv b' s'a \<Gamma> i' ca. \<lbrakk>Some sa = i xa;  \<Theta>  \<turnstile> sa ~ ba [ bv ::= b' ] \<setminus> s'a ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; \<lbrakk>Some (b, c) = lookup \<Gamma> x; Some s = i x; Some s' = i' x\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; Some (b, c) = lookup ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>) x; Some s = i x; Some s' = (i'(xa \<mapsto> s'a)) x\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
case (boxed_i_GConsI s i x1 \<Theta> b1 bv b' s'  \<Gamma> i' c)
[PROOF STATE]
proof (state)
this:
Some s = i x1
 \<Theta>  \<turnstile> s ~ b1 [ bv ::= b' ] \<setminus> s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
\<lbrakk>Some (b, c) = lookup \<Gamma> x; Some s = i x; Some s' = i' x\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
Some (b, c) = lookup ((x1, b1, c) #\<^sub>\<Gamma> \<Gamma>) x
Some s = i x
Some s' = (i'(x1 \<mapsto> s')) x

goal (1 subgoal):
 1. \<And>sa i xa \<Theta> ba bv b' s'a \<Gamma> i' ca. \<lbrakk>Some sa = i xa;  \<Theta>  \<turnstile> sa ~ ba [ bv ::= b' ] \<setminus> s'a ;  \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'; \<lbrakk>Some (b, c) = lookup \<Gamma> x; Some s = i x; Some s' = i' x\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s' ; Some (b, c) = lookup ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>) x; Some s = i x; Some s' = (i'(xa \<mapsto> s'a)) x\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
proof (cases "x=x1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = x1 \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. x \<noteq> x1 \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = x1

goal (2 subgoals):
 1. x = x1 \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
 2. x \<noteq> x1 \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = x1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = x1

goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
using boxed_i_GConsI
        fun_upd_same lookup.simps(2) option.inject prod.inject
[PROOF STATE]
proof (prove)
using this:
x = x1
Some s = i x1
 \<Theta>  \<turnstile> s ~ b1 [ bv ::= b' ] \<setminus> s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
\<lbrakk>Some (b, c) = lookup \<Gamma> x; Some s = i x; Some s' = i' x\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
Some (b, c) = lookup ((x1, b1, c) #\<^sub>\<Gamma> \<Gamma>) x
Some s = i x
Some s' = (i'(x1 \<mapsto> s')) x
(?f(?x := ?y)) ?x = ?y
lookup ((?x, ?b, ?c) #\<^sub>\<Gamma> ?G) ?y = (if ?x = ?y then Some (?b, ?c) else lookup ?G ?y)
(Some ?x2.0 = Some ?y2.0) = (?x2.0 = ?y2.0)
((?x1.0, ?x2.0) = (?y1.0, ?y2.0)) = (?x1.0 = ?y1.0 \<and> ?x2.0 = ?y2.0)

goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
 \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'

goal (1 subgoal):
 1. x \<noteq> x1 \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> x1 \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> x1

goal (1 subgoal):
 1. x \<noteq> x1 \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> x1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<noteq> x1

goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
using boxed_i_GConsI
        fun_upd_same lookup.simps option.inject prod.inject
[PROOF STATE]
proof (prove)
using this:
x \<noteq> x1
Some s = i x1
 \<Theta>  \<turnstile> s ~ b1 [ bv ::= b' ] \<setminus> s'
 \<Theta>  ; \<Gamma> ; b' , bv \<turnstile> i \<approx> i'
\<lbrakk>Some (b, c) = lookup \<Gamma> x; Some s = i x; Some s' = i' x\<rbrakk> \<Longrightarrow>  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
Some (b, c) = lookup ((x1, b1, c) #\<^sub>\<Gamma> \<Gamma>) x
Some s = i x
Some s' = (i'(x1 \<mapsto> s')) x
(?f(?x := ?y)) ?x = ?y
lookup GNil ?x = None
lookup ((?x, ?b, ?c) #\<^sub>\<Gamma> ?G) ?y = (if ?x = ?y then Some (?b, ?c) else lookup ?G ?y)
(Some ?x2.0 = Some ?y2.0) = (?x2.0 = ?y2.0)
((?x1.0, ?x2.0) = (?y1.0, ?y2.0)) = (?x1.0 = ?y1.0 \<and> ?x2.0 = ?y2.0)

goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
 \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
 \<Theta>  \<turnstile> s ~ b [ bv ::= b' ] \<setminus> s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eval_l_boxed_b:
  assumes  "\<lbrakk> l \<rbrakk> = s"
  shows   "boxed_b \<Theta> s (base_for_lit l) bv b' s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s ~ base_for_lit l [ bv ::= b' ] \<setminus> s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk> l \<rbrakk>  = s

goal (1 subgoal):
 1.  \<Theta>  \<turnstile> s ~ base_for_lit l [ bv ::= b' ] \<setminus> s
[PROOF STEP]
proof(nominal_induct l arbitrary: s  rule:l.strong_induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x s. \<lbrakk> L_num x \<rbrakk>  = s \<Longrightarrow>  \<Theta>  \<turnstile> s ~ base_for_lit (L_num x) [ bv ::= b' ] \<setminus> s
 2. \<And>s. \<lbrakk> L_true \<rbrakk>  = s \<Longrightarrow>  \<Theta>  \<turnstile> s ~ base_for_lit L_true [ bv ::= b' ] \<setminus> s
 3. \<And>s. \<lbrakk> L_false \<rbrakk>  = s \<Longrightarrow>  \<Theta>  \<turnstile> s ~ base_for_lit L_false [ bv ::= b' ] \<setminus> s
 4. \<And>s. \<lbrakk> L_unit \<rbrakk>  = s \<Longrightarrow>  \<Theta>  \<turnstile> s ~ base_for_lit L_unit [ bv ::= b' ] \<setminus> s
 5. \<And>x s. \<lbrakk> L_bitvec x \<rbrakk>  = s \<Longrightarrow>  \<Theta>  \<turnstile> s ~ base_for_lit (L_bitvec x) [ bv ::= b' ] \<setminus> s
[PROOF STEP]
qed(auto simp add:  boxed_b.intros wfRCV.intros )+