theory Intent_DR

lemma weak_det_spec_mapM:
  assumes single:
    "\<And>r P. weak_det_spec P (g r)"
  shows
    "weak_det_spec Q (mapM g ls)" proof (induct ls arbitrary:Q) case Nil show ?case apply (clarsimp simp:mapM_def sequence_def det_spec_return) apply (rule det_imply_weak_det[OF det_spec_return]) done next case (Cons x xs) show ?case using Cons.hyps apply (clarsimp simp:mapM_Cons weak_det_spec_def) apply (drule no_fail_compose_imp) apply clarsimp apply (rule det_compose) apply (rule weak_det_specD) apply (simp add: assms)+ apply (drule_tac x = r in spec) apply (drule meta_spec) apply (drule no_fail_compose_imp) apply clarsimp apply (rule det_compose) apply fastforce apply (rule det_spec_return) apply simp apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_det_spec Q (mapM g ls) proof (state)
goal (2 subgoals):
 1. \<And>Q. weak_det_spec Q (mapM g [])
 2. \<And>a ls Q. (\<And>Q. weak_det_spec Q (mapM g ls)) \<Longrightarrow> weak_det_spec Q (mapM g (a # ls)) proof (state)
this:


goal (2 subgoals):
 1. \<And>Q. weak_det_spec Q (mapM g [])
 2. \<And>a ls Q. (\<And>Q. weak_det_spec Q (mapM g ls)) \<Longrightarrow> weak_det_spec Q (mapM g (a # ls)) proof (prove)
goal (1 subgoal):
 1. weak_det_spec Q (mapM g []) proof (prove)
goal (1 subgoal):
 1. weak_det_spec Q (return []) proof (prove)
goal:
No subgoals! proof (state)
this:
weak_det_spec Q (mapM g [])

goal (1 subgoal):
 1. \<And>a ls Q. (\<And>Q. weak_det_spec Q (mapM g ls)) \<Longrightarrow> weak_det_spec Q (mapM g (a # ls)) proof (state)
goal (1 subgoal):
 1. \<And>a ls Q. (\<And>Q. weak_det_spec Q (mapM g ls)) \<Longrightarrow> weak_det_spec Q (mapM g (a # ls)) proof (state)
this:
weak_det_spec ?Q (mapM g xs)

goal (1 subgoal):
 1. \<And>a ls Q. (\<And>Q. weak_det_spec Q (mapM g ls)) \<Longrightarrow> weak_det_spec Q (mapM g (a # ls)) proof (prove)
goal (1 subgoal):
 1. weak_det_spec Q (mapM g (x # xs)) proof (prove)
using this:
weak_det_spec ?Q (mapM g xs)

goal (1 subgoal):
 1. weak_det_spec Q (mapM g (x # xs)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (do y <- g x;
ys <- mapM g xs;
return (y # ys)
od)\<rbrakk> \<Longrightarrow> det_spec Q (do y <- g x;
ys <- mapM g xs;
return (y # ys)
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x) \<and> (\<exists>Q. \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace> \<and> (\<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)))\<rbrakk> \<Longrightarrow> det_spec Q (do y <- g x;
ys <- mapM g xs;
return (y # ys)
od) proof (prove)
goal (1 subgoal):
 1. \<And>Q. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> det_spec Q (do y <- g x;
ys <- mapM g xs;
return (y # ys)
od) proof (prove)
goal (3 subgoals):
 1. \<And>Q. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> det_spec Q (g x)
 2. \<And>Q r. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> det_spec (?Q8 Q r) (do ys <- mapM g xs;
return (r # ys)
od)
 3. \<And>Q. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> g x \<lbrace>?Q8 Q\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>Q. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> weak_det_spec Q (g x)
 2. \<And>Q. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> no_fail Q (g x)
 3. \<And>Q r. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> det_spec (?Q8 Q r) (do ys <- mapM g xs;
return (r # ys)
od)
 4. \<And>Q. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> g x \<lbrace>?Q8 Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>Q r. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> det_spec (?Q8 Q r) (do ys <- mapM g xs;
return (r # ys)
od)
 2. \<And>Q. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> g x \<lbrace>?Q8 Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>Q r. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> det_spec (?Q8 Q r) (do ys <- mapM g xs;
return (r # ys)
od)
 2. \<And>Q. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> g x \<lbrace>?Q8 Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>Q r. \<lbrakk>no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od); no_fail (?Q17 Q r) (mapM g xs) \<longrightarrow> det_spec (?Q17 Q r) (mapM g xs)\<rbrakk> \<Longrightarrow> det_spec (?Q8 Q r) (do ys <- mapM g xs;
return (r # ys)
od)
 2. \<And>Q. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> g x \<lbrace>?Q8 Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>Q r. \<lbrakk>no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; no_fail (?Q17 Q r) (mapM g xs) \<longrightarrow> det_spec (?Q17 Q r) (mapM g xs); no_fail (Q r) (mapM g xs) \<and> (\<exists>Qa. \<lbrace>Q r\<rbrace> mapM g xs \<lbrace>Qa\<rbrace> \<and> (\<forall>ra. no_fail (Qa ra) (return (r # ra))))\<rbrakk> \<Longrightarrow> det_spec (?Q8 Q r) (do ys <- mapM g xs;
return (r # ys)
od)
 2. \<And>Q. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> g x \<lbrace>?Q8 Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>Q r Qaa. \<lbrakk>no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; no_fail (?Q17 Q r) (mapM g xs) \<longrightarrow> det_spec (?Q17 Q r) (mapM g xs); no_fail (Q r) (mapM g xs); \<lbrace>Q r\<rbrace> mapM g xs \<lbrace>Qaa\<rbrace>; \<forall>ra. no_fail (Qaa ra) (return (r # ra))\<rbrakk> \<Longrightarrow> det_spec (?Q8 Q r) (do ys <- mapM g xs;
return (r # ys)
od)
 2. \<And>Q. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> g x \<lbrace>?Q8 Q\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>Q r Qaa. \<lbrakk>no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; no_fail (?Q17 Q r) (mapM g xs) \<longrightarrow> det_spec (?Q17 Q r) (mapM g xs); no_fail (Q r) (mapM g xs); \<lbrace>Q r\<rbrace> mapM g xs \<lbrace>Qaa\<rbrace>; \<forall>ra. no_fail (Qaa ra) (return (r # ra))\<rbrakk> \<Longrightarrow> det_spec (?Q8 Q r) (mapM g xs)
 2. \<And>Q r Qaa ra. \<lbrakk>no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; no_fail (?Q17 Q r) (mapM g xs) \<longrightarrow> det_spec (?Q17 Q r) (mapM g xs); no_fail (Q r) (mapM g xs); \<lbrace>Q r\<rbrace> mapM g xs \<lbrace>Qaa\<rbrace>; \<forall>ra. no_fail (Qaa ra) (return (r # ra))\<rbrakk> \<Longrightarrow> det_spec (?Q26 Q r Qaa ra) (return (r # ra))
 3. \<And>Q r Qaa. \<lbrakk>no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; no_fail (?Q17 Q r) (mapM g xs) \<longrightarrow> det_spec (?Q17 Q r) (mapM g xs); no_fail (Q r) (mapM g xs); \<lbrace>Q r\<rbrace> mapM g xs \<lbrace>Qaa\<rbrace>; \<forall>ra. no_fail (Qaa ra) (return (r # ra))\<rbrakk> \<Longrightarrow> \<lbrace>?Q8 Q r\<rbrace> mapM g xs \<lbrace>?Q26 Q r Qaa\<rbrace>
 4. \<And>Q. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> g x \<lbrace>?Q8 Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>Q r Qaa ra. \<lbrakk>no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; no_fail (Q r) (mapM g xs) \<longrightarrow> det_spec (Q r) (mapM g xs); no_fail (Q r) (mapM g xs); \<lbrace>Q r\<rbrace> mapM g xs \<lbrace>Qaa\<rbrace>; \<forall>ra. no_fail (Qaa ra) (return (r # ra))\<rbrakk> \<Longrightarrow> det_spec (?Q26 Q r Qaa ra) (return (r # ra))
 2. \<And>Q r Qaa. \<lbrakk>no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; no_fail (Q r) (mapM g xs) \<longrightarrow> det_spec (Q r) (mapM g xs); no_fail (Q r) (mapM g xs); \<lbrace>Q r\<rbrace> mapM g xs \<lbrace>Qaa\<rbrace>; \<forall>ra. no_fail (Qaa ra) (return (r # ra))\<rbrakk> \<Longrightarrow> \<lbrace>Q r\<rbrace> mapM g xs \<lbrace>?Q26 Q r Qaa\<rbrace>
 3. \<And>Q. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>Q r Qaa. \<lbrakk>no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; no_fail (Q r) (mapM g xs) \<longrightarrow> det_spec (Q r) (mapM g xs); no_fail (Q r) (mapM g xs); \<lbrace>Q r\<rbrace> mapM g xs \<lbrace>Qaa\<rbrace>; \<forall>ra. no_fail (Qaa ra) (return (r # ra))\<rbrakk> \<Longrightarrow> \<lbrace>Q r\<rbrace> mapM g xs \<lbrace>?Q26 Q r Qaa\<rbrace>
 2. \<And>Q. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>Q. \<lbrakk>\<And>Q. no_fail Q (mapM g xs) \<longrightarrow> det_spec Q (mapM g xs); no_fail Q (g x); \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (do ys <- mapM g xs;
return (r # ys)
od)\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> g x \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
weak_det_spec Q (mapM g (x # xs))

goal:
No subgoals!