kings-crown/FVELER_Isabelle huggingface dataset:
theory CCorresLemmas

lemma exec_handlers_Hoare_Post:
  "\<lbrakk> exec_handlers_Hoare \<Gamma> P c Q' A'; Q' \<subseteq> Q; A' \<subseteq> A \<rbrakk>
      \<Longrightarrow> exec_handlers_Hoare \<Gamma> P c Q A" apply (simp add: exec_handlers_Hoare_def
             split del: if_split) apply (elim allEI) apply (simp split: if_split_asm) apply blast+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>exec_handlers_Hoare \<Gamma> P c Q' A'; Q' \<subseteq> Q; A' \<subseteq> A\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> P c Q A proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> s \<in> P \<longrightarrow> t \<notin> Normal ` (if n = length c - Suc 0 then - Q' else - A'); Q' \<subseteq> Q; A' \<subseteq> A\<rbrakk> \<Longrightarrow> \<forall>s n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> s \<in> P \<longrightarrow> t \<notin> Normal ` (if n = length c - Suc 0 then - Q else - A) proof (prove)
goal (1 subgoal):
 1. \<And>s n t. \<lbrakk>Q' \<subseteq> Q; A' \<subseteq> A; \<Gamma>\<turnstile>\<^sub>h \<langle>c,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> s \<in> P \<longrightarrow> t \<notin> Normal ` (if n = length c - Suc 0 then - Q' else - A')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> s \<in> P \<longrightarrow> t \<notin> Normal ` (if n = length c - Suc 0 then - Q else - A) proof (prove)
goal (2 subgoals):
 1. \<And>s n t. \<lbrakk>Q' \<subseteq> Q; A' \<subseteq> A; n = length c - Suc 0; \<Gamma>\<turnstile>\<^sub>h \<langle>c,s\<rangle> \<Rightarrow> (length c - Suc 0, t) \<longrightarrow> s \<in> P \<longrightarrow> t \<notin> Normal ` (- Q')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c,s\<rangle> \<Rightarrow> (length c - Suc 0, t) \<longrightarrow> s \<in> P \<longrightarrow> t \<notin> Normal ` (- Q)
 2. \<And>s n t. \<lbrakk>Q' \<subseteq> Q; A' \<subseteq> A; n \<noteq> length c - Suc 0; \<Gamma>\<turnstile>\<^sub>h \<langle>c,s\<rangle> \<Rightarrow> (n, t) \<longrightarrow> s \<in> P \<longrightarrow> t \<notin> Normal ` (- A')\<rbrakk> \<Longrightarrow> \<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 CCorresLemmas

lemma ccorres_can't_happen:
  "ccorres_underlying st \<Gamma> r xf arrel axf \<bottom> G hs a b" apply (rule ccorres_guard_imp2) apply (rule ccorres_gen_asm [where P = False]) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying st \<Gamma> r xf arrel axf (\<lambda>_. False) G hs a b proof (prove)
goal (2 subgoals):
 1. ccorres_underlying st \<Gamma> r xf arrel axf ?Q ?Q' hs a b
 2. \<And>s s'. \<lbrakk>(s, s') \<in> st; False; s' \<in> G\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. False \<Longrightarrow> ccorres_underlying st \<Gamma> r xf arrel axf ?G3 ?Q' hs a b
 2. \<And>s s'. \<lbrakk>(s, s') \<in> st; False; s' \<in> G\<rbrakk> \<Longrightarrow> (?G3 and (\<lambda>_. False)) s \<and> s' \<in> ?Q' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> st; False; s' \<in> G\<rbrakk> \<Longrightarrow> (?G3 and (\<lambda>_. False)) s \<and> s' \<in> ?Q' proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma ccorres_can't_happen2:
  "ccorres_underlying sr \<Gamma> r xf arrel axf G {} hs a b" apply (rule ccorres_guard_imp2) apply (rule ccorres_gen_asm2 [where P = False]) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf G {} hs a b proof (prove)
goal (2 subgoals):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf ?Q ?Q' hs a b
 2. \<And>s s'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> {}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. False \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Q ?G'3 hs a b
 2. \<And>s s'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> {}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?G'3 \<inter> \<lbrace>False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> {}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?G'3 \<inter> \<lbrace>False\<rbrace> proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma ccorres_split_when_throwError_cond:
  fixes e :: 'e
  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
  and     cc: "P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf
                        R R' (SKIP # hs) (throwError e) c"
  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf
                        U U' (SKIP # hs) b d"
  and cthrows: "\<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> PT' c {}, UNIV" \<comment> \<open>c always throws\<close>
  shows  "ccorres_underlying sr \<Gamma> r xf ar axf
          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
          (SKIP # hs)
          (whenE P (throwError e) >>=E (\<lambda>_. b)) (Cond P' c SKIP ;; d)" apply (subst whenE_bindE_throwError_to_if) apply (rule ccorres_if_cond_throws [OF abs cc bd cthrows]) apply assumption apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf ar axf (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s)) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) (doE _ <- whenE P (throwError e);
b
odE) (Cond P' c SKIP;;
d) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf ar axf (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s)) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) (if P then throwError e else b) (Cond P' c SKIP;;
d) proof (prove)
goal (2 subgoals):
 1. P \<Longrightarrow> P
 2. \<not> P \<Longrightarrow> \<not> P proof (prove)
goal (1 subgoal):
 1. \<not> P \<Longrightarrow> \<not> P proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma ccorres_returnOk_skip:
  "ccorres_underlying sr \<Gamma> r xf arrel axf \<top>
     {s. r (Inr v) (xf s)} hs (returnOk v) Skip" using ccorres_return_Skip' by (simp add: returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (\<lambda>_. True) {s. r (Inr v) (xf s)} hs (returnOk v) SKIP proof (prove)
using this:
ccorres_underlying ?sr ?\<Gamma> ?r ?xf ?arrel ?axf (\<lambda>_. True) (UNIV \<inter> {s. ?r ?a (?xf s)}) ?hs (return ?a) SKIP

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (\<lambda>_. True) {s. r (Inr v) (xf s)} hs (returnOk v) SKIP
theory CCorresLemmas

lemma exec_handlers_less:
  "\<lbrakk> \<Gamma> \<turnstile>\<^sub>h \<langle>hs, s'\<rangle> \<Rightarrow> (n, t); t \<notin> range Abrupt \<rbrakk>
       \<Longrightarrow> n < length hs" by (induct rule: exec_handlers.induct, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile>\<^sub>h \<langle>hs,s'\<rangle> \<Rightarrow> (n, t); t \<notin> range Abrupt\<rbrakk> \<Longrightarrow> n < length hs
theory CCorresLemmas

lemma exec_handlers_less2:
  "\<lbrakk> \<Gamma> \<turnstile>\<^sub>h \<langle>hs, s'\<rangle> \<Rightarrow> (n, t); t \<notin> range Abrupt \<rbrakk>
       \<Longrightarrow> \<exists>v. length hs - n = Suc v" apply (drule(1) exec_handlers_less) apply (case_tac "length hs - n", simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile>\<^sub>h \<langle>hs,s'\<rangle> \<Rightarrow> (n, t); t \<notin> range Abrupt\<rbrakk> \<Longrightarrow> \<exists>v. length hs - n = Suc v proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<notin> range Abrupt; n < length hs\<rbrakk> \<Longrightarrow> \<exists>v. length hs - n = Suc v proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma ccorres_seq_skip:
  "ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (Skip ;; c)
       = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a 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 (SKIP;;
c) = 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' (SKIP;;
c) c proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>SKIP;;
c,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma ccorres_expand_while_iff:
  "ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (Cond P (c ;; While P c) Skip) =
   ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (While P 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) SKIP) = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (While P 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) SKIP) (While P c) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond P (c;;
While P c) SKIP,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>While P c,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma fg_consD1:
  "fg_cons xf (xfu \<circ> (\<lambda>x _. x)) \<Longrightarrow> xf (xfu (\<lambda>_. v) s) = v" unfolding fg_cons_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fg_cons xf (xfu \<circ> (\<lambda>x _. x)) \<Longrightarrow> xf (xfu (\<lambda>_. v) s) = v proof (prove)
goal (1 subgoal):
 1. (\<forall>bs v. xf ((xfu \<circ> (\<lambda>x _. x)) bs v) = bs) \<and> (\<forall>bs bs' v. (xfu \<circ> (\<lambda>x _. x)) bs ((xfu \<circ> (\<lambda>x _. x)) bs' v) = (xfu \<circ> (\<lambda>x _. x)) bs v) \<and> (\<forall>v. (xfu \<circ> (\<lambda>x _. x)) (xf v) v = v) \<Longrightarrow> xf (xfu (\<lambda>_. v) s) = v
theory CCorresLemmas

lemma exec_handlers_BasicD [dest?]:
  assumes eh: "\<Gamma> \<turnstile>\<^sub>h \<langle>Basic g # hs, s\<rangle> \<Rightarrow> (n, s')"
  shows "s' = Normal (g s)" using eh by (auto elim: exec_Normal_elim_cases  exec_handlers.cases)

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

goal (1 subgoal):
 1. s' = Normal (g s)
theory CCorresLemmas

lemma ccorres_add_True:
  "ccorres_underlying rf_sr \<Gamma> r xf arrel axf P (P' \<inter> {s. True}) hs a c \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf P P' hs a c" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf P (P' \<inter> \<lbrace>True\<rbrace>) hs a c \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf P P' hs a c
theory CCorresLemmas

lemma ccorres_add_UNIV_Int:
  "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (UNIV \<inter> G') hs a c \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' hs a c" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (UNIV \<inter> G') hs a c \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' hs a c
theory CCorresLemmas

lemma Collect_const_mem:
  "(x \<in> (if P then UNIV else {})) = P" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<in> (if P then UNIV else {})) = P
theory CCorresLemmas

lemma ccorres_cond_univ_iff:
  "ccorres_underlying sr Gamm r xf arrel axf G G' hs a (Cond UNIV x y) = ccorres_underlying sr Gamm r xf arrel axf G G' hs a x" 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 Gamm r xf arrel axf G G' hs a (Cond UNIV x y) = ccorres_underlying sr Gamm r xf arrel axf G G' hs a x proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv Gamm s s' (Cond UNIV x y) x proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> Gamm\<turnstile> \<langle>Cond UNIV x y,Normal s\<rangle> \<Rightarrow> s' = Gamm\<turnstile> \<langle>x,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma ccorres_cond_empty_iff:
  "ccorres_underlying sr Gamm r xf arrel axf G G' hs a (Cond {} y x) = ccorres_underlying sr Gamm r xf arrel axf G G' hs a x" 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 Gamm r xf arrel axf G G' hs a (Cond {} y x) = ccorres_underlying sr Gamm r xf arrel axf G G' hs a x proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv Gamm s s' (Cond {} y x) x proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> Gamm\<turnstile> \<langle>Cond {} y x,Normal s\<rangle> \<Rightarrow> s' = Gamm\<turnstile> \<langle>x,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma vcg_no_global_inv:
  assumes Pginv: "\<And>x t. x \<in> P \<Longrightarrow> g x t (x\<lparr>globals := globals t\<rparr>) \<in> P"
  and        st: "\<forall>Z. \<Gamma>\<turnstile> UNIV Call f UNIV"
  shows "\<Gamma> \<turnstile> P (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y))) P" apply (rule HoarePartial.ProcSpecNoAbrupt [OF _ _ st]) apply simp prefer 2 apply (intro allI) apply (rule HoarePartial.Basic) apply (rule subset_refl) apply clarsimp apply (erule Pginv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> P call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) P proof (prove)
goal (2 subgoals):
 1. P \<subseteq> {s. \<exists>Z. i s \<in> UNIV \<and> (\<forall>t. t \<in> UNIV \<longrightarrow> s\<lparr>globals := globals t\<rparr> \<in> ?R s t)}
 2. \<forall>s t. \<Gamma>\<turnstile> (?R s t) Basic (g s t) P proof (prove)
goal (2 subgoals):
 1. P \<subseteq> {s. \<forall>t. s\<lparr>globals := globals t\<rparr> \<in> ?R s t}
 2. \<forall>s t. \<Gamma>\<turnstile> (?R s t) Basic (g s t) P proof (prove)
goal (2 subgoals):
 1. \<forall>s t. \<Gamma>\<turnstile> (?R s t) Basic (g s t) P
 2. P \<subseteq> {s. \<forall>t. s\<lparr>globals := globals t\<rparr> \<in> ?R s t} proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<Gamma>\<turnstile> (?R s t) Basic (g s t) P
 2. P \<subseteq> {s. \<forall>t. s\<lparr>globals := globals t\<rparr> \<in> ?R s t} proof (prove)
goal (2 subgoals):
 1. \<And>s t. ?R s t \<subseteq> {sa. g s t sa \<in> P}
 2. P \<subseteq> {s. \<forall>t. s\<lparr>globals := globals t\<rparr> \<in> ?R s t} proof (prove)
goal (1 subgoal):
 1. P \<subseteq> {s. \<forall>t. s\<lparr>globals := globals t\<rparr> \<in> {sa. g s t sa \<in> P}} proof (prove)
goal (1 subgoal):
 1. \<And>x t. x \<in> P \<Longrightarrow> g x t (x\<lparr>globals := globals t\<rparr>) \<in> P proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma liftt_if:
  "lift_t g hdv = (\<lambda>p. if (snd hdv),g \<Turnstile>\<^sub>t p then Some (h_val (fst hdv) p) else None)" apply (cases hdv) apply (simp add: lift_t_if split_def cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lift_t g hdv = (\<lambda>p. if snd hdv,g \<Turnstile>\<^sub>t p then Some (h_val (fst hdv) p) else None) proof (prove)
goal (1 subgoal):
 1. \<And>a b. hdv = (a, b) \<Longrightarrow> lift_t g hdv = (\<lambda>p. if snd hdv,g \<Turnstile>\<^sub>t p then Some (h_val (fst hdv) p) else None) proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma clift_h_t_validD:
  "lift_t g hp p = Some x \<Longrightarrow> snd hp,g \<Turnstile>\<^sub>t p" apply (cases hp, simp) apply (erule lift_t_h_t_valid) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lift_t g hp p = Some x \<Longrightarrow> snd hp,g \<Turnstile>\<^sub>t p proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>lift_t g (a, b) p = Some x; hp = (a, b)\<rbrakk> \<Longrightarrow> b,g \<Turnstile>\<^sub>t p proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma sep_conj_dom:
  "((\<lambda>s. dom s = X) \<and>\<^sup>* (\<lambda>s. dom s = Y)) = (\<lambda>s. dom s = X \<union> Y \<and> X \<inter> Y = {})" unfolding sep_conj_def apply (rule ext) apply rule apply (clarsimp simp: map_disj_def) apply (rule_tac x = "s |` X" in exI) apply (rule_tac x = "s |` Y" in exI) apply (clarsimp simp: map_disj_def Int_Un_distrib2) apply (simp add: Int_ac heap_merge_restrict_dom_un Un_ac) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. dom s = X) \<and>\<^sup>* (\<lambda>s. dom s = Y)) = (\<lambda>s. dom s = X \<union> Y \<and> X \<inter> Y = {}) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<exists>s\<^sub>0 s\<^sub>1. s\<^sub>0 \<bottom> s\<^sub>1 \<and> s = s\<^sub>1 ++ s\<^sub>0 \<and> dom s\<^sub>0 = X \<and> dom s\<^sub>1 = Y) = (\<lambda>s. dom s = X \<union> Y \<and> X \<inter> Y = {}) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>s\<^sub>0 s\<^sub>1. s\<^sub>0 \<bottom> s\<^sub>1 \<and> s = s\<^sub>1 ++ s\<^sub>0 \<and> dom s\<^sub>0 = X \<and> dom s\<^sub>1 = Y) = (dom s = X \<union> Y \<and> X \<inter> Y = {}) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<exists>s\<^sub>0 s\<^sub>1. s\<^sub>0 \<bottom> s\<^sub>1 \<and> s = s\<^sub>1 ++ s\<^sub>0 \<and> dom s\<^sub>0 = X \<and> dom s\<^sub>1 = Y \<Longrightarrow> dom s = X \<union> Y \<and> X \<inter> Y = {}
 2. \<And>s. dom s = X \<union> Y \<and> X \<inter> Y = {} \<Longrightarrow> \<exists>s\<^sub>0 s\<^sub>1. s\<^sub>0 \<bottom> s\<^sub>1 \<and> s = s\<^sub>1 ++ s\<^sub>0 \<and> dom s\<^sub>0 = X \<and> dom s\<^sub>1 = Y proof (prove)
goal (1 subgoal):
 1. \<And>s. dom s = X \<union> Y \<and> X \<inter> Y = {} \<Longrightarrow> \<exists>s\<^sub>0 s\<^sub>1. s\<^sub>0 \<bottom> s\<^sub>1 \<and> s = s\<^sub>1 ++ s\<^sub>0 \<and> dom s\<^sub>0 = X \<and> dom s\<^sub>1 = Y proof (prove)
goal (1 subgoal):
 1. \<And>s. dom s = X \<union> Y \<and> X \<inter> Y = {} \<Longrightarrow> \<exists>s\<^sub>1. s|\<^bsub>X\<^esub> \<bottom> s\<^sub>1 \<and> s = s\<^sub>1 ++ (s|\<^bsub>X\<^esub>) \<and> dom (s|\<^bsub>X\<^esub>) = X \<and> dom s\<^sub>1 = Y proof (prove)
goal (1 subgoal):
 1. \<And>s. dom s = X \<union> Y \<and> X \<inter> Y = {} \<Longrightarrow> s|\<^bsub>X\<^esub> \<bottom> s|\<^bsub>Y\<^esub> \<and> s = (s|\<^bsub>Y\<^esub>) ++ (s|\<^bsub>X\<^esub>) \<and> dom (s|\<^bsub>X\<^esub>) = X \<and> dom (s|\<^bsub>Y\<^esub>) = Y proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>dom s = X \<union> Y; X \<inter> Y = {}\<rbrakk> \<Longrightarrow> s = (s|\<^bsub>Y\<^esub>) ++ (s|\<^bsub>X\<^esub>) proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma Diff_Diff_Un_eq: "(A - B) - C = A - (B \<union> C)" by (simp add: Diff_eq Int_ac)

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

lemma Diff_Diff_Un: "(A - B - C) \<union> B = A - C \<union> B" apply (simp add: Diff_eq) apply (subst Un_Int_distrib2) apply (subst Un_Int_distrib2) apply (simp add: Compl_partition2) apply (rule Un_Int_distrib2 [symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A - B - C \<union> B = A - C \<union> B proof (prove)
goal (1 subgoal):
 1. A \<inter> - B \<inter> - C \<union> B = A \<inter> - C \<union> B proof (prove)
goal (1 subgoal):
 1. (A \<inter> - B \<union> B) \<inter> (- C \<union> B) = A \<inter> - C \<union> B proof (prove)
goal (1 subgoal):
 1. (A \<union> B) \<inter> (- B \<union> B) \<inter> (- C \<union> B) = A \<inter> - C \<union> B proof (prove)
goal (1 subgoal):
 1. (A \<union> B) \<inter> (- C \<union> B) = A \<inter> - C \<union> B proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma Diff_Subset_Un_UNIV:
  assumes subset: "B \<subseteq> B'"
  shows "(- B \<union> B') = UNIV" proof - from subset obtain X where "B' = B \<union> X" by auto thus ?thesis by (simp add: Compl_partition2 Un_assoc [symmetric]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - B \<union> B' = UNIV proof (state)
goal (1 subgoal):
 1. - B \<union> B' = UNIV proof (chain)
picking this:
B \<subseteq> B' proof (prove)
using this:
B \<subseteq> B'

goal (1 subgoal):
 1. (\<And>X. B' = B \<union> X \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
B' = B \<union> X

goal (1 subgoal):
 1. - B \<union> B' = UNIV proof (prove)
using this:
B' = B \<union> X

goal (1 subgoal):
 1. - B \<union> B' = UNIV proof (state)
this:
- B \<union> B' = UNIV

goal:
No subgoals!
theory CCorresLemmas

lemma Diff_Diff_Subset_cancel: "B \<subseteq> B' \<Longrightarrow> (A - B - C) \<union> B' = A - C \<union> B'" apply (simp add: Diff_eq) apply (subst Un_Int_distrib2) apply (subst Un_Int_distrib2) apply (simp add: Diff_Subset_Un_UNIV) apply (rule Un_Int_distrib2 [symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. B \<subseteq> B' \<Longrightarrow> A - B - C \<union> B' = A - C \<union> B' proof (prove)
goal (1 subgoal):
 1. B \<subseteq> B' \<Longrightarrow> A \<inter> - B \<inter> - C \<union> B' = A \<inter> - C \<union> B' proof (prove)
goal (1 subgoal):
 1. B \<subseteq> B' \<Longrightarrow> (A \<inter> - B \<union> B') \<inter> (- C \<union> B') = A \<inter> - C \<union> B' proof (prove)
goal (1 subgoal):
 1. B \<subseteq> B' \<Longrightarrow> (A \<union> B') \<inter> (- B \<union> B') \<inter> (- C \<union> B') = A \<inter> - C \<union> B' proof (prove)
goal (1 subgoal):
 1. B \<subseteq> B' \<Longrightarrow> (A \<union> B') \<inter> (- C \<union> B') = A \<inter> - C \<union> B' proof (prove)
goal:
No subgoals!