theory Finalise_IF

lemma set_thread_state_ext_reads_respects:
  "reads_respects aag l (\<lambda>s. is_subject aag (cur_thread s)) (set_thread_state_ext ref)" apply (case_tac "is_subject aag ref") apply (simp add: set_thread_state_ext_def when_def get_thread_state_def | wp thread_get_rev)+ apply (simp add: reads_equiv_def) apply (simp add: set_thread_state_ext_def when_def) apply (simp add: equiv_valid_def2) apply (rule equiv_valid_rv_bind[where W="\<top>\<top>"]) apply (clarsimp simp: equiv_valid_2_def get_thread_state_def thread_get_def gets_the_def
                          return_def bind_def assert_opt_def gets_def get_tcb_def fail_def get_def
                   split: option.splits) apply clarsimp apply (rule equiv_valid_2_bind[where R'="(=)" and Q="\<lambda>rv _. rv \<noteq> ref" and Q'="\<lambda>rv _. rv \<noteq> ref"]) apply (rule gen_asm_ev2) apply (simp add: equiv_valid_def2[symmetric] | wp)+ apply (clarsimp simp: reads_equiv_def) apply (subst equiv_valid_def2[symmetric]) apply wp+ apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>s. is_subject aag (cur_thread s)) (set_thread_state_ext ref) proof (prove)
goal (2 subgoals):
 1. is_subject aag ref \<Longrightarrow> reads_respects aag l (\<lambda>s. is_subject aag (cur_thread s)) (set_thread_state_ext ref)
 2. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> reads_respects aag l (\<lambda>s. is_subject aag (cur_thread s)) (set_thread_state_ext ref) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag ref; is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t) \<and> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> scheduler_action s = scheduler_action t)
 2. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> reads_respects aag l (\<lambda>s. is_subject aag (cur_thread s)) (set_thread_state_ext ref) proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> reads_respects aag l (\<lambda>s. is_subject aag (cur_thread s)) (set_thread_state_ext ref) proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> reads_respects aag l (\<lambda>s. is_subject aag (cur_thread s)) (do ts <- get_thread_state ref;
cur <- gets cur_thread;
action <- gets scheduler_action;
if \<not> runnable ts \<and> cur = ref \<and> action = resume_cur_thread then set_scheduler_action choose_new_thread else return ()
od) proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (\<lambda>s. is_subject aag (cur_thread s)) (do ts <- get_thread_state ref;
cur <- gets cur_thread;
action <- gets scheduler_action;
if \<not> runnable ts \<and> cur = ref \<and> action = resume_cur_thread then set_scheduler_action choose_new_thread else return ()
od) proof (prove)
goal (3 subgoals):
 1. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>_ _. True) (\<lambda>s. is_subject aag (cur_thread s)) (get_thread_state ref)
 2. \<And>rv rv'. \<lbrakk>pasObjectAbs aag ref \<noteq> pasSubject aag; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q22 rv) (?Q22 rv') (do cur <- gets cur_thread;
action <- gets scheduler_action;
if \<not> runnable rv \<and> cur = ref \<and> action = resume_cur_thread then set_scheduler_action choose_new_thread else return ()
od) (do cur <- gets cur_thread;
action <- gets scheduler_action;
if \<not> runnable rv' \<and> cur = ref \<and> action = resume_cur_thread then set_scheduler_action choose_new_thread else return ()
od)
 3. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>\<lambda>s. is_subject aag (cur_thread s)\<rbrace> get_thread_state ref \<lbrace>?Q22\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. \<lbrakk>pasObjectAbs aag ref \<noteq> pasSubject aag; True\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q22 rv) (?Q22 rv') (do cur <- gets cur_thread;
action <- gets scheduler_action;
if \<not> runnable rv \<and> cur = ref \<and> action = resume_cur_thread then set_scheduler_action choose_new_thread else return ()
od) (do cur <- gets cur_thread;
action <- gets scheduler_action;
if \<not> runnable rv' \<and> cur = ref \<and> action = resume_cur_thread then set_scheduler_action choose_new_thread else return ()
od)
 2. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>\<lambda>s. is_subject aag (cur_thread s)\<rbrace> get_thread_state ref \<lbrace>?Q22\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?Q22 rv) (?Q22 rv') (do cur <- gets cur_thread;
action <- gets scheduler_action;
if \<not> runnable rv \<and> cur = ref \<and> action = resume_cur_thread then set_scheduler_action choose_new_thread else return ()
od) (do cur <- gets cur_thread;
action <- gets scheduler_action;
if \<not> runnable rv' \<and> cur = ref \<and> action = resume_cur_thread then set_scheduler_action choose_new_thread else return ()
od)
 2. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>\<lambda>s. is_subject aag (cur_thread s)\<rbrace> get_thread_state ref \<lbrace>?Q22\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag ref \<noteq> pasSubject aag; rva = rv'a\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. rva \<noteq> ref) (\<lambda>_. rv'a \<noteq> ref) (do action <- gets scheduler_action;
if \<not> runnable rv \<and> rva = ref \<and> action = resume_cur_thread then set_scheduler_action choose_new_thread else return ()
od) (do action <- gets scheduler_action;
if \<not> runnable rv' \<and> rv'a = ref \<and> action = resume_cur_thread then set_scheduler_action choose_new_thread else return ()
od)
 2. \<And>rv rv'. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?P'76 rv) (?P'76 rv') (gets cur_thread) (gets cur_thread)
 3. \<And>rv rv'. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?S'77 rv\<rbrace> gets cur_thread \<lbrace>\<lambda>rv _. rv \<noteq> ref\<rbrace>
 4. \<And>rv rv'. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?S'77 rv'\<rbrace> gets cur_thread \<lbrace>\<lambda>rv _. rv \<noteq> ref\<rbrace>
 5. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>\<lambda>s. is_subject aag (cur_thread s)\<rbrace> get_thread_state ref \<lbrace>\<lambda>rv s. ?P'76 rv s \<and> ?S'77 rv s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>pasObjectAbs aag ref \<noteq> pasSubject aag; rva = rv'a; rva \<noteq> ref; rv'a \<noteq> ref\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (\<lambda>_. True) (do action <- gets scheduler_action;
if \<not> runnable rv \<and> rva = ref \<and> action = resume_cur_thread then set_scheduler_action choose_new_thread else return ()
od) (do action <- gets scheduler_action;
if \<not> runnable rv' \<and> rv'a = ref \<and> action = resume_cur_thread then set_scheduler_action choose_new_thread else return ()
od)
 2. \<And>rv rv'. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?P'76 rv) (?P'76 rv') (gets cur_thread) (gets cur_thread)
 3. \<And>rv rv'. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?S'77 rv\<rbrace> gets cur_thread \<lbrace>\<lambda>rv _. rv \<noteq> ref\<rbrace>
 4. \<And>rv rv'. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?S'77 rv'\<rbrace> gets cur_thread \<lbrace>\<lambda>rv _. rv \<noteq> ref\<rbrace>
 5. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>\<lambda>s. is_subject aag (cur_thread s)\<rbrace> get_thread_state ref \<lbrace>\<lambda>rv s. ?P'76 rv s \<and> ?S'77 rv s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rva rv'a. \<lbrakk>pasObjectAbs aag ref \<noteq> pasSubject aag; rva = rv'a; rv'a \<noteq> ref\<rbrakk> \<Longrightarrow> \<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> scheduler_action s = scheduler_action t
 2. \<And>rv rv'. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?P'76 rv) (?P'76 rv') (gets cur_thread) (gets cur_thread)
 3. \<And>rv rv'. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?S'77 rv\<rbrace> gets cur_thread \<lbrace>\<lambda>rv _. rv \<noteq> ref\<rbrace>
 4. \<And>rv rv'. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?S'77 rv'\<rbrace> gets cur_thread \<lbrace>\<lambda>rv _. rv \<noteq> ref\<rbrace>
 5. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>\<lambda>s. is_subject aag (cur_thread s)\<rbrace> get_thread_state ref \<lbrace>\<lambda>rv s. ?P'76 rv s \<and> ?S'77 rv s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (?P'76 rv) (?P'76 rv') (gets cur_thread) (gets cur_thread)
 2. \<And>rv rv'. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?S'77 rv\<rbrace> gets cur_thread \<lbrace>\<lambda>rv _. rv \<noteq> ref\<rbrace>
 3. \<And>rv rv'. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?S'77 rv'\<rbrace> gets cur_thread \<lbrace>\<lambda>rv _. rv \<noteq> ref\<rbrace>
 4. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>\<lambda>s. is_subject aag (cur_thread s)\<rbrace> get_thread_state ref \<lbrace>\<lambda>rv s. ?P'76 rv s \<and> ?S'77 rv s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> reads_respects aag l (\<lambda>s. ?P'94) (gets cur_thread)
 2. \<And>rv rv'. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?S'77 rv\<rbrace> gets cur_thread \<lbrace>\<lambda>rv _. rv \<noteq> ref\<rbrace>
 3. \<And>rv rv'. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>?S'77 rv'\<rbrace> gets cur_thread \<lbrace>\<lambda>rv _. rv \<noteq> ref\<rbrace>
 4. pasObjectAbs aag ref \<noteq> pasSubject aag \<Longrightarrow> \<lbrace>\<lambda>s. is_subject aag (cur_thread s)\<rbrace> get_thread_state ref \<lbrace>\<lambda>rv s. ?P'94 \<and> ?S'77 rv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag ref \<noteq> pasSubject aag; is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t) \<and> cur_thread s \<noteq> ref proof (prove)
goal:
No subgoals!