kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_C

lemma cap_get_tag_isArchCap_unfolded_H_cap:
  "ccap_relation (capability.ArchObjectCap a_cap) cap' \<Longrightarrow>
   (isArchCap_tag (cap_get_tag cap'))" apply (frule cap_get_tag_isCap(11), simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccap_relation (capability.ArchObjectCap a_cap) cap' \<Longrightarrow> isArchCap_tag (cap_get_tag cap') proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma framesize_to_H_eq:
  "\<lbrakk> a \<le> 3; b \<le> 3; a \<noteq> 0; b \<noteq> 0 \<rbrakk> \<Longrightarrow>
   (framesize_to_H a = framesize_to_H b) = (a = b)" by (fastforce simp: framesize_to_H_def Kernel_C.ARMSmallPage_def
                     Kernel_C.ARMLargePage_def Kernel_C.ARMSection_def
                     word_le_make_less
              split: if_split
               dest: word_less_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> 3; b \<le> 3; a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> (framesize_to_H a = framesize_to_H b) = (a = b)
theory CSpace_C

lemma capFSize_range:
  "\<And>cap. cap_get_tag cap = scast cap_frame_cap \<Longrightarrow>
   capFSize_CL (cap_frame_cap_lift cap) \<le> 3" apply (simp add: cap_frame_cap_lift_def) apply (simp add: cap_lift_def cap_tag_defs word_and_le1 mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<Longrightarrow> capFSize_CL (cap_frame_cap_lift cap) \<le> 3 proof (prove)
goal (1 subgoal):
 1. \<And>cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<Longrightarrow> capFSize_CL (case cap_lift cap of Some (Cap_frame_cap rec) \<Rightarrow> rec) \<le> 3 proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma isArchCap_T_isArchObjectCap:
  "isArchCap \<top> = isArchObjectCap" by (rule ext, auto simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isArchCap (\<lambda>_. True) = isArchObjectCap
theory CSpace_C

lemma deriveCap_ccorres:
  "ccorres (syscall_error_rel \<currency> ccap_relation) deriveCap_xf
  (invs') (UNIV \<inter> {s. ccap_relation cap (cap_' s)} \<inter> {s. slot_' s = Ptr slot}) []
  (deriveCap slot cap) (Call deriveCap_'proc)" apply (rule ccorres_guard_imp2, rule deriveCap_ccorres') apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (syscall_error_rel \<currency> ccap_relation) (liftxf errstate deriveCap_ret_C.status_C deriveCap_ret_C.cap_C ret__struct_deriveCap_ret_C_') invs' (UNIV \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace>) [] (global.deriveCap slot cap) (Call deriveCap_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace>\<rbrakk> \<Longrightarrow> (valid_objs' and valid_mdb') s \<and> s' \<in> UNIV \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr slot\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_All

lemma ccorres_return_into_rel:
  "ccorres (r \<circ> f) xf G G' hs a c
  \<Longrightarrow> ccorres r xf G G' hs (a >>= (\<lambda>rv. return (f rv))) c" by (simp add: liftM_def[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (r \<circ> f) xf G G' hs a c \<Longrightarrow> ccorres r xf G G' hs (do rv <- a;
return (f rv)
od) c
theory CSpace_All

lemma lookupCap_ccorres:
  "ccorres (lookup_failure_rel \<currency> ccap_relation) lookupCap_xf
   (\<lambda>s. invs' s \<and> (tcb_at' a s))
   (UNIV \<inter> {s. cPtr_' s = b} \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr a}) []
  (lookupCap a b) (Call lookupCap_'proc)" apply (rule ccorres_guard_imp2, rule lookupCap_ccorres') apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (lookup_failure_rel \<currency> ccap_relation) (liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_') (\<lambda>s. invs' s \<and> tcb_at' a s) (UNIV \<inter> \<lbrace>\<acute>cPtr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>) [] (lookupCap a b) (Call lookupCap_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s \<and> tcb_at' a s; s' \<in> UNIV \<inter> \<lbrace>\<acute>cPtr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace>\<rbrakk> \<Longrightarrow> (valid_pspace' and tcb_at' a) s \<and> s' \<in> UNIV \<inter> \<lbrace>\<acute>cPtr = b\<rbrace> \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr a\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_All

lemma lookupErrorOnFailure_ccorres:
  "ccorres (f \<currency> r) xf P P' hs a c
    \<Longrightarrow> ccorres ((\<lambda>x y z. \<exists>w. x = FailedLookup isSource w \<and> f w y z) \<currency> r)
             xf P P' hs
             (lookupErrorOnFailure isSource a) c" apply (simp add: lookupError_injection injection_handler_liftM) apply (erule ccorres_rel_imp) apply (auto split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (f \<currency> r) xf P P' hs a c \<Longrightarrow> ccorres ((\<lambda>x y z. \<exists>w. x = Fault_H.syscall_error.FailedLookup isSource w \<and> f w y z) \<currency> r) xf P P' hs (lookupErrorOnFailure isSource a) c proof (prove)
goal (1 subgoal):
 1. ccorres (f \<currency> r) xf P P' hs a c \<Longrightarrow> ccorres ((\<lambda>x y z. \<exists>w. x = Fault_H.syscall_error.FailedLookup isSource w \<and> f w y z) \<currency> r \<circ> case_sum (\<lambda>ex. Inl (Fault_H.syscall_error.FailedLookup isSource ex)) Inr) xf P P' hs a c proof (prove)
goal (1 subgoal):
 1. \<And>x y. (f \<currency> r) x (xf y) \<Longrightarrow> ((\<lambda>x y z. \<exists>w. x = Fault_H.syscall_error.FailedLookup isSource w \<and> f w y z) \<currency> r \<circ> case_sum (\<lambda>ex. Inl (Fault_H.syscall_error.FailedLookup isSource ex)) Inr) x (xf y) proof (prove)
goal:
No subgoals!
theory CSpace_All

lemma lookup_failure_rel_fault_lift:
  " \<lbrakk> st \<noteq> scast EXCEPTION_NONE;
      lookup_failure_rel err st (errstate t)\<rbrakk>
     \<Longrightarrow> \<exists>v. lookup_fault_lift (current_lookup_fault_' (globals t)) = Some v \<and> lookup_fault_to_H v = err" apply (case_tac err, clarsimp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; lookup_failure_rel err st (errstate t)\<rbrakk> \<Longrightarrow> \<exists>v. lookup_fault_lift (current_lookup_fault_' (globals t)) = Some v \<and> lookup_fault_to_H v = err proof (prove)
goal:
No subgoals!
theory CSpace_All

lemma lookupSlotForCNodeOp_ccorres:
  "ccorres
   (syscall_error_rel \<currency>  (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf
   (\<lambda>s.  invs' s \<and> s  \<turnstile>' croot \<and> depth < 2 ^ word_bits)
   (UNIV \<inter> {s. capptr_' s = capptr} \<inter>
            {s. to_bool (isSource_' s) = isSource}  \<inter>
            {s. ccap_relation croot (root_' s)} \<inter>
            {s. depth_' s = of_nat depth} ) []
  (lookupSlotForCNodeOp isSource croot capptr depth)
  (Call lookupSlotForCNodeOp_'proc)" apply (rule ccorres_guard_imp2, rule lookupSlotForCNodeOp_ccorres') apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (syscall_error_rel \<currency> (\<lambda>w w'. w' = cte_Ptr w \<and> depth \<le> word_bits)) (liftxf errstate lookupSlot_ret_C.status_C lookupSlot_ret_C.slot_C ret__struct_lookupSlot_ret_C_') (\<lambda>s. invs' s \<and> valid_cap' croot s \<and> depth < 2 ^ word_bits) (UNIV \<inter> \<lbrace>\<acute>capptr = capptr\<rbrace> \<inter> \<lbrace>to_bool \<acute>isSource = isSource\<rbrace> \<inter> \<lbrace>ccap_relation croot \<acute>root\<rbrace> \<inter> \<lbrace>\<acute>depth = word_of_nat depth\<rbrace>) [] (lookupSlotForCNodeOp isSource croot capptr depth) (Call lookupSlotForCNodeOp_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s \<and> valid_cap' croot s \<and> depth < 2 ^ word_bits; s' \<in> UNIV \<inter> \<lbrace>\<acute>capptr = capptr\<rbrace> \<inter> \<lbrace>to_bool \<acute>isSource = isSource\<rbrace> \<inter> \<lbrace>ccap_relation croot \<acute>root\<rbrace> \<inter> \<lbrace>\<acute>depth = word_of_nat depth\<rbrace>\<rbrakk> \<Longrightarrow> (valid_pspace' s \<and> valid_cap' croot s \<and> depth < 2 ^ word_bits) \<and> s' \<in> UNIV \<inter> \<lbrace>\<acute>capptr = capptr\<rbrace> \<inter> \<lbrace>to_bool \<acute>isSource = isSource\<rbrace> \<inter> \<lbrace>ccap_relation croot \<acute>root\<rbrace> \<inter> \<lbrace>\<acute>depth = word_of_nat depth\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_All

lemma lookupSourceSlot_ccorres:
  "ccorres
   (syscall_error_rel \<currency> (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf
   (\<lambda>s.  invs' s \<and> s  \<turnstile>' croot \<and>  depth < 2 ^ word_bits)
   (UNIV \<inter> {s. capptr_' s = capptr} \<inter>
            {s. ccap_relation croot (root_' s)} \<inter>
            {s. depth_' s = of_nat depth} ) []
  (lookupSourceSlot croot capptr depth)
  (Call lookupSourceSlot_'proc)" apply (rule ccorres_guard_imp2, rule lookupSourceSlot_ccorres') apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (syscall_error_rel \<currency> (\<lambda>w w'. w' = cte_Ptr w \<and> depth \<le> word_bits)) (liftxf errstate lookupSlot_ret_C.status_C lookupSlot_ret_C.slot_C ret__struct_lookupSlot_ret_C_') (\<lambda>s. invs' s \<and> valid_cap' croot s \<and> depth < 2 ^ word_bits) (UNIV \<inter> \<lbrace>\<acute>capptr = capptr\<rbrace> \<inter> \<lbrace>ccap_relation croot \<acute>root\<rbrace> \<inter> \<lbrace>\<acute>depth = word_of_nat depth\<rbrace>) [] (lookupSourceSlot croot capptr depth) (Call lookupSourceSlot_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s \<and> valid_cap' croot s \<and> depth < 2 ^ word_bits; s' \<in> UNIV \<inter> \<lbrace>\<acute>capptr = capptr\<rbrace> \<inter> \<lbrace>ccap_relation croot \<acute>root\<rbrace> \<inter> \<lbrace>\<acute>depth = word_of_nat depth\<rbrace>\<rbrakk> \<Longrightarrow> (valid_pspace' s \<and> valid_cap' croot s \<and> depth < 2 ^ word_bits) \<and> s' \<in> UNIV \<inter> \<lbrace>\<acute>capptr = capptr\<rbrace> \<inter> \<lbrace>ccap_relation croot \<acute>root\<rbrace> \<inter> \<lbrace>\<acute>depth = word_of_nat depth\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_All

lemma lookupTargetSlot_ccorres:
  "ccorres
   (syscall_error_rel \<currency>  (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf
   (\<lambda>s.  invs' s \<and> s  \<turnstile>' croot \<and>  depth < 2 ^ word_bits)
  (UNIV \<inter> {s. capptr_' s = capptr} \<inter>
            {s. ccap_relation croot (root_' s)} \<inter>
            {s. depth_' s = of_nat depth} ) []
  (lookupTargetSlot croot capptr depth)
  (Call lookupTargetSlot_'proc)" apply (rule ccorres_guard_imp2, rule lookupTargetSlot_ccorres') apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (syscall_error_rel \<currency> (\<lambda>w w'. w' = cte_Ptr w \<and> depth \<le> word_bits)) (liftxf errstate lookupSlot_ret_C.status_C lookupSlot_ret_C.slot_C ret__struct_lookupSlot_ret_C_') (\<lambda>s. invs' s \<and> valid_cap' croot s \<and> depth < 2 ^ word_bits) (UNIV \<inter> \<lbrace>\<acute>capptr = capptr\<rbrace> \<inter> \<lbrace>ccap_relation croot \<acute>root\<rbrace> \<inter> \<lbrace>\<acute>depth = word_of_nat depth\<rbrace>) [] (lookupTargetSlot croot capptr depth) (Call lookupTargetSlot_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s \<and> valid_cap' croot s \<and> depth < 2 ^ word_bits; s' \<in> UNIV \<inter> \<lbrace>\<acute>capptr = capptr\<rbrace> \<inter> \<lbrace>ccap_relation croot \<acute>root\<rbrace> \<inter> \<lbrace>\<acute>depth = word_of_nat depth\<rbrace>\<rbrakk> \<Longrightarrow> (valid_pspace' s \<and> valid_cap' croot s \<and> depth < 2 ^ word_bits) \<and> s' \<in> UNIV \<inter> \<lbrace>\<acute>capptr = capptr\<rbrace> \<inter> \<lbrace>ccap_relation croot \<acute>root\<rbrace> \<inter> \<lbrace>\<acute>depth = word_of_nat depth\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbQueue_C

lemma tcb_queue_memberD:
  assumes queue_rel: "tcb_queue_relation getNext getPrev (cslift s') queue qprev qhead"
  and      in_queue: "tcbp \<in> set queue"
  and     valid_ntfn: "\<forall>t\<in>set queue. tcb_at' t s"
  and        rf_sr: "(s, s') \<in> rf_sr"
  shows "\<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb" using assms apply - apply (drule (1) bspec) apply (drule (1) tcb_at_h_t_valid) apply (clarsimp simp add: h_t_valid_clift_Some_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb proof (prove)
using this:
tcb_queue_relation getNext getPrev (cslift s') queue qprev qhead
tcbp \<in> set queue
\<forall>t\<in>set queue. tcb_at' t s
(s, s') \<in> rf_sr

goal (1 subgoal):
 1. \<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev (cslift s') queue qprev qhead; tcbp \<in> set queue; \<forall>t\<in>set queue. tcb_at' t s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev (cslift s') queue qprev qhead; tcbp \<in> set queue; (s, s') \<in> rf_sr; tcb_at' tcbp s\<rbrakk> \<Longrightarrow> \<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev (cslift s') queue qprev qhead; tcbp \<in> set queue; (s, s') \<in> rf_sr; s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr tcbp\<rbrakk> \<Longrightarrow> \<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb proof (prove)
goal:
No subgoals!
theory TcbQueue_C

lemma tcb_queue_relation_restrict:
  "tcb_queue_relation getNext getPrev mp queue qprev qhead =
  tcb_queue_relation getNext getPrev (restrict_map mp (tcb_ptr_to_ctcb_ptr ` set queue)) queue qprev qhead" apply (rule tcb_queue_relation_restrict0) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` set queue)\<^esub>) queue qprev qhead proof (prove)
goal (1 subgoal):
 1. set queue \<subseteq> set queue proof (prove)
goal:
No subgoals!
theory TcbQueue_C

lemma tcb_queue_relation_head_hd:
  assumes   tq: "tcb_queue_relation getNext getPrev mp queue qprev qhead"
  and     tcbs: "queue \<noteq> []"
  shows   "ctcb_ptr_to_tcb_ptr qhead = hd queue" using assms apply (cases queue) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctcb_ptr_to_tcb_ptr qhead = hd queue proof (prove)
using this:
tcb_queue_relation getNext getPrev mp queue qprev qhead
queue \<noteq> []

goal (1 subgoal):
 1. ctcb_ptr_to_tcb_ptr qhead = hd queue proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; queue \<noteq> []; queue = []\<rbrakk> \<Longrightarrow> ctcb_ptr_to_tcb_ptr qhead = hd queue
 2. \<And>a list. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; queue \<noteq> []; queue = a # list\<rbrakk> \<Longrightarrow> ctcb_ptr_to_tcb_ptr qhead = hd queue proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; queue \<noteq> []; queue = a # list\<rbrakk> \<Longrightarrow> ctcb_ptr_to_tcb_ptr qhead = hd queue proof (prove)
goal:
No subgoals!
theory TcbQueue_C

lemma tcb_queue_relation_next_not_NULL:
  assumes   tq: "tcb_queue_relation getNext getPrev mp queue qprev qhead"
  and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue"
  and     tcbs: "queue \<noteq> []"
  shows   "qhead \<noteq> NULL" proof - have "ctcb_ptr_to_tcb_ptr qhead \<in> set queue" using tq tcbs by (simp add: tcb_queue_relation_head_hd) with tq valid_ep(1) have "tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr qhead) \<noteq> NULL" by (rule tcb_queue_relation_not_NULL') thus ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. qhead \<noteq> NULL proof (state)
goal (1 subgoal):
 1. qhead \<noteq> NULL proof (prove)
goal (1 subgoal):
 1. ctcb_ptr_to_tcb_ptr qhead \<in> set queue proof (prove)
using this:
tcb_queue_relation getNext getPrev mp queue qprev qhead
queue \<noteq> []

goal (1 subgoal):
 1. ctcb_ptr_to_tcb_ptr qhead \<in> set queue proof (state)
this:
ctcb_ptr_to_tcb_ptr qhead \<in> set queue

goal (1 subgoal):
 1. qhead \<noteq> NULL proof (chain)
picking this:
tcb_queue_relation getNext getPrev mp queue qprev qhead
\<forall>t\<in>set queue. tcb_at' t s
ctcb_ptr_to_tcb_ptr qhead \<in> set queue proof (prove)
using this:
tcb_queue_relation getNext getPrev mp queue qprev qhead
\<forall>t\<in>set queue. tcb_at' t s
ctcb_ptr_to_tcb_ptr qhead \<in> set queue

goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr qhead) \<noteq> NULL proof (state)
this:
tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr qhead) \<noteq> NULL

goal (1 subgoal):
 1. qhead \<noteq> NULL proof (prove)
using this:
tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr qhead) \<noteq> NULL

goal (1 subgoal):
 1. qhead \<noteq> NULL proof (state)
this:
qhead \<noteq> NULL

goal:
No subgoals!
theory TcbQueue_C

lemma distinct_nth:
  assumes dist: "distinct xs"
  and     ln: "n < length xs"
  and     lm: "m < length xs"
  shows   "(xs ! n = xs ! m) = (n = m)" using dist ln lm apply (cases "n = m") apply simp apply (clarsimp simp: distinct_conv_nth) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (xs ! n = xs ! m) = (n = m) proof (prove)
using this:
distinct xs
n < length xs
m < length xs

goal (1 subgoal):
 1. (xs ! n = xs ! m) = (n = m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct xs; n < length xs; m < length xs; n = m\<rbrakk> \<Longrightarrow> (xs ! n = xs ! m) = (n = m)
 2. \<lbrakk>distinct xs; n < length xs; m < length xs; n \<noteq> m\<rbrakk> \<Longrightarrow> (xs ! n = xs ! m) = (n = m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; n < length xs; m < length xs; n \<noteq> m\<rbrakk> \<Longrightarrow> (xs ! n = xs ! m) = (n = m) proof (prove)
goal:
No subgoals!
theory TcbQueue_C

lemma null_not_in:
  "\<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue\<rbrakk>
   \<Longrightarrow> ctcb_ptr_to_tcb_ptr NULL \<notin> set queue" apply - apply (rule notI) apply (drule (2) tcb_queue_relation_not_NULL') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue\<rbrakk> \<Longrightarrow> ctcb_ptr_to_tcb_ptr NULL \<notin> set queue proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue\<rbrakk> \<Longrightarrow> ctcb_ptr_to_tcb_ptr NULL \<notin> set queue proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; ctcb_ptr_to_tcb_ptr NULL \<in> set queue\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t\<in>set queue. tcb_at' t s; distinct queue; ctcb_ptr_to_tcb_ptr NULL \<in> set queue; tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr NULL) \<noteq> NULL\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory TcbQueue_C

lemma tcb_queue_relationI':
  "\<lbrakk> tcb_queue_relation getNext getPrev hp queue NULL qhead;
     qend = (if queue = [] then NULL else (tcb_ptr_to_ctcb_ptr (last queue))) \<rbrakk>
  \<Longrightarrow> tcb_queue_relation' getNext getPrev hp queue qhead qend" unfolding tcb_queue_relation'_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev hp queue NULL qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue))\<rbrakk> \<Longrightarrow> tcb_queue_relation' getNext getPrev hp queue qhead qend proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev hp queue NULL qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue))\<rbrakk> \<Longrightarrow> qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue)) \<and> tcb_queue_relation getNext getPrev hp queue NULL qhead
theory TcbQueue_C

lemma tcb_queue_relationE':
  "\<lbrakk> tcb_queue_relation' getNext getPrev hp queue qhead qend;
   \<lbrakk> tcb_queue_relation getNext getPrev hp queue NULL qhead;
     qend = (if queue = [] then NULL else (tcb_ptr_to_ctcb_ptr (last queue))) \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" unfolding tcb_queue_relation'_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation' getNext getPrev hp queue qhead qend; \<lbrakk>tcb_queue_relation getNext getPrev hp queue NULL qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue))\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue)) \<and> tcb_queue_relation getNext getPrev hp queue NULL qhead; \<lbrakk>tcb_queue_relation getNext getPrev hp queue NULL qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue))\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory TcbQueue_C

lemma upd_unless_null_cong_helper:
  "\<And>p p' v mp S. \<lbrakk> p' \<in> tcb_ptr_to_ctcb_ptr ` S; ctcb_ptr_to_tcb_ptr p \<notin> S \<rbrakk> \<Longrightarrow> (upd_unless_null p v mp) p' = mp p'" unfolding upd_unless_null_def apply simp apply (intro impI conjI) apply (erule imageE) apply hypsubst apply (simp only: ctcb_ptr_to_ctcb_ptr) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>p p' v mp S. \<lbrakk>p' \<in> tcb_ptr_to_ctcb_ptr ` S; ctcb_ptr_to_tcb_ptr p \<notin> S\<rbrakk> \<Longrightarrow> upd_unless_null p v mp p' = mp p' proof (prove)
goal (1 subgoal):
 1. \<And>p p' v mp S. \<lbrakk>p' \<in> tcb_ptr_to_ctcb_ptr ` S; ctcb_ptr_to_tcb_ptr p \<notin> S\<rbrakk> \<Longrightarrow> (if p = NULL then mp else mp(p \<mapsto> v)) p' = mp p' proof (prove)
goal (1 subgoal):
 1. \<And>p p' v mp S. \<lbrakk>p' \<in> tcb_ptr_to_ctcb_ptr ` S; ctcb_ptr_to_tcb_ptr p \<notin> S\<rbrakk> \<Longrightarrow> p' = p \<longrightarrow> p \<noteq> NULL \<longrightarrow> Some v = mp p proof (prove)
goal (1 subgoal):
 1. \<And>p p' v mp S. \<lbrakk>p' \<in> tcb_ptr_to_ctcb_ptr ` S; ctcb_ptr_to_tcb_ptr p \<notin> S; p' = p; p \<noteq> NULL\<rbrakk> \<Longrightarrow> Some v = mp p proof (prove)
goal (1 subgoal):
 1. \<And>p p' v mp S x. \<lbrakk>ctcb_ptr_to_tcb_ptr p \<notin> S; p' = p; p \<noteq> NULL; p' = tcb_ptr_to_ctcb_ptr x; x \<in> S\<rbrakk> \<Longrightarrow> Some v = mp p proof (prove)
goal (1 subgoal):
 1. \<And>p p' v mp S x. \<lbrakk>ctcb_ptr_to_tcb_ptr (tcb_ptr_to_ctcb_ptr x) \<notin> S; tcb_ptr_to_ctcb_ptr x \<noteq> NULL; x \<in> S\<rbrakk> \<Longrightarrow> Some v = mp (tcb_ptr_to_ctcb_ptr x) proof (prove)
goal (1 subgoal):
 1. \<And>p p' v mp S x. \<lbrakk>\<not> True; tcb_ptr_to_ctcb_ptr x \<noteq> NULL; x \<in> S\<rbrakk> \<Longrightarrow> Some v = mp (tcb_ptr_to_ctcb_ptr x) proof (prove)
goal:
No subgoals!