[STATEMENT]
lemma rhs_interpret_eq:
  "\<lbrakk>state_check cf e v'; \<forall>V \<in> fv e. cf V = cf' V\<rbrakk>
   \<Longrightarrow> state_check cf' e v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>state_check cf e v'; \<forall>V\<in>fv e. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e v'
[PROOF STEP]
proof(induct e arbitrary:v')
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x v'. \<lbrakk>state_check cf (Val x) v'; \<forall>V\<in>fv (Val x). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (Val x) v'
 2. \<And>x v'. \<lbrakk>state_check cf (Var x) v'; \<forall>V\<in>fv (Var x). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (Var x) v'
 3. \<And>e1 x2a e2 v'. \<lbrakk>\<And>v'. \<lbrakk>state_check cf e1 v'; \<forall>V\<in>fv e1. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e1 v'; \<And>v'. \<lbrakk>state_check cf e2 v'; \<forall>V\<in>fv e2. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e2 v'; state_check cf (e1 \<guillemotleft>x2a\<guillemotright> e2) v'; \<forall>V\<in>fv (e1 \<guillemotleft>x2a\<guillemotright> e2). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (e1 \<guillemotleft>x2a\<guillemotright> e2) v'
[PROOF STEP]
case (Val v)
[PROOF STATE]
proof (state)
this:
state_check cf (Val v) v'
\<forall>V\<in>fv (Val v). cf V = cf' V

goal (3 subgoals):
 1. \<And>x v'. \<lbrakk>state_check cf (Val x) v'; \<forall>V\<in>fv (Val x). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (Val x) v'
 2. \<And>x v'. \<lbrakk>state_check cf (Var x) v'; \<forall>V\<in>fv (Var x). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (Var x) v'
 3. \<And>e1 x2a e2 v'. \<lbrakk>\<And>v'. \<lbrakk>state_check cf e1 v'; \<forall>V\<in>fv e1. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e1 v'; \<And>v'. \<lbrakk>state_check cf e2 v'; \<forall>V\<in>fv e2. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e2 v'; state_check cf (e1 \<guillemotleft>x2a\<guillemotright> e2) v'; \<forall>V\<in>fv (e1 \<guillemotleft>x2a\<guillemotright> e2). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (e1 \<guillemotleft>x2a\<guillemotright> e2) v'
[PROOF STEP]
from \<open>state_check cf (Val v) v'\<close>
[PROOF STATE]
proof (chain)
picking this:
state_check cf (Val v) v'
[PROOF STEP]
have "v' = Some v"
[PROOF STATE]
proof (prove)
using this:
state_check cf (Val v) v'

goal (1 subgoal):
 1. v' = Some v
[PROOF STEP]
by(fastforce elim:interpret.cases)
[PROOF STATE]
proof (state)
this:
v' = Some v

goal (3 subgoals):
 1. \<And>x v'. \<lbrakk>state_check cf (Val x) v'; \<forall>V\<in>fv (Val x). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (Val x) v'
 2. \<And>x v'. \<lbrakk>state_check cf (Var x) v'; \<forall>V\<in>fv (Var x). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (Var x) v'
 3. \<And>e1 x2a e2 v'. \<lbrakk>\<And>v'. \<lbrakk>state_check cf e1 v'; \<forall>V\<in>fv e1. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e1 v'; \<And>v'. \<lbrakk>state_check cf e2 v'; \<forall>V\<in>fv e2. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e2 v'; state_check cf (e1 \<guillemotleft>x2a\<guillemotright> e2) v'; \<forall>V\<in>fv (e1 \<guillemotleft>x2a\<guillemotright> e2). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (e1 \<guillemotleft>x2a\<guillemotright> e2) v'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
v' = Some v

goal (1 subgoal):
 1. state_check cf' (Val v) v'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
state_check cf' (Val v) v'

goal (2 subgoals):
 1. \<And>x v'. \<lbrakk>state_check cf (Var x) v'; \<forall>V\<in>fv (Var x). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (Var x) v'
 2. \<And>e1 x2a e2 v'. \<lbrakk>\<And>v'. \<lbrakk>state_check cf e1 v'; \<forall>V\<in>fv e1. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e1 v'; \<And>v'. \<lbrakk>state_check cf e2 v'; \<forall>V\<in>fv e2. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e2 v'; state_check cf (e1 \<guillemotleft>x2a\<guillemotright> e2) v'; \<forall>V\<in>fv (e1 \<guillemotleft>x2a\<guillemotright> e2). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (e1 \<guillemotleft>x2a\<guillemotright> e2) v'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x v'. \<lbrakk>state_check cf (Var x) v'; \<forall>V\<in>fv (Var x). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (Var x) v'
 2. \<And>e1 x2a e2 v'. \<lbrakk>\<And>v'. \<lbrakk>state_check cf e1 v'; \<forall>V\<in>fv e1. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e1 v'; \<And>v'. \<lbrakk>state_check cf e2 v'; \<forall>V\<in>fv e2. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e2 v'; state_check cf (e1 \<guillemotleft>x2a\<guillemotright> e2) v'; \<forall>V\<in>fv (e1 \<guillemotleft>x2a\<guillemotright> e2). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (e1 \<guillemotleft>x2a\<guillemotright> e2) v'
[PROOF STEP]
case (Var V)
[PROOF STATE]
proof (state)
this:
state_check cf (Var V) v'
\<forall>V\<in>fv (Var V). cf V = cf' V

goal (2 subgoals):
 1. \<And>x v'. \<lbrakk>state_check cf (Var x) v'; \<forall>V\<in>fv (Var x). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (Var x) v'
 2. \<And>e1 x2a e2 v'. \<lbrakk>\<And>v'. \<lbrakk>state_check cf e1 v'; \<forall>V\<in>fv e1. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e1 v'; \<And>v'. \<lbrakk>state_check cf e2 v'; \<forall>V\<in>fv e2. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e2 v'; state_check cf (e1 \<guillemotleft>x2a\<guillemotright> e2) v'; \<forall>V\<in>fv (e1 \<guillemotleft>x2a\<guillemotright> e2). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (e1 \<guillemotleft>x2a\<guillemotright> e2) v'
[PROOF STEP]
hence "cf' (V) = v'"
[PROOF STATE]
proof (prove)
using this:
state_check cf (Var V) v'
\<forall>V\<in>fv (Var V). cf V = cf' V

goal (1 subgoal):
 1. cf' V = v'
[PROOF STEP]
by(fastforce elim:interpret.cases)
[PROOF STATE]
proof (state)
this:
cf' V = v'

goal (2 subgoals):
 1. \<And>x v'. \<lbrakk>state_check cf (Var x) v'; \<forall>V\<in>fv (Var x). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (Var x) v'
 2. \<And>e1 x2a e2 v'. \<lbrakk>\<And>v'. \<lbrakk>state_check cf e1 v'; \<forall>V\<in>fv e1. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e1 v'; \<And>v'. \<lbrakk>state_check cf e2 v'; \<forall>V\<in>fv e2. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e2 v'; state_check cf (e1 \<guillemotleft>x2a\<guillemotright> e2) v'; \<forall>V\<in>fv (e1 \<guillemotleft>x2a\<guillemotright> e2). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (e1 \<guillemotleft>x2a\<guillemotright> e2) v'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
cf' V = v'

goal (1 subgoal):
 1. state_check cf' (Var V) v'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
state_check cf' (Var V) v'

goal (1 subgoal):
 1. \<And>e1 x2a e2 v'. \<lbrakk>\<And>v'. \<lbrakk>state_check cf e1 v'; \<forall>V\<in>fv e1. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e1 v'; \<And>v'. \<lbrakk>state_check cf e2 v'; \<forall>V\<in>fv e2. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e2 v'; state_check cf (e1 \<guillemotleft>x2a\<guillemotright> e2) v'; \<forall>V\<in>fv (e1 \<guillemotleft>x2a\<guillemotright> e2). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (e1 \<guillemotleft>x2a\<guillemotright> e2) v'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e1 x2a e2 v'. \<lbrakk>\<And>v'. \<lbrakk>state_check cf e1 v'; \<forall>V\<in>fv e1. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e1 v'; \<And>v'. \<lbrakk>state_check cf e2 v'; \<forall>V\<in>fv e2. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e2 v'; state_check cf (e1 \<guillemotleft>x2a\<guillemotright> e2) v'; \<forall>V\<in>fv (e1 \<guillemotleft>x2a\<guillemotright> e2). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (e1 \<guillemotleft>x2a\<guillemotright> e2) v'
[PROOF STEP]
case (BinOp b1 bop b2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>state_check cf b1 ?v'; \<forall>V\<in>fv b1. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' b1 ?v'
\<lbrakk>state_check cf b2 ?v'; \<forall>V\<in>fv b2. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' b2 ?v'
state_check cf (b1 \<guillemotleft>bop\<guillemotright> b2) v'
\<forall>V\<in>fv (b1 \<guillemotleft>bop\<guillemotright> b2). cf V = cf' V

goal (1 subgoal):
 1. \<And>e1 x2a e2 v'. \<lbrakk>\<And>v'. \<lbrakk>state_check cf e1 v'; \<forall>V\<in>fv e1. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e1 v'; \<And>v'. \<lbrakk>state_check cf e2 v'; \<forall>V\<in>fv e2. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e2 v'; state_check cf (e1 \<guillemotleft>x2a\<guillemotright> e2) v'; \<forall>V\<in>fv (e1 \<guillemotleft>x2a\<guillemotright> e2). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (e1 \<guillemotleft>x2a\<guillemotright> e2) v'
[PROOF STEP]
note IH1 = \<open>\<And>v'. \<lbrakk>state_check cf b1 v'; \<forall>V\<in>fv b1. cf V = cf' V\<rbrakk>
    \<Longrightarrow> state_check cf' b1 v'\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>state_check cf b1 ?v'; \<forall>V\<in>fv b1. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' b1 ?v'

goal (1 subgoal):
 1. \<And>e1 x2a e2 v'. \<lbrakk>\<And>v'. \<lbrakk>state_check cf e1 v'; \<forall>V\<in>fv e1. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e1 v'; \<And>v'. \<lbrakk>state_check cf e2 v'; \<forall>V\<in>fv e2. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e2 v'; state_check cf (e1 \<guillemotleft>x2a\<guillemotright> e2) v'; \<forall>V\<in>fv (e1 \<guillemotleft>x2a\<guillemotright> e2). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (e1 \<guillemotleft>x2a\<guillemotright> e2) v'
[PROOF STEP]
note IH2 = \<open>\<And>v'. \<lbrakk>state_check cf b2 v'; \<forall>V\<in>fv b2. cf V = cf' V\<rbrakk>
    \<Longrightarrow> state_check cf' b2 v'\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>state_check cf b2 ?v'; \<forall>V\<in>fv b2. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' b2 ?v'

goal (1 subgoal):
 1. \<And>e1 x2a e2 v'. \<lbrakk>\<And>v'. \<lbrakk>state_check cf e1 v'; \<forall>V\<in>fv e1. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e1 v'; \<And>v'. \<lbrakk>state_check cf e2 v'; \<forall>V\<in>fv e2. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e2 v'; state_check cf (e1 \<guillemotleft>x2a\<guillemotright> e2) v'; \<forall>V\<in>fv (e1 \<guillemotleft>x2a\<guillemotright> e2). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (e1 \<guillemotleft>x2a\<guillemotright> e2) v'
[PROOF STEP]
from \<open>\<forall>V \<in> fv (b1 \<guillemotleft>bop\<guillemotright> b2). cf V = cf' V\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>V\<in>fv (b1 \<guillemotleft>bop\<guillemotright> b2). cf V = cf' V
[PROOF STEP]
have "\<forall>V \<in> fv b1. cf V = cf' V"
    and "\<forall>V \<in> fv b2. cf V = cf' V"
[PROOF STATE]
proof (prove)
using this:
\<forall>V\<in>fv (b1 \<guillemotleft>bop\<guillemotright> b2). cf V = cf' V

goal (1 subgoal):
 1. \<forall>V\<in>fv b1. cf V = cf' V &&& \<forall>V\<in>fv b2. cf V = cf' V
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>fv b1. cf V = cf' V
\<forall>V\<in>fv b2. cf V = cf' V

goal (1 subgoal):
 1. \<And>e1 x2a e2 v'. \<lbrakk>\<And>v'. \<lbrakk>state_check cf e1 v'; \<forall>V\<in>fv e1. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e1 v'; \<And>v'. \<lbrakk>state_check cf e2 v'; \<forall>V\<in>fv e2. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e2 v'; state_check cf (e1 \<guillemotleft>x2a\<guillemotright> e2) v'; \<forall>V\<in>fv (e1 \<guillemotleft>x2a\<guillemotright> e2). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (e1 \<guillemotleft>x2a\<guillemotright> e2) v'
[PROOF STEP]
from \<open>state_check cf (b1 \<guillemotleft>bop\<guillemotright> b2) v'\<close>
[PROOF STATE]
proof (chain)
picking this:
state_check cf (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
have "((state_check cf b1 None \<and> v' = None) \<or>
          (state_check cf b2 None \<and> v' = None)) \<or>
    (\<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and>
    binop bop v\<^sub>1 v\<^sub>2 = v')"
[PROOF STATE]
proof (prove)
using this:
state_check cf (b1 \<guillemotleft>bop\<guillemotright> b2) v'

goal (1 subgoal):
 1. (state_check cf b1 None \<and> v' = None \<or> state_check cf b2 None \<and> v' = None) \<or> (\<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v')
[PROOF STEP]
apply(cases "interpret b1 cf",simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>state_check cf (b1 \<guillemotleft>bop\<guillemotright> b2) v'; state_check cf b1 (Some a)\<rbrakk> \<Longrightarrow> (state_check cf b1 None \<and> v' = None \<or> state_check cf b2 None \<and> v' = None) \<or> (\<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v')
[PROOF STEP]
apply(cases "interpret b2 cf",simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. \<lbrakk>state_check cf (b1 \<guillemotleft>bop\<guillemotright> b2) v'; state_check cf b1 (Some a); state_check cf b2 (Some aa)\<rbrakk> \<Longrightarrow> (state_check cf b1 None \<and> v' = None \<or> state_check cf b2 None \<and> v' = None) \<or> (\<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v')
[PROOF STEP]
by(case_tac "binop bop a aa",simp+)
[PROOF STATE]
proof (state)
this:
(state_check cf b1 None \<and> v' = None \<or> state_check cf b2 None \<and> v' = None) \<or> (\<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v')

goal (1 subgoal):
 1. \<And>e1 x2a e2 v'. \<lbrakk>\<And>v'. \<lbrakk>state_check cf e1 v'; \<forall>V\<in>fv e1. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e1 v'; \<And>v'. \<lbrakk>state_check cf e2 v'; \<forall>V\<in>fv e2. cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' e2 v'; state_check cf (e1 \<guillemotleft>x2a\<guillemotright> e2) v'; \<forall>V\<in>fv (e1 \<guillemotleft>x2a\<guillemotright> e2). cf V = cf' V\<rbrakk> \<Longrightarrow> state_check cf' (e1 \<guillemotleft>x2a\<guillemotright> e2) v'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(state_check cf b1 None \<and> v' = None \<or> state_check cf b2 None \<and> v' = None) \<or> (\<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v')

goal (1 subgoal):
 1. state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (state_check cf b1 None \<and> v' = None \<or> state_check cf b2 None \<and> v' = None) \<or> (\<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v') \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
proof(erule disjE)+
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. state_check cf b1 None \<and> v' = None \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
 2. state_check cf b2 None \<and> v' = None \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
 3. \<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v' \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
assume "state_check cf b1 None \<and> v' = None"
[PROOF STATE]
proof (state)
this:
state_check cf b1 None \<and> v' = None

goal (3 subgoals):
 1. state_check cf b1 None \<and> v' = None \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
 2. state_check cf b2 None \<and> v' = None \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
 3. \<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v' \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
hence check:"state_check cf b1 None" and "v' = None"
[PROOF STATE]
proof (prove)
using this:
state_check cf b1 None \<and> v' = None

goal (1 subgoal):
 1. state_check cf b1 None &&& v' = None
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
state_check cf b1 None
v' = None

goal (3 subgoals):
 1. state_check cf b1 None \<and> v' = None \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
 2. state_check cf b2 None \<and> v' = None \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
 3. \<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v' \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
from IH1[OF check \<open>\<forall>V \<in> fv b1. cf V = cf' V\<close>]
[PROOF STATE]
proof (chain)
picking this:
state_check cf' b1 None
[PROOF STEP]
have "state_check cf' b1 None"
[PROOF STATE]
proof (prove)
using this:
state_check cf' b1 None

goal (1 subgoal):
 1. state_check cf' b1 None
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
state_check cf' b1 None

goal (3 subgoals):
 1. state_check cf b1 None \<and> v' = None \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
 2. state_check cf b2 None \<and> v' = None \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
 3. \<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v' \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
with \<open>v' = None\<close>
[PROOF STATE]
proof (chain)
picking this:
v' = None
state_check cf' b1 None
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
v' = None
state_check cf' b1 None

goal (1 subgoal):
 1. state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'

goal (2 subgoals):
 1. state_check cf b2 None \<and> v' = None \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
 2. \<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v' \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. state_check cf b2 None \<and> v' = None \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
 2. \<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v' \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
assume "state_check cf b2 None \<and> v' = None"
[PROOF STATE]
proof (state)
this:
state_check cf b2 None \<and> v' = None

goal (2 subgoals):
 1. state_check cf b2 None \<and> v' = None \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
 2. \<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v' \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
hence check:"state_check cf b2 None" and "v' = None"
[PROOF STATE]
proof (prove)
using this:
state_check cf b2 None \<and> v' = None

goal (1 subgoal):
 1. state_check cf b2 None &&& v' = None
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
state_check cf b2 None
v' = None

goal (2 subgoals):
 1. state_check cf b2 None \<and> v' = None \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
 2. \<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v' \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
from IH2[OF check \<open>\<forall>V \<in> fv b2. cf V = cf' V\<close>]
[PROOF STATE]
proof (chain)
picking this:
state_check cf' b2 None
[PROOF STEP]
have "state_check cf' b2 None"
[PROOF STATE]
proof (prove)
using this:
state_check cf' b2 None

goal (1 subgoal):
 1. state_check cf' b2 None
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
state_check cf' b2 None

goal (2 subgoals):
 1. state_check cf b2 None \<and> v' = None \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
 2. \<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v' \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
with \<open>v' = None\<close>
[PROOF STATE]
proof (chain)
picking this:
v' = None
state_check cf' b2 None
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
v' = None
state_check cf' b2 None

goal (1 subgoal):
 1. state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
by(cases "interpret b1 cf'") simp+
[PROOF STATE]
proof (state)
this:
state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'

goal (1 subgoal):
 1. \<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v' \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v' \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
assume "\<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and>
      state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v'"
[PROOF STATE]
proof (state)
this:
\<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v'

goal (1 subgoal):
 1. \<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v' \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v'
[PROOF STEP]
obtain v\<^sub>1 v\<^sub>2 where "state_check cf b1 (Some v\<^sub>1)"
      and "state_check cf b2 (Some v\<^sub>2)" and "binop bop v\<^sub>1 v\<^sub>2 = v'"
[PROOF STATE]
proof (prove)
using this:
\<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v'

goal (1 subgoal):
 1. (\<And>v\<^sub>1 v\<^sub>2. \<lbrakk>state_check cf b1 (Some v\<^sub>1); state_check cf b2 (Some v\<^sub>2); binop bop v\<^sub>1 v\<^sub>2 = v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
state_check cf b1 (Some v\<^sub>1)
state_check cf b2 (Some v\<^sub>2)
binop bop v\<^sub>1 v\<^sub>2 = v'

goal (1 subgoal):
 1. \<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v' \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
from \<open>\<forall>V \<in> fv (b1 \<guillemotleft>bop\<guillemotright> b2). cf V = cf' V\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>V\<in>fv (b1 \<guillemotleft>bop\<guillemotright> b2). cf V = cf' V
[PROOF STEP]
have "\<forall>V \<in> fv b1. cf V = cf' V"
[PROOF STATE]
proof (prove)
using this:
\<forall>V\<in>fv (b1 \<guillemotleft>bop\<guillemotright> b2). cf V = cf' V

goal (1 subgoal):
 1. \<forall>V\<in>fv b1. cf V = cf' V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>fv b1. cf V = cf' V

goal (1 subgoal):
 1. \<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v' \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
from IH1[OF \<open>state_check cf b1 (Some v\<^sub>1)\<close> this]
[PROOF STATE]
proof (chain)
picking this:
state_check cf' b1 (Some v\<^sub>1)
[PROOF STEP]
have "interpret b1 cf' = Some v\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
state_check cf' b1 (Some v\<^sub>1)

goal (1 subgoal):
 1. state_check cf' b1 (Some v\<^sub>1)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
state_check cf' b1 (Some v\<^sub>1)

goal (1 subgoal):
 1. \<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v' \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
from \<open>\<forall>V \<in> fv (b1 \<guillemotleft>bop\<guillemotright> b2). cf V = cf' V\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>V\<in>fv (b1 \<guillemotleft>bop\<guillemotright> b2). cf V = cf' V
[PROOF STEP]
have "\<forall>V \<in> fv b2. cf V = cf' V"
[PROOF STATE]
proof (prove)
using this:
\<forall>V\<in>fv (b1 \<guillemotleft>bop\<guillemotright> b2). cf V = cf' V

goal (1 subgoal):
 1. \<forall>V\<in>fv b2. cf V = cf' V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>fv b2. cf V = cf' V

goal (1 subgoal):
 1. \<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v' \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
from IH2[OF \<open>state_check cf b2 (Some v\<^sub>2)\<close> this]
[PROOF STATE]
proof (chain)
picking this:
state_check cf' b2 (Some v\<^sub>2)
[PROOF STEP]
have "interpret b2 cf' = Some v\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
state_check cf' b2 (Some v\<^sub>2)

goal (1 subgoal):
 1. state_check cf' b2 (Some v\<^sub>2)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
state_check cf' b2 (Some v\<^sub>2)

goal (1 subgoal):
 1. \<exists>v\<^sub>1 v\<^sub>2. state_check cf b1 (Some v\<^sub>1) \<and> state_check cf b2 (Some v\<^sub>2) \<and> binop bop v\<^sub>1 v\<^sub>2 = v' \<Longrightarrow> state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
with \<open>interpret b1 cf' = Some v\<^sub>1\<close> \<open>binop bop v\<^sub>1 v\<^sub>2 = v'\<close>
[PROOF STATE]
proof (chain)
picking this:
state_check cf' b1 (Some v\<^sub>1)
binop bop v\<^sub>1 v\<^sub>2 = v'
state_check cf' b2 (Some v\<^sub>2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
state_check cf' b1 (Some v\<^sub>1)
binop bop v\<^sub>1 v\<^sub>2 = v'
state_check cf' b2 (Some v\<^sub>2)

goal (1 subgoal):
 1. state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'
[PROOF STEP]
by(cases v') simp+
[PROOF STATE]
proof (state)
this:
state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
state_check cf' (b1 \<guillemotleft>bop\<guillemotright> b2) v'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma PCFG_CallEdge_THE_es:
  "prog \<turnstile> n -CEdge(p,es,rets)\<rightarrow>\<^sub>p n'
\<Longrightarrow> (THE es'. \<exists>p' rets' n'. prog \<turnstile> n -CEdge(p',es',rets')\<rightarrow>\<^sub>p n') = es"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prog \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p n' \<Longrightarrow> (THE es'. \<exists>p' rets' n'. prog \<turnstile> n -CEdge (p', es', rets')\<rightarrow>\<^sub>p n') = es
[PROOF STEP]
by(fastforce intro:the_equality dest:Proc_CFG_Call_nodes_eq)


[STATEMENT]
lemma ParamUses_Main_Return_target:
  "\<lbrakk>Rep_wf_prog wfp = (prog,procs); prog \<turnstile> n -CEdge(p',es,rets)\<rightarrow>\<^sub>p n' \<rbrakk>
  \<Longrightarrow> ParamUses wfp (Main,n) = map fv es"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_wf_prog wfp = (prog, procs); prog \<turnstile> n -CEdge (p', es, rets)\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> ParamUses wfp (Main, n) = map fv es
[PROOF STEP]
by(fastforce dest:PCFG_CallEdge_THE_es simp:ParamUses_def ParamUses_proc_def)


[STATEMENT]
lemma ParamUses_Proc_Return_target:
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c) \<in> set procs" and "c \<turnstile> n -CEdge(p',es,rets)\<rightarrow>\<^sub>p n'"
  shows "ParamUses wfp (p,n) = map fv es"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ParamUses wfp (p, n) = map fv es
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ParamUses wfp (p, n) = map fv es
[PROOF STEP]
from \<open>Rep_wf_prog wfp = (prog,procs)\<close>
[PROOF STATE]
proof (chain)
picking this:
Rep_wf_prog wfp = (prog, procs)
[PROOF STEP]
have "well_formed procs"
[PROOF STATE]
proof (prove)
using this:
Rep_wf_prog wfp = (prog, procs)

goal (1 subgoal):
 1. well_formed procs
[PROOF STEP]
by(fastforce intro:wf_wf_prog)
[PROOF STATE]
proof (state)
this:
well_formed procs

goal (1 subgoal):
 1. ParamUses wfp (p, n) = map fv es
[PROOF STEP]
with \<open>(p,ins,outs,c) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
(p, ins, outs, c) \<in> set procs
well_formed procs
[PROOF STEP]
have "p \<noteq> Main"
[PROOF STATE]
proof (prove)
using this:
(p, ins, outs, c) \<in> set procs
well_formed procs

goal (1 subgoal):
 1. p \<noteq> Main
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p \<noteq> Main

goal (1 subgoal):
 1. ParamUses wfp (p, n) = map fv es
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<noteq> Main

goal (1 subgoal):
 1. ParamUses wfp (p, n) = map fv es
[PROOF STEP]
from \<open>well_formed procs\<close> \<open>(p,ins,outs,c) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
well_formed procs
(p, ins, outs, c) \<in> set procs
[PROOF STEP]
have "(THE c'. \<exists>ins' outs'. (p,ins',outs',c') \<in> set procs) = c"
[PROOF STATE]
proof (prove)
using this:
well_formed procs
(p, ins, outs, c) \<in> set procs

goal (1 subgoal):
 1. (THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c
[PROOF STEP]
by(rule in_procs_THE_in_procs_cmd)
[PROOF STATE]
proof (state)
this:
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c

goal (1 subgoal):
 1. ParamUses wfp (p, n) = map fv es
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c

goal (1 subgoal):
 1. ParamUses wfp (p, n) = map fv es
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c
Rep_wf_prog wfp = (prog, procs)
(p, ins, outs, c) \<in> set procs
c \<turnstile> n -CEdge (p', es, rets)\<rightarrow>\<^sub>p n'

goal (1 subgoal):
 1. ParamUses wfp (p, n) = map fv es
[PROOF STEP]
by(fastforce dest:PCFG_CallEdge_THE_es simp:ParamUses_def ParamUses_proc_def)
[PROOF STATE]
proof (state)
this:
ParamUses wfp (p, n) = map fv es

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ParamUses_Main_IEdge_Nil:
  "\<lbrakk>Rep_wf_prog wfp = (prog,procs); prog \<turnstile> n -IEdge et\<rightarrow>\<^sub>p n'\<rbrakk>
  \<Longrightarrow> ParamUses wfp (Main,n) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_wf_prog wfp = (prog, procs); prog \<turnstile> n -IEdge et\<rightarrow>\<^sub>p n'\<rbrakk> \<Longrightarrow> ParamUses wfp (Main, n) = []
[PROOF STEP]
by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_source
            simp:ParamUses_def ParamUses_proc_def)


[STATEMENT]
lemma ParamUses_Proc_IEdge_Nil:
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c) \<in> set procs" and "c \<turnstile> n -IEdge et\<rightarrow>\<^sub>p n'"
  shows "ParamUses wfp (p,n) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ParamUses wfp (p, n) = []
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ParamUses wfp (p, n) = []
[PROOF STEP]
from \<open>Rep_wf_prog wfp = (prog,procs)\<close>
[PROOF STATE]
proof (chain)
picking this:
Rep_wf_prog wfp = (prog, procs)
[PROOF STEP]
have "well_formed procs"
[PROOF STATE]
proof (prove)
using this:
Rep_wf_prog wfp = (prog, procs)

goal (1 subgoal):
 1. well_formed procs
[PROOF STEP]
by(fastforce intro:wf_wf_prog)
[PROOF STATE]
proof (state)
this:
well_formed procs

goal (1 subgoal):
 1. ParamUses wfp (p, n) = []
[PROOF STEP]
with \<open>(p,ins,outs,c) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
(p, ins, outs, c) \<in> set procs
well_formed procs
[PROOF STEP]
have "p \<noteq> Main"
[PROOF STATE]
proof (prove)
using this:
(p, ins, outs, c) \<in> set procs
well_formed procs

goal (1 subgoal):
 1. p \<noteq> Main
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p \<noteq> Main

goal (1 subgoal):
 1. ParamUses wfp (p, n) = []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<noteq> Main

goal (1 subgoal):
 1. ParamUses wfp (p, n) = []
[PROOF STEP]
from \<open>well_formed procs\<close> \<open>(p,ins,outs,c) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
well_formed procs
(p, ins, outs, c) \<in> set procs
[PROOF STEP]
have "(THE c'. \<exists>ins' outs'. (p,ins',outs',c') \<in> set procs) = c"
[PROOF STATE]
proof (prove)
using this:
well_formed procs
(p, ins, outs, c) \<in> set procs

goal (1 subgoal):
 1. (THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c
[PROOF STEP]
by(rule in_procs_THE_in_procs_cmd)
[PROOF STATE]
proof (state)
this:
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c

goal (1 subgoal):
 1. ParamUses wfp (p, n) = []
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c

goal (1 subgoal):
 1. ParamUses wfp (p, n) = []
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c
Rep_wf_prog wfp = (prog, procs)
(p, ins, outs, c) \<in> set procs
c \<turnstile> n -IEdge et\<rightarrow>\<^sub>p n'

goal (1 subgoal):
 1. ParamUses wfp (p, n) = []
[PROOF STEP]
by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_source
                simp:ParamUses_def ParamUses_proc_def)
[PROOF STATE]
proof (state)
this:
ParamUses wfp (p, n) = []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ParamUses_Main_CEdge_Nil:
  "\<lbrakk>Rep_wf_prog wfp = (prog,procs); prog \<turnstile> n' -CEdge(p',es,rets)\<rightarrow>\<^sub>p n\<rbrakk>
  \<Longrightarrow> ParamUses wfp (Main,n) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_wf_prog wfp = (prog, procs); prog \<turnstile> n' -CEdge (p', es, rets)\<rightarrow>\<^sub>p n\<rbrakk> \<Longrightarrow> ParamUses wfp (Main, n) = []
[PROOF STEP]
by(fastforce dest:Proc_CFG_Call_targetnode_no_Call_sourcenode
            simp:ParamUses_def ParamUses_proc_def)


[STATEMENT]
lemma ParamUses_Proc_CEdge_Nil:
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c) \<in> set procs" and "c \<turnstile> n' -CEdge(p',es,rets)\<rightarrow>\<^sub>p n"
  shows "ParamUses wfp (p,n) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ParamUses wfp (p, n) = []
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ParamUses wfp (p, n) = []
[PROOF STEP]
from \<open>Rep_wf_prog wfp = (prog,procs)\<close>
[PROOF STATE]
proof (chain)
picking this:
Rep_wf_prog wfp = (prog, procs)
[PROOF STEP]
have "well_formed procs"
[PROOF STATE]
proof (prove)
using this:
Rep_wf_prog wfp = (prog, procs)

goal (1 subgoal):
 1. well_formed procs
[PROOF STEP]
by(fastforce intro:wf_wf_prog)
[PROOF STATE]
proof (state)
this:
well_formed procs

goal (1 subgoal):
 1. ParamUses wfp (p, n) = []
[PROOF STEP]
with \<open>(p,ins,outs,c) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
(p, ins, outs, c) \<in> set procs
well_formed procs
[PROOF STEP]
have "p \<noteq> Main"
[PROOF STATE]
proof (prove)
using this:
(p, ins, outs, c) \<in> set procs
well_formed procs

goal (1 subgoal):
 1. p \<noteq> Main
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p \<noteq> Main

goal (1 subgoal):
 1. ParamUses wfp (p, n) = []
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<noteq> Main

goal (1 subgoal):
 1. ParamUses wfp (p, n) = []
[PROOF STEP]
from \<open>well_formed procs\<close>
    \<open>(p,ins,outs,c) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
well_formed procs
(p, ins, outs, c) \<in> set procs
[PROOF STEP]
have "(THE c'. \<exists>ins' outs'. (p,ins',outs',c') \<in> set procs) = c"
[PROOF STATE]
proof (prove)
using this:
well_formed procs
(p, ins, outs, c) \<in> set procs

goal (1 subgoal):
 1. (THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c
[PROOF STEP]
by(rule in_procs_THE_in_procs_cmd)
[PROOF STATE]
proof (state)
this:
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c

goal (1 subgoal):
 1. ParamUses wfp (p, n) = []
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c

goal (1 subgoal):
 1. ParamUses wfp (p, n) = []
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<noteq> Main
(THE c'. \<exists>ins' outs'. (p, ins', outs', c') \<in> set procs) = c
Rep_wf_prog wfp = (prog, procs)
(p, ins, outs, c) \<in> set procs
c \<turnstile> n' -CEdge (p', es, rets)\<rightarrow>\<^sub>p n

goal (1 subgoal):
 1. ParamUses wfp (p, n) = []
[PROOF STEP]
by(fastforce dest:Proc_CFG_Call_targetnode_no_Call_sourcenode
                simp:ParamUses_def ParamUses_proc_def)
[PROOF STATE]
proof (state)
this:
ParamUses wfp (p, n) = []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lhs_fst_cmd:"lhs (fst_cmd c) = lhs c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lhs (fst_cmd c) = lhs c
[PROOF STEP]
by(induct c) auto


[STATEMENT]
lemma Proc_CFG_Call_source_empty_lhs:
  assumes "prog \<turnstile> Label l -CEdge (p,es,rets)\<rightarrow>\<^sub>p n'"
  shows "lhs (label prog l) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lhs (label prog l) = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lhs (label prog l) = {}
[PROOF STEP]
from \<open>prog \<turnstile> Label l -CEdge (p,es,rets)\<rightarrow>\<^sub>p n'\<close>
[PROOF STATE]
proof (chain)
picking this:
prog \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
[PROOF STEP]
have "l < #:prog"
[PROOF STATE]
proof (prove)
using this:
prog \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'

goal (1 subgoal):
 1. l < #:prog
[PROOF STEP]
by(rule Proc_CFG_sourcelabel_less_num_nodes)
[PROOF STATE]
proof (state)
this:
l < #:prog

goal (1 subgoal):
 1. lhs (label prog l) = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l < #:prog
[PROOF STEP]
obtain c' where "labels prog l c'"
[PROOF STATE]
proof (prove)
using this:
l < #:prog

goal (1 subgoal):
 1. (\<And>c'. labels prog l c' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule less_num_inner_nodes_label)
[PROOF STATE]
proof (state)
this:
labels prog l c'

goal (1 subgoal):
 1. lhs (label prog l) = {}
[PROOF STEP]
hence "label prog l = c'"
[PROOF STATE]
proof (prove)
using this:
labels prog l c'

goal (1 subgoal):
 1. label prog l = c'
[PROOF STEP]
by(rule labels_label)
[PROOF STATE]
proof (state)
this:
label prog l = c'

goal (1 subgoal):
 1. lhs (label prog l) = {}
[PROOF STEP]
from \<open>labels prog l c'\<close> \<open>prog \<turnstile> Label l -CEdge (p,es,rets)\<rightarrow>\<^sub>p n'\<close>
[PROOF STATE]
proof (chain)
picking this:
labels prog l c'
prog \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'
[PROOF STEP]
have "\<exists>p es rets. fst_cmd c' = Call p es rets"
[PROOF STATE]
proof (prove)
using this:
labels prog l c'
prog \<turnstile> Label l -CEdge (p, es, rets)\<rightarrow>\<^sub>p n'

goal (1 subgoal):
 1. \<exists>p es rets. fst_cmd c' = Call p es rets
[PROOF STEP]
by(rule Proc_CFG_Call_source_fst_cmd_Call)
[PROOF STATE]
proof (state)
this:
\<exists>p es rets. fst_cmd c' = Call p es rets

goal (1 subgoal):
 1. lhs (label prog l) = {}
[PROOF STEP]
with lhs_fst_cmd[of c']
[PROOF STATE]
proof (chain)
picking this:
lhs (fst_cmd c') = lhs c'
\<exists>p es rets. fst_cmd c' = Call p es rets
[PROOF STEP]
have "lhs c' = {}"
[PROOF STATE]
proof (prove)
using this:
lhs (fst_cmd c') = lhs c'
\<exists>p es rets. fst_cmd c' = Call p es rets

goal (1 subgoal):
 1. lhs c' = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lhs c' = {}

goal (1 subgoal):
 1. lhs (label prog l) = {}
[PROOF STEP]
with \<open>label prog l = c'\<close>
[PROOF STATE]
proof (chain)
picking this:
label prog l = c'
lhs c' = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
label prog l = c'
lhs c' = {}

goal (1 subgoal):
 1. lhs (label prog l) = {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lhs (label prog l) = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_procs_THE_in_procs_ins:
  "\<lbrakk>well_formed procs; (p,ins,outs,c) \<in> set procs\<rbrakk>
  \<Longrightarrow> (THE ins'. \<exists>c' outs'. (p,ins',outs',c') \<in> set procs) = ins"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_formed procs; (p, ins, outs, c) \<in> set procs\<rbrakk> \<Longrightarrow> (THE ins'. \<exists>c' outs'. (p, ins', outs', c') \<in> set procs) = ins
[PROOF STEP]
by(fastforce intro:the_equality)


[STATEMENT]
lemma Entry_Def_empty:"Def wfp (Main, Entry) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Def wfp (Main, Entry) = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Def wfp (Main, Entry) = {}
[PROOF STEP]
obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>prog procs. Rep_wf_prog wfp = (prog, procs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases "Rep_wf_prog wfp") auto
[PROOF STATE]
proof (state)
this:
Rep_wf_prog wfp = (prog, procs)

goal (1 subgoal):
 1. Def wfp (Main, Entry) = {}
[PROOF STEP]
hence "well_formed procs"
[PROOF STATE]
proof (prove)
using this:
Rep_wf_prog wfp = (prog, procs)

goal (1 subgoal):
 1. well_formed procs
[PROOF STEP]
by(fastforce intro:wf_wf_prog)
[PROOF STATE]
proof (state)
this:
well_formed procs

goal (1 subgoal):
 1. Def wfp (Main, Entry) = {}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
well_formed procs

goal (1 subgoal):
 1. Def wfp (Main, Entry) = {}
[PROOF STEP]
by(auto simp:Def_def ParamDefs_def ParamDefs_proc_def)
[PROOF STATE]
proof (state)
this:
Def wfp (Main, Entry) = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Exit_Def_empty:"Def wfp (Main, Exit) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Def wfp (Main, Exit) = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Def wfp (Main, Exit) = {}
[PROOF STEP]
obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>prog procs. Rep_wf_prog wfp = (prog, procs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases "Rep_wf_prog wfp") auto
[PROOF STATE]
proof (state)
this:
Rep_wf_prog wfp = (prog, procs)

goal (1 subgoal):
 1. Def wfp (Main, Exit) = {}
[PROOF STEP]
hence "well_formed procs"
[PROOF STATE]
proof (prove)
using this:
Rep_wf_prog wfp = (prog, procs)

goal (1 subgoal):
 1. well_formed procs
[PROOF STEP]
by(fastforce intro:wf_wf_prog)
[PROOF STATE]
proof (state)
this:
well_formed procs

goal (1 subgoal):
 1. Def wfp (Main, Exit) = {}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
well_formed procs

goal (1 subgoal):
 1. Def wfp (Main, Exit) = {}
[PROOF STEP]
by(auto dest:Proc_CFG_Call_Labels simp:Def_def ParamDefs_def ParamDefs_proc_def)
[PROOF STATE]
proof (state)
this:
Def wfp (Main, Exit) = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rhs_fst_cmd:"rhs (fst_cmd c) = rhs c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rhs (fst_cmd c) = rhs c
[PROOF STEP]
by(induct c) auto


[STATEMENT]
lemma Proc_CFG_Call_target_empty_rhs:
  assumes "prog \<turnstile> n -CEdge (p,es,rets)\<rightarrow>\<^sub>p Label l'"
  shows "rhs (label prog l') = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rhs (label prog l') = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rhs (label prog l') = {}
[PROOF STEP]
from \<open>prog \<turnstile> n -CEdge (p,es,rets)\<rightarrow>\<^sub>p Label l'\<close>
[PROOF STATE]
proof (chain)
picking this:
prog \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l'
[PROOF STEP]
have "l' < #:prog"
[PROOF STATE]
proof (prove)
using this:
prog \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l'

goal (1 subgoal):
 1. l' < #:prog
[PROOF STEP]
by(rule Proc_CFG_targetlabel_less_num_nodes)
[PROOF STATE]
proof (state)
this:
l' < #:prog

goal (1 subgoal):
 1. rhs (label prog l') = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l' < #:prog
[PROOF STEP]
obtain c' where "labels prog l' c'"
[PROOF STATE]
proof (prove)
using this:
l' < #:prog

goal (1 subgoal):
 1. (\<And>c'. labels prog l' c' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule less_num_inner_nodes_label)
[PROOF STATE]
proof (state)
this:
labels prog l' c'

goal (1 subgoal):
 1. rhs (label prog l') = {}
[PROOF STEP]
hence "label prog l' = c'"
[PROOF STATE]
proof (prove)
using this:
labels prog l' c'

goal (1 subgoal):
 1. label prog l' = c'
[PROOF STEP]
by(rule labels_label)
[PROOF STATE]
proof (state)
this:
label prog l' = c'

goal (1 subgoal):
 1. rhs (label prog l') = {}
[PROOF STEP]
from \<open>labels prog l' c'\<close> \<open>prog \<turnstile> n -CEdge (p,es,rets)\<rightarrow>\<^sub>p Label l'\<close>
[PROOF STATE]
proof (chain)
picking this:
labels prog l' c'
prog \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l'
[PROOF STEP]
have "fst_cmd c' = Skip"
[PROOF STATE]
proof (prove)
using this:
labels prog l' c'
prog \<turnstile> n -CEdge (p, es, rets)\<rightarrow>\<^sub>p Label l'

goal (1 subgoal):
 1. fst_cmd c' = Skip
[PROOF STEP]
by(rule Proc_CFG_Call_target_fst_cmd_Skip)
[PROOF STATE]
proof (state)
this:
fst_cmd c' = Skip

goal (1 subgoal):
 1. rhs (label prog l') = {}
[PROOF STEP]
with rhs_fst_cmd[of c']
[PROOF STATE]
proof (chain)
picking this:
rhs (fst_cmd c') = rhs c'
fst_cmd c' = Skip
[PROOF STEP]
have "rhs c' = {}"
[PROOF STATE]
proof (prove)
using this:
rhs (fst_cmd c') = rhs c'
fst_cmd c' = Skip

goal (1 subgoal):
 1. rhs c' = {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rhs c' = {}

goal (1 subgoal):
 1. rhs (label prog l') = {}
[PROOF STEP]
with \<open>label prog l' = c'\<close>
[PROOF STATE]
proof (chain)
picking this:
label prog l' = c'
rhs c' = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
label prog l' = c'
rhs c' = {}

goal (1 subgoal):
 1. rhs (label prog l') = {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rhs (label prog l') = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_procs_THE_in_procs_outs:
  "\<lbrakk>well_formed procs; (p,ins,outs,c) \<in> set procs\<rbrakk>
  \<Longrightarrow> (THE outs'. \<exists>c' ins'. (p,ins',outs',c') \<in> set procs) = outs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_formed procs; (p, ins, outs, c) \<in> set procs\<rbrakk> \<Longrightarrow> (THE outs'. \<exists>c' ins'. (p, ins', outs', c') \<in> set procs) = outs
[PROOF STEP]
by(fastforce intro:the_equality)


[STATEMENT]
lemma Entry_Use_empty:"Use wfp (Main, Entry) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Use wfp (Main, Entry) = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Use wfp (Main, Entry) = {}
[PROOF STEP]
obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>prog procs. Rep_wf_prog wfp = (prog, procs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases "Rep_wf_prog wfp") auto
[PROOF STATE]
proof (state)
this:
Rep_wf_prog wfp = (prog, procs)

goal (1 subgoal):
 1. Use wfp (Main, Entry) = {}
[PROOF STEP]
hence "well_formed procs"
[PROOF STATE]
proof (prove)
using this:
Rep_wf_prog wfp = (prog, procs)

goal (1 subgoal):
 1. well_formed procs
[PROOF STEP]
by(fastforce intro:wf_wf_prog)
[PROOF STATE]
proof (state)
this:
well_formed procs

goal (1 subgoal):
 1. Use wfp (Main, Entry) = {}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
well_formed procs

goal (1 subgoal):
 1. Use wfp (Main, Entry) = {}
[PROOF STEP]
by(auto dest:Proc_CFG_Call_Labels
    simp:Use_def ParamUses_def ParamUses_proc_def ParamDefs_def ParamDefs_proc_def)
[PROOF STATE]
proof (state)
this:
Use wfp (Main, Entry) = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Exit_Use_empty:"Use wfp (Main, Exit) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Use wfp (Main, Exit) = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Use wfp (Main, Exit) = {}
[PROOF STEP]
obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>prog procs. Rep_wf_prog wfp = (prog, procs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases "Rep_wf_prog wfp") auto
[PROOF STATE]
proof (state)
this:
Rep_wf_prog wfp = (prog, procs)

goal (1 subgoal):
 1. Use wfp (Main, Exit) = {}
[PROOF STEP]
hence "well_formed procs"
[PROOF STATE]
proof (prove)
using this:
Rep_wf_prog wfp = (prog, procs)

goal (1 subgoal):
 1. well_formed procs
[PROOF STEP]
by(fastforce intro:wf_wf_prog)
[PROOF STATE]
proof (state)
this:
well_formed procs

goal (1 subgoal):
 1. Use wfp (Main, Exit) = {}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
well_formed procs

goal (1 subgoal):
 1. Use wfp (Main, Exit) = {}
[PROOF STEP]
by(auto dest:Proc_CFG_Call_Labels
    simp:Use_def ParamUses_def ParamUses_proc_def ParamDefs_def ParamDefs_proc_def)
[PROOF STATE]
proof (state)
this:
Use wfp (Main, Exit) = {}

goal:
No subgoals!
[PROOF STEP]
qed