theory Nondet_While_Loop_Rules_Completeness

lemma snd_whileLoop_complete:
  shows "snd (whileLoop C B r s) =
              (\<exists>I. I r s \<and> C r s \<and>
                   (\<forall>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s) \<rbrace>
                            B r \<exists>\<lbrace> \<lambda>r s. C r s \<and> I r s \<rbrace>))"
  (is "?LHS = ?RHS") proof (rule iffI) assume "?LHS" thus "?RHS" apply (clarsimp simp: whileLoop_def) apply (erule disjE) apply (rule exI [where x="\<lambda>r s. (Some (r, s), None) \<in> whileLoop_results C B"]) apply (intro conjI) apply simp apply (metis Pair_inject whileLoop_results_cases_fail) apply (clarsimp simp: exs_valid_def) apply (erule whileLoop_results_cases_fail, fastforce) apply clarsimp apply (erule bexI [rotated]) apply clarsimp apply (metis fst_conv snd_conv whileLoop_results_cases_fail) apply (rule exI [where x="\<lambda>r s. \<not> whileLoop_terminates C B r s"]) apply clarsimp apply (rule conjI) apply (subst (asm)  whileLoop_terminates_simps) apply clarsimp apply (clarsimp simp: exs_valid_def) apply (subst (asm) (2)  whileLoop_terminates_simps) apply clarsimp apply (erule bexI [rotated]) apply clarsimp apply (subst (asm) (2)  whileLoop_terminates_simps) apply clarsimp done next assume "?RHS" thus "?LHS" apply clarsimp apply (erule (1) snd_whileLoop) apply force done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd (whileLoop C
  B r s) = (\<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>)) proof (state)
goal (2 subgoals):
 1. snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>)
 2. \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) \<Longrightarrow> snd (whileLoop C
  B r s) proof (state)
this:
snd (whileLoop C
  B r s)

goal (2 subgoals):
 1. snd (whileLoop C
  B r s) \<Longrightarrow> \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>)
 2. \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) \<Longrightarrow> snd (whileLoop C
  B r s) proof (prove)
using this:
snd (whileLoop C
  B r s)

goal (1 subgoal):
 1. \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) proof (prove)
goal (1 subgoal):
 1. (Some (r, s), None) \<in> whileLoop_results C B \<or> \<not> whileLoop_terminates C B r s \<Longrightarrow> \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) proof (prove)
goal (2 subgoals):
 1. (Some (r, s), None) \<in> whileLoop_results C B \<Longrightarrow> \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>)
 2. \<not> whileLoop_terminates C B r s \<Longrightarrow> \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) proof (prove)
goal (2 subgoals):
 1. (Some (r, s), None) \<in> whileLoop_results C B \<Longrightarrow> (Some (r, s), None) \<in> whileLoop_results C B \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. (Some (r, s), None) \<in> whileLoop_results C B \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> (Some (r, s), None) \<in> whileLoop_results C B\<rbrace>)
 2. \<not> whileLoop_terminates C B r s \<Longrightarrow> \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) proof (prove)
goal (4 subgoals):
 1. (Some (r, s), None) \<in> whileLoop_results C B \<Longrightarrow> (Some (r, s), None) \<in> whileLoop_results C B
 2. (Some (r, s), None) \<in> whileLoop_results C B \<Longrightarrow> C r s
 3. (Some (r, s), None) \<in> whileLoop_results C B \<Longrightarrow> \<forall>r. \<lbrace>\<lambda>s. (Some (r, s), None) \<in> whileLoop_results C B \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> (Some (r, s), None) \<in> whileLoop_results C B\<rbrace>
 4. \<not> whileLoop_terminates C B r s \<Longrightarrow> \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) proof (prove)
goal (3 subgoals):
 1. (Some (r, s), None) \<in> whileLoop_results C B \<Longrightarrow> C r s
 2. (Some (r, s), None) \<in> whileLoop_results C B \<Longrightarrow> \<forall>r. \<lbrace>\<lambda>s. (Some (r, s), None) \<in> whileLoop_results C B \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> (Some (r, s), None) \<in> whileLoop_results C B\<rbrace>
 3. \<not> whileLoop_terminates C B r s \<Longrightarrow> \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) proof (prove)
goal (2 subgoals):
 1. (Some (r, s), None) \<in> whileLoop_results C B \<Longrightarrow> \<forall>r. \<lbrace>\<lambda>s. (Some (r, s), None) \<in> whileLoop_results C B \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> (Some (r, s), None) \<in> whileLoop_results C B\<rbrace>
 2. \<not> whileLoop_terminates C B r s \<Longrightarrow> \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<And>ra sa. \<lbrakk>(Some (r, s), None) \<in> whileLoop_results C B; (Some (ra, sa), None) \<in> whileLoop_results C B; C ra sa; \<not> snd (B ra sa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B ra sa). case x of (rv, s') \<Rightarrow> C rv s' \<and> (Some (rv, s'), None) \<in> whileLoop_results C B
 2. \<not> whileLoop_terminates C B r s \<Longrightarrow> \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<And>ra sa raa saa r' s'. \<lbrakk>(Some (r, s), None) \<in> whileLoop_results C B; C ra sa; \<not> snd (B ra sa); (ra, sa) = (raa, saa); C raa saa; (r', s') \<in> fst (B raa saa); (Some (r', s'), None) \<in> whileLoop_results C B\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B ra sa). case x of (rv, s') \<Rightarrow> C rv s' \<and> (Some (rv, s'), None) \<in> whileLoop_results C B
 2. \<not> whileLoop_terminates C B r s \<Longrightarrow> \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<And>sa ra r' s'. \<lbrakk>(Some (r, s), None) \<in> whileLoop_results C B; \<not> snd (B ra sa); C ra sa; (r', s') \<in> fst (B ra sa); (Some (r', s'), None) \<in> whileLoop_results C B\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B ra sa). case x of (rv, s') \<Rightarrow> C rv s' \<and> (Some (rv, s'), None) \<in> whileLoop_results C B
 2. \<not> whileLoop_terminates C B r s \<Longrightarrow> \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<And>sa ra r' s'. \<lbrakk>(Some (r, s), None) \<in> whileLoop_results C B; \<not> snd (B ra sa); C ra sa; (Some (r', s'), None) \<in> whileLoop_results C B\<rbrakk> \<Longrightarrow> case (r', s') of (rv, s') \<Rightarrow> C rv s' \<and> (Some (rv, s'), None) \<in> whileLoop_results C B
 2. \<not> whileLoop_terminates C B r s \<Longrightarrow> \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<And>sa ra r' s'. \<lbrakk>(Some (r, s), None) \<in> whileLoop_results C B; \<not> snd (B ra sa); C ra sa; (Some (r', s'), None) \<in> whileLoop_results C B\<rbrakk> \<Longrightarrow> C r' s'
 2. \<not> whileLoop_terminates C B r s \<Longrightarrow> \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) proof (prove)
goal (1 subgoal):
 1. \<not> whileLoop_terminates C B r s \<Longrightarrow> \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) proof (prove)
goal (1 subgoal):
 1. \<not> whileLoop_terminates C B r s \<Longrightarrow> \<not> whileLoop_terminates C B r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. \<not> whileLoop_terminates C B r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> \<not> whileLoop_terminates C B r s\<rbrace>) proof (prove)
goal (1 subgoal):
 1. \<not> whileLoop_terminates C B r s \<Longrightarrow> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. \<not> whileLoop_terminates C B r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> \<not> whileLoop_terminates C B r s\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<not> whileLoop_terminates C B r s \<Longrightarrow> C r s
 2. \<not> whileLoop_terminates C B r s \<Longrightarrow> \<forall>r. \<lbrace>\<lambda>s. \<not> whileLoop_terminates C B r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> \<not> whileLoop_terminates C B r s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<not> (C r s \<longrightarrow> (\<forall>(x, y)\<in>fst (B r s). whileLoop_terminates C B x y)) \<Longrightarrow> C r s
 2. \<not> whileLoop_terminates C B r s \<Longrightarrow> \<forall>r. \<lbrace>\<lambda>s. \<not> whileLoop_terminates C B r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> \<not> whileLoop_terminates C B r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> whileLoop_terminates C B r s \<Longrightarrow> \<forall>r. \<lbrace>\<lambda>s. \<not> whileLoop_terminates C B r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> \<not> whileLoop_terminates C B r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ra sa. \<lbrakk>\<not> whileLoop_terminates C B r s; \<not> whileLoop_terminates C B ra sa; C ra sa; \<not> snd (B ra sa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B ra sa). case x of (rv, s') \<Rightarrow> C rv s' \<and> \<not> whileLoop_terminates C B rv s' proof (prove)
goal (1 subgoal):
 1. \<And>ra sa. \<lbrakk>\<not> whileLoop_terminates C B r s; \<not> (C ra sa \<longrightarrow> (\<forall>(x, y)\<in>fst (B ra sa). whileLoop_terminates C B x y)); C ra sa; \<not> snd (B ra sa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B ra sa). case x of (rv, s') \<Rightarrow> C rv s' \<and> \<not> whileLoop_terminates C B rv s' proof (prove)
goal (1 subgoal):
 1. \<And>ra sa a b. \<lbrakk>\<not> whileLoop_terminates C B r s; C ra sa; \<not> snd (B ra sa); (a, b) \<in> fst (B ra sa); \<not> whileLoop_terminates C B a b\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B ra sa). case x of (rv, s') \<Rightarrow> C rv s' \<and> \<not> whileLoop_terminates C B rv s' proof (prove)
goal (1 subgoal):
 1. \<And>ra sa a b. \<lbrakk>\<not> whileLoop_terminates C B r s; C ra sa; \<not> snd (B ra sa); \<not> whileLoop_terminates C B a b\<rbrakk> \<Longrightarrow> case (a, b) of (rv, s') \<Rightarrow> C rv s' \<and> \<not> whileLoop_terminates C B rv s' proof (prove)
goal (1 subgoal):
 1. \<And>ra sa a b. \<lbrakk>\<not> whileLoop_terminates C B r s; C ra sa; \<not> snd (B ra sa); \<not> whileLoop_terminates C B a b\<rbrakk> \<Longrightarrow> C a b proof (prove)
goal (1 subgoal):
 1. \<And>ra sa a b. \<lbrakk>\<not> whileLoop_terminates C B r s; C ra sa; \<not> snd (B ra sa); \<not> (C a b \<longrightarrow> (\<forall>(x, y)\<in>fst (B a b). whileLoop_terminates C B x y))\<rbrakk> \<Longrightarrow> C a b proof (prove)
goal:
No subgoals! proof (state)
this:
\<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>)

goal (1 subgoal):
 1. \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) \<Longrightarrow> snd (whileLoop C
  B r s) proof (state)
goal (1 subgoal):
 1. \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) \<Longrightarrow> snd (whileLoop C
  B r s) proof (state)
this:
\<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>)

goal (1 subgoal):
 1. \<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>) \<Longrightarrow> snd (whileLoop C
  B r s) proof (prove)
using this:
\<exists>I. I r s \<and> C r s \<and> (\<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>)

goal (1 subgoal):
 1. snd (whileLoop C
  B r s) proof (prove)
goal (1 subgoal):
 1. \<And>I. \<lbrakk>I r s; C r s; \<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>\<rbrakk> \<Longrightarrow> snd (whileLoop C
  B r s) proof (prove)
goal (1 subgoal):
 1. \<And>I ra. \<lbrakk>C r s; \<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s)\<rbrace> B r \<exists>\<lbrace>\<lambda>r s. C r s \<and> I r s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. I ra s \<and> C ra s \<and> \<not> snd (B ra s)\<rbrace> B ra \<exists>\<lbrace>\<lambda>r' s'. C r' s' \<and> I r' s'\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
snd (whileLoop C
  B r s)

goal:
No subgoals!