theory Nondet_While_Loop_Rules_Completeness

lemma valid_whileLoop_complete:
  "(\<exists>I.
       (\<forall>s. P r s \<longrightarrow> I r s )
     \<and> (\<forall>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<rbrace> B r \<lbrace> I \<rbrace>)
     \<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>" apply (rule iffI) apply clarsimp apply (rename_tac I) apply (rule_tac I=I in valid_whileLoop, auto)[1] apply (rule exI [where x="\<lambda>r s. \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<lbrace> Q \<rbrace>"]) apply (intro conjI) apply (clarsimp simp: valid_def) apply (subst (2) valid_def) apply clarsimp apply (rename_tac a b) apply (subst (asm) (2) whileLoop_unroll) apply (case_tac "C a b") apply (clarsimp simp: valid_def bind_def' Bex_def condition_def split: if_split_asm) apply force apply (clarsimp simp: valid_def bind_def' Bex_def condition_def split: if_split_asm) apply force apply (subst whileLoop_unroll) apply (clarsimp simp: valid_def bind_def' condition_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>I. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>) \<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 (prove)
goal (2 subgoals):
 1. \<exists>I. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>) \<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. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>) \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
goal (2 subgoals):
 1. \<And>I. \<lbrakk>\<forall>s. P r s \<longrightarrow> I r s; \<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>; \<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s\<rbrakk> \<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. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>) \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
goal (2 subgoals):
 1. \<And>I. \<lbrakk>\<forall>s. P r s \<longrightarrow> I r s; \<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>; \<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s\<rbrakk> \<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. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>) \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> \<exists>I. (\<forall>s. P r s \<longrightarrow> I r s) \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>) \<and> (\<forall>r s. I r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> (\<forall>s. P r s \<longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>) \<and> (\<forall>r. \<lbrace>\<lambda>s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<and> C r s\<rbrace> B r \<lbrace>\<lambda>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>\<rbrace>) \<and> (\<forall>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
goal (3 subgoals):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>s. P r s \<longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>
 2. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>r. \<lbrace>\<lambda>s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<and> C r s\<rbrace> B r \<lbrace>\<lambda>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>\<rbrace>
 3. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<and> \<not> C r s \<longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>r. \<lbrace>\<lambda>s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<and> C r s\<rbrace> B r \<lbrace>\<lambda>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>\<rbrace>
 2. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<and> \<not> C r s \<longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<and> C r s \<longrightarrow> (\<forall>(r, s')\<in>fst (B r s). \<lbrace>\<lambda>s'a. s'a = s'\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>)
 2. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<and> \<not> C r s \<longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. \<And>ra s a b. \<lbrakk>\<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>; (a, b) \<in> fst (B ra s); \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B ra \<lbrace>Q\<rbrace>; C ra s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. s' = b\<rbrace> whileLoop C
  B a \<lbrace>Q\<rbrace>
 2. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<and> \<not> C r s \<longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. \<And>ra s a b. \<lbrakk>\<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>; (a, b) \<in> fst (B ra s); \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B ra \<lbrace>Q\<rbrace>; C ra s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. s' = b\<rbrace> whileLoop C
  B a \<lbrace>Q\<rbrace>
 2. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<and> \<not> C r s \<longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. \<And>ra s a b. \<lbrakk>\<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>; (a, b) \<in> fst (B ra s); \<lbrace>\<lambda>s'. s' = s\<rbrace> condition (C ra)
  (B ra >>= whileLoop C
  B)
  (return ra) \<lbrace>Q\<rbrace>; C ra s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. s' = b\<rbrace> whileLoop C
  B a \<lbrace>Q\<rbrace>
 2. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<and> \<not> C r s \<longrightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. \<And>ra s a b. \<lbrakk>\<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>; (a, b) \<in> fst (B ra s); \<lbrace>\<lambda>s'. s' = s\<rbrace> condition (C ra)
  (B ra >>= whileLoop C
  B)
  (return ra) \<lbrace>Q\<rbrace>; C ra s; C a b\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. s' = b\<rbrace> whileLoop C
  B a \<lbrace>Q\<rbrace>
 2. \<And>ra s a b. \<lbrakk>\<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>; (a, b) \<in> fst (B ra s); \<lbrace>\<lambda>s'. s' = s\<rbrace> condition (C ra)
  (B ra >>= whileLoop C
  B)
  (return ra) \<lbrace>Q\<rbrace>; C ra s; \<not> C a b\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. s' = b\<rbrace> whileLoop C
  B a \<lbrace>Q\<rbrace>
 3. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<and> \<not> C r s \<longrightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. \<And>ra s a b aa ba. \<lbrakk>\<forall>s. P r s \<longrightarrow> (\<forall>x\<in>fst (whileLoop C
  B r s). case x of (x, xa) \<Rightarrow> Q x xa); (a, b) \<in> fst (B ra s); \<forall>a b. (\<exists>aa ba. (aa, ba) \<in> fst (B ra s) \<and> (a, b) \<in> fst (whileLoop C
  B aa ba)) \<longrightarrow> Q a b; C ra s; C a b; (aa, ba) \<in> fst (whileLoop C
  B a b)\<rbrakk> \<Longrightarrow> Q aa ba
 2. \<And>ra s a b. \<lbrakk>\<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>; (a, b) \<in> fst (B ra s); \<lbrace>\<lambda>s'. s' = s\<rbrace> condition (C ra)
  (B ra >>= whileLoop C
  B)
  (return ra) \<lbrace>Q\<rbrace>; C ra s; \<not> C a b\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. s' = b\<rbrace> whileLoop C
  B a \<lbrace>Q\<rbrace>
 3. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<and> \<not> C r s \<longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. \<And>ra s a b. \<lbrakk>\<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>; (a, b) \<in> fst (B ra s); \<lbrace>\<lambda>s'. s' = s\<rbrace> condition (C ra)
  (B ra >>= whileLoop C
  B)
  (return ra) \<lbrace>Q\<rbrace>; C ra s; \<not> C a b\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. s' = b\<rbrace> whileLoop C
  B a \<lbrace>Q\<rbrace>
 2. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<and> \<not> C r s \<longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. \<And>ra s a b aa ba. \<lbrakk>\<forall>s. P r s \<longrightarrow> (\<forall>x\<in>fst (whileLoop C
  B r s). case x of (x, xa) \<Rightarrow> Q x xa); (a, b) \<in> fst (B ra s); \<forall>a b. (\<exists>aa ba. (aa, ba) \<in> fst (B ra s) \<and> (a, b) \<in> fst (whileLoop C
  B aa ba)) \<longrightarrow> Q a b; C ra s; \<not> C a b; (aa, ba) \<in> fst (whileLoop C
  B a b)\<rbrakk> \<Longrightarrow> Q aa ba
 2. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<and> \<not> C r s \<longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<and> \<not> C r s \<longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>r s. \<lbrace>\<lambda>s'. s' = s\<rbrace> condition (C r)
  (B r >>= whileLoop C
  B)
  (return r) \<lbrace>Q\<rbrace> \<and> \<not> C r s \<longrightarrow> Q r s proof (prove)
goal:
No subgoals!