theory Nondet_While_Loop_Rules

lemma whileLoop_terminates_cong [cong]:
  assumes r: "r = r'"
  and s: "s = s'"
  and C: "\<And>r s. C r s = C' r s"
  and B: "\<And>r s. C' r s \<Longrightarrow> B r s = B' r s"
  shows "whileLoop_terminates C B r s = whileLoop_terminates C' B' r' s'" proof (rule iffI) assume T: "whileLoop_terminates C B r s" show "whileLoop_terminates C' B' r' s'" apply (insert T r s) apply (induct arbitrary: r' s' rule: whileLoop_terminates.induct) apply (clarsimp simp: C) apply (erule whileLoop_terminates.intros) apply (clarsimp simp: C B split: prod.splits) apply (rule whileLoop_terminates.intros, assumption) apply (clarsimp simp: C B split: prod.splits) done next assume T: "whileLoop_terminates C' B' r' s'" show "whileLoop_terminates C B r s" apply (insert T r s) apply (induct arbitrary: r s rule: whileLoop_terminates.induct) apply (rule whileLoop_terminates.intros) apply (clarsimp simp: C) apply (rule whileLoop_terminates.intros, fastforce simp: C) apply (clarsimp simp: C B split: prod.splits) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whileLoop_terminates C B r s = whileLoop_terminates C' B' r' s' proof (state)
goal (2 subgoals):
 1. whileLoop_terminates C B r s \<Longrightarrow> whileLoop_terminates C' B' r' s'
 2. whileLoop_terminates C' B' r' s' \<Longrightarrow> whileLoop_terminates C B r s proof (state)
this:
whileLoop_terminates C B r s

goal (2 subgoals):
 1. whileLoop_terminates C B r s \<Longrightarrow> whileLoop_terminates C' B' r' s'
 2. whileLoop_terminates C' B' r' s' \<Longrightarrow> whileLoop_terminates C B r s proof (prove)
goal (1 subgoal):
 1. whileLoop_terminates C' B' r' s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>whileLoop_terminates C B r s; r = r'; s = s'\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r' s' proof (prove)
goal (2 subgoals):
 1. \<And>r s r' s'. \<lbrakk>\<not> C r s; r = r'; s = s'\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r' s'
 2. \<And>r s r' s'. \<lbrakk>C r s; \<forall>(r', s')\<in>fst (B r s). whileLoop_terminates C B r' s' \<and> (\<forall>x. r' = x \<longrightarrow> (\<forall>xa. s' = xa \<longrightarrow> whileLoop_terminates C' B' x xa)); r = r'; s = s'\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r' s' proof (prove)
goal (2 subgoals):
 1. \<And>r' s'. \<not> C' r' s' \<Longrightarrow> whileLoop_terminates C' B' r' s'
 2. \<And>r s r' s'. \<lbrakk>C r s; \<forall>(r', s')\<in>fst (B r s). whileLoop_terminates C B r' s' \<and> (\<forall>x. r' = x \<longrightarrow> (\<forall>xa. s' = xa \<longrightarrow> whileLoop_terminates C' B' x xa)); r = r'; s = s'\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r' s' proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s'. \<lbrakk>C r s; \<forall>(r', s')\<in>fst (B r s). whileLoop_terminates C B r' s' \<and> (\<forall>x. r' = x \<longrightarrow> (\<forall>xa. s' = xa \<longrightarrow> whileLoop_terminates C' B' x xa)); r = r'; s = s'\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r' s' proof (prove)
goal (1 subgoal):
 1. \<And>r' s'. \<lbrakk>\<forall>x\<in>fst (B' r' s'). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> whileLoop_terminates C' B x1 x2 \<and> whileLoop_terminates C' B' x1 x2; C' r' s'\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r' s' proof (prove)
goal (1 subgoal):
 1. \<And>r' s'. \<lbrakk>\<forall>x\<in>fst (B' r' s'). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> whileLoop_terminates C' B x1 x2 \<and> whileLoop_terminates C' B' x1 x2; C' r' s'\<rbrakk> \<Longrightarrow> \<forall>(r', s')\<in>fst (B' r' s'). whileLoop_terminates C' B' r' s' proof (prove)
goal:
No subgoals! proof (state)
this:
whileLoop_terminates C' B' r' s'

goal (1 subgoal):
 1. whileLoop_terminates C' B' r' s' \<Longrightarrow> whileLoop_terminates C B r s proof (state)
goal (1 subgoal):
 1. whileLoop_terminates C' B' r' s' \<Longrightarrow> whileLoop_terminates C B r s proof (state)
this:
whileLoop_terminates C' B' r' s'

goal (1 subgoal):
 1. whileLoop_terminates C' B' r' s' \<Longrightarrow> whileLoop_terminates C B r s proof (prove)
goal (1 subgoal):
 1. whileLoop_terminates C B r s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>whileLoop_terminates C' B' r' s'; r = r'; s = s'\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r s proof (prove)
goal (2 subgoals):
 1. \<And>r s ra sa. \<lbrakk>\<not> C' r s; ra = r; sa = s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B ra sa
 2. \<And>r s ra sa. \<lbrakk>C' r s; \<forall>(r', s')\<in>fst (B' r s). whileLoop_terminates C' B' r' s' \<and> (\<forall>x. x = r' \<longrightarrow> (\<forall>xa. xa = s' \<longrightarrow> whileLoop_terminates C B x xa)); ra = r; sa = s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B ra sa proof (prove)
goal (2 subgoals):
 1. \<And>r s ra sa. \<lbrakk>\<not> C' r s; ra = r; sa = s\<rbrakk> \<Longrightarrow> \<not> C ra sa
 2. \<And>r s ra sa. \<lbrakk>C' r s; \<forall>(r', s')\<in>fst (B' r s). whileLoop_terminates C' B' r' s' \<and> (\<forall>x. x = r' \<longrightarrow> (\<forall>xa. xa = s' \<longrightarrow> whileLoop_terminates C B x xa)); ra = r; sa = s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B ra sa proof (prove)
goal (1 subgoal):
 1. \<And>r s ra sa. \<lbrakk>C' r s; \<forall>(r', s')\<in>fst (B' r s). whileLoop_terminates C' B' r' s' \<and> (\<forall>x. x = r' \<longrightarrow> (\<forall>xa. xa = s' \<longrightarrow> whileLoop_terminates C B x xa)); ra = r; sa = s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B ra sa proof (prove)
goal (1 subgoal):
 1. \<And>r s ra sa. \<lbrakk>C' r s; \<forall>(r', s')\<in>fst (B' r s). whileLoop_terminates C' B' r' s' \<and> (\<forall>x. x = r' \<longrightarrow> (\<forall>xa. xa = s' \<longrightarrow> whileLoop_terminates C B x xa)); ra = r; sa = s\<rbrakk> \<Longrightarrow> \<forall>(r', s')\<in>fst (B ra sa). whileLoop_terminates C B r' s' proof (prove)
goal:
No subgoals! proof (state)
this:
whileLoop_terminates C B r s

goal:
No subgoals!