theory Nondet_While_Loop_Rules

lemma empty_fail_whileLoop[empty_fail_cond, intro!, wp]:
  assumes body_empty_fail: "\<And>r. empty_fail (B r)"
  shows "empty_fail (whileLoop C B r)" proof - { fix s A assume empty: "fst (whileLoop C B r s) = {}" have cond_true: "\<And>x s. fst (whileLoop C B x s) = {} \<Longrightarrow> C x s" apply (subst (asm) whileLoop_unroll) apply (clarsimp simp: condition_def return_def split: if_split_asm) done have  "snd (whileLoop C B r s)" apply (rule snd_whileLoop [where I="\<lambda>x s. fst (whileLoop C B x s) = {}"]) apply fact apply (rule cond_true, fact) apply (clarsimp simp: exs_valid_def) apply (drule empty_failD3[OF body_empty_fail]) apply (subst (asm) whileLoop_unroll) apply (fastforce simp: condition_def bind_def split_def cond_true) done } thus ?thesis by (clarsimp simp: empty_fail_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (whileLoop C
  B r) proof (state)
goal (1 subgoal):
 1. empty_fail (whileLoop C
  B r) proof (state)
goal (1 subgoal):
 1. empty_fail (whileLoop C
  B r) proof (state)
goal (1 subgoal):
 1. empty_fail (whileLoop C
  B r) proof (state)
this:
fst (whileLoop C
  B r s) = {}

goal (1 subgoal):
 1. empty_fail (whileLoop C
  B r) proof (prove)
goal (1 subgoal):
 1. \<And>x s. fst (whileLoop C
  B x s) = {} \<Longrightarrow> C x s proof (prove)
goal (1 subgoal):
 1. \<And>x s. fst (condition (C x)
  (B x >>= whileLoop C
  B)
  (return x) s) = {} \<Longrightarrow> C x s proof (prove)
goal:
No subgoals! proof (state)
this:
fst (whileLoop C
  B ?x ?s) = {} \<Longrightarrow> C ?x ?s

goal (1 subgoal):
 1. empty_fail (whileLoop C
  B r) proof (prove)
goal (1 subgoal):
 1. snd (whileLoop C
  B r s) proof (prove)
goal (3 subgoals):
 1. fst (whileLoop C
  B r s) = {}
 2. C r s
 3. \<And>r. \<lbrace>\<lambda>s. fst (whileLoop 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> fst (whileLoop C
  B r' s') = {}\<rbrace> proof (prove)
goal (2 subgoals):
 1. C r s
 2. \<And>r. \<lbrace>\<lambda>s. fst (whileLoop 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> fst (whileLoop C
  B r' s') = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrace>\<lambda>s. fst (whileLoop 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> fst (whileLoop C
  B r' s') = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>fst (whileLoop C
  B r s) = {}; C r s; \<not> snd (B r s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B r s). case x of (rv, s') \<Rightarrow> C rv s' \<and> fst (whileLoop C
  B rv s') = {} proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>fst (whileLoop C
  B r s) = {}; C r s; fst (B r s) \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B r s). case x of (rv, s') \<Rightarrow> C rv s' \<and> fst (whileLoop C
  B rv s') = {} proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>fst (condition (C r)
  (B r >>= whileLoop C
  B)
  (return r) s) = {}; C r s; fst (B r s) \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B r s). case x of (rv, s') \<Rightarrow> C rv s' \<and> fst (whileLoop C
  B rv s') = {} proof (prove)
goal:
No subgoals! proof (state)
this:
snd (whileLoop C
  B r s)

goal (1 subgoal):
 1. empty_fail (whileLoop C
  B r) proof (state)
this:
fst (whileLoop C
  B r ?s2) = {} \<Longrightarrow> snd (whileLoop C
  B r ?s2)

goal (1 subgoal):
 1. empty_fail (whileLoop C
  B r) proof (prove)
using this:
fst (whileLoop C
  B r ?s2) = {} \<Longrightarrow> snd (whileLoop C
  B r ?s2)

goal (1 subgoal):
 1. empty_fail (whileLoop C
  B r) proof (state)
this:
empty_fail (whileLoop C
  B r)

goal:
No subgoals!