kings-crown/FVELER_Isabelle huggingface dataset:
theory SIMPL_Lemmas

lemma exec_While_cong:
  "\<lbrakk> \<And>s s'. \<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> s' = \<Gamma> \<turnstile> \<langle>c', Normal s\<rangle> \<Rightarrow> s' \<rbrakk>
       \<Longrightarrow> \<Gamma> \<turnstile> \<langle>While S c, Normal s\<rangle> \<Rightarrow> s' = \<Gamma> \<turnstile> \<langle>While S c', Normal s\<rangle> \<Rightarrow> s'" apply (rule iffI) apply (erule(1) exec_While_cong'[OF _ _ refl refl]) apply (erule(1) exec_While_cong'[OF sym _ refl refl]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s s'. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> s') \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While S c,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>While S c',Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s s'. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>While S c,Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While S c',Normal s\<rangle> \<Rightarrow> s'
 2. \<lbrakk>\<And>s s'. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>While S c',Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While S c,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s s'. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>While S c',Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While S c,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory SIMPL_Lemmas

lemma exec_Guard_UNIV_simp:
  "\<Gamma> \<turnstile> \<langle>Guard F UNIV c, Normal s\<rangle> \<Rightarrow> s' = \<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> s'" by (auto elim!: exec_Normal_elim_cases intro: exec.intros)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Guard F UNIV c,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'
theory SIMPL_Lemmas

lemma hoarep_exec_gen:
  assumes h: "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/F s\<^esub> (P s) c (Q s),(A s)"
  assumes e: "\<Gamma>\<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> t"
  shows "s \<in> P x \<longrightarrow> (\<exists>f \<in> F x. t = Fault f) \<or> (\<exists>t' \<in> Q x. t = Normal t') \<or> (\<exists>t' \<in> A x. t = Abrupt t')" by (rule impI, erule hoarep_exec[OF _ e spec[OF h]])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<in> P x \<longrightarrow> (\<exists>f\<in>F x. t = Fault f) \<or> (\<exists>t'\<in>Q x. t = Normal t') \<or> (\<exists>t'\<in>A x. t = Abrupt t')
theory SIMPL_Lemmas

lemma guard_is_UNIVI:
  "(\<And>s rv. r rv (xf s) \<Longrightarrow> s \<in> Q rv (xf s)) \<Longrightarrow> guard_is_UNIV r xf Q" unfolding guard_is_UNIV_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s rv. r rv (xf s) \<Longrightarrow> s \<in> Q rv (xf s)) \<Longrightarrow> guard_is_UNIV r xf Q proof (prove)
goal (1 subgoal):
 1. (\<And>s rv. r rv (xf s) \<Longrightarrow> s \<in> Q rv (xf s)) \<Longrightarrow> \<forall>s rv. r rv (xf s) \<longrightarrow> s \<in> Q rv (xf s)
theory SIMPL_Lemmas

lemma guard_is_UNIVD:
  "\<lbrakk> guard_is_UNIV r xf Q; r rv (xf s) \<rbrakk> \<Longrightarrow> s \<in> Q rv (xf s)" unfolding guard_is_UNIV_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>guard_is_UNIV r xf Q; r rv (xf s)\<rbrakk> \<Longrightarrow> s \<in> Q rv (xf s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s rv. r rv (xf s) \<longrightarrow> s \<in> Q rv (xf s); r rv (xf s)\<rbrakk> \<Longrightarrow> s \<in> Q rv (xf s)
theory SIMPL_Lemmas

lemma isNormal_simps:
  "isNormal (Normal s) = True"
  "isNormal (Abrupt s) = False"
  "isNormal (Fault f) = False"
  "isNormal Stuck = False" by (auto simp add: isNormal_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (isNormal (Normal s) = True &&& isNormal (Abrupt s) = False) &&& isNormal (Fault f) = False &&& isNormal Stuck = False
theory SIMPL_Lemmas

lemma intermediate_Normal_state:
  "\<lbrakk>\<Gamma> \<turnstile> \<langle>Seq c\<^sub>1 c\<^sub>2, Normal t\<rangle> \<Rightarrow> t''; t \<in> P; \<Gamma> \<turnstile> P c\<^sub>1 Q\<rbrakk>
   \<Longrightarrow> \<exists>t'. \<Gamma> \<turnstile> \<langle>c\<^sub>1, Normal t\<rangle> \<Rightarrow> Normal t' \<and> \<Gamma> \<turnstile> \<langle>c\<^sub>2, Normal t'\<rangle> \<Rightarrow> t''" apply (erule exec_Normal_elim_cases(8)) apply (insert hoarep_exec) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1;;
c\<^sub>2,Normal t\<rangle> \<Rightarrow> t''; t \<in> P; \<Gamma>\<turnstile> P c\<^sub>1 Q\<rbrakk> \<Longrightarrow> \<exists>t'. \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal t\<rangle> \<Rightarrow> Normal t' \<and> \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal t'\<rangle> \<Rightarrow> t'' proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>t \<in> P; \<Gamma>\<turnstile> P c\<^sub>1 Q; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t''\<rbrakk> \<Longrightarrow> \<exists>t'. \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal t\<rangle> \<Rightarrow> Normal t' \<and> \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal t'\<rangle> \<Rightarrow> t'' proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>t \<in> P; \<Gamma>\<turnstile> P c\<^sub>1 Q; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal t\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t''; \<And>s P \<Gamma> c t F Q A. \<lbrakk>s \<in> P; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,A\<rbrakk> \<Longrightarrow> (\<exists>f\<in>F. t = Fault f) \<or> (\<exists>t'\<in>Q. t = Normal t') \<or> (\<exists>t'\<in>A. t = Abrupt t')\<rbrakk> \<Longrightarrow> \<exists>t'. \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal t\<rangle> \<Rightarrow> Normal t' \<and> \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal t'\<rangle> \<Rightarrow> t'' proof (prove)
goal:
No subgoals!
theory SIMPL_Lemmas

lemma hoarep_ex_pre:
  "(\<And>x. \<Gamma> \<turnstile> {s. P x s} c Q) \<Longrightarrow> \<Gamma> \<turnstile> {s. \<exists>x. P x s} c Q" apply (rule hoare_complete) apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) apply (fastforce dest: hoarep_exec'[rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<Gamma>\<turnstile> {s. P x s} c Q) \<Longrightarrow> \<Gamma>\<turnstile> {s. \<exists>x. P x s} c Q proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<Gamma>\<turnstile> {s. P x s} c Q) \<Longrightarrow> \<Gamma>\<Turnstile>\<^bsub>/{}\<^esub> {s. \<exists>x. P x s} c Q,{} proof (prove)
goal (1 subgoal):
 1. \<And>t x xa. \<lbrakk>\<And>x. \<Gamma>\<turnstile> (Collect (P x)) c Q; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; P xa x\<rbrakk> \<Longrightarrow> t \<in> Normal ` Q proof (prove)
goal:
No subgoals!
theory SIMPL_Lemmas

lemma hoarep_ex_lift:
  "(\<And>x. \<Gamma> \<turnstile> {s. P x s} c {s. Q x s}) \<Longrightarrow> \<Gamma> \<turnstile> {s. \<exists>x. P x s} c {s. \<exists>x. Q x s}" apply (rule hoare_complete) apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) apply (rename_tac s x) apply (drule_tac x=x in meta_spec) apply (prop_tac "s \<in> Collect (P x)") apply fastforce apply (frule (2) hoarep_exec) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<Gamma>\<turnstile> {s. P x s} c {s. Q x s}) \<Longrightarrow> \<Gamma>\<turnstile> {s. \<exists>x. P x s} c {s. \<exists>x. Q x s} proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<Gamma>\<turnstile> {s. P x s} c {s. Q x s}) \<Longrightarrow> \<Gamma>\<Turnstile>\<^bsub>/{}\<^esub> {s. \<exists>x. P x s} c {s. \<exists>x. Q x s},{} proof (prove)
goal (1 subgoal):
 1. \<And>t x xa. \<lbrakk>\<And>x. \<Gamma>\<turnstile> (Collect (P x)) c (Collect (Q x)); \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; P xa x\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. \<exists>x. Q x s} proof (prove)
goal (1 subgoal):
 1. \<And>t s x. \<lbrakk>\<And>x. \<Gamma>\<turnstile> (Collect (P x)) c (Collect (Q x)); \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; P x s\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. \<exists>x. Q x s} proof (prove)
goal (1 subgoal):
 1. \<And>t s x. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; P x s; \<Gamma>\<turnstile> (Collect (P x)) c (Collect (Q x))\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. \<exists>x. Q x s} proof (prove)
goal (2 subgoals):
 1. \<And>t s x. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; P x s; \<Gamma>\<turnstile> (Collect (P x)) c (Collect (Q x))\<rbrakk> \<Longrightarrow> s \<in> Collect (P x)
 2. \<And>t s x. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; P x s; \<Gamma>\<turnstile> (Collect (P x)) c (Collect (Q x)); s \<in> Collect (P x)\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. \<exists>x. Q x s} proof (prove)
goal (1 subgoal):
 1. \<And>t s x. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; P x s; \<Gamma>\<turnstile> (Collect (P x)) c (Collect (Q x)); s \<in> Collect (P x)\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. \<exists>x. Q x s} proof (prove)
goal (1 subgoal):
 1. \<And>t s x. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; P x s; \<Gamma>\<turnstile> (Collect (P x)) c (Collect (Q x)); s \<in> Collect (P x); (\<exists>f\<in>{}. t = Fault f) \<or> (\<exists>t'\<in>Collect (Q x). t = Normal t') \<or> (\<exists>t'\<in>{}. t = Abrupt t')\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. \<exists>x. Q x s} proof (prove)
goal:
No subgoals!
theory SIMPL_Lemmas

lemma hoarep_conj_lift_pre_fix:
  "\<lbrakk>\<Gamma> \<turnstile> P c {s. Q s}; \<Gamma> \<turnstile> P c {s. Q' s}\<rbrakk>
   \<Longrightarrow> \<Gamma> \<turnstile> P c {s. Q s \<and> Q' s}" apply (rule hoare_complete) apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) apply (frule (2) hoarep_exec[where Q="Collect Q"]) apply (frule (2) hoarep_exec[where Q="Collect Q'"]) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> P c {s. Q s}; \<Gamma>\<turnstile> P c {s. Q' s}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> P c {s. Q s \<and> Q' s} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> P c {s. Q s}; \<Gamma>\<turnstile> P c {s. Q' s}\<rbrakk> \<Longrightarrow> \<Gamma>\<Turnstile>\<^bsub>/{}\<^esub> P c {s. Q s \<and> Q' s},{} proof (prove)
goal (1 subgoal):
 1. \<And>t x. \<lbrakk>\<Gamma>\<turnstile> P c (Collect Q); \<Gamma>\<turnstile> P c (Collect Q'); \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; x \<in> P\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. Q s \<and> Q' s} proof (prove)
goal (1 subgoal):
 1. \<And>t x. \<lbrakk>\<Gamma>\<turnstile> P c (Collect Q); \<Gamma>\<turnstile> P c (Collect Q'); \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; x \<in> P; (\<exists>f\<in>{}. t = Fault f) \<or> (\<exists>t'\<in>Collect Q. t = Normal t') \<or> (\<exists>t'\<in>{}. t = Abrupt t')\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. Q s \<and> Q' s} proof (prove)
goal (1 subgoal):
 1. \<And>t x. \<lbrakk>\<Gamma>\<turnstile> P c (Collect Q); \<Gamma>\<turnstile> P c (Collect Q'); \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; x \<in> P; (\<exists>f\<in>{}. t = Fault f) \<or> (\<exists>t'\<in>Collect Q. t = Normal t') \<or> (\<exists>t'\<in>{}. t = Abrupt t'); (\<exists>f\<in>{}. t = Fault f) \<or> (\<exists>t'\<in>Collect Q'. t = Normal t') \<or> (\<exists>t'\<in>{}. t = Abrupt t')\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. Q s \<and> Q' s} proof (prove)
goal:
No subgoals!
theory SIMPL_Lemmas

lemma exec_While_final_inv'':
  "\<lbrakk> \<Gamma> \<turnstile> \<langle>b, x\<rangle> \<Rightarrow> s'; b = While C B; x = Normal s;
    \<And>s. s \<notin> C \<Longrightarrow> I s (Normal s);
    \<And>t t' t''. \<lbrakk> t \<in> C; \<Gamma>\<turnstile> \<langle>B, Normal t\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>While C B, Normal t'\<rangle> \<Rightarrow> t'';
                 I t' t'' \<rbrakk> \<Longrightarrow> I t t'';
    \<And>t t'. \<lbrakk> t \<in> C; \<Gamma>\<turnstile> \<langle>B, Normal t\<rangle> \<Rightarrow> Abrupt t' \<rbrakk> \<Longrightarrow> I t (Abrupt t');
    \<And>t. \<lbrakk> t \<in> C; \<Gamma> \<turnstile> \<langle>B, Normal t\<rangle> \<Rightarrow> Stuck \<rbrakk> \<Longrightarrow> I t Stuck;
    \<And>t f. \<lbrakk> t \<in> C; \<Gamma>\<turnstile> \<langle>B, Normal t\<rangle> \<Rightarrow> Fault f \<rbrakk> \<Longrightarrow> I t (Fault f) \<rbrakk>
   \<Longrightarrow> I s s'" apply (induct arbitrary: s rule: exec.induct; simp) apply (erule exec_elim_cases; fastforce simp: exec.WhileTrue exec.WhileFalse) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> \<langle>b,x\<rangle> \<Rightarrow> s'; b = While C B; x = Normal s; \<And>s. s \<notin> C \<Longrightarrow> I s (Normal s); \<And>t t' t''. \<lbrakk>t \<in> C; \<Gamma>\<turnstile> \<langle>B,Normal t\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>While C B,Normal t'\<rangle> \<Rightarrow> t''; I t' t''\<rbrakk> \<Longrightarrow> I t t''; \<And>t t'. \<lbrakk>t \<in> C; \<Gamma>\<turnstile> \<langle>B,Normal t\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> I t (Abrupt t'); \<And>t. \<lbrakk>t \<in> C; \<Gamma>\<turnstile> \<langle>B,Normal t\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> I t Stuck; \<And>t f. \<lbrakk>t \<in> C; \<Gamma>\<turnstile> \<langle>B,Normal t\<rangle> \<Rightarrow> Fault f\<rbrakk> \<Longrightarrow> I t (Fault f)\<rbrakk> \<Longrightarrow> I s s' proof (prove)
goal (1 subgoal):
 1. \<And>s b s' t sa. \<lbrakk>sa \<in> C; \<Gamma>\<turnstile> \<langle>B,Normal sa\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>While C B,s'\<rangle> \<Rightarrow> t; \<And>s. s' = Normal s \<Longrightarrow> I s t; b = C; s = sa; \<And>s. s \<notin> C \<Longrightarrow> I s (Normal s); \<And>t t' t''. \<lbrakk>t \<in> C; \<Gamma>\<turnstile> \<langle>B,Normal t\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>While C B,Normal t'\<rangle> \<Rightarrow> t''; I t' t''\<rbrakk> \<Longrightarrow> I t t''; \<And>t t'. \<lbrakk>t \<in> C; \<Gamma>\<turnstile> \<langle>B,Normal t\<rangle> \<Rightarrow> Abrupt t'\<rbrakk> \<Longrightarrow> I t (Abrupt t'); \<And>t. \<lbrakk>t \<in> C; \<Gamma>\<turnstile> \<langle>B,Normal t\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> I t Stuck; \<And>t f. \<lbrakk>t \<in> C; \<Gamma>\<turnstile> \<langle>B,Normal t\<rangle> \<Rightarrow> Fault f\<rbrakk> \<Longrightarrow> I t (Fault f)\<rbrakk> \<Longrightarrow> I sa t proof (prove)
goal:
No subgoals!
theory SIMPL_Lemmas

lemma While_inv_from_body:
  "\<Gamma> \<turnstile> (G \<inter> C) B G \<Longrightarrow> \<Gamma> \<turnstile> G While C B G" apply (drule hoare_sound)+ apply (rule hoare_complete) apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) by (erule exec_While_final_inv''[where I="\<lambda>s s'. s \<in> G \<longrightarrow> s' \<in> Normal ` G", THEN impE],
      fastforce+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (G \<inter> C) B G \<Longrightarrow> \<Gamma>\<turnstile> G While C B G proof (prove)
goal (1 subgoal):
 1. \<Gamma>,{}\<Turnstile>\<^bsub>/{}\<^esub> (G \<inter> C) B G,{} \<Longrightarrow> \<Gamma>\<turnstile> G While C B G proof (prove)
goal (1 subgoal):
 1. \<Gamma>,{}\<Turnstile>\<^bsub>/{}\<^esub> (G \<inter> C) B G,{} \<Longrightarrow> \<Gamma>\<Turnstile>\<^bsub>/{}\<^esub> G While C B G,{} proof (prove)
goal (1 subgoal):
 1. \<And>t x. \<lbrakk>\<forall>s t. \<Gamma>\<turnstile> \<langle>B,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` (G \<inter> C) \<longrightarrow> t \<in> Normal ` G; \<Gamma>\<turnstile> \<langle>While C B,Normal x\<rangle> \<Rightarrow> t; x \<in> G\<rbrakk> \<Longrightarrow> t \<in> Normal ` G
theory Corres_UL_C

lemma unif_rrel_simps:
  "unif_rrel True rrel xf arrel axf = (\<lambda>x s. rrel x (xf s))"
  "unif_rrel False rrel xf arrel axf = (\<lambda>x s. arrel x (axf s))" by (simp add: unif_rrel_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unif_rrel True rrel xf arrel axf = (\<lambda>x s. rrel x (xf s)) &&& unif_rrel False rrel xf arrel axf = (\<lambda>x s. arrel x (axf s))
theory Corres_UL_C

lemma ccorres_prog_only_cong:
  "\<lbrakk> m=m'; c=c' \<rbrakk> \<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'" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m = m'; c = c'\<rbrakk> \<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'
theory Corres_UL_C

lemma exec_handlers_Cons_le[simplified]:
  "\<Gamma> \<turnstile>\<^sub>h \<langle>h # hs, s'\<rangle> \<Rightarrow> (n, t) \<Longrightarrow> n \<le> length (tl (h # hs))" by (induct rule: exec_handlers.induct, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^sub>h \<langle>h # hs,s'\<rangle> \<Rightarrow> (n, t) \<Longrightarrow> n \<le> length (tl (h # hs))
theory Corres_UL_C

lemma exec_handlers_le:
  "\<Gamma> \<turnstile>\<^sub>h \<langle>hs, s'\<rangle> \<Rightarrow> (n, t) \<Longrightarrow> n \<le> length hs" by (induct rule: exec_handlers.induct, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^sub>h \<langle>hs,s'\<rangle> \<Rightarrow> (n, t) \<Longrightarrow> n \<le> length hs
theory Corres_UL_C

lemma ccorresE_gets_the:
  "\<lbrakk>ccorresG srel \<Gamma> rrel xf G G' hs (gets_the c) c'; (s, s') \<in> srel; G s; s' \<in> G'; no_ofail G c;
    \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs, s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk>
   \<Longrightarrow> (s, t') \<in> srel \<and> rrel (the (c s)) (xf t')" by (fastforce simp: ccorres_underlying_def no_ofail_def unif_rrel_def gets_the_def gets_def
                      get_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorresG srel \<Gamma> rrel xf G G' hs (gets_the c) c'; (s, s') \<in> srel; G s; s' \<in> G'; no_ofail G c; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, Normal t')\<rbrakk> \<Longrightarrow> (s, t') \<in> srel \<and> rrel (the (c s)) (xf t')
theory Corres_UL_C

lemma ccorres_from_vcg_nofail:
  "(\<forall>\<sigma>. \<Gamma> \<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> srel}
  c
  {s. \<not> snd (a \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>') \<in> fst (a \<sigma>). (\<sigma>', s) \<in> srel \<and> rrel rv (xf s))})
  \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' hs a c" apply (rule ccorres_from_vcg_nofail2) apply (erule allEI) apply (case_tac "snd (a \<sigma>)", simp_all) apply (rule hoare_complete, simp add: HoarePartialDef.valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> srel} c {s. \<not> snd (a \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> srel \<and> rrel rv (xf s))} \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' hs a c proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> srel} c {s. \<not> snd (a \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> srel \<and> rrel rv (xf s))} \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> srel \<and> \<not> snd (a \<sigma>)} c {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> srel \<and> rrel rv (xf s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> srel} c {s. \<not> snd (a \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> srel \<and> rrel rv (xf s))} \<Longrightarrow> \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> srel \<and> \<not> snd (a \<sigma>)} c {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> srel \<and> rrel rv (xf s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> srel} c UNIV; snd (a \<sigma>)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {} c {s. \<exists>x\<in>fst (a \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> srel \<and> rrel rv (xf s)} proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_to_vcg_Normal:
  "\<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; no_fail Q a\<rbrakk>
   \<Longrightarrow> \<Gamma> \<turnstile> {s'. P s \<and> Q s \<and> s' \<in> P' \<and> (s, s') \<in> srel} c UNIV" apply (frule (1) ccorres_to_vcg_with_prop[where R="\<top>\<top>" and s=s]) apply wpsimp apply (fastforce elim: conseqPost) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; no_fail Q a\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s'. P s \<and> Q s \<and> s' \<in> P' \<and> (s, s') \<in> srel} c UNIV proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; no_fail Q a\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; no_fail Q a; \<Gamma>\<turnstile> {s'. P s \<and> Q s \<and> s' \<in> P' \<and> (s, s') \<in> srel} c {t'. \<exists>(rv, t)\<in>fst (a s). (t, t') \<in> srel \<and> rrel rv (xf t') \<and> True}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s'. P s \<and> Q s \<and> s' \<in> P' \<and> (s, s') \<in> srel} c UNIV proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; no_fail Q a; \<Gamma>\<turnstile> {s'. P s \<and> Q s \<and> s' \<in> P' \<and> (s, s') \<in> srel} c {t'. \<exists>(rv, t)\<in>fst (a s). (t, t') \<in> srel \<and> rrel rv (xf t') \<and> True}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s'. P s \<and> Q s \<and> s' \<in> P' \<and> (s, s') \<in> srel} c UNIV proof (prove)
goal:
No subgoals!