theory Nondet_While_Loop_Rules

lemma whileLoop_results_bisim_helper:
  assumes base: "(a, b) \<in> whileLoop_results C B"
    and inv_init: "case a of Some (r, s) \<Rightarrow> I r s | _ \<Rightarrow> True"
    and inv_step: "\<And>r s r' s'. \<lbrakk> I r s; C r s; (r', s') \<in> fst (B r s) \<rbrakk> \<Longrightarrow> I r' s'"
    and cond_match: "\<And>r s. I r s \<Longrightarrow> C r s = C' (rt r) (st s)"
    and fail_step: "\<And>r s. \<lbrakk>C r s; snd (B r s); I r s\<rbrakk>
                         \<Longrightarrow> (Some (rt r, st s), None) \<in> whileLoop_results C' B'"
    and refine: "\<And>r s r' s'. \<lbrakk> I r s; C r s; (r', s') \<in>  fst (B r s) \<rbrakk>
                            \<Longrightarrow> (rt r', st s') \<in> fst (B' (rt r) (st s))"
  defines [simp]: "Q x \<equiv> (case x of Some (r, s) \<Rightarrow> Some (rt r, st s) | _ \<Rightarrow> None)"
    and [simp]: "R y\<equiv> (case y of Some (r, s) \<Rightarrow> Some (rt r, st s) | _ \<Rightarrow> None)"
  shows "(Q a, R b) \<in> whileLoop_results C' B'" using base inv_init proof (induct rule: whileLoop_results.induct) case (1 r s) then show ?case apply clarsimp apply (subst (asm) cond_match) apply (clarsimp simp: option.splits) apply (clarsimp simp: option.splits) done next case (2 r s) then show ?case apply (clarsimp simp: option.splits) apply (metis fail_step) done next case (3 r s r' s' z) then show ?case apply (cases z) apply (clarsimp simp: option.splits) apply (metis cond_match inv_step refine whileLoop_results.intros(3)) apply (clarsimp simp: option.splits) apply (metis cond_match inv_step refine whileLoop_results.intros(3)) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Q a, R b) \<in> whileLoop_results C' B' proof (prove)
using this:
(a, b) \<in> whileLoop_results C B
case a of None \<Rightarrow> True | Some (r, s) \<Rightarrow> I r s

goal (1 subgoal):
 1. (Q a, R b) \<in> whileLoop_results C' B' proof (state)
goal (3 subgoals):
 1. \<And>r s. \<lbrakk>\<not> C r s; case Some (r, s) of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R (Some (r, s))) \<in> whileLoop_results C' B'
 2. \<And>r s. \<lbrakk>C r s; snd (B r s); case Some (r, s) of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R None) \<in> whileLoop_results C' B'
 3. \<And>r s r' s' z. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; case Some (r', s') of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb \<Longrightarrow> (Q (Some (r', s')), R z) \<in> whileLoop_results C' B'; case Some (r, s) of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R z) \<in> whileLoop_results C' B' proof (state)
this:
\<not> C r s
case Some (r, s) of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c

goal (3 subgoals):
 1. \<And>r s. \<lbrakk>\<not> C r s; case Some (r, s) of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R (Some (r, s))) \<in> whileLoop_results C' B'
 2. \<And>r s. \<lbrakk>C r s; snd (B r s); case Some (r, s) of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R None) \<in> whileLoop_results C' B'
 3. \<And>r s r' s' z. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; case Some (r', s') of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb \<Longrightarrow> (Q (Some (r', s')), R z) \<in> whileLoop_results C' B'; case Some (r, s) of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R z) \<in> whileLoop_results C' B' proof (chain)
picking this:
\<not> C r s
case Some (r, s) of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c proof (prove)
using this:
\<not> C r s
case Some (r, s) of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c

goal (1 subgoal):
 1. (Q (Some (r, s)), R (Some (r, s))) \<in> whileLoop_results C' B' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> C r s; I r s; C' (rt r) (st s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>I r s; C' (rt r) (st s)\<rbrakk> \<Longrightarrow> I r s
 2. \<lbrakk>\<not> C' (rt r) (st s); I r s; C' (rt r) (st s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> C' (rt r) (st s); I r s; C' (rt r) (st s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
(Q (Some (r, s)), R (Some (r, s))) \<in> whileLoop_results C' B'

goal (2 subgoals):
 1. \<And>r s. \<lbrakk>C r s; snd (B r s); case Some (r, s) of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R None) \<in> whileLoop_results C' B'
 2. \<And>r s r' s' z. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; case Some (r', s') of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb \<Longrightarrow> (Q (Some (r', s')), R z) \<in> whileLoop_results C' B'; case Some (r, s) of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R z) \<in> whileLoop_results C' B' proof (state)
goal (2 subgoals):
 1. \<And>r s. \<lbrakk>C r s; snd (B r s); case Some (r, s) of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R None) \<in> whileLoop_results C' B'
 2. \<And>r s r' s' z. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; case Some (r', s') of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb \<Longrightarrow> (Q (Some (r', s')), R z) \<in> whileLoop_results C' B'; case Some (r, s) of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R z) \<in> whileLoop_results C' B' proof (state)
this:
C r s
snd (B r s)
case Some (r, s) of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c

goal (2 subgoals):
 1. \<And>r s. \<lbrakk>C r s; snd (B r s); case Some (r, s) of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R None) \<in> whileLoop_results C' B'
 2. \<And>r s r' s' z. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; case Some (r', s') of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb \<Longrightarrow> (Q (Some (r', s')), R z) \<in> whileLoop_results C' B'; case Some (r, s) of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R z) \<in> whileLoop_results C' B' proof (chain)
picking this:
C r s
snd (B r s)
case Some (r, s) of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c proof (prove)
using this:
C r s
snd (B r s)
case Some (r, s) of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c

goal (1 subgoal):
 1. (Q (Some (r, s)), R None) \<in> whileLoop_results C' B' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C r s; snd (B r s); I r s\<rbrakk> \<Longrightarrow> (Some (rt r, st s), None) \<in> whileLoop_results C' B' proof (prove)
goal:
No subgoals! proof (state)
this:
(Q (Some (r, s)), R None) \<in> whileLoop_results C' B'

goal (1 subgoal):
 1. \<And>r s r' s' z. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; case Some (r', s') of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb \<Longrightarrow> (Q (Some (r', s')), R z) \<in> whileLoop_results C' B'; case Some (r, s) of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R z) \<in> whileLoop_results C' B' proof (state)
goal (1 subgoal):
 1. \<And>r s r' s' z. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; case Some (r', s') of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb \<Longrightarrow> (Q (Some (r', s')), R z) \<in> whileLoop_results C' B'; case Some (r, s) of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R z) \<in> whileLoop_results C' B' proof (state)
this:
C r s
(r', s') \<in> fst (B r s)
(Some (r', s'), z) \<in> whileLoop_results C B
case Some (r', s') of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c \<Longrightarrow> (Q (Some (r', s')), R z) \<in> whileLoop_results C' B'
case Some (r, s) of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c

goal (1 subgoal):
 1. \<And>r s r' s' z. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; case Some (r', s') of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb \<Longrightarrow> (Q (Some (r', s')), R z) \<in> whileLoop_results C' B'; case Some (r, s) of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> I xa xb\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R z) \<in> whileLoop_results C' B' proof (chain)
picking this:
C r s
(r', s') \<in> fst (B r s)
(Some (r', s'), z) \<in> whileLoop_results C B
case Some (r', s') of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c \<Longrightarrow> (Q (Some (r', s')), R z) \<in> whileLoop_results C' B'
case Some (r, s) of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c proof (prove)
using this:
C r s
(r', s') \<in> fst (B r s)
(Some (r', s'), z) \<in> whileLoop_results C B
case Some (r', s') of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c \<Longrightarrow> (Q (Some (r', s')), R z) \<in> whileLoop_results C' B'
case Some (r, s) of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c

goal (1 subgoal):
 1. (Q (Some (r, s)), R z) \<in> whileLoop_results C' B' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; case Some (r', s') of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c \<Longrightarrow> (Q (Some (r', s')), R z) \<in> whileLoop_results C' B'; case Some (r, s) of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c; z = None\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R z) \<in> whileLoop_results C' B'
 2. \<And>a. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; case Some (r', s') of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c \<Longrightarrow> (Q (Some (r', s')), R z) \<in> whileLoop_results C' B'; case Some (r, s) of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c; z = Some a\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R z) \<in> whileLoop_results C' B' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), None) \<in> whileLoop_results C B; I r' s' \<Longrightarrow> (Some (rt r', st s'), None) \<in> whileLoop_results C' B'; I r s; z = None\<rbrakk> \<Longrightarrow> (Some (rt r, st s), None) \<in> whileLoop_results C' B'
 2. \<And>a. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; case Some (r', s') of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c \<Longrightarrow> (Q (Some (r', s')), R z) \<in> whileLoop_results C' B'; case Some (r, s) of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c; z = Some a\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R z) \<in> whileLoop_results C' B' proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; case Some (r', s') of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c \<Longrightarrow> (Q (Some (r', s')), R z) \<in> whileLoop_results C' B'; case Some (r, s) of None \<Rightarrow> True | Some (b, c) \<Rightarrow> I b c; z = Some a\<rbrakk> \<Longrightarrow> (Q (Some (r, s)), R z) \<in> whileLoop_results C' B' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), Some (a, b)) \<in> whileLoop_results C B; I r' s' \<Longrightarrow> (Some (rt r', st s'), Some (rt a, st b)) \<in> whileLoop_results C' B'; I r s; z = Some (a, b)\<rbrakk> \<Longrightarrow> (Some (rt r, st s), Some (rt a, st b)) \<in> whileLoop_results C' B' proof (prove)
goal:
No subgoals! proof (state)
this:
(Q (Some (r, s)), R z) \<in> whileLoop_results C' B'

goal:
No subgoals!