theory KHeap_DR

lemma corres_dummy_set_thread_state:
  "\<not>generates_pending st \<Longrightarrow>
  dcorres dc \<top> (st_tcb_at (Not \<circ> generates_pending) thread)
          (return ()) (set_thread_state thread st)" supply option.case_cong[cong] apply (simp add:set_thread_state_def) apply (rule dcorres_absorb_gets_the) apply (rule dcorres_rhs_noop_below) apply (rule set_thread_state_ext_dcorres) apply (rule corres_free_set_object) apply (clarsimp simp: transform_def) apply (clarsimp simp:transform_current_thread_def) apply (clarsimp dest!:get_tcb_SomeD simp:st_tcb_at_def obj_at_def) apply (rule ext) apply (clarsimp simp: restrict_map_def map_add_def generates_pending_def
                        st_tcb_at_def obj_at_def
                  cong: transform_full_intent_cong
                 split: Structures_A.thread_state.split_asm
                  simp: transform_tcb_def transform_objects_def
                        infer_tcb_pending_op_def) apply (rule hoare_TrueI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> generates_pending st \<Longrightarrow> dcorres dc (\<lambda>_. True) (st_tcb_at (Not \<circ> generates_pending) thread) (return ()) (set_thread_state thread st) proof (prove)
goal (1 subgoal):
 1. \<not> generates_pending st \<Longrightarrow> dcorres dc (\<lambda>_. True) (st_tcb_at (Not \<circ> generates_pending) thread) (return ()) (set_thread_state thread st) proof (prove)
goal (1 subgoal):
 1. \<not> generates_pending st \<Longrightarrow> dcorres dc (\<lambda>_. True) (st_tcb_at (Not \<circ> generates_pending) thread) (return ()) (do tcb <- gets_the (get_tcb thread);
y <- KHeap_A.set_object thread (TCB (update_tcb_state st tcb));
set_thread_state_ext thread
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do y <- KHeap_A.set_object thread (TCB (update_tcb_state st obj'));
set_thread_state_ext thread
od) proof (prove)
goal (4 subgoals):
 1. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc (?Q2 s' obj') (?Q'2 s' obj') (return ()) (set_thread_state_ext thread)
 2. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (KHeap_A.set_object thread (TCB (update_tcb_state st obj')))
 3. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> return () \<lbrace>\<lambda>y. ?Q2 s' obj'\<rbrace>
 4. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object thread (TCB (update_tcb_state st obj')) \<lbrace>\<lambda>y. ?Q'2 s' obj'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (KHeap_A.set_object thread (TCB (update_tcb_state st obj')))
 2. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> return () \<lbrace>\<lambda>y. ?Q2 s' obj'\<rbrace>
 3. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object thread (TCB (update_tcb_state st obj')) \<lbrace>\<lambda>y. ?Q'2 s' obj'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<forall>s s'a. s = transform s'a \<and> transform s' = s \<and> s' = s'a \<longrightarrow> s = transform (update_kheap ((kheap s'a)(thread \<mapsto> TCB (update_tcb_state st obj'))) s'a)
 2. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> return () \<lbrace>\<lambda>y. ?Q2 s' obj'\<rbrace>
 3. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object thread (TCB (update_tcb_state st obj')) \<lbrace>\<lambda>y. ?Q'2 s' obj'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'\<rbrakk> \<Longrightarrow> transform_objects s' = transform_objects (update_kheap ((kheap s')(thread \<mapsto> TCB (update_tcb_state st obj'))) s') \<and> transform_current_thread s' = transform_current_thread (update_kheap ((kheap s')(thread \<mapsto> TCB (update_tcb_state st obj'))) s')
 2. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> return () \<lbrace>\<lambda>y. ?Q2 s' obj'\<rbrace>
 3. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object thread (TCB (update_tcb_state st obj')) \<lbrace>\<lambda>y. ?Q'2 s' obj'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'\<rbrakk> \<Longrightarrow> transform_objects s' = transform_objects (update_kheap ((kheap s')(thread \<mapsto> TCB (update_tcb_state st obj'))) s')
 2. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> return () \<lbrace>\<lambda>y. ?Q2 s' obj'\<rbrace>
 3. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object thread (TCB (update_tcb_state st obj')) \<lbrace>\<lambda>y. ?Q'2 s' obj'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; kheap s' thread = Some (TCB obj'); \<not> generates_pending (tcb_state obj')\<rbrakk> \<Longrightarrow> transform_objects s' = transform_objects (update_kheap ((kheap s')(thread \<mapsto> TCB (update_tcb_state st obj'))) s')
 2. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> return () \<lbrace>\<lambda>y. ?Q2 s' obj'\<rbrace>
 3. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object thread (TCB (update_tcb_state st obj')) \<lbrace>\<lambda>y. ?Q'2 s' obj'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s' obj' x. \<lbrakk>\<not> generates_pending st; kheap s' thread = Some (TCB obj'); \<not> generates_pending (tcb_state obj')\<rbrakk> \<Longrightarrow> transform_objects s' x = transform_objects (update_kheap ((kheap s')(thread \<mapsto> TCB (update_tcb_state st obj'))) s') x
 2. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> return () \<lbrace>\<lambda>y. ?Q2 s' obj'\<rbrace>
 3. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object thread (TCB (update_tcb_state st obj')) \<lbrace>\<lambda>y. ?Q'2 s' obj'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> return () \<lbrace>\<lambda>y. ?Q2 s' obj'\<rbrace>
 2. \<And>s' obj'. \<lbrakk>\<not> generates_pending st; st_tcb_at (Not \<circ> generates_pending) thread s'; get_tcb thread s' = Some obj'; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object thread (TCB (update_tcb_state st obj')) \<lbrace>\<lambda>y. ?Q'2 s' obj'\<rbrace> proof (prove)
goal:
No subgoals!