theory KHeap_DR

lemma set_irq_state_dcorres:
  "dcorres dc \<top> \<top> (return ()) (set_irq_state irq st)" apply (simp add: set_irq_state_def) apply (rule corres_dummy_return_pl [where b="()"]) apply (rule corres_underlying_split [where r'=dc]) apply (clarsimp simp: corres_underlying_def in_monad return_def) apply (clarsimp simp: transform_def transform_current_thread_def
                           transform_objects_def transform_cdt_def
                           transform_asid_table_def) apply simp apply (rule dmo_maskIRQ_dcorres) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (set_irq_state irq st) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (do y <- modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(st := irq)\<rparr>);
do_machine_op (maskInterrupt (irq = IRQInactive) st)
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (do return ();
return ()
od) (do y <- modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(st := irq)\<rparr>);
do_machine_op (maskInterrupt (irq = IRQInactive) st)
od) proof (prove)
goal (4 subgoals):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(st := irq)\<rparr>))
 2. \<And>rv y. dc rv y \<Longrightarrow> dcorres dc (?Q2 rv) (?Q'2 y) (K_bind (return ()) rv) (do_machine_op (maskInterrupt (irq = IRQInactive) st))
 3. \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>?Q2\<rbrace>
 4. \<lbrace>\<lambda>_. True\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(st := irq)\<rparr>) \<lbrace>?Q'2\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>b. transform (b\<lparr>interrupt_states := (interrupt_states b)(st := irq)\<rparr>) = transform b
 2. \<And>rv y. dc rv y \<Longrightarrow> dcorres dc (?Q2 rv) (?Q'2 y) (K_bind (return ()) rv) (do_machine_op (maskInterrupt (irq = IRQInactive) st))
 3. \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>?Q2\<rbrace>
 4. \<lbrace>\<lambda>_. True\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(st := irq)\<rparr>) \<lbrace>?Q'2\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv y. dc rv y \<Longrightarrow> dcorres dc (?Q2 rv) (?Q'2 y) (K_bind (return ()) rv) (do_machine_op (maskInterrupt (irq = IRQInactive) st))
 2. \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>?Q2\<rbrace>
 3. \<lbrace>\<lambda>_. True\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(st := irq)\<rparr>) \<lbrace>?Q'2\<rbrace> proof (prove)
goal (3 subgoals):
 1. dcorres dc (?Q2 ()) (?Q'2 ()) (return ()) (do_machine_op (maskInterrupt (irq = IRQInactive) st))
 2. \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>?Q2\<rbrace>
 3. \<lbrace>\<lambda>_. True\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(st := irq)\<rparr>) \<lbrace>?Q'2\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>_. True\<rbrace> return () \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<lbrace>\<lambda>_. True\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(st := irq)\<rparr>) \<lbrace>\<lambda>a b. True\<rbrace> proof (prove)
goal:
No subgoals!