[STATEMENT]
lemma reds_smaller_L: "\<lbrakk> \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z;
   set L' \<subseteq> set L
  \<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>L'\<^esub> \<Delta> : z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>L'\<^esub> \<Delta> : z
[PROOF STEP]
proof(nominal_induct avoiding : L' rule: reds.strong_induct)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>\<Gamma> x e L L'. set L' \<subseteq> set L \<Longrightarrow> \<Gamma> : Lam [x]. e \<Down>\<^bsub>L'\<^esub> \<Gamma> : Lam [x]. e
 2. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' L'. \<lbrakk>atom y \<sharp> L'; atom y \<sharp> \<Gamma>; atom y \<sharp> e; atom y \<sharp> x; atom y \<sharp> L; atom y \<sharp> \<Delta>; atom y \<sharp> \<Theta>; atom y \<sharp> z; \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>b\<^esub> \<Delta> : Lam [y]. e'; \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> : e'[y::=x] \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : App e x \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 3. \<And>\<Gamma> x e L \<Delta> z L'. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>b. set b \<subseteq> set (x # L) \<Longrightarrow> delete x \<Gamma> : e \<Down>\<^bsub>b\<^esub> \<Delta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Var x \<Down>\<^bsub>L'\<^esub> (x, z) # \<Delta> : z
 4. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 5. \<And>\<Gamma> b L L'. set L' \<subseteq> set L \<Longrightarrow> \<Gamma> : Bool b \<Down>\<^bsub>L'\<^esub> \<Gamma> : Bool b
 6. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z L'. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Gamma> : scrut \<Down>\<^bsub>ba\<^esub> \<Delta> : Bool b; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>ba\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
case (Lambda \<Gamma> x e L L')
[PROOF STATE]
proof (state)
this:
set L' \<subseteq> set L

goal (6 subgoals):
 1. \<And>\<Gamma> x e L L'. set L' \<subseteq> set L \<Longrightarrow> \<Gamma> : Lam [x]. e \<Down>\<^bsub>L'\<^esub> \<Gamma> : Lam [x]. e
 2. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' L'. \<lbrakk>atom y \<sharp> L'; atom y \<sharp> \<Gamma>; atom y \<sharp> e; atom y \<sharp> x; atom y \<sharp> L; atom y \<sharp> \<Delta>; atom y \<sharp> \<Theta>; atom y \<sharp> z; \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>b\<^esub> \<Delta> : Lam [y]. e'; \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> : e'[y::=x] \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : App e x \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 3. \<And>\<Gamma> x e L \<Delta> z L'. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>b. set b \<subseteq> set (x # L) \<Longrightarrow> delete x \<Gamma> : e \<Down>\<^bsub>b\<^esub> \<Delta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Var x \<Down>\<^bsub>L'\<^esub> (x, z) # \<Delta> : z
 4. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 5. \<And>\<Gamma> b L L'. set L' \<subseteq> set L \<Longrightarrow> \<Gamma> : Bool b \<Down>\<^bsub>L'\<^esub> \<Gamma> : Bool b
 6. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z L'. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Gamma> : scrut \<Down>\<^bsub>ba\<^esub> \<Delta> : Bool b; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>ba\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> : Lam [x]. e \<Down>\<^bsub>L'\<^esub> \<Gamma> : Lam [x]. e
[PROOF STEP]
by (rule reds.Lambda)
[PROOF STATE]
proof (state)
this:
\<Gamma> : Lam [x]. e \<Down>\<^bsub>L'\<^esub> \<Gamma> : Lam [x]. e

goal (5 subgoals):
 1. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' L'. \<lbrakk>atom y \<sharp> L'; atom y \<sharp> \<Gamma>; atom y \<sharp> e; atom y \<sharp> x; atom y \<sharp> L; atom y \<sharp> \<Delta>; atom y \<sharp> \<Theta>; atom y \<sharp> z; \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>b\<^esub> \<Delta> : Lam [y]. e'; \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> : e'[y::=x] \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : App e x \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 2. \<And>\<Gamma> x e L \<Delta> z L'. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>b. set b \<subseteq> set (x # L) \<Longrightarrow> delete x \<Gamma> : e \<Down>\<^bsub>b\<^esub> \<Delta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Var x \<Down>\<^bsub>L'\<^esub> (x, z) # \<Delta> : z
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 4. \<And>\<Gamma> b L L'. set L' \<subseteq> set L \<Longrightarrow> \<Gamma> : Bool b \<Down>\<^bsub>L'\<^esub> \<Gamma> : Bool b
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z L'. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Gamma> : scrut \<Down>\<^bsub>ba\<^esub> \<Delta> : Bool b; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>ba\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' L'. \<lbrakk>atom y \<sharp> L'; atom y \<sharp> \<Gamma>; atom y \<sharp> e; atom y \<sharp> x; atom y \<sharp> L; atom y \<sharp> \<Delta>; atom y \<sharp> \<Theta>; atom y \<sharp> z; \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>b\<^esub> \<Delta> : Lam [y]. e'; \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> : e'[y::=x] \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : App e x \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 2. \<And>\<Gamma> x e L \<Delta> z L'. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>b. set b \<subseteq> set (x # L) \<Longrightarrow> delete x \<Gamma> : e \<Down>\<^bsub>b\<^esub> \<Delta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Var x \<Down>\<^bsub>L'\<^esub> (x, z) # \<Delta> : z
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 4. \<And>\<Gamma> b L L'. set L' \<subseteq> set L \<Longrightarrow> \<Gamma> : Bool b \<Down>\<^bsub>L'\<^esub> \<Gamma> : Bool b
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z L'. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Gamma> : scrut \<Down>\<^bsub>ba\<^esub> \<Delta> : Bool b; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>ba\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
case (Application y \<Gamma> e xa L \<Delta> \<Theta> z e' L')
[PROOF STATE]
proof (state)
this:
atom y \<sharp> L'
atom y \<sharp> \<Gamma>
atom y \<sharp> e
atom y \<sharp> xa
atom y \<sharp> L
atom y \<sharp> \<Delta>
atom y \<sharp> \<Theta>
atom y \<sharp> z
\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'
set ?b \<subseteq> set L \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>?b\<^esub> \<Delta> : Lam [y]. e'
\<Delta> : e'[y::=xa] \<Down>\<^bsub>L\<^esub> \<Theta> : z
set ?b \<subseteq> set L \<Longrightarrow> \<Delta> : e'[y::=xa] \<Down>\<^bsub>?b\<^esub> \<Theta> : z
set L' \<subseteq> set L

goal (5 subgoals):
 1. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' L'. \<lbrakk>atom y \<sharp> L'; atom y \<sharp> \<Gamma>; atom y \<sharp> e; atom y \<sharp> x; atom y \<sharp> L; atom y \<sharp> \<Delta>; atom y \<sharp> \<Theta>; atom y \<sharp> z; \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>b\<^esub> \<Delta> : Lam [y]. e'; \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> : e'[y::=x] \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : App e x \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 2. \<And>\<Gamma> x e L \<Delta> z L'. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>b. set b \<subseteq> set (x # L) \<Longrightarrow> delete x \<Gamma> : e \<Down>\<^bsub>b\<^esub> \<Delta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Var x \<Down>\<^bsub>L'\<^esub> (x, z) # \<Delta> : z
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 4. \<And>\<Gamma> b L L'. set L' \<subseteq> set L \<Longrightarrow> \<Gamma> : Bool b \<Down>\<^bsub>L'\<^esub> \<Gamma> : Bool b
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z L'. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Gamma> : scrut \<Down>\<^bsub>ba\<^esub> \<Delta> : Bool b; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>ba\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
from Application.hyps(10)[OF Application.prems] Application.hyps(12)[OF Application.prems]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> : e \<Down>\<^bsub>L'\<^esub> \<Delta> : Lam [y]. e'
\<Delta> : e'[y::=xa] \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> : e \<Down>\<^bsub>L'\<^esub> \<Delta> : Lam [y]. e'
\<Delta> : e'[y::=xa] \<Down>\<^bsub>L'\<^esub> \<Theta> : z

goal (1 subgoal):
 1. \<Gamma> : App e xa \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
by (rule reds_ApplicationI)
[PROOF STATE]
proof (state)
this:
\<Gamma> : App e xa \<Down>\<^bsub>L'\<^esub> \<Theta> : z

goal (4 subgoals):
 1. \<And>\<Gamma> x e L \<Delta> z L'. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>b. set b \<subseteq> set (x # L) \<Longrightarrow> delete x \<Gamma> : e \<Down>\<^bsub>b\<^esub> \<Delta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Var x \<Down>\<^bsub>L'\<^esub> (x, z) # \<Delta> : z
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 3. \<And>\<Gamma> b L L'. set L' \<subseteq> set L \<Longrightarrow> \<Gamma> : Bool b \<Down>\<^bsub>L'\<^esub> \<Gamma> : Bool b
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z L'. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Gamma> : scrut \<Down>\<^bsub>ba\<^esub> \<Delta> : Bool b; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>ba\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>\<Gamma> x e L \<Delta> z L'. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>b. set b \<subseteq> set (x # L) \<Longrightarrow> delete x \<Gamma> : e \<Down>\<^bsub>b\<^esub> \<Delta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Var x \<Down>\<^bsub>L'\<^esub> (x, z) # \<Delta> : z
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 3. \<And>\<Gamma> b L L'. set L' \<subseteq> set L \<Longrightarrow> \<Gamma> : Bool b \<Down>\<^bsub>L'\<^esub> \<Gamma> : Bool b
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z L'. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Gamma> : scrut \<Down>\<^bsub>ba\<^esub> \<Delta> : Bool b; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>ba\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
case (Variable \<Gamma> xa e L \<Delta> z L')
[PROOF STATE]
proof (state)
this:
map_of \<Gamma> xa = Some e
delete xa \<Gamma> : e \<Down>\<^bsub>xa # L\<^esub> \<Delta> : z
set ?b \<subseteq> set (xa # L) \<Longrightarrow> delete xa \<Gamma> : e \<Down>\<^bsub>?b\<^esub> \<Delta> : z
set L' \<subseteq> set L

goal (4 subgoals):
 1. \<And>\<Gamma> x e L \<Delta> z L'. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>b. set b \<subseteq> set (x # L) \<Longrightarrow> delete x \<Gamma> : e \<Down>\<^bsub>b\<^esub> \<Delta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Var x \<Down>\<^bsub>L'\<^esub> (x, z) # \<Delta> : z
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 3. \<And>\<Gamma> b L L'. set L' \<subseteq> set L \<Longrightarrow> \<Gamma> : Bool b \<Down>\<^bsub>L'\<^esub> \<Gamma> : Bool b
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z L'. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Gamma> : scrut \<Down>\<^bsub>ba\<^esub> \<Delta> : Bool b; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>ba\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
have "set (xa # L') \<subseteq> set (xa # L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (xa # L') \<subseteq> set (xa # L)
[PROOF STEP]
using Variable.prems
[PROOF STATE]
proof (prove)
using this:
set L' \<subseteq> set L

goal (1 subgoal):
 1. set (xa # L') \<subseteq> set (xa # L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (xa # L') \<subseteq> set (xa # L)

goal (4 subgoals):
 1. \<And>\<Gamma> x e L \<Delta> z L'. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>b. set b \<subseteq> set (x # L) \<Longrightarrow> delete x \<Gamma> : e \<Down>\<^bsub>b\<^esub> \<Delta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Var x \<Down>\<^bsub>L'\<^esub> (x, z) # \<Delta> : z
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 3. \<And>\<Gamma> b L L'. set L' \<subseteq> set L \<Longrightarrow> \<Gamma> : Bool b \<Down>\<^bsub>L'\<^esub> \<Gamma> : Bool b
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z L'. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Gamma> : scrut \<Down>\<^bsub>ba\<^esub> \<Delta> : Bool b; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>ba\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
set (xa # L') \<subseteq> set (xa # L)

goal (1 subgoal):
 1. \<Gamma> : Var xa \<Down>\<^bsub>L'\<^esub> (xa, z) # \<Delta> : z
[PROOF STEP]
by (rule reds.Variable[OF Variable(1) Variable.hyps(3)])
[PROOF STATE]
proof (state)
this:
\<Gamma> : Var xa \<Down>\<^bsub>L'\<^esub> (xa, z) # \<Delta> : z

goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 2. \<And>\<Gamma> b L L'. set L' \<subseteq> set L \<Longrightarrow> \<Gamma> : Bool b \<Down>\<^bsub>L'\<^esub> \<Gamma> : Bool b
 3. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z L'. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Gamma> : scrut \<Down>\<^bsub>ba\<^esub> \<Delta> : Bool b; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>ba\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 2. \<And>\<Gamma> b L L'. set L' \<subseteq> set L \<Longrightarrow> \<Gamma> : Bool b \<Down>\<^bsub>L'\<^esub> \<Gamma> : Bool b
 3. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z L'. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Gamma> : scrut \<Down>\<^bsub>ba\<^esub> \<Delta> : Bool b; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>ba\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
case (Bool b)
[PROOF STATE]
proof (state)
this:
set L' \<subseteq> set L_

goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 2. \<And>\<Gamma> b L L'. set L' \<subseteq> set L \<Longrightarrow> \<Gamma> : Bool b \<Down>\<^bsub>L'\<^esub> \<Gamma> : Bool b
 3. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z L'. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Gamma> : scrut \<Down>\<^bsub>ba\<^esub> \<Delta> : Bool b; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>ba\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b : Bool b_ \<Down>\<^bsub>L'\<^esub> b : Bool b_
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
b : Bool b_ \<Down>\<^bsub>L'\<^esub> b : Bool b_

goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z L'. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Gamma> : scrut \<Down>\<^bsub>ba\<^esub> \<Delta> : Bool b; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>ba\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z L'. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Gamma> : scrut \<Down>\<^bsub>ba\<^esub> \<Delta> : Bool b; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>ba\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
case (IfThenElse \<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z L')
[PROOF STATE]
proof (state)
this:
\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b
set ?b \<subseteq> set L \<Longrightarrow> \<Gamma> : scrut \<Down>\<^bsub>?b\<^esub> \<Delta> : Bool b
\<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z
set ?b \<subseteq> set L \<Longrightarrow> \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>?b\<^esub> \<Theta> : z
set L' \<subseteq> set L

goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z L'. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Gamma> : scrut \<Down>\<^bsub>ba\<^esub> \<Delta> : Bool b; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>ba. set ba \<subseteq> set L \<Longrightarrow> \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>ba\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b
set ?b \<subseteq> set L \<Longrightarrow> \<Gamma> : scrut \<Down>\<^bsub>?b\<^esub> \<Delta> : Bool b
\<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z
set ?b \<subseteq> set L \<Longrightarrow> \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>?b\<^esub> \<Theta> : z
set L' \<subseteq> set L

goal (1 subgoal):
 1. \<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
by (metis  reds.IfThenElse)
[PROOF STATE]
proof (state)
this:
\<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>L'\<^esub> \<Theta> : z

goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
case (Let \<Delta> \<Gamma>  L body \<Theta> z L')
[PROOF STATE]
proof (state)
this:
atom ` domA \<Delta> \<sharp>* \<Gamma>
atom ` domA \<Delta> \<sharp>* L
\<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z
set ?b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>?b\<^esub> \<Theta> : z
set L' \<subseteq> set L

goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
have "atom ` domA \<Delta> \<sharp>* (\<Gamma>, L')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom ` domA \<Delta> \<sharp>* (\<Gamma>, L')
[PROOF STEP]
using Let(1-3) Let.prems
[PROOF STATE]
proof (prove)
using this:
atom ` domA \<Delta> \<sharp>* \<Gamma>
atom ` domA \<Delta> \<sharp>* L
\<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z
set L' \<subseteq> set L

goal (1 subgoal):
 1. atom ` domA \<Delta> \<sharp>* (\<Gamma>, L')
[PROOF STEP]
by (auto simp add: fresh_star_Pair  fresh_star_set_subset)
[PROOF STATE]
proof (state)
this:
atom ` domA \<Delta> \<sharp>* (\<Gamma>, L')

goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z L'. \<lbrakk>atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* L; \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>b. set b \<subseteq> set L \<Longrightarrow> \<Delta> @ \<Gamma> : body \<Down>\<^bsub>b\<^esub> \<Theta> : z; set L' \<subseteq> set L\<rbrakk> \<Longrightarrow> \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
atom ` domA \<Delta> \<sharp>* (\<Gamma>, L')

goal (1 subgoal):
 1. \<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z
[PROOF STEP]
by (rule reds.Let[OF _ Let.hyps(4)[OF Let.prems]])
[PROOF STATE]
proof (state)
this:
\<Gamma> : Let \<Delta> body \<Down>\<^bsub>L'\<^esub> \<Theta> : z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma result_evaluated:
  "\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z \<Longrightarrow> isVal z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z \<Longrightarrow> isVal z
[PROOF STEP]
by (induct \<Gamma> e L \<Delta> z rule:reds.induct) (auto dest: reds_doesnt_forget)


[STATEMENT]
lemma result_evaluated_fresh:
  assumes "\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z"
  obtains y e'
  where "z = (Lam [y]. e')" and "atom y \<sharp> (c::'a::fs)" | b where "z = Bool b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>y e'. \<lbrakk>z = Lam [y]. e'; atom y \<sharp> c\<rbrakk> \<Longrightarrow> thesis; \<And>b. z = Bool b \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>y e'. \<lbrakk>z = Lam [y]. e'; atom y \<sharp> c\<rbrakk> \<Longrightarrow> thesis; \<And>b. z = Bool b \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z
[PROOF STEP]
have "isVal z"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z

goal (1 subgoal):
 1. isVal z
[PROOF STEP]
by (rule result_evaluated)
[PROOF STATE]
proof (state)
this:
isVal z

goal (1 subgoal):
 1. \<lbrakk>\<And>y e'. \<lbrakk>z = Lam [y]. e'; atom y \<sharp> c\<rbrakk> \<Longrightarrow> thesis; \<And>b. z = Bool b \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "(\<exists> y e'. z = Lam [y]. e' \<and> atom y \<sharp> c) \<or> (\<exists> b. z = Bool b)"
[PROOF STATE]
proof (prove)
using this:
isVal z

goal (1 subgoal):
 1. (\<exists>y e'. z = Lam [y]. e' \<and> atom y \<sharp> c) \<or> (\<exists>b. z = Bool b)
[PROOF STEP]
by (nominal_induct z avoiding: c rule:exp_strong_induct) auto
[PROOF STATE]
proof (state)
this:
(\<exists>y e'. z = Lam [y]. e' \<and> atom y \<sharp> c) \<or> (\<exists>b. z = Bool b)

goal (1 subgoal):
 1. \<lbrakk>\<And>y e'. \<lbrakk>z = Lam [y]. e'; atom y \<sharp> c\<rbrakk> \<Longrightarrow> thesis; \<And>b. z = Bool b \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>y e'. z = Lam [y]. e' \<and> atom y \<sharp> c) \<or> (\<exists>b. z = Bool b)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
(\<exists>y e'. z = Lam [y]. e' \<and> atom y \<sharp> c) \<or> (\<exists>b. z = Bool b)
\<lbrakk>z = Lam [?y]. ?e'; atom ?y \<sharp> c\<rbrakk> \<Longrightarrow> thesis
z = Bool ?b \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bisim1_list1_has_methodD: "bisim1_list1 t h ex exs xcp ((stk, loc, C, M, pc) # frs) \<Longrightarrow> P \<turnstile> C has M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bisim1_list1 t h ex exs xcp ((stk, loc, C, M, pc) # frs) \<Longrightarrow> P \<turnstile> C has M
[PROOF STEP]
by(fastforce elim!: bisim1_list1.cases intro: has_methodI)


[STATEMENT]
lemma \<tau>exec_1_d_silent_move:
  "\<tau>exec_1_d P t (xcp, h, frs) (xcp', h', frs')
  \<Longrightarrow> \<tau>trsys.silent_move (mexecd P t) (\<tau>MOVE2 P) ((xcp, frs), h) ((xcp', frs'), h')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_1_d P t (xcp, h, frs) (xcp', h', frs') \<Longrightarrow> execd_mthr.silent_move P t ((xcp, frs), h) ((xcp', frs'), h')
[PROOF STEP]
apply(rule \<tau>trsys.silent_move.intros)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<tau>exec_1_d P t (xcp, h, frs) (xcp', h', frs') \<Longrightarrow> execd_mthr.r_syntax P t (xcp, frs) h ?tl (xcp', frs') h'
 2. \<tau>exec_1_d P t (xcp, h, frs) (xcp', h', frs') \<Longrightarrow> (case ((xcp, frs), h) of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 P (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) ?tl ((xcp', frs'), h')
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_1_d P t (xcp, h, frs) (xcp', h', frs') \<Longrightarrow> P,t \<turnstile> Normal (xcp, h, frs) -\<lbrace>\<rbrace>-jvmd\<rightarrow> Normal (xcp', h', frs')
[PROOF STEP]
apply(rule exec_1_d_NormalI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<tau>exec_1_d P t (xcp, h, frs) (xcp', h', frs') \<Longrightarrow> exec_d P t (xcp, h, frs) = Normal ?\<Sigma>11
 2. \<tau>exec_1_d P t (xcp, h, frs) (xcp', h', frs') \<Longrightarrow> (\<lbrace>\<rbrace>, xcp', h', frs') \<in> ?\<Sigma>11
[PROOF STEP]
apply(auto simp add: exec_1_iff exec_d_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma silent_move_\<tau>exec_1_d:
  "\<tau>trsys.silent_move (mexecd P t) (\<tau>MOVE2 P) ((xcp, frs), h) ((xcp', frs'), h')
  \<Longrightarrow> \<tau>exec_1_d P t (xcp, h, frs) (xcp', h', frs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execd_mthr.silent_move P t ((xcp, frs), h) ((xcp', frs'), h') \<Longrightarrow> \<tau>exec_1_d P t (xcp, h, frs) (xcp', h', frs')
[PROOF STEP]
apply(erule \<tau>trsys.silent_move.cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' tl. \<lbrakk>((xcp, frs), h) = s; ((xcp', frs'), h') = s'; mexecd P t s tl s'; (case s of (x, xa) \<Rightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h ta s. \<tau>Move2 P (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>) xa) tl s'\<rbrakk> \<Longrightarrow> \<tau>exec_1_d P t (xcp, h, frs) (xcp', h', frs')
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,t \<turnstile> Normal (xcp, h, frs) -\<lbrace>\<rbrace>-jvmd\<rightarrow> Normal (xcp', h', frs'); \<tau>Move2 P (xcp, h, frs)\<rbrakk> \<Longrightarrow> \<tau>exec_1_d P t (xcp, h, frs) (xcp', h', frs')
[PROOF STEP]
apply(erule jvmd_NormalE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xcpa ha f frsa. \<lbrakk>\<tau>Move2 P (xcp, h, frs); check P (xcp, h, frs); (\<lbrace>\<rbrace>, xcp', h', frs') \<in> exec P t (xcp, h, frs); (xcp, h, frs) = (xcpa, ha, f # frsa)\<rbrakk> \<Longrightarrow> \<tau>exec_1_d P t (xcp, h, frs) (xcp', h', frs')
[PROOF STEP]
apply(auto simp add: exec_1_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma \<tau>Exec_1_dr_rtranclpD:
  "\<tau>Exec_1_dr P t (xcp, h, frs) (xcp', h', frs')
  \<Longrightarrow> \<tau>trsys.silent_moves (mexecd P t) (\<tau>MOVE2 P) ((xcp, frs), h) ((xcp', frs'), h')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_1_dr P t (xcp, h, frs) (xcp', h', frs') \<Longrightarrow> execd_mthr.silent_moves P t ((xcp, frs), h) ((xcp', frs'), h')
[PROOF STEP]
by(induct rule: rtranclp_induct3)(blast intro: rtranclp.rtrancl_into_rtrancl \<tau>exec_1_d_silent_move)+


[STATEMENT]
lemma \<tau>Exec_1_dt_tranclpD:
  "\<tau>Exec_1_dt P t (xcp, h, frs) (xcp', h', frs')
  \<Longrightarrow> \<tau>trsys.silent_movet (mexecd P t) (\<tau>MOVE2 P) ((xcp, frs), h) ((xcp', frs'), h')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_1_dt P t (xcp, h, frs) (xcp', h', frs') \<Longrightarrow> execd_mthr.silent_movet P t ((xcp, frs), h) ((xcp', frs'), h')
[PROOF STEP]
by(induct rule: tranclp_induct3)(blast intro: tranclp.trancl_into_trancl \<tau>exec_1_d_silent_move)+


[STATEMENT]
lemma rtranclp_\<tau>Exec_1_dr:
  "\<tau>trsys.silent_moves (mexecd P t) (\<tau>MOVE2 P) ((xcp, frs), h) ((xcp', frs'), h')
  \<Longrightarrow> \<tau>Exec_1_dr P t (xcp, h, frs) (xcp', h', frs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execd_mthr.silent_moves P t ((xcp, frs), h) ((xcp', frs'), h') \<Longrightarrow> \<tau>Exec_1_dr P t (xcp, h, frs) (xcp', h', frs')
[PROOF STEP]
by(induct rule: rtranclp_induct[of _ "((ax, ay), az)" "((bx, by), bz)", split_rule, consumes 1])(blast intro: rtranclp.rtrancl_into_rtrancl silent_move_\<tau>exec_1_d)+


[STATEMENT]
lemma tranclp_\<tau>Exec_1_dt:
  "\<tau>trsys.silent_movet (mexecd P t) (\<tau>MOVE2 P) ((xcp, frs), h) ((xcp', frs'), h')
  \<Longrightarrow> \<tau>Exec_1_dt P t (xcp, h, frs) (xcp', h', frs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execd_mthr.silent_movet P t ((xcp, frs), h) ((xcp', frs'), h') \<Longrightarrow> \<tau>Exec_1_dt P t (xcp, h, frs) (xcp', h', frs')
[PROOF STEP]
by(induct rule: tranclp_induct[of _ "((ax, ay), az)" "((bx, by), bz)", split_rule, consumes 1])(blast intro: tranclp.trancl_into_trancl silent_move_\<tau>exec_1_d)+


[STATEMENT]
lemma \<tau>Exec_1_dr_conv_rtranclp:
  "\<tau>Exec_1_dr P t (xcp, h, frs) (xcp', h', frs') =
  \<tau>trsys.silent_moves (mexecd P t) (\<tau>MOVE2 P) ((xcp, frs), h) ((xcp', frs'), h')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_1_dr P t (xcp, h, frs) (xcp', h', frs') = execd_mthr.silent_moves P t ((xcp, frs), h) ((xcp', frs'), h')
[PROOF STEP]
by(blast intro: \<tau>Exec_1_dr_rtranclpD rtranclp_\<tau>Exec_1_dr)


[STATEMENT]
lemma \<tau>Exec_1_dt_conv_tranclp:
  "\<tau>Exec_1_dt P t (xcp, h, frs) (xcp', h', frs') =
  \<tau>trsys.silent_movet (mexecd P t) (\<tau>MOVE2 P) ((xcp, frs), h) ((xcp', frs'), h')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_1_dt P t (xcp, h, frs) (xcp', h', frs') = execd_mthr.silent_movet P t ((xcp, frs), h) ((xcp', frs'), h')
[PROOF STEP]
by(blast intro: \<tau>Exec_1_dt_tranclpD tranclp_\<tau>Exec_1_dt)