theory Nondet_While_Loop_Rules

lemma whileLoop_terminates_results:
  assumes non_term: "\<And>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>"
  shows
    "\<lbrakk>whileLoop_terminates C B r s; (Some (r, s), None) \<notin> whileLoop_results C B; I r s; C r s\<rbrakk>
     \<Longrightarrow> False" proof (induct rule: whileLoop_terminates.induct) case (1 r s) then show ?case apply clarsimp done next case (2 r s) then show ?case apply (cut_tac non_term[where r=r]) apply (clarsimp simp: exs_valid_def) apply (subst (asm) (2) whileLoop_results.simps) apply clarsimp apply (insert whileLoop_results.simps) apply fast done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>whileLoop_terminates C B r s; (Some (r, s), None) \<notin> whileLoop_results C B; I r s; C r s\<rbrakk> \<Longrightarrow> False proof (state)
goal (2 subgoals):
 1. \<And>r s. \<lbrakk>\<not> C r s; (Some (r, s), None) \<notin> whileLoop_results C B; I r s; C r s\<rbrakk> \<Longrightarrow> False
 2. \<And>r s. \<lbrakk>C r s; \<forall>(r', s')\<in>fst (B r s). whileLoop_terminates C B r' s' \<and> ((Some (r', s'), None) \<notin> whileLoop_results C B \<longrightarrow> I r' s' \<longrightarrow> C r' s' \<longrightarrow> False); (Some (r, s), None) \<notin> whileLoop_results C B; I r s; C r s\<rbrakk> \<Longrightarrow> False proof (state)
this:
\<not> C r s
(Some (r, s), None) \<notin> whileLoop_results C B
I r s
C r s

goal (2 subgoals):
 1. \<And>r s. \<lbrakk>\<not> C r s; (Some (r, s), None) \<notin> whileLoop_results C B; I r s; C r s\<rbrakk> \<Longrightarrow> False
 2. \<And>r s. \<lbrakk>C r s; \<forall>(r', s')\<in>fst (B r s). whileLoop_terminates C B r' s' \<and> ((Some (r', s'), None) \<notin> whileLoop_results C B \<longrightarrow> I r' s' \<longrightarrow> C r' s' \<longrightarrow> False); (Some (r, s), None) \<notin> whileLoop_results C B; I r s; C r s\<rbrakk> \<Longrightarrow> False proof (chain)
picking this:
\<not> C r s
(Some (r, s), None) \<notin> whileLoop_results C B
I r s
C r s proof (prove)
using this:
\<not> C r s
(Some (r, s), None) \<notin> whileLoop_results C B
I r s
C r s

goal (1 subgoal):
 1. False proof (prove)
goal:
No subgoals! proof (state)
this:
False

goal (1 subgoal):
 1. \<And>r s. \<lbrakk>C r s; \<forall>(r', s')\<in>fst (B r s). whileLoop_terminates C B r' s' \<and> ((Some (r', s'), None) \<notin> whileLoop_results C B \<longrightarrow> I r' s' \<longrightarrow> C r' s' \<longrightarrow> False); (Some (r, s), None) \<notin> whileLoop_results C B; I r s; C r s\<rbrakk> \<Longrightarrow> False proof (state)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>C r s; \<forall>(r', s')\<in>fst (B r s). whileLoop_terminates C B r' s' \<and> ((Some (r', s'), None) \<notin> whileLoop_results C B \<longrightarrow> I r' s' \<longrightarrow> C r' s' \<longrightarrow> False); (Some (r, s), None) \<notin> whileLoop_results C B; I r s; C r s\<rbrakk> \<Longrightarrow> False proof (state)
this:
C r s
\<forall>(r', s')\<in>fst (B r s). whileLoop_terminates C B r' s' \<and> ((Some (r', s'), None) \<notin> whileLoop_results C B \<longrightarrow> I r' s' \<longrightarrow> C r' s' \<longrightarrow> False)
(Some (r, s), None) \<notin> whileLoop_results C B
I r s
C r s

goal (1 subgoal):
 1. \<And>r s. \<lbrakk>C r s; \<forall>(r', s')\<in>fst (B r s). whileLoop_terminates C B r' s' \<and> ((Some (r', s'), None) \<notin> whileLoop_results C B \<longrightarrow> I r' s' \<longrightarrow> C r' s' \<longrightarrow> False); (Some (r, s), None) \<notin> whileLoop_results C B; I r s; C r s\<rbrakk> \<Longrightarrow> False proof (chain)
picking this:
C r s
\<forall>(r', s')\<in>fst (B r s). whileLoop_terminates C B r' s' \<and> ((Some (r', s'), None) \<notin> whileLoop_results C B \<longrightarrow> I r' s' \<longrightarrow> C r' s' \<longrightarrow> False)
(Some (r, s), None) \<notin> whileLoop_results C B
I r s
C r s proof (prove)
using this:
C r s
\<forall>(r', s')\<in>fst (B r s). whileLoop_terminates C B r' s' \<and> ((Some (r', s'), None) \<notin> whileLoop_results C B \<longrightarrow> I r' s' \<longrightarrow> C r' s' \<longrightarrow> False)
(Some (r, s), None) \<notin> whileLoop_results C B
I r s
C r s

goal (1 subgoal):
 1. False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C r s; \<forall>(r', s')\<in>fst (B r s). whileLoop_terminates C B r' s' \<and> ((Some (r', s'), None) \<notin> whileLoop_results C B \<longrightarrow> I r' s' \<longrightarrow> C r' s' \<longrightarrow> False); (Some (r, s), None) \<notin> whileLoop_results C B; I r s; C r s; \<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> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>fst (B r s). case x of (r', s') \<Rightarrow> whileLoop_terminates C B r' s' \<and> ((Some (r', s'), None) \<notin> whileLoop_results C B \<longrightarrow> I r' s' \<longrightarrow> \<not> C r' s'); (Some (r, s), None) \<notin> whileLoop_results C B; I r s; C r s; \<forall>s. I r s \<and> C r s \<and> \<not> snd (B r s) \<longrightarrow> (\<exists>x\<in>fst (B r s). case x of (rv, s') \<Rightarrow> C rv s' \<and> I rv s')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>fst (B r s). case x of (r', s') \<Rightarrow> whileLoop_terminates C B r' s' \<and> ((Some (r', s'), None) \<notin> whileLoop_results C B \<longrightarrow> I r' s' \<longrightarrow> \<not> C r' s'); \<not> ((\<exists>r s. Some (r, s) = Some (r, s) \<and> None = Some (r, s) \<and> \<not> C r s) \<or> (\<exists>r s. Some (r, s) = Some (r, s) \<and> None = None \<and> C r s \<and> snd (B r s)) \<or> (\<exists>r s r' s' z. Some (r, s) = Some (r, s) \<and> None = z \<and> C r s \<and> (r', s') \<in> fst (B r s) \<and> (Some (r', s'), z) \<in> whileLoop_results C B)); I r s; C r s; \<forall>s. I r s \<and> C r s \<and> \<not> snd (B r s) \<longrightarrow> (\<exists>x\<in>fst (B r s). case x of (rv, s') \<Rightarrow> C rv s' \<and> I rv s')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>fst (B r s). case x of (r', s') \<Rightarrow> whileLoop_terminates C B r' s' \<and> ((Some (r', s'), None) \<notin> whileLoop_results C B \<longrightarrow> I r' s' \<longrightarrow> \<not> C r' s'); I r s; C r s; \<forall>s. I r s \<and> C r s \<and> \<not> snd (B r s) \<longrightarrow> (\<exists>x\<in>fst (B r s). case x of (rv, s') \<Rightarrow> C rv s' \<and> I rv s'); \<not> snd (B r s); \<forall>r' s'. (r', s') \<in> fst (B r s) \<longrightarrow> (Some (r', s'), None) \<notin> whileLoop_results C B\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>fst (B r s). case x of (r', s') \<Rightarrow> whileLoop_terminates C B r' s' \<and> ((Some (r', s'), None) \<notin> whileLoop_results C B \<longrightarrow> I r' s' \<longrightarrow> \<not> C r' s'); I r s; C r s; \<forall>s. I r s \<and> C r s \<and> \<not> snd (B r s) \<longrightarrow> (\<exists>x\<in>fst (B r s). case x of (rv, s') \<Rightarrow> C rv s' \<and> I rv s'); \<not> snd (B r s); \<forall>r' s'. (r', s') \<in> fst (B r s) \<longrightarrow> (Some (r', s'), None) \<notin> whileLoop_results C B; \<And>a1 a2 C B. ((a1, a2) \<in> whileLoop_results C B) = ((\<exists>r s. a1 = Some (r, s) \<and> a2 = Some (r, s) \<and> \<not> C r s) \<or> (\<exists>r s. a1 = Some (r, s) \<and> a2 = None \<and> C r s \<and> snd (B r s)) \<or> (\<exists>r s r' s' z. a1 = Some (r, s) \<and> a2 = z \<and> C r s \<and> (r', s') \<in> fst (B r s) \<and> (Some (r', s'), z) \<in> whileLoop_results C B))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
False

goal:
No subgoals!