theory Scheduler_IF

lemma dmo_distr:
  "do_machine_op (f >>= g) = (do_machine_op f >>= (\<lambda>x. do_machine_op (g x)))" apply (clarsimp simp: do_machine_op_def bind_assoc) apply (clarsimp simp: gets_def simpler_modify_def select_f_def
                  bind_def get_def return_def) apply (rule ext) apply safe apply ((clarsimp, force)+)[5] apply (simp add: image_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do_machine_op (f >>= g) = do x <- do_machine_op f;
do_machine_op (g x)
od proof (prove)
goal (1 subgoal):
 1. do ms <- gets machine_state;
(r, ms') <- select_f ((f >>= g) ms);
y <- modify (machine_state_update (\<lambda>_. ms'));
return r
od = do x <- gets machine_state;
x <- select_f (f x);
x <- case x of (r, ms') \<Rightarrow> do y <- modify (machine_state_update (\<lambda>_. ms'));
return r
od;
ms <- gets machine_state;
(r, ms') <- select_f (g x ms);
y <- modify (machine_state_update (\<lambda>_. ms'));
return r
od proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. (\<Union>a\<in>(\<Union>a\<in>fst (f (machine_state s)). fst (case a of (x, xa) \<Rightarrow> g x xa)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) xa), (\<exists>y\<in>fst (f (machine_state s)). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> g x xa). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)) \<or> (\<exists>x\<in>fst (f (machine_state s)). snd (case x of (x, xa) \<Rightarrow> g x xa)) \<or> snd (f (machine_state s)))) = (\<lambda>s. (\<Union>a\<in>fst (f (machine_state s)) \<times> {s}. fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (g x (machine_state s)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) xa), (\<exists>x\<in>fst (g x (machine_state s)). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)) \<or> snd (g x (machine_state s)))), (\<exists>x\<in>fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (g x (machine_state s)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) xa), (\<exists>x\<in>fst (g x (machine_state s)). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)) \<or> snd (g x (machine_state s))))) \<or> snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s))), (\<exists>x\<in>fst (f (machine_state s)). (\<exists>x\<in>fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (g x (machine_state s)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) xa), (\<exists>x\<in>fst (g x (machine_state s)). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)) \<or> snd (g x (machine_state s))))) \<or> snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)) \<or> snd (f (machine_state s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<Union>a\<in>(\<Union>a\<in>fst (f (machine_state s)). fst (case a of (x, xa) \<Rightarrow> g x xa)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) xa), (\<exists>y\<in>fst (f (machine_state s)). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> g x xa). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)) \<or> (\<exists>x\<in>fst (f (machine_state s)). snd (case x of (x, xa) \<Rightarrow> g x xa)) \<or> snd (f (machine_state s))) = (\<Union>a\<in>fst (f (machine_state s)) \<times> {s}. fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (g x (machine_state s)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) xa), (\<exists>x\<in>fst (g x (machine_state s)). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)) \<or> snd (g x (machine_state s)))), (\<exists>x\<in>fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (g x (machine_state s)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) xa), (\<exists>x\<in>fst (g x (machine_state s)). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)) \<or> snd (g x (machine_state s))))) \<or> snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s))), (\<exists>x\<in>fst (f (machine_state s)). (\<exists>x\<in>fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (g x (machine_state s)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) xa), (\<exists>x\<in>fst (g x (machine_state s)). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)) \<or> snd (g x (machine_state s))))) \<or> snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)) \<or> snd (f (machine_state s))) proof (prove)
goal (6 subgoals):
 1. \<And>s a b aa ba bb ab bc. \<lbrakk>(a, b) \<in> fst ({(aa, s\<lparr>machine_state := ba\<rparr>)}, False); (ab, bc) \<in> fst (f (machine_state s)); (aa, ba) \<in> fst (g ab bc)\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<Union>a\<in>fst (f (machine_state s)) \<times> {s}. fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (g x (machine_state s)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) xa), (\<exists>x\<in>fst (g x (machine_state s)). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)) \<or> snd (g x (machine_state s)))), (\<exists>x\<in>fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (g x (machine_state s)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) xa), (\<exists>x\<in>fst (g x (machine_state s)). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)) \<or> snd (g x (machine_state s))))) \<or> snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s))))
 2. \<And>s a b aa ba bb. \<lbrakk>(a, b) \<in> fst (\<Union>a\<in>fst ({(aa, s\<lparr>machine_state := ba\<rparr>)}, False). fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>fst (g x (machine_state s)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) xa), (\<exists>x\<in>fst (g x (machine_state s)). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)) \<or> snd (g x (machine_state s)))), (\<exists>x\<in>fst ({(aa, s\<lparr>machine_state := ba\<rparr>)}, False). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (g x (machine_state s)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) xa), (\<exists>x\<in>fst (g x (machine_state s)). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)) \<or> snd (g x (machine_state s))))) \<or> snd ({(aa, s\<lparr>machine_state := ba\<rparr>)}, False)); (aa, ba) \<in> fst (f (machine_state s))\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<Union>a\<in>(\<Union>a\<in>fst (f (machine_state s)). fst (case a of (x, xa) \<Rightarrow> g x xa)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) xa))
 3. \<And>s a b aa ba. \<lbrakk>\<not> snd (f (machine_state s)); (a, b) \<in> fst (f (machine_state s)); (aa, ba) \<in> fst (g a b); snd ({(aa, s\<lparr>machine_state := ba\<rparr>)}, False)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f (machine_state s)). (\<exists>x\<in>fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (g x (machine_state s)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) xa), (\<exists>x\<in>fst (g x (machine_state s)). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)) \<or> snd (g x (machine_state s))))) \<or> snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)
 4. \<And>s a b. \<lbrakk>\<not> snd (f (machine_state s)); (a, b) \<in> fst (f (machine_state s)); snd (g a b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f (machine_state s)). (\<exists>x\<in>fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s). snd (case x of (x, s) \<Rightarrow> (\<Union>a\<in>fst (g x (machine_state s)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) xa), (\<exists>x\<in>fst (g x (machine_state s)). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)) \<or> snd (g x (machine_state s))))) \<or> snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)
 5. \<And>s a b aa ba. \<lbrakk>\<not> (\<exists>y\<in>fst (f (machine_state s)). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> g x xa). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)); \<not> snd (f (machine_state s)); (a, b) \<in> fst (f (machine_state s)); (aa, ba) \<in> fst ({(a, s\<lparr>machine_state := b\<rparr>)}, False); snd (\<Union>a\<in>fst (g aa (machine_state ba)) \<times> {ba}. fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) xa), (\<exists>x\<in>fst (g aa (machine_state ba)). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) ba)) \<or> snd (g aa (machine_state ba)))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f (machine_state s)). snd (case x of (x, xa) \<Rightarrow> g x xa)
 6. \<And>s a b. \<lbrakk>\<not> (\<exists>y\<in>fst (f (machine_state s)). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> g x xa). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)); \<not> snd (f (machine_state s)); (a, b) \<in> fst (f (machine_state s)); snd ({(a, s\<lparr>machine_state := b\<rparr>)}, False)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f (machine_state s)). snd (case x of (x, xa) \<Rightarrow> g x xa) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<not> (\<exists>y\<in>fst (f (machine_state s)). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> g x xa). snd ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state := ms'\<rparr>)}, False)) s)); \<not> snd (f (machine_state s)); (a, b) \<in> fst (f (machine_state s)); snd ({(a, s\<lparr>machine_state := b\<rparr>)}, False)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f (machine_state s)). snd (case x of (x, xa) \<Rightarrow> g x xa) proof (prove)
goal:
No subgoals!