theory Intent_DR

lemma evalMonad_compose:
  "\<lbrakk>empty_when_fail a;weak_det_spec ((=) s) a;\<And>s. \<lbrace>(=) s\<rbrace> a \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk>
    \<Longrightarrow> evalMonad (a>>=b) s = (case (evalMonad a s) of Some r \<Rightarrow> evalMonad (b r) s | _ \<Rightarrow> None)" apply (clarsimp simp:evalMonad_def weak_det_spec_def) apply (clarsimp simp:no_fail_def det_spec_def empty_when_fail_def) apply (drule_tac x = s in spec)+ apply (case_tac "snd (a s)") apply (simp_all) apply (fastforce simp:bind_def valid_def) apply (clarsimp simp:valid_def) apply (drule_tac x = s in meta_spec) apply (clarsimp simp:bind_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_when_fail a; weak_det_spec ((=) s) a; \<And>s. \<lbrace>(=) s\<rbrace> a \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> evalMonad (a >>= b) s = (case evalMonad a s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (b r) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_when_fail a; no_fail ((=) s) a \<longrightarrow> det_spec ((=) s) a; \<And>s. \<lbrace>(=) s\<rbrace> a \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> (fst (b (pick (fst ` fst (a s))) s) = {} \<longrightarrow> fst ((a >>= b) s) = {}) \<and> (fst (b (pick (fst ` fst (a s))) s) \<noteq> {} \<longrightarrow> (fst (a s) = {} \<longrightarrow> fst ((a >>= b) s) = {}) \<and> (fst (a s) \<noteq> {} \<longrightarrow> fst ((a >>= b) s) \<noteq> {} \<and> (fst ((a >>= b) s) \<noteq> {} \<longrightarrow> pick (fst ` fst ((a >>= b) s)) = pick (fst ` fst (b (pick (fst ` fst (a s))) s))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. snd (a s) \<longrightarrow> fst (a s) = {}; \<not> snd (a s) \<longrightarrow> (\<exists>aa b. a s = ({(aa, b)}, False)); \<And>s. \<lbrace>(=) s\<rbrace> a \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> (fst (b (pick (fst ` fst (a s))) s) = {} \<longrightarrow> fst ((a >>= b) s) = {}) \<and> (fst (b (pick (fst ` fst (a s))) s) \<noteq> {} \<longrightarrow> (fst (a s) = {} \<longrightarrow> fst ((a >>= b) s) = {}) \<and> (fst (a s) \<noteq> {} \<longrightarrow> fst ((a >>= b) s) \<noteq> {} \<and> (fst ((a >>= b) s) \<noteq> {} \<longrightarrow> pick (fst ` fst ((a >>= b) s)) = pick (fst ` fst (b (pick (fst ` fst (a s))) s))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> snd (a s) \<longrightarrow> (\<exists>aa b. a s = ({(aa, b)}, False)); \<And>s. \<lbrace>(=) s\<rbrace> a \<lbrace>\<lambda>r. (=) s\<rbrace>; snd (a s) \<longrightarrow> fst (a s) = {}\<rbrakk> \<Longrightarrow> (fst (b (pick (fst ` fst (a s))) s) = {} \<longrightarrow> fst ((a >>= b) s) = {}) \<and> (fst (b (pick (fst ` fst (a s))) s) \<noteq> {} \<longrightarrow> (fst (a s) = {} \<longrightarrow> fst ((a >>= b) s) = {}) \<and> (fst (a s) \<noteq> {} \<longrightarrow> fst ((a >>= b) s) \<noteq> {} \<and> (fst ((a >>= b) s) \<noteq> {} \<longrightarrow> pick (fst ` fst ((a >>= b) s)) = pick (fst ` fst (b (pick (fst ` fst (a s))) s))))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> snd (a s) \<longrightarrow> (\<exists>aa b. a s = ({(aa, b)}, False)); \<And>s. \<lbrace>(=) s\<rbrace> a \<lbrace>\<lambda>r. (=) s\<rbrace>; snd (a s) \<longrightarrow> fst (a s) = {}; snd (a s)\<rbrakk> \<Longrightarrow> (fst (b (pick (fst ` fst (a s))) s) = {} \<longrightarrow> fst ((a >>= b) s) = {}) \<and> (fst (b (pick (fst ` fst (a s))) s) \<noteq> {} \<longrightarrow> (fst (a s) = {} \<longrightarrow> fst ((a >>= b) s) = {}) \<and> (fst (a s) \<noteq> {} \<longrightarrow> fst ((a >>= b) s) \<noteq> {} \<and> (fst ((a >>= b) s) \<noteq> {} \<longrightarrow> pick (fst ` fst ((a >>= b) s)) = pick (fst ` fst (b (pick (fst ` fst (a s))) s)))))
 2. \<lbrakk>\<not> snd (a s) \<longrightarrow> (\<exists>aa b. a s = ({(aa, b)}, False)); \<And>s. \<lbrace>(=) s\<rbrace> a \<lbrace>\<lambda>r. (=) s\<rbrace>; snd (a s) \<longrightarrow> fst (a s) = {}; \<not> snd (a s)\<rbrakk> \<Longrightarrow> (fst (b (pick (fst ` fst (a s))) s) = {} \<longrightarrow> fst ((a >>= b) s) = {}) \<and> (fst (b (pick (fst ` fst (a s))) s) \<noteq> {} \<longrightarrow> (fst (a s) = {} \<longrightarrow> fst ((a >>= b) s) = {}) \<and> (fst (a s) \<noteq> {} \<longrightarrow> fst ((a >>= b) s) \<noteq> {} \<and> (fst ((a >>= b) s) \<noteq> {} \<longrightarrow> pick (fst ` fst ((a >>= b) s)) = pick (fst ` fst (b (pick (fst ` fst (a s))) s))))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> a \<lbrace>\<lambda>r. (=) s\<rbrace>; fst (a s) = {}; snd (a s)\<rbrakk> \<Longrightarrow> fst ((a >>= b) s) = {}
 2. \<lbrakk>\<exists>aa b. a s = ({(aa, b)}, False); \<And>s. \<lbrace>(=) s\<rbrace> a \<lbrace>\<lambda>r. (=) s\<rbrace>; \<not> snd (a s)\<rbrakk> \<Longrightarrow> (fst (b (pick (fst ` fst (a s))) s) = {} \<longrightarrow> fst ((a >>= b) s) = {}) \<and> (fst (b (pick (fst ` fst (a s))) s) \<noteq> {} \<longrightarrow> (fst (a s) = {} \<longrightarrow> fst ((a >>= b) s) = {}) \<and> (fst (a s) \<noteq> {} \<longrightarrow> fst ((a >>= b) s) \<noteq> {} \<and> (fst ((a >>= b) s) \<noteq> {} \<longrightarrow> pick (fst ` fst ((a >>= b) s)) = pick (fst ` fst (b (pick (fst ` fst (a s))) s))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>aa b. a s = ({(aa, b)}, False); \<And>s. \<lbrace>(=) s\<rbrace> a \<lbrace>\<lambda>r. (=) s\<rbrace>; \<not> snd (a s)\<rbrakk> \<Longrightarrow> (fst (b (pick (fst ` fst (a s))) s) = {} \<longrightarrow> fst ((a >>= b) s) = {}) \<and> (fst (b (pick (fst ` fst (a s))) s) \<noteq> {} \<longrightarrow> (fst (a s) = {} \<longrightarrow> fst ((a >>= b) s) = {}) \<and> (fst (a s) \<noteq> {} \<longrightarrow> fst ((a >>= b) s) \<noteq> {} \<and> (fst ((a >>= b) s) \<noteq> {} \<longrightarrow> pick (fst ` fst ((a >>= b) s)) = pick (fst ` fst (b (pick (fst ` fst (a s))) s))))) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>\<And>s. \<forall>x\<in>fst (a s). case x of (r, x) \<Rightarrow> s = x; a s = ({(aa, ba)}, False)\<rbrakk> \<Longrightarrow> (fst (b aa s) = {} \<longrightarrow> fst ((a >>= b) s) = {}) \<and> (fst (b aa s) \<noteq> {} \<longrightarrow> fst ((a >>= b) s) \<noteq> {} \<and> (fst ((a >>= b) s) \<noteq> {} \<longrightarrow> pick (fst ` fst ((a >>= b) s)) = pick (fst ` fst (b aa s)))) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>a s = ({(aa, ba)}, False); \<forall>x\<in>fst (a s). case x of (r, x) \<Rightarrow> s = x\<rbrakk> \<Longrightarrow> (fst (b aa s) = {} \<longrightarrow> fst ((a >>= b) s) = {}) \<and> (fst (b aa s) \<noteq> {} \<longrightarrow> fst ((a >>= b) s) \<noteq> {} \<and> (fst ((a >>= b) s) \<noteq> {} \<longrightarrow> pick (fst ` fst ((a >>= b) s)) = pick (fst ` fst (b aa s)))) proof (prove)
goal:
No subgoals!