theory Nondet_While_Loop_Rules_Completeness

lemma exs_valid_whileLoop_complete:
   "(\<exists>T R.
         (\<forall>s. P s \<longrightarrow> T r s)
         \<and> (\<forall>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
         \<and> (\<forall>r s. (T r s \<and> \<not> C r s) \<longrightarrow> Q r s))
      = (\<lbrace> P \<rbrace> whileLoop C B r \<exists>\<lbrace> Q \<rbrace>)"
  (is "(\<exists>T R. ?LHS T R) = ?RHS") proof (rule iffI) assume lhs: "\<exists>T R. ?LHS T R" obtain T R where TR: "?LHS T R" using lhs by blast show "?RHS" by (rule exs_valid_whileLoop [where T=T and R=R], auto simp: TR) next assume rhs: "?RHS" define I where "I \<equiv> \<lambda>r s. \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<exists>\<lbrace> Q \<rbrace>" define R where "R \<equiv> measure (\<lambda>(r, s). shortest_path_length C B (r, s) Q)" have P_s: "\<And>s. P s \<Longrightarrow> I r s" using rhs by (clarsimp simp: I_def exs_valid_def) have inv_holds: "\<And>r s. \<lbrakk> I r s; C r s \<rbrakk> \<Longrightarrow>
              \<exists>(r', s') \<in> fst (B r s). I r' s' \<and> ((r', s'), r, s) \<in> R" apply (clarsimp simp: I_def R_def) apply (frule (1) shortest_path_gets_shorter) apply clarsimp apply (rule bexI [rotated], assumption) apply clarsimp done have wf_R: "wf R" by (clarsimp simp: R_def) have last_step: "\<And>r s. \<lbrakk> I r s; \<not> C r s \<rbrakk> \<Longrightarrow> Q r s" apply (clarsimp simp: I_def exs_valid_def) apply (metis in_return whileLoop_cond_fail) done show "\<exists>I R. ?LHS I R" apply (rule exI [where x=I]) apply (rule exI [where x=R]) using P_s inv_holds wf_R last_step apply (clarsimp simp: exs_valid_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s)) = \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> proof (state)
goal (2 subgoals):
 1. \<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s) \<Longrightarrow> \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace>
 2. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> \<Longrightarrow> \<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (state)
this:
\<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s)

goal (2 subgoals):
 1. \<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s) \<Longrightarrow> \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace>
 2. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> \<Longrightarrow> \<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
goal (1 subgoal):
 1. (\<And>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
\<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s)

goal (1 subgoal):
 1. (\<And>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
(\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s)

goal (2 subgoals):
 1. \<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s) \<Longrightarrow> \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace>
 2. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> \<Longrightarrow> \<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
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 (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> \<Longrightarrow> \<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (state)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> \<Longrightarrow> \<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (state)
this:
\<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> \<Longrightarrow> \<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T 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 \<exists>\<lbrace>Q\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> \<Longrightarrow> \<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (state)
this:
R \<equiv> measure (\<lambda>(r, s). shortest_path_length C B (r, s) Q)

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> \<Longrightarrow> \<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> I r s proof (prove)
using this:
\<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace>

goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> I r s proof (state)
this:
P ?s \<Longrightarrow> I r ?s

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> \<Longrightarrow> \<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>I r s; C r s\<rbrakk> \<Longrightarrow> \<exists>(r', s')\<in>fst (B r s). I r' s' \<and> ((r', s'), r, s) \<in> R proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>\<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace>; C r s\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B r s). case x of (r', s') \<Rightarrow> \<lbrace>\<lambda>s'a. s'a = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace> \<and> shortest_path_length C B (r', s') Q < shortest_path_length C B (r, s) Q proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>\<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace>; C r s; \<exists>(r', s')\<in>fst (B r s). shortest_path_length C B (r', s') Q < shortest_path_length C B (r, s) Q \<and> \<lbrace>\<lambda>s. s = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B r s). case x of (r', s') \<Rightarrow> \<lbrace>\<lambda>s'a. s'a = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace> \<and> shortest_path_length C B (r', s') Q < shortest_path_length C B (r, s) Q proof (prove)
goal (1 subgoal):
 1. \<And>r s a b. \<lbrakk>\<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace>; C r s; (a, b) \<in> fst (B r s); shortest_path_length C B (a, b) Q < shortest_path_length C B (r, s) Q; \<lbrace>\<lambda>s. s = b\<rbrace> whileLoop C
  B a \<exists>\<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B r s). case x of (r', s') \<Rightarrow> \<lbrace>\<lambda>s'a. s'a = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace> \<and> shortest_path_length C B (r', s') Q < shortest_path_length C B (r, s) Q proof (prove)
goal (1 subgoal):
 1. \<And>r s a b. \<lbrakk>\<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace>; C r s; (a, b) \<in> fst (B r s); shortest_path_length C B (a, b) Q < shortest_path_length C B (r, s) Q; \<lbrace>\<lambda>s. s = b\<rbrace> whileLoop C
  B a \<exists>\<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> case (a, b) of (r', s') \<Rightarrow> \<lbrace>\<lambda>s'a. s'a = s'\<rbrace> whileLoop C
  B r' \<exists>\<lbrace>Q\<rbrace> \<and> shortest_path_length C B (r', s') Q < shortest_path_length C B (r, s) Q proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>I ?r ?s; C ?r ?s\<rbrakk> \<Longrightarrow> \<exists>(r', s')\<in>fst (B ?r ?s). I r' s' \<and> ((r', s'), ?r, ?s) \<in> R

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> \<Longrightarrow> \<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
goal (1 subgoal):
 1. wf R proof (state)
this:
wf R

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> \<Longrightarrow> \<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T 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 a b. \<lbrakk>\<not> C r s; (a, b) \<in> fst (whileLoop C
  B r s); Q a b\<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\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace> \<Longrightarrow> \<exists>T R. (\<forall>s. P s \<longrightarrow> T r s) \<and> (\<forall>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 \<and> (\<forall>r s. T r s \<and> \<not> C r s \<longrightarrow> Q r s) proof (prove)
goal (1 subgoal):
 1. \<exists>I R. (\<forall>s. P s \<longrightarrow> I r s) \<and> (\<forall>r s0. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> s = s0\<rbrace> B r \<exists>\<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s0) \<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>R. (\<forall>s. P s \<longrightarrow> I r s) \<and> (\<forall>r s0. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> s = s0\<rbrace> B r \<exists>\<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s0) \<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. (\<forall>s. P s \<longrightarrow> I r s) \<and> (\<forall>r s0. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> s = s0\<rbrace> B r \<exists>\<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s0) \<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:
P ?s \<Longrightarrow> I r ?s
\<lbrakk>I ?r ?s; C ?r ?s\<rbrakk> \<Longrightarrow> \<exists>(r', s')\<in>fst (B ?r ?s). I r' s' \<and> ((r', s'), ?r, ?s) \<in> R
wf R
\<lbrakk>I ?r ?s; \<not> C ?r ?s\<rbrakk> \<Longrightarrow> Q ?r ?s

goal (1 subgoal):
 1. (\<forall>s. P s \<longrightarrow> I r s) \<and> (\<forall>r s0. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> s = s0\<rbrace> B r \<exists>\<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s0) \<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:
No subgoals! proof (state)
this:
\<exists>I R. (\<forall>s. P s \<longrightarrow> I r s) \<and> (\<forall>r s0. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> s = s0\<rbrace> B r \<exists>\<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s0) \<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!