theory Intent_DR

lemma empty_when_fail_mapM:
  "(\<And>P l. weak_det_spec P (x l) \<and> empty_when_fail (x l))
  \<Longrightarrow> empty_when_fail (mapM x ls)" proof (induct ls) case Nil show ?case by (clarsimp simp:mapM_def sequence_def empty_when_fail_return) next case (Cons x xs) show ?case apply (clarsimp simp:mapM_Cons) apply (rule empty_when_fail_compose)+ apply (simp add: empty_when_fail_return) apply (rule Cons)+ apply (rule weak_det_spec_mapM) apply (simp add: Cons)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>P l. weak_det_spec P (x l) \<and> empty_when_fail (x l)) \<Longrightarrow> empty_when_fail (mapM x ls) proof (state)
goal (2 subgoals):
 1. (\<And>P l. weak_det_spec P (x l) \<and> empty_when_fail (x l)) \<Longrightarrow> empty_when_fail (mapM x [])
 2. \<And>a ls. \<lbrakk>(\<And>P l. weak_det_spec P (x l) \<and> empty_when_fail (x l)) \<Longrightarrow> empty_when_fail (mapM x ls); \<And>P l. weak_det_spec P (x l) \<and> empty_when_fail (x l)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM x (a # ls)) proof (state)
this:
weak_det_spec ?P (x ?l) \<and> empty_when_fail (x ?l)

goal (2 subgoals):
 1. (\<And>P l. weak_det_spec P (x l) \<and> empty_when_fail (x l)) \<Longrightarrow> empty_when_fail (mapM x [])
 2. \<And>a ls. \<lbrakk>(\<And>P l. weak_det_spec P (x l) \<and> empty_when_fail (x l)) \<Longrightarrow> empty_when_fail (mapM x ls); \<And>P l. weak_det_spec P (x l) \<and> empty_when_fail (x l)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM x (a # ls)) proof (prove)
goal (1 subgoal):
 1. empty_when_fail (mapM x []) proof (state)
this:
empty_when_fail (mapM x [])

goal (1 subgoal):
 1. \<And>a ls. \<lbrakk>(\<And>P l. weak_det_spec P (x l) \<and> empty_when_fail (x l)) \<Longrightarrow> empty_when_fail (mapM x ls); \<And>P l. weak_det_spec P (x l) \<and> empty_when_fail (x l)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM x (a # ls)) proof (state)
goal (1 subgoal):
 1. \<And>a ls. \<lbrakk>(\<And>P l. weak_det_spec P (x l) \<and> empty_when_fail (x l)) \<Longrightarrow> empty_when_fail (mapM x ls); \<And>P l. weak_det_spec P (x l) \<and> empty_when_fail (x l)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM x (a # ls)) proof (state)
this:
(\<And>P l. weak_det_spec P (x l) \<and> empty_when_fail (x l)) \<Longrightarrow> empty_when_fail (mapM x xs)
weak_det_spec ?P (x ?l) \<and> empty_when_fail (x ?l)

goal (1 subgoal):
 1. \<And>a ls. \<lbrakk>(\<And>P l. weak_det_spec P (x l) \<and> empty_when_fail (x l)) \<Longrightarrow> empty_when_fail (mapM x ls); \<And>P l. weak_det_spec P (x l) \<and> empty_when_fail (x l)\<rbrakk> \<Longrightarrow> empty_when_fail (mapM x (a # ls)) proof (prove)
goal (1 subgoal):
 1. empty_when_fail (mapM x (x # xs)) proof (prove)
goal (1 subgoal):
 1. empty_when_fail (do y <- x x;
ys <- mapM x xs;
return (y # ys)
od) proof (prove)
goal (5 subgoals):
 1. \<And>r ra. empty_when_fail (return (r # ra))
 2. \<And>r. empty_when_fail (mapM x xs)
 3. \<And>r P. weak_det_spec P (mapM x xs)
 4. empty_when_fail (x x)
 5. \<And>P. weak_det_spec P (x x) proof (prove)
goal (4 subgoals):
 1. \<And>r. empty_when_fail (mapM x xs)
 2. \<And>r P. weak_det_spec P (mapM x xs)
 3. empty_when_fail (x x)
 4. \<And>P. weak_det_spec P (x x) proof (prove)
goal (3 subgoals):
 1. \<And>r P. weak_det_spec P (mapM x xs)
 2. empty_when_fail (x x)
 3. \<And>P. weak_det_spec P (x x) proof (prove)
goal (3 subgoals):
 1. \<And>r P ra Pa. weak_det_spec Pa (x ra)
 2. empty_when_fail (x x)
 3. \<And>P. weak_det_spec P (x x) proof (prove)
goal:
No subgoals! proof (state)
this:
empty_when_fail (mapM x (x # xs))

goal:
No subgoals!