theory Corres_UL_C

lemma ccorres_cond_seq:
  "ccorres_underlying sr \<Gamma> r xf r' xf' P P' hs H (Cond Q (c;;d) (c';;d)) \<Longrightarrow>
   ccorres_underlying sr \<Gamma> r xf r' xf' P P' hs H (Cond Q c c';; d)" apply (erule ccorres_semantic_equivD2) apply (simp only: semantic_equiv_def) apply (clarsimp simp: ceqv_def) apply (rule iffI) apply (erule exec_elim_cases, simp_all)[1] apply (erule exec_elim_cases, simp_all)[1] apply (erule exec.CondTrue) apply (erule (1) exec.Seq) apply (erule exec.CondFalse) apply (erule (1) exec.Seq) apply (erule exec_elim_cases, simp_all)[1] apply (erule exec_elim_cases, simp_all)[1] apply (rule exec.Seq) apply (erule exec.CondTrue) apply assumption apply assumption apply (erule exec_elim_cases, simp_all)[1] apply (rule exec.Seq) apply (erule exec.CondFalse) apply assumption apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf r' xf' P P' hs H (Cond Q (c;;
d) (c';;
d)) \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' P P' hs H (Cond Q c c';;
d) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> P' \<Longrightarrow> semantic_equiv \<Gamma> s s' (Cond Q c c';;
d) (Cond Q (c;;
d) (c';;
d)) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> P' \<Longrightarrow> ceqv \<Gamma> (\<lambda>_. ()) () s s' (Cond Q c c';;
d) (Cond Q (c;;
d) (c';;
d)) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> P' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>Cond Q (c;;
d) (c';;
d),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> P'; \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q (c;;
d) (c';;
d),Normal s\<rangle> \<Rightarrow> s'
 2. \<And>s s'. \<lbrakk>s \<in> P'; \<Gamma>\<turnstile> \<langle>Cond Q (c;;
d) (c';;
d),Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa s'a. \<lbrakk>sa \<in> P'; s = sa; \<Gamma>\<turnstile> \<langle>Cond Q c c',Normal sa\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q (c;;
d) (c';;
d),Normal sa\<rangle> \<Rightarrow> s'
 2. \<And>s s'. \<lbrakk>s \<in> P'; \<Gamma>\<turnstile> \<langle>Cond Q (c;;
d) (c';;
d),Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (3 subgoals):
 1. \<And>s s' sa s'a sb. \<lbrakk>sb \<in> P'; s = sb; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'; sa = sb; sb \<in> Q; \<Gamma>\<turnstile> \<langle>c,Normal sb\<rangle> \<Rightarrow> s'a\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q (c;;
d) (c';;
d),Normal sb\<rangle> \<Rightarrow> s'
 2. \<And>s s' sa s'a sb. \<lbrakk>sb \<in> P'; s = sb; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'; sa = sb; sb \<notin> Q; \<Gamma>\<turnstile> \<langle>c',Normal sb\<rangle> \<Rightarrow> s'a\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q (c;;
d) (c';;
d),Normal sb\<rangle> \<Rightarrow> s'
 3. \<And>s s'. \<lbrakk>s \<in> P'; \<Gamma>\<turnstile> \<langle>Cond Q (c;;
d) (c';;
d),Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (3 subgoals):
 1. \<And>s s' sa s'a sb. \<lbrakk>sb \<in> P'; s = sb; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'; sa = sb; \<Gamma>\<turnstile> \<langle>c,Normal sb\<rangle> \<Rightarrow> s'a\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c;;
d,Normal sb\<rangle> \<Rightarrow> s'
 2. \<And>s s' sa s'a sb. \<lbrakk>sb \<in> P'; s = sb; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'; sa = sb; sb \<notin> Q; \<Gamma>\<turnstile> \<langle>c',Normal sb\<rangle> \<Rightarrow> s'a\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q (c;;
d) (c';;
d),Normal sb\<rangle> \<Rightarrow> s'
 3. \<And>s s'. \<lbrakk>s \<in> P'; \<Gamma>\<turnstile> \<langle>Cond Q (c;;
d) (c';;
d),Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa s'a sb. \<lbrakk>sb \<in> P'; s = sb; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'; sa = sb; sb \<notin> Q; \<Gamma>\<turnstile> \<langle>c',Normal sb\<rangle> \<Rightarrow> s'a\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q (c;;
d) (c';;
d),Normal sb\<rangle> \<Rightarrow> s'
 2. \<And>s s'. \<lbrakk>s \<in> P'; \<Gamma>\<turnstile> \<langle>Cond Q (c;;
d) (c';;
d),Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa s'a sb. \<lbrakk>sb \<in> P'; s = sb; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'; sa = sb; \<Gamma>\<turnstile> \<langle>c',Normal sb\<rangle> \<Rightarrow> s'a\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c';;
d,Normal sb\<rangle> \<Rightarrow> s'
 2. \<And>s s'. \<lbrakk>s \<in> P'; \<Gamma>\<turnstile> \<langle>Cond Q (c;;
d) (c';;
d),Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s \<in> P'; \<Gamma>\<turnstile> \<langle>Cond Q (c;;
d) (c';;
d),Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa. \<lbrakk>sa \<in> P'; s = sa; sa \<in> Q; \<Gamma>\<turnstile> \<langle>c;;
d,Normal sa\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal sa\<rangle> \<Rightarrow> s'
 2. \<And>s s' sa. \<lbrakk>sa \<in> P'; s = sa; sa \<notin> Q; \<Gamma>\<turnstile> \<langle>c';;
d,Normal sa\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal sa\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa sb s'a. \<lbrakk>sb \<in> P'; s = sb; sb \<in> Q; sa = sb; \<Gamma>\<turnstile> \<langle>c,Normal sb\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal sb\<rangle> \<Rightarrow> s'
 2. \<And>s s' sa. \<lbrakk>sa \<in> P'; s = sa; sa \<notin> Q; \<Gamma>\<turnstile> \<langle>c';;
d,Normal sa\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal sa\<rangle> \<Rightarrow> s' proof (prove)
goal (3 subgoals):
 1. \<And>s s' sa sb s'a. \<lbrakk>sb \<in> P'; s = sb; sb \<in> Q; sa = sb; \<Gamma>\<turnstile> \<langle>c,Normal sb\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c',Normal sb\<rangle> \<Rightarrow> ?s'44 s s' sa sb s'a
 2. \<And>s s' sa sb s'a. \<lbrakk>sb \<in> P'; s = sb; sb \<in> Q; sa = sb; \<Gamma>\<turnstile> \<langle>c,Normal sb\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d,?s'44 s s' sa sb s'a\<rangle> \<Rightarrow> s'
 3. \<And>s s' sa. \<lbrakk>sa \<in> P'; s = sa; sa \<notin> Q; \<Gamma>\<turnstile> \<langle>c';;
d,Normal sa\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal sa\<rangle> \<Rightarrow> s' proof (prove)
goal (3 subgoals):
 1. \<And>s s' sa sb s'a. \<lbrakk>sb \<in> P'; s = sb; sa = sb; \<Gamma>\<turnstile> \<langle>c,Normal sb\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c,Normal sb\<rangle> \<Rightarrow> ?s'44 s s' sa sb s'a
 2. \<And>s s' sa sb s'a. \<lbrakk>sb \<in> P'; s = sb; sb \<in> Q; sa = sb; \<Gamma>\<turnstile> \<langle>c,Normal sb\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d,?s'44 s s' sa sb s'a\<rangle> \<Rightarrow> s'
 3. \<And>s s' sa. \<lbrakk>sa \<in> P'; s = sa; sa \<notin> Q; \<Gamma>\<turnstile> \<langle>c';;
d,Normal sa\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal sa\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa sb s'a. \<lbrakk>sb \<in> P'; s = sb; sb \<in> Q; sa = sb; \<Gamma>\<turnstile> \<langle>c,Normal sb\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'
 2. \<And>s s' sa. \<lbrakk>sa \<in> P'; s = sa; sa \<notin> Q; \<Gamma>\<turnstile> \<langle>c';;
d,Normal sa\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal sa\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa. \<lbrakk>sa \<in> P'; s = sa; sa \<notin> Q; \<Gamma>\<turnstile> \<langle>c';;
d,Normal sa\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal sa\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa sb s'a. \<lbrakk>sb \<in> P'; s = sb; sb \<notin> Q; sa = sb; \<Gamma>\<turnstile> \<langle>c',Normal sb\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c';;
d,Normal sb\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa sb s'a. \<lbrakk>sb \<in> P'; s = sb; sb \<notin> Q; sa = sb; \<Gamma>\<turnstile> \<langle>c',Normal sb\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond Q c c',Normal sb\<rangle> \<Rightarrow> ?s'56 s s' sa sb s'a
 2. \<And>s s' sa sb s'a. \<lbrakk>sb \<in> P'; s = sb; sb \<notin> Q; sa = sb; \<Gamma>\<turnstile> \<langle>c',Normal sb\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d,?s'56 s s' sa sb s'a\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa sb s'a. \<lbrakk>sb \<in> P'; s = sb; sa = sb; \<Gamma>\<turnstile> \<langle>c',Normal sb\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c',Normal sb\<rangle> \<Rightarrow> ?s'56 s s' sa sb s'a
 2. \<And>s s' sa sb s'a. \<lbrakk>sb \<in> P'; s = sb; sb \<notin> Q; sa = sb; \<Gamma>\<turnstile> \<langle>c',Normal sb\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d,?s'56 s s' sa sb s'a\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa sb s'a. \<lbrakk>sb \<in> P'; s = sb; sb \<notin> Q; sa = sb; \<Gamma>\<turnstile> \<langle>c',Normal sb\<rangle> \<Rightarrow> s'a; \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>d,s'a\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!