theory Nondet_While_Loop_Rules

lemma validE_whileLoopE:
  "\<lbrakk>\<And>s. P r s \<Longrightarrow> I r s;
    \<And>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<rbrace> B r \<lbrace> I \<rbrace>,\<lbrace> A \<rbrace>;
    \<And>r s. \<lbrakk> I r s; \<not> C r s \<rbrakk> \<Longrightarrow> Q r s\<rbrakk> \<Longrightarrow>
   \<lbrace> P r \<rbrace> whileLoopE C B r \<lbrace> Q \<rbrace>,\<lbrace> A \<rbrace>" apply (clarsimp simp: whileLoopE_def validE_def) apply (rule valid_whileLoop [where I="\<lambda>r s. (case r of Inl x \<Rightarrow> A x s | Inr x \<Rightarrow> I x s)"
                                 and Q="\<lambda>r s. (case r of Inl x \<Rightarrow> A x s | Inr x \<Rightarrow> Q x s)"]) apply atomize apply (clarsimp simp: valid_def lift_def split: sum.splits) apply (clarsimp simp: valid_def lift_def split: sum.splits) apply (clarsimp split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P r s \<Longrightarrow> I r s; \<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>, \<lbrace>A\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s\<rbrakk> \<Longrightarrow> \<lbrace>P r\<rbrace> whileLoopE C
  B r \<lbrace>Q\<rbrace>, \<lbrace>A\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P r s \<Longrightarrow> I r s; \<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> A e s | Inr r \<Rightarrow> I r s\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s\<rbrakk> \<Longrightarrow> \<lbrace>P r\<rbrace> whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) (Inr r) \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> A e s | Inr r \<Rightarrow> Q r s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>s. P r s \<Longrightarrow> I r s; \<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> A e s | Inr r \<Rightarrow> I r s\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s; P r s\<rbrakk> \<Longrightarrow> case Inr r of Inl e \<Rightarrow> A e s | Inr e \<Rightarrow> I e s
 2. \<And>v. \<lbrakk>\<And>s. P r s \<Longrightarrow> I r s; \<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> A e s | Inr r \<Rightarrow> I r s\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (case v of Inl e \<Rightarrow> A e s | Inr e \<Rightarrow> I e s) \<and> (case v of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)\<rbrace> lift B v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> A e s | Inr e \<Rightarrow> I e s\<rbrace>
 3. \<And>v s. \<lbrakk>\<And>s. P r s \<Longrightarrow> I r s; \<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> A e s | Inr r \<Rightarrow> I r s\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s; case v of Inl e \<Rightarrow> A e s | Inr e \<Rightarrow> I e s; \<not> (case v of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)\<rbrakk> \<Longrightarrow> case v of Inl e \<Rightarrow> A e s | Inr e \<Rightarrow> Q e s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<forall>s. P r s \<longrightarrow> I r s; \<forall>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> A e s | Inr r \<Rightarrow> I r s\<rbrace>; \<forall>r s. I r s \<longrightarrow> \<not> C r s \<longrightarrow> Q r s; P r s\<rbrakk> \<Longrightarrow> case Inr r of Inl e \<Rightarrow> A e s | Inr e \<Rightarrow> I e s
 2. \<And>v. \<lbrakk>\<And>s. P r s \<Longrightarrow> I r s; \<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> A e s | Inr r \<Rightarrow> I r s\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (case v of Inl e \<Rightarrow> A e s | Inr e \<Rightarrow> I e s) \<and> (case v of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)\<rbrace> lift B v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> A e s | Inr e \<Rightarrow> I e s\<rbrace>
 3. \<And>v s. \<lbrakk>\<And>s. P r s \<Longrightarrow> I r s; \<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> A e s | Inr r \<Rightarrow> I r s\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s; case v of Inl e \<Rightarrow> A e s | Inr e \<Rightarrow> I e s; \<not> (case v of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)\<rbrakk> \<Longrightarrow> case v of Inl e \<Rightarrow> A e s | Inr e \<Rightarrow> Q e s proof (prove)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>\<And>s. P r s \<Longrightarrow> I r s; \<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> A e s | Inr r \<Rightarrow> I r s\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (case v of Inl e \<Rightarrow> A e s | Inr e \<Rightarrow> I e s) \<and> (case v of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)\<rbrace> lift B v \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> A e s | Inr e \<Rightarrow> I e s\<rbrace>
 2. \<And>v s. \<lbrakk>\<And>s. P r s \<Longrightarrow> I r s; \<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> A e s | Inr r \<Rightarrow> I r s\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s; case v of Inl e \<Rightarrow> A e s | Inr e \<Rightarrow> I e s; \<not> (case v of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)\<rbrakk> \<Longrightarrow> case v of Inl e \<Rightarrow> A e s | Inr e \<Rightarrow> Q e s proof (prove)
goal (1 subgoal):
 1. \<And>v s. \<lbrakk>\<And>s. P r s \<Longrightarrow> I r s; \<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> A e s | Inr r \<Rightarrow> I r s\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s; case v of Inl e \<Rightarrow> A e s | Inr e \<Rightarrow> I e s; \<not> (case v of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)\<rbrakk> \<Longrightarrow> case v of Inl e \<Rightarrow> A e s | Inr e \<Rightarrow> Q e s proof (prove)
goal:
No subgoals!