theory VSpace_C

lemma ccorres_flip_Guard:
  assumes cc: "ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F S (Guard F1 S1 c))"
  shows "ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F1 S1 (Guard F S c))" apply (rule ccorres_name_pre_C) using cc apply (case_tac "s \<in> (S1 \<inter> S)") apply (clarsimp simp: ccorres_underlying_def) apply (erule exec_handlers.cases;
    fastforce elim!: exec_Normal_elim_cases intro: exec_handlers.intros exec.Guard) apply (clarsimp simp: ccorres_underlying_def) apply (case_tac "s \<in> S") apply (fastforce intro: exec.Guard exec.GuardFault exec_handlers.intros) apply (fastforce intro: exec.Guard exec.GuardFault exec_handlers.intros) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F1 S1 (Guard F S c)) proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> C \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf A {s} hs a (Guard F1 S1 (Guard F S c)) proof (prove)
using this:
ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F S (Guard F1 S1 c))

goal (1 subgoal):
 1. \<And>s. s \<in> C \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf A {s} hs a (Guard F1 S1 (Guard F S c)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> C; ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F S (Guard F1 S1 c)); s \<in> S1 \<inter> S\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf A {s} hs a (Guard F1 S1 (Guard F S c))
 2. \<And>s. \<lbrakk>s \<in> C; ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F S (Guard F1 S1 c)); s \<notin> S1 \<inter> S\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf A {s} hs a (Guard F1 S1 (Guard F S c)) proof (prove)
goal (2 subgoals):
 1. \<And>s aa n t. \<lbrakk>s \<in> C; \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> A s \<and> s' \<in> C \<and> \<not> snd (a s) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>Guard F S (Guard F1 S1 c) # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a s). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False)); (aa, s) \<in> sr; s \<in> S1; s \<in> S; A aa; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>Guard F1 S1 (Guard F S c) # hs,s\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a aa). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False
 2. \<And>s. \<lbrakk>s \<in> C; ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F S (Guard F1 S1 c)); s \<notin> S1 \<inter> S\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf A {s} hs a (Guard F1 S1 (Guard F S c)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> C; ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F S (Guard F1 S1 c)); s \<notin> S1 \<inter> S\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf A {s} hs a (Guard F1 S1 (Guard F S c)) proof (prove)
goal (1 subgoal):
 1. \<And>s aa n t. \<lbrakk>s \<in> C; \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> A s \<and> s' \<in> C \<and> \<not> snd (a s) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>Guard F S (Guard F1 S1 c) # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a s). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False)); s \<in> S1 \<longrightarrow> s \<notin> S; (aa, s) \<in> sr; A aa; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>Guard F1 S1 (Guard F S c) # hs,s\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a aa). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s aa n t. \<lbrakk>s \<in> C; \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> A s \<and> s' \<in> C \<and> \<not> snd (a s) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>Guard F S (Guard F1 S1 c) # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a s). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False)); s \<in> S1 \<longrightarrow> s \<notin> S; (aa, s) \<in> sr; A aa; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>Guard F1 S1 (Guard F S c) # hs,s\<rangle> \<Rightarrow> (n, t); s \<in> S\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a aa). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False
 2. \<And>s aa n t. \<lbrakk>s \<in> C; \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> A s \<and> s' \<in> C \<and> \<not> snd (a s) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>Guard F S (Guard F1 S1 c) # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a s). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False)); s \<in> S1 \<longrightarrow> s \<notin> S; (aa, s) \<in> sr; A aa; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>Guard F1 S1 (Guard F S c) # hs,s\<rangle> \<Rightarrow> (n, t); s \<notin> S\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a aa). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s aa n t. \<lbrakk>s \<in> C; \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> A s \<and> s' \<in> C \<and> \<not> snd (a s) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>Guard F S (Guard F1 S1 c) # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a s). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False)); s \<in> S1 \<longrightarrow> s \<notin> S; (aa, s) \<in> sr; A aa; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>Guard F1 S1 (Guard F S c) # hs,s\<rangle> \<Rightarrow> (n, t); s \<notin> S\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (a aa). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False proof (prove)
goal:
No subgoals!