theory Finalise_IF

lemma set_thread_state_ext_runnable_reads_respects:
  "reads_respects aag l (st_tcb_at runnable ref) (set_thread_state_ext ref)" 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>" and Q="\<lambda>rv _. runnable rv"]) 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 (rule gen_asm_ev2) apply (clarsimp simp: equiv_valid_def2[symmetric] | wp)+ apply (simp add: reads_equiv_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (st_tcb_at runnable ref) (set_thread_state_ext ref) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (st_tcb_at runnable ref) (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. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (=) (st_tcb_at runnable ref) (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. reads_equiv_valid_rv_inv (affects_equiv aag l) aag (\<lambda>_ _. True) (st_tcb_at runnable ref) (get_thread_state ref)
 2. \<And>rv rv'. True \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. runnable rv) (\<lambda>_. runnable 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. \<lbrace>st_tcb_at runnable ref\<rbrace> get_thread_state ref \<lbrace>\<lambda>rv _. runnable rv\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. True \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. runnable rv) (\<lambda>_. runnable 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. \<lbrace>st_tcb_at runnable ref\<rbrace> get_thread_state ref \<lbrace>\<lambda>rv _. runnable rv\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. \<lbrakk>True; runnable rv; runnable rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (=) (\<lambda>_. True) (\<lambda>_. True) (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. \<lbrace>st_tcb_at runnable ref\<rbrace> get_thread_state ref \<lbrace>\<lambda>rv _. runnable rv\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. \<lbrakk>runnable rv; runnable rv'\<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. \<lbrace>st_tcb_at runnable ref\<rbrace> get_thread_state ref \<lbrace>\<lambda>rv _. runnable rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at runnable ref\<rbrace> get_thread_state ref \<lbrace>\<lambda>rv _. runnable rv\<rbrace> proof (prove)
goal:
No subgoals!