theory Nondet_While_Loop_Rules

lemma whileLoop_terminates_inv:
  assumes init_I: "I r s"
  assumes inv: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<and> ((r', s'), (r, s)) \<in> R \<rbrace>"
  assumes wf_R: "wf R"
  shows "whileLoop_terminates C B r s" apply (insert init_I) using wf_R apply (induction "(r, s)" arbitrary: r s) apply atomize apply (subst whileLoop_terminates_simps) apply clarsimp apply (erule use_valid) apply (rule hoare_strengthen_post, rule inv) apply force apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whileLoop_terminates C B r s proof (prove)
goal (1 subgoal):
 1. I r s \<Longrightarrow> whileLoop_terminates C B r s proof (prove)
using this:
wf R

goal (1 subgoal):
 1. I r s \<Longrightarrow> whileLoop_terminates C B r s proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>\<And>ra sa. \<lbrakk>((ra, sa), r, s) \<in> R; I ra sa\<rbrakk> \<Longrightarrow> whileLoop_terminates C B ra sa; I r s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r s proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>\<forall>ra sa. ((ra, sa), r, s) \<in> R \<longrightarrow> I ra sa \<longrightarrow> whileLoop_terminates C B ra sa; I r s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r s proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>\<forall>ra sa. ((ra, sa), r, s) \<in> R \<longrightarrow> I ra sa \<longrightarrow> whileLoop_terminates C B ra sa; I r s\<rbrakk> \<Longrightarrow> C r s \<longrightarrow> (\<forall>(x, y)\<in>fst (B r s). whileLoop_terminates C B x y) proof (prove)
goal (1 subgoal):
 1. \<And>r s a b. \<lbrakk>\<forall>ra sa. ((ra, sa), r, s) \<in> R \<longrightarrow> I ra sa \<longrightarrow> whileLoop_terminates C B ra sa; I r s; C r s; (a, b) \<in> fst (B r s)\<rbrakk> \<Longrightarrow> whileLoop_terminates C B a b proof (prove)
goal (2 subgoals):
 1. \<And>r s a b. \<lbrakk>\<forall>ra sa. ((ra, sa), r, s) \<in> R \<longrightarrow> I ra sa \<longrightarrow> whileLoop_terminates C B ra sa; I r s; C r s\<rbrakk> \<Longrightarrow> \<lbrace>?P11 r s a b\<rbrace> B r \<lbrace>whileLoop_terminates C B\<rbrace>
 2. \<And>r s a b. \<lbrakk>\<forall>ra sa. ((ra, sa), r, s) \<in> R \<longrightarrow> I ra sa \<longrightarrow> whileLoop_terminates C B ra sa; I r s; C r s\<rbrakk> \<Longrightarrow> ?P11 r s a b s proof (prove)
goal (2 subgoals):
 1. \<And>r s a b rv sa. \<lbrakk>\<forall>ra sa. ((ra, sa), r, s) \<in> R \<longrightarrow> I ra sa \<longrightarrow> whileLoop_terminates C B ra sa; I r s; C r s; I rv sa \<and> ((rv, sa), r, ?s17 r s a b) \<in> R\<rbrakk> \<Longrightarrow> whileLoop_terminates C B rv sa
 2. \<And>r s a b. \<lbrakk>\<forall>ra sa. ((ra, sa), r, s) \<in> R \<longrightarrow> I ra sa \<longrightarrow> whileLoop_terminates C B ra sa; I r s; C r s\<rbrakk> \<Longrightarrow> I r s \<and> C r s \<and> s = ?s17 r s a b proof (prove)
goal (1 subgoal):
 1. \<And>r s a b. \<lbrakk>\<forall>ra sa. ((ra, sa), r, s) \<in> R \<longrightarrow> I ra sa \<longrightarrow> whileLoop_terminates C B ra sa; I r s; C r s\<rbrakk> \<Longrightarrow> I r s \<and> C r s \<and> s = s proof (prove)
goal:
No subgoals!