[STATEMENT]
lemma vebt_inserti_rule: "x < 2^n \<Longrightarrow> <vebt_assn n s ti> vebt_inserti ti x <\<lambda> r. vebt_assn n (s \<union> {x}) r >T[13 + 13 * (nat \<lceil>lb n \<rceil>)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < 2 ^ n \<Longrightarrow> <vebt_assn n s ti> vebt_inserti ti x <vebt_assn n (s \<union> {x})> T[13 + 13 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
apply(sep_auto simp: norm_pre_pure_iff_htt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < 2 ^ n \<Longrightarrow> <vebt_assn n s ti> vebt_inserti ti x <vebt_assn n (insert x s)> T[13 + 13 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
unfolding vebt_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < 2 ^ n \<Longrightarrow> <\<exists>\<^sub>At. vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)> vebt_inserti ti x <\<lambda>r. \<exists>\<^sub>At. vebt_assn_raw t r * \<up> (insert x s = set_vebt t \<and> invar_vebt t n)> T[13 + 13 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
apply(rule norm_pre_ex_rule_htt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. x < 2 ^ n \<Longrightarrow> <vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)> vebt_inserti ti x <\<lambda>r. \<exists>\<^sub>At. vebt_assn_raw t r * \<up> (insert x s = set_vebt t \<and> invar_vebt t n)> T[13 + 13 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
apply(clarsimp simp: norm_pre_pure_iff_htt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> <vebt_assn_raw t ti> vebt_inserti ti x <\<lambda>r. \<exists>\<^sub>Ata. vebt_assn_raw ta r * \<up> (insert x (set_vebt t) = set_vebt ta \<and> invar_vebt ta n)> T[13 + 13 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
apply(rule htt_cons_rule[OF htt_vebt_inserti_invar_vebt])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> invar_vebt (?t6 t) (?n6 t)
 2. \<And>t. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti \<Longrightarrow>\<^sub>A vebt_assn_raw (?t6 t) ti
 3. \<And>t r. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw (vebt_insert (?t6 t) x) r \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta r * \<up> (insert x (set_vebt t) = set_vebt ta \<and> invar_vebt ta n)
 4. \<And>t. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 13 + 13 * nat \<lceil>log 2 (real (?n6 t))\<rceil> \<le> 13 + 13 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti \<Longrightarrow>\<^sub>A vebt_assn_raw t ti
 2. \<And>t r. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw (vebt_insert t x) r \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta r * \<up> (insert x (set_vebt t) = set_vebt ta \<and> invar_vebt ta n)
 3. \<And>t. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 13 + 13 * nat \<lceil>log 2 (real n)\<rceil> \<le> 13 + 13 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t r. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw (vebt_insert t x) r \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta r * \<up> (insert x (set_vebt t) = set_vebt ta \<and> invar_vebt ta n)
 2. \<And>t. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 13 + 13 * nat \<lceil>log 2 (real n)\<rceil> \<le> 13 + 13 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>t r a b. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n; (a, b) \<Turnstile> vebt_assn_raw (vebt_insert t x) r\<rbrakk> \<Longrightarrow> x \<in> set_vebt (vebt_insert t x)
 2. \<And>t r a b xa. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n; (a, b) \<Turnstile> vebt_assn_raw (vebt_insert t x) r; xa \<in> set_vebt t\<rbrakk> \<Longrightarrow> xa \<in> set_vebt (vebt_insert t x)
 3. \<And>t r a b xa. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n; (a, b) \<Turnstile> vebt_assn_raw (vebt_insert t x) r; xa \<in> set_vebt (vebt_insert t x); xa \<notin> set_vebt t\<rbrakk> \<Longrightarrow> xa = x
 4. \<And>t r. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n; \<exists>h. h \<Turnstile> vebt_assn_raw (vebt_insert t x) r\<rbrakk> \<Longrightarrow> invar_vebt (vebt_insert t x) n
 5. \<And>t. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 13 + 13 * nat \<lceil>log 2 (real n)\<rceil> \<le> 13 + 13 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply (auto simp add: insert_correct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t r a b. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n; (a, b) \<Turnstile> vebt_assn_raw (vebt_insert t x) r\<rbrakk> \<Longrightarrow> x \<in> set_vebt (vebt_insert t x)
 2. \<And>t r a b xa. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n; (a, b) \<Turnstile> vebt_assn_raw (vebt_insert t x) r; xa \<in> set_vebt t\<rbrakk> \<Longrightarrow> xa \<in> set_vebt (vebt_insert t x)
 3. \<And>t r a b xa. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n; (a, b) \<Turnstile> vebt_assn_raw (vebt_insert t x) r; xa \<in> set_vebt (vebt_insert t x); xa \<notin> set_vebt t\<rbrakk> \<Longrightarrow> xa = x
 4. \<And>t r a b. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n; (a, b) \<Turnstile> vebt_assn_raw (vebt_insert t x) r\<rbrakk> \<Longrightarrow> invar_vebt (vebt_insert t x) n
[PROOF STEP]
apply (simp add: valid_insert_both_member_options_add set_vebt_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>t r a b xa. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n; (a, b) \<Turnstile> vebt_assn_raw (vebt_insert t x) r; xa \<in> set_vebt t\<rbrakk> \<Longrightarrow> xa \<in> set_vebt (vebt_insert t x)
 2. \<And>t r a b xa. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n; (a, b) \<Turnstile> vebt_assn_raw (vebt_insert t x) r; xa \<in> set_vebt (vebt_insert t x); xa \<notin> set_vebt t\<rbrakk> \<Longrightarrow> xa = x
 3. \<And>t r a b. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n; (a, b) \<Turnstile> vebt_assn_raw (vebt_insert t x) r\<rbrakk> \<Longrightarrow> invar_vebt (vebt_insert t x) n
[PROOF STEP]
apply (metis UnCI insert_correct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t r a b xa. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n; (a, b) \<Turnstile> vebt_assn_raw (vebt_insert t x) r; xa \<in> set_vebt (vebt_insert t x); xa \<notin> set_vebt t\<rbrakk> \<Longrightarrow> xa = x
 2. \<And>t r a b. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n; (a, b) \<Turnstile> vebt_assn_raw (vebt_insert t x) r\<rbrakk> \<Longrightarrow> invar_vebt (vebt_insert t x) n
[PROOF STEP]
apply (metis UnE insert_correct singletonD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t r a b. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n; (a, b) \<Turnstile> vebt_assn_raw (vebt_insert t x) r\<rbrakk> \<Longrightarrow> invar_vebt (vebt_insert t x) n
[PROOF STEP]
using valid_pres_insert
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>invar_vebt ?t ?n; ?x < 2 ^ ?n\<rbrakk> \<Longrightarrow> invar_vebt (vebt_insert ?t ?x) ?n

goal (1 subgoal):
 1. \<And>t r a b. \<lbrakk>x < 2 ^ n; s = set_vebt t; invar_vebt t n; (a, b) \<Turnstile> vebt_assn_raw (vebt_insert t x) r\<rbrakk> \<Longrightarrow> invar_vebt (vebt_insert t x) n
[PROOF STEP]
by presburger


[STATEMENT]
lemma vebt_maxti_rule: "<vebt_assn n s ti> vebt_maxti ti <\<lambda> r. vebt_assn n s ti *  \<up>( r = Some y \<longleftrightarrow> max_in_set s y)>T[1]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <vebt_assn n s ti> vebt_maxti ti <\<lambda>r. vebt_assn n s ti * \<up> ((r = Some y) = max_in_set s y)> T[1]
[PROOF STEP]
unfolding vebt_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<exists>\<^sub>At. vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)> vebt_maxti ti <\<lambda>r. (\<exists>\<^sub>At. vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)) * \<up> ((r = Some y) = max_in_set s y)> T[1]
[PROOF STEP]
apply(rule norm_pre_ex_rule_htt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. <vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)> vebt_maxti ti <\<lambda>r. (\<exists>\<^sub>At. vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)) * \<up> ((r = Some y) = max_in_set s y)> T[1]
[PROOF STEP]
apply(clarsimp simp: norm_pre_pure_iff_htt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> <vebt_assn_raw t ti> vebt_maxti ti <\<lambda>r. \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> ((r = Some y) = max_in_set (set_vebt t) y)> T[Suc 0]
[PROOF STEP]
apply(rule htt_cons_rule[OF vebt_maxti_hT])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti \<Longrightarrow>\<^sub>A vebt_assn_raw (?t6 t) ti
 2. \<And>t r. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw (?t6 t) ti * \<up> (r = vebt_maxt (?t6 t)) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> ((r = Some y) = max_in_set (set_vebt t) y)
 3. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 1 \<le> Suc 0
[PROOF STEP]
apply(rule ent_refl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t r. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti * \<up> (r = vebt_maxt t) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> ((r = Some y) = max_in_set (set_vebt t) y)
 2. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 1 \<le> Suc 0
[PROOF STEP]
apply (sep_auto simp: set_vebt_maxt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 1 \<le> Suc 0
[PROOF STEP]
by simp


[STATEMENT]
lemma vebt_minti_rule: "<vebt_assn n s ti> vebt_minti ti <\<lambda> r. vebt_assn n s ti *  \<up>( r = Some y \<longleftrightarrow> min_in_set s y)>T[1]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <vebt_assn n s ti> vebt_minti ti <\<lambda>r. vebt_assn n s ti * \<up> ((r = Some y) = min_in_set s y)> T[1]
[PROOF STEP]
unfolding vebt_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<exists>\<^sub>At. vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)> vebt_minti ti <\<lambda>r. (\<exists>\<^sub>At. vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)) * \<up> ((r = Some y) = min_in_set s y)> T[1]
[PROOF STEP]
apply(rule norm_pre_ex_rule_htt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. <vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)> vebt_minti ti <\<lambda>r. (\<exists>\<^sub>At. vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)) * \<up> ((r = Some y) = min_in_set s y)> T[1]
[PROOF STEP]
apply(clarsimp simp: norm_pre_pure_iff_htt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> <vebt_assn_raw t ti> vebt_minti ti <\<lambda>r. \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> ((r = Some y) = min_in_set (set_vebt t) y)> T[Suc 0]
[PROOF STEP]
apply(rule htt_cons_rule[OF vebt_minti_hT])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti \<Longrightarrow>\<^sub>A vebt_assn_raw (?t6 t) ti
 2. \<And>t r. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw (?t6 t) ti * \<up> (r = vebt_mint (?t6 t)) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> ((r = Some y) = min_in_set (set_vebt t) y)
 3. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 1 \<le> Suc 0
[PROOF STEP]
apply(rule ent_refl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t r. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti * \<up> (r = vebt_mint t) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> ((r = Some y) = min_in_set (set_vebt t) y)
 2. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 1 \<le> Suc 0
[PROOF STEP]
apply (sep_auto simp: set_vebt_mint)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 1 \<le> Suc 0
[PROOF STEP]
by auto


[STATEMENT]
lemma vebt_succi_rule: "<vebt_assn n s ti> vebt_succi ti x <\<lambda> r. vebt_assn n s ti *  \<up>( r = Some y \<longleftrightarrow> is_succ_in_set s x y)>T[7 + 7 * (nat \<lceil>lb n \<rceil>)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <vebt_assn n s ti> vebt_succi ti x <\<lambda>r. vebt_assn n s ti * \<up> ((r = Some y) = is_succ_in_set s x y)> T[7 + 7 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
unfolding vebt_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<exists>\<^sub>At. vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)> vebt_succi ti x <\<lambda>r. (\<exists>\<^sub>At. vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)) * \<up> ((r = Some y) = is_succ_in_set s x y)> T[7 + 7 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
apply(rule norm_pre_ex_rule_htt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. <vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)> vebt_succi ti x <\<lambda>r. (\<exists>\<^sub>At. vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)) * \<up> ((r = Some y) = is_succ_in_set s x y)> T[7 + 7 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
apply(clarsimp simp: norm_pre_pure_iff_htt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> <vebt_assn_raw t ti> vebt_succi ti x <\<lambda>r. \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> ((r = Some y) = is_succ_in_set (set_vebt t) x y)> T[7 + 7 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
apply(rule htt_cons_rule[OF htt_vebt_succi])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> invar_vebt (?t6 t) (?n6 t)
 2. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti \<Longrightarrow>\<^sub>A vebt_assn_raw (?t6 t) ti
 3. \<And>t r. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw (?t6 t) ti * \<up> (r = vebt_succ (?t6 t) x) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> ((r = Some y) = is_succ_in_set (set_vebt t) x y)
 4. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 7 + 7 * nat \<lceil>log 2 (real (?n6 t))\<rceil> \<le> 7 + 7 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti \<Longrightarrow>\<^sub>A vebt_assn_raw t ti
 2. \<And>t r. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti * \<up> (r = vebt_succ t x) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> ((r = Some y) = is_succ_in_set (set_vebt t) x y)
 3. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 7 + 7 * nat \<lceil>log 2 (real n)\<rceil> \<le> 7 + 7 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t r. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti * \<up> (r = vebt_succ t x) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> ((r = Some y) = is_succ_in_set (set_vebt t) x y)
 2. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 7 + 7 * nat \<lceil>log 2 (real n)\<rceil> \<le> 7 + 7 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply (sep_auto simp: set_vebt_succ)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 7 + 7 * nat \<lceil>log 2 (real n)\<rceil> \<le> 7 + 7 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma vebt_predi_rule: "<vebt_assn n s ti> vebt_predi ti x <\<lambda> r. vebt_assn n s ti *  \<up>( r = Some y \<longleftrightarrow> is_pred_in_set s x y)>T[7 + 7 * (nat \<lceil>lb n \<rceil>)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <vebt_assn n s ti> vebt_predi ti x <\<lambda>r. vebt_assn n s ti * \<up> ((r = Some y) = is_pred_in_set s x y)> T[7 + 7 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
unfolding vebt_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<exists>\<^sub>At. vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)> vebt_predi ti x <\<lambda>r. (\<exists>\<^sub>At. vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)) * \<up> ((r = Some y) = is_pred_in_set s x y)> T[7 + 7 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
apply(rule norm_pre_ex_rule_htt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. <vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)> vebt_predi ti x <\<lambda>r. (\<exists>\<^sub>At. vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)) * \<up> ((r = Some y) = is_pred_in_set s x y)> T[7 + 7 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
apply(clarsimp simp: norm_pre_pure_iff_htt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> <vebt_assn_raw t ti> vebt_predi ti x <\<lambda>r. \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> ((r = Some y) = is_pred_in_set (set_vebt t) x y)> T[7 + 7 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
apply(rule htt_cons_rule[OF htt_vebt_predi])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> invar_vebt (?t6 t) (?n6 t)
 2. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti \<Longrightarrow>\<^sub>A vebt_assn_raw (?t6 t) ti
 3. \<And>t r. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw (?t6 t) ti * \<up> (r = vebt_pred (?t6 t) x) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> ((r = Some y) = is_pred_in_set (set_vebt t) x y)
 4. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 7 + 7 * nat \<lceil>log 2 (real (?n6 t))\<rceil> \<le> 7 + 7 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti \<Longrightarrow>\<^sub>A vebt_assn_raw t ti
 2. \<And>t r. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti * \<up> (r = vebt_pred t x) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> ((r = Some y) = is_pred_in_set (set_vebt t) x y)
 3. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 7 + 7 * nat \<lceil>log 2 (real n)\<rceil> \<le> 7 + 7 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t r. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti * \<up> (r = vebt_pred t x) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta ti * \<up> (set_vebt t = set_vebt ta \<and> invar_vebt ta n) * \<up> ((r = Some y) = is_pred_in_set (set_vebt t) x y)
 2. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 7 + 7 * nat \<lceil>log 2 (real n)\<rceil> \<le> 7 + 7 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply (sep_auto simp: set_vebt_pred)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 7 + 7 * nat \<lceil>log 2 (real n)\<rceil> \<le> 7 + 7 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma vebt_deletei_rule: "<vebt_assn n s ti > vebt_deletei ti x <\<lambda> r. vebt_assn n (s - {x}) r >T[20 + 20 * (nat \<lceil>lb n \<rceil>)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <vebt_assn n s ti> vebt_deletei ti x <vebt_assn n (s - {x})> T[20 + 20 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
unfolding vebt_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<exists>\<^sub>At. vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)> vebt_deletei ti x <\<lambda>r. \<exists>\<^sub>At. vebt_assn_raw t r * \<up> (s - {x} = set_vebt t \<and> invar_vebt t n)> T[20 + 20 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
apply(rule norm_pre_ex_rule_htt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. <vebt_assn_raw t ti * \<up> (s = set_vebt t \<and> invar_vebt t n)> vebt_deletei ti x <\<lambda>r. \<exists>\<^sub>At. vebt_assn_raw t r * \<up> (s - {x} = set_vebt t \<and> invar_vebt t n)> T[20 + 20 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
apply(clarsimp simp: norm_pre_pure_iff_htt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> <vebt_assn_raw t ti> vebt_deletei ti x <\<lambda>r. \<exists>\<^sub>Ata. vebt_assn_raw ta r * \<up> (set_vebt t - {x} = set_vebt ta \<and> invar_vebt ta n)> T[20 + 20 * nat \<lceil>log 2 (real n)\<rceil>]
[PROOF STEP]
apply(rule htt_cons_rule[OF htt_vebt_deletei])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> invar_vebt (?t6 t) (?n6 t)
 2. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti \<Longrightarrow>\<^sub>A vebt_assn_raw (?t6 t) ti
 3. \<And>t r. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw (vebt_delete (?t6 t) x) r \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta r * \<up> (set_vebt t - {x} = set_vebt ta \<and> invar_vebt ta n)
 4. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 20 + 20 * nat \<lceil>log 2 (real (?n6 t))\<rceil> \<le> 20 + 20 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw t ti \<Longrightarrow>\<^sub>A vebt_assn_raw t ti
 2. \<And>t r. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw (vebt_delete t x) r \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta r * \<up> (set_vebt t - {x} = set_vebt ta \<and> invar_vebt ta n)
 3. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 20 + 20 * nat \<lceil>log 2 (real n)\<rceil> \<le> 20 + 20 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t r. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> vebt_assn_raw (vebt_delete t x) r \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ata. vebt_assn_raw ta r * \<up> (set_vebt t - {x} = set_vebt ta \<and> invar_vebt ta n)
 2. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 20 + 20 * nat \<lceil>log 2 (real n)\<rceil> \<le> 20 + 20 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>t r a b xa. \<lbrakk>s = set_vebt t; invar_vebt t n; (a, b) \<Turnstile> vebt_assn_raw (vebt_delete t x) r; xa \<in> set_vebt t; xa \<notin> set_vebt (vebt_delete t x)\<rbrakk> \<Longrightarrow> xa = x
 2. \<And>t r a b xa. \<lbrakk>s = set_vebt t; invar_vebt t n; (a, b) \<Turnstile> vebt_assn_raw (vebt_delete t x) r; xa \<in> set_vebt (vebt_delete t x)\<rbrakk> \<Longrightarrow> xa \<in> set_vebt t
 3. \<And>t r a b. \<lbrakk>s = set_vebt t; invar_vebt t n; (a, b) \<Turnstile> vebt_assn_raw (vebt_delete t x) r; x \<in> set_vebt (vebt_delete t x)\<rbrakk> \<Longrightarrow> False
 4. \<And>t r. \<lbrakk>s = set_vebt t; invar_vebt t n; \<exists>h. h \<Turnstile> vebt_assn_raw (vebt_delete t x) r\<rbrakk> \<Longrightarrow> invar_vebt (vebt_delete t x) n
 5. \<And>t. \<lbrakk>s = set_vebt t; invar_vebt t n\<rbrakk> \<Longrightarrow> 20 + 20 * nat \<lceil>log 2 (real n)\<rceil> \<le> 20 + 20 * nat \<lceil>log 2 (real n)\<rceil>
[PROOF STEP]
apply (auto simp add: set_vebt_delete invar_vebt_delete)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma shr_jvm_mstate_of_jvm_mstate' [simp]: "shr (jvm_mstate_of_jvm_mstate' s) = shr s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shr (jvm_mstate_of_jvm_mstate' s) = shr s
[PROOF STEP]
by(cases s) clarsimp


[STATEMENT]
lemma jvm_mstate_of_jvm_mstate'_sc_start_state [simp]:
  "jvm_mstate_of_jvm_mstate'
  (sc_start_state (\<lambda>C M Ts T (mxs, mxl0, ins, xt) vs. (None, [((ins, ins, xt), [], Null # vs @ replicate mxl0 undefined_value, C, M, 0)])) P C M vs) = sc_JVM_start_state P C M vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. jvm_mstate_of_jvm_mstate' (sc_start_state (\<lambda>C M Ts T (mxs, mxl0, ins, xt) vs. (None, [((ins, ins, xt), [], Null # vs @ replicate mxl0 undefined_value, C, M, 0)])) P C M vs) = sc_start_state JVM_local_start P C M vs
[PROOF STEP]
by(simp add: sc.start_state_def split_beta fun_eq_iff)


[STATEMENT]
lemma sc_jvm_start_state_invar:
  assumes "wf_jvm_prog\<^bsub>\<Phi>\<^esub> P"
  and "sc_wf_start_state P C M vs"
  shows "sc_state_\<alpha> (sc_jvm_start_state_refine P C M vs) \<in> sc_jvm_state_invar P \<Phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_refine_base.state_\<alpha> rm.\<alpha> rm.\<alpha> rs.\<alpha> (heap_base.start_state_refine (\<lambda>x. x) (rm.empty ()) (sc_allocate P) (rm.empty ()) rm.update (rm.empty ()) (rs.empty ()) (\<lambda>C M Ts T (mxs, mxl0, ins, xt) vs. (None, [((ins, ins, xt), [], Null # vs @ replicate mxl0 undefined_value, C, M, 0)])) P C M vs) \<in> sc_jvm_state_invar P \<Phi>
[PROOF STEP]
unfolding sc_jvm_state_invar_def Int_iff mem_Collect_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. jvm_mstate_of_jvm_mstate' (state_refine_base.state_\<alpha> rm.\<alpha> rm.\<alpha> rs.\<alpha> (heap_base.start_state_refine (\<lambda>x. x) (rm.empty ()) (sc_allocate P) (rm.empty ()) rm.update (rm.empty ()) (rs.empty ()) (\<lambda>C M Ts T (mxs, mxl0, ins, xt) vs. (None, [((ins, ins, xt), [], Null # vs @ replicate mxl0 undefined_value, C, M, 0)])) P C M vs)) \<in> sc.execute.correct_jvm_state P \<Phi> \<and> ts_ok (\<lambda>t (xcp, frs) h. jvm_state'_ok P (xcp, h, frs)) (thr (state_refine_base.state_\<alpha> rm.\<alpha> rm.\<alpha> rs.\<alpha> (heap_base.start_state_refine (\<lambda>x. x) (rm.empty ()) (sc_allocate P) (rm.empty ()) rm.update (rm.empty ()) (rs.empty ()) (\<lambda>C M Ts T (mxs, mxl0, ins, xt) vs. (None, [((ins, ins, xt), [], Null # vs @ replicate mxl0 undefined_value, C, M, 0)])) P C M vs))) (shr (state_refine_base.state_\<alpha> rm.\<alpha> rm.\<alpha> rs.\<alpha> (heap_base.start_state_refine (\<lambda>x. x) (rm.empty ()) (sc_allocate P) (rm.empty ()) rm.update (rm.empty ()) (rs.empty ()) (\<lambda>C M Ts T (mxs, mxl0, ins, xt) vs. (None, [((ins, ins, xt), [], Null # vs @ replicate mxl0 undefined_value, C, M, 0)])) P C M vs)))
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. jvm_mstate_of_jvm_mstate' (state_refine_base.state_\<alpha> rm.\<alpha> rm.\<alpha> rs.\<alpha> (heap_base.start_state_refine (\<lambda>x. x) (rm.empty ()) (sc_allocate P) (rm.empty ()) rm.update (rm.empty ()) (rs.empty ()) (\<lambda>C M Ts T (mxs, mxl0, ins, xt) vs. (None, [((ins, ins, xt), [], Null # vs @ replicate mxl0 undefined_value, C, M, 0)])) P C M vs)) \<in> sc.execute.correct_jvm_state P \<Phi>
 2. ts_ok (\<lambda>t (xcp, frs) h. jvm_state'_ok P (xcp, h, frs)) (thr (state_refine_base.state_\<alpha> rm.\<alpha> rm.\<alpha> rs.\<alpha> (heap_base.start_state_refine (\<lambda>x. x) (rm.empty ()) (sc_allocate P) (rm.empty ()) rm.update (rm.empty ()) (rs.empty ()) (\<lambda>C M Ts T (mxs, mxl0, ins, xt) vs. (None, [((ins, ins, xt), [], Null # vs @ replicate mxl0 undefined_value, C, M, 0)])) P C M vs))) (shr (state_refine_base.state_\<alpha> rm.\<alpha> rm.\<alpha> rs.\<alpha> (heap_base.start_state_refine (\<lambda>x. x) (rm.empty ()) (sc_allocate P) (rm.empty ()) rm.update (rm.empty ()) (rs.empty ()) (\<lambda>C M Ts T (mxs, mxl0, ins, xt) vs. (None, [((ins, ins, xt), [], Null # vs @ replicate mxl0 undefined_value, C, M, 0)])) P C M vs)))
[PROOF STEP]
apply(simp add: sc.execute.correct_jvm_state_initial[OF assms])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts_ok (\<lambda>t (xcp, frs) h. jvm_state'_ok P (xcp, h, frs)) (thr (state_refine_base.state_\<alpha> rm.\<alpha> rm.\<alpha> rs.\<alpha> (heap_base.start_state_refine (\<lambda>x. x) (rm.empty ()) (sc_allocate P) (rm.empty ()) rm.update (rm.empty ()) (rs.empty ()) (\<lambda>C M Ts T (mxs, mxl0, ins, xt) vs. (None, [((ins, ins, xt), [], Null # vs @ replicate mxl0 undefined_value, C, M, 0)])) P C M vs))) (shr (state_refine_base.state_\<alpha> rm.\<alpha> rm.\<alpha> rs.\<alpha> (heap_base.start_state_refine (\<lambda>x. x) (rm.empty ()) (sc_allocate P) (rm.empty ()) rm.update (rm.empty ()) (rs.empty ()) (\<lambda>C M Ts T (mxs, mxl0, ins, xt) vs. (None, [((ins, ins, xt), [], Null # vs @ replicate mxl0 undefined_value, C, M, 0)])) P C M vs)))
[PROOF STEP]
apply(rule ts_okI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t x ln. thr (state_refine_base.state_\<alpha> rm.\<alpha> rm.\<alpha> rs.\<alpha> (heap_base.start_state_refine (\<lambda>x. x) (rm.empty ()) (sc_allocate P) (rm.empty ()) rm.update (rm.empty ()) (rs.empty ()) (\<lambda>C M Ts T (mxs, mxl0, ins, xt) vs. (None, [((ins, ins, xt), [], Null # vs @ replicate mxl0 undefined_value, C, M, 0)])) P C M vs)) t = \<lfloor>(x, ln)\<rfloor> \<Longrightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h. jvm_state'_ok P (xcp, h, frs)) (shr (state_refine_base.state_\<alpha> rm.\<alpha> rm.\<alpha> rs.\<alpha> (heap_base.start_state_refine (\<lambda>x. x) (rm.empty ()) (sc_allocate P) (rm.empty ()) rm.update (rm.empty ()) (rs.empty ()) (\<lambda>C M Ts T (mxs, mxl0, ins, xt) vs. (None, [((ins, ins, xt), [], Null # vs @ replicate mxl0 undefined_value, C, M, 0)])) P C M vs)))
[PROOF STEP]
using \<open>sc_wf_start_state P C M vs\<close>
[PROOF STATE]
proof (prove)
using this:
sc_wf_start_state P C M vs

goal (1 subgoal):
 1. \<And>t x ln. thr (state_refine_base.state_\<alpha> rm.\<alpha> rm.\<alpha> rs.\<alpha> (heap_base.start_state_refine (\<lambda>x. x) (rm.empty ()) (sc_allocate P) (rm.empty ()) rm.update (rm.empty ()) (rs.empty ()) (\<lambda>C M Ts T (mxs, mxl0, ins, xt) vs. (None, [((ins, ins, xt), [], Null # vs @ replicate mxl0 undefined_value, C, M, 0)])) P C M vs)) t = \<lfloor>(x, ln)\<rfloor> \<Longrightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h. jvm_state'_ok P (xcp, h, frs)) (shr (state_refine_base.state_\<alpha> rm.\<alpha> rm.\<alpha> rs.\<alpha> (heap_base.start_state_refine (\<lambda>x. x) (rm.empty ()) (sc_allocate P) (rm.empty ()) rm.update (rm.empty ()) (rs.empty ()) (\<lambda>C M Ts T (mxs, mxl0, ins, xt) vs. (None, [((ins, ins, xt), [], Null # vs @ replicate mxl0 undefined_value, C, M, 0)])) P C M vs)))
[PROOF STEP]
apply(auto simp add: sc.start_state_def split_beta sc_wf_start_state_iff split: if_split_asm dest: sees_method_idemp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma invariant3p_sc_jvm_state_invar:
  assumes "wf_jvm_prog\<^bsub>\<Phi>\<^esub> P"
  shows "invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. Predicate.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
proof(rule invariant3pI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s tl s'. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s tl s'\<rbrakk> \<Longrightarrow> s' \<in> sc_jvm_state_invar P \<Phi>
[PROOF STEP]
fix s tl s'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s tl s'. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s tl s'\<rbrakk> \<Longrightarrow> s' \<in> sc_jvm_state_invar P \<Phi>
[PROOF STEP]
assume red: "multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. Predicate.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s tl s'"
    and invar: "s \<in> sc_jvm_state_invar P \<Phi>"
[PROOF STATE]
proof (state)
this:
multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s tl s'
s \<in> sc_jvm_state_invar P \<Phi>

goal (1 subgoal):
 1. \<And>s tl s'. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s tl s'\<rbrakk> \<Longrightarrow> s' \<in> sc_jvm_state_invar P \<Phi>
[PROOF STEP]
obtain t ta where tl: "tl = (t, ta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t ta. tl = (t, ta) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases tl)
[PROOF STATE]
proof (state)
this:
tl = (t, ta)

goal (1 subgoal):
 1. \<And>s tl s'. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s tl s'\<rbrakk> \<Longrightarrow> s' \<in> sc_jvm_state_invar P \<Phi>
[PROOF STEP]
from red
[PROOF STATE]
proof (chain)
picking this:
multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s tl s'
[PROOF STEP]
have red': "multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s) (t, jvm_thread_action_of_jvm_thread_action' ta) (jvm_mstate_of_jvm_mstate' s')"
[PROOF STATE]
proof (prove)
using this:
multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s tl s'

goal (1 subgoal):
 1. multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s) (t, jvm_thread_action_of_jvm_thread_action' ta) (jvm_mstate_of_jvm_mstate' s')
[PROOF STEP]
proof(cases rule: multithreaded_base.redT.cases[consumes 1, case_names normal acquire])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>tb x sa taa x' m' s'a. \<lbrakk>s = sa; tl = (tb, taa); s' = s'a; pred.eval (sc_mexec P tb (x, shr sa)) (taa, x', m'); thr sa tb = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' sa tb taa; redT_upd sa tb taa x' m' s'a\<rbrakk> \<Longrightarrow> multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s) (t, jvm_thread_action_of_jvm_thread_action' ta) (jvm_mstate_of_jvm_mstate' s')
 2. \<And>sa tb x n s'a ln. \<lbrakk>s = sa; tl = (tb, K$ [], [], [], [], [], convert_RA ln); s' = s'a; thr sa tb = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset sa tb); may_acquire_all (locks sa) tb ln; 0 < ln $ n; s'a = (acquire_all (locks sa) tb ln, (thr sa(tb \<mapsto> (x, no_wait_locks)), shr sa), wset sa, interrupts sa)\<rbrakk> \<Longrightarrow> multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s) (t, jvm_thread_action_of_jvm_thread_action' ta) (jvm_mstate_of_jvm_mstate' s')
[PROOF STEP]
case (acquire s t x ln n s')
[PROOF STATE]
proof (state)
this:
s__ = s
tl = (t, K$ [], [], [], [], [], convert_RA s')
s'__ = n
thr s t = \<lfloor>(x, s')\<rfloor>
\<not> waiting (wset s t)
may_acquire_all (locks s) t s'
0 < s' $ ln
n = (acquire_all (locks s) t s', (thr s(t \<mapsto> (x, no_wait_locks)), shr s), wset s, interrupts s)

goal (2 subgoals):
 1. \<And>tb x sa taa x' m' s'a. \<lbrakk>s__ = sa; tl = (tb, taa); s'__ = s'a; pred.eval (sc_mexec P tb (x, shr sa)) (taa, x', m'); thr sa tb = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' sa tb taa; redT_upd sa tb taa x' m' s'a\<rbrakk> \<Longrightarrow> multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s__) (t__, jvm_thread_action_of_jvm_thread_action' ta) (jvm_mstate_of_jvm_mstate' s'__)
 2. \<And>sa tb x n s'a ln. \<lbrakk>s__ = sa; tl = (tb, K$ [], [], [], [], [], convert_RA ln); s'__ = s'a; thr sa tb = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset sa tb); may_acquire_all (locks sa) tb ln; 0 < ln $ n; s'a = (acquire_all (locks sa) tb ln, (thr sa(tb \<mapsto> (x, no_wait_locks)), shr sa), wset sa, interrupts sa)\<rbrakk> \<Longrightarrow> multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s__) (t__, jvm_thread_action_of_jvm_thread_action' ta) (jvm_mstate_of_jvm_mstate' s'__)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s__ = s
tl = (t, K$ [], [], [], [], [], convert_RA s')
s'__ = n
thr s t = \<lfloor>(x, s')\<rfloor>
\<not> waiting (wset s t)
may_acquire_all (locks s) t s'
0 < s' $ ln
n = (acquire_all (locks s) t s', (thr s(t \<mapsto> (x, no_wait_locks)), shr s), wset s, interrupts s)

goal (1 subgoal):
 1. multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s__) (t__, jvm_thread_action_of_jvm_thread_action' ta) (jvm_mstate_of_jvm_mstate' s'__)
[PROOF STEP]
using tl
[PROOF STATE]
proof (prove)
using this:
s__ = s
tl = (t, K$ [], [], [], [], [], convert_RA s')
s'__ = n
thr s t = \<lfloor>(x, s')\<rfloor>
\<not> waiting (wset s t)
may_acquire_all (locks s) t s'
0 < s' $ ln
n = (acquire_all (locks s) t s', (thr s(t \<mapsto> (x, no_wait_locks)), shr s), wset s, interrupts s)
tl = (t__, ta)

goal (1 subgoal):
 1. multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s__) (t__, jvm_thread_action_of_jvm_thread_action' ta) (jvm_mstate_of_jvm_mstate' s'__)
[PROOF STEP]
by(cases s)(auto intro!: multithreaded_base.redT.redT_acquire)
[PROOF STATE]
proof (state)
this:
multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s__) (t__, jvm_thread_action_of_jvm_thread_action' ta) (jvm_mstate_of_jvm_mstate' s'__)

goal (1 subgoal):
 1. \<And>tb x sa taa x' m' s'a. \<lbrakk>s__ = sa; tl = (tb, taa); s'__ = s'a; pred.eval (sc_mexec P tb (x, shr sa)) (taa, x', m'); thr sa tb = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' sa tb taa; redT_upd sa tb taa x' m' s'a\<rbrakk> \<Longrightarrow> multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s__) (t__, jvm_thread_action_of_jvm_thread_action' ta) (jvm_mstate_of_jvm_mstate' s'__)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>tb x sa taa x' m' s'a. \<lbrakk>s = sa; tl = (tb, taa); s' = s'a; pred.eval (sc_mexec P tb (x, shr sa)) (taa, x', m'); thr sa tb = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' sa tb taa; redT_upd sa tb taa x' m' s'a\<rbrakk> \<Longrightarrow> multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s) (t, jvm_thread_action_of_jvm_thread_action' ta) (jvm_mstate_of_jvm_mstate' s')
[PROOF STEP]
case (normal t x s ta x' m' s')
[PROOF STATE]
proof (state)
this:
s__ = s
tl = (t, ta)
s'__ = s'
pred.eval (sc_mexec P t (x, shr s)) (ta, x', m')
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
final_thread.actions_ok JVM_final' s t ta
redT_upd s t ta x' m' s'

goal (1 subgoal):
 1. \<And>tb x sa taa x' m' s'a. \<lbrakk>s__ = sa; tl = (tb, taa); s'__ = s'a; pred.eval (sc_mexec P tb (x, shr sa)) (taa, x', m'); thr sa tb = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' sa tb taa; redT_upd sa tb taa x' m' s'a\<rbrakk> \<Longrightarrow> multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s__) (t__, jvm_thread_action_of_jvm_thread_action' ta__) (jvm_mstate_of_jvm_mstate' s'__)
[PROOF STEP]
obtain xcp frs where x: "x = (xcp, frs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xcp frs. x = (xcp, frs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases x)
[PROOF STATE]
proof (state)
this:
x = (xcp, frs)

goal (1 subgoal):
 1. \<And>tb x sa taa x' m' s'a. \<lbrakk>s__ = sa; tl = (tb, taa); s'__ = s'a; pred.eval (sc_mexec P tb (x, shr sa)) (taa, x', m'); thr sa tb = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' sa tb taa; redT_upd sa tb taa x' m' s'a\<rbrakk> \<Longrightarrow> multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s__) (t__, jvm_thread_action_of_jvm_thread_action' ta__) (jvm_mstate_of_jvm_mstate' s'__)
[PROOF STEP]
with invar normal tl
[PROOF STATE]
proof (chain)
picking this:
s__ \<in> sc_jvm_state_invar P \<Phi>
s__ = s
tl = (t, ta)
s'__ = s'
pred.eval (sc_mexec P t (x, shr s)) (ta, x', m')
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
final_thread.actions_ok JVM_final' s t ta
redT_upd s t ta x' m' s'
tl = (t__, ta__)
x = (xcp, frs)
[PROOF STEP]
have correct: "sc.execute.correct_state P \<Phi> t (jvm_state_of_jvm_state' (xcp, shr s, frs))"
      and ok: "jvm_state'_ok P (xcp, shr s, frs)"
[PROOF STATE]
proof (prove)
using this:
s__ \<in> sc_jvm_state_invar P \<Phi>
s__ = s
tl = (t, ta)
s'__ = s'
pred.eval (sc_mexec P t (x, shr s)) (ta, x', m')
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
final_thread.actions_ok JVM_final' s t ta
redT_upd s t ta x' m' s'
tl = (t__, ta__)
x = (xcp, frs)

goal (1 subgoal):
 1. sc.execute.correct_state P \<Phi> t (jvm_state_of_jvm_state' (xcp, shr s, frs)) &&& jvm_state'_ok P (xcp, shr s, frs)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s__ \<in> sc_jvm_state_invar P \<Phi>; s__ = s; tl = (t, ta); s'__ = s'; pred.eval (sc_mexec P t (x, shr s)) (ta, x', m'); thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' s t ta; redT_upd s t ta x' m' s'; tl = (t__, ta__); x = (xcp, frs)\<rbrakk> \<Longrightarrow> sc.execute.correct_state P \<Phi> t (jvm_state_of_jvm_state' (xcp, shr s, frs))
 2. \<lbrakk>s__ \<in> sc_jvm_state_invar P \<Phi>; s__ = s; tl = (t, ta); s'__ = s'; pred.eval (sc_mexec P t (x, shr s)) (ta, x', m'); thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' s t ta; redT_upd s t ta x' m' s'; tl = (t__, ta__); x = (xcp, frs)\<rbrakk> \<Longrightarrow> jvm_state'_ok P (xcp, shr s, frs)
[PROOF STEP]
apply(case_tac [!] s)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c d. \<lbrakk>s__ \<in> sc_jvm_state_invar P \<Phi>; s__ = s; tl = (t, ta); s'__ = s'; pred.eval (sc_mexec P t (x, shr s)) (ta, x', m'); thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' s t ta; redT_upd s t ta x' m' s'; tl = (t__, ta__); x = (xcp, frs); s = (a, b, c, d)\<rbrakk> \<Longrightarrow> sc.execute.correct_state P \<Phi> t (jvm_state_of_jvm_state' (xcp, shr s, frs))
 2. \<And>a b c d. \<lbrakk>s__ \<in> sc_jvm_state_invar P \<Phi>; s__ = s; tl = (t, ta); s'__ = s'; pred.eval (sc_mexec P t (x, shr s)) (ta, x', m'); thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' s t ta; redT_upd s t ta x' m' s'; tl = (t__, ta__); x = (xcp, frs); s = (a, b, c, d)\<rbrakk> \<Longrightarrow> jvm_state'_ok P (xcp, shr s, frs)
[PROOF STEP]
apply(fastforce simp add: sc_jvm_state_invar_def sc.execute.correct_jvm_state_def dest: ts_okD)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
sc.execute.correct_state P \<Phi> t (jvm_state_of_jvm_state' (xcp, shr s, frs))
jvm_state'_ok P (xcp, shr s, frs)

goal (1 subgoal):
 1. \<And>tb x sa taa x' m' s'a. \<lbrakk>s__ = sa; tl = (tb, taa); s'__ = s'a; pred.eval (sc_mexec P tb (x, shr sa)) (taa, x', m'); thr sa tb = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' sa tb taa; redT_upd sa tb taa x' m' s'a\<rbrakk> \<Longrightarrow> multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s__) (t__, jvm_thread_action_of_jvm_thread_action' ta__) (jvm_mstate_of_jvm_mstate' s'__)
[PROOF STEP]
note eq = sc.exec_correct_state(1)[OF assms this]
[PROOF STATE]
proof (state)
this:
sc_exec P t (xcp, shr s, frs) = jvm_ta_state'_of_jvm_ta_state P ` JVM_heap_base.exec (\<lambda>x. x) (\<lambda>x. x) sc_spurious_wakeups (rm.empty ()) (sc_allocate P) sc_typeof_addr sc_heap_read sc_heap_write P t (jvm_state_of_jvm_state' (xcp, shr s, frs))

goal (1 subgoal):
 1. \<And>tb x sa taa x' m' s'a. \<lbrakk>s__ = sa; tl = (tb, taa); s'__ = s'a; pred.eval (sc_mexec P tb (x, shr sa)) (taa, x', m'); thr sa tb = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' sa tb taa; redT_upd sa tb taa x' m' s'a\<rbrakk> \<Longrightarrow> multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s__) (t__, jvm_thread_action_of_jvm_thread_action' ta__) (jvm_mstate_of_jvm_mstate' s'__)
[PROOF STEP]
with normal x tl
[PROOF STATE]
proof (chain)
picking this:
s__ = s
tl = (t, ta)
s'__ = s'
pred.eval (sc_mexec P t (x, shr s)) (ta, x', m')
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
final_thread.actions_ok JVM_final' s t ta
redT_upd s t ta x' m' s'
x = (xcp, frs)
tl = (t__, ta__)
sc_exec P t (xcp, shr s, frs) = jvm_ta_state'_of_jvm_ta_state P ` JVM_heap_base.exec (\<lambda>x. x) (\<lambda>x. x) sc_spurious_wakeups (rm.empty ()) (sc_allocate P) sc_typeof_addr sc_heap_read sc_heap_write P t (jvm_state_of_jvm_state' (xcp, shr s, frs))
[PROOF STEP]
have "sc_execute_mexec P t (jvm_thread_state_of_jvm_thread_state' x, shr (jvm_mstate_of_jvm_mstate' s)) (jvm_thread_action_of_jvm_thread_action' ta) (jvm_thread_state_of_jvm_thread_state' x', m')"
[PROOF STATE]
proof (prove)
using this:
s__ = s
tl = (t, ta)
s'__ = s'
pred.eval (sc_mexec P t (x, shr s)) (ta, x', m')
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
final_thread.actions_ok JVM_final' s t ta
redT_upd s t ta x' m' s'
x = (xcp, frs)
tl = (t__, ta__)
sc_exec P t (xcp, shr s, frs) = jvm_ta_state'_of_jvm_ta_state P ` JVM_heap_base.exec (\<lambda>x. x) (\<lambda>x. x) sc_spurious_wakeups (rm.empty ()) (sc_allocate P) sc_typeof_addr sc_heap_read sc_heap_write P t (jvm_state_of_jvm_state' (xcp, shr s, frs))

goal (1 subgoal):
 1. sc_execute_mexec P t (jvm_thread_state_of_jvm_thread_state' x, shr (jvm_mstate_of_jvm_mstate' s)) (jvm_thread_action_of_jvm_thread_action' ta) (jvm_thread_state_of_jvm_thread_state' x', m')
[PROOF STEP]
by(auto simp add: sc.exec_1_def eq jvm_thread_action'_of_jvm_thread_action_def sc.execute.exec_1_iff)
[PROOF STATE]
proof (state)
this:
sc_execute_mexec P t (jvm_thread_state_of_jvm_thread_state' x, shr (jvm_mstate_of_jvm_mstate' s)) (jvm_thread_action_of_jvm_thread_action' ta) (jvm_thread_state_of_jvm_thread_state' x', m')

goal (1 subgoal):
 1. \<And>tb x sa taa x' m' s'a. \<lbrakk>s__ = sa; tl = (tb, taa); s'__ = s'a; pred.eval (sc_mexec P tb (x, shr sa)) (taa, x', m'); thr sa tb = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' sa tb taa; redT_upd sa tb taa x' m' s'a\<rbrakk> \<Longrightarrow> multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s__) (t__, jvm_thread_action_of_jvm_thread_action' ta__) (jvm_mstate_of_jvm_mstate' s'__)
[PROOF STEP]
with normal tl
[PROOF STATE]
proof (chain)
picking this:
s__ = s
tl = (t, ta)
s'__ = s'
pred.eval (sc_mexec P t (x, shr s)) (ta, x', m')
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
final_thread.actions_ok JVM_final' s t ta
redT_upd s t ta x' m' s'
tl = (t__, ta__)
sc_execute_mexec P t (jvm_thread_state_of_jvm_thread_state' x, shr (jvm_mstate_of_jvm_mstate' s)) (jvm_thread_action_of_jvm_thread_action' ta) (jvm_thread_state_of_jvm_thread_state' x', m')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s__ = s
tl = (t, ta)
s'__ = s'
pred.eval (sc_mexec P t (x, shr s)) (ta, x', m')
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
final_thread.actions_ok JVM_final' s t ta
redT_upd s t ta x' m' s'
tl = (t__, ta__)
sc_execute_mexec P t (jvm_thread_state_of_jvm_thread_state' x, shr (jvm_mstate_of_jvm_mstate' s)) (jvm_thread_action_of_jvm_thread_action' ta) (jvm_thread_state_of_jvm_thread_state' x', m')

goal (1 subgoal):
 1. multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s__) (t__, jvm_thread_action_of_jvm_thread_action' ta__) (jvm_mstate_of_jvm_mstate' s'__)
[PROOF STEP]
by(cases s)(fastforce intro!: multithreaded_base.redT.redT_normal simp add: final_thread.actions_ok_iff fun_eq_iff map_redT_updTs elim: rev_iffD1[OF _ thread_oks_ts_change] cond_action_oks_final_change)
[PROOF STATE]
proof (state)
this:
multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s__) (t__, jvm_thread_action_of_jvm_thread_action' ta__) (jvm_mstate_of_jvm_mstate' s'__)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s) (t, jvm_thread_action_of_jvm_thread_action' ta) (jvm_mstate_of_jvm_mstate' s')

goal (1 subgoal):
 1. \<And>s tl s'. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s tl s'\<rbrakk> \<Longrightarrow> s' \<in> sc_jvm_state_invar P \<Phi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s) (t, jvm_thread_action_of_jvm_thread_action' ta) (jvm_mstate_of_jvm_mstate' s')

goal (1 subgoal):
 1. \<And>s tl s'. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s tl s'\<rbrakk> \<Longrightarrow> s' \<in> sc_jvm_state_invar P \<Phi>
[PROOF STEP]
from invar
[PROOF STATE]
proof (chain)
picking this:
s \<in> sc_jvm_state_invar P \<Phi>
[PROOF STEP]
have "sc.execute.correct_state_ts P \<Phi> (thr (jvm_mstate_of_jvm_mstate' s)) (shr (jvm_mstate_of_jvm_mstate' s))"
    and "lock_thread_ok (locks (jvm_mstate_of_jvm_mstate' s)) (thr (jvm_mstate_of_jvm_mstate' s))"
[PROOF STATE]
proof (prove)
using this:
s \<in> sc_jvm_state_invar P \<Phi>

goal (1 subgoal):
 1. sc.execute.correct_state_ts P \<Phi> (thr (jvm_mstate_of_jvm_mstate' s)) (shr (jvm_mstate_of_jvm_mstate' s)) &&& lock_thread_ok (locks (jvm_mstate_of_jvm_mstate' s)) (thr (jvm_mstate_of_jvm_mstate' s))
[PROOF STEP]
by(simp_all add: sc_jvm_state_invar_def sc.execute.correct_jvm_state_def)
[PROOF STATE]
proof (state)
this:
sc.execute.correct_state_ts P \<Phi> (thr (jvm_mstate_of_jvm_mstate' s)) (shr (jvm_mstate_of_jvm_mstate' s))
lock_thread_ok (locks (jvm_mstate_of_jvm_mstate' s)) (thr (jvm_mstate_of_jvm_mstate' s))

goal (1 subgoal):
 1. \<And>s tl s'. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s tl s'\<rbrakk> \<Longrightarrow> s' \<in> sc_jvm_state_invar P \<Phi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s) (t, jvm_thread_action_of_jvm_thread_action' ta) (jvm_mstate_of_jvm_mstate' s')
sc.execute.correct_state_ts P \<Phi> (thr (jvm_mstate_of_jvm_mstate' s)) (shr (jvm_mstate_of_jvm_mstate' s))
lock_thread_ok (locks (jvm_mstate_of_jvm_mstate' s)) (thr (jvm_mstate_of_jvm_mstate' s))
[PROOF STEP]
have "sc.execute.correct_state_ts P \<Phi> (thr (jvm_mstate_of_jvm_mstate' s')) (shr (jvm_mstate_of_jvm_mstate' s'))"
    and "lock_thread_ok (locks (jvm_mstate_of_jvm_mstate' s')) (thr (jvm_mstate_of_jvm_mstate' s'))"
[PROOF STATE]
proof (prove)
using this:
multithreaded_base.redT JVM_final (sc_execute_mexec P) convert_RA (jvm_mstate_of_jvm_mstate' s) (t, jvm_thread_action_of_jvm_thread_action' ta) (jvm_mstate_of_jvm_mstate' s')
sc.execute.correct_state_ts P \<Phi> (thr (jvm_mstate_of_jvm_mstate' s)) (shr (jvm_mstate_of_jvm_mstate' s))
lock_thread_ok (locks (jvm_mstate_of_jvm_mstate' s)) (thr (jvm_mstate_of_jvm_mstate' s))

goal (1 subgoal):
 1. sc.execute.correct_state_ts P \<Phi> (thr (jvm_mstate_of_jvm_mstate' s')) (shr (jvm_mstate_of_jvm_mstate' s')) &&& lock_thread_ok (locks (jvm_mstate_of_jvm_mstate' s')) (thr (jvm_mstate_of_jvm_mstate' s'))
[PROOF STEP]
by(blast intro: lifting_wf.redT_preserves[OF sc.execute.lifting_wf_correct_state, OF assms] sc.execute.exec_mthr.redT_preserves_lock_thread_ok)+
[PROOF STATE]
proof (state)
this:
sc.execute.correct_state_ts P \<Phi> (thr (jvm_mstate_of_jvm_mstate' s')) (shr (jvm_mstate_of_jvm_mstate' s'))
lock_thread_ok (locks (jvm_mstate_of_jvm_mstate' s')) (thr (jvm_mstate_of_jvm_mstate' s'))

goal (1 subgoal):
 1. \<And>s tl s'. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s tl s'\<rbrakk> \<Longrightarrow> s' \<in> sc_jvm_state_invar P \<Phi>
[PROOF STEP]
hence "jvm_mstate_of_jvm_mstate' s' \<in> sc.execute.correct_jvm_state P \<Phi>"
[PROOF STATE]
proof (prove)
using this:
sc.execute.correct_state_ts P \<Phi> (thr (jvm_mstate_of_jvm_mstate' s')) (shr (jvm_mstate_of_jvm_mstate' s'))
lock_thread_ok (locks (jvm_mstate_of_jvm_mstate' s')) (thr (jvm_mstate_of_jvm_mstate' s'))

goal (1 subgoal):
 1. jvm_mstate_of_jvm_mstate' s' \<in> sc.execute.correct_jvm_state P \<Phi>
[PROOF STEP]
by(simp add: sc.execute.correct_jvm_state_def)
[PROOF STATE]
proof (state)
this:
jvm_mstate_of_jvm_mstate' s' \<in> sc.execute.correct_jvm_state P \<Phi>

goal (1 subgoal):
 1. \<And>s tl s'. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s tl s'\<rbrakk> \<Longrightarrow> s' \<in> sc_jvm_state_invar P \<Phi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
jvm_mstate_of_jvm_mstate' s' \<in> sc.execute.correct_jvm_state P \<Phi>

goal (1 subgoal):
 1. \<And>s tl s'. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s tl s'\<rbrakk> \<Longrightarrow> s' \<in> sc_jvm_state_invar P \<Phi>
[PROOF STEP]
from red
[PROOF STATE]
proof (chain)
picking this:
multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s tl s'
[PROOF STEP]
have "ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s') (shr s')"
[PROOF STATE]
proof (prove)
using this:
multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s tl s'

goal (1 subgoal):
 1. ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s') (shr s')
[PROOF STEP]
unfolding tl
[PROOF STATE]
proof (prove)
using this:
multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s (t, ta) s'

goal (1 subgoal):
 1. ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s') (shr s')
[PROOF STEP]
proof(cases rule: multithreaded_base.redT.cases[consumes 1, case_names normal acquire])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>tb x sa taa x' m' s'a. \<lbrakk>s = sa; (t, ta) = (tb, taa); s' = s'a; pred.eval (sc_mexec P tb (x, shr sa)) (taa, x', m'); thr sa tb = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' sa tb taa; redT_upd sa tb taa x' m' s'a\<rbrakk> \<Longrightarrow> ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s') (shr s')
 2. \<And>sa tb x n s'a ln. \<lbrakk>s = sa; (t, ta) = (tb, K$ [], [], [], [], [], convert_RA ln); s' = s'a; thr sa tb = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset sa tb); may_acquire_all (locks sa) tb ln; 0 < ln $ n; s'a = (acquire_all (locks sa) tb ln, (thr sa(tb \<mapsto> (x, no_wait_locks)), shr sa), wset sa, interrupts sa)\<rbrakk> \<Longrightarrow> ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s') (shr s')
[PROOF STEP]
case acquire
[PROOF STATE]
proof (state)
this:
s = s_
(t, ta) = (t_, K$ [], [], [], [], [], convert_RA ln_)
s' = s'_
thr s_ t_ = \<lfloor>(x_, ln_)\<rfloor>
\<not> waiting (wset s_ t_)
may_acquire_all (locks s_) t_ ln_
0 < ln_ $ n_
s'_ = (acquire_all (locks s_) t_ ln_, (thr s_(t_ \<mapsto> (x_, no_wait_locks)), shr s_), wset s_, interrupts s_)

goal (2 subgoals):
 1. \<And>tb x sa taa x' m' s'a. \<lbrakk>s = sa; (t, ta) = (tb, taa); s' = s'a; pred.eval (sc_mexec P tb (x, shr sa)) (taa, x', m'); thr sa tb = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' sa tb taa; redT_upd sa tb taa x' m' s'a\<rbrakk> \<Longrightarrow> ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s') (shr s')
 2. \<And>sa tb x n s'a ln. \<lbrakk>s = sa; (t, ta) = (tb, K$ [], [], [], [], [], convert_RA ln); s' = s'a; thr sa tb = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset sa tb); may_acquire_all (locks sa) tb ln; 0 < ln $ n; s'a = (acquire_all (locks sa) tb ln, (thr sa(tb \<mapsto> (x, no_wait_locks)), shr sa), wset sa, interrupts sa)\<rbrakk> \<Longrightarrow> ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s') (shr s')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s = s_
(t, ta) = (t_, K$ [], [], [], [], [], convert_RA ln_)
s' = s'_
thr s_ t_ = \<lfloor>(x_, ln_)\<rfloor>
\<not> waiting (wset s_ t_)
may_acquire_all (locks s_) t_ ln_
0 < ln_ $ n_
s'_ = (acquire_all (locks s_) t_ ln_, (thr s_(t_ \<mapsto> (x_, no_wait_locks)), shr s_), wset s_, interrupts s_)

goal (1 subgoal):
 1. ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s') (shr s')
[PROOF STEP]
using invar
[PROOF STATE]
proof (prove)
using this:
s = s_
(t, ta) = (t_, K$ [], [], [], [], [], convert_RA ln_)
s' = s'_
thr s_ t_ = \<lfloor>(x_, ln_)\<rfloor>
\<not> waiting (wset s_ t_)
may_acquire_all (locks s_) t_ ln_
0 < ln_ $ n_
s'_ = (acquire_all (locks s_) t_ ln_, (thr s_(t_ \<mapsto> (x_, no_wait_locks)), shr s_), wset s_, interrupts s_)
s \<in> sc_jvm_state_invar P \<Phi>

goal (1 subgoal):
 1. ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s') (shr s')
[PROOF STEP]
by(fastforce simp add: sc_jvm_state_invar_def intro!: ts_okI dest: ts_okD bspec split: if_split_asm)
[PROOF STATE]
proof (state)
this:
ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s') (shr s')

goal (1 subgoal):
 1. \<And>tb x sa taa x' m' s'a. \<lbrakk>s = sa; (t, ta) = (tb, taa); s' = s'a; pred.eval (sc_mexec P tb (x, shr sa)) (taa, x', m'); thr sa tb = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' sa tb taa; redT_upd sa tb taa x' m' s'a\<rbrakk> \<Longrightarrow> ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s') (shr s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>tb x sa taa x' m' s'a. \<lbrakk>s = sa; (t, ta) = (tb, taa); s' = s'a; pred.eval (sc_mexec P tb (x, shr sa)) (taa, x', m'); thr sa tb = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' sa tb taa; redT_upd sa tb taa x' m' s'a\<rbrakk> \<Longrightarrow> ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s') (shr s')
[PROOF STEP]
case (normal t x s ta x' m' s')
[PROOF STATE]
proof (state)
this:
s__ = s
(t__, ta__) = (t, ta)
s'__ = s'
pred.eval (sc_mexec P t (x, shr s)) (ta, x', m')
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
final_thread.actions_ok JVM_final' s t ta
redT_upd s t ta x' m' s'

goal (1 subgoal):
 1. \<And>tb x sa taa x' m' s'a. \<lbrakk>s__ = sa; (t__, ta__) = (tb, taa); s'__ = s'a; pred.eval (sc_mexec P tb (x, shr sa)) (taa, x', m'); thr sa tb = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' sa tb taa; redT_upd sa tb taa x' m' s'a\<rbrakk> \<Longrightarrow> ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s'__) (shr s'__)
[PROOF STEP]
obtain xcp frs where x: "x = (xcp, frs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xcp frs. x = (xcp, frs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases x)
[PROOF STATE]
proof (state)
this:
x = (xcp, frs)

goal (1 subgoal):
 1. \<And>tb x sa taa x' m' s'a. \<lbrakk>s__ = sa; (t__, ta__) = (tb, taa); s'__ = s'a; pred.eval (sc_mexec P tb (x, shr sa)) (taa, x', m'); thr sa tb = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' sa tb taa; redT_upd sa tb taa x' m' s'a\<rbrakk> \<Longrightarrow> ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s'__) (shr s'__)
[PROOF STEP]
with invar normal tl
[PROOF STATE]
proof (chain)
picking this:
s__ \<in> sc_jvm_state_invar P \<Phi>
s__ = s
(t__, ta__) = (t, ta)
s'__ = s'
pred.eval (sc_mexec P t (x, shr s)) (ta, x', m')
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
final_thread.actions_ok JVM_final' s t ta
redT_upd s t ta x' m' s'
tl = (t__, ta__)
x = (xcp, frs)
[PROOF STEP]
have correct: "sc.execute.correct_state P \<Phi> t (jvm_state_of_jvm_state' (xcp, shr s, frs))"
      and ok: "jvm_state'_ok P (xcp, shr s, frs)"
[PROOF STATE]
proof (prove)
using this:
s__ \<in> sc_jvm_state_invar P \<Phi>
s__ = s
(t__, ta__) = (t, ta)
s'__ = s'
pred.eval (sc_mexec P t (x, shr s)) (ta, x', m')
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
final_thread.actions_ok JVM_final' s t ta
redT_upd s t ta x' m' s'
tl = (t__, ta__)
x = (xcp, frs)

goal (1 subgoal):
 1. sc.execute.correct_state P \<Phi> t (jvm_state_of_jvm_state' (xcp, shr s, frs)) &&& jvm_state'_ok P (xcp, shr s, frs)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s__ \<in> sc_jvm_state_invar P \<Phi>; s__ = s; (t__, ta__) = (t, ta); s'__ = s'; pred.eval (sc_mexec P t (x, shr s)) (ta, x', m'); thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' s t ta; redT_upd s t ta x' m' s'; tl = (t__, ta__); x = (xcp, frs)\<rbrakk> \<Longrightarrow> sc.execute.correct_state P \<Phi> t (jvm_state_of_jvm_state' (xcp, shr s, frs))
 2. \<lbrakk>s__ \<in> sc_jvm_state_invar P \<Phi>; s__ = s; (t__, ta__) = (t, ta); s'__ = s'; pred.eval (sc_mexec P t (x, shr s)) (ta, x', m'); thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' s t ta; redT_upd s t ta x' m' s'; tl = (t__, ta__); x = (xcp, frs)\<rbrakk> \<Longrightarrow> jvm_state'_ok P (xcp, shr s, frs)
[PROOF STEP]
apply(case_tac [!] s)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c d. \<lbrakk>s__ \<in> sc_jvm_state_invar P \<Phi>; s__ = s; (t__, ta__) = (t, ta); s'__ = s'; pred.eval (sc_mexec P t (x, shr s)) (ta, x', m'); thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' s t ta; redT_upd s t ta x' m' s'; tl = (t__, ta__); x = (xcp, frs); s = (a, b, c, d)\<rbrakk> \<Longrightarrow> sc.execute.correct_state P \<Phi> t (jvm_state_of_jvm_state' (xcp, shr s, frs))
 2. \<And>a b c d. \<lbrakk>s__ \<in> sc_jvm_state_invar P \<Phi>; s__ = s; (t__, ta__) = (t, ta); s'__ = s'; pred.eval (sc_mexec P t (x, shr s)) (ta, x', m'); thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' s t ta; redT_upd s t ta x' m' s'; tl = (t__, ta__); x = (xcp, frs); s = (a, b, c, d)\<rbrakk> \<Longrightarrow> jvm_state'_ok P (xcp, shr s, frs)
[PROOF STEP]
apply(fastforce simp add: sc_jvm_state_invar_def sc.execute.correct_jvm_state_def dest: ts_okD)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
sc.execute.correct_state P \<Phi> t (jvm_state_of_jvm_state' (xcp, shr s, frs))
jvm_state'_ok P (xcp, shr s, frs)

goal (1 subgoal):
 1. \<And>tb x sa taa x' m' s'a. \<lbrakk>s__ = sa; (t__, ta__) = (tb, taa); s'__ = s'a; pred.eval (sc_mexec P tb (x, shr sa)) (taa, x', m'); thr sa tb = \<lfloor>(x, no_wait_locks)\<rfloor>; final_thread.actions_ok JVM_final' sa tb taa; redT_upd sa tb taa x' m' s'a\<rbrakk> \<Longrightarrow> ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s'__) (shr s'__)
[PROOF STEP]
from normal x invar
[PROOF STATE]
proof (chain)
picking this:
s__ = s
(t__, ta__) = (t, ta)
s'__ = s'
pred.eval (sc_mexec P t (x, shr s)) (ta, x', m')
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
final_thread.actions_ok JVM_final' s t ta
redT_upd s t ta x' m' s'
x = (xcp, frs)
s__ \<in> sc_jvm_state_invar P \<Phi>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s__ = s
(t__, ta__) = (t, ta)
s'__ = s'
pred.eval (sc_mexec P t (x, shr s)) (ta, x', m')
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
final_thread.actions_ok JVM_final' s t ta
redT_upd s t ta x' m' s'
x = (xcp, frs)
s__ \<in> sc_jvm_state_invar P \<Phi>

goal (1 subgoal):
 1. ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s'__) (shr s'__)
[PROOF STEP]
apply(auto simp add: sc.exec_1_def final_thread.actions_ok_iff jvm_thread_action'_ok_def sc_jvm_state_invar_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab ac ad b ae ba ws'. \<lbrakk>s__ = s; s'__ = (redT_updLs (locks s) t a, (redT_updTs (thr s) aa(t \<mapsto> ((ae, ba), redT_updLns (locks s) t no_wait_locks a)), m'), ws', redT_updIs (interrupts s) ad); thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; x = (xcp, frs); ((a, aa, ab, ac, ad, b), ae, m', ba) \<in> sc_exec P t (xcp, shr s, frs); t__ = t; ta__ = (a, aa, ab, ac, ad, b); lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; s' = (redT_updLs (locks s) t a, (redT_updTs (thr s) aa(t \<mapsto> ((ae, ba), redT_updLns (locks s) t no_wait_locks a)), m'), ws', redT_updIs (interrupts s) ad); thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; ta = (a, aa, ab, ac, ad, b); x' = (ae, ba)\<rbrakk> \<Longrightarrow> ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (redT_updTs (thr s) aa(t \<mapsto> ((ae, ba), redT_updLns (locks s) t no_wait_locks a))) m'
[PROOF STEP]
apply hypsubst_thin
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab ac ad b ae ba ws'. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; ((a, aa, ab, ac, ad, b), ae, m', ba) \<in> sc_exec P t (xcp, shr s, frs); lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad\<rbrakk> \<Longrightarrow> ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (redT_updTs (thr s) aa(t \<mapsto> ((ae, ba), redT_updLns (locks s) t no_wait_locks a))) m'
[PROOF STEP]
apply(drule sc.exec_correct_state(3)[OF assms correct ok])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab ac ad b ae ba ws'. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; jvm_ta_state'_ok P ((a, aa, ab, ac, ad, b), ae, m', ba)\<rbrakk> \<Longrightarrow> ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (redT_updTs (thr s) aa(t \<mapsto> ((ae, ba), redT_updLns (locks s) t no_wait_locks a))) m'
[PROOF STEP]
apply(rule ts_okI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab ac ad b ae ba ws' t x ln. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; jvm_ta_state'_ok P ((a, aa, ab, ac, ad, b), ae, m', ba); (redT_updTs (thr s) aa(t \<mapsto> ((ae, ba), redT_updLns (locks s) t no_wait_locks a))) t = \<lfloor>(x, ln)\<rfloor>\<rbrakk> \<Longrightarrow> (case x of (xcp, frs) \<Rightarrow> \<lambda>h. \<forall>x\<in>set frs. frame'_ok P x) m'
[PROOF STEP]
apply(clarsimp split: if_split_asm simp add: jvm_thread_action'_ok_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab ac ad ws' b ag ah bb ai aj ak al bc. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; \<forall>nt\<in>set aa. \<forall>t x. (\<exists>h. nt = NewThread t x h) \<longrightarrow> jvm_thread_state'_ok P x; \<forall>x\<in>set b. frame'_ok P x; ((ag, ah, bb), ai, aj, ak, al, bc) \<in> set b\<rbrakk> \<Longrightarrow> ag = drop bc (instrs_of P ak al) \<and> (ah, bb) = snd (snd (the (snd (snd (snd (method P ak al))))))
 2. \<And>a aa ab ac ad ba ws' t ae b ln af ag bb ah ai aj ak bc. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>nt\<in>set aa. \<forall>t x. (\<exists>h. nt = NewThread t x h) \<longrightarrow> jvm_thread_state'_ok P x; \<forall>x\<in>set ba. frame'_ok P x; redT_updTs (thr s) aa t = \<lfloor>((ae, b), ln)\<rfloor>; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
[PROOF STEP]
apply(drule (1) bspec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab ac ad ws' b ag ah bb ai aj ak al bc. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; \<forall>nt\<in>set aa. \<forall>t x. (\<exists>h. nt = NewThread t x h) \<longrightarrow> jvm_thread_state'_ok P x; ((ag, ah, bb), ai, aj, ak, al, bc) \<in> set b; frame'_ok P ((ag, ah, bb), ai, aj, ak, al, bc)\<rbrakk> \<Longrightarrow> ag = drop bc (instrs_of P ak al) \<and> (ah, bb) = snd (snd (the (snd (snd (snd (method P ak al))))))
 2. \<And>a aa ab ac ad ba ws' t ae b ln af ag bb ah ai aj ak bc. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>nt\<in>set aa. \<forall>t x. (\<exists>h. nt = NewThread t x h) \<longrightarrow> jvm_thread_state'_ok P x; \<forall>x\<in>set ba. frame'_ok P x; redT_updTs (thr s) aa t = \<lfloor>((ae, b), ln)\<rfloor>; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab ac ad ba ws' t ae b ln af ag bb ah ai aj ak bc. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>nt\<in>set aa. \<forall>t x. (\<exists>h. nt = NewThread t x h) \<longrightarrow> jvm_thread_state'_ok P x; \<forall>x\<in>set ba. frame'_ok P x; redT_updTs (thr s) aa t = \<lfloor>((ae, b), ln)\<rfloor>; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
[PROOF STEP]
apply(case_tac "thr s t")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab ac ad ba ws' t ae b ln af ag bb ah ai aj ak bc. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>nt\<in>set aa. \<forall>t x. (\<exists>h. nt = NewThread t x h) \<longrightarrow> jvm_thread_state'_ok P x; \<forall>x\<in>set ba. frame'_ok P x; redT_updTs (thr s) aa t = \<lfloor>((ae, b), ln)\<rfloor>; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b; thr s t = None\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
 2. \<And>a aa ab ac ad ba ws' t ae b ln af ag bb ah ai aj ak bc al. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>nt\<in>set aa. \<forall>t x. (\<exists>h. nt = NewThread t x h) \<longrightarrow> jvm_thread_state'_ok P x; \<forall>x\<in>set ba. frame'_ok P x; redT_updTs (thr s) aa t = \<lfloor>((ae, b), ln)\<rfloor>; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b; thr s t = \<lfloor>al\<rfloor>\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
[PROOF STEP]
apply(drule (2) redT_updTs_new_thread)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab ac ad ba ws' t ae b ln af ag bb ah ai aj ak bc. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>nt\<in>set aa. \<forall>t x. (\<exists>h. nt = NewThread t x h) \<longrightarrow> jvm_thread_state'_ok P x; \<forall>x\<in>set ba. frame'_ok P x; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b; thr s t = None; \<exists>m. NewThread t (ae, b) m \<in> set aa \<and> ln = no_wait_locks\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
 2. \<And>a aa ab ac ad ba ws' t ae b ln af ag bb ah ai aj ak bc al. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>nt\<in>set aa. \<forall>t x. (\<exists>h. nt = NewThread t x h) \<longrightarrow> jvm_thread_state'_ok P x; \<forall>x\<in>set ba. frame'_ok P x; redT_updTs (thr s) aa t = \<lfloor>((ae, b), ln)\<rfloor>; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b; thr s t = \<lfloor>al\<rfloor>\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab ac ad ba ws' t ae b af ag bb ah ai aj ak bc m. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>nt\<in>set aa. \<forall>t x. (\<exists>h. nt = NewThread t x h) \<longrightarrow> jvm_thread_state'_ok P x; \<forall>x\<in>set ba. frame'_ok P x; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b; thr s t = None; NewThread t (ae, b) m \<in> set aa\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
 2. \<And>a aa ab ac ad ba ws' t ae b ln af ag bb ah ai aj ak bc al. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>nt\<in>set aa. \<forall>t x. (\<exists>h. nt = NewThread t x h) \<longrightarrow> jvm_thread_state'_ok P x; \<forall>x\<in>set ba. frame'_ok P x; redT_updTs (thr s) aa t = \<lfloor>((ae, b), ln)\<rfloor>; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b; thr s t = \<lfloor>al\<rfloor>\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
[PROOF STEP]
apply(drule (1) bspec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab ac ad ba ws' t ae b af ag bb ah ai aj ak bc m. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>x\<in>set ba. frame'_ok P x; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b; thr s t = None; NewThread t (ae, b) m \<in> set aa; \<forall>ta x. (\<exists>h. NewThread t (ae, b) m = NewThread ta x h) \<longrightarrow> jvm_thread_state'_ok P x\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
 2. \<And>a aa ab ac ad ba ws' t ae b ln af ag bb ah ai aj ak bc al. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>nt\<in>set aa. \<forall>t x. (\<exists>h. nt = NewThread t x h) \<longrightarrow> jvm_thread_state'_ok P x; \<forall>x\<in>set ba. frame'_ok P x; redT_updTs (thr s) aa t = \<lfloor>((ae, b), ln)\<rfloor>; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b; thr s t = \<lfloor>al\<rfloor>\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab ac ad ba ws' t ae b af ag bb ah ai aj ak bc m. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>x\<in>set ba. frame'_ok P x; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b; thr s t = None; NewThread t (ae, b) m \<in> set aa; Ball (set b) (frame'_ok P)\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
 2. \<And>a aa ab ac ad ba ws' t ae b ln af ag bb ah ai aj ak bc al. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>nt\<in>set aa. \<forall>t x. (\<exists>h. nt = NewThread t x h) \<longrightarrow> jvm_thread_state'_ok P x; \<forall>x\<in>set ba. frame'_ok P x; redT_updTs (thr s) aa t = \<lfloor>((ae, b), ln)\<rfloor>; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b; thr s t = \<lfloor>al\<rfloor>\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
[PROOF STEP]
apply(drule (1) bspec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab ac ad ba ws' t ae b af ag bb ah ai aj ak bc m. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>x\<in>set ba. frame'_ok P x; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b; thr s t = None; NewThread t (ae, b) m \<in> set aa; frame'_ok P ((af, ag, bb), ah, ai, aj, ak, bc)\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
 2. \<And>a aa ab ac ad ba ws' t ae b ln af ag bb ah ai aj ak bc al. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>nt\<in>set aa. \<forall>t x. (\<exists>h. nt = NewThread t x h) \<longrightarrow> jvm_thread_state'_ok P x; \<forall>x\<in>set ba. frame'_ok P x; redT_updTs (thr s) aa t = \<lfloor>((ae, b), ln)\<rfloor>; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b; thr s t = \<lfloor>al\<rfloor>\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab ac ad ba ws' t ae b ln af ag bb ah ai aj ak bc al. \<lbrakk>thr s t = \<lfloor>((xcp, frs), no_wait_locks)\<rfloor>; lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>nt\<in>set aa. \<forall>t x. (\<exists>h. nt = NewThread t x h) \<longrightarrow> jvm_thread_state'_ok P x; \<forall>x\<in>set ba. frame'_ok P x; redT_updTs (thr s) aa t = \<lfloor>((ae, b), ln)\<rfloor>; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b; thr s t = \<lfloor>al\<rfloor>\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
[PROOF STEP]
apply(erule thin_rl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab ac ad ba ws' t ae b ln af ag bb ah ai aj ak bc al. \<lbrakk>lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>nt\<in>set aa. \<forall>t x. (\<exists>h. nt = NewThread t x h) \<longrightarrow> jvm_thread_state'_ok P x; \<forall>x\<in>set ba. frame'_ok P x; redT_updTs (thr s) aa t = \<lfloor>((ae, b), ln)\<rfloor>; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b; thr s t = \<lfloor>al\<rfloor>\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
[PROOF STEP]
apply(frule (1) redT_updTs_Some)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab ac ad ba ws' t ae b ln af ag bb ah ai aj ak bc al. \<lbrakk>lock_ok_las (locks s) t a; jvm_mstate_of_jvm_mstate' s \<in> sc.execute.correct_jvm_state P \<Phi>; ts_ok (\<lambda>t (xcp, frs) h. \<forall>x\<in>set frs. frame'_ok P x) (thr s) (shr s); redT_updWs t (wset s) ac ws'; thread_oks (thr s) aa; final_thread.cond_action_oks JVM_final' s t ab; wset_actions_ok (wset s) t ac; interrupt_actions_ok (interrupts s) ad; t \<noteq> t; \<forall>nt\<in>set aa. \<forall>t x. (\<exists>h. nt = NewThread t x h) \<longrightarrow> jvm_thread_state'_ok P x; \<forall>x\<in>set ba. frame'_ok P x; redT_updTs (thr s) aa t = \<lfloor>((ae, b), ln)\<rfloor>; ((af, ag, bb), ah, ai, aj, ak, bc) \<in> set b; thr s t = \<lfloor>al\<rfloor>; redT_updTs (thr s) aa t = \<lfloor>al\<rfloor>\<rbrakk> \<Longrightarrow> af = drop bc (instrs_of P aj ak) \<and> (ag, bb) = snd (snd (the (snd (snd (snd (method P aj ak))))))
[PROOF STEP]
apply(fastforce dest: ts_okD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s'__) (shr s'__)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s') (shr s')

goal (1 subgoal):
 1. \<And>s tl s'. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA s tl s'\<rbrakk> \<Longrightarrow> s' \<in> sc_jvm_state_invar P \<Phi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
jvm_mstate_of_jvm_mstate' s' \<in> sc.execute.correct_jvm_state P \<Phi>
ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s') (shr s')
[PROOF STEP]
show "s' \<in> sc_jvm_state_invar P \<Phi>"
[PROOF STATE]
proof (prove)
using this:
jvm_mstate_of_jvm_mstate' s' \<in> sc.execute.correct_jvm_state P \<Phi>
ts_ok (\<lambda>t (xcp, frs) h. \<forall>f\<in>set frs. frame'_ok P f) (thr s') (shr s')

goal (1 subgoal):
 1. s' \<in> sc_jvm_state_invar P \<Phi>
[PROOF STEP]
by(simp add: sc_jvm_state_invar_def)
[PROOF STATE]
proof (state)
this:
s' \<in> sc_jvm_state_invar P \<Phi>

goal:
No subgoals!
[PROOF STEP]
qed