theory Nondet_While_Loop_Rules_Completeness

lemma whileLoop_rule_strong_complete:
  "(\<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<lbrace> \<lambda>r s. (r, s) \<in> fst Q \<rbrace>
        \<and> (\<forall>r'' s''. (r'', s'') \<in> fst Q \<longrightarrow> \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<exists>\<lbrace> \<lambda>r s. r = r'' \<and> s = s'' \<rbrace>)
        \<and> (snd Q \<longrightarrow> snd (whileLoop C B r s))
        \<and> (\<not> snd Q \<longrightarrow> \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<lbrace> \<lambda>_ _. True \<rbrace>!))
    = (whileLoop C B r s = Q)" apply (rule iffI) apply (rule whileLoop_rule_strong, auto)[1] apply (clarsimp simp: valid_def exs_valid_def validNF_alt_def) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>\<lambda>r s. (r, s) \<in> fst Q\<rbrace> \<and> (\<forall>r'' s''. (r'', s'') \<in> fst Q \<longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>\<lambda>r s. r = r'' \<and> s = s''\<rbrace>) \<and> (snd Q \<longrightarrow> snd (whileLoop C
  B r s)) \<and> (\<not> snd Q \<longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>\<lambda>_ _. True\<rbrace>!)) = (whileLoop C
  B r s = Q) proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>\<lambda>r s. (r, s) \<in> fst Q\<rbrace> \<and> (\<forall>r'' s''. (r'', s'') \<in> fst Q \<longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>\<lambda>r s. r = r'' \<and> s = s''\<rbrace>) \<and> (snd Q \<longrightarrow> snd (whileLoop C
  B r s)) \<and> (\<not> snd Q \<longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>\<lambda>_ _. True\<rbrace>!) \<Longrightarrow> whileLoop C
  B r s = Q
 2. whileLoop C
  B r s = Q \<Longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>\<lambda>r s. (r, s) \<in> fst Q\<rbrace> \<and> (\<forall>r'' s''. (r'', s'') \<in> fst Q \<longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>\<lambda>r s. r = r'' \<and> s = s''\<rbrace>) \<and> (snd Q \<longrightarrow> snd (whileLoop C
  B r s)) \<and> (\<not> snd Q \<longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>\<lambda>_ _. True\<rbrace>!) proof (prove)
goal (1 subgoal):
 1. whileLoop C
  B r s = Q \<Longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>\<lambda>r s. (r, s) \<in> fst Q\<rbrace> \<and> (\<forall>r'' s''. (r'', s'') \<in> fst Q \<longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>\<lambda>r s. r = r'' \<and> s = s''\<rbrace>) \<and> (snd Q \<longrightarrow> snd (whileLoop C
  B r s)) \<and> (\<not> snd Q \<longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>\<lambda>_ _. True\<rbrace>!) proof (prove)
goal (1 subgoal):
 1. \<And>r'' s''. \<lbrakk>Q = whileLoop C
  B r s; (r'', s'') \<in> fst (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (whileLoop C
  B r s). case x of (rv, s') \<Rightarrow> rv = r'' \<and> s' = s'' proof (prove)
goal:
No subgoals!