theory Nondet_While_Loop_Rules

lemma exs_valid_whileLoop:
  assumes init_T: "\<And>s. P s \<Longrightarrow> T r s"
    and iter_I: "\<And>r s0. \<lbrace>\<lambda>s. T r s \<and> C r s \<and> s = s0\<rbrace> B r \<exists>\<lbrace>\<lambda>r' s'. T r' s' \<and> ((r', s'),(r, s0)) \<in> R\<rbrace>"
    and wf_R: "wf R"
    and final_I: "\<And>r s. \<lbrakk> T r s; \<not> C r s  \<rbrakk> \<Longrightarrow> Q r s"
  shows "\<lbrace> P \<rbrace> whileLoop C B r \<exists>\<lbrace> Q \<rbrace>" proof - { fix s assume "P s" { fix x have "T (fst x) (snd x) \<Longrightarrow> \<exists>r' s'. (r', s') \<in> fst (whileLoop C B (fst x) (snd x)) \<and> T r' s'" using wf_R proof induct case (less x) then show ?case apply atomize apply (cases "C (fst x) (snd x)") apply (subst whileLoop_unroll) apply (clarsimp simp: condition_def bind_def') apply (cut_tac iter_I[where ?s0.0="snd x" and r="fst x"]) apply (clarsimp simp: exs_valid_def) apply blast apply (subst whileLoop_unroll) apply (cases x) apply (clarsimp simp: condition_def bind_def' return_def) done qed } then have "\<exists>r' s'. (r', s') \<in> fst (whileLoop C B r s) \<and> Q r' s'" by (metis \<open>P s\<close> fst_conv init_T snd_conv final_I fst_whileLoop_cond_false) } thus ?thesis by (clarsimp simp: exs_valid_def Bex_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> proof (state)
this:
P s

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

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. T (fst x) (snd x) \<Longrightarrow> \<exists>r' s'. (r', s') \<in> fst (whileLoop C
  B (fst x) (snd x)) \<and> T r' s' proof (prove)
using this:
wf R

goal (1 subgoal):
 1. T (fst x) (snd x) \<Longrightarrow> \<exists>r' s'. (r', s') \<in> fst (whileLoop C
  B (fst x) (snd x)) \<and> T r' s' proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> R; T (fst y) (snd y)\<rbrakk> \<Longrightarrow> \<exists>r' s'. (r', s') \<in> fst (whileLoop C
  B (fst y) (snd y)) \<and> T r' s'; T (fst x) (snd x)\<rbrakk> \<Longrightarrow> \<exists>r' s'. (r', s') \<in> fst (whileLoop C
  B (fst x) (snd x)) \<and> T r' s' proof (state)
this:
\<lbrakk>(?y, x) \<in> R; T (fst ?y) (snd ?y)\<rbrakk> \<Longrightarrow> \<exists>r' s'. (r', s') \<in> fst (whileLoop C
  B (fst ?y) (snd ?y)) \<and> T r' s'
T (fst x) (snd x)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> R; T (fst y) (snd y)\<rbrakk> \<Longrightarrow> \<exists>r' s'. (r', s') \<in> fst (whileLoop C
  B (fst y) (snd y)) \<and> T r' s'; T (fst x) (snd x)\<rbrakk> \<Longrightarrow> \<exists>r' s'. (r', s') \<in> fst (whileLoop C
  B (fst x) (snd x)) \<and> T r' s' proof (chain)
picking this:
\<lbrakk>(?y, x) \<in> R; T (fst ?y) (snd ?y)\<rbrakk> \<Longrightarrow> \<exists>r' s'. (r', s') \<in> fst (whileLoop C
  B (fst ?y) (snd ?y)) \<and> T r' s'
T (fst x) (snd x) proof (prove)
using this:
\<lbrakk>(?y, x) \<in> R; T (fst ?y) (snd ?y)\<rbrakk> \<Longrightarrow> \<exists>r' s'. (r', s') \<in> fst (whileLoop C
  B (fst ?y) (snd ?y)) \<and> T r' s'
T (fst x) (snd x)

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

goal:
No subgoals! proof (state)
this:
T (fst x) (snd x) \<Longrightarrow> \<exists>r' s'. (r', s') \<in> fst (whileLoop C
  B (fst x) (snd x)) \<and> T r' s'

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> proof (state)
this:
T (fst ?x2) (snd ?x2) \<Longrightarrow> \<exists>r' s'. (r', s') \<in> fst (whileLoop C
  B (fst ?x2) (snd ?x2)) \<and> T r' s'

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> proof (chain)
picking this:
T (fst ?x2) (snd ?x2) \<Longrightarrow> \<exists>r' s'. (r', s') \<in> fst (whileLoop C
  B (fst ?x2) (snd ?x2)) \<and> T r' s' proof (prove)
using this:
T (fst ?x2) (snd ?x2) \<Longrightarrow> \<exists>r' s'. (r', s') \<in> fst (whileLoop C
  B (fst ?x2) (snd ?x2)) \<and> T r' s'

goal (1 subgoal):
 1. \<exists>r' s'. (r', s') \<in> fst (whileLoop C
  B r s) \<and> Q r' s' proof (state)
this:
\<exists>r' s'. (r', s') \<in> fst (whileLoop C
  B r s) \<and> Q r' s'

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> proof (state)
this:
P ?s2 \<Longrightarrow> \<exists>r' s'. (r', s') \<in> fst (whileLoop C
  B r ?s2) \<and> Q r' s'

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> proof (prove)
using this:
P ?s2 \<Longrightarrow> \<exists>r' s'. (r', s') \<in> fst (whileLoop C
  B r ?s2) \<and> Q r' s'

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

goal:
No subgoals!