theory Nondet_While_Loop_Rules

lemma not_snd_whileLoop:
  assumes init_I: "I r s"
      and inv_holds: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<and> ((r', s'), (r, s)) \<in> R \<rbrace>!"
      and wf_R: "wf R"
  shows "\<not> snd (whileLoop C B r s)" proof - { fix x y have "\<lbrakk> (x, y) \<in> whileLoop_results C B; x = Some (r, s); y = None \<rbrakk> \<Longrightarrow> False" apply (insert init_I) apply (induct arbitrary: r s rule: whileLoop_results.inducts) apply simp apply simp apply (insert validNF_not_failed[OF inv_holds])[1] apply blast apply (drule use_validNF [OF _ inv_holds]) apply simp apply clarsimp done } also have "whileLoop_terminates C B r s" apply (rule whileLoop_terminates_inv [where I=I, OF init_I _ wf_R]) apply (insert inv_holds) apply (clarsimp simp: validNF_def) done ultimately show ?thesis by (clarsimp simp: whileLoop_def, blast) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) proof (state)
goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) proof (state)
goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) proof (state)
goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, y) \<in> whileLoop_results C B; x = Some (r, s); y = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, y) \<in> whileLoop_results C B; x = Some (r, s); y = None; I r s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>r s ra sa. \<lbrakk>\<not> C r s; Some (r, s) = Some (ra, sa); Some (r, s) = None; I ra sa\<rbrakk> \<Longrightarrow> False
 2. \<And>r s ra sa. \<lbrakk>C r s; snd (B r s); Some (r, s) = Some (ra, sa); None = None; I ra sa\<rbrakk> \<Longrightarrow> False
 3. \<And>r s r' s' z ra sa. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; \<And>r s. \<lbrakk>Some (r', s') = Some (r, s); z = None; I r s\<rbrakk> \<Longrightarrow> False; Some (r, s) = Some (ra, sa); z = None; I ra sa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>r s ra sa. \<lbrakk>C r s; snd (B r s); Some (r, s) = Some (ra, sa); None = None; I ra sa\<rbrakk> \<Longrightarrow> False
 2. \<And>r s r' s' z ra sa. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; \<And>r s. \<lbrakk>Some (r', s') = Some (r, s); z = None; I r s\<rbrakk> \<Longrightarrow> False; Some (r, s) = Some (ra, sa); z = None; I ra sa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>r s ra. \<lbrakk>C ra s; snd (B ra s); r = ra; I ra s\<rbrakk> \<Longrightarrow> False
 2. \<And>r s r' s' z ra sa. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; \<And>r s. \<lbrakk>Some (r', s') = Some (r, s); z = None; I r s\<rbrakk> \<Longrightarrow> False; Some (r, s) = Some (ra, sa); z = None; I ra sa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>r s ra. \<lbrakk>C ra s; snd (B ra s); r = ra; I ra s; \<And>r s sa. I r s \<and> C r s \<and> s = sa \<Longrightarrow> \<not> snd (B r s)\<rbrakk> \<Longrightarrow> False
 2. \<And>r s r' s' z ra sa. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; \<And>r s. \<lbrakk>Some (r', s') = Some (r, s); z = None; I r s\<rbrakk> \<Longrightarrow> False; Some (r, s) = Some (ra, sa); z = None; I ra sa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s' z ra sa. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; \<And>r s. \<lbrakk>Some (r', s') = Some (r, s); z = None; I r s\<rbrakk> \<Longrightarrow> False; Some (r, s) = Some (ra, sa); z = None; I ra sa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>r s r' s' z ra sa. \<lbrakk>C r s; (Some (r', s'), z) \<in> whileLoop_results C B; \<And>r s. \<lbrakk>Some (r', s') = Some (r, s); z = None; I r s\<rbrakk> \<Longrightarrow> False; Some (r, s) = Some (ra, sa); z = None; I ra sa\<rbrakk> \<Longrightarrow> I r s \<and> C r s \<and> s = ?sa28 r s r' s' z ra sa
 2. \<And>r s r' s' z ra sa. \<lbrakk>C r s; (Some (r', s'), z) \<in> whileLoop_results C B; \<And>r s. \<lbrakk>Some (r', s') = Some (r, s); z = None; I r s\<rbrakk> \<Longrightarrow> False; Some (r, s) = Some (ra, sa); z = None; I ra sa; I r' s' \<and> ((r', s'), r, ?sa28 r s r' s' z ra sa) \<in> R\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s' z ra sa. \<lbrakk>C r s; (Some (r', s'), z) \<in> whileLoop_results C B; \<And>r s. \<lbrakk>Some (r', s') = Some (r, s); z = None; I r s\<rbrakk> \<Longrightarrow> False; Some (r, s) = Some (ra, sa); z = None; I ra sa; I r' s' \<and> ((r', s'), r, sa) \<in> R\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>(x, y) \<in> whileLoop_results C B; x = Some (r, s); y = None\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) proof (state)
this:
\<lbrakk>(?x2, ?y2) \<in> whileLoop_results C B; ?x2 = Some (r, s); ?y2 = None\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) proof (state)
this:
\<lbrakk>(?x2, ?y2) \<in> whileLoop_results C B; ?x2 = Some (r, s); ?y2 = None\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) proof (prove)
goal (1 subgoal):
 1. whileLoop_terminates C B r s proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>r s. (\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!) \<Longrightarrow> \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
whileLoop_terminates C B r s

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) proof (chain)
picking this:
\<lbrakk>(?x2, ?y2) \<in> whileLoop_results C B; ?x2 = Some (r, s); ?y2 = None\<rbrakk> \<Longrightarrow> False
whileLoop_terminates C B r s proof (prove)
using this:
\<lbrakk>(?x2, ?y2) \<in> whileLoop_results C B; ?x2 = Some (r, s); ?y2 = None\<rbrakk> \<Longrightarrow> False
whileLoop_terminates C B r s

goal (1 subgoal):
 1. \<not> snd (whileLoop C
  B r s) proof (state)
this:
\<not> snd (whileLoop C
  B r s)

goal:
No subgoals!