theory TcbAcc_AI

lemma sts_tcb_cap_valid_cases:
  "\<lbrace>\<lambda>s. (t = t' \<longrightarrow> (case tcb_cap_cases ref of
                         None \<Rightarrow> True
                       | Some (getF, setF, restr) \<Rightarrow> restr t ts cap)
                   \<and> (ref = tcb_cnode_index 4 \<longrightarrow>
                        (\<forall>tcb. ko_at (TCB tcb) t' s \<longrightarrow>
                             valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))) \<and>
        (t \<noteq> t' \<longrightarrow> tcb_cap_valid cap (t', ref) s)\<rbrace>
   set_thread_state t ts
   \<lbrace>\<lambda>_ s. tcb_cap_valid cap (t', ref) s\<rbrace>" apply (rule hoare_pre) apply (simp add: tcb_cap_valid_def tcb_at_typ) apply (subst imp_conv_disj) apply (wp hoare_vcg_disj_lift sts_st_tcb_at_cases
             hoare_vcg_const_imp_lift sts_tcb_ko_at
             hoare_vcg_all_lift) apply (clarsimp simp: tcb_at_typ tcb_cap_valid_def split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (t = t' \<longrightarrow> (case tcb_cap_cases ref of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr t ts cap) \<and> (ref = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) t' s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))) \<and> (t \<noteq> t' \<longrightarrow> tcb_cap_valid cap (t', ref) s)\<rbrace> set_thread_state t ts \<lbrace>\<lambda>_. tcb_cap_valid cap (t', ref)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_thread_state t ts \<lbrace>\<lambda>_. tcb_cap_valid cap (t', ref)\<rbrace>
 2. \<And>s. (t = t' \<longrightarrow> (case tcb_cap_cases ref of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr t ts cap) \<and> (ref = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) t' s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))) \<and> (t \<noteq> t' \<longrightarrow> tcb_cap_valid cap (t', ref) s) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_thread_state t ts \<lbrace>\<lambda>_ s. typ_at ATCB t' s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases ref of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst (t', ref)) st cap) t' s \<and> (ref = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) t' s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))\<rbrace>
 2. \<And>s. (t = t' \<longrightarrow> (case tcb_cap_cases ref of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr t ts cap) \<and> (ref = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) t' s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))) \<and> (t \<noteq> t' \<longrightarrow> tcb_cap_valid cap (t', ref) s) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_thread_state t ts \<lbrace>\<lambda>_ s. \<not> typ_at ATCB t' s \<or> st_tcb_at (\<lambda>st. case tcb_cap_cases ref of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst (t', ref)) st cap) t' s \<and> (ref = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) t' s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))\<rbrace>
 2. \<And>s. (t = t' \<longrightarrow> (case tcb_cap_cases ref of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr t ts cap) \<and> (ref = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) t' s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))) \<and> (t \<noteq> t' \<longrightarrow> tcb_cap_valid cap (t', ref) s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (t = t' \<longrightarrow> (case tcb_cap_cases ref of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr t ts cap) \<and> (ref = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) t' s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))) \<and> (t \<noteq> t' \<longrightarrow> tcb_cap_valid cap (t', ref) s) \<Longrightarrow> \<not> typ_at ATCB t' s \<or> ((t = t' \<longrightarrow> (case tcb_cap_cases ref of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst (t', ref)) ts cap)) \<and> (t \<noteq> t' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases ref of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst (t', ref)) st cap) t' s)) \<and> (ref = tcb_cnode_index 4 \<longrightarrow> (\<forall>x v'. x = (if t = t' then v'\<lparr>tcb_state := ts\<rparr> else v') \<longrightarrow> ko_at (TCB v') t' s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer x))) proof (prove)
goal:
No subgoals!