theory Refine_C

lemma device_update_corres_C:
  "corres_underlying rf_sr False nf (=) (\<lambda>_. True) (\<lambda>_. True)
   (doMachineOp (device_memory_update ms))
   (setDeviceState_C ms)" apply (clarsimp simp: corres_underlying_def) apply (rule conjI) prefer 2 apply (clarsimp simp add: setDeviceState_C_def simpler_modify_def) apply (rule ballI) apply (clarsimp simp: simpler_modify_def setDeviceState_C_def) apply (clarsimp simp: doMachineOp_def device_memory_update_def Nondet_Monad.bind_def in_monad
                        gets_def get_def return_def simpler_modify_def select_f_def) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
                        cmachine_state_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False nf (=) (\<lambda>_. True) (\<lambda>_. True) (doMachineOp (device_memory_update ms)) (setDeviceState_C ms) proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> rf_sr \<Longrightarrow> (\<forall>x\<in>fst (setDeviceState_C ms b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doMachineOp (device_memory_update ms) a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr) \<and> (nf \<longrightarrow> \<not> snd (setDeviceState_C ms b)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> rf_sr \<Longrightarrow> \<forall>x\<in>fst (setDeviceState_C ms b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doMachineOp (device_memory_update ms) a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr
 2. \<And>a b. (a, b) \<in> rf_sr \<Longrightarrow> nf \<longrightarrow> \<not> snd (setDeviceState_C ms b) proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> rf_sr \<Longrightarrow> nf \<longrightarrow> \<not> snd (setDeviceState_C ms b)
 2. \<And>a b. (a, b) \<in> rf_sr \<Longrightarrow> \<forall>x\<in>fst (setDeviceState_C ms b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doMachineOp (device_memory_update ms) a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> rf_sr \<Longrightarrow> \<forall>x\<in>fst (setDeviceState_C ms b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doMachineOp (device_memory_update ms) a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>(a, b) \<in> rf_sr; x \<in> fst (setDeviceState_C ms b)\<rbrakk> \<Longrightarrow> case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (doMachineOp (device_memory_update ms) a). case x of (r, t) \<Rightarrow> (t, t') \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> rf_sr \<Longrightarrow> \<exists>x\<in>fst (doMachineOp (device_memory_update ms) a). case x of (r, t) \<Rightarrow> (t, b\<lparr>globals := globals b\<lparr>phantom_machine_state_' := phantom_machine_state_' (globals b)\<lparr>device_state := device_state (phantom_machine_state_' (globals b)) ++ ms\<rparr>\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> rf_sr \<Longrightarrow> (a\<lparr>ksMachineState := ksMachineState a\<lparr>device_state := device_state (ksMachineState a) ++ ms\<rparr>\<rparr>, b\<lparr>globals := globals b\<lparr>phantom_machine_state_' := phantom_machine_state_' (globals b)\<lparr>device_state := device_state (phantom_machine_state_' (globals b)) ++ ms\<rparr>\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal:
No subgoals!