theory Tcb_AI

lemma decode_domain_inv_wf:
  "\<lbrace>valid_objs and valid_global_refs and
     (\<lambda>s. \<forall>x\<in>set excs. s \<turnstile> fst x) and
     (\<lambda>s. \<forall>x\<in>set excs. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s)\<rbrace>
     decode_domain_invocation label args excs
   \<lbrace>\<lambda>(t, d) s. tcb_at t s \<and> t \<noteq> idle_thread s\<rbrace>, -" apply (clarsimp simp: decode_domain_invocation_def whenE_def split del: if_split
        | wp hoare_vcg_if_splitE | wpc)+ apply (erule ballE[where x="hd excs"]) apply (clarsimp simp: valid_cap_simps) apply (drule(1) idle_no_ex_cap) apply (erule ballE[where x="hd excs"]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_global_refs and (\<lambda>s. \<forall>x\<in>set excs. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excs. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s)\<rbrace> decode_domain_invocation label args excs \<lbrace>\<lambda>(t, d) s. tcb_at t s \<and> t \<noteq> idle_thread s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>valid_objs s; valid_global_refs s; \<forall>x\<in>set excs. s \<turnstile> fst x; \<forall>x\<in>set excs. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; gen_invocation_type label = DomainSetSet; args = x # xa; \<not> numDomains \<le> unat x; excs \<noteq> []; fst (hd excs) = ThreadCap xb\<rbrakk> \<Longrightarrow> tcb_at xb s \<and> xb \<noteq> idle_thread s proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb. \<lbrakk>valid_objs s; valid_global_refs s; \<forall>x\<in>set excs. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; gen_invocation_type label = DomainSetSet; args = x # xa; \<not> numDomains \<le> unat x; excs \<noteq> []; fst (hd excs) = ThreadCap xb; s \<turnstile> fst (hd excs)\<rbrakk> \<Longrightarrow> tcb_at xb s \<and> xb \<noteq> idle_thread s
 2. \<And>s x xa xb. \<lbrakk>valid_objs s; valid_global_refs s; \<forall>x\<in>set excs. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; gen_invocation_type label = DomainSetSet; args = x # xa; \<not> numDomains \<le> unat x; excs \<noteq> []; fst (hd excs) = ThreadCap xb; hd excs \<notin> set excs\<rbrakk> \<Longrightarrow> tcb_at xb s \<and> xb \<noteq> idle_thread s proof (prove)
goal (2 subgoals):
 1. \<And>s x xa. \<lbrakk>valid_objs s; valid_global_refs s; \<forall>x\<in>set excs. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; gen_invocation_type label = DomainSetSet; args = x # xa; \<not> numDomains \<le> unat x; excs \<noteq> []; fst (hd excs) = ThreadCap (idle_thread s); cap_aligned (ThreadCap (idle_thread s)); tcb_at (idle_thread s) s\<rbrakk> \<Longrightarrow> False
 2. \<And>s x xa xb. \<lbrakk>valid_objs s; valid_global_refs s; \<forall>x\<in>set excs. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; gen_invocation_type label = DomainSetSet; args = x # xa; \<not> numDomains \<le> unat x; excs \<noteq> []; fst (hd excs) = ThreadCap xb; hd excs \<notin> set excs\<rbrakk> \<Longrightarrow> tcb_at xb s \<and> xb \<noteq> idle_thread s proof (prove)
goal (2 subgoals):
 1. \<And>s x xa. \<lbrakk>valid_objs s; \<forall>x\<in>set excs. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; gen_invocation_type label = DomainSetSet; args = x # xa; \<not> numDomains \<le> unat x; excs \<noteq> []; fst (hd excs) = ThreadCap (idle_thread s); cap_aligned (ThreadCap (idle_thread s)); tcb_at (idle_thread s) s; \<not> ex_nonz_cap_to (idle_thread s) s\<rbrakk> \<Longrightarrow> False
 2. \<And>s x xa xb. \<lbrakk>valid_objs s; valid_global_refs s; \<forall>x\<in>set excs. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; gen_invocation_type label = DomainSetSet; args = x # xa; \<not> numDomains \<le> unat x; excs \<noteq> []; fst (hd excs) = ThreadCap xb; hd excs \<notin> set excs\<rbrakk> \<Longrightarrow> tcb_at xb s \<and> xb \<noteq> idle_thread s proof (prove)
goal (3 subgoals):
 1. \<And>s x xa. \<lbrakk>valid_objs s; gen_invocation_type label = DomainSetSet; args = x # xa; \<not> numDomains \<le> unat x; excs \<noteq> []; fst (hd excs) = ThreadCap (idle_thread s); cap_aligned (ThreadCap (idle_thread s)); tcb_at (idle_thread s) s; \<not> ex_nonz_cap_to (idle_thread s) s; \<forall>r\<in>zobj_refs (fst (hd excs)). ex_nonz_cap_to r s\<rbrakk> \<Longrightarrow> False
 2. \<And>s x xa. \<lbrakk>valid_objs s; gen_invocation_type label = DomainSetSet; args = x # xa; \<not> numDomains \<le> unat x; excs \<noteq> []; fst (hd excs) = ThreadCap (idle_thread s); cap_aligned (ThreadCap (idle_thread s)); tcb_at (idle_thread s) s; \<not> ex_nonz_cap_to (idle_thread s) s; hd excs \<notin> set excs\<rbrakk> \<Longrightarrow> False
 3. \<And>s x xa xb. \<lbrakk>valid_objs s; valid_global_refs s; \<forall>x\<in>set excs. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s; gen_invocation_type label = DomainSetSet; args = x # xa; \<not> numDomains \<le> unat x; excs \<noteq> []; fst (hd excs) = ThreadCap xb; hd excs \<notin> set excs\<rbrakk> \<Longrightarrow> tcb_at xb s \<and> xb \<noteq> idle_thread s proof (prove)
goal:
No subgoals!