theory Detype_R

lemma doMachineOp_ksArchState_commute:
  "monad_commute \<top> (doMachineOp f) (gets (g \<circ> ksArchState))" apply (clarsimp simp:monad_commute_def gets_def return_def get_def bind_def) apply (intro conjI set_eqI iffI) apply (clarsimp simp: doMachineOp_def select_f_def gets_def get_def bind_def
                           return_def simpler_modify_def) apply (erule bexI[rotated]) apply clarsimp apply (clarsimp simp: doMachineOp_def select_f_def gets_def get_def bind_def return_def
                          simpler_modify_def) apply (erule bexI[rotated]) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) (doMachineOp f) (gets (g \<circ> ksArchState)) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<Union>a\<in>fst (doMachineOp f s). fst (case a of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False))) = (\<Union>a\<in>fst (doMachineOp f s). fst (case a of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<and> ((\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False))) \<or> snd (doMachineOp f s)) = ((\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<or> snd (doMachineOp f s)) proof (prove)
goal (4 subgoals):
 1. \<And>s x. x \<in> (\<Union>a\<in>fst (doMachineOp f s). fst (case a of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False))) \<Longrightarrow> x \<in> (\<Union>a\<in>fst (doMachineOp f s). fst (case a of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False)))
 2. \<And>s x. x \<in> (\<Union>a\<in>fst (doMachineOp f s). fst (case a of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<Longrightarrow> x \<in> (\<Union>a\<in>fst (doMachineOp f s). fst (case a of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False)))
 3. \<And>s. (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False))) \<or> snd (doMachineOp f s) \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<or> snd (doMachineOp f s)
 4. \<And>s. (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<or> snd (doMachineOp f s) \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False))) \<or> snd (doMachineOp f s) proof (prove)
goal (4 subgoals):
 1. \<And>s a bb. (a, bb) \<in> fst (f (ksMachineState s)) \<Longrightarrow> \<exists>x\<in>fst (f (ksMachineState s)). \<exists>x\<in>fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>ksMachineState := ms'\<rparr>)}, False)) s). ((a, g (ksArchState s)), s\<lparr>ksMachineState := bb\<rparr>) \<in> fst (case x of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))
 2. \<And>s x. x \<in> (\<Union>a\<in>fst (doMachineOp f s). fst (case a of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<Longrightarrow> x \<in> (\<Union>a\<in>fst (doMachineOp f s). fst (case a of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False)))
 3. \<And>s. (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False))) \<or> snd (doMachineOp f s) \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<or> snd (doMachineOp f s)
 4. \<And>s. (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<or> snd (doMachineOp f s) \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False))) \<or> snd (doMachineOp f s) proof (prove)
goal (4 subgoals):
 1. \<And>s a bb. \<exists>x\<in>fst ((case (a, bb) of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>ksMachineState := ms'\<rparr>)}, False)) s). ((a, g (ksArchState s)), s\<lparr>ksMachineState := bb\<rparr>) \<in> fst (case x of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))
 2. \<And>s x. x \<in> (\<Union>a\<in>fst (doMachineOp f s). fst (case a of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<Longrightarrow> x \<in> (\<Union>a\<in>fst (doMachineOp f s). fst (case a of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False)))
 3. \<And>s. (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False))) \<or> snd (doMachineOp f s) \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<or> snd (doMachineOp f s)
 4. \<And>s. (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<or> snd (doMachineOp f s) \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False))) \<or> snd (doMachineOp f s) proof (prove)
goal (3 subgoals):
 1. \<And>s x. x \<in> (\<Union>a\<in>fst (doMachineOp f s). fst (case a of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<Longrightarrow> x \<in> (\<Union>a\<in>fst (doMachineOp f s). fst (case a of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False)))
 2. \<And>s. (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False))) \<or> snd (doMachineOp f s) \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<or> snd (doMachineOp f s)
 3. \<And>s. (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<or> snd (doMachineOp f s) \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False))) \<or> snd (doMachineOp f s) proof (prove)
goal (3 subgoals):
 1. \<And>s a bb. (a, bb) \<in> fst (f (ksMachineState s)) \<Longrightarrow> \<exists>x\<in>fst (f (ksMachineState s)). \<exists>x\<in>fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>ksMachineState := ms'\<rparr>)}, False)) s). ((a, g (ksArchState s)), s\<lparr>ksMachineState := bb\<rparr>) \<in> fst (case x of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False))
 2. \<And>s. (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False))) \<or> snd (doMachineOp f s) \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<or> snd (doMachineOp f s)
 3. \<And>s. (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<or> snd (doMachineOp f s) \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False))) \<or> snd (doMachineOp f s) proof (prove)
goal (3 subgoals):
 1. \<And>s a bb. \<exists>x\<in>fst ((case (a, bb) of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>ksMachineState := ms'\<rparr>)}, False)) s). ((a, g (ksArchState s)), s\<lparr>ksMachineState := bb\<rparr>) \<in> fst (case x of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False))
 2. \<And>s. (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False))) \<or> snd (doMachineOp f s) \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<or> snd (doMachineOp f s)
 3. \<And>s. (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, sa) \<Rightarrow> ({((x, g (ksArchState s)), sa)}, False))) \<or> snd (doMachineOp f s) \<Longrightarrow> (\<exists>x\<in>fst (doMachineOp f s). snd (case x of (x, s) \<Rightarrow> ({((x, g (ksArchState s)), s)}, False))) \<or> snd (doMachineOp f s) proof (prove)
goal:
No subgoals!