kings-crown/FVELER_Isabelle huggingface dataset:
theory AutoCorres_C

lemma [terminates_trivial]:
  fixes \<Gamma> return init shows
  "\<lbrakk> \<And>s. \<Gamma> \<turnstile> Call p \<down> Normal s; \<And>s t u. \<Gamma> \<turnstile> c s t \<down> Normal u \<rbrakk> \<Longrightarrow>
   \<Gamma> \<turnstile> call init p return c \<down> Normal s" apply (case_tac "\<Gamma> p") apply (erule terminates_callUndefined) apply (fastforce simp: terminates_Call_body intro: terminates_call) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<Gamma>\<turnstile>Call p \<down> Normal s; \<And>s t u. \<Gamma>\<turnstile>c s t \<down> Normal u\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>call init p return c \<down> Normal s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. \<Gamma>\<turnstile>Call p \<down> Normal s; \<And>s t u. \<Gamma>\<turnstile>c s t \<down> Normal u; \<Gamma> p = None\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>call init p return c \<down> Normal s
 2. \<And>a. \<lbrakk>\<And>s. \<Gamma>\<turnstile>Call p \<down> Normal s; \<And>s t u. \<Gamma>\<turnstile>c s t \<down> Normal u; \<Gamma> p = Some a\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>call init p return c \<down> Normal s proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>s. \<Gamma>\<turnstile>Call p \<down> Normal s; \<And>s t u. \<Gamma>\<turnstile>c s t \<down> Normal u; \<Gamma> p = Some a\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>call init p return c \<down> Normal s proof (prove)
goal:
No subgoals!
theory AutoCorres_C

lemma condition_const: "condition (\<lambda>_. P) L R = (if P then L else R)" by (simp add: condition_def split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. condition (\<lambda>_. P)
  L
  R = (if P then L else R)
theory AutoCorres_C

lemma errstate_errglobals:
  "errstate s' = errglobals (globals s')" by (auto simp: errstate_def errglobals_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. errstate s' = errglobals (globals s')
theory AutoCorres_C

lemma errglobals_simps [simp]:
  "errfault (errglobals s) = seL4_Fault_lift (current_fault_' s)"
  "errlookup_fault (errglobals s) = lookup_fault_lift (current_lookup_fault_' s)"
  "errsyscall (errglobals s) = current_syscall_error_' s" by (auto simp: errglobals_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. errfault (errglobals s) = seL4_Fault_lift (current_fault_' s) &&& errlookup_fault (errglobals s) = lookup_fault_lift (current_lookup_fault_' s) &&& errsyscall (errglobals s) = current_syscall_error_' s
theory AutoCorres_C

lemma corres_to_ccorres_rv_spec_liftxf:
  assumes ac: "ac_corres globals check_term \<Gamma> ret_xf G (liftE ac) c"
  assumes cu:
    "corres_underlying
      {(s,s'). cstate_relation s s'} True True (lift_rv ef vf elf R' E)
      P Q a (do r' \<leftarrow> ac; e' \<leftarrow> gets exf; return (r',e') od)"
  assumes "\<And>s'. esf (errstate s') = elf (exf (globals s'))"
  assumes "\<And>e f e'. E' e f e' = E e f (esf e')"
  assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> P s \<and> Q (globals s')"
  assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> G s'"
  shows "ccorres (E' \<currency> R') (liftxf errstate ef vf ret_xf) P' Q' [] a c" apply (rule corres_to_ccorres_extra_globals_rv_spec[OF _ _ corres_rel_imp, OF rf_sr_def ac cu]) apply (all \<open>clarsimp simp: assms(5-6) liftxf_def\<close>) apply (clarsimp simp: lift_rv_def liftxf_def assms(3-4) split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (E' \<currency> R') (liftxf errstate ef vf ret_xf) P' Q' [] a c proof (prove)
goal (3 subgoals):
 1. \<And>x y. lift_rv ef vf elf R' E x y \<Longrightarrow> case y of (xa, y) \<Rightarrow> \<forall>s'. xa = ret_xf s' \<and> y = exf (globals s') \<longrightarrow> (E' \<currency> R') x (liftxf errstate ef vf ret_xf s')
 2. \<And>s s'. \<lbrakk>cstate_relation s (globals s'); P' s \<and> s' \<in> Q'\<rbrakk> \<Longrightarrow> P s \<and> Q (globals s')
 3. \<And>s s'. \<lbrakk>cstate_relation s (globals s'); P' s \<and> s' \<in> Q'\<rbrakk> \<Longrightarrow> G s' proof (prove)
goal (1 subgoal):
 1. \<And>x s'. lift_rv ef vf elf R' E x (ret_xf s', exf (globals s')) \<Longrightarrow> (E' \<currency> R') x \<lparr>exflag = ef (ret_xf s'), exstate = errstate s', exvalue = vf (ret_xf s')\<rparr> proof (prove)
goal:
No subgoals!
theory AutoCorres_C

lemma lift_rv_returnOk:
  assumes "ef r = scast EXCEPTION_NONE"
  assumes "R rv (vf r)"
  shows "corres_underlying
           {(x, y). cstate_relation x y} True True (lift_rv ef vf elf R E) \<top> \<top>
           (returnOk rv)
           (do e' \<leftarrow> gets exf; return (r, e') od)" apply (clarsimp simp: corres_underlying_def snd_bind snd_modify snd_gets in_monad) apply (rule bexI[of _ "(Inr rv, s)" for s]; simp add: in_monad lift_rv_def assms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying {(x, y). cstate_relation x y} True True (lift_rv ef vf elf R E) (\<lambda>_. True) (\<lambda>_. True) (returnOk rv) (do e' <- gets exf;
return (r, e')
od) proof (prove)
goal (1 subgoal):
 1. \<And>a b. cstate_relation a b \<Longrightarrow> \<exists>x\<in>fst (returnOk rv a). case x of (ra, t) \<Rightarrow> cstate_relation t b \<and> lift_rv ef vf elf R E ra (r, exf b) proof (prove)
goal:
No subgoals!
theory AutoCorres_C

lemma lift_rv_throwError':
  assumes "\<And>s s'. cstate_relation s s' \<longrightarrow> cstate_relation s (esu s')"
  assumes "ef r \<noteq> scast EXCEPTION_NONE"
  assumes "\<And>err'. E err (ef r) (elf (exf (esu err')))"
  shows "corres_underlying
           {(x, y). cstate_relation x y} True True (lift_rv ef vf elf R E) \<top> \<top>
           (throwError err)
           (do _ \<leftarrow> modify esu; e' \<leftarrow> gets exf; return (r, e') od)" apply (clarsimp simp: corres_underlying_def snd_bind snd_modify snd_gets in_monad) apply (rule bexI[of _ "(Inl err, s)" for s]; simp add: in_monad lift_rv_def assms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying {(x, y). cstate_relation x y} True True (lift_rv ef vf elf R E) (\<lambda>_. True) (\<lambda>_. True) (throwError err) (do _ <- modify esu;
e' <- gets exf;
return (r, e')
od) proof (prove)
goal (1 subgoal):
 1. \<And>a b. cstate_relation a b \<Longrightarrow> \<exists>x\<in>fst (throwError err a). case x of (ra, t) \<Rightarrow> cstate_relation t (esu b) \<and> lift_rv ef vf elf R E ra (r, exf (esu b)) proof (prove)
goal:
No subgoals!
theory AutoCorres_C

lemma cstate_relation_errglobals_updates:
  "cstate_relation s s' \<longrightarrow> cstate_relation s (current_fault_'_update f s')"
  "cstate_relation s s' \<longrightarrow> cstate_relation s (current_lookup_fault_'_update lf s')"
  "cstate_relation s s' \<longrightarrow> cstate_relation s (current_syscall_error_'_update sce s')" by (auto simp: cstate_relation_def carch_state_relation_def cmachine_state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cstate_relation s s' \<longrightarrow> cstate_relation s (current_fault_'_update f s') &&& cstate_relation s s' \<longrightarrow> cstate_relation s (current_lookup_fault_'_update lf s') &&& cstate_relation s s' \<longrightarrow> cstate_relation s (current_syscall_error_'_update sce s')
theory AutoCorres_C

lemma valid_spec_to_wp:
  assumes "\<And>\<sigma>. \<lbrace> \<lambda>s. s = \<sigma> \<and> P s \<rbrace> f \<lbrace> \<lambda>r s. s = \<sigma> \<and> R r s \<rbrace>"
  shows "\<lbrace> \<lambda>s. P s \<and> (\<forall>r. R r s \<longrightarrow> Q r s) \<rbrace> f \<lbrace> Q \<rbrace>" using assms by (fastforce simp: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<and> (\<forall>r. R r s \<longrightarrow> Q r s)\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
using this:
\<lbrace>\<lambda>s. s = ?\<sigma>1 \<and> P s\<rbrace> f \<lbrace>\<lambda>r s. s = ?\<sigma>1 \<and> R r s\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<and> (\<forall>r. R r s \<longrightarrow> Q r s)\<rbrace> f \<lbrace>Q\<rbrace>
theory AutoCorres_C

lemma spec_result_Normal:
  fixes \<Gamma>
  assumes p_spec: "\<forall>s. \<Gamma>,{} \<turnstile> {s'. s = s' \<and> P s s'} p (Q s)"
  shows "\<forall>s t. P s s \<longrightarrow> \<Gamma> \<turnstile> \<langle>p, Normal s\<rangle> \<Rightarrow> t \<longrightarrow> t \<in> range Normal" by (rule all_forward[OF p_spec], drule hoare_sound)
     (auto simp: cvalid_def HoarePartialDef.valid_def image_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s t. P s s \<longrightarrow> \<Gamma>\<turnstile> \<langle>p,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> t \<in> range Normal
theory AutoCorres_C

lemma valid_spec_to_corres_symb_exec_r:
  assumes spec': "\<And>\<sigma>. \<lbrace> \<lambda>s. s = \<sigma> \<and> P' s \<rbrace> f \<lbrace> \<lambda>r s. s = \<sigma> \<and> Q' r s \<rbrace>"
  assumes nf: "nf' \<Longrightarrow> no_fail N' f"
  assumes corres_rv: "\<And>rv'. corres_underlying sr nf nf' r P (R' rv') a (c rv')"
  shows "corres_underlying sr nf nf' r P (\<lambda>s. N' s \<and> P' s \<and> (\<forall>r. Q' r s \<longrightarrow> R' r s)) a (f >>= c)" by (rule corres_symb_exec_r[OF corres_rv])
     (wpsimp wp: valid_spec_to_wp[OF spec'] nf)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P (\<lambda>s. N' s \<and> P' s \<and> (\<forall>r. Q' r s \<longrightarrow> R' r s)) a (f >>= c)
theory AutoCorres_C

lemma valid_spec_to_corres_gen_symb_exec_r:
  assumes spec': "\<And>\<sigma>. \<lbrace> \<lambda>s. s = \<sigma> \<and> P' s \<rbrace> f \<lbrace> \<lambda>r s. s = \<sigma> \<and> Q' r \<rbrace>"
  assumes nf: "nf' \<Longrightarrow> no_fail N' f"
  assumes corres_rv: "\<And>rv'. Q' rv' \<Longrightarrow> corres_underlying sr nf nf' r P (R' rv') a (c rv')"
  shows "corres_underlying sr nf nf' r P (\<lambda>s. N' s \<and> P' s \<and> (\<forall>r. Q' r \<longrightarrow> R' r s)) a (f >>= c)" by (rule corres_symb_exec_r, rule_tac F="Q' rv" in corres_gen_asm2, erule corres_rv)
     (wpsimp wp: valid_spec_to_wp[OF spec'] nf)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P (\<lambda>s. N' s \<and> P' s \<and> (\<forall>r. Q' r \<longrightarrow> R' r s)) a (f >>= c)
theory AutoCorres_C

lemma corres_stateAssert_l:
  assumes "corres_underlying sr nf nf' r P P' (a ()) c"
  shows "corres_underlying sr nf nf' r
                           (\<lambda>s. (\<not> nf \<longrightarrow> Q s) \<and> (Q s \<longrightarrow> P s)) P'
                           (stateAssert Q bs >>= a) c" apply (rule corres_guard_imp[OF corres_symb_exec_l''[where P="\<lambda>s. nf \<or> Q s"]]) using assms apply simp apply (wpsimp simp: stateAssert_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (\<lambda>s. (\<not> nf \<longrightarrow> Q s) \<and> (Q s \<longrightarrow> P s)) P' (stateAssert Q bs >>= a) c proof (prove)
goal (7 subgoals):
 1. \<And>rv. corres_underlying sr nf nf' r (?R1 rv) (?R'1 rv) (a rv) c
 2. \<And>s. nf \<or> Q s \<Longrightarrow> \<lbrace>(=) s\<rbrace> stateAssert Q bs \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q1\<rbrace> stateAssert Q bs \<lbrace>?R1\<rbrace>
 4. \<not> nf \<longrightarrow> no_fail (\<lambda>s. nf \<or> Q s) (stateAssert Q bs)
 5. empty_fail (stateAssert Q bs)
 6. \<And>s. (\<not> nf \<longrightarrow> Q s) \<and> (Q s \<longrightarrow> P s) \<Longrightarrow> ((\<lambda>s. nf \<or> Q s) and ?Q1) s
 7. \<And>s. P' s \<Longrightarrow> \<forall>rv sa. (sa, s) \<in> sr \<and> ?R1 rv sa \<longrightarrow> ?R'1 rv s proof (prove)
using this:
corres_underlying sr nf nf' r P P' (a ()) c

goal (7 subgoals):
 1. \<And>rv. corres_underlying sr nf nf' r (?R1 rv) (?R'1 rv) (a rv) c
 2. \<And>s. nf \<or> Q s \<Longrightarrow> \<lbrace>(=) s\<rbrace> stateAssert Q bs \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q1\<rbrace> stateAssert Q bs \<lbrace>?R1\<rbrace>
 4. \<not> nf \<longrightarrow> no_fail (\<lambda>s. nf \<or> Q s) (stateAssert Q bs)
 5. empty_fail (stateAssert Q bs)
 6. \<And>s. (\<not> nf \<longrightarrow> Q s) \<and> (Q s \<longrightarrow> P s) \<Longrightarrow> ((\<lambda>s. nf \<or> Q s) and ?Q1) s
 7. \<And>s. P' s \<Longrightarrow> \<forall>rv sa. (sa, s) \<in> sr \<and> ?R1 rv sa \<longrightarrow> ?R'1 rv s proof (prove)
goal (6 subgoals):
 1. \<And>s. nf \<or> Q s \<Longrightarrow> \<lbrace>(=) s\<rbrace> stateAssert Q bs \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrace>?Q1\<rbrace> stateAssert Q bs \<lbrace>\<lambda>a. P\<rbrace>
 3. \<not> nf \<longrightarrow> no_fail (\<lambda>s. nf \<or> Q s) (stateAssert Q bs)
 4. empty_fail (stateAssert Q bs)
 5. \<And>s. (\<not> nf \<longrightarrow> Q s) \<and> (Q s \<longrightarrow> P s) \<Longrightarrow> ((\<lambda>s. nf \<or> Q s) and ?Q1) s
 6. \<And>s. P' s \<Longrightarrow> \<forall>rv sa. (sa, s) \<in> sr \<and> P sa \<longrightarrow> P' s proof (prove)
goal:
No subgoals!
theory AutoCorres_C

lemma corres_guard_r:
  assumes "corres_underlying sr nf nf' r P P' a (c ())"
  shows "corres_underlying sr nf nf' r P (\<lambda>s. (nf' \<longrightarrow> f s) \<and> (f s \<longrightarrow> P' s))
                           a (guard f >>= c)" apply (rule corres_guard_imp[OF corres_symb_exec_r'[where R'="\<lambda>s. nf' \<longrightarrow> f s"]]) using assms apply simp apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P (\<lambda>s. (nf' \<longrightarrow> f s) \<and> (f s \<longrightarrow> P' s)) a (guard f >>= c) proof (prove)
goal (6 subgoals):
 1. \<And>rv. corres_underlying sr nf nf' r ?Q (?P''1 rv) a (c rv)
 2. \<lbrace>?P'1\<rbrace> guard f \<lbrace>?P''1\<rbrace>
 3. \<And>s. ?Q'1 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> guard f \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. nf' \<Longrightarrow> no_fail (\<lambda>s. nf' \<longrightarrow> f s) (guard f)
 5. \<And>s. P s \<Longrightarrow> ?Q s
 6. \<And>s. (nf' \<longrightarrow> f s) \<and> (f s \<longrightarrow> P' s) \<Longrightarrow> (?P'1 and ?Q'1 and (\<lambda>s. nf' \<longrightarrow> f s)) s proof (prove)
using this:
corres_underlying sr nf nf' r P P' a (c ())

goal (6 subgoals):
 1. \<And>rv. corres_underlying sr nf nf' r ?Q (?P''1 rv) a (c rv)
 2. \<lbrace>?P'1\<rbrace> guard f \<lbrace>?P''1\<rbrace>
 3. \<And>s. ?Q'1 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> guard f \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. nf' \<Longrightarrow> no_fail (\<lambda>s. nf' \<longrightarrow> f s) (guard f)
 5. \<And>s. P s \<Longrightarrow> ?Q s
 6. \<And>s. (nf' \<longrightarrow> f s) \<and> (f s \<longrightarrow> P' s) \<Longrightarrow> (?P'1 and ?Q'1 and (\<lambda>s. nf' \<longrightarrow> f s)) s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?P'1\<rbrace> guard f \<lbrace>\<lambda>a. P'\<rbrace>
 2. \<And>s. ?Q'1 s \<Longrightarrow> \<lbrace>(=) s\<rbrace> guard f \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. nf' \<Longrightarrow> no_fail (\<lambda>s. nf' \<longrightarrow> f s) (guard f)
 4. \<And>s. P s \<Longrightarrow> P s
 5. \<And>s. (nf' \<longrightarrow> f s) \<and> (f s \<longrightarrow> P' s) \<Longrightarrow> (?P'1 and ?Q'1 and (\<lambda>s. nf' \<longrightarrow> f s)) s proof (prove)
goal:
No subgoals!
theory AutoCorres_C

lemma corres_cross_over_guard:
  assumes "corres_underlying sr nf nf' r P P' a c"
  shows "corres_underlying sr nf nf' r (P and Q) (\<lambda>s'. \<forall>s. (s,s') \<in> sr \<and> Q s \<longrightarrow> P' s') a c" by (rule stronger_corres_guard_imp[OF assms]) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (P and Q) (\<lambda>s'. \<forall>s. (s, s') \<in> sr \<and> Q s \<longrightarrow> P' s') a c
theory XPres

lemma xpres_eq_If_False:
  "xpres_eq_If False x y y" by (simp add: xpres_eq_If_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_eq_If False x y y
theory XPres

lemma xpres_eq_If_True:
  "xpres_eq_If True x y x" by (simp add: xpres_eq_If_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_eq_If True x y x
theory XPres

lemma xpres_abnormalD:
  assumes "xpres_abnormal \<Gamma> c abnormal"
  assumes "abnormal"
  assumes "\<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Normal t"
  shows False using assms by (auto simp: xpres_abnormal_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. False proof (prove)
using this:
xpres_abnormal \<Gamma> c abnormal
abnormal
\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal t

goal (1 subgoal):
 1. False
theory XPres

lemma xpres_abnormalI:
  assumes "\<And>s t. \<lbrakk>abnormal; \<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Normal t\<rbrakk> \<Longrightarrow> False"
  shows "xpres_abnormal \<Gamma> c abnormal" using assms by (auto simp: xpres_abnormal_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_abnormal \<Gamma> c abnormal proof (prove)
using this:
\<lbrakk>abnormal; \<Gamma>\<turnstile> \<langle>c,Normal ?s\<rangle> \<Rightarrow> Normal ?t\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. xpres_abnormal \<Gamma> c abnormal
theory XPres

lemma xpres_abnormal_trivial:
  "xpres_abnormal \<Gamma> c False" by (auto simp: xpres_abnormal_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_abnormal \<Gamma> c False
theory XPres

lemma xpres_abnormal_throw:
  "xpres_abnormal \<Gamma> Throw True" by (auto simp: xpres_abnormal_def elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_abnormal \<Gamma> THROW True
theory XPres

lemma xpres_abnormal_creturn:
  "xpres_abnormal \<Gamma> (creturn rtu xfu v) True" by (auto simp: xpres_abnormal_def creturn_def elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_abnormal \<Gamma> (creturn rtu xfu v) True
theory XPres

lemma xpres_abnormal_creturn_void:
  "xpres_abnormal \<Gamma> (creturn_void rtu) True" by (auto simp: xpres_abnormal_def creturn_void_def elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_abnormal \<Gamma> (creturn_void rtu) True
theory XPres

lemma xpres_abnormal_cbreak:
  "xpres_abnormal \<Gamma> (cbreak rtu) True" by (auto simp: xpres_abnormal_def cbreak_def elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_abnormal \<Gamma> (cbreak rtu) True
theory XPres

lemma xpres_abnormal_guard:
  assumes "xpres_abnormal \<Gamma> c abnormal"
  shows "xpres_abnormal \<Gamma> (Guard f g c) abnormal" apply (rule xpres_abnormalI) apply (erule exec_elim_cases; clarsimp; erule (1) assms[THEN xpres_abnormalD]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_abnormal \<Gamma> (Guard f g c) abnormal proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>abnormal; \<Gamma>\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Normal t\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory XPres

lemma xpres_abnormal_seq:
  assumes C: "xpres_abnormal \<Gamma> c C"
             "xpres_abnormal \<Gamma> d D"
  assumes S: "xpres_eq_If C True D S"
  shows "xpres_abnormal \<Gamma> (Seq c d) S" apply (rule xpres_abnormalI) apply (erule exec_elim_cases; clarsimp) apply (frule Normal_result, clarsimp, rename_tac s s') apply (clarsimp simp: S[unfolded xpres_eq_If_def] if_bool_simps) apply (erule disjE; erule (1) C[THEN xpres_abnormalD]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_abnormal \<Gamma> (c;;
d) S proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>S; \<Gamma>\<turnstile> \<langle>c;;
d,Normal s\<rangle> \<Rightarrow> Normal t\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>t sa s'. \<lbrakk>S; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>d,s'\<rangle> \<Rightarrow> Normal t\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>t s s'. \<lbrakk>S; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal s'; \<Gamma>\<turnstile> \<langle>d,Normal s'\<rangle> \<Rightarrow> Normal t\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>t s s'. \<lbrakk>C \<or> D; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal s'; \<Gamma>\<turnstile> \<langle>d,Normal s'\<rangle> \<Rightarrow> Normal t\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory XPres

lemma xpres_abnormal_cond:
  assumes C: "xpres_abnormal \<Gamma> c C"
             "xpres_abnormal \<Gamma> d D"
  assumes S: "xpres_eq_If C D False S" (* S = (C \<and> D) *)
  shows "xpres_abnormal \<Gamma> (Cond b c d) S" apply (rule xpres_abnormalI) apply (clarsimp simp: S[unfolded xpres_eq_If_def] if_bool_simps) apply (erule exec_elim_cases; clarsimp; erule (1) C[THEN xpres_abnormalD]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_abnormal \<Gamma> (Cond b c d) S proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>S; \<Gamma>\<turnstile> \<langle>Cond b c d,Normal s\<rangle> \<Rightarrow> Normal t\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>\<Gamma>\<turnstile> \<langle>Cond b c d,Normal s\<rangle> \<Rightarrow> Normal t; C; D\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory XPres

lemma xpres_def:
  "xpres \<Gamma> xf v c \<equiv> \<forall>s t. \<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> t
                          \<longrightarrow> xf s = v \<longrightarrow> (\<forall>t'. t = Normal t' \<or> t = Abrupt t' \<longrightarrow> xf t' = v)" by (auto simp: xpres_strong_def atomize_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres \<Gamma> xf v c \<equiv> \<forall>s t. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> xf s = v \<longrightarrow> (\<forall>t'. t = Normal t' \<or> t = Abrupt t' \<longrightarrow> xf t' = v)
theory XPres

lemma xpres_strong_abnormalD:
  "xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal \<Longrightarrow> abnormal \<Longrightarrow> pres_norm" by (simp add: xpres_strong_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal; abnormal\<rbrakk> \<Longrightarrow> pres_norm
theory XPres

lemma xpresI:
  "\<lbrakk>\<And>s t t'. \<lbrakk>\<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> t; xf s = v; t = Normal t' \<or> t = Abrupt t' \<rbrakk> \<Longrightarrow> xf t' = v\<rbrakk> \<Longrightarrow>
  xpres \<Gamma> xf v c" unfolding xpres_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s t t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; xf s = v; t = Normal t' \<or> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v) \<Longrightarrow> xpres \<Gamma> xf v c proof (prove)
goal (1 subgoal):
 1. (\<And>s t t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; xf s = v; t = Normal t' \<or> t = Abrupt t'\<rbrakk> \<Longrightarrow> xf t' = v) \<Longrightarrow> \<forall>s t. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> xf s = v \<longrightarrow> (\<forall>t'. t = Normal t' \<or> t = Abrupt t' \<longrightarrow> xf t' = v)
theory XPres

lemma xpres_strong_abnormal_iff:
  "xpres_strong \<Gamma> xf v c abnormal False abnormal \<longleftrightarrow> xpres_abnormal \<Gamma> c abnormal" by (auto simp: xpres_strong_def xpres_abnormal_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v c abnormal False abnormal = xpres_abnormal \<Gamma> c abnormal
theory XPres

lemma xpres_skip:
  "xpres \<Gamma> xf v Skip" by (rule xpresI; erule exec_Normal_elim_cases; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres \<Gamma> xf v SKIP