kings-crown/FVELER_Isabelle huggingface dataset:
theory CCorresLemmas

lemma Diff_Diff_Un_Diff: "(A - B - C) \<union> (B - D) =
  ((A - C) \<union> B) \<inter> (A - B - C \<union> - D)" (is "?LHS = ?RHS") proof - have "?LHS = (A - B - C) \<union> (B \<inter> - D)" by (simp add: Diff_eq) also have "\<dots> = ?RHS" by (simp add: Un_Int_distrib Diff_Diff_Subset_cancel) finally show ?thesis . qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A - B - C \<union> (B - D) = (A - C \<union> B) \<inter> (A - B - C \<union> - D) proof (state)
goal (1 subgoal):
 1. A - B - C \<union> (B - D) = (A - C \<union> B) \<inter> (A - B - C \<union> - D) proof (prove)
goal (1 subgoal):
 1. A - B - C \<union> (B - D) = A - B - C \<union> B \<inter> - D proof (state)
this:
A - B - C \<union> (B - D) = A - B - C \<union> B \<inter> - D

goal (1 subgoal):
 1. A - B - C \<union> (B - D) = (A - C \<union> B) \<inter> (A - B - C \<union> - D) proof (state)
this:
A - B - C \<union> (B - D) = A - B - C \<union> B \<inter> - D

goal (1 subgoal):
 1. A - B - C \<union> (B - D) = (A - C \<union> B) \<inter> (A - B - C \<union> - D) proof (prove)
goal (1 subgoal):
 1. A - B - C \<union> B \<inter> - D = (A - C \<union> B) \<inter> (A - B - C \<union> - D) proof (state)
this:
A - B - C \<union> B \<inter> - D = (A - C \<union> B) \<inter> (A - B - C \<union> - D)

goal (1 subgoal):
 1. A - B - C \<union> (B - D) = (A - C \<union> B) \<inter> (A - B - C \<union> - D) proof (chain)
picking this:
A - B - C \<union> (B - D) = (A - C \<union> B) \<inter> (A - B - C \<union> - D) proof (prove)
using this:
A - B - C \<union> (B - D) = (A - C \<union> B) \<inter> (A - B - C \<union> - D)

goal (1 subgoal):
 1. A - B - C \<union> (B - D) = (A - C \<union> B) \<inter> (A - B - C \<union> - D) proof (state)
this:
A - B - C \<union> (B - D) = (A - C \<union> B) \<inter> (A - B - C \<union> - D)

goal:
No subgoals!
theory CCorresLemmas

lemma lift_t_field_h_val:
  fixes pa :: "'a :: mem_type ptr"
  assumes fl: "(field_lookup (typ_info_t TYPE('a)) f 0) \<equiv> Some (t, m')"
  and   eu: "export_uinfo t = typ_uinfo_t TYPE('b :: mem_type)"
  shows "clift (h, d) pa = Some v \<Longrightarrow> h_val h (Ptr &(pa\<rightarrow>f) :: 'b :: mem_type ptr) = from_bytes (access_ti\<^sub>0 t v)" using fl eu apply - apply (rule lift_t_h_val [where g=c_guard]) apply (erule (2) lift_t_mono [OF meta_eq_to_obj_eq]) apply (rule c_guard_mono) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (h, d) pa = Some v \<Longrightarrow> h_val h (PTR('b) &(pa\<rightarrow>f)) = from_bytes (access_ti\<^sub>0 t v) proof (prove)
using this:
field_lookup (typ_info_t TYPE('a)) f 0 \<equiv> Some (t, m')
export_uinfo t = typ_uinfo_t TYPE('b)

goal (1 subgoal):
 1. clift (h, d) pa = Some v \<Longrightarrow> h_val h (PTR('b) &(pa\<rightarrow>f)) = from_bytes (access_ti\<^sub>0 t v) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>clift (h, d) pa = Some v; field_lookup (typ_info_t TYPE('a)) f 0 \<equiv> Some (t, m'); export_uinfo t = typ_uinfo_t TYPE('b)\<rbrakk> \<Longrightarrow> h_val h (PTR('b) &(pa\<rightarrow>f)) = from_bytes (access_ti\<^sub>0 t v) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>clift (h, d) pa = Some v; field_lookup (typ_info_t TYPE('a)) f 0 \<equiv> Some (t, m'); export_uinfo t = typ_uinfo_t TYPE('b)\<rbrakk> \<Longrightarrow> clift (h, ?d2) (PTR('b) &(pa\<rightarrow>f)) = Some (from_bytes (access_ti\<^sub>0 t v)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>clift (h, d) pa = Some v; export_uinfo t = typ_uinfo_t TYPE('b)\<rbrakk> \<Longrightarrow> guard_mono c_guard c_guard proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma fl_sub_typ:
  "\<lbrakk> field_lookup (typ_info_t TYPE('a :: c_type)) f 0 = Some (t, n); export_uinfo t = typ_uinfo_t TYPE('b :: c_type) \<rbrakk>
  \<Longrightarrow> TYPE ('b) \<le>\<^sub>\<tau> TYPE ('a)" unfolding sub_typ_def apply (simp add: typ_simps) apply (drule td_set_field_lookupD) apply (drule td_set_export_uinfoD) apply simp apply (erule exI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n); export_uinfo t = typ_uinfo_t TYPE('b)\<rbrakk> \<Longrightarrow> TYPE('b) \<le>\<^sub>\<tau> TYPE('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n); export_uinfo t = typ_uinfo_t TYPE('b)\<rbrakk> \<Longrightarrow> typ_uinfo_t TYPE('b) \<le> typ_uinfo_t TYPE('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n); export_uinfo t = export_uinfo (typ_info_t TYPE('b))\<rbrakk> \<Longrightarrow> \<exists>n. (export_uinfo (typ_info_t TYPE('b)), n) \<in> td_set (export_uinfo (typ_info_t TYPE('a))) 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>export_uinfo t = export_uinfo (typ_info_t TYPE('b)); (t, n) \<in> td_set (typ_info_t TYPE('a)) 0\<rbrakk> \<Longrightarrow> \<exists>n. (export_uinfo (typ_info_t TYPE('b)), n) \<in> td_set (export_uinfo (typ_info_t TYPE('a))) 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>export_uinfo t = export_uinfo (typ_info_t TYPE('b)); (export_uinfo t, n) \<in> td_set (export_uinfo (typ_info_t TYPE('a))) 0\<rbrakk> \<Longrightarrow> \<exists>n. (export_uinfo (typ_info_t TYPE('b)), n) \<in> td_set (export_uinfo (typ_info_t TYPE('a))) 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>export_uinfo t = export_uinfo (typ_info_t TYPE('b)); (export_uinfo (typ_info_t TYPE('b)), n) \<in> td_set (export_uinfo (typ_info_t TYPE('a))) 0\<rbrakk> \<Longrightarrow> \<exists>n. (export_uinfo (typ_info_t TYPE('b)), n) \<in> td_set (export_uinfo (typ_info_t TYPE('a))) 0 proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma ccorres_assert2:
  "\<lbrakk> P \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf G G' hs (f ()) c \<rbrakk>
      \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf
              (\<lambda>s. P \<longrightarrow> G s) {s. P \<longrightarrow> s \<in> G'} hs (assert P >>= f) c" by (cases P, simp_all add: ccorres_fail')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf G G' hs (f ()) c) \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf (\<lambda>s. P \<longrightarrow> G s) {s. P \<longrightarrow> s \<in> G'} hs (assert P >>= f) c
theory CCorresLemmas

lemma ccorres_assertE2:
  "\<lbrakk> P \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf G G' hs (f ()) c \<rbrakk>
      \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf
              (\<lambda>s. P \<longrightarrow> G s) {s. P \<longrightarrow> s \<in> G'} hs (assertE P >>=E f) c" by (cases P, simp_all add: ccorres_fail')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf G G' hs (f ()) c) \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf (\<lambda>s. P \<longrightarrow> G s) {s. P \<longrightarrow> s \<in> G'} hs (assertE P >>=E f) c
theory CCorresLemmas

lemma ccorres_if_lhs:
  "\<lbrakk> P \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf Q S hs f conc;
     \<not> P \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf R T hs g conc \<rbrakk>
   \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s))
                      {s. (P \<longrightarrow> s \<in> S) \<and> (\<not> P \<longrightarrow> s \<in> T)}
          hs (if P then f else g) conc" by (simp split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf Q S hs f conc; \<not> P \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf R T hs g conc\<rbrakk> \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)) {s. (P \<longrightarrow> s \<in> S) \<and> (\<not> P \<longrightarrow> s \<in> T)} hs (if P then f else g) conc
theory CCorresLemmas

lemma ccorres_if_bindE:
  "ccorres_underlying sr Gamm r xf arrel axf G G' hs (if a then (b >>=E f) else (c >>=E f)) d
  \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf G G' hs ((if a then b else c) >>=E f) d" by (simp split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr Gamm r xf arrel axf G G' hs (if a then b >>=E f else c >>=E f) d \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf G G' hs ((if a then b else c) >>=E f) d
theory CCorresLemmas

lemma ccorres_liftE:
  fixes \<Gamma>
  assumes cc: "ccorresG sr \<Gamma> (\<lambda> rv. r (Inr rv)) xf P P' hs a c"
  shows   "ccorresG sr \<Gamma> r xf P P' hs (liftE a) c" using cc by (fastforce split: xstate.splits
                simp: liftE_def ccorres_underlying_def bind_def' return_def unif_rrel_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorresG sr \<Gamma> r xf P P' hs (liftE a) c proof (prove)
using this:
ccorresG sr \<Gamma> (\<lambda>rv. r (Inr rv)) xf P P' hs a c

goal (1 subgoal):
 1. ccorresG sr \<Gamma> r xf P P' hs (liftE a) c
theory CCorresLemmas

lemma ccorres_liftE':
  fixes \<Gamma>
  assumes cc: "ccorresG sr \<Gamma> (r \<circ> Inr) xf P P' hs a c"
  shows   "ccorresG sr \<Gamma> r xf P P' hs (liftE a) c" using cc by (auto intro!: ccorres_liftE cong: ccorres_context_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorresG sr \<Gamma> r xf P P' hs (liftE a) c proof (prove)
using this:
ccorresG sr \<Gamma> (r \<circ> Inr) xf P P' hs a c

goal (1 subgoal):
 1. ccorresG sr \<Gamma> r xf P P' hs (liftE a) c
theory CCorresLemmas

lemma ccorres_if_bind:
  "ccorres_underlying sr Gamm r xf arrel axf G G' hs (if a then (b >>= f) else (c >>= f)) d
  \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf G G' hs ((if a then b else c) >>= f) d" by (simp split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr Gamm r xf arrel axf G G' hs (if a then b >>= f else c >>= f) d \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf G G' hs ((if a then b else c) >>= f) d
theory CCorresLemmas

lemma ccorres_Cond_rhs:
  "\<lbrakk> P \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf Q S hs absf f;
     \<not> P \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf R T hs absf g \<rbrakk>
   \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s))
                      {s. (P \<longrightarrow> s \<in> S) \<and> (\<not> P \<longrightarrow> s \<in> T)}
          hs absf (Cond {s. P} f g)" by (cases P, simp_all add: ccorres_cond_iffs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf Q S hs absf f; \<not> P \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf R T hs absf g\<rbrakk> \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)) {s. (P \<longrightarrow> s \<in> S) \<and> (\<not> P \<longrightarrow> s \<in> T)} hs absf (IF P THEN
  f
ELSE
  g
FI)
theory CCorresLemmas

lemma ccorres_Cond_rhs_Seq:
  "\<lbrakk> P \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf Q S hs absf (f ;; h);
     \<not> P \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf R T hs absf (g ;; h) \<rbrakk>
   \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s))
                      {s. (P \<longrightarrow> s \<in> S) \<and> (\<not> P \<longrightarrow> s \<in> T)}
          hs absf (Cond {s. P} f g ;; h)" by (cases P, simp_all add: ccorres_cond_iffs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf Q S hs absf (f;;
h); \<not> P \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf R T hs absf (g;;
h)\<rbrakk> \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)) {s. (P \<longrightarrow> s \<in> S) \<and> (\<not> P \<longrightarrow> s \<in> T)} hs absf (IF P THEN
  f
ELSE
  g
FI;;
h)
theory CCorresLemmas

lemma ccorres_disj_division:
  "\<lbrakk> P \<or> Q; P \<Longrightarrow> ccorres_underlying sr G r xf ar axf R S hs a c;
            Q \<Longrightarrow> ccorres_underlying sr G r xf ar axf T U hs a c \<rbrakk>
     \<Longrightarrow> ccorres_underlying sr G r xf ar axf
             (\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)) {s. (P \<longrightarrow> s \<in> S) \<and> (Q \<longrightarrow> s \<in> U)}
                hs a c" apply (erule disjE, simp_all) apply (auto elim!: ccorres_guard_imp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<or> Q; P \<Longrightarrow> ccorres_underlying sr G r xf ar axf R S hs a c; Q \<Longrightarrow> ccorres_underlying sr G r xf ar axf T U hs a c\<rbrakk> \<Longrightarrow> ccorres_underlying sr G r xf ar axf (\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)) {s. (P \<longrightarrow> s \<in> S) \<and> (Q \<longrightarrow> s \<in> U)} hs a c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccorres_underlying sr G r xf ar axf R S hs a c; Q \<Longrightarrow> ccorres_underlying sr G r xf ar axf T U hs a c; P\<rbrakk> \<Longrightarrow> ccorres_underlying sr G r xf ar axf (\<lambda>s. R s \<and> (Q \<longrightarrow> T s)) {s \<in> S. Q \<longrightarrow> s \<in> U} hs a c
 2. \<lbrakk>P \<Longrightarrow> ccorres_underlying sr G r xf ar axf R S hs a c; ccorres_underlying sr G r xf ar axf T U hs a c; Q\<rbrakk> \<Longrightarrow> ccorres_underlying sr G r xf ar axf (\<lambda>s. (P \<longrightarrow> R s) \<and> T s) {s. (P \<longrightarrow> s \<in> S) \<and> s \<in> U} hs a c proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma disj_division_bool: "b \<or> \<not> b" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b \<or> \<not> b
theory CCorresLemmas

lemma ceqv_tuple:
  "\<lbrakk> ceqv \<Gamma> xfa va s s' x y; ceqv \<Gamma> xfb vb s s' y z \<rbrakk>
        \<Longrightarrow> ceqv \<Gamma> (\<lambda>s. (xfa s, xfb s)) (va, vb) s s' x z" by (simp add: ceqv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ceqv \<Gamma> xfa va s s' x y; ceqv \<Gamma> xfb vb s s' y z\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (\<lambda>s. (xfa s, xfb s)) (va, vb) s s' x z
theory CCorresLemmas

lemma ceqv_tuple2:
  "\<lbrakk> ceqv \<Gamma> xfa (fst v) s s' x y; ceqv \<Gamma> xfb (snd v) s s' y z \<rbrakk>
        \<Longrightarrow> ceqv \<Gamma> (\<lambda>s. (xfa s, xfb s)) v s s' x z" by (cases v, simp add: ceqv_tuple)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ceqv \<Gamma> xfa (fst v) s s' x y; ceqv \<Gamma> xfb (snd v) s s' y z\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (\<lambda>s. (xfa s, xfb s)) v s s' x z
theory CCorresLemmas

lemma ccorres_inst:
  "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs h c
     \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs h c" by simp

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

lemma ccorres_cross_over_guard:
  "ccorres_underlying sr Gamm rvr xf arrel axf P' Q hs af cf \<Longrightarrow>
      ccorres_underlying sr Gamm rvr xf arrel axf (P and P') {s'. \<forall>s. (s, s') \<in> sr \<and> P s \<longrightarrow> s' \<in> Q} hs af cf" apply (erule ccorres_guard_imp2) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr Gamm rvr xf arrel axf P' Q hs af cf \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf (P and P') {s'. \<forall>s. (s, s') \<in> sr \<and> P s \<longrightarrow> s' \<in> Q} hs af cf proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> sr; (P and P') s; s' \<in> {s'. \<forall>s. (s, s') \<in> sr \<and> P s \<longrightarrow> s' \<in> Q}\<rbrakk> \<Longrightarrow> P' s \<and> s' \<in> Q proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma ccorres_cross_over_guard_no_st:
  "ccorres_underlying sr Gamm rvr xf arrel axf P' Q hs af cf \<Longrightarrow>
      ccorres_underlying sr Gamm rvr xf arrel axf (K P and P') {s'. P \<longrightarrow> s' \<in> Q} hs af cf" apply (erule ccorres_guard_imp2) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr Gamm rvr xf arrel axf P' Q hs af cf \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf (K P and P') {s'. P \<longrightarrow> s' \<in> Q} hs af cf proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> sr; (K P and P') s; s' \<in> {s'. P \<longrightarrow> s' \<in> Q}\<rbrakk> \<Longrightarrow> P' s \<and> s' \<in> Q proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma sequence_x_sequence:
  "sequence_x xs = (sequence xs >>= (\<lambda>_. return ()))" by (induct xs, simp_all add: sequence_def sequence_x_def Let_def
                               bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sequence_x xs = do _ <- Nondet_Monad.sequence xs;
return ()
od
theory CCorresLemmas

lemma sequence_Cons:
  "sequence (x # xs) = do v \<leftarrow> x; vs \<leftarrow> sequence xs; return (v # vs) od" by (simp add: sequence_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Nondet_Monad.sequence (x # xs) = do v <- x;
vs <- Nondet_Monad.sequence xs;
return (v # vs)
od
theory CCorresLemmas

lemma inl_rrel_inl_rrel:
  "inl_rrel (inl_rrel r) = inl_rrel r" by (intro ext, simp add: inl_rrel_def split: sum.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inl_rrel (inl_rrel r) = inl_rrel r
theory CCorresLemmas

lemma ccorres_abstract_h_val:
  fixes p :: "'a :: c_type ptr"
  shows "(\<And>rv. P rv \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G (G' rv) hs a c) \<Longrightarrow>
  ccorres_underlying sr Gamm rvr xf arrel axf G ({s. P ((f::'a \<Rightarrow> ('b::{type})) s) \<longrightarrow> s \<in> G' (f s)} \<inter> {s. P (f s)}) hs a c" apply (rule ccorres_tmp_lift1 [where P = P]) apply (clarsimp simp: Collect_conj_eq [symmetric]) apply (fastforce intro: ccorres_guard_imp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>rv. P rv \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G (G' rv) hs a c) \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G ({s. P (f s) \<longrightarrow> s \<in> G' (f s)} \<inter> {s. P (f s)}) hs a c proof (prove)
goal (1 subgoal):
 1. \<And>rv'. \<lbrakk>\<And>rv. P rv \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G (G' rv) hs a c; P rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G ({s. P (f s) \<longrightarrow> s \<in> G' (f s)} \<inter> {s. f s = rv'}) hs a c proof (prove)
goal (1 subgoal):
 1. \<And>rv'. \<lbrakk>\<And>rv. P rv \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G (G' rv) hs a c; P rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G {s. (P (f s) \<longrightarrow> s \<in> G' (f s)) \<and> f s = rv'} hs a c proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma ccorres_abstract_cslift:
  fixes p :: "'a :: c_type ptr"
  shows "(\<And>rv. P rv \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G (G' rv) hs a c) \<Longrightarrow>
  ccorres_underlying sr Gamm rvr xf arrel axf G ({s. P ((f::'a \<Rightarrow> ('b::{type})) s) \<longrightarrow> s \<in> G' (f s)} \<inter> {s. P (f s)}) hs a c" by (fact ccorres_abstract_h_val)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>rv. P rv \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G (G' rv) hs a c) \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G ({s. P (f s) \<longrightarrow> s \<in> G' (f s)} \<inter> {s. P (f s)}) hs a c
theory CCorresLemmas

lemma ccorres_expand_while_iff_Seq:
  "ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (Cond P (c ;; While P c ;; c') c') =
   ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (While P c ;; c')" apply (rule ccorres_semantic_equiv) apply (rule semantic_equivI) apply (auto elim!: exec_Normal_elim_cases intro: exec.intros) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (Cond P (c;;
While P c;;
c') c') = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (While P c;;
c') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' (Cond P (c;;
While P c;;
c') c') (While P c;;
c') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond P (c;;
While P c;;
c') c',Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>While P c;;
c',Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma ccorres_expand_while_iff_Seq2:
  "ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (c'' ;; Cond P (c ;; While P c ;; c') c') =
   ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (c'' ;; While P c ;; c')" apply (rule ccorres_semantic_equiv) apply (rule semantic_equivI) apply (auto elim!: exec_Normal_elim_cases intro: exec.intros
              | erule exec_elim_cases)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (c'';;
Cond P (c;;
While P c;;
c') c') = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (c'';;
While P c;;
c') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' (c'';;
Cond P (c;;
While P c;;
c') c') (c'';;
While P c;;
c') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c'';;
Cond P (c;;
While P c;;
c') c',Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c'';;
While P c;;
c',Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma ccorres_seq_skip':
  "ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (c ;; Skip)
       = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a c" apply (rule ccorres_semantic_equiv) apply (rule semantic_equivI) apply (case_tac s', auto elim!: exec_elim_cases intro: exec.intros) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (c;;
SKIP) = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a c proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' (c;;
SKIP) c proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c;;
SKIP,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma ccorres_abstract_cleanup:
  "ccorres_underlying sr \<Gamma> r xf ar axf G G' hs a c \<Longrightarrow>
   ccorres_underlying sr \<Gamma> r xf ar axf G ({s. s \<in> S \<longrightarrow> s \<in> G'} \<inter> S) hs a c" by (fastforce intro: ccorres_guard_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf ar axf G G' hs a c \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf G ({s. s \<in> S \<longrightarrow> s \<in> G'} \<inter> S) hs a c