kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_AI

lemma thread_set_iflive_trivial:
  assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
                  getF (f tcb) = getF tcb"
  assumes z: "\<And>tcb. tcb_state  (f tcb) = tcb_state  tcb"
  assumes y: "\<And>tcb. tcb_bound_notification (f tcb) = tcb_bound_notification tcb"
  assumes a: "\<And>tcb. tcb_arch_ref (f tcb) = tcb_arch_ref tcb"
  shows      "\<lbrace>if_live_then_nonz_cap\<rbrace> thread_set f t \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>" apply (simp add: thread_set_def) apply (wp set_object_iflive) apply (clarsimp dest!: get_tcb_SomeD) apply (clarsimp simp: obj_at_def get_tcb_def
                        split_paired_Ball
                        bspec_split [OF x]) apply (subgoal_tac "live (TCB y)") apply (fastforce elim: if_live_then_nonz_capD2) apply (clarsimp simp: live_def hyp_live_tcb_def z y a) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap\<rbrace> thread_set f t \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (f tcb))
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. if_live_then_nonz_cap s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> if_live_then_nonz_cap s \<and> (live (TCB (f (the (get_tcb t s)))) \<longrightarrow> ex_nonz_cap_to t s) \<and> obj_at (same_caps (TCB (f (the (get_tcb t s))))) t s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>if_live_then_nonz_cap s; kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> (live (TCB (f (the (get_tcb t s)))) \<longrightarrow> ex_nonz_cap_to t s) \<and> obj_at (same_caps (TCB (f (the (get_tcb t s))))) t s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>if_live_then_nonz_cap s; kheap s t = Some (TCB y); live (TCB (f y))\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>if_live_then_nonz_cap s; kheap s t = Some (TCB y); live (TCB (f y)); live (TCB y)\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s
 2. \<And>s y. \<lbrakk>if_live_then_nonz_cap s; kheap s t = Some (TCB y); live (TCB (f y))\<rbrakk> \<Longrightarrow> live (TCB y) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>if_live_then_nonz_cap s; kheap s t = Some (TCB y); live (TCB (f y))\<rbrakk> \<Longrightarrow> live (TCB y) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_ifunsafe_trivial:
  assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
                  getF (f tcb) = getF tcb"
  shows      "\<lbrace>if_unsafe_then_cap\<rbrace> thread_set f t \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>" apply (simp add: thread_set_def) apply (wp set_object_ifunsafe) apply (clarsimp simp: x) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> thread_set f t \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (f tcb))
od \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. if_unsafe_then_cap s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (if_unsafe_then_cap and obj_at (same_caps (TCB (f (the (get_tcb t s))))) t) s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_zombies_trivial:
  assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
                  getF (f tcb) = getF tcb"
  shows      "\<lbrace>zombies_final\<rbrace> thread_set f t \<lbrace>\<lambda>rv. zombies_final\<rbrace>" apply (simp add: thread_set_def) apply wp apply (clarsimp simp: x) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> thread_set f t \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (f tcb))
od \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. zombies_final s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (zombies_final and obj_at (same_caps (TCB (f (the (get_tcb t s))))) t) s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_refs_trivial:
  assumes x: "\<And>tcb. tcb_state  (f tcb) = tcb_state  tcb"
  assumes y: "\<And>tcb. tcb_bound_notification (f tcb) = tcb_bound_notification tcb"
  shows      "\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>" apply (simp add: thread_set_def set_object_def get_object_def) apply wp apply (clarsimp dest!: get_tcb_SomeD) apply (clarsimp simp: state_refs_of_def get_tcb_def x y
                 elim!: rsubst[where P=P]
                intro!: ext) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> do tcb <- gets_the (get_tcb t);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t = Some y);
return (the (kh t))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (state_refs_of s) \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> P (state_refs_of (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f (the (get_tcb t s))))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>P (state_refs_of s); kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> P (state_refs_of (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (f (the (get_tcb t s)))) else kheap s a\<rparr>)) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_valid_idle_trivial:
  assumes "\<And>tcb. tcb_state (f tcb) = tcb_state tcb"
  assumes "\<And>tcb. tcb_bound_notification (f tcb) = tcb_bound_notification tcb"
  assumes "\<And>tcb. tcb_iarch (f tcb) = tcb_iarch tcb"
  shows      "\<lbrace>valid_idle\<rbrace> thread_set f t \<lbrace>\<lambda>_. valid_idle\<rbrace>" apply (simp add: thread_set_def set_object_def get_object_def valid_idle_def) apply wp apply (clarsimp simp: assms get_tcb_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> thread_set f t \<lbrace>\<lambda>_. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) (idle_thread s) s \<and> idle_thread s = idle_thread_ptr\<rbrace> do tcb <- gets_the (get_tcb t);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t = Some y);
return (the (kh t))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>_ s. idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) (idle_thread s) s \<and> idle_thread s = idle_thread_ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) (idle_thread s) s \<and> idle_thread s = idle_thread_ptr \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) (idle_thread (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f (the (get_tcb t s))))\<rparr>)) (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f (the (get_tcb t s))))\<rparr>) \<and> idle_thread (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f (the (get_tcb t s))))\<rparr>) = idle_thread_ptr proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_caps_of_state_trivial:
  assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
                  getF (f tcb) = getF tcb"
  shows      "\<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>" apply (simp add: thread_set_def set_object_def get_object_def) apply wp apply (clarsimp elim!: rsubst[where P=P]
                 intro!: ext
                  dest!: get_tcb_SomeD) apply (subst caps_of_state_after_update) apply (clarsimp simp: obj_at_def get_tcb_def bspec_split [OF x]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do tcb <- gets_the (get_tcb t);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t = Some y);
return (the (kh t))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (caps_of_state s) \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f (the (get_tcb t s))))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b tcb. kheap s t = Some (TCB tcb) \<Longrightarrow> caps_of_state s (a, b) = caps_of_state (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (f (the (get_tcb t s)))) else kheap s a\<rparr>) (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b tcb. kheap s t = Some (TCB tcb) \<Longrightarrow> obj_at (same_caps (TCB (f (the (get_tcb t s))))) t s
 2. \<And>s a b tcb. kheap s t = Some (TCB tcb) \<Longrightarrow> caps_of_state s (a, b) = caps_of_state s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b tcb. kheap s t = Some (TCB tcb) \<Longrightarrow> caps_of_state s (a, b) = caps_of_state s (a, b) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_global_refs_triv:
  assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
                  getF (f tcb) = getF tcb"
  shows "\<lbrace>valid_global_refs\<rbrace> thread_set f t \<lbrace>\<lambda>_. valid_global_refs\<rbrace>" apply (rule valid_global_refs_cte_lift) apply (wp thread_set_caps_of_state_trivial x)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs\<rbrace> thread_set f t \<lbrace>\<lambda>_. valid_global_refs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (interrupt_irq_node s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (interrupt_irq_node s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_valid_reply_caps_trivial:
  assumes x: "\<And>tcb. tcb_state     (f tcb) = tcb_state      tcb"
  assumes z: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
                  getF (f tcb) = getF tcb"
  shows "\<lbrace>valid_reply_caps\<rbrace> thread_set f t \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>" by (wp valid_reply_caps_st_cte_lift  thread_set_caps_of_state_trivial
         thread_set_no_change_tcb_state x z)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps\<rbrace> thread_set f t \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>
theory TcbAcc_AI

lemma thread_set_valid_reply_masters_trivial:
  assumes y: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
                  getF (f tcb) = getF tcb"
  shows "\<lbrace>valid_reply_masters\<rbrace> thread_set f t \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>" by (wp valid_reply_masters_cte_lift thread_set_caps_of_state_trivial y)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters\<rbrace> thread_set f t \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>
theory TcbAcc_AI

lemma thread_set_obj_at_impossible:
  "\<lbrakk> \<And>tcb. \<not> (P (TCB tcb)) \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. obj_at P p s\<rbrace> thread_set f t \<lbrace>\<lambda>rv. obj_at P p\<rbrace>" apply (simp add: thread_set_def set_object_def get_object_def) apply wp apply (clarsimp dest!: get_tcb_SomeD) apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. \<not> P (TCB tcb)) \<Longrightarrow> \<lbrace>obj_at P p\<rbrace> thread_set f t \<lbrace>\<lambda>rv. obj_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. \<not> P (TCB tcb)) \<Longrightarrow> \<lbrace>obj_at P p\<rbrace> do tcb <- gets_the (get_tcb t);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t = Some y);
return (the (kh t))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>rv. obj_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>tcb. \<not> P (TCB tcb); obj_at P p s\<rbrakk> \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> obj_at P p (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f (the (get_tcb t s))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>\<And>tcb. \<not> P (TCB tcb); obj_at P p s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> obj_at P p (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (f (the (get_tcb t s)))) else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma tcb_not_empty_table:
  "\<not> empty_table S (TCB tcb)" by (simp add: empty_table_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> empty_table S (TCB tcb)
theory TcbAcc_AI

lemma thread_set_only_idle:
  "\<lbrace>only_idle and K (\<forall>tcb. tcb_state (f tcb) = tcb_state tcb \<or> \<not>idle (tcb_state (f tcb)))\<rbrace>
  thread_set f t \<lbrace>\<lambda>_. only_idle\<rbrace>" apply (simp add: thread_set_def set_object_def get_object_def) apply wp apply (clarsimp simp: only_idle_def pred_tcb_at_def obj_at_def) apply (drule get_tcb_SomeD) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_idle and K (\<forall>tcb. tcb_state (f tcb) = tcb_state tcb \<or> tcb_state (f tcb) \<noteq> IdleThreadState)\<rbrace> thread_set f t \<lbrace>\<lambda>_. only_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_idle and (\<lambda>y. \<forall>tcb. tcb_state (f tcb) = tcb_state tcb \<or> tcb_state (f tcb) \<noteq> IdleThreadState)\<rbrace> do tcb <- gets_the (get_tcb t);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t = Some y);
return (the (kh t))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>_. only_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (only_idle and (\<lambda>y. \<forall>tcb. tcb_state (f tcb) = tcb_state tcb \<or> tcb_state (f tcb) \<noteq> IdleThreadState)) s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> only_idle (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f (the (get_tcb t s))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>\<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread s; \<forall>tcb. tcb_state (f tcb) = tcb_state tcb \<or> tcb_state (f tcb) \<noteq> IdleThreadState; get_tcb t s = Some y; kheap s t = Some (TCB tcb); idle (tcb_state (f y))\<rbrakk> \<Longrightarrow> t = idle_thread s proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>\<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread s; \<forall>tcb. tcb_state (f tcb) = tcb_state tcb \<or> tcb_state (f tcb) \<noteq> IdleThreadState; kheap s t = Some (TCB tcb); idle (tcb_state (f y)); kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> t = idle_thread s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_pspace_in_kernel_window[wp]:
  "\<lbrace>pspace_in_kernel_window\<rbrace> thread_set f t \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>" apply (simp add: thread_set_def) apply (wp set_object_pspace_in_kernel_window) apply (clarsimp simp: obj_at_def dest!: get_tcb_SomeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> thread_set f t \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (f tcb))
od \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_in_kernel_window s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> pspace_in_kernel_window s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_cap_refs_in_kernel_window:
  assumes y: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
                  getF (f tcb) = getF tcb"
  shows
  "\<lbrace>cap_refs_in_kernel_window\<rbrace> thread_set f t \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" apply (simp add: thread_set_def) apply (wp set_object_cap_refs_in_kernel_window) apply (clarsimp simp: obj_at_def) apply (clarsimp dest!: get_tcb_SomeD) apply (drule bspec[OF y]) apply simp apply (erule sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window\<rbrace> thread_set f t \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (f tcb))
od \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cap_refs_in_kernel_window s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (cap_refs_in_kernel_window and obj_at (same_caps (TCB (f (the (get_tcb t s))))) t) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>cap_refs_in_kernel_window s; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb'. ko = TCB tcb' \<and> (\<forall>x\<in>ran tcb_cap_cases. case x of (getF, t) \<Rightarrow> getF tcb' = getF (f y))) proof (prove)
goal (1 subgoal):
 1. \<And>s y a aa b. \<lbrakk>cap_refs_in_kernel_window s; kheap s t = Some (TCB y); (a, aa, b) \<in> ran tcb_cap_cases\<rbrakk> \<Longrightarrow> a y = a (f y) proof (prove)
goal (1 subgoal):
 1. \<And>s y a aa b. \<lbrakk>cap_refs_in_kernel_window s; kheap s t = Some (TCB y); case (a, aa, b) of (getF, v) \<Rightarrow> getF (f (?tcb10 s y a aa b)) = getF (?tcb10 s y a aa b)\<rbrakk> \<Longrightarrow> a y = a (f y) proof (prove)
goal (1 subgoal):
 1. \<And>s y a aa b. \<lbrakk>cap_refs_in_kernel_window s; kheap s t = Some (TCB y); a (f (?tcb10 s y a aa b)) = a (?tcb10 s y a aa b)\<rbrakk> \<Longrightarrow> a y = a (f y) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_cap_refs_respects_device_region:
  assumes y: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
                  getF (f tcb) = getF tcb"
  shows
  "\<lbrace>cap_refs_respects_device_region\<rbrace> thread_set f t \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" apply (simp add: thread_set_def) apply (wp set_object_cap_refs_respects_device_region) apply (clarsimp simp: obj_at_def) apply (clarsimp dest!: get_tcb_SomeD) apply (drule bspec[OF y]) apply simp apply (erule sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region\<rbrace> thread_set f t \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (f tcb))
od \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cap_refs_respects_device_region s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (cap_refs_respects_device_region and obj_at (same_caps (TCB (f (the (get_tcb t s))))) t) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>cap_refs_respects_device_region s; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb'. ko = TCB tcb' \<and> (\<forall>x\<in>ran tcb_cap_cases. case x of (getF, t) \<Rightarrow> getF tcb' = getF (f y))) proof (prove)
goal (1 subgoal):
 1. \<And>s y a aa b. \<lbrakk>cap_refs_respects_device_region s; kheap s t = Some (TCB y); (a, aa, b) \<in> ran tcb_cap_cases\<rbrakk> \<Longrightarrow> a y = a (f y) proof (prove)
goal (1 subgoal):
 1. \<And>s y a aa b. \<lbrakk>cap_refs_respects_device_region s; kheap s t = Some (TCB y); case (a, aa, b) of (getF, v) \<Rightarrow> getF (f (?tcb10 s y a aa b)) = getF (?tcb10 s y a aa b)\<rbrakk> \<Longrightarrow> a y = a (f y) proof (prove)
goal (1 subgoal):
 1. \<And>s y a aa b. \<lbrakk>cap_refs_respects_device_region s; kheap s t = Some (TCB y); a (f (?tcb10 s y a aa b)) = a (?tcb10 s y a aa b)\<rbrakk> \<Longrightarrow> a y = a (f y) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_ioports:
  assumes y: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
                  getF (f tcb) = getF tcb"
  shows
  "\<lbrace>valid_ioports\<rbrace> thread_set f t \<lbrace>\<lambda>rv. valid_ioports\<rbrace>" by (wpsimp wp: valid_ioports_lift thread_set_caps_of_state_trivial y)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioports\<rbrace> thread_set f t \<lbrace>\<lambda>rv. valid_ioports\<rbrace>
theory TcbAcc_AI

lemma thread_set_cte_wp_at_trivial:
  assumes x: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases.
                  getF (f tcb) = getF tcb"
  shows "\<lbrace>\<lambda>s. Q (cte_wp_at P p s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. Q (cte_wp_at P p s)\<rbrace>" by (auto simp: cte_wp_at_caps_of_state
          intro: thread_set_caps_of_state_trivial [OF x])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (cte_wp_at P p s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. Q (cte_wp_at P p s)\<rbrace>