theory Nondet_While_Loop_Rules

lemma whileLoop_results_cong [cong]:
  assumes C:  "\<And>r s. C r s = C' r s"
  and B:"\<And>(r :: 'r) (s :: 's). C' r s \<Longrightarrow> B r s = B' r s"
  shows "whileLoop_results C B = whileLoop_results C' B'" proof - { fix x y C B C' B' have  "\<lbrakk> (x, y) \<in> whileLoop_results C B;
             \<And>(r :: 'r) (s :: 's). C r s = C' r s; \<And>r s. C' r s \<Longrightarrow> B r s = B' r s \<rbrakk>
           \<Longrightarrow> (x, y) \<in> whileLoop_results C' B'" by (induct rule: whileLoop_results.induct) (auto intro: whileLoop_results.intros) } thus ?thesis apply - apply (rule set_eqI, rule iffI; clarsimp split: prod.splits) apply (clarsimp simp: C B) apply (clarsimp simp: C [symmetric] B [symmetric]) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whileLoop_results C B = whileLoop_results C' B' proof (state)
goal (1 subgoal):
 1. whileLoop_results C B = whileLoop_results C' B' proof (state)
goal (1 subgoal):
 1. whileLoop_results C B = whileLoop_results C' B' proof (state)
goal (1 subgoal):
 1. whileLoop_results C B = whileLoop_results C' B' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, y) \<in> whileLoop_results C B; \<And>r s. C r s = C' r s; \<And>r s. C' r s \<Longrightarrow> B r s = B' r s\<rbrakk> \<Longrightarrow> (x, y) \<in> whileLoop_results C' B' proof (state)
this:
\<lbrakk>(x, y) \<in> whileLoop_results C B; \<And>r s. C r s = C' r s; \<And>r s. C' r s \<Longrightarrow> B r s = B' r s\<rbrakk> \<Longrightarrow> (x, y) \<in> whileLoop_results C' B'

goal (1 subgoal):
 1. whileLoop_results C B = whileLoop_results C' B' proof (state)
this:
\<lbrakk>(?x2, ?y2) \<in> whileLoop_results ?Ca2 ?Ba2; \<And>r s. ?Ca2 r s = ?C'a2 r s; \<And>r s. ?C'a2 r s \<Longrightarrow> ?Ba2 r s = ?B'a2 r s\<rbrakk> \<Longrightarrow> (?x2, ?y2) \<in> whileLoop_results ?C'a2 ?B'a2

goal (1 subgoal):
 1. whileLoop_results C B = whileLoop_results C' B' proof (prove)
using this:
\<lbrakk>(?x2, ?y2) \<in> whileLoop_results ?Ca2 ?Ba2; \<And>r s. ?Ca2 r s = ?C'a2 r s; \<And>r s. ?C'a2 r s \<Longrightarrow> ?Ba2 r s = ?B'a2 r s\<rbrakk> \<Longrightarrow> (?x2, ?y2) \<in> whileLoop_results ?C'a2 ?B'a2

goal (1 subgoal):
 1. whileLoop_results C B = whileLoop_results C' B' proof (prove)
goal (1 subgoal):
 1. (\<And>x y Ca Ba C'a B'a. \<lbrakk>(x, y) \<in> whileLoop_results Ca Ba; \<And>r s. Ca r s = C'a r s; \<And>r s. C'a r s \<Longrightarrow> Ba r s = B'a r s\<rbrakk> \<Longrightarrow> (x, y) \<in> whileLoop_results C'a B'a) \<Longrightarrow> whileLoop_results C B = whileLoop_results C' B' proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<And>x y Ca Ba C'a B'a. \<lbrakk>(x, y) \<in> whileLoop_results Ca Ba; \<And>r s. Ca r s = C'a r s; \<And>r s. C'a r s \<Longrightarrow> Ba r s = B'a r s\<rbrakk> \<Longrightarrow> (x, y) \<in> whileLoop_results C'a B'a; (a, b) \<in> whileLoop_results C B\<rbrakk> \<Longrightarrow> (a, b) \<in> whileLoop_results C' B'
 2. \<And>a b. \<lbrakk>\<And>x y Ca Ba C'a B'a. \<lbrakk>(x, y) \<in> whileLoop_results Ca Ba; \<And>r s. Ca r s = C'a r s; \<And>r s. C'a r s \<Longrightarrow> Ba r s = B'a r s\<rbrakk> \<Longrightarrow> (x, y) \<in> whileLoop_results C'a B'a; (a, b) \<in> whileLoop_results C' B'\<rbrakk> \<Longrightarrow> (a, b) \<in> whileLoop_results C B proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>x y Ca Ba C'a B'a. \<lbrakk>(x, y) \<in> whileLoop_results Ca Ba; \<And>r s. Ca r s = C'a r s; \<And>r s. C'a r s \<Longrightarrow> Ba r s = B'a r s\<rbrakk> \<Longrightarrow> (x, y) \<in> whileLoop_results C'a B'a; (a, b) \<in> whileLoop_results C' B'\<rbrakk> \<Longrightarrow> (a, b) \<in> whileLoop_results C B proof (prove)
goal:
No subgoals! proof (state)
this:
whileLoop_results C B = whileLoop_results C' B'

goal:
No subgoals!