theory SyscallArgs_C

lemma syscall_error_throwError_ccorres_succs:
  "\<lbrakk> is_syscall_error_code f code;
     \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err \<rbrakk>
   \<Longrightarrow>
   ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id v' ret__unsigned_long_')
      \<top> (UNIV) (SKIP # hs)
      (throwError (Inl err)) (code ;; remainder)" apply (rule ccorres_guard_imp2,
         rule ccorres_split_throws) apply (erule syscall_error_throwError_ccorres_direct) apply simp apply (rule HoarePartialProps.augment_Faults) apply (erule iffD1[OF is_syscall_error_code_def, THEN spec]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id v' ret__unsigned_long_') (\<lambda>_. True) UNIV (SKIP # hs) (throwError (Inl err)) (code;;
remainder) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id v' ret__unsigned_long_') ?Q ?P'3 (SKIP # hs) (throwError (Inl err)) code
 2. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'3 code {},UNIV
 3. \<And>s s'. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?P'3 \<inter> ?R'3 proof (prove)
goal (3 subgoals):
 1. \<And>err' ft'. (\<And>err' ft'. syscall_error_to_H (f err') ft' = Some err) \<Longrightarrow> syscall_error_to_H (f err') ft' = Some err
 2. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'3 code {},UNIV
 3. \<And>s s'. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> True \<and> s' \<in> UNIV \<inter> ?R'3 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'3 code {},UNIV
 2. \<And>s s'. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> True \<and> s' \<in> UNIV \<inter> ?R'3 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F8\<^esub> ?R'3 code {},UNIV
 2. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err\<rbrakk> \<Longrightarrow> ?F8 \<subseteq> UNIV
 3. \<And>s s'. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> True \<and> s' \<in> UNIV \<inter> ?R'3 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err\<rbrakk> \<Longrightarrow> {} \<subseteq> UNIV
 2. \<And>s s'. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> True \<and> s' \<in> UNIV \<inter> {s. globals_update (current_syscall_error_'_update f) s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr> \<in> UNIV} proof (prove)
goal:
No subgoals!