kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_C

lemma Cond_if_mem:
   "(Cond (if P then UNIV else {})) = (Cond {s. P})" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Cond (if P then UNIV else {}) = _Cond P
theory Ipc_C

lemma asUser_atcbContext_obj_at:
  "t \<noteq> t' \<Longrightarrow>
    \<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
      asUser t' m
    \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>" apply (simp add: asUser_def split_def atcbContextGet_def atcbContextSet_def) apply (wp threadGet_wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> asUser t' m \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>obj_at' (\<lambda>tcb. P (atcbContext (tcbArch tcb))) t\<rbrace> do uc <- threadGet (atcbContext \<circ> tcbArch) t';
p <- select_f (m uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. snd p) (tcbArch tcb)) tcb) t';
return (fst p)
od \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (atcbContext (tcbArch tcb))) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>t \<noteq> t'; obj_at' (\<lambda>tcb. P (atcbContext (tcbArch tcb))) t s\<rbrakk> \<Longrightarrow> \<forall>tcb. ko_at' tcb t' s \<longrightarrow> (\<forall>x\<in>fst (m ((atcbContext \<circ> tcbArch) tcb)). obj_at' (\<lambda>obj. if t' = t then P (atcbContext (tcbArch (tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. snd x) (tcbArch obj)) obj))) else P (atcbContext (tcbArch obj))) t s) proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma setMR_atcbContext_obj_at:
  "t \<noteq> t' \<Longrightarrow>
    \<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
      setMR t' b r v
    \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>" apply (simp add: setMR_def) apply (rule hoare_pre) apply (wp asUser_atcbContext_obj_at[simplified] | simp | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> setMR t' b r v \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) t\<rbrace> if r < length TCB_H.msgRegisters then do asUser t' (setRegister (TCB_H.msgRegisters ! r) v);
return (r + 1)
od else case b of None \<Rightarrow> return (length TCB_H.msgRegisters) | Some buf \<Rightarrow> do storeWordUser (buf + word_of_nat (r + 1) * word_size) v;
return (r + 1)
od \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) t\<rbrace> proof (prove)
goal (2 subgoals):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>?Q\<rbrace> if r < length TCB_H.msgRegisters then do asUser t' (setRegister (TCB_H.msgRegisters ! r) v);
return (r + 1)
od else case b of None \<Rightarrow> return (length TCB_H.msgRegisters) | Some buf \<Rightarrow> do storeWordUser (buf + word_of_nat (r + 1) * word_size) v;
return (r + 1)
od \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) t\<rbrace>
 2. \<And>s. \<lbrakk>t \<noteq> t'; obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) t s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma setMR_tcbFault_obj_at:
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> setMR t' b r v
   \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>" apply (simp add: setMR_def) apply (rule hoare_pre) apply (wp asUser_tcbFault_obj_at | wpc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> setMR t' b r v \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> if r < length TCB_H.msgRegisters then do asUser t' (setRegister (TCB_H.msgRegisters ! r) v);
return (r + 1)
od else case b of None \<Rightarrow> return (length TCB_H.msgRegisters) | Some buf \<Rightarrow> do storeWordUser (buf + word_of_nat (r + 1) * word_size) v;
return (r + 1)
od \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> if r < length TCB_H.msgRegisters then do asUser t' (setRegister (TCB_H.msgRegisters ! r) v);
return (r + 1)
od else case b of None \<Rightarrow> return (length TCB_H.msgRegisters) | Some buf \<Rightarrow> do storeWordUser (buf + word_of_nat (r + 1) * word_size) v;
return (r + 1)
od \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>
 2. \<And>s. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t s \<Longrightarrow> (r < length TCB_H.msgRegisters \<longrightarrow> obj_at' (\<lambda>tcb. P (tcbFault tcb)) t s) \<and> (\<not> r < length TCB_H.msgRegisters \<longrightarrow> (b = None \<longrightarrow> obj_at' (\<lambda>tcb. P (tcbFault tcb)) t s) \<and> (\<forall>x. b = Some x \<longrightarrow> obj_at' (\<lambda>a. P (tcbFault a)) t s)) proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma ccorres_abstract_known:
  "\<lbrakk> \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val) \<rbrakk>
     \<Longrightarrow> ccorres rvr xf P (P' \<inter> {s. xf' s = val}) hs f g" apply (rule ccorres_guard_imp2) apply (rule_tac xf'=xf' in ccorres_abstract) apply assumption apply (rule_tac P="rv' = val" in ccorres_gen_asm2) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val)\<rbrakk> \<Longrightarrow> ccorres rvr xf P (P' \<inter> {s. xf' s = val}) hs f g proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val)\<rbrakk> \<Longrightarrow> ccorres rvr xf ?Q ?Q' hs f g
 2. \<And>s s'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val); (s, s') \<in> rf_sr; P s; s' \<in> P' \<inter> {s. xf' s = val}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (3 subgoals):
 1. \<And>rv' t t'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' g (?d'3 rv')
 2. \<And>rv'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val)\<rbrakk> \<Longrightarrow> ccorres rvr xf ?Q (?G'3 rv') hs f (?d'3 rv')
 3. \<And>s s'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val); (s, s') \<in> rf_sr; P s; s' \<in> P' \<inter> {s. xf' s = val}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s. s \<in> ?G'3 (xf' s)} proof (prove)
goal (2 subgoals):
 1. \<And>rv'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val)\<rbrakk> \<Longrightarrow> ccorres rvr xf ?Q (?G'3 rv') hs f (g' rv')
 2. \<And>s s'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val); (s, s') \<in> rf_sr; P s; s' \<in> P' \<inter> {s. xf' s = val}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s. s \<in> ?G'3 (xf' s)} proof (prove)
goal (2 subgoals):
 1. \<And>rv'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val); rv' = val\<rbrakk> \<Longrightarrow> ccorres rvr xf ?Q (?G'7 rv') hs f (g' rv')
 2. \<And>s s'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val); (s, s') \<in> rf_sr; P s; s' \<in> P' \<inter> {s. xf' s = val}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s. s \<in> ?G'7 (xf' s) \<inter> \<lbrace>xf' s = val\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val); (s, s') \<in> rf_sr; P s; s' \<in> P' \<inter> {s. xf' s = val}\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> {s. s \<in> P' \<inter> \<lbrace>xf' s = val\<rbrace>} proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma exceptionMessage_ccorres:
  "n < unat n_exceptionMessage
      \<Longrightarrow> register_from_H (ARM_H.exceptionMessage ! n)
             = index exceptionMessageC n" apply (simp add: exceptionMessageC_def ARM_H.exceptionMessage_def
                   ARM.exceptionMessage_def MessageID_Exception_def) by (simp add: Arrays.update_def n_exceptionMessage_def nth_Cons'
                fupdate_def
         split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < unat n_exceptionMessage \<Longrightarrow> register_from_H (FaultHandler_H.exceptionMessage ! n) = kernel_all_global_addresses.fault_messages.[unat MessageID_Exception].[n] proof (prove)
goal (1 subgoal):
 1. n < unat n_exceptionMessage \<Longrightarrow> register_from_H ([register.FaultIP, register.SP, register.CPSR] ! n) = fupdate (Suc 0) (fupdate 2 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.CPSR)) (fupdate (Suc 0) (fupdate (Suc 0) (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.SP)) (fupdate (Suc 0) (fupdate 0 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP)) (fupdate 0 (fupdate 11 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.CPSR)) (fupdate 0 (fupdate 10 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.LR)) (fupdate 0 (fupdate 9 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.SP)) (fupdate 0 (fupdate 8 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP)) (fupdate 0 (fupdate 7 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R7)) (fupdate 0 (fupdate 6 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R6)) (fupdate 0 (fupdate 5 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R5)) (fupdate 0 (fupdate 4 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R4)) (fupdate 0 (fupdate 3 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R3)) (fupdate 0 (fupdate 2 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R2)) (fupdate 0 (fupdate (Suc 0) (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R1)) (fupdate 0 (fupdate 0 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.R0)) (ARRAY _ _. 0))))))))))))))).[Suc 0].[n]
theory Ipc_C

lemma asUser_obj_at_elsewhere:
  "\<lbrace>obj_at' (P :: tcb \<Rightarrow> bool) t' and (\<lambda>_. t \<noteq> t')\<rbrace> asUser t m \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace>" apply (rule hoare_gen_asm') apply (simp add: asUser_def split_def) apply (wp threadGet_wp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t' and (\<lambda>_. t \<noteq> t')\<rbrace> asUser t m \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>obj_at' P t'\<rbrace> asUser t m \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>obj_at' P t'\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (m uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>t \<noteq> t'; obj_at' P t' s\<rbrakk> \<Longrightarrow> \<forall>tcb. ko_at' tcb t s \<longrightarrow> (\<forall>x\<in>fst (m ((atcbContextGet \<circ> tcbArch) tcb)). obj_at' (\<lambda>obj. if t = t' then P (tcbArch_update (\<lambda>_. atcbContextSet (snd x) (tcbArch obj)) obj) else P obj) t' s) proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma exceptionMessage_length_aux :
  "\<And>n. n < length ARM_H.exceptionMessage \<Longrightarrow> n < unat n_exceptionMessage" by (simp add: ARM.exceptionMessage_def ARM_H.exceptionMessage_def n_exceptionMessage_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < length FaultHandler_H.exceptionMessage \<Longrightarrow> n < unat n_exceptionMessage
theory Ipc_C

lemma mapM_cong: "\<lbrakk> \<forall>x. elem x xs \<longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> mapM_x f xs =  mapM_x g xs" by (induction xs, (simp add: mapM_x_Nil mapM_x_Cons)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x. elem x xs \<longrightarrow> f x = g x \<Longrightarrow> mapM_x f xs = mapM_x g xs
theory Ipc_C

lemma makeFaultMessage2:
  "makeFaultMessage ft thread
    = (do x \<leftarrow> makeFaultMessage ft thread;
       return (case ft of CapFault _ _ _ \<Rightarrow> 1
                   | UnknownSyscallException _ \<Rightarrow> 2
                   | UserException _ _ \<Rightarrow> 3
                   | ArchFault aft \<Rightarrow> makeArchFaultMessage2 aft, snd x) od)" by (simp add: makeFaultMessage_def makeArchFaultMessage2_def makeArchFaultMessage_def
           split: fault.split arch_fault.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makeFaultMessage ft thread = do x <- makeFaultMessage ft thread;
return (case ft of Fault_H.fault.UserException x xa \<Rightarrow> 3 | Fault_H.fault.CapFault x xa xb \<Rightarrow> 1 | Fault_H.fault.UnknownSyscallException x \<Rightarrow> 2 | Fault_H.fault.ArchFault aft \<Rightarrow> makeArchFaultMessage2 aft, snd x)
od
theory Ipc_C

lemma array_assertion_shrink_left_add:
  "array_assertion (Ptr ptr :: ('a :: wf_type) ptr) j htd
    \<Longrightarrow> n = of_nat (k * size_of TYPE('a)) \<and> k + i \<le> j \<and> 0 < i
    \<Longrightarrow> array_assertion (Ptr (ptr + n) :: 'a ptr) i htd" apply (cases "k = 0") apply (simp add: unat_eq_0) apply (erule array_assertion_shrink_right, simp) apply (drule_tac j=k in array_assertion_shrink_leftD) apply simp apply simp apply (erule array_assertion_shrink_right) apply arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>array_assertion (PTR('a) ptr) j htd; n = word_of_nat (k * size_of TYPE('a)) \<and> k + i \<le> j \<and> 0 < i\<rbrakk> \<Longrightarrow> array_assertion (PTR('a) (ptr + n)) i htd proof (prove)
goal (2 subgoals):
 1. \<lbrakk>array_assertion (PTR('a) ptr) j htd; n = word_of_nat (k * size_of TYPE('a)) \<and> k + i \<le> j \<and> 0 < i; k = 0\<rbrakk> \<Longrightarrow> array_assertion (PTR('a) (ptr + n)) i htd
 2. \<lbrakk>array_assertion (PTR('a) ptr) j htd; n = word_of_nat (k * size_of TYPE('a)) \<and> k + i \<le> j \<and> 0 < i; k \<noteq> 0\<rbrakk> \<Longrightarrow> array_assertion (PTR('a) (ptr + n)) i htd proof (prove)
goal (2 subgoals):
 1. \<lbrakk>array_assertion (PTR('a) ptr) j htd; n = 0 \<and> i \<le> j \<and> 0 < i; k = 0\<rbrakk> \<Longrightarrow> array_assertion (PTR('a) ptr) i htd
 2. \<lbrakk>array_assertion (PTR('a) ptr) j htd; n = word_of_nat (k * size_of TYPE('a)) \<and> k + i \<le> j \<and> 0 < i; k \<noteq> 0\<rbrakk> \<Longrightarrow> array_assertion (PTR('a) (ptr + n)) i htd proof (prove)
goal (1 subgoal):
 1. \<lbrakk>array_assertion (PTR('a) ptr) j htd; n = word_of_nat (k * size_of TYPE('a)) \<and> k + i \<le> j \<and> 0 < i; k \<noteq> 0\<rbrakk> \<Longrightarrow> array_assertion (PTR('a) (ptr + n)) i htd proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = word_of_nat (k * size_of TYPE('a)) \<and> k + i \<le> j \<and> 0 < i; k \<noteq> 0\<rbrakk> \<Longrightarrow> k < j
 2. \<lbrakk>n = word_of_nat (k * size_of TYPE('a)) \<and> k + i \<le> j \<and> 0 < i; k \<noteq> 0; array_assertion (PTR('a) ptr +\<^sub>p int k) (j - k) htd\<rbrakk> \<Longrightarrow> array_assertion (PTR('a) (ptr + n)) i htd proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = word_of_nat (k * size_of TYPE('a)) \<and> k + i \<le> j \<and> 0 < i; k \<noteq> 0; array_assertion (PTR('a) ptr +\<^sub>p int k) (j - k) htd\<rbrakk> \<Longrightarrow> array_assertion (PTR('a) (ptr + n)) i htd proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = word_of_nat k * word_of_nat (size_of TYPE('a)) \<and> k + i \<le> j \<and> 0 < i; 0 < k; array_assertion (PTR('a) (ptr + word_of_nat k * word_of_nat (size_of TYPE('a)))) (j - k) htd\<rbrakk> \<Longrightarrow> array_assertion (PTR('a) (ptr + word_of_nat k * word_of_nat (size_of TYPE('a)))) i htd proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = word_of_nat k * word_of_nat (size_of TYPE('a)) \<and> k + i \<le> j \<and> 0 < i; 0 < k\<rbrakk> \<Longrightarrow> i \<le> j - k proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma array_assertion_shrink_left_add_div:
  "array_assertion (Ptr ptr :: ('a :: wf_type) ptr) j htd
    \<Longrightarrow> n = of_nat (unat n div size_of TYPE('a)) * of_nat (size_of TYPE('a))
        \<and> i + (unat n div size_of TYPE('a)) \<le> j \<and> 0 < i
    \<Longrightarrow> array_assertion (Ptr (ptr + n) :: 'a ptr) i htd" apply (erule_tac k="unat n div size_of TYPE('a)"
    in array_assertion_shrink_left_add) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>array_assertion (PTR('a) ptr) j htd; n = word_of_nat (unat n div size_of TYPE('a)) * word_of_nat (size_of TYPE('a)) \<and> i + unat n div size_of TYPE('a) \<le> j \<and> 0 < i\<rbrakk> \<Longrightarrow> array_assertion (PTR('a) (ptr + n)) i htd proof (prove)
goal (1 subgoal):
 1. n = word_of_nat (unat n div size_of TYPE('a)) * word_of_nat (size_of TYPE('a)) \<and> i + unat n div size_of TYPE('a) \<le> j \<and> 0 < i \<Longrightarrow> n = word_of_nat (unat n div size_of TYPE('a) * size_of TYPE('a)) \<and> unat n div size_of TYPE('a) + i \<le> j \<and> 0 < i proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma ccorres_split_when_throwError_cond_break:
  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' (catchbrk_C # hs) (throwError e) c"
  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf
                        U U' (catchbrk_C # 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')})
          (catchbrk_C # 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_break [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')}) (catchbrk_C # 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')}) (catchbrk_C # 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 Ipc_C

lemma maskAsFull_isEndpoint[simp]:
  "isEndpointCap a \<Longrightarrow> maskedAsFull a b = a" by (clarsimp simp:isCap_simps maskedAsFull_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isEndpointCap a \<Longrightarrow> maskedAsFull a b = a
theory Ipc_C

lemma is_derived_capMasterCap:
  "is_derived' m slot cap cap'
         \<Longrightarrow> capMasterCap cap = capMasterCap cap'" by (clarsimp simp:is_derived'_def badge_derived'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived' m slot cap cap' \<Longrightarrow> capMasterCap cap = capMasterCap cap'
theory Ipc_C

lemma maskedAsFull_again:
  "maskedAsFull (maskedAsFull aa aa) r = maskedAsFull aa aa" apply (case_tac aa) apply (simp_all add:maskedAsFull_def isCap_simps split: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. maskedAsFull (maskedAsFull aa aa) r = maskedAsFull aa aa proof (prove)
goal (12 subgoals):
 1. \<And>x1. aa = capability.ThreadCap x1 \<Longrightarrow> maskedAsFull (maskedAsFull aa aa) r = maskedAsFull aa aa
 2. aa = capability.NullCap \<Longrightarrow> maskedAsFull (maskedAsFull aa aa) r = maskedAsFull aa aa
 3. \<And>x31 x32 x33 x34. aa = capability.NotificationCap x31 x32 x33 x34 \<Longrightarrow> maskedAsFull (maskedAsFull aa aa) r = maskedAsFull aa aa
 4. \<And>x4. aa = capability.IRQHandlerCap x4 \<Longrightarrow> maskedAsFull (maskedAsFull aa aa) r = maskedAsFull aa aa
 5. \<And>x51 x52 x53 x54 x55 x56. aa = capability.EndpointCap x51 x52 x53 x54 x55 x56 \<Longrightarrow> maskedAsFull (maskedAsFull aa aa) r = maskedAsFull aa aa
 6. aa = capability.DomainCap \<Longrightarrow> maskedAsFull (maskedAsFull aa aa) r = maskedAsFull aa aa
 7. \<And>x71 x72 x73. aa = capability.Zombie x71 x72 x73 \<Longrightarrow> maskedAsFull (maskedAsFull aa aa) r = maskedAsFull aa aa
 8. \<And>x8. aa = capability.ArchObjectCap x8 \<Longrightarrow> maskedAsFull (maskedAsFull aa aa) r = maskedAsFull aa aa
 9. \<And>x91 x92 x93. aa = capability.ReplyCap x91 x92 x93 \<Longrightarrow> maskedAsFull (maskedAsFull aa aa) r = maskedAsFull aa aa
 10. \<And>x101 x102 x103 x104. aa = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> maskedAsFull (maskedAsFull aa aa) r = maskedAsFull aa aa
A total of 12 subgoals... proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma ccap_relation_lift:
  "ccap_relation cap cap'
   \<Longrightarrow> (cap_to_H (the (cap_lift cap'))) = cap" apply (case_tac "cap_lift cap'") apply (auto simp:ccap_relation_def split:option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccap_relation cap cap' \<Longrightarrow> cap_to_H (the (cap_lift cap')) = cap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccap_relation cap cap'; cap_lift cap' = None\<rbrakk> \<Longrightarrow> cap_to_H (the (cap_lift cap')) = cap
 2. \<And>a. \<lbrakk>ccap_relation cap cap'; cap_lift cap' = Some a\<rbrakk> \<Longrightarrow> cap_to_H (the (cap_lift cap')) = cap proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma ccap_relation_inject:
  "\<lbrakk>ccap_relation acap cap; ccap_relation bcap cap\<rbrakk> \<Longrightarrow> acap = bcap" apply (case_tac "cap_lift cap") apply (auto simp:ccap_relation_def split:option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation acap cap; ccap_relation bcap cap\<rbrakk> \<Longrightarrow> acap = bcap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccap_relation acap cap; ccap_relation bcap cap; cap_lift cap = None\<rbrakk> \<Longrightarrow> acap = bcap
 2. \<And>a. \<lbrakk>ccap_relation acap cap; ccap_relation bcap cap; cap_lift cap = Some a\<rbrakk> \<Longrightarrow> acap = bcap proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma cte_wp_at_imp_consequent':
  "cte_wp_at' Q p s \<longrightarrow> cte_wp_at' (\<lambda>cte. P cte \<longrightarrow> Q cte) p s" by (clarsimp simp: cte_wp_at_ctes_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' Q p s \<longrightarrow> cte_wp_at' (\<lambda>cte. P cte \<longrightarrow> Q cte) p s