theory Nondet_While_Loop_Rules

lemma whileLoop_rule_strong:
  assumes init_U: "\<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<lbrace> \<lambda>r s. (r, s) \<in> fst Q \<rbrace>"
  and path_exists: "\<And>r'' s''. \<lbrakk> (r'', s'') \<in> fst Q \<rbrakk> \<Longrightarrow> \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<exists>\<lbrace> \<lambda>r s. r = r'' \<and> s = s'' \<rbrace>"
  and loop_fail: "snd Q \<Longrightarrow> snd (whileLoop C B r s)"
  and loop_nofail: "\<not> snd Q \<Longrightarrow> \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<lbrace> \<lambda>_ _. True \<rbrace>!"
  shows "whileLoop C B r s = Q" using assms apply atomize apply (clarsimp simp: valid_def exs_valid_def validNF_def no_fail_def) apply rule apply blast apply blast apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whileLoop C
  B r s = Q proof (prove)
using this:
\<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>\<lambda>r s. (r, s) \<in> fst Q\<rbrace>
(?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>
snd Q \<Longrightarrow> snd (whileLoop C
  B r s)
\<not> snd Q \<Longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>\<lambda>_ _. True\<rbrace>!

goal (1 subgoal):
 1. whileLoop C
  B r s = Q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>\<lambda>r s. (r, s) \<in> fst Q\<rbrace>; \<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>; snd Q \<longrightarrow> snd (whileLoop C
  B r s); \<not> snd Q \<longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>\<lambda>_ _. True\<rbrace>!\<rbrakk> \<Longrightarrow> whileLoop C
  B r s = Q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>fst (whileLoop C
  B r s). x \<in> fst Q; \<forall>r'' s''. (r'', s'') \<in> fst Q \<longrightarrow> (\<exists>x\<in>fst (whileLoop C
  B r s). case x of (rv, s') \<Rightarrow> rv = r'' \<and> s' = s''); snd Q \<longrightarrow> snd (whileLoop C
  B r s); \<not> snd Q \<longrightarrow> \<not> snd (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> whileLoop C
  B r s = Q proof (prove)
goal (3 subgoals):
 1. \<And>ra t. \<lbrakk>\<forall>x\<in>fst (whileLoop C
  B r s). x \<in> fst Q; \<forall>r'' s''. (r'', s'') \<in> fst Q \<longrightarrow> (\<exists>x\<in>fst (whileLoop C
  B r s). case x of (rv, s') \<Rightarrow> rv = r'' \<and> s' = s''); snd Q \<longrightarrow> snd (whileLoop C
  B r s); \<not> snd Q \<longrightarrow> \<not> snd (whileLoop C
  B r s); (ra, t) \<in> fst (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> (ra, t) \<in> fst Q
 2. \<And>ra t. \<lbrakk>\<forall>x\<in>fst (whileLoop C
  B r s). x \<in> fst Q; \<forall>r'' s''. (r'', s'') \<in> fst Q \<longrightarrow> (\<exists>x\<in>fst (whileLoop C
  B r s). case x of (rv, s') \<Rightarrow> rv = r'' \<and> s' = s''); snd Q \<longrightarrow> snd (whileLoop C
  B r s); \<not> snd Q \<longrightarrow> \<not> snd (whileLoop C
  B r s); (ra, t) \<in> fst Q\<rbrakk> \<Longrightarrow> (ra, t) \<in> fst (whileLoop C
  B r s)
 3. \<lbrakk>\<forall>x\<in>fst (whileLoop C
  B r s). x \<in> fst Q; \<forall>r'' s''. (r'', s'') \<in> fst Q \<longrightarrow> (\<exists>x\<in>fst (whileLoop C
  B r s). case x of (rv, s') \<Rightarrow> rv = r'' \<and> s' = s''); snd Q \<longrightarrow> snd (whileLoop C
  B r s); \<not> snd Q \<longrightarrow> \<not> snd (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> snd (whileLoop C
  B r s) = snd Q proof (prove)
goal (2 subgoals):
 1. \<And>ra t. \<lbrakk>\<forall>x\<in>fst (whileLoop C
  B r s). x \<in> fst Q; \<forall>r'' s''. (r'', s'') \<in> fst Q \<longrightarrow> (\<exists>x\<in>fst (whileLoop C
  B r s). case x of (rv, s') \<Rightarrow> rv = r'' \<and> s' = s''); snd Q \<longrightarrow> snd (whileLoop C
  B r s); \<not> snd Q \<longrightarrow> \<not> snd (whileLoop C
  B r s); (ra, t) \<in> fst Q\<rbrakk> \<Longrightarrow> (ra, t) \<in> fst (whileLoop C
  B r s)
 2. \<lbrakk>\<forall>x\<in>fst (whileLoop C
  B r s). x \<in> fst Q; \<forall>r'' s''. (r'', s'') \<in> fst Q \<longrightarrow> (\<exists>x\<in>fst (whileLoop C
  B r s). case x of (rv, s') \<Rightarrow> rv = r'' \<and> s' = s''); snd Q \<longrightarrow> snd (whileLoop C
  B r s); \<not> snd Q \<longrightarrow> \<not> snd (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> snd (whileLoop C
  B r s) = snd Q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>fst (whileLoop C
  B r s). x \<in> fst Q; \<forall>r'' s''. (r'', s'') \<in> fst Q \<longrightarrow> (\<exists>x\<in>fst (whileLoop C
  B r s). case x of (rv, s') \<Rightarrow> rv = r'' \<and> s' = s''); snd Q \<longrightarrow> snd (whileLoop C
  B r s); \<not> snd Q \<longrightarrow> \<not> snd (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> snd (whileLoop C
  B r s) = snd Q proof (prove)
goal:
No subgoals!