kings-crown/FVELER_Isabelle huggingface dataset:
theory Corres_UL_C

lemma ccorres_to_vcg_gets_the:
  "\<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] (gets_the r) c; no_ofail P r\<rbrakk>
   \<Longrightarrow> \<Gamma> \<turnstile> (P' \<inter> {s'. (s, s') \<in> srel \<and> P s})
           c {t'. (s, t') \<in> srel \<and> P s \<and> (r s \<noteq> None) \<and> rrel (the (r s)) (xf t')}" apply (frule ccorres_to_vcg_with_prop[where R="\<lambda>_. P" and s=s]) apply (erule no_ofail_gets_the) apply wpsimp apply (clarsimp simp: gets_the_def simpler_gets_def bind_def return_def get_def assert_opt_def
                        fail_def conseq_under_new_pre
                 split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] (gets_the r) c; no_ofail P r\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (P' \<inter> {s'. (s, s') \<in> srel \<and> P s}) c {t'. (s, t') \<in> srel \<and> P s \<and> r s \<noteq> None \<and> rrel (the (r s)) (xf t')} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] (gets_the r) c; no_ofail P r\<rbrakk> \<Longrightarrow> no_fail ?Q (gets_the r)
 2. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] (gets_the r) c; no_ofail P r\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> gets_the r \<lbrace>\<lambda>_. P\<rbrace>
 3. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] (gets_the r) c; no_ofail P r; \<Gamma>\<turnstile> {s'. P s \<and> ?Q s \<and> s' \<in> P' \<and> (s, s') \<in> srel} c {t'. \<exists>(rv, t)\<in>fst (gets_the r s). (t, t') \<in> srel \<and> rrel rv (xf t') \<and> P t}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (P' \<inter> {s'. (s, s') \<in> srel \<and> P s}) c {t'. (s, t') \<in> srel \<and> P s \<and> r s \<noteq> None \<and> rrel (the (r s)) (xf t')} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] (gets_the r) c; no_ofail P r\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> gets_the r \<lbrace>\<lambda>_. P\<rbrace>
 2. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] (gets_the r) c; no_ofail P r; \<Gamma>\<turnstile> {s'. P s \<and> P s \<and> s' \<in> P' \<and> (s, s') \<in> srel} c {t'. \<exists>(rv, t)\<in>fst (gets_the r s). (t, t') \<in> srel \<and> rrel rv (xf t') \<and> P t}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (P' \<inter> {s'. (s, s') \<in> srel \<and> P s}) c {t'. (s, t') \<in> srel \<and> P s \<and> r s \<noteq> None \<and> rrel (the (r s)) (xf t')} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] (gets_the r) c; no_ofail P r; \<Gamma>\<turnstile> {s'. P s \<and> P s \<and> s' \<in> P' \<and> (s, s') \<in> srel} c {t'. \<exists>(rv, t)\<in>fst (gets_the r s). (t, t') \<in> srel \<and> rrel rv (xf t') \<and> P t}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (P' \<inter> {s'. (s, s') \<in> srel \<and> P s}) c {t'. (s, t') \<in> srel \<and> P s \<and> r s \<noteq> None \<and> rrel (the (r s)) (xf t')} proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma exec_handlers_Seq_cases' [consumes 1, case_names NotAbrupt Abrupt]:
  assumes eh: "\<Gamma> \<turnstile>\<^sub>h \<langle>(a ;; b) # hs, s\<rangle> \<Rightarrow> (n, t)"
  and     r1: "\<And>z t'. \<lbrakk>\<Gamma> \<turnstile> \<langle>a, Normal s\<rangle> \<Rightarrow> t';  \<Gamma> \<turnstile> \<langle>b, t'\<rangle> \<Rightarrow> z;
  ((\<not> isAbr z \<or> hs = []) \<and> n = length hs \<and> z = t) \<or> (\<exists>q. z = Abrupt q \<and> \<Gamma> \<turnstile>\<^sub>h \<langle>hs, q\<rangle> \<Rightarrow> (n, t));  \<not> isAbr t' \<rbrakk> \<Longrightarrow> P"
  and     r2: "\<And>t'. \<lbrakk>\<Gamma> \<turnstile> \<langle>a, Normal s\<rangle> \<Rightarrow> Abrupt t'; \<Gamma> \<turnstile>\<^sub>h \<langle>hs, t'\<rangle> \<Rightarrow> (n, t) \<rbrakk> \<Longrightarrow> P"
  shows P using eh r1 r2 by (rule exec_handlers_Seq_cases0' [OF _ refl], auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P proof (prove)
using this:
\<Gamma>\<turnstile>\<^sub>h \<langle>(a;;
b) # hs,s\<rangle> \<Rightarrow> (n, t)
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> ?t'; \<Gamma>\<turnstile> \<langle>b,?t'\<rangle> \<Rightarrow> ?z; (\<not> isAbr ?z \<or> hs = []) \<and> n = length hs \<and> ?z = t \<or> (\<exists>q. ?z = Abrupt q \<and> \<Gamma>\<turnstile>\<^sub>h \<langle>hs,q\<rangle> \<Rightarrow> (n, t)); \<not> isAbr ?t'\<rbrakk> \<Longrightarrow> P
\<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> Abrupt ?t'; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,?t'\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
theory Corres_UL_C

lemma ccorres_abstract_fail:
  assumes fl: "\<And>s. P s \<Longrightarrow> snd (a s)"
  shows  "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a c" apply (rule ccorresI') apply (drule fl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a c proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); snd (a s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_fail':
  "ccorres_underlying sr \<Gamma> rvr xf arrel axf P P' hs fail cfn" by (simp add: ccorres_underlying_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> rvr xf arrel axf P P' hs fail cfn
theory Corres_UL_C

lemma ccorres_fail:
  "ccorres_underlying sr \<Gamma> rvr xf arrel axf \<top> UNIV hs fail cfn" by (rule ccorres_fail')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> rvr xf arrel axf (\<lambda>_. True) UNIV hs fail cfn
theory Corres_UL_C

lemma ccorres_assert:
  assumes rl: "P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs f c"
  shows "ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs (assert P >>= (\<lambda>_. f)) c" apply (cases P) apply (simp add: assert_def) apply (erule rl) apply (simp add: ccorres_fail') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs (do _ <- assert P;
f
od) c proof (prove)
goal (2 subgoals):
 1. P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs (do _ <- assert P;
f
od) c
 2. \<not> P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs (do _ <- assert P;
f
od) c proof (prove)
goal (2 subgoals):
 1. P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs f c
 2. \<not> P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs (do _ <- assert P;
f
od) c proof (prove)
goal (1 subgoal):
 1. \<not> P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs (do _ <- assert P;
f
od) c proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma exec_handlers_Hoare_single_from_vcg:
  "\<Gamma> \<turnstile>\<^bsub>/F\<^esub> P c Q, A \<Longrightarrow> exec_handlers_Hoare \<Gamma> P [c] Q A" apply (drule hoare_sound) apply (simp add: cvalid_def HoarePartialDef.valid_def
                   exec_handlers_Hoare_def) apply (auto elim!: exec_handlers.cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow> exec_handlers_Hoare \<Gamma> P [c] Q A proof (prove)
goal (1 subgoal):
 1. \<Gamma>,{}\<Turnstile>\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow> exec_handlers_Hoare \<Gamma> P [c] Q A proof (prove)
goal (1 subgoal):
 1. \<forall>s t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` A \<Longrightarrow> \<forall>s n. (n = 0 \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s\<rangle> \<Rightarrow> (0, t) \<longrightarrow> s \<in> P \<longrightarrow> t \<notin> Normal ` (- Q))) \<and> (0 < n \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile>\<^sub>h \<langle>[c],s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> s \<in> P \<longrightarrow> t \<notin> Normal ` (- A))) proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma exec_handlers_Hoare_from_vcg_nofail:
  "\<Gamma> \<turnstile>\<^bsub>/F\<^esub> P c Q \<Longrightarrow> exec_handlers_Hoare \<Gamma> P (c # cs) Q A" apply (drule hoare_sound) apply (simp add: cvalid_def HoarePartialDef.valid_def
                   exec_handlers_Hoare_def split del: if_split) apply (clarsimp split del: if_split) apply (erule exec_handlers.cases, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q \<Longrightarrow> exec_handlers_Hoare \<Gamma> P (c # cs) Q A proof (prove)
goal (1 subgoal):
 1. \<Gamma>,{}\<Turnstile>\<^bsub>/F\<^esub> P c Q,{} \<Longrightarrow> exec_handlers_Hoare \<Gamma> P (c # cs) Q A proof (prove)
goal (1 subgoal):
 1. \<forall>s t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q \<Longrightarrow> \<forall>s n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # cs,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> s \<in> P \<longrightarrow> t \<notin> Normal ` (if n = length cs then - Q else - A) proof (prove)
goal (1 subgoal):
 1. \<And>s n x. \<lbrakk>\<forall>s t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q; \<Gamma>\<turnstile>\<^sub>h \<langle>c # cs,s\<rangle> \<Rightarrow> (n, Normal x); s \<in> P; x \<in> (if n = length cs then - Q else - A)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma exec_handlers_Hoare_NormalD:
  "\<lbrakk> exec_handlers_Hoare \<Gamma> P cs Q A; s \<in> P; \<Gamma>  \<turnstile>\<^sub>h \<langle>cs, s\<rangle> \<Rightarrow> (n, Normal t); n = length cs - 1 \<rbrakk>
       \<Longrightarrow> t \<in> Q" by (fastforce simp add: exec_handlers_Hoare_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>exec_handlers_Hoare \<Gamma> P cs Q A; s \<in> P; \<Gamma>\<turnstile>\<^sub>h \<langle>cs,s\<rangle> \<Rightarrow> (n, Normal t); n = length cs - 1\<rbrakk> \<Longrightarrow> t \<in> Q
theory Corres_UL_C

lemma exec_handlers_Hoare_CatchD:
  "\<lbrakk> exec_handlers_Hoare \<Gamma> P cs Q A; s \<in> P; \<Gamma>  \<turnstile>\<^sub>h \<langle>cs, s\<rangle> \<Rightarrow> (n, Normal a); n \<noteq> length cs - 1 \<rbrakk>
       \<Longrightarrow> a \<in> A" by (fastforce simp add: exec_handlers_Hoare_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>exec_handlers_Hoare \<Gamma> P cs Q A; s \<in> P; \<Gamma>\<turnstile>\<^sub>h \<langle>cs,s\<rangle> \<Rightarrow> (n, Normal a); n \<noteq> length cs - 1\<rbrakk> \<Longrightarrow> a \<in> A
theory Corres_UL_C

lemma ccorres_False:
  "ccorres_underlying sr \<Gamma> r xf arrel axf (\<lambda>s. False) P' hs a c" apply (rule ccorresI') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (\<lambda>s. False) P' hs a c proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; False; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_guard_imp:
  assumes x: "ccorres_underlying sr \<Gamma> r xf arrel axf Q Q' hs f g"
  assumes y: "\<And>s. A s \<Longrightarrow> Q s" "\<And>s. s \<in> A' \<Longrightarrow> s \<in> Q'" (* Do we prefer using subset? *)
  shows      "ccorres_underlying sr \<Gamma> r xf arrel axf A A' hs f g" apply (rule stronger_ccorres_guard_imp) apply (rule x) apply (simp add: y)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf A A' hs f g proof (prove)
goal (3 subgoals):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf ?Q ?Q' hs f g
 2. \<And>s s'. \<lbrakk>A s; s' \<in> A'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s s'. \<lbrakk>A s; s' \<in> A'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>A s; s' \<in> A'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> Q s
 2. \<And>s s'. \<lbrakk>A s; s' \<in> A'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> s' \<in> Q' proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_add_return:
  "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (return () >>= (\<lambda>_. a)) c
      \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a c" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (do _ <- return ();
a
od) c \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a c
theory Corres_UL_C

lemma ccorres_add_return2:
  "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (a >>= (\<lambda>x. return x)) c
      \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a c" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (a >>= return) c \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a c
theory Corres_UL_C

lemma ccorres_return_Skip':
  shows  "ccorres_underlying sr \<Gamma> r xf arrel axf \<top> (UNIV \<inter> {s. r a (xf s)}) hs
                             (return a) SKIP" apply (rule ccorres_return) apply simp apply (rule HoarePartial.Skip) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (\<lambda>_. True) (UNIV \<inter> {s. r a (xf s)}) hs (return a) SKIP proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<Gamma>\<turnstile> (UNIV \<inter> {s. r a (xf s)} \<inter> {s'. (s, s') \<in> sr}) SKIP {s'. (s, s') \<in> sr \<and> r a (xf s')} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<Gamma>\<turnstile> ({s. r a (xf s)} \<inter> {s'. (s, s') \<in> sr}) SKIP {s'. (s, s') \<in> sr \<and> r a (xf s')} proof (prove)
goal (1 subgoal):
 1. \<And>s. {s. r a (xf s)} \<inter> {s'. (s, s') \<in> sr} \<subseteq> {s'. (s, s') \<in> sr \<and> r a (xf s')} proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_return_Skip:
  shows  "ccorres_underlying sr \<Gamma> dc xf arrel axf \<top> UNIV hs (return a) SKIP" by (rule ccorres_return_Skip'[where r=dc, simplified])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> dc xf arrel axf (\<lambda>_. True) UNIV hs (return a) SKIP
theory Corres_UL_C

lemma ccorres_split_throw:
  assumes abh: "ccorres_underlying sr \<Gamma> arrel axf arrel axf P P' hs a h"
  shows "ccorres_underlying sr \<Gamma> r xf arrel axf P P' (h#hs) a (Throw ;; d)" apply (rule ccorres_guard_imp, rule ccorres_split_throws) apply (rule ccorres_throw[OF abh]) apply (rule HoarePartial.Throw) apply (rule order_refl) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf P P' (h # hs) a (THROW;;
d) proof (prove)
goal (4 subgoals):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf ?Q ?P'4 (h # hs) a THROW
 2. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'4 THROW {},UNIV
 3. \<And>s. P s \<Longrightarrow> ?Q s
 4. \<And>s. s \<in> P' \<Longrightarrow> s \<in> ?P'4 \<inter> ?R'4 proof (prove)
goal (3 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'4 THROW {},UNIV
 2. \<And>s. P s \<Longrightarrow> P s
 3. \<And>s. s \<in> P' \<Longrightarrow> s \<in> P' \<inter> ?R'4 proof (prove)
goal (3 subgoals):
 1. ?R'4 \<subseteq> UNIV
 2. \<And>s. P s \<Longrightarrow> P s
 3. \<And>s. s \<in> P' \<Longrightarrow> s \<in> P' \<inter> ?R'4 proof (prove)
goal (2 subgoals):
 1. \<And>s. P s \<Longrightarrow> P s
 2. \<And>s. s \<in> P' \<Longrightarrow> s \<in> P' \<inter> UNIV proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_tmp_lift1:
  assumes rl: "\<And>rv'. P rv'
  \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf G (G' \<inter> {s. xf' s = rv'}) hs m c"
  shows "ccorres_underlying srel \<Gamma> rrel xf arrel axf G (G' \<inter> {s. P (xf' s)}) hs m c" by (auto intro!: ccorresI dest!: rl elim: ccorresE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying srel \<Gamma> rrel xf arrel axf G (G' \<inter> {s. P (xf' s)}) hs m c
theory Corres_UL_C

lemma exec_handlers_semantic_equiv0:
  assumes se: "\<And>s'. semantic_equiv \<Gamma> s s' a b"
  and     eh: "\<Gamma> \<turnstile>\<^sub>h \<langle>a # hs, s\<rangle> \<Rightarrow> (n, t)"
  shows   "\<Gamma> \<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, t)" using se eh apply - apply (erule ceqvhD1 [where xf = "\<lambda>_. ()" and v = "()", folded semantic_equiv_def]) apply simp apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, t) proof (prove)
using this:
semantic_equiv \<Gamma> s ?s' a b
\<Gamma>\<turnstile>\<^sub>h \<langle>a # hs,s\<rangle> \<Rightarrow> (n, t)

goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, t) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s'. semantic_equiv \<Gamma> s s' a b; \<Gamma>\<turnstile>\<^sub>h \<langle>a # hs,s\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, t) proof (prove)
goal (2 subgoals):
 1. (\<And>s'. semantic_equiv \<Gamma> s s' a b) \<Longrightarrow> () = ()
 2. \<And>s'. (\<And>s'. semantic_equiv \<Gamma> s s' a b) \<Longrightarrow> semantic_equiv \<Gamma> s s' a b proof (prove)
goal (1 subgoal):
 1. \<And>s'. (\<And>s'. semantic_equiv \<Gamma> s s' a b) \<Longrightarrow> semantic_equiv \<Gamma> s s' a b proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma exec_handlers_semantic_equiv:
  assumes se: "\<And>s'. semantic_equiv \<Gamma> s s' a b"
  shows   "\<Gamma> \<turnstile>\<^sub>h \<langle>a # hs, s\<rangle> \<Rightarrow> (n, t) = \<Gamma> \<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, t)" using se apply - apply rule apply (erule (1) exec_handlers_semantic_equiv0) apply (subst (asm) semantic_equiv_sym) apply (erule (1) exec_handlers_semantic_equiv0) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^sub>h \<langle>a # hs,s\<rangle> \<Rightarrow> (n, t) = \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, t) proof (prove)
using this:
semantic_equiv \<Gamma> s ?s' a b

goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^sub>h \<langle>a # hs,s\<rangle> \<Rightarrow> (n, t) = \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, t) proof (prove)
goal (1 subgoal):
 1. (\<And>s'. semantic_equiv \<Gamma> s s' a b) \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>a # hs,s\<rangle> \<Rightarrow> (n, t) = \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, t) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s'. semantic_equiv \<Gamma> s s' a b; \<Gamma>\<turnstile>\<^sub>h \<langle>a # hs,s\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, t)
 2. \<lbrakk>\<And>s'. semantic_equiv \<Gamma> s s' a b; \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>a # hs,s\<rangle> \<Rightarrow> (n, t) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s'. semantic_equiv \<Gamma> s s' a b; \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>a # hs,s\<rangle> \<Rightarrow> (n, t) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s'. semantic_equiv \<Gamma> s s' b a; \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>a # hs,s\<rangle> \<Rightarrow> (n, t) proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_semantic_equiv:
  assumes rl: "\<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' c c'"
  shows "ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c =
  ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c'" using rl apply - apply rule apply (erule (1) ccorres_semantic_equiv0) apply (subst (asm) semantic_equiv_sym) apply (erule (1) ccorres_semantic_equiv0) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c = ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c' proof (prove)
using this:
?s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> ?s ?s' c c'

goal (1 subgoal):
 1. ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c = ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c' proof (prove)
goal (1 subgoal):
 1. (\<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' c c') \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c = ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' c c'; ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c\<rbrakk> \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c'
 2. \<lbrakk>\<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' c c'; ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c'\<rbrakk> \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' c c'; ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c'\<rbrakk> \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' c' c; ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c'\<rbrakk> \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma test_ccorres_exec_congs:
  "ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a
         (Guard F UNIV Skip ;; While S (c ;; Guard F UNIV Skip))
   = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (While S c)" apply (simp add: exec_eq_simps cong: ccorres_exec_congs) oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (Guard F UNIV SKIP;;
While S (c;;
Guard F UNIV SKIP)) = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (While S c) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (While S (c;;
Guard F UNIV SKIP)) = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (While S c)