theory Nondet_While_Loop_Rules_Completeness

lemma validNF_whileLoop_complete:
  "(\<exists>I R.
       (\<forall>s. P r s \<longrightarrow> I r s )
     \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!)
     \<and> (wf R)
     \<and> (\<forall>r s. ( I r s \<and> \<not> C r s ) \<longrightarrow> Q r s))
    = \<lbrace> P r \<rbrace> whileLoop C B r \<lbrace> Q \<rbrace>!"
  (is "(\<exists>I R. ?LHS I R) = ?RHS") proof (rule iffI) assume lhs: "\<exists>I R. ?LHS I R" obtain I R where "?LHS I R" using lhs by auto thus ?RHS by - (rule validNF_whileLoop[where I=I and R=R], auto) next assume loop: "?RHS" define I where "I \<equiv> \<lambda>r s. \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<lbrace> \<lambda>r s. Q r s \<rbrace>!" define R where "R \<equiv> {(x, y). C (fst y) (snd y) \<and> x \<in> fst (B (fst y) (snd y)) \<and>
                                whileLoop_terminates C B (fst y) (snd y)}" have "wf R" using R_def whileLoop_terminates_wf by auto have start: "\<And>s. P r s \<Longrightarrow> I r s" by (metis (full_types) I_def loop validNF_weaken_pre) have fin: "\<And>r s. \<lbrakk> I r s; \<not> C r s \<rbrakk> \<Longrightarrow> Q r s" apply (unfold I_def) apply (subst (asm) whileLoop_unroll) apply (clarsimp simp: condition_def bind_def'
                     validNF_alt_def return_def) done have step: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r
                   \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!"
             (is "\<And>r s. \<lbrace> ?pre r s \<rbrace> B r \<lbrace> ?post r s \<rbrace>!") proof - have inv_step:
        "\<And>r s r' s'. \<lbrakk> I r s; C r s; (r', s') \<in> fst (B r s) \<rbrakk> \<Longrightarrow> I r' s'" apply (clarsimp simp: I_def) apply (subst (asm) whileLoop_unroll) apply (clarsimp simp: condition_def bind_def' validNF_alt_def) apply force done have R_step:
        "\<And>r s r' s'. \<lbrakk> I r s; C r s; (r', s') \<in> fst (B r s) \<rbrakk> \<Longrightarrow> ((r', s'), (r, s)) \<in> R" apply (clarsimp simp: I_def R_def) apply (clarsimp simp: validNF_alt_def whileLoop_def) done show "\<And>r s. ?thesis r s" apply rule apply (clarsimp simp: valid_def inv_step R_step) apply (clarsimp simp: no_fail_def I_def validNF_alt_def) apply (drule (1) snd_whileLoop_first_step) apply simp done qed show "\<exists>I' R'. ?LHS I' R'" using \<open>wf R\<close> start fin step by blast qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s)) = \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>! proof (state)
goal (2 subgoals):
 1. \<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) \<Longrightarrow> \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>!
 2. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>! \<Longrightarrow> \<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (state)
this:
\<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s)

goal (2 subgoals):
 1. \<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) \<Longrightarrow> \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>!
 2. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>! \<Longrightarrow> \<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
goal (1 subgoal):
 1. (\<And>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
\<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s)

goal (1 subgoal):
 1. (\<And>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
(\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s)

goal (2 subgoals):
 1. \<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) \<Longrightarrow> \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>!
 2. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>! \<Longrightarrow> \<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
using this:
(\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s)

goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>! proof (state)
this:
\<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>!

goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>! \<Longrightarrow> \<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (state)
goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>! \<Longrightarrow> \<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (state)
this:
\<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>!

goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>! \<Longrightarrow> \<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (state)
this:
I \<equiv> \<lambda>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>!

goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>! \<Longrightarrow> \<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (state)
this:
R \<equiv> {(x, y). C (fst y) (snd y) \<and> x \<in> fst (B (fst y) (snd y)) \<and> whileLoop_terminates C B (fst y) (snd y)}

goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>! \<Longrightarrow> \<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
goal (1 subgoal):
 1. wf R proof (prove)
using this:
R \<equiv> {(x, y). C (fst y) (snd y) \<and> x \<in> fst (B (fst y) (snd y)) \<and> whileLoop_terminates C B (fst y) (snd y)}
wf {(x, y). ?C (fst y) (snd y) \<and> x \<in> fst (?B (fst y) (snd y)) \<and> whileLoop_terminates ?C ?B (fst y) (snd y)}

goal (1 subgoal):
 1. wf R proof (state)
this:
wf R

goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>! \<Longrightarrow> \<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
goal (1 subgoal):
 1. \<And>s. P r s \<Longrightarrow> I r s proof (state)
this:
P r ?s \<Longrightarrow> I r ?s

goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>! \<Longrightarrow> \<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>\<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>!; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>\<lbrace>\<lambda>s'. s' = s\<rbrace> condition (C r)
  (B r >>= whileLoop C
  B)
  (return r) \<lbrace>Q\<rbrace>!; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>I ?r ?s; \<not> C ?r ?s\<rbrakk> \<Longrightarrow> Q ?r ?s

goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>! \<Longrightarrow> \<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>! proof (state)
goal (1 subgoal):
 1. \<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s'. \<lbrakk>I r s; C r s; (r', s') \<in> fst (B r s)\<rbrakk> \<Longrightarrow> I r' s' proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s'. \<lbrakk>\<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>!; C r s; (r', s') \<in> fst (B r s)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'a. s'a = s'\<rbrace> whileLoop C
  B r' \<lbrace>Q\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s'. \<lbrakk>\<lbrace>\<lambda>s'. s' = s\<rbrace> condition (C r)
  (B r >>= whileLoop C
  B)
  (return r) \<lbrace>Q\<rbrace>!; C r s; (r', s') \<in> fst (B r s)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'a. s'a = s'\<rbrace> whileLoop C
  B r' \<lbrace>Q\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s'. \<lbrakk>C r s; (r', s') \<in> fst (B r s); \<forall>a b. (\<exists>x\<in>fst (B r s). case x of (r', s') \<Rightarrow> (a, b) \<in> fst (whileLoop C
  B r' s')) \<longrightarrow> Q a b; \<not> snd (B r s); \<forall>x\<in>fst (B r s). \<not> (case x of (r', s') \<Rightarrow> snd (whileLoop C
  B r' s'))\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (whileLoop C
  B r' s'). case x of (x, xa) \<Rightarrow> Q x xa) \<and> \<not> snd (whileLoop C
  B r' s') proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>I ?r ?s; C ?r ?s; (?r', ?s') \<in> fst (B ?r ?s)\<rbrakk> \<Longrightarrow> I ?r' ?s'

goal (1 subgoal):
 1. \<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s'. \<lbrakk>I r s; C r s; (r', s') \<in> fst (B r s)\<rbrakk> \<Longrightarrow> ((r', s'), r, s) \<in> R proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s'. \<lbrakk>\<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>!; C r s; (r', s') \<in> fst (B r s)\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>I ?r ?s; C ?r ?s; (?r', ?s') \<in> fst (B ?r ?s)\<rbrakk> \<Longrightarrow> ((?r', ?s'), ?r, ?s) \<in> R

goal (1 subgoal):
 1. \<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>! proof (prove)
goal (2 subgoals):
 1. \<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>
 2. \<And>r s. no_fail (\<lambda>s'. I r s' \<and> C r s' \<and> s' = s) (B r) proof (prove)
goal (1 subgoal):
 1. \<And>r s. no_fail (\<lambda>s'. I r s' \<and> C r s' \<and> s' = s) (B r) proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>\<forall>x\<in>fst (whileLoop C
  B r s). case x of (x, xa) \<Rightarrow> Q x xa; \<not> snd (whileLoop C
  B r s); C r s; snd (B r s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>\<forall>x\<in>fst (whileLoop C
  B r s). case x of (x, xa) \<Rightarrow> Q x xa; C r s; snd (B r s); \<not> snd (B r s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s'. I ?r s' \<and> C ?r s' \<and> s' = ?s\<rbrace> B ?r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), ?r, ?s) \<in> R\<rbrace>!

goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s'. I ?r s' \<and> C ?r s' \<and> s' = ?s\<rbrace> B ?r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), ?r, ?s) \<in> R\<rbrace>!

goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>! \<Longrightarrow> \<exists>I R. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<and> wf R \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
goal (1 subgoal):
 1. \<exists>I' R'. (\<forall>s. P r s \<longrightarrow> I' r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I' r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I' r' s' \<and> ((r', s'), r, s) \<in> R'\<rbrace>!) \<and> wf R' \<and> (\<forall>r s. I' r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
using this:
wf R
P r ?s \<Longrightarrow> I r ?s
\<lbrakk>I ?r ?s; \<not> C ?r ?s\<rbrakk> \<Longrightarrow> Q ?r ?s
\<lbrace>\<lambda>s'. I ?r s' \<and> C ?r s' \<and> s' = ?s\<rbrace> B ?r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), ?r, ?s) \<in> R\<rbrace>!

goal (1 subgoal):
 1. \<exists>I' R'. (\<forall>s. P r s \<longrightarrow> I' r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I' r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I' r' s' \<and> ((r', s'), r, s) \<in> R'\<rbrace>!) \<and> wf R' \<and> (\<forall>r s. I' r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (state)
this:
\<exists>I' R'. (\<forall>s. P r s \<longrightarrow> I' r s) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. I' r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I' r' s' \<and> ((r', s'), r, s) \<in> R'\<rbrace>!) \<and> wf R' \<and> (\<forall>r s. I' r s \<and> \<not> C r s \<longrightarrow> Q r s)

goal:
No subgoals!