[STATEMENT]
lemma valid_stepI [intro]:
  "revision_step r s s' \<Longrightarrow> s \<leadsto> s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. revision_step r s s' \<Longrightarrow> s \<leadsto> s'
[PROOF STEP]
using steps_def
[PROOF STATE]
proof (prove)
using this:
[\<leadsto>] = {(s, s') |s s'. \<exists>r. revision_step r s s'}

goal (1 subgoal):
 1. revision_step r s s' \<Longrightarrow> s \<leadsto> s'
[PROOF STEP]
by auto


[STATEMENT]
lemma valid_stepE [dest]:
  "s \<leadsto> s' \<Longrightarrow> \<exists>r. revision_step r s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<leadsto> s' \<Longrightarrow> \<exists>r. revision_step r s s'
[PROOF STEP]
by (simp add: steps_def)


[STATEMENT]
lemma refl_rewritesI [intro]: "s \<leadsto> s' \<Longrightarrow> s \<leadsto>\<^sup>= s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<leadsto> s' \<Longrightarrow> (s, s') \<in> [\<leadsto>]\<^sup>=
[PROOF STEP]
by blast


[STATEMENT]
lemma inductive_invariantI [intro]:
  "(\<And>s. initial_state s \<Longrightarrow> P s) \<Longrightarrow> (\<And>s s'. s \<leadsto> s' \<Longrightarrow> P s \<Longrightarrow> P s') \<Longrightarrow> inductive_invariant P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<exists>e r. s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e \<Longrightarrow> P s; \<And>s s'. \<lbrakk>s \<leadsto> s'; P s\<rbrakk> \<Longrightarrow> P s'\<rbrakk> \<Longrightarrow> inductive_invariant P
[PROOF STEP]
by (auto simp add: inductive_invariant_def)


[STATEMENT]
lemma inductive_invariant_is_execution_invariant: "reachable s \<Longrightarrow> inductive_invariant P \<Longrightarrow> P s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; inductive_invariant P\<rbrakk> \<Longrightarrow> P s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>reachable s; inductive_invariant P\<rbrakk> \<Longrightarrow> P s
[PROOF STEP]
assume reach: "reachable s" and ind_inv: "inductive_invariant P"
[PROOF STATE]
proof (state)
this:
reachable s
inductive_invariant P

goal (1 subgoal):
 1. \<lbrakk>reachable s; inductive_invariant P\<rbrakk> \<Longrightarrow> P s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
reachable s
inductive_invariant P
[PROOF STEP]
obtain e initial n where initializes: "initializes initial e" and trace: "(initial,s) \<in> [\<leadsto>]^^n"
[PROOF STATE]
proof (prove)
using this:
reachable s
inductive_invariant P

goal (1 subgoal):
 1. (\<And>initial e n. \<lbrakk>\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis execution_def reachable_def rtrancl_power)
[PROOF STATE]
proof (state)
this:
\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e
(initial, s) \<in> [\<leadsto>] ^^ n

goal (1 subgoal):
 1. \<lbrakk>reachable s; inductive_invariant P\<rbrakk> \<Longrightarrow> P s
[PROOF STEP]
thus "P s"
[PROOF STATE]
proof (prove)
using this:
\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e
(initial, s) \<in> [\<leadsto>] ^^ n

goal (1 subgoal):
 1. P s
[PROOF STEP]
proof (induct n arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ 0\<rbrakk> \<Longrightarrow> P s
 2. \<And>n s. \<lbrakk>\<And>s. \<lbrakk>\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ n\<rbrakk> \<Longrightarrow> P s; \<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> P s
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e
(initial, s) \<in> [\<leadsto>] ^^ 0

goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ 0\<rbrakk> \<Longrightarrow> P s
 2. \<And>n s. \<lbrakk>\<And>s. \<lbrakk>\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ n\<rbrakk> \<Longrightarrow> P s; \<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> P s
[PROOF STEP]
have "initial = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. initial = s
[PROOF STEP]
using "0.prems"(2)
[PROOF STATE]
proof (prove)
using this:
(initial, s) \<in> [\<leadsto>] ^^ 0

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

goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ 0\<rbrakk> \<Longrightarrow> P s
 2. \<And>n s. \<lbrakk>\<And>s. \<lbrakk>\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ n\<rbrakk> \<Longrightarrow> P s; \<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> P s
[PROOF STEP]
hence "initial_state s"
[PROOF STATE]
proof (prove)
using this:
initial = s

goal (1 subgoal):
 1. \<exists>e r. s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e
[PROOF STEP]
using initializes
[PROOF STATE]
proof (prove)
using this:
initial = s
\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e

goal (1 subgoal):
 1. \<exists>e r. s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>e r. s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e

goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ 0\<rbrakk> \<Longrightarrow> P s
 2. \<And>n s. \<lbrakk>\<And>s. \<lbrakk>\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ n\<rbrakk> \<Longrightarrow> P s; \<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> P s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>e r. s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>e r. s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e

goal (1 subgoal):
 1. P s
[PROOF STEP]
using ind_inv inductive_invariant_def
[PROOF STATE]
proof (prove)
using this:
\<exists>e r. s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e
inductive_invariant P
inductive_invariant ?P \<equiv> (\<forall>s. (\<exists>e r. s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e) \<longrightarrow> ?P s) \<and> (\<forall>s s'. s \<leadsto> s' \<longrightarrow> ?P s \<longrightarrow> ?P s')

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

goal (1 subgoal):
 1. \<And>n s. \<lbrakk>\<And>s. \<lbrakk>\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ n\<rbrakk> \<Longrightarrow> P s; \<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> P s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n s. \<lbrakk>\<And>s. \<lbrakk>\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ n\<rbrakk> \<Longrightarrow> P s; \<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> P s
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, ?s) \<in> [\<leadsto>] ^^ n\<rbrakk> \<Longrightarrow> P ?s
\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e
(initial, s) \<in> [\<leadsto>] ^^ Suc n

goal (1 subgoal):
 1. \<And>n s. \<lbrakk>\<And>s. \<lbrakk>\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ n\<rbrakk> \<Longrightarrow> P s; \<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> P s
[PROOF STEP]
obtain s' where nfold: "(initial, s') \<in> [\<leadsto>]^^n" and step: "s' \<leadsto> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s'. \<lbrakk>(initial, s') \<in> [\<leadsto>] ^^ n; s' \<leadsto> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Suc.prems(2)
[PROOF STATE]
proof (prove)
using this:
(initial, s) \<in> [\<leadsto>] ^^ Suc n

goal (1 subgoal):
 1. (\<And>s'. \<lbrakk>(initial, s') \<in> [\<leadsto>] ^^ n; s' \<leadsto> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(initial, s') \<in> [\<leadsto>] ^^ n
s' \<leadsto> s

goal (1 subgoal):
 1. \<And>n s. \<lbrakk>\<And>s. \<lbrakk>\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ n\<rbrakk> \<Longrightarrow> P s; \<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> P s
[PROOF STEP]
have "P s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P s'
[PROOF STEP]
using Suc(1) nfold initializes
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, ?s) \<in> [\<leadsto>] ^^ n\<rbrakk> \<Longrightarrow> P ?s
(initial, s') \<in> [\<leadsto>] ^^ n
\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e

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

goal (1 subgoal):
 1. \<And>n s. \<lbrakk>\<And>s. \<lbrakk>\<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ n\<rbrakk> \<Longrightarrow> P s; \<exists>r. initial = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e; (initial, s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> P s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P s'

goal (1 subgoal):
 1. P s
[PROOF STEP]
using ind_inv step inductive_invariant_def
[PROOF STATE]
proof (prove)
using this:
P s'
inductive_invariant P
s' \<leadsto> s
inductive_invariant ?P \<equiv> (\<forall>s. (\<exists>e r. s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e) \<longrightarrow> ?P s) \<and> (\<forall>s s'. s \<leadsto> s' \<longrightarrow> ?P s \<longrightarrow> ?P s')

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nice_ind_inv_is_inductive_invariant: "inductive_invariant (\<lambda>s. \<S>\<^sub>G s \<and> \<A>\<^sub>G s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inductive_invariant (\<lambda>s. \<S>\<^sub>G s \<and> \<A>\<^sub>G s)
[PROOF STEP]
proof (rule inductive_invariantI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<exists>e r. s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e \<Longrightarrow> \<S>\<^sub>G s \<and> \<A>\<^sub>G s
 2. \<And>s s'. \<lbrakk>s \<leadsto> s'; \<S>\<^sub>G s \<and> \<A>\<^sub>G s\<rbrakk> \<Longrightarrow> \<S>\<^sub>G s' \<and> \<A>\<^sub>G s'
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<exists>e r. s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e \<Longrightarrow> \<S>\<^sub>G s \<and> \<A>\<^sub>G s
 2. \<And>s s'. \<lbrakk>s \<leadsto> s'; \<S>\<^sub>G s \<and> \<A>\<^sub>G s\<rbrakk> \<Longrightarrow> \<S>\<^sub>G s' \<and> \<A>\<^sub>G s'
[PROOF STEP]
assume "initial_state s"
[PROOF STATE]
proof (state)
this:
\<exists>e r. s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e

goal (2 subgoals):
 1. \<And>s. \<exists>e r. s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e \<Longrightarrow> \<S>\<^sub>G s \<and> \<A>\<^sub>G s
 2. \<And>s s'. \<lbrakk>s \<leadsto> s'; \<S>\<^sub>G s \<and> \<A>\<^sub>G s\<rbrakk> \<Longrightarrow> \<S>\<^sub>G s' \<and> \<A>\<^sub>G s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>e r. s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e
[PROOF STEP]
obtain e r where s: "s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))" and prog_expr_e: "program_expr e"
[PROOF STATE]
proof (prove)
using this:
\<exists>e r. s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e

goal (1 subgoal):
 1. (\<And>r e. \<lbrakk>s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)); program_expr e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))
program_expr e

goal (2 subgoals):
 1. \<And>s. \<exists>e r. s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e \<Longrightarrow> \<S>\<^sub>G s \<and> \<A>\<^sub>G s
 2. \<And>s s'. \<lbrakk>s \<leadsto> s'; \<S>\<^sub>G s \<and> \<A>\<^sub>G s\<rbrakk> \<Longrightarrow> \<S>\<^sub>G s' \<and> \<A>\<^sub>G s'
[PROOF STEP]
show "\<S>\<^sub>G s \<and> \<A>\<^sub>G s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<S>\<^sub>G s \<and> \<A>\<^sub>G s
[PROOF STEP]
proof (rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<S>\<^sub>G s
 2. \<A>\<^sub>G s
[PROOF STEP]
show "\<S>\<^sub>G s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<S>\<^sub>G s
[PROOF STEP]
proof (rule domains_subsume_globallyI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r \<sigma> \<tau> e. s r = Some (\<sigma>, \<tau>, e) \<Longrightarrow> \<S> (\<sigma>, \<tau>, e)
[PROOF STEP]
fix r' \<sigma>' \<tau>' e'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r \<sigma> \<tau> e. s r = Some (\<sigma>, \<tau>, e) \<Longrightarrow> \<S> (\<sigma>, \<tau>, e)
[PROOF STEP]
assume s_r': "s r' = Some (\<sigma>',\<tau>',e')"
[PROOF STATE]
proof (state)
this:
s r' = Some (\<sigma>', \<tau>', e')

goal (1 subgoal):
 1. \<And>r \<sigma> \<tau> e. s r = Some (\<sigma>, \<tau>, e) \<Longrightarrow> \<S> (\<sigma>, \<tau>, e)
[PROOF STEP]
have "r' = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r' = r
[PROOF STEP]
using s s_r' prog_expr_e
[PROOF STATE]
proof (prove)
using this:
s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))
s r' = Some (\<sigma>', \<tau>', e')
program_expr e

goal (1 subgoal):
 1. r' = r
[PROOF STEP]
by (meson domI domIff fun_upd_other)
[PROOF STATE]
proof (state)
this:
r' = r

goal (1 subgoal):
 1. \<And>r \<sigma> \<tau> e. s r = Some (\<sigma>, \<tau>, e) \<Longrightarrow> \<S> (\<sigma>, \<tau>, e)
[PROOF STEP]
hence "LID\<^sub>L (\<sigma>',\<tau>',e') = LID\<^sub>L (\<epsilon>, \<epsilon>, e)"
[PROOF STATE]
proof (prove)
using this:
r' = r

goal (1 subgoal):
 1. LID\<^sub>L (\<sigma>', \<tau>', e') = LID\<^sub>L (\<epsilon>, \<epsilon>, e)
[PROOF STEP]
using s s_r'
[PROOF STATE]
proof (prove)
using this:
r' = r
s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))
s r' = Some (\<sigma>', \<tau>', e')

goal (1 subgoal):
 1. LID\<^sub>L (\<sigma>', \<tau>', e') = LID\<^sub>L (\<epsilon>, \<epsilon>, e)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
LID\<^sub>L (\<sigma>', \<tau>', e') = LID\<^sub>L (\<epsilon>, \<epsilon>, e)

goal (1 subgoal):
 1. \<And>r \<sigma> \<tau> e. s r = Some (\<sigma>, \<tau>, e) \<Longrightarrow> \<S> (\<sigma>, \<tau>, e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LID\<^sub>L (\<sigma>', \<tau>', e') = LID\<^sub>L (\<epsilon>, \<epsilon>, e)

goal (1 subgoal):
 1. \<And>r \<sigma> \<tau> e. s r = Some (\<sigma>, \<tau>, e) \<Longrightarrow> \<S> (\<sigma>, \<tau>, e)
[PROOF STEP]
have "... = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LID\<^sub>L (\<epsilon>, \<epsilon>, e) = {}
[PROOF STEP]
using prog_expr_e
[PROOF STATE]
proof (prove)
using this:
program_expr e

goal (1 subgoal):
 1. LID\<^sub>L (\<epsilon>, \<epsilon>, e) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
LID\<^sub>L (\<epsilon>, \<epsilon>, e) = {}

goal (1 subgoal):
 1. \<And>r \<sigma> \<tau> e. s r = Some (\<sigma>, \<tau>, e) \<Longrightarrow> \<S> (\<sigma>, \<tau>, e)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LID\<^sub>L (\<epsilon>, \<epsilon>, e) = {}

goal (1 subgoal):
 1. \<And>r \<sigma> \<tau> e. s r = Some (\<sigma>, \<tau>, e) \<Longrightarrow> \<S> (\<sigma>, \<tau>, e)
[PROOF STEP]
have "... = dom \<sigma>' \<union> dom \<tau>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} = dom \<sigma>' \<union> dom \<tau>'
[PROOF STEP]
using \<open>r' = r\<close> s s_r'
[PROOF STATE]
proof (prove)
using this:
r' = r
s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))
s r' = Some (\<sigma>', \<tau>', e')

goal (1 subgoal):
 1. {} = dom \<sigma>' \<union> dom \<tau>'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{} = dom \<sigma>' \<union> dom \<tau>'

goal (1 subgoal):
 1. \<And>r \<sigma> \<tau> e. s r = Some (\<sigma>, \<tau>, e) \<Longrightarrow> \<S> (\<sigma>, \<tau>, e)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
LID\<^sub>L (\<sigma>', \<tau>', e') = dom \<sigma>' \<union> dom \<tau>'
[PROOF STEP]
show "\<S> (\<sigma>', \<tau>', e')"
[PROOF STATE]
proof (prove)
using this:
LID\<^sub>L (\<sigma>', \<tau>', e') = dom \<sigma>' \<union> dom \<tau>'

goal (1 subgoal):
 1. \<S> (\<sigma>', \<tau>', e')
[PROOF STEP]
by (simp add: domains_subsume_def)
[PROOF STATE]
proof (state)
this:
\<S> (\<sigma>', \<tau>', e')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<S>\<^sub>G s

goal (1 subgoal):
 1. \<A>\<^sub>G s
[PROOF STEP]
show "\<A>\<^sub>G s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<A>\<^sub>G s
[PROOF STEP]
proof (rule subsumes_accessible_globallyI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r\<^sub>1 \<sigma>\<^sub>1 \<tau>\<^sub>1 e\<^sub>1 r\<^sub>2 \<sigma>\<^sub>2 \<tau>\<^sub>2 e\<^sub>2. \<lbrakk>s r\<^sub>1 = Some (\<sigma>\<^sub>1, \<tau>\<^sub>1, e\<^sub>1); s r\<^sub>2 = Some (\<sigma>\<^sub>2, \<tau>\<^sub>2, e\<^sub>2)\<rbrakk> \<Longrightarrow> \<A> r\<^sub>1 r\<^sub>2 s
[PROOF STEP]
fix r\<^sub>1 \<sigma>\<^sub>1 \<tau>\<^sub>1 e\<^sub>1 r\<^sub>2 \<sigma>\<^sub>2 \<tau>\<^sub>2 e\<^sub>2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r\<^sub>1 \<sigma>\<^sub>1 \<tau>\<^sub>1 e\<^sub>1 r\<^sub>2 \<sigma>\<^sub>2 \<tau>\<^sub>2 e\<^sub>2. \<lbrakk>s r\<^sub>1 = Some (\<sigma>\<^sub>1, \<tau>\<^sub>1, e\<^sub>1); s r\<^sub>2 = Some (\<sigma>\<^sub>2, \<tau>\<^sub>2, e\<^sub>2)\<rbrakk> \<Longrightarrow> \<A> r\<^sub>1 r\<^sub>2 s
[PROOF STEP]
assume s_r1: "s r\<^sub>1 = Some (\<sigma>\<^sub>1, \<tau>\<^sub>1, e\<^sub>1)" and s_r2: "s r\<^sub>2 = Some (\<sigma>\<^sub>2, \<tau>\<^sub>2, e\<^sub>2)"
[PROOF STATE]
proof (state)
this:
s r\<^sub>1 = Some (\<sigma>\<^sub>1, \<tau>\<^sub>1, e\<^sub>1)
s r\<^sub>2 = Some (\<sigma>\<^sub>2, \<tau>\<^sub>2, e\<^sub>2)

goal (1 subgoal):
 1. \<And>r\<^sub>1 \<sigma>\<^sub>1 \<tau>\<^sub>1 e\<^sub>1 r\<^sub>2 \<sigma>\<^sub>2 \<tau>\<^sub>2 e\<^sub>2. \<lbrakk>s r\<^sub>1 = Some (\<sigma>\<^sub>1, \<tau>\<^sub>1, e\<^sub>1); s r\<^sub>2 = Some (\<sigma>\<^sub>2, \<tau>\<^sub>2, e\<^sub>2)\<rbrakk> \<Longrightarrow> \<A> r\<^sub>1 r\<^sub>2 s
[PROOF STEP]
have "r\<^sub>2 = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r\<^sub>2 = r
[PROOF STEP]
using s s_r2 prog_expr_e
[PROOF STATE]
proof (prove)
using this:
s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))
s r\<^sub>2 = Some (\<sigma>\<^sub>2, \<tau>\<^sub>2, e\<^sub>2)
program_expr e

goal (1 subgoal):
 1. r\<^sub>2 = r
[PROOF STEP]
by (meson domI domIff fun_upd_other)
[PROOF STATE]
proof (state)
this:
r\<^sub>2 = r

goal (1 subgoal):
 1. \<And>r\<^sub>1 \<sigma>\<^sub>1 \<tau>\<^sub>1 e\<^sub>1 r\<^sub>2 \<sigma>\<^sub>2 \<tau>\<^sub>2 e\<^sub>2. \<lbrakk>s r\<^sub>1 = Some (\<sigma>\<^sub>1, \<tau>\<^sub>1, e\<^sub>1); s r\<^sub>2 = Some (\<sigma>\<^sub>2, \<tau>\<^sub>2, e\<^sub>2)\<rbrakk> \<Longrightarrow> \<A> r\<^sub>1 r\<^sub>2 s
[PROOF STEP]
hence "\<sigma>\<^sub>2 = \<epsilon>"
[PROOF STATE]
proof (prove)
using this:
r\<^sub>2 = r

goal (1 subgoal):
 1. \<sigma>\<^sub>2 = \<epsilon>
[PROOF STEP]
using s s_r2
[PROOF STATE]
proof (prove)
using this:
r\<^sub>2 = r
s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))
s r\<^sub>2 = Some (\<sigma>\<^sub>2, \<tau>\<^sub>2, e\<^sub>2)

goal (1 subgoal):
 1. \<sigma>\<^sub>2 = \<epsilon>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma>\<^sub>2 = \<epsilon>

goal (1 subgoal):
 1. \<And>r\<^sub>1 \<sigma>\<^sub>1 \<tau>\<^sub>1 e\<^sub>1 r\<^sub>2 \<sigma>\<^sub>2 \<tau>\<^sub>2 e\<^sub>2. \<lbrakk>s r\<^sub>1 = Some (\<sigma>\<^sub>1, \<tau>\<^sub>1, e\<^sub>1); s r\<^sub>2 = Some (\<sigma>\<^sub>2, \<tau>\<^sub>2, e\<^sub>2)\<rbrakk> \<Longrightarrow> \<A> r\<^sub>1 r\<^sub>2 s
[PROOF STEP]
hence "LID\<^sub>S \<sigma>\<^sub>2 = {}"
[PROOF STATE]
proof (prove)
using this:
\<sigma>\<^sub>2 = \<epsilon>

goal (1 subgoal):
 1. LID\<^sub>S \<sigma>\<^sub>2 = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
LID\<^sub>S \<sigma>\<^sub>2 = {}

goal (1 subgoal):
 1. \<And>r\<^sub>1 \<sigma>\<^sub>1 \<tau>\<^sub>1 e\<^sub>1 r\<^sub>2 \<sigma>\<^sub>2 \<tau>\<^sub>2 e\<^sub>2. \<lbrakk>s r\<^sub>1 = Some (\<sigma>\<^sub>1, \<tau>\<^sub>1, e\<^sub>1); s r\<^sub>2 = Some (\<sigma>\<^sub>2, \<tau>\<^sub>2, e\<^sub>2)\<rbrakk> \<Longrightarrow> \<A> r\<^sub>1 r\<^sub>2 s
[PROOF STEP]
thus "\<A> r\<^sub>1 r\<^sub>2 s"
[PROOF STATE]
proof (prove)
using this:
LID\<^sub>S \<sigma>\<^sub>2 = {}

goal (1 subgoal):
 1. \<A> r\<^sub>1 r\<^sub>2 s
[PROOF STEP]
using s_r2
[PROOF STATE]
proof (prove)
using this:
LID\<^sub>S \<sigma>\<^sub>2 = {}
s r\<^sub>2 = Some (\<sigma>\<^sub>2, \<tau>\<^sub>2, e\<^sub>2)

goal (1 subgoal):
 1. \<A> r\<^sub>1 r\<^sub>2 s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<A> r\<^sub>1 r\<^sub>2 s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<A>\<^sub>G s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<S>\<^sub>G s \<and> \<A>\<^sub>G s

goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s \<leadsto> s'; \<S>\<^sub>G s \<and> \<A>\<^sub>G s\<rbrakk> \<Longrightarrow> \<S>\<^sub>G s' \<and> \<A>\<^sub>G s'
[PROOF STEP]
qed (use step_preserves_\<S>\<^sub>G_and_\<A>\<^sub>G in auto)


[STATEMENT]
lemma transition_relations_equivalent: "reachable s \<Longrightarrow> revision_step r s s' = revision_step_relaxed r s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> revision_step r s s' = revision_step_relaxed r s s'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> revision_step r s s' = revision_step_relaxed r s s'
[PROOF STEP]
assume reach: "reachable s"
[PROOF STATE]
proof (state)
this:
reachable s

goal (1 subgoal):
 1. reachable s \<Longrightarrow> revision_step r s s' = revision_step_relaxed r s s'
[PROOF STEP]
have doms_sub_local: "\<S>\<^sub>G s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<S>\<^sub>G s
[PROOF STEP]
by (rule reachable_imp_\<S>\<^sub>G[OF reach])
[PROOF STATE]
proof (state)
this:
\<S>\<^sub>G s

goal (1 subgoal):
 1. reachable s \<Longrightarrow> revision_step r s s' = revision_step_relaxed r s s'
[PROOF STEP]
show "revision_step r s s' = revision_step_relaxed r s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. revision_step r s s' = revision_step_relaxed r s s'
[PROOF STEP]
proof (rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. revision_step r s s' \<Longrightarrow> revision_step_relaxed r s s'
 2. revision_step_relaxed r s s' \<Longrightarrow> revision_step r s s'
[PROOF STEP]
assume step: "revision_step r s s'"
[PROOF STATE]
proof (state)
this:
revision_step r s s'

goal (2 subgoals):
 1. revision_step r s s' \<Longrightarrow> revision_step_relaxed r s s'
 2. revision_step_relaxed r s s' \<Longrightarrow> revision_step r s s'
[PROOF STEP]
show "revision_step_relaxed r s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. revision_step_relaxed r s s'
[PROOF STEP]
proof (use step in \<open>induct rule: revision_stepE\<close>)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 4. \<And>\<sigma> \<tau> \<E> v l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])); s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)]); l \<notin> LID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 5. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 6. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 7. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 8. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 9. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
[PROOF STEP]
case (new \<sigma> \<tau> \<E> v l)
[PROOF STATE]
proof (state)
this:
s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)]))
s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)])
l \<notin> LID\<^sub>G s

goal (9 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 4. \<And>\<sigma> \<tau> \<E> v l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])); s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)]); l \<notin> LID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 5. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 6. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 7. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 8. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 9. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
[PROOF STEP]
have "revision_step_relaxed r s (s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. revision_step_relaxed r s (s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])))
[PROOF STEP]
proof (rule revision_step_relaxed.new)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)])
 2. l \<notin> \<Union> {doms ls |ls. ls \<in> ran s}
[PROOF STEP]
show "l \<notin> \<Union> { doms ls | ls. ls \<in> ran s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<notin> \<Union> {doms ls |ls. ls \<in> ran s}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<in> \<Union> {doms ls |ls. ls \<in> ran s} \<Longrightarrow> False
[PROOF STEP]
assume "l \<in> \<Union> { doms ls | ls. ls \<in> ran s}"
[PROOF STATE]
proof (state)
this:
l \<in> \<Union> {doms ls |ls. ls \<in> ran s}

goal (1 subgoal):
 1. l \<in> \<Union> {doms ls |ls. ls \<in> ran s} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<in> \<Union> {doms ls |ls. ls \<in> ran s}
[PROOF STEP]
obtain ls where in_ran: "ls \<in> ran s" and in_doms: "l \<in> doms ls"
[PROOF STATE]
proof (prove)
using this:
l \<in> \<Union> {doms ls |ls. ls \<in> ran s}

goal (1 subgoal):
 1. (\<And>ls. \<lbrakk>ls \<in> ran s; l \<in> doms ls\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ls \<in> ran s
l \<in> doms ls

goal (1 subgoal):
 1. l \<in> \<Union> {doms ls |ls. ls \<in> ran s} \<Longrightarrow> False
[PROOF STEP]
from in_doms
[PROOF STATE]
proof (chain)
picking this:
l \<in> doms ls
[PROOF STEP]
have "l \<in> LID\<^sub>L ls"
[PROOF STATE]
proof (prove)
using this:
l \<in> doms ls

goal (1 subgoal):
 1. l \<in> LID\<^sub>L ls
[PROOF STEP]
by (cases ls) auto
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>L ls

goal (1 subgoal):
 1. l \<in> \<Union> {doms ls |ls. ls \<in> ran s} \<Longrightarrow> False
[PROOF STEP]
have "l \<in> LID\<^sub>G s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<in> LID\<^sub>G s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<in> LID\<^sub>G s
[PROOF STEP]
have "ls \<in> {ls. \<exists>r. s r = Some ls}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ls \<in> {ls. \<exists>r. s r = Some ls}
[PROOF STEP]
by (metis (full_types) in_ran ran_def)
[PROOF STATE]
proof (state)
this:
ls \<in> {ls. \<exists>r. s r = Some ls}

goal (1 subgoal):
 1. l \<in> LID\<^sub>G s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ls \<in> {ls. \<exists>r. s r = Some ls}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ls \<in> {ls. \<exists>r. s r = Some ls}

goal (1 subgoal):
 1. l \<in> LID\<^sub>G s
[PROOF STEP]
using \<open>l \<in> LID\<^sub>L ls\<close>
[PROOF STATE]
proof (prove)
using this:
ls \<in> {ls. \<exists>r. s r = Some ls}
l \<in> LID\<^sub>L ls

goal (1 subgoal):
 1. l \<in> LID\<^sub>G s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>G s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>G s

goal (1 subgoal):
 1. l \<in> \<Union> {doms ls |ls. ls \<in> ran s} \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
l \<in> LID\<^sub>G s

goal (1 subgoal):
 1. False
[PROOF STEP]
using new
[PROOF STATE]
proof (prove)
using this:
l \<in> LID\<^sub>G s
s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)]))
s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)])
l \<notin> LID\<^sub>G s

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l \<notin> \<Union> {doms ls |ls. ls \<in> ran s}

goal (1 subgoal):
 1. s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)])
[PROOF STEP]
qed (simp add: new.hyps(2))
[PROOF STATE]
proof (state)
this:
revision_step_relaxed r s (s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])))

goal (9 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 4. \<And>\<sigma> \<tau> \<E> v l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])); s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)]); l \<notin> LID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 5. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 6. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 7. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 8. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 9. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
revision_step_relaxed r s (s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])))

goal (1 subgoal):
 1. revision_step_relaxed r s s'
[PROOF STEP]
using new.hyps(1)
[PROOF STATE]
proof (prove)
using this:
revision_step_relaxed r s (s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])))
s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)]))

goal (1 subgoal):
 1. revision_step_relaxed r s s'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
revision_step_relaxed r s s'

goal (8 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 4. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 5. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 6. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 7. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
 8. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> revision_step_relaxed r s s'
[PROOF STEP]
qed (use revision_step_relaxed.intros in simp)+
[PROOF STATE]
proof (state)
this:
revision_step_relaxed r s s'

goal (1 subgoal):
 1. revision_step_relaxed r s s' \<Longrightarrow> revision_step r s s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. revision_step_relaxed r s s' \<Longrightarrow> revision_step r s s'
[PROOF STEP]
assume step: "revision_step_relaxed r s s'"
[PROOF STATE]
proof (state)
this:
revision_step_relaxed r s s'

goal (1 subgoal):
 1. revision_step_relaxed r s s' \<Longrightarrow> revision_step r s s'
[PROOF STEP]
show "revision_step r s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. revision_step r s s'
[PROOF STEP]
proof (use step in \<open>induct rule: revision_step_relaxedE\<close>)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 4. \<And>\<sigma> \<tau> \<E> v l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])); s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)]); \<forall>x. (\<forall>a aa. x = dom a \<union> dom aa \<longrightarrow> (\<forall>b. (a, aa, b) \<notin> ran s)) \<or> l \<notin> x\<rbrakk> \<Longrightarrow> revision_step r s s'
 5. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])\<rbrakk> \<Longrightarrow> revision_step r s s'
 6. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 7. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step r s s'
 8. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> revision_step r s s'
 9. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> revision_step r s s'
[PROOF STEP]
case (new \<sigma> \<tau> \<E> v l)
[PROOF STATE]
proof (state)
this:
s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)]))
s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)])
\<forall>x. (\<forall>a aa. x = dom a \<union> dom aa \<longrightarrow> (\<forall>b. (a, aa, b) \<notin> ran s)) \<or> l \<notin> x

goal (9 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 4. \<And>\<sigma> \<tau> \<E> v l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])); s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)]); \<forall>x. (\<forall>a aa. x = dom a \<union> dom aa \<longrightarrow> (\<forall>b. (a, aa, b) \<notin> ran s)) \<or> l \<notin> x\<rbrakk> \<Longrightarrow> revision_step r s s'
 5. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])\<rbrakk> \<Longrightarrow> revision_step r s s'
 6. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 7. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step r s s'
 8. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> revision_step r s s'
 9. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> revision_step r s s'
[PROOF STEP]
have "revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])))
[PROOF STEP]
proof (rule revision_step.new)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)])
 2. l \<notin> LID\<^sub>G s
[PROOF STEP]
show "s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)])
[PROOF STEP]
by (simp add: new.hyps(2))
[PROOF STATE]
proof (state)
this:
s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)])

goal (1 subgoal):
 1. l \<notin> LID\<^sub>G s
[PROOF STEP]
show "l \<notin> LID\<^sub>G s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<notin> LID\<^sub>G s
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<in> LID\<^sub>G s \<Longrightarrow> False
[PROOF STEP]
assume "l \<in> LID\<^sub>G s"
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>G s

goal (1 subgoal):
 1. l \<in> LID\<^sub>G s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<in> LID\<^sub>G s
[PROOF STEP]
obtain r' \<sigma>' \<tau>' e' where s_r': "s r' = Some (\<sigma>',\<tau>',e')" and l_in_local: "l \<in> LID\<^sub>L (\<sigma>',\<tau>',e')"
[PROOF STATE]
proof (prove)
using this:
l \<in> LID\<^sub>G s

goal (1 subgoal):
 1. (\<And>r' \<sigma>' \<tau>' e'. \<lbrakk>s r' = Some (\<sigma>', \<tau>', e'); l \<in> LID\<^sub>L (\<sigma>', \<tau>', e')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s r' = Some (\<sigma>', \<tau>', e')
l \<in> LID\<^sub>L (\<sigma>', \<tau>', e')

goal (1 subgoal):
 1. l \<in> LID\<^sub>G s \<Longrightarrow> False
[PROOF STEP]
hence "l \<in> dom \<sigma>' \<union> dom \<tau>'"
[PROOF STATE]
proof (prove)
using this:
s r' = Some (\<sigma>', \<tau>', e')
l \<in> LID\<^sub>L (\<sigma>', \<tau>', e')

goal (1 subgoal):
 1. l \<in> dom \<sigma>' \<union> dom \<tau>'
[PROOF STEP]
by (metis (no_types, lifting) domains_subsume_def domains_subsume_globally_def doms.simps doms_sub_local rev_subsetD)
[PROOF STATE]
proof (state)
this:
l \<in> dom \<sigma>' \<union> dom \<tau>'

goal (1 subgoal):
 1. l \<in> LID\<^sub>G s \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
l \<in> dom \<sigma>' \<union> dom \<tau>'

goal (1 subgoal):
 1. False
[PROOF STEP]
by (meson s_r' new.hyps(3) ranI)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l \<notin> LID\<^sub>G s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])))

goal (9 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 4. \<And>\<sigma> \<tau> \<E> v l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])); s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)]); \<forall>x. (\<forall>a aa. x = dom a \<union> dom aa \<longrightarrow> (\<forall>b. (a, aa, b) \<notin> ran s)) \<or> l \<notin> x\<rbrakk> \<Longrightarrow> revision_step r s s'
 5. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])\<rbrakk> \<Longrightarrow> revision_step r s s'
 6. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 7. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step r s s'
 8. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> revision_step r s s'
 9. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> revision_step r s s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])))

goal (1 subgoal):
 1. revision_step r s s'
[PROOF STEP]
using new.hyps(1)
[PROOF STATE]
proof (prove)
using this:
revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])))
s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)]))

goal (1 subgoal):
 1. revision_step r s s'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
revision_step r s s'

goal (8 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 4. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])\<rbrakk> \<Longrightarrow> revision_step r s s'
 5. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 6. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step r s s'
 7. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> revision_step r s s'
 8. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> revision_step r s s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 4. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])\<rbrakk> \<Longrightarrow> revision_step r s s'
 5. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 6. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step r s s'
 7. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> revision_step r s s'
 8. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> revision_step r s s'
[PROOF STEP]
case (get \<sigma> \<tau> \<E> l)
[PROOF STATE]
proof (state)
this:
s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))]))
s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])

goal (8 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 4. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])\<rbrakk> \<Longrightarrow> revision_step r s s'
 5. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 6. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step r s s'
 7. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> revision_step r s s'
 8. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> revision_step r s s'
[PROOF STEP]
have "revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the ((\<sigma>;;\<tau>) l))])))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the ((\<sigma>;;\<tau>) l))])))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])
 2. l \<in> dom (\<sigma>;;\<tau>)
[PROOF STEP]
show "s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])
[PROOF STEP]
by (simp add: get.hyps(2))
[PROOF STATE]
proof (state)
this:
s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])

goal (1 subgoal):
 1. l \<in> dom (\<sigma>;;\<tau>)
[PROOF STEP]
show "l \<in> dom (\<sigma>;;\<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<in> dom (\<sigma>;;\<tau>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<in> dom (\<sigma>;;\<tau>)
[PROOF STEP]
have "l \<in> LID\<^sub>L (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<in> LID\<^sub>L (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>L (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])

goal (1 subgoal):
 1. l \<in> dom (\<sigma>;;\<tau>)
[PROOF STEP]
hence "l \<in> dom \<sigma> \<union> dom \<tau>"
[PROOF STATE]
proof (prove)
using this:
l \<in> LID\<^sub>L (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])

goal (1 subgoal):
 1. l \<in> dom \<sigma> \<union> dom \<tau>
[PROOF STEP]
using domains_subsume_def domains_subsume_globally_def doms_sub_local get.hyps(2)
[PROOF STATE]
proof (prove)
using this:
l \<in> LID\<^sub>L (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])
\<S> ?ls = (LID\<^sub>L ?ls \<subseteq> doms ?ls)
\<S>\<^sub>G ?s = (\<forall>r ls. ?s r = Some ls \<longrightarrow> \<S> ls)
\<S>\<^sub>G s
s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])

goal (1 subgoal):
 1. l \<in> dom \<sigma> \<union> dom \<tau>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
l \<in> dom \<sigma> \<union> dom \<tau>

goal (1 subgoal):
 1. l \<in> dom (\<sigma>;;\<tau>)
[PROOF STEP]
thus "l \<in> dom (\<sigma>;;\<tau>)"
[PROOF STATE]
proof (prove)
using this:
l \<in> dom \<sigma> \<union> dom \<tau>

goal (1 subgoal):
 1. l \<in> dom (\<sigma>;;\<tau>)
[PROOF STEP]
by (simp add: dom_combination_dom_union)
[PROOF STATE]
proof (state)
this:
l \<in> dom (\<sigma>;;\<tau>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l \<in> dom (\<sigma>;;\<tau>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the ((\<sigma>;;\<tau>) l))])))

goal (8 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 4. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))])\<rbrakk> \<Longrightarrow> revision_step r s s'
 5. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 6. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step r s s'
 7. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> revision_step r s s'
 8. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> revision_step r s s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the ((\<sigma>;;\<tau>) l))])))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the ((\<sigma>;;\<tau>) l))])))

goal (1 subgoal):
 1. revision_step r s s'
[PROOF STEP]
using get.hyps(1)
[PROOF STATE]
proof (prove)
using this:
revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the ((\<sigma>;;\<tau>) l))])))
s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))]))

goal (1 subgoal):
 1. revision_step r s s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
revision_step r s s'

goal (7 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 4. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 5. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step r s s'
 6. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> revision_step r s s'
 7. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> revision_step r s s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 4. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 5. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step r s s'
 6. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> revision_step r s s'
 7. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> revision_step r s s'
[PROOF STEP]
case (set \<sigma> \<tau> \<E> l v)
[PROOF STATE]
proof (state)
this:
s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)]))
s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])

goal (7 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 4. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 5. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step r s s'
 6. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> revision_step r s s'
 7. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> revision_step r s s'
[PROOF STEP]
have "revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])
 2. l \<in> dom (\<sigma>;;\<tau>)
[PROOF STEP]
show "s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])
[PROOF STEP]
by (simp add: set.hyps(2))
[PROOF STATE]
proof (state)
this:
s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])

goal (1 subgoal):
 1. l \<in> dom (\<sigma>;;\<tau>)
[PROOF STEP]
show "l \<in> dom (\<sigma>;;\<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<in> dom (\<sigma>;;\<tau>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<in> dom (\<sigma>;;\<tau>)
[PROOF STEP]
have "l \<in> LID\<^sub>L (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<in> LID\<^sub>L (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l \<in> LID\<^sub>L (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])

goal (1 subgoal):
 1. l \<in> dom (\<sigma>;;\<tau>)
[PROOF STEP]
hence "l \<in> dom \<sigma> \<union> dom \<tau>"
[PROOF STATE]
proof (prove)
using this:
l \<in> LID\<^sub>L (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])

goal (1 subgoal):
 1. l \<in> dom \<sigma> \<union> dom \<tau>
[PROOF STEP]
using domains_subsume_def domains_subsume_globally_def doms_sub_local set.hyps(2)
[PROOF STATE]
proof (prove)
using this:
l \<in> LID\<^sub>L (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])
\<S> ?ls = (LID\<^sub>L ?ls \<subseteq> doms ?ls)
\<S>\<^sub>G ?s = (\<forall>r ls. ?s r = Some ls \<longrightarrow> \<S> ls)
\<S>\<^sub>G s
s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])

goal (1 subgoal):
 1. l \<in> dom \<sigma> \<union> dom \<tau>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
l \<in> dom \<sigma> \<union> dom \<tau>

goal (1 subgoal):
 1. l \<in> dom (\<sigma>;;\<tau>)
[PROOF STEP]
thus "l \<in> dom (\<sigma>;;\<tau>)"
[PROOF STATE]
proof (prove)
using this:
l \<in> dom \<sigma> \<union> dom \<tau>

goal (1 subgoal):
 1. l \<in> dom (\<sigma>;;\<tau>)
[PROOF STEP]
by (simp add: dom_combination_dom_union)
[PROOF STATE]
proof (state)
this:
l \<in> dom (\<sigma>;;\<tau>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
l \<in> dom (\<sigma>;;\<tau>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])))

goal (7 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 4. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 5. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step r s s'
 6. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> revision_step r s s'
 7. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> revision_step r s s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])))

goal (1 subgoal):
 1. revision_step r s s'
[PROOF STEP]
using set.hyps(1)
[PROOF STATE]
proof (prove)
using this:
revision_step r s (s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])))
s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)]))

goal (1 subgoal):
 1. revision_step r s s'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
revision_step r s s'

goal (6 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> revision_step r s s'
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> revision_step r s s'
 4. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> revision_step r s s'
 5. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> revision_step r s s'
 6. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> revision_step r s s'
[PROOF STEP]
qed (simp add: revision_step.intros)+
[PROOF STATE]
proof (state)
this:
revision_step r s s'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
revision_step r s s' = revision_step_relaxed r s s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_occurrences_val_expr [simp]:
  fixes
    v :: "('r,'l,'v) val" and
    e :: "('r,'l,'v) expr"
  shows
  "finite (RID\<^sub>V v)"
  "finite (RID\<^sub>E e)"
  "finite (LID\<^sub>V v)"
  "finite (LID\<^sub>E e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (finite (RID\<^sub>V v) &&& finite (RID\<^sub>E e)) &&& finite (LID\<^sub>V v) &&& finite (LID\<^sub>E e)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. finite (RID\<^sub>V v)
 2. finite (RID\<^sub>E e)
 3. finite (LID\<^sub>V v)
 4. finite (LID\<^sub>E e)
[PROOF STEP]
have "(finite (RID\<^sub>V v) \<and> finite (LID\<^sub>V v)) \<and> finite (RID\<^sub>E e) \<and> finite (LID\<^sub>E e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (finite (RID\<^sub>V v) \<and> finite (LID\<^sub>V v)) \<and> finite (RID\<^sub>E e) \<and> finite (LID\<^sub>E e)
[PROOF STEP]
by (induct rule: val_expr.induct) auto
[PROOF STATE]
proof (state)
this:
(finite (RID\<^sub>V v) \<and> finite (LID\<^sub>V v)) \<and> finite (RID\<^sub>E e) \<and> finite (LID\<^sub>E e)

goal (4 subgoals):
 1. finite (RID\<^sub>V v)
 2. finite (RID\<^sub>E e)
 3. finite (LID\<^sub>V v)
 4. finite (LID\<^sub>E e)
[PROOF STEP]
thus
    "finite (RID\<^sub>V v)"
    "finite (RID\<^sub>E e)"
    "finite (LID\<^sub>V v)"
    "finite (LID\<^sub>E e)"
[PROOF STATE]
proof (prove)
using this:
(finite (RID\<^sub>V v) \<and> finite (LID\<^sub>V v)) \<and> finite (RID\<^sub>E e) \<and> finite (LID\<^sub>E e)

goal (1 subgoal):
 1. (finite (RID\<^sub>V v) &&& finite (RID\<^sub>E e)) &&& finite (LID\<^sub>V v) &&& finite (LID\<^sub>E e)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (RID\<^sub>V v)
finite (RID\<^sub>E e)
finite (LID\<^sub>V v)
finite (LID\<^sub>E e)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma store_finite_upd [intro]:
  "finite (RID\<^sub>S \<tau>) \<Longrightarrow> finite (RID\<^sub>S (\<tau>(l := None)))"
  "finite (LID\<^sub>S \<tau>) \<Longrightarrow> finite (LID\<^sub>S (\<tau>(l := None)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (finite (RID\<^sub>S \<tau>) \<Longrightarrow> finite (RID\<^sub>S (\<tau>(l := None)))) &&& (finite (LID\<^sub>S \<tau>) \<Longrightarrow> finite (LID\<^sub>S (\<tau>(l := None))))
[PROOF STEP]
apply (meson ID_restricted_store_subset_store(1) finite_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (LID\<^sub>S \<tau>) \<Longrightarrow> finite (LID\<^sub>S (\<tau>(l := None)))
[PROOF STEP]
by (simp add: ID_restricted_store_subset_store(2) rev_finite_subset)


[STATEMENT]
lemma finite_state_imp_restriction_finite [intro]:
  "finite (RID\<^sub>G s) \<Longrightarrow> finite (RID\<^sub>G (s(r := None)))"
  "finite (LID\<^sub>G s) \<Longrightarrow> finite (LID\<^sub>G (s(r := None)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (finite (RID\<^sub>G s) \<Longrightarrow> finite (RID\<^sub>G (s(r := None)))) &&& (finite (LID\<^sub>G s) \<Longrightarrow> finite (LID\<^sub>G (s(r := None))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (RID\<^sub>G s) \<Longrightarrow> finite (RID\<^sub>G (s(r := None)))
 2. finite (LID\<^sub>G s) \<Longrightarrow> finite (LID\<^sub>G (s(r := None)))
[PROOF STEP]
assume "finite (RID\<^sub>G s)"
[PROOF STATE]
proof (state)
this:
finite (RID\<^sub>G s)

goal (2 subgoals):
 1. finite (RID\<^sub>G s) \<Longrightarrow> finite (RID\<^sub>G (s(r := None)))
 2. finite (LID\<^sub>G s) \<Longrightarrow> finite (LID\<^sub>G (s(r := None)))
[PROOF STEP]
thus "finite (RID\<^sub>G (s(r := None)))"
[PROOF STATE]
proof (prove)
using this:
finite (RID\<^sub>G s)

goal (1 subgoal):
 1. finite (RID\<^sub>G (s(r := None)))
[PROOF STEP]
by (meson infinite_super ID_restricted_global_subset_unrestricted)
[PROOF STATE]
proof (state)
this:
finite (RID\<^sub>G (s(r := None)))

goal (1 subgoal):
 1. finite (LID\<^sub>G s) \<Longrightarrow> finite (LID\<^sub>G (s(r := None)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (LID\<^sub>G s) \<Longrightarrow> finite (LID\<^sub>G (s(r := None)))
[PROOF STEP]
assume fin: "finite (LID\<^sub>G s)"
[PROOF STATE]
proof (state)
this:
finite (LID\<^sub>G s)

goal (1 subgoal):
 1. finite (LID\<^sub>G s) \<Longrightarrow> finite (LID\<^sub>G (s(r := None)))
[PROOF STEP]
have "LID\<^sub>G (s(r := None)) \<subseteq> LID\<^sub>G s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LID\<^sub>G (s(r := None)) \<subseteq> LID\<^sub>G s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
LID\<^sub>G (s(r := None)) \<subseteq> LID\<^sub>G s

goal (1 subgoal):
 1. finite (LID\<^sub>G s) \<Longrightarrow> finite (LID\<^sub>G (s(r := None)))
[PROOF STEP]
thus "finite (LID\<^sub>G (s(r := None)))"
[PROOF STATE]
proof (prove)
using this:
LID\<^sub>G (s(r := None)) \<subseteq> LID\<^sub>G s

goal (1 subgoal):
 1. finite (LID\<^sub>G (s(r := None)))
[PROOF STEP]
using fin finite_subset
[PROOF STATE]
proof (prove)
using this:
LID\<^sub>G (s(r := None)) \<subseteq> LID\<^sub>G s
finite (LID\<^sub>G s)
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (LID\<^sub>G (s(r := None)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (LID\<^sub>G (s(r := None)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma local_state_of_finite_restricted_global_state_is_finite [intro]:
  "s r' = Some ls \<Longrightarrow> finite (RID\<^sub>G (s(r := None))) \<Longrightarrow> r \<noteq> r' \<Longrightarrow> finite (RID\<^sub>L ls)"
  "s r' = Some ls \<Longrightarrow> finite (LID\<^sub>G (s(r := None))) \<Longrightarrow> r \<noteq> r' \<Longrightarrow> finite (LID\<^sub>L ls)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>s r' = Some ls; finite (RID\<^sub>G (s(r := None))); r \<noteq> r'\<rbrakk> \<Longrightarrow> finite (RID\<^sub>L ls)) &&& (\<lbrakk>s r' = Some ls; finite (LID\<^sub>G (s(r := None))); r \<noteq> r'\<rbrakk> \<Longrightarrow> finite (LID\<^sub>L ls))
[PROOF STEP]
apply (metis (no_types, lifting) ID_distr_global(1) finite_Un finite_insert fun_upd_triv fun_upd_twist)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s r' = Some ls; finite (LID\<^sub>G (s(r := None))); r \<noteq> r'\<rbrakk> \<Longrightarrow> finite (LID\<^sub>L ls)
[PROOF STEP]
by (metis ID_distr_global(2) finite_Un fun_upd_triv fun_upd_twist)


[STATEMENT]
lemma empty_map_finite [simp]:
  "finite (RID\<^sub>S \<epsilon>)"
  "finite (LID\<^sub>S \<epsilon>)"
  "finite (RID\<^sub>G \<epsilon>)"
  "finite (LID\<^sub>G \<epsilon>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (finite (RID\<^sub>S \<epsilon>) &&& finite (LID\<^sub>S \<epsilon>)) &&& finite (RID\<^sub>G \<epsilon>) &&& finite (LID\<^sub>G \<epsilon>)
[PROOF STEP]
by (simp add: RID\<^sub>S_def LID\<^sub>S_def RID\<^sub>G_def LID\<^sub>G_def)+


[STATEMENT]
lemma finite_combination [intro]:
  "finite (RID\<^sub>S \<sigma>) \<Longrightarrow> finite (RID\<^sub>S \<tau>) \<Longrightarrow> finite (RID\<^sub>S (\<sigma>;;\<tau>))"
  "finite (LID\<^sub>S \<sigma>) \<Longrightarrow> finite (LID\<^sub>S \<tau>) \<Longrightarrow> finite (LID\<^sub>S (\<sigma>;;\<tau>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>finite (RID\<^sub>S \<sigma>); finite (RID\<^sub>S \<tau>)\<rbrakk> \<Longrightarrow> finite (RID\<^sub>S (\<sigma>;;\<tau>))) &&& (\<lbrakk>finite (LID\<^sub>S \<sigma>); finite (LID\<^sub>S \<tau>)\<rbrakk> \<Longrightarrow> finite (LID\<^sub>S (\<sigma>;;\<tau>)))
[PROOF STEP]
by (meson finite_UnI rev_finite_subset ID_combination_subset_union)+


[STATEMENT]
lemma RID\<^sub>G_finite_invariant:
  assumes
    step: "revision_step r s s'" and
    fin: "finite (RID\<^sub>G s)"
shows
    "finite (RID\<^sub>G s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (RID\<^sub>G s')
[PROOF STEP]
proof (use step in \<open>cases rule: revision_stepE\<close>)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 4. \<And>\<sigma> \<tau> \<E> v l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])); s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)]); l \<notin> LID\<^sub>G s\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 5. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 6. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 7. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 8. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 9. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
[PROOF STEP]
case (join \<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v)
[PROOF STATE]
proof (state)
this:
s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None)
s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))])
s r' = Some (\<sigma>', \<tau>', VE v)

goal (9 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 4. \<And>\<sigma> \<tau> \<E> v l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])); s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)]); l \<notin> LID\<^sub>G s\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 5. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 6. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 7. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 8. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 9. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
[PROOF STEP]
hence "r \<noteq> r'"
[PROOF STATE]
proof (prove)
using this:
s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None)
s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))])
s r' = Some (\<sigma>', \<tau>', VE v)

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

goal (9 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 4. \<And>\<sigma> \<tau> \<E> v l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])); s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)]); l \<notin> LID\<^sub>G s\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 5. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 6. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 7. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 8. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 9. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<noteq> r'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<noteq> r'

goal (1 subgoal):
 1. finite (RID\<^sub>G s')
[PROOF STEP]
by (metis (mono_tags, lifting) ID_distr_global(1) ID_distr_local(2) fin finite_Un finite_combination(1) finite_insert finite_occurrences_val_expr(2) finite_state_imp_restriction_finite(1) join local_state_of_finite_restricted_global_state_is_finite(1))
[PROOF STATE]
proof (state)
this:
finite (RID\<^sub>G s')

goal (8 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 4. \<And>\<sigma> \<tau> \<E> v l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])); s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)]); l \<notin> LID\<^sub>G s\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 5. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 6. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 7. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
 8. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s')
[PROOF STEP]
qed (use fin in \<open>auto simp add: ID_distr_global_conditional\<close>)