theory Nondet_While_Loop_Rules_Completeness

lemma path_exists:
  assumes path: "\<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<exists>\<lbrace> Q \<rbrace>"
  shows "\<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l))" proof - { fix r' s' assume x: "(r', s') \<in> fst (whileLoop C B r s)" assume y: "Q r' s'" have ?thesis using x y proof (induct rule: in_whileLoop_induct) case (1 r s) then show ?case apply - apply (rule exI[where x="[(r,s)]"]) apply clarsimp done next case (2 r s r' s' r'' s'') then show ?case apply clarsimp apply (frule valid_path_not_empty) apply (rename_tac l) apply (rule_tac x="(r, s)#l" in exI) apply (clarsimp simp: neq_Nil_conv) done qed } thus ?thesis using path by (clarsimp simp: exs_valid_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (state)
goal (1 subgoal):
 1. \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (state)
goal (1 subgoal):
 1. \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (state)
goal (1 subgoal):
 1. \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (state)
this:
(r', s') \<in> fst (whileLoop C
  B r s)

goal (1 subgoal):
 1. \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (state)
this:
Q r' s'

goal (1 subgoal):
 1. \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (prove)
goal (1 subgoal):
 1. \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (prove)
using this:
(r', s') \<in> fst (whileLoop C
  B r s)
Q r' s'

goal (1 subgoal):
 1. \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (state)
goal (2 subgoals):
 1. \<And>r s. \<lbrakk>\<not> C r s; Q r s\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l))
 2. \<And>r s r' s' r'' s''. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (r'', s'') \<in> fst (whileLoop C
  B r' s'); Q r'' s'' \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r', s') \<and> Q (fst (last l)) (snd (last l)); Q r'' s''\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (state)
this:
\<not> C r s
Q r s

goal (2 subgoals):
 1. \<And>r s. \<lbrakk>\<not> C r s; Q r s\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l))
 2. \<And>r s r' s' r'' s''. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (r'', s'') \<in> fst (whileLoop C
  B r' s'); Q r'' s'' \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r', s') \<and> Q (fst (last l)) (snd (last l)); Q r'' s''\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (chain)
picking this:
\<not> C r s
Q r s proof (prove)
using this:
\<not> C r s
Q r s

goal (1 subgoal):
 1. \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> C r s; Q r s\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> C r s; Q r s\<rbrakk> \<Longrightarrow> valid_path C B [(r, s)] \<and> hd [(r, s)] = (r, s) \<and> Q (fst (last [(r, s)])) (snd (last [(r, s)])) proof (prove)
goal:
No subgoals! proof (state)
this:
\<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l))

goal (1 subgoal):
 1. \<And>r s r' s' r'' s''. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (r'', s'') \<in> fst (whileLoop C
  B r' s'); Q r'' s'' \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r', s') \<and> Q (fst (last l)) (snd (last l)); Q r'' s''\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (state)
goal (1 subgoal):
 1. \<And>r s r' s' r'' s''. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (r'', s'') \<in> fst (whileLoop C
  B r' s'); Q r'' s'' \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r', s') \<and> Q (fst (last l)) (snd (last l)); Q r'' s''\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (state)
this:
C r s
(r', s') \<in> fst (B r s)
(r'', s'') \<in> fst (whileLoop C
  B r' s')
Q r'' s'' \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r', s') \<and> Q (fst (last l)) (snd (last l))
Q r'' s''

goal (1 subgoal):
 1. \<And>r s r' s' r'' s''. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (r'', s'') \<in> fst (whileLoop C
  B r' s'); Q r'' s'' \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r', s') \<and> Q (fst (last l)) (snd (last l)); Q r'' s''\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (chain)
picking this:
C r s
(r', s') \<in> fst (B r s)
(r'', s'') \<in> fst (whileLoop C
  B r' s')
Q r'' s'' \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r', s') \<and> Q (fst (last l)) (snd (last l))
Q r'' s'' proof (prove)
using this:
C r s
(r', s') \<in> fst (B r s)
(r'', s'') \<in> fst (whileLoop C
  B r' s')
Q r'' s'' \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r', s') \<and> Q (fst (last l)) (snd (last l))
Q r'' s''

goal (1 subgoal):
 1. \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (r'', s'') \<in> fst (whileLoop C
  B r' s'); Q r'' s''; valid_path C B l; hd l = (r', s'); Q (fst (last l)) (snd (last l))\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (r'', s'') \<in> fst (whileLoop C
  B r' s'); Q r'' s''; valid_path C B l; hd l = (r', s'); Q (fst (last l)) (snd (last l)); l \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (r'', s'') \<in> fst (whileLoop C
  B r' s'); Q r'' s''; valid_path C B l; hd l = (r', s'); Q (fst (last l)) (snd (last l)); l \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (r'', s'') \<in> fst (whileLoop C
  B r' s'); Q r'' s''; valid_path C B l; hd l = (r', s'); Q (fst (last l)) (snd (last l)); l \<noteq> []\<rbrakk> \<Longrightarrow> valid_path C B ((r, s) # l) \<and> hd ((r, s) # l) = (r, s) \<and> Q (fst (last ((r, s) # l))) (snd (last ((r, s) # l))) proof (prove)
goal:
No subgoals! proof (state)
this:
\<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l))

goal:
No subgoals! proof (state)
this:
\<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l))

goal (1 subgoal):
 1. \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (state)
this:
\<lbrakk>(?r'2, ?s'2) \<in> fst (whileLoop C
  B r s); Q ?r'2 ?s'2\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l))

goal (1 subgoal):
 1. \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (prove)
using this:
\<lbrakk>(?r'2, ?s'2) \<in> fst (whileLoop C
  B r s); Q ?r'2 ?s'2\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l))

goal (1 subgoal):
 1. \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (prove)
using this:
\<lbrakk>(?r'2, ?s'2) \<in> fst (whileLoop C
  B r s); Q ?r'2 ?s'2\<rbrakk> \<Longrightarrow> \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l))
\<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>Q\<rbrace>

goal (1 subgoal):
 1. \<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l)) proof (state)
this:
\<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l))

goal:
No subgoals!