theory Nondet_While_Loop_Rules_Completeness

lemma valid_path_implies_exs_valid_whileLoop:
  "valid_path C B l \<Longrightarrow> \<lbrace> \<lambda>s. s = snd (hd l) \<rbrace> whileLoop C B (fst (hd l)) \<exists>\<lbrace> \<lambda>r s. (r, s) = last l  \<rbrace>" proof (induct l) case Nil then show ?case by clarsimp next case (Cons a l) then show ?case apply clarsimp apply rule apply clarsimp apply (subst whileLoop_unroll) apply (clarsimp simp: condition_def bind_def' exs_valid_def return_def) apply clarsimp apply (subst whileLoop_unroll) apply (clarsimp simp: condition_def bind_def' exs_valid_def return_def) apply rule apply (clarsimp split: prod.splits) apply (cases l) apply clarsimp apply (clarsimp split del: if_split) apply (erule bexI[rotated]) apply clarsimp apply clarsimp apply (cases l; clarsimp) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_path C B l \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd l)\<rbrace> whileLoop C
  B (fst (hd l)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace> proof (state)
goal (2 subgoals):
 1. valid_path C B [] \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd [])\<rbrace> whileLoop C
  B (fst (hd [])) \<exists>\<lbrace>\<lambda>r s. (r, s) = last []\<rbrace>
 2. \<And>a l. \<lbrakk>valid_path C B l \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd l)\<rbrace> whileLoop C
  B (fst (hd l)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace>; valid_path C B (a # l)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd (a # l))\<rbrace> whileLoop C
  B (fst (hd (a # l))) \<exists>\<lbrace>\<lambda>r s. (r, s) = last (a # l)\<rbrace> proof (state)
this:
valid_path C B []

goal (2 subgoals):
 1. valid_path C B [] \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd [])\<rbrace> whileLoop C
  B (fst (hd [])) \<exists>\<lbrace>\<lambda>r s. (r, s) = last []\<rbrace>
 2. \<And>a l. \<lbrakk>valid_path C B l \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd l)\<rbrace> whileLoop C
  B (fst (hd l)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace>; valid_path C B (a # l)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd (a # l))\<rbrace> whileLoop C
  B (fst (hd (a # l))) \<exists>\<lbrace>\<lambda>r s. (r, s) = last (a # l)\<rbrace> proof (chain)
picking this:
valid_path C B [] proof (prove)
using this:
valid_path C B []

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s = snd (hd [])\<rbrace> whileLoop C
  B (fst (hd [])) \<exists>\<lbrace>\<lambda>r s. (r, s) = last []\<rbrace> proof (state)
this:
\<lbrace>\<lambda>s. s = snd (hd [])\<rbrace> whileLoop C
  B (fst (hd [])) \<exists>\<lbrace>\<lambda>r s. (r, s) = last []\<rbrace>

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>valid_path C B l \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd l)\<rbrace> whileLoop C
  B (fst (hd l)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace>; valid_path C B (a # l)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd (a # l))\<rbrace> whileLoop C
  B (fst (hd (a # l))) \<exists>\<lbrace>\<lambda>r s. (r, s) = last (a # l)\<rbrace> proof (state)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>valid_path C B l \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd l)\<rbrace> whileLoop C
  B (fst (hd l)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace>; valid_path C B (a # l)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd (a # l))\<rbrace> whileLoop C
  B (fst (hd (a # l))) \<exists>\<lbrace>\<lambda>r s. (r, s) = last (a # l)\<rbrace> proof (state)
this:
valid_path C B l \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd l)\<rbrace> whileLoop C
  B (fst (hd l)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace>
valid_path C B (a # l)

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>valid_path C B l \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd l)\<rbrace> whileLoop C
  B (fst (hd l)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace>; valid_path C B (a # l)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd (a # l))\<rbrace> whileLoop C
  B (fst (hd (a # l))) \<exists>\<lbrace>\<lambda>r s. (r, s) = last (a # l)\<rbrace> proof (chain)
picking this:
valid_path C B l \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd l)\<rbrace> whileLoop C
  B (fst (hd l)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace>
valid_path C B (a # l) proof (prove)
using this:
valid_path C B l \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd l)\<rbrace> whileLoop C
  B (fst (hd l)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace>
valid_path C B (a # l)

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s = snd (hd (a # l))\<rbrace> whileLoop C
  B (fst (hd (a # l))) \<exists>\<lbrace>\<lambda>r s. (r, s) = last (a # l)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_path C B l \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd l)\<rbrace> whileLoop C
  B (fst (hd l)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace>; valid_path C B (a # l)\<rbrakk> \<Longrightarrow> (l = [] \<longrightarrow> \<lbrace>\<lambda>s. s = snd a\<rbrace> whileLoop C
  B (fst a) \<exists>\<lbrace>\<lambda>r s. (r, s) = a\<rbrace>) \<and> (l \<noteq> [] \<longrightarrow> \<lbrace>\<lambda>s. s = snd a\<rbrace> whileLoop C
  B (fst a) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_path C B l \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd l)\<rbrace> whileLoop C
  B (fst (hd l)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace>; valid_path C B (a # l)\<rbrakk> \<Longrightarrow> l = [] \<longrightarrow> \<lbrace>\<lambda>s. s = snd a\<rbrace> whileLoop C
  B (fst a) \<exists>\<lbrace>\<lambda>r s. (r, s) = a\<rbrace>
 2. \<lbrakk>valid_path C B l \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd l)\<rbrace> whileLoop C
  B (fst (hd l)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace>; valid_path C B (a # l)\<rbrakk> \<Longrightarrow> l \<noteq> [] \<longrightarrow> \<lbrace>\<lambda>s. s = snd a\<rbrace> whileLoop C
  B (fst a) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> C (fst a) (snd a); l = []\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = snd a\<rbrace> whileLoop C
  B (fst a) \<exists>\<lbrace>\<lambda>r s. (r, s) = a\<rbrace>
 2. \<lbrakk>valid_path C B l \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd l)\<rbrace> whileLoop C
  B (fst (hd l)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace>; valid_path C B (a # l)\<rbrakk> \<Longrightarrow> l \<noteq> [] \<longrightarrow> \<lbrace>\<lambda>s. s = snd a\<rbrace> whileLoop C
  B (fst a) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> C (fst a) (snd a); l = []\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = snd a\<rbrace> condition (C (fst a))
  (B (fst a) >>= whileLoop C
  B)
  (return (fst a)) \<exists>\<lbrace>\<lambda>r s. (r, s) = a\<rbrace>
 2. \<lbrakk>valid_path C B l \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd l)\<rbrace> whileLoop C
  B (fst (hd l)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace>; valid_path C B (a # l)\<rbrakk> \<Longrightarrow> l \<noteq> [] \<longrightarrow> \<lbrace>\<lambda>s. s = snd a\<rbrace> whileLoop C
  B (fst a) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_path C B l \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd l)\<rbrace> whileLoop C
  B (fst (hd l)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace>; valid_path C B (a # l)\<rbrakk> \<Longrightarrow> l \<noteq> [] \<longrightarrow> \<lbrace>\<lambda>s. s = snd a\<rbrace> whileLoop C
  B (fst a) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_path C B l \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd l)\<rbrace> whileLoop C
  B (fst (hd l)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace>; valid_path C B (a # l); l \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = snd a\<rbrace> whileLoop C
  B (fst a) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_path C B l \<Longrightarrow> \<lbrace>\<lambda>s. s = snd (hd l)\<rbrace> whileLoop C
  B (fst (hd l)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace>; valid_path C B (a # l); l \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = snd a\<rbrace> condition (C (fst a))
  (B (fst a) >>= whileLoop C
  B)
  (return (fst a)) \<exists>\<lbrace>\<lambda>r s. (r, s) = last l\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_path C B l \<Longrightarrow> last l \<in> fst (whileLoop C
  B (fst (hd l)) (snd (hd l))); valid_path C B (a # l); l \<noteq> []\<rbrakk> \<Longrightarrow> (C (fst a) (snd a) \<longrightarrow> (\<exists>x\<in>fst (B (fst a) (snd a)). case x of (r', s') \<Rightarrow> last l \<in> fst (whileLoop C
  B r' s'))) \<and> (\<not> C (fst a) (snd a) \<longrightarrow> last l = a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_path C B l \<Longrightarrow> last l \<in> fst (whileLoop C
  B (fst (hd l)) (snd (hd l))); valid_path C B (a # l); l \<noteq> []\<rbrakk> \<Longrightarrow> C (fst a) (snd a) \<longrightarrow> (\<exists>x\<in>fst (B (fst a) (snd a)). case x of (r', s') \<Rightarrow> last l \<in> fst (whileLoop C
  B r' s'))
 2. \<lbrakk>valid_path C B l \<Longrightarrow> last l \<in> fst (whileLoop C
  B (fst (hd l)) (snd (hd l))); valid_path C B (a # l); l \<noteq> []\<rbrakk> \<Longrightarrow> \<not> C (fst a) (snd a) \<longrightarrow> last l = a proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_path C B l \<Longrightarrow> last l \<in> fst (whileLoop C
  B (fst (hd l)) (snd (hd l))); valid_path C B (a # l); l \<noteq> []; C (fst a) (snd a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B (fst a) (snd a)). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> last l \<in> fst (whileLoop C
  B x1 x2)
 2. \<lbrakk>valid_path C B l \<Longrightarrow> last l \<in> fst (whileLoop C
  B (fst (hd l)) (snd (hd l))); valid_path C B (a # l); l \<noteq> []\<rbrakk> \<Longrightarrow> \<not> C (fst a) (snd a) \<longrightarrow> last l = a proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_path C B l \<Longrightarrow> last l \<in> fst (whileLoop C
  B (fst (hd l)) (snd (hd l))); valid_path C B (a # l); l \<noteq> []; C (fst a) (snd a); l = []\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B (fst a) (snd a)). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> last l \<in> fst (whileLoop C
  B x1 x2)
 2. \<And>aa list. \<lbrakk>valid_path C B l \<Longrightarrow> last l \<in> fst (whileLoop C
  B (fst (hd l)) (snd (hd l))); valid_path C B (a # l); l \<noteq> []; C (fst a) (snd a); l = aa # list\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B (fst a) (snd a)). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> last l \<in> fst (whileLoop C
  B x1 x2)
 3. \<lbrakk>valid_path C B l \<Longrightarrow> last l \<in> fst (whileLoop C
  B (fst (hd l)) (snd (hd l))); valid_path C B (a # l); l \<noteq> []\<rbrakk> \<Longrightarrow> \<not> C (fst a) (snd a) \<longrightarrow> last l = a proof (prove)
goal (2 subgoals):
 1. \<And>aa list. \<lbrakk>valid_path C B l \<Longrightarrow> last l \<in> fst (whileLoop C
  B (fst (hd l)) (snd (hd l))); valid_path C B (a # l); l \<noteq> []; C (fst a) (snd a); l = aa # list\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B (fst a) (snd a)). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> last l \<in> fst (whileLoop C
  B x1 x2)
 2. \<lbrakk>valid_path C B l \<Longrightarrow> last l \<in> fst (whileLoop C
  B (fst (hd l)) (snd (hd l))); valid_path C B (a # l); l \<noteq> []\<rbrakk> \<Longrightarrow> \<not> C (fst a) (snd a) \<longrightarrow> last l = a proof (prove)
goal (2 subgoals):
 1. \<And>aa b list. \<lbrakk>(if list = [] then (aa, b) else last list) \<in> fst (whileLoop C
  B aa b); C (fst a) (snd a); l = (aa, b) # list; (aa, b) \<in> fst (B (fst a) (snd a)); valid_path C B ((aa, b) # list)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B (fst a) (snd a)). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> (if list = [] then (aa, b) else last list) \<in> fst (whileLoop C
  B x1 x2)
 2. \<lbrakk>valid_path C B l \<Longrightarrow> last l \<in> fst (whileLoop C
  B (fst (hd l)) (snd (hd l))); valid_path C B (a # l); l \<noteq> []\<rbrakk> \<Longrightarrow> \<not> C (fst a) (snd a) \<longrightarrow> last l = a proof (prove)
goal (2 subgoals):
 1. \<And>aa b list. \<lbrakk>(if list = [] then (aa, b) else last list) \<in> fst (whileLoop C
  B aa b); C (fst a) (snd a); l = (aa, b) # list; valid_path C B ((aa, b) # list)\<rbrakk> \<Longrightarrow> \<forall>x1 x2. (aa, b) = (x1, x2) \<longrightarrow> (if list = [] then (aa, b) else last list) \<in> fst (whileLoop C
  B x1 x2)
 2. \<lbrakk>valid_path C B l \<Longrightarrow> last l \<in> fst (whileLoop C
  B (fst (hd l)) (snd (hd l))); valid_path C B (a # l); l \<noteq> []\<rbrakk> \<Longrightarrow> \<not> C (fst a) (snd a) \<longrightarrow> last l = a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_path C B l \<Longrightarrow> last l \<in> fst (whileLoop C
  B (fst (hd l)) (snd (hd l))); valid_path C B (a # l); l \<noteq> []\<rbrakk> \<Longrightarrow> \<not> C (fst a) (snd a) \<longrightarrow> last l = a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_path C B l \<Longrightarrow> last l \<in> fst (whileLoop C
  B (fst (hd l)) (snd (hd l))); valid_path C B (a # l); l \<noteq> []; \<not> C (fst a) (snd a)\<rbrakk> \<Longrightarrow> last l = a proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. s = snd (hd (a # l))\<rbrace> whileLoop C
  B (fst (hd (a # l))) \<exists>\<lbrace>\<lambda>r s. (r, s) = last (a # l)\<rbrace>

goal:
No subgoals!