theory Reader_Option_VCG

lemma owhile_NF[wp]:
  "\<lbrakk>\<And>a. ovalidNF (\<lambda>s. I a s \<and> C a s) (B a) I;
    \<And>a m. ovalid (\<lambda>s. I a s \<and> C a s \<and> M a s = m) (B a) (\<lambda>r s. M r s < m);
    \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s\<rbrakk>
   \<Longrightarrow> ovalidNF (I a) (owhile_inv C B a I M) Q" unfolding owhile_inv_def ovalidNF_def ovalid_def apply clarify apply (rule owhile_rule[where I = I and M = "measure (\<lambda>r. M r s)" and s = s for s]) apply fastforce apply fastforce apply fastforce apply blast+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. ovalidNF (\<lambda>s. I a s \<and> C a s) (B a) I; \<And>a m. \<lblot>\<lambda>s. I a s \<and> C a s \<and> M a s = m\<rblot> B a \<lblot>\<lambda>r s. M r s < m\<rblot>; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s\<rbrakk> \<Longrightarrow> ovalidNF (I a) (owhile_inv C B a I M) Q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s\<rbrakk> \<Longrightarrow> \<forall>s. I a s \<longrightarrow> owhile C B a s \<noteq> None \<and> (\<forall>r. owhile C B a s = Some r \<longrightarrow> Q r s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s\<rbrakk> \<Longrightarrow> owhile C B a s \<noteq> None \<and> (\<forall>r. owhile C B a s = Some r \<longrightarrow> Q r s) proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s\<rbrakk> \<Longrightarrow> I a s
 2. \<And>s. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s\<rbrakk> \<Longrightarrow> wf (measure (\<lambda>r. M r s))
 3. \<And>s r r'. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; I r s; C r s; B r s = Some r'\<rbrakk> \<Longrightarrow> (r', r) \<in> measure (\<lambda>r. M r s)
 4. \<And>s r r'. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; I r s; C r s; B r s = Some r'\<rbrakk> \<Longrightarrow> I r' s
 5. \<And>s r. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; I r s; C r s; B r s = None\<rbrakk> \<Longrightarrow> None \<noteq> None \<and> (\<forall>r. None = Some r \<longrightarrow> Q r s)
 6. \<And>s r. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Some r \<noteq> None \<and> (\<forall>ra. Some r = Some ra \<longrightarrow> Q ra s) proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s\<rbrakk> \<Longrightarrow> wf (measure (\<lambda>r. M r s))
 2. \<And>s r r'. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; I r s; C r s; B r s = Some r'\<rbrakk> \<Longrightarrow> (r', r) \<in> measure (\<lambda>r. M r s)
 3. \<And>s r r'. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; I r s; C r s; B r s = Some r'\<rbrakk> \<Longrightarrow> I r' s
 4. \<And>s r. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; I r s; C r s; B r s = None\<rbrakk> \<Longrightarrow> None \<noteq> None \<and> (\<forall>r. None = Some r \<longrightarrow> Q r s)
 5. \<And>s r. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Some r \<noteq> None \<and> (\<forall>ra. Some r = Some ra \<longrightarrow> Q ra s) proof (prove)
goal (4 subgoals):
 1. \<And>s r r'. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; I r s; C r s; B r s = Some r'\<rbrakk> \<Longrightarrow> (r', r) \<in> measure (\<lambda>r. M r s)
 2. \<And>s r r'. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; I r s; C r s; B r s = Some r'\<rbrakk> \<Longrightarrow> I r' s
 3. \<And>s r. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; I r s; C r s; B r s = None\<rbrakk> \<Longrightarrow> None \<noteq> None \<and> (\<forall>r. None = Some r \<longrightarrow> Q r s)
 4. \<And>s r. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Some r \<noteq> None \<and> (\<forall>ra. Some r = Some ra \<longrightarrow> Q ra s) proof (prove)
goal (3 subgoals):
 1. \<And>s r r'. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; I r s; C r s; B r s = Some r'\<rbrakk> \<Longrightarrow> I r' s
 2. \<And>s r. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; I r s; C r s; B r s = None\<rbrakk> \<Longrightarrow> None \<noteq> None \<and> (\<forall>r. None = Some r \<longrightarrow> Q r s)
 3. \<And>s r. \<lbrakk>\<And>a. \<forall>s. I a s \<and> C a s \<longrightarrow> B a s \<noteq> None \<and> (\<forall>r. B a s = Some r \<longrightarrow> I r s); \<And>a m. \<forall>s r. (I a s \<and> C a s \<and> M a s = m) \<and> B a s = Some r \<longrightarrow> M r s < m; \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s; I a s; I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Some r \<noteq> None \<and> (\<forall>ra. Some r = Some ra \<longrightarrow> Q ra s) proof (prove)
goal:
No subgoals!