theory Intent_DR

lemma weak_det_spec_ret:
assumes no_fail_det:   "weak_det_spec ((=) s) f"
assumes op_eq: "g s = f s"
shows "\<lbrakk> x = the (evalMonad g s); empty_when_fail f\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r s. r = x\<rbrace>" apply (rule wp_no_fail_spec) apply clarsimp+ apply (clarsimp simp:op_eq evalMonad_def weak_det_spec_def  empty_when_fail_def)+ apply (drule_tac x = s in spec) apply (clarsimp simp:|rule conjI)+ apply (clarsimp simp:valid_def) apply (clarsimp) using no_fail_det[unfolded weak_det_spec_def] apply (clarsimp simp:det_spec_def valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = the (evalMonad g s); empty_when_fail f\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r s. r = x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x = the (evalMonad g s); empty_when_fail f\<rbrakk> \<Longrightarrow> empty_when_fail f
 2. \<lbrakk>x = the (evalMonad g s); empty_when_fail f\<rbrakk> \<Longrightarrow> no_fail ((=) s) f \<longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r s. r = x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = the (evalMonad g s); empty_when_fail f; no_fail ((=) s) f\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r sa. r = the (evalMonad g s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = the (if fst (f s) = {} then None else Some (pick (fst ` fst (g s)))); \<forall>s. snd (f s) \<longrightarrow> fst (f s) = {}; no_fail ((=) s) f\<rbrakk> \<Longrightarrow> (fst (f s) = {} \<longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r s. r = the None\<rbrace>) \<and> (fst (f s) \<noteq> {} \<longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r sa. r = pick (fst ` fst (f s))\<rbrace>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = the (if fst (f s) = {} then None else Some (pick (fst ` fst (g s)))); no_fail ((=) s) f; snd (f s) \<longrightarrow> fst (f s) = {}\<rbrakk> \<Longrightarrow> (fst (f s) = {} \<longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r s. r = the None\<rbrace>) \<and> (fst (f s) \<noteq> {} \<longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r sa. r = pick (fst ` fst (f s))\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x = the None; no_fail ((=) s) f; fst (f s) = {}\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r s. r = the None\<rbrace>
 2. \<lbrakk>x = the (if fst (f s) = {} then None else Some (pick (fst ` fst (g s)))); no_fail ((=) s) f; snd (f s) \<longrightarrow> fst (f s) = {}\<rbrakk> \<Longrightarrow> fst (f s) \<noteq> {} \<longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r sa. r = pick (fst ` fst (f s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = the (if fst (f s) = {} then None else Some (pick (fst ` fst (g s)))); no_fail ((=) s) f; snd (f s) \<longrightarrow> fst (f s) = {}\<rbrakk> \<Longrightarrow> fst (f s) \<noteq> {} \<longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r sa. r = pick (fst ` fst (f s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = pick (fst ` fst (g s)); no_fail ((=) s) f; fst (f s) \<noteq> {}; \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r sa. r = pick (fst ` fst (f s))\<rbrace> proof (prove)
using this:
no_fail ((=) s) f \<longrightarrow> det_spec ((=) s) f

goal (1 subgoal):
 1. \<lbrakk>x = pick (fst ` fst (g s)); no_fail ((=) s) f; fst (f s) \<noteq> {}; \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r sa. r = pick (fst ` fst (f s))\<rbrace> proof (prove)
goal:
No subgoals!