theory Nondet_While_Loop_Rules

lemma valid_whileLoop:
  assumes first_step: "\<And>s. P r s \<Longrightarrow> I r s"
      and inv_step: "\<And>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<rbrace> B r \<lbrace> I \<rbrace>"
      and final_step: "\<And>r s. \<lbrakk> I r s; \<not> C r s \<rbrakk> \<Longrightarrow> Q r s"
  shows "\<lbrace> P r \<rbrace> whileLoop C B r \<lbrace> Q \<rbrace>" proof - { fix r' s' s assume inv: "I r s" assume step: "(r', s') \<in> fst (whileLoop C B r s)" have "I r' s'" using step inv apply (induct rule: in_whileLoop_induct) apply simp apply (drule use_valid, rule inv_step, auto) done } thus ?thesis apply (clarsimp simp: valid_def) apply (drule first_step) apply (rule final_step, simp) apply (metis fst_whileLoop_cond_false) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> proof (state)
this:
I r s

goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> proof (state)
this:
(r', s') \<in> fst (whileLoop C
  B r s)

goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. I r' s' proof (prove)
using this:
(r', s') \<in> fst (whileLoop C
  B r s)
I r s

goal (1 subgoal):
 1. I r' s' proof (prove)
goal (2 subgoals):
 1. \<And>r s. \<lbrakk>\<not> C r s; I r s\<rbrakk> \<Longrightarrow> I r s
 2. \<And>r s r' s' r'' s''. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (r'', s'') \<in> fst (whileLoop C
  B r' s'); I r' s' \<Longrightarrow> I r'' s''; I r s\<rbrakk> \<Longrightarrow> I r'' s'' proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s' r'' s''. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (r'', s'') \<in> fst (whileLoop C
  B r' s'); I r' s' \<Longrightarrow> I r'' s''; I r s\<rbrakk> \<Longrightarrow> I r'' s'' proof (prove)
goal:
No subgoals! proof (state)
this:
I r' s'

goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> proof (state)
this:
\<lbrakk>I r ?s2; (?r'2, ?s'2) \<in> fst (whileLoop C
  B r ?s2)\<rbrakk> \<Longrightarrow> I ?r'2 ?s'2

goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> proof (prove)
using this:
\<lbrakk>I r ?s2; (?r'2, ?s'2) \<in> fst (whileLoop C
  B r ?s2)\<rbrakk> \<Longrightarrow> I ?r'2 ?s'2

goal (1 subgoal):
 1. \<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>s r' s'. \<lbrakk>I r s; (r', s') \<in> fst (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> I r' s'; P r s; (a, b) \<in> fst (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>s r' s'. \<lbrakk>I r s; (r', s') \<in> fst (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> I r' s'; (a, b) \<in> fst (whileLoop C
  B r s); I r s\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>s r' s'. \<lbrakk>I r s; (r', s') \<in> fst (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> I r' s'; (a, b) \<in> fst (whileLoop C
  B r s); I r s\<rbrakk> \<Longrightarrow> \<not> C a b proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>P r\<rbrace> whileLoop C
  B r \<lbrace>Q\<rbrace>

goal:
No subgoals!