theory Intent_DR

lemma evalMonad_do_machine_op:
assumes "weak_det_spec ((=) (machine_state sa)) f"
assumes "empty_when_fail f"
shows "evalMonad (f) (machine_state sa) =
          evalMonad (do_machine_op (f)) sa" apply (clarsimp simp:evalMonad_def do_machine_op_def gets_def get_def bind_def return_def simpler_modify_def) apply (clarsimp simp:select_f_def | rule conjI)+ apply (drule not_emptyI) apply clarsimp apply (rule_tac x = "(a,b)" in bexI) apply clarsimp+ apply (rule arg_cong[where f = "(\<lambda>A. (SOME x. x\<in> A))"]) apply (rule set_eqI) apply (clarsimp simp:image_def) apply (rule iffI) apply clarsimp using assms apply (clarsimp simp:empty_when_fail_def weak_det_spec_def no_fail_def) apply (drule_tac x = "machine_state sa" in spec) apply (clarsimp simp:det_spec_def) using assms apply (clarsimp simp:empty_when_fail_def weak_det_spec_def no_fail_def) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. evalMonad f (machine_state sa) = evalMonad (do_machine_op f) sa proof (prove)
goal (1 subgoal):
 1. (fst (f (machine_state sa)) = {} \<longrightarrow> (\<forall>x\<in>fst (select_f (f (machine_state sa)) sa). fst (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) xa) = {})) \<and> (fst (f (machine_state sa)) \<noteq> {} \<longrightarrow> (\<exists>x\<in>fst (select_f (f (machine_state sa)) sa). fst (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) xa) \<noteq> {}) \<and> ((\<exists>x\<in>fst (select_f (f (machine_state sa)) sa). fst (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) xa) \<noteq> {}) \<longrightarrow> pick (fst ` fst (f (machine_state sa))) = pick (fst ` (\<Union>a\<in>fst (select_f (f (machine_state sa)) sa). fst (case a of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) xa))))) proof (prove)
goal (2 subgoals):
 1. fst (f (machine_state sa)) \<noteq> {} \<Longrightarrow> \<exists>x\<in>fst (f (machine_state sa)). fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa) \<noteq> {}
 2. fst (f (machine_state sa)) \<noteq> {} \<Longrightarrow> (\<exists>x\<in>fst (f (machine_state sa)). fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa) \<noteq> {}) \<longrightarrow> pick (fst ` fst (f (machine_state sa))) = pick (fst ` (\<Union>x\<in>fst (f (machine_state sa)) \<times> {sa}. fst (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) xa))) proof (prove)
goal (2 subgoals):
 1. \<exists>x. x \<in> fst (f (machine_state sa)) \<Longrightarrow> \<exists>x\<in>fst (f (machine_state sa)). fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa) \<noteq> {}
 2. fst (f (machine_state sa)) \<noteq> {} \<Longrightarrow> (\<exists>x\<in>fst (f (machine_state sa)). fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa) \<noteq> {}) \<longrightarrow> pick (fst ` fst (f (machine_state sa))) = pick (fst ` (\<Union>x\<in>fst (f (machine_state sa)) \<times> {sa}. fst (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) xa))) proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> fst (f (machine_state sa)) \<Longrightarrow> \<exists>x\<in>fst (f (machine_state sa)). fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa) \<noteq> {}
 2. fst (f (machine_state sa)) \<noteq> {} \<Longrightarrow> (\<exists>x\<in>fst (f (machine_state sa)). fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa) \<noteq> {}) \<longrightarrow> pick (fst ` fst (f (machine_state sa))) = pick (fst ` (\<Union>x\<in>fst (f (machine_state sa)) \<times> {sa}. fst (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) xa))) proof (prove)
goal (3 subgoals):
 1. \<And>a b. (a, b) \<in> fst (f (machine_state sa)) \<Longrightarrow> fst ((case (a, b) of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa) \<noteq> {}
 2. \<And>a b. (a, b) \<in> fst (f (machine_state sa)) \<Longrightarrow> (a, b) \<in> fst (f (machine_state sa))
 3. fst (f (machine_state sa)) \<noteq> {} \<Longrightarrow> (\<exists>x\<in>fst (f (machine_state sa)). fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa) \<noteq> {}) \<longrightarrow> pick (fst ` fst (f (machine_state sa))) = pick (fst ` (\<Union>x\<in>fst (f (machine_state sa)) \<times> {sa}. fst (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) xa))) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>fst (f (machine_state sa)) \<noteq> {}; (a, b) \<in> fst (f (machine_state sa))\<rbrakk> \<Longrightarrow> pick (fst ` fst (f (machine_state sa))) = pick (fst ` (\<Union>x\<in>fst (f (machine_state sa)) \<times> {sa}. fst (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) xa))) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>fst (f (machine_state sa)) \<noteq> {}; (a, b) \<in> fst (f (machine_state sa))\<rbrakk> \<Longrightarrow> fst ` fst (f (machine_state sa)) = fst ` (\<Union>x\<in>fst (f (machine_state sa)) \<times> {sa}. fst (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) xa)) proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>fst (f (machine_state sa)) \<noteq> {}; (a, b) \<in> fst (f (machine_state sa))\<rbrakk> \<Longrightarrow> (x \<in> fst ` fst (f (machine_state sa))) = (x \<in> fst ` (\<Union>x\<in>fst (f (machine_state sa)) \<times> {sa}. fst (case x of (x, xa) \<Rightarrow> (case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) xa))) proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>fst (f (machine_state sa)) \<noteq> {}; (a, b) \<in> fst (f (machine_state sa))\<rbrakk> \<Longrightarrow> (\<exists>xa\<in>fst (f (machine_state sa)). x = fst xa) = (\<exists>y. (\<exists>x\<in>fst (f (machine_state sa)). y = fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa)) \<and> (\<exists>xa\<in>y. x = fst xa)) proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>fst (f (machine_state sa)) \<noteq> {}; (a, b) \<in> fst (f (machine_state sa)); \<exists>xa\<in>fst (f (machine_state sa)). x = fst xa\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x\<in>fst (f (machine_state sa)). y = fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa)) \<and> (\<exists>xa\<in>y. x = fst xa)
 2. \<And>a b x. \<lbrakk>fst (f (machine_state sa)) \<noteq> {}; (a, b) \<in> fst (f (machine_state sa)); \<exists>y. (\<exists>x\<in>fst (f (machine_state sa)). y = fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa)) \<and> (\<exists>xa\<in>y. x = fst xa)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (f (machine_state sa)). x = fst xa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>fst (f (machine_state sa)) \<noteq> {}; (a, b) \<in> fst (f (machine_state sa)); (aa, ba) \<in> fst (f (machine_state sa))\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x\<in>fst (f (machine_state sa)). y = fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa)) \<and> (\<exists>x\<in>y. aa = fst x)
 2. \<And>a b x. \<lbrakk>fst (f (machine_state sa)) \<noteq> {}; (a, b) \<in> fst (f (machine_state sa)); \<exists>y. (\<exists>x\<in>fst (f (machine_state sa)). y = fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa)) \<and> (\<exists>xa\<in>y. x = fst xa)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (f (machine_state sa)). x = fst xa proof (prove)
using this:
weak_det_spec ((=) (machine_state sa)) f
empty_when_fail f

goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>fst (f (machine_state sa)) \<noteq> {}; (a, b) \<in> fst (f (machine_state sa)); (aa, ba) \<in> fst (f (machine_state sa))\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x\<in>fst (f (machine_state sa)). y = fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa)) \<and> (\<exists>x\<in>y. aa = fst x)
 2. \<And>a b x. \<lbrakk>fst (f (machine_state sa)) \<noteq> {}; (a, b) \<in> fst (f (machine_state sa)); \<exists>y. (\<exists>x\<in>fst (f (machine_state sa)). y = fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa)) \<and> (\<exists>xa\<in>y. x = fst xa)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (f (machine_state sa)). x = fst xa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>fst (f (machine_state sa)) \<noteq> {}; (a, b) \<in> fst (f (machine_state sa)); (aa, ba) \<in> fst (f (machine_state sa)); \<not> snd (f (machine_state sa)) \<longrightarrow> det_spec ((=) (machine_state sa)) f; \<forall>s. snd (f s) \<longrightarrow> fst (f s) = {}\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x\<in>fst (f (machine_state sa)). y = fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa)) \<and> (\<exists>x\<in>y. aa = fst x)
 2. \<And>a b x. \<lbrakk>fst (f (machine_state sa)) \<noteq> {}; (a, b) \<in> fst (f (machine_state sa)); \<exists>y. (\<exists>x\<in>fst (f (machine_state sa)). y = fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa)) \<and> (\<exists>xa\<in>y. x = fst xa)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (f (machine_state sa)). x = fst xa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>fst (f (machine_state sa)) \<noteq> {}; (a, b) \<in> fst (f (machine_state sa)); (aa, ba) \<in> fst (f (machine_state sa)); \<not> snd (f (machine_state sa)) \<longrightarrow> det_spec ((=) (machine_state sa)) f; snd (f (machine_state sa)) \<longrightarrow> fst (f (machine_state sa)) = {}\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x\<in>fst (f (machine_state sa)). y = fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa)) \<and> (\<exists>x\<in>y. aa = fst x)
 2. \<And>a b x. \<lbrakk>fst (f (machine_state sa)) \<noteq> {}; (a, b) \<in> fst (f (machine_state sa)); \<exists>y. (\<exists>x\<in>fst (f (machine_state sa)). y = fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa)) \<and> (\<exists>xa\<in>y. x = fst xa)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (f (machine_state sa)). x = fst xa proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>fst (f (machine_state sa)) \<noteq> {}; (a, b) \<in> fst (f (machine_state sa)); \<exists>y. (\<exists>x\<in>fst (f (machine_state sa)). y = fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa)) \<and> (\<exists>xa\<in>y. x = fst xa)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (f (machine_state sa)). x = fst xa proof (prove)
using this:
weak_det_spec ((=) (machine_state sa)) f
empty_when_fail f

goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>fst (f (machine_state sa)) \<noteq> {}; (a, b) \<in> fst (f (machine_state sa)); \<exists>y. (\<exists>x\<in>fst (f (machine_state sa)). y = fst ((case x of (r, ms') \<Rightarrow> \<lambda>s. ({(r, update_machine ms' s)}, False)) sa)) \<and> (\<exists>xa\<in>y. x = fst xa)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (f (machine_state sa)). x = fst xa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>fst (f (machine_state sa)) \<noteq> {}; (a, b) \<in> fst (f (machine_state sa)); \<not> snd (f (machine_state sa)) \<longrightarrow> det_spec ((=) (machine_state sa)) f; \<forall>s. snd (f s) \<longrightarrow> fst (f s) = {}; (aa, ba) \<in> fst (f (machine_state sa))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f (machine_state sa)). aa = fst x proof (prove)
goal:
No subgoals!