theory TcbAcc_AI

lemma thread_set_valid_ioc_trivial:
  assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
                  getF (f tcb) = getF tcb"
  shows "\<lbrace>valid_ioc\<rbrace> thread_set f p \<lbrace>\<lambda>_. valid_ioc\<rbrace>" apply (simp add: thread_set_def, wp set_object_valid_ioc_caps) apply clarsimp apply (rule conjI) apply clarsimp apply (clarsimp simp: valid_ioc_def) apply (drule spec, drule spec, erule impE, assumption) apply (cut_tac tcb=y in x) apply (clarsimp simp: cte_wp_at_cases get_tcb_def cap_of_def null_filter_def
                        split_def tcb_cnode_map_tcb_cap_cases
                 split: option.splits Structures_A.kernel_object.splits) apply (drule_tac x="(get,set,restr)" in bspec) apply (fastforce simp: ranI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> thread_set f p \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_ioc s \<Longrightarrow> get_tcb p s \<noteq> None \<longrightarrow> valid_ioc s \<and> typ_at (a_type (TCB (f (the (get_tcb p s))))) p s \<and> (\<forall>b. is_original_cap s (p, b) \<longrightarrow> null_filter (cap_of (TCB (f (the (get_tcb p s))))) b \<noteq> None) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>valid_ioc s; get_tcb p s = Some y\<rbrakk> \<Longrightarrow> typ_at ATCB p s \<and> (\<forall>b. is_original_cap s (p, b) \<longrightarrow> (\<exists>ya. null_filter (cap_of (TCB (f y))) b = Some ya)) proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>valid_ioc s; get_tcb p s = Some y\<rbrakk> \<Longrightarrow> typ_at ATCB p s
 2. \<And>s y. \<lbrakk>valid_ioc s; get_tcb p s = Some y\<rbrakk> \<Longrightarrow> \<forall>b. is_original_cap s (p, b) \<longrightarrow> (\<exists>ya. null_filter (cap_of (TCB (f y))) b = Some ya) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>valid_ioc s; get_tcb p s = Some y\<rbrakk> \<Longrightarrow> \<forall>b. is_original_cap s (p, b) \<longrightarrow> (\<exists>ya. null_filter (cap_of (TCB (f y))) b = Some ya) proof (prove)
goal (1 subgoal):
 1. \<And>s y b. \<lbrakk>\<forall>a b. is_original_cap s (a, b) \<longrightarrow> cte_wp_at (\<lambda>x. x \<noteq> NullCap) (a, b) s; get_tcb p s = Some y; is_original_cap s (p, b)\<rbrakk> \<Longrightarrow> \<exists>ya. null_filter (cap_of (TCB (f y))) b = Some ya proof (prove)
goal (1 subgoal):
 1. \<And>s y b. \<lbrakk>get_tcb p s = Some y; is_original_cap s (p, b); cte_wp_at (\<lambda>x. x \<noteq> NullCap) (p, b) s\<rbrakk> \<Longrightarrow> \<exists>ya. null_filter (cap_of (TCB (f y))) b = Some ya proof (prove)
goal (1 subgoal):
 1. \<And>s y b. \<lbrakk>get_tcb p s = Some y; is_original_cap s (p, b); cte_wp_at (\<lambda>x. x \<noteq> NullCap) (p, b) s; \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (f y) = getF y\<rbrakk> \<Longrightarrow> \<exists>ya. null_filter (cap_of (TCB (f y))) b = Some ya proof (prove)
goal (1 subgoal):
 1. \<And>s y b get set restr. \<lbrakk>is_original_cap s (p, b); \<forall>x\<in>ran tcb_cap_cases. fst x (f y) = fst x y; kheap s p = Some (TCB y); get y \<noteq> NullCap; tcb_cap_cases b = Some (get, set, restr); get (f y) = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s y b get set restr. \<lbrakk>is_original_cap s (p, b); kheap s p = Some (TCB y); get y \<noteq> NullCap; tcb_cap_cases b = Some (get, set, restr); get (f y) = NullCap\<rbrakk> \<Longrightarrow> (get, set, restr) \<in> ran tcb_cap_cases
 2. \<And>s y b get set restr. \<lbrakk>is_original_cap s (p, b); kheap s p = Some (TCB y); get y \<noteq> NullCap; tcb_cap_cases b = Some (get, set, restr); get (f y) = NullCap; fst (get, set, restr) (f y) = fst (get, set, restr) y\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!