theory Interrupt_DR

lemma handle_interrupt_corres_branch:
  "dcorres dc \<top> \<top> (return ())
             (do y \<leftarrow> do_machine_op (maskInterrupt True x);
                 do_machine_op (ackInterrupt x)
              od)" apply (rule corres_dummy_return_pl) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule dcorres_machine_op_noop) apply wp apply (clarsimp simp:dc_def[symmetric]) apply (rule dcorres_machine_op_noop) apply (wp|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (do return ?b;
return ()
od) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q2 ?Q'2 (do return ?b;
return ()
od) (do y <- do_machine_op (maskInterrupt True x);
do_machine_op (ackInterrupt x)
od)
 2. \<And>s. True \<Longrightarrow> ?Q2 s
 3. \<And>s. True \<Longrightarrow> ?Q'2 s proof (prove)
goal (6 subgoals):
 1. dcorres ?r'6 ?P6 ?P'6 (return ?b) (do_machine_op (maskInterrupt True x))
 2. \<And>rv y. ?r'6 rv y \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 y) (K_bind (return ()) rv) (do_machine_op (ackInterrupt x))
 3. \<lbrace>?Q6\<rbrace> return ?b \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> do_machine_op (maskInterrupt True x) \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> (?P6 and ?Q6) s
 6. \<And>s. True \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> maskInterrupt True x \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
 2. \<And>rv y. dc rv y \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 y) (K_bind (return ()) rv) (do_machine_op (ackInterrupt x))
 3. \<lbrace>?Q6\<rbrace> return () \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> do_machine_op (maskInterrupt True x) \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>rv y. dc rv y \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 y) (K_bind (return ()) rv) (do_machine_op (ackInterrupt x))
 2. \<lbrace>?Q6\<rbrace> return () \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> do_machine_op (maskInterrupt True x) \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. dcorres dc (?R6 ()) (?R'6 ()) (return ()) (do_machine_op (ackInterrupt x))
 2. \<lbrace>?Q6\<rbrace> return () \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> do_machine_op (maskInterrupt True x) \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> ackInterrupt x \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
 2. \<lbrace>?Q6\<rbrace> return () \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> do_machine_op (maskInterrupt True x) \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal:
No subgoals!