theory Intent_DR

lemma select_f_evalMonad:
  "\<lbrakk>empty_fail g; empty_when_fail g; \<And>P. weak_det_spec P g; \<And>ms. \<lbrace>(=) ms\<rbrace>g\<lbrace>\<lambda>r. (=) ms\<rbrace>\<rbrakk>
  \<Longrightarrow> (select_f (g ms)) = (case (evalMonad g ms) of Some a \<Rightarrow> return (a,ms) | None \<Rightarrow> fail)" apply (rule ext) apply (clarsimp simp: return_def select_f_def fail_def empty_fail_def split:option.splits) apply (drule_tac x = ms in spec) apply (rule conjI) apply (clarsimp simp:evalMonad_def valid_def weak_det_spec_def)+ apply (drule_tac x = "(=) ms" in meta_spec)+ apply (clarsimp simp:no_fail_def empty_when_fail_def) apply (drule_tac x = ms in meta_spec) apply (clarsimp simp:det_spec_def) apply (drule_tac x = ms in spec) apply clarsimp done

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