kings-crown/FVELER_Isabelle huggingface dataset:
theory Boolean_C

lemma to_bool_to_bool_bf:
  "w = false \<or> w = true \<Longrightarrow> to_bool_bf w = to_bool w" by (auto simp: false_def true_def to_bool_def to_bool_bf_def mask_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w = false \<or> w = true \<Longrightarrow> to_bool_bf w = to_bool w
theory Boolean_C

lemma to_bool_bf_and[simp]:
  "to_bool_bf (a && b) = (to_bool_bf a \<and> to_bool_bf b)" apply (clarsimp simp: to_bool_bf_def) apply (rule iffI) apply (subst (asm) bang_eq) apply (simp add: word_size) apply (rule conjI) apply (rule word_eqI) apply (auto simp add: word_size)[1] apply (rule word_eqI) apply (auto simp add: word_size)[1] apply clarsimp apply (rule word_eqI) apply (subst (asm) bang_eq)+ apply (auto simp add: word_size)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bool_bf (a && b) = (to_bool_bf a \<and> to_bool_bf b) proof (prove)
goal (1 subgoal):
 1. ((a && b) && 1 = 1) = (a && 1 = 1 \<and> b && 1 = 1) proof (prove)
goal (2 subgoals):
 1. (a && b) && 1 = 1 \<Longrightarrow> a && 1 = 1 \<and> b && 1 = 1
 2. a && 1 = 1 \<and> b && 1 = 1 \<Longrightarrow> (a && b) && 1 = 1 proof (prove)
goal (2 subgoals):
 1. \<forall>n. ((a && b) && 1) !! n = 1 !! n \<Longrightarrow> a && 1 = 1 \<and> b && 1 = 1
 2. a && 1 = 1 \<and> b && 1 = 1 \<Longrightarrow> (a && b) && 1 = 1 proof (prove)
goal (2 subgoals):
 1. \<forall>n. (a !! n \<and> b !! n \<and> n = 0) = (n = 0) \<Longrightarrow> a && 1 = 1 \<and> b && 1 = 1
 2. a && 1 = 1 \<and> b && 1 = 1 \<Longrightarrow> (a && b) && 1 = 1 proof (prove)
goal (3 subgoals):
 1. \<forall>n. (a !! n \<and> b !! n \<and> n = 0) = (n = 0) \<Longrightarrow> a && 1 = 1
 2. \<forall>n. (a !! n \<and> b !! n \<and> n = 0) = (n = 0) \<Longrightarrow> b && 1 = 1
 3. a && 1 = 1 \<and> b && 1 = 1 \<Longrightarrow> (a && b) && 1 = 1 proof (prove)
goal (3 subgoals):
 1. \<And>n. \<forall>n. (a !! n \<and> b !! n \<and> n = 0) = (n = 0) \<Longrightarrow> n < size (a && 1) \<longrightarrow> (a && 1) !! n = 1 !! n
 2. \<forall>n. (a !! n \<and> b !! n \<and> n = 0) = (n = 0) \<Longrightarrow> b && 1 = 1
 3. a && 1 = 1 \<and> b && 1 = 1 \<Longrightarrow> (a && b) && 1 = 1 proof (prove)
goal (2 subgoals):
 1. \<forall>n. (a !! n \<and> b !! n \<and> n = 0) = (n = 0) \<Longrightarrow> b && 1 = 1
 2. a && 1 = 1 \<and> b && 1 = 1 \<Longrightarrow> (a && b) && 1 = 1 proof (prove)
goal (2 subgoals):
 1. \<And>n. \<forall>n. (a !! n \<and> b !! n \<and> n = 0) = (n = 0) \<Longrightarrow> n < size (b && 1) \<longrightarrow> (b && 1) !! n = 1 !! n
 2. a && 1 = 1 \<and> b && 1 = 1 \<Longrightarrow> (a && b) && 1 = 1 proof (prove)
goal (1 subgoal):
 1. a && 1 = 1 \<and> b && 1 = 1 \<Longrightarrow> (a && b) && 1 = 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a && 1 = 1; b && 1 = 1\<rbrakk> \<Longrightarrow> (a && b) && 1 = 1 proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>a && 1 = 1; b && 1 = 1\<rbrakk> \<Longrightarrow> n < size ((a && b) && 1) \<longrightarrow> ((a && b) && 1) !! n = 1 !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n. (a && 1) !! n = 1 !! n; \<forall>n. (b && 1) !! n = 1 !! n\<rbrakk> \<Longrightarrow> n < size ((a && b) && 1) \<longrightarrow> ((a && b) && 1) !! n = 1 !! n proof (prove)
goal:
No subgoals!
theory Boolean_C

lemma to_bool_bf_to_bool_mask:
  "w && mask (Suc 0) = w \<Longrightarrow> to_bool_bf w = to_bool (w::machine_word)" by (metis mask_Suc_0 bool_mask mask_1 to_bool_0 to_bool_1 to_bool_bf_def word_gt_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w && mask (Suc 0) = w \<Longrightarrow> to_bool_bf w = to_bool w
theory Boolean_C

lemma to_bool_mask_to_bool_bf:
  "to_bool (x && 1) = to_bool_bf (x::machine_word)" by (simp add: to_bool_bf_def to_bool_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bool (x && 1) = to_bool_bf x
theory CLevityCatch

lemma ntfnQueue_head_mask_4 :
  "ntfnQueue_head_CL (notification_lift ko') && ~~ mask 4 = ntfnQueue_head_CL (notification_lift ko')" unfolding notification_lift_def by (clarsimp simp: mask_def word_bw_assocs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ntfnQueue_head_CL (notification_lift ko') && ~~ mask 4 = ntfnQueue_head_CL (notification_lift ko') proof (prove)
goal (1 subgoal):
 1. ntfnQueue_head_CL \<lparr>ntfnBoundTCB_CL = (notification_C.words_C ko'.[3] << 0) && ~~ mask 4, ntfnMsgIdentifier_CL = notification_C.words_C ko'.[2] >> 0, ntfnQueue_head_CL = (notification_C.words_C ko'.[1] << 0) && ~~ mask 4, ntfnQueue_tail_CL = (notification_C.words_C ko'.[0] << 0) && ~~ mask 4, state_CL = (notification_C.words_C ko'.[0] >> 0) && mask 2\<rparr> && ~~ mask 4 = ntfnQueue_head_CL \<lparr>ntfnBoundTCB_CL = (notification_C.words_C ko'.[3] << 0) && ~~ mask 4, ntfnMsgIdentifier_CL = notification_C.words_C ko'.[2] >> 0, ntfnQueue_head_CL = (notification_C.words_C ko'.[1] << 0) && ~~ mask 4, ntfnQueue_tail_CL = (notification_C.words_C ko'.[0] << 0) && ~~ mask 4, state_CL = (notification_C.words_C ko'.[0] >> 0) && mask 2\<rparr>
theory CLevityCatch

lemma empty_fail_doMachineOp[intro!]:
  "empty_fail m \<Longrightarrow> empty_fail (doMachineOp m)" by (rule ef_dmo')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail m \<Longrightarrow> empty_fail (doMachineOp m)
theory CLevityCatch

lemma no_overlap_new_cap_addrs_disjoint:
  "\<lbrakk> range_cover ptr sz (objBitsKO ko) n;
     pspace_aligned' s;
     pspace_no_overlap' ptr sz s \<rbrakk> \<Longrightarrow>
   set (new_cap_addrs n ptr ko) \<inter> dom (ksPSpace s) = {}" apply (erule disjoint_subset [OF new_cap_addrs_subset, where sz1=sz]) apply (clarsimp simp: More_Word_Operations.ptr_add_def field_simps) apply (rule pspace_no_overlap_disjoint') apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO ko) n; pspace_aligned' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> set (new_cap_addrs n ptr ko) \<inter> dom (ksPSpace s) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> {ptr..More_Word_Operations.ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)} \<inter> dom (ksPSpace s) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_aligned' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> pspace_aligned' s
 2. \<lbrakk>pspace_aligned' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr sz s proof (prove)
goal:
No subgoals!
theory Wellformed_C

lemma halt_spec:
  "Gamma \<turnstile> {} Call halt_'proc {}" apply (rule hoare_complete) apply (simp add: HoarePartialDef.valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Gamma\<turnstile> {} Call halt_'proc {} proof (prove)
goal (1 subgoal):
 1. Gamma\<Turnstile>\<^bsub>/{}\<^esub> {} Call halt_'proc {},{} proof (prove)
goal:
No subgoals!
theory Wellformed_C

lemma ptr_val_tcb_ptr_mask2:
  "is_aligned thread tcbBlockSizeBits
      \<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr thread) && (~~ mask tcbBlockSizeBits)
                  = thread" apply (clarsimp simp: tcb_ptr_to_ctcb_ptr_def projectKOs) apply (simp add: is_aligned_add_helper ctcb_offset_defs objBits_simps') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned thread tcbBlockSizeBits \<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr thread) && ~~ mask tcbBlockSizeBits = thread proof (prove)
goal (1 subgoal):
 1. is_aligned thread tcbBlockSizeBits \<Longrightarrow> thread + ctcb_offset && ~~ mask tcbBlockSizeBits = thread proof (prove)
goal:
No subgoals!
theory Wellformed_C

lemma min_prio_dom_sanity:
  "seL4_MinPrio = 0"
  "Kernel_C.minDom = 0" by (auto simp: seL4_MinPrio_def minDom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. seL4_MinPrio = 0 &&& minDom = 0
theory Wellformed_C

lemma less_numDomains_is_domain[simplified word_size, simplified]:
  "x < numDomains \<Longrightarrow> x < 2 ^ size (y::domain)" unfolding Kernel_Config.numDomains_def by (simp add: word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < numDomains \<Longrightarrow> x < 2 ^ size y proof (prove)
goal (1 subgoal):
 1. x < 16 \<Longrightarrow> x < 2 ^ size y
theory Wellformed_C

lemma sint_numDomains_to_H:
  "sint Kernel_C.numDomains = int Kernel_Config.numDomains" by (clarsimp simp: Kernel_C.numDomains_def Kernel_Config.numDomains_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sint Kernel_C.numDomains = int numDomains
theory Wellformed_C

lemma unat_numDomains_to_H:
  "unat Kernel_C.numDomains = Kernel_Config.numDomains" by (clarsimp simp: Kernel_C.numDomains_def Kernel_Config.numDomains_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat Kernel_C.numDomains = numDomains
theory Wellformed_C

lemma maxDom_sgt_0_maxDomain:
  "0 <s maxDom \<longleftrightarrow> 0 < maxDomain" unfolding Kernel_C.maxDom_def maxDomain_def Kernel_Config.numDomains_def by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0 <s maxDom) = (0 < maxDomain) proof (prove)
goal (1 subgoal):
 1. (0 <s 0xF) = (0 < fromIntegral (16 - 1))
theory Wellformed_C

lemma num_domains_calculation:
  "num_domains = numDomains" unfolding num_domains_def by eval

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. num_domains = numDomains proof (prove)
goal (1 subgoal):
 1. 16 = numDomains
theory Wellformed_C

lemma num_domains_card_explicit:
  "num_domains = CARD(num_domains)" by (simp add: num_domains_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. num_domains = CARD(16)
theory Wellformed_C

lemma numDomains_less_numeric_explicit[simplified num_domains_def One_nat_def]:
  "x < Kernel_Config.numDomains \<Longrightarrow> x < num_domains" by (simp add: num_domains_calculation)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < numDomains \<Longrightarrow> x < num_domains
theory Wellformed_C

lemma numDomains_less_unat_ucast_explicit[simplified num_domains_def]:
  "unat x < Kernel_Config.numDomains \<Longrightarrow> (ucast (x::domain) :: machine_word) < of_nat num_domains" apply (rule word_less_nat_alt[THEN iffD2]) apply transfer apply simp apply (drule numDomains_less_numeric_explicit, simp add: num_domains_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat x < numDomains \<Longrightarrow> UCAST(8 \<rightarrow> 32) x < word_of_nat num_domains proof (prove)
goal (1 subgoal):
 1. unat x < numDomains \<Longrightarrow> unat (UCAST(8 \<rightarrow> 32) x) < unat (word_of_nat num_domains) proof (prove)
goal (1 subgoal):
 1. \<And>x. (nat \<circ> take_bit LENGTH(8)) x < numDomains \<Longrightarrow> (nat \<circ> take_bit LENGTH(32)) (take_bit LENGTH(8) x) < (nat \<circ> take_bit LENGTH(32)) (int num_domains) proof (prove)
goal (1 subgoal):
 1. \<And>x. nat (take_bit 8 x) < numDomains \<Longrightarrow> 0 < take_bit 32 (int num_domains) \<and> take_bit 8 x < take_bit 32 (int num_domains) proof (prove)
goal:
No subgoals!
theory Wellformed_C

lemma maxPrio_to_H:
  "ucast seL4_MaxPrio = maxPriority" by (simp add: maxPriority_def seL4_MaxPrio_def numPriorities_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio = maxPriority
theory Wellformed_C

lemma num_tcb_queues_calculation:
  "num_tcb_queues = numDomains * numPriorities" unfolding num_tcb_queues_def by eval

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. num_tcb_queues = numDomains * Config_H.numPriorities proof (prove)
goal (1 subgoal):
 1. 4096 = numDomains * Config_H.numPriorities
theory StateRelation_C

lemma ccap_relation_c_valid_cap: "ccap_relation  c c' \<Longrightarrow> c_valid_cap c'" by (simp add: ccap_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccap_relation c c' \<Longrightarrow> c_valid_cap c'
theory SR_lemmas_C

lemma cteMDBNode_cte_to_H [simp]:
  "cteMDBNode (cte_to_H cte) = mdb_node_to_H (cteMDBNode_CL cte)" unfolding cte_to_H_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cteMDBNode (cte_to_H cte) = mdb_node_to_H (cteMDBNode_CL cte) proof (prove)
goal (1 subgoal):
 1. cteMDBNode (CTE (cap_to_H (cap_CL cte)) (mdb_node_to_H (cteMDBNode_CL cte))) = mdb_node_to_H (cteMDBNode_CL cte)
theory SR_lemmas_C

lemma cteMDBNode_CL_lift [simp]:
  "cte_lift cte' = Some ctel \<Longrightarrow>
  mdb_node_lift (cteMDBNode_C cte') = cteMDBNode_CL ctel" unfolding cte_lift_def by (fastforce split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_lift cte' = Some ctel \<Longrightarrow> mdb_node_lift (cteMDBNode_C cte') = cteMDBNode_CL ctel proof (prove)
goal (1 subgoal):
 1. (case cap_lift (cte_C.cap_C cte') of None \<Rightarrow> None | Some cap \<Rightarrow> Some \<lparr>cap_CL = cap, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte')\<rparr>) = Some ctel \<Longrightarrow> mdb_node_lift (cteMDBNode_C cte') = cteMDBNode_CL ctel
theory SR_lemmas_C

lemma cteCap_cte_to_H [simp]:
  "cteCap (cte_to_H cte) = cap_to_H (cap_CL cte)" unfolding cte_to_H_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cteCap (cte_to_H cte) = cap_to_H (cap_CL cte) proof (prove)
goal (1 subgoal):
 1. cteCap (CTE (cap_to_H (cap_CL cte)) (mdb_node_to_H (cteMDBNode_CL cte))) = cap_to_H (cap_CL cte)
theory SR_lemmas_C

lemma cap_CL_lift [simp]:
  "cte_lift cte' = Some ctel \<Longrightarrow> cap_lift (cte_C.cap_C cte') = Some (cap_CL ctel)" unfolding cte_lift_def by (fastforce split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_lift cte' = Some ctel \<Longrightarrow> cap_lift (cte_C.cap_C cte') = Some (cap_CL ctel) proof (prove)
goal (1 subgoal):
 1. (case cap_lift (cte_C.cap_C cte') of None \<Rightarrow> None | Some cap \<Rightarrow> Some \<lparr>cap_CL = cap, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte')\<rparr>) = Some ctel \<Longrightarrow> cap_lift (cte_C.cap_C cte') = Some (cap_CL ctel)
theory SR_lemmas_C

lemma cteMDBNode_C_update_lift [simp]:
  "cte_lift cte' = Some ctel \<Longrightarrow>
  (cte_lift (cteMDBNode_C_update (\<lambda>_. m) cte') = Some x)
  = (cteMDBNode_CL_update (\<lambda>_. mdb_node_lift m) ctel = x)" unfolding cte_lift_def by (fastforce split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_lift cte' = Some ctel \<Longrightarrow> (cte_lift (cteMDBNode_C_update (\<lambda>_. m) cte') = Some x) = (ctel\<lparr>cteMDBNode_CL := mdb_node_lift m\<rparr> = x) proof (prove)
goal (1 subgoal):
 1. (case cap_lift (cte_C.cap_C cte') of None \<Rightarrow> None | Some cap \<Rightarrow> Some \<lparr>cap_CL = cap, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte')\<rparr>) = Some ctel \<Longrightarrow> ((case cap_lift (cte_C.cap_C (cteMDBNode_C_update (\<lambda>_. m) cte')) of None \<Rightarrow> None | Some cap \<Rightarrow> Some \<lparr>cap_CL = cap, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C (cteMDBNode_C_update (\<lambda>_. m) cte'))\<rparr>) = Some x) = (ctel\<lparr>cteMDBNode_CL := mdb_node_lift m\<rparr> = x)
theory SR_lemmas_C

lemma ccap_relationE:
  "\<lbrakk>ccap_relation c v; \<And>vl. \<lbrakk> cap_lift v = Some vl; c = cap_to_H vl; c_valid_cap v\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" unfolding ccap_relation_def map_option_case apply clarsimp apply (drule sym) apply (clarsimp split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation c v; \<And>vl. \<lbrakk>cap_lift v = Some vl; c = cap_to_H vl; c_valid_cap v\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some c = (case cap_lift v of None \<Rightarrow> None | Some x \<Rightarrow> Some (cap_to_H x)) \<and> c_valid_cap v; \<And>vl. \<lbrakk>cap_lift v = Some vl; c = cap_to_H vl; c_valid_cap v\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>vl. \<lbrakk>cap_lift v = Some vl; c = cap_to_H vl\<rbrakk> \<Longrightarrow> P; Some c = (case cap_lift v of None \<Rightarrow> None | Some x \<Rightarrow> Some (cap_to_H x)); c_valid_cap v\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>vl. \<lbrakk>cap_lift v = Some vl; c = cap_to_H vl\<rbrakk> \<Longrightarrow> P; c_valid_cap v; (case cap_lift v of None \<Rightarrow> None | Some x \<Rightarrow> Some (cap_to_H x)) = Some c\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma isArchCap_tag_def2:
  "isArchCap_tag n \<equiv> n && 1 = 1" by (simp add: isArchCap_tag_def word_mod_2p_is_mask[where n=1, simplified] mask_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isArchCap_tag n \<equiv> n && 1 = 1
theory SR_lemmas_C

lemma framesize_to_H_not_Small [simp]:
  "framesize_to_H w \<noteq> ARMSmallPage" by (simp add: framesize_to_H_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. framesize_to_H w \<noteq> Wellformed_C.ARMSmallPage
theory SR_lemmas_C

lemma cap_get_tag_NullCap:
  assumes cr: "ccap_relation cap cap'"
  shows "(cap_get_tag cap' = scast cap_null_cap) = (cap = NullCap)" using cr apply - apply (rule iffI) apply (clarsimp simp add: cap_lifts cap_get_tag_isCap cap_to_H_def) apply (simp add: cap_get_tag_isCap isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cap = capability.NullCap) proof (prove)
using this:
ccap_relation cap cap'

goal (1 subgoal):
 1. (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cap = capability.NullCap) proof (prove)
goal (1 subgoal):
 1. ccap_relation cap cap' \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cap = capability.NullCap) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccap_relation cap cap'; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> cap = capability.NullCap
 2. \<lbrakk>ccap_relation cap cap'; cap = capability.NullCap\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_null_cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap cap'; cap = capability.NullCap\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_null_cap proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma cap_get_tag_ThreadCap:
  assumes cr: "ccap_relation cap cap'"
  shows "(cap_get_tag cap' = scast cap_thread_cap) =
  (cap = ThreadCap (ctcb_ptr_to_tcb_ptr (Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap')))))" using cr apply - apply (rule iffI) apply (erule ccap_relationE) apply (clarsimp simp add: cap_lifts cap_to_H_def) apply (simp add: cap_get_tag_isCap isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) = (cap = capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap'))))) proof (prove)
using this:
ccap_relation cap cap'

goal (1 subgoal):
 1. (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) = (cap = capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap'))))) proof (prove)
goal (1 subgoal):
 1. ccap_relation cap cap' \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) = (cap = capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap'))))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccap_relation cap cap'; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_thread_cap\<rbrakk> \<Longrightarrow> cap = capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap'))))
 2. \<lbrakk>ccap_relation cap cap'; cap = capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap'))))\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_thread_cap proof (prove)
goal (2 subgoals):
 1. \<And>vl. \<lbrakk>cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_thread_cap; cap_lift cap' = Some vl; cap = cap_to_H vl; c_valid_cap cap'\<rbrakk> \<Longrightarrow> cap = capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap'))))
 2. \<lbrakk>ccap_relation cap cap'; cap = capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap'))))\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_thread_cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap cap'; cap = capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap'))))\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_thread_cap proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma cap_get_tag_IRQControlCap:
  assumes cr: "ccap_relation cap cap'"
  shows "(cap_get_tag cap' = scast cap_irq_control_cap) =
  (cap = capability.IRQControlCap)" using cr apply - apply (rule iffI) apply (clarsimp simp add: cap_lifts cap_get_tag_isCap isCap_simps cap_to_H_def) apply (simp add: cap_get_tag_isCap isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap) = (cap = capability.IRQControlCap) proof (prove)
using this:
ccap_relation cap cap'

goal (1 subgoal):
 1. (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap) = (cap = capability.IRQControlCap) proof (prove)
goal (1 subgoal):
 1. ccap_relation cap cap' \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap) = (cap = capability.IRQControlCap) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccap_relation cap cap'; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap\<rbrakk> \<Longrightarrow> cap = capability.IRQControlCap
 2. \<lbrakk>ccap_relation cap cap'; cap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap cap'; cap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma cap_get_tag_DomainCap:
  assumes cr: "ccap_relation cap cap'"
  shows "(cap_get_tag cap' = scast cap_domain_cap) = (cap = DomainCap)" using cr apply - apply (rule iffI) apply (clarsimp simp add: cap_lifts cap_get_tag_isCap cap_to_H_def) apply (simp add: cap_get_tag_isCap isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_domain_cap) = (cap = capability.DomainCap) proof (prove)
using this:
ccap_relation cap cap'

goal (1 subgoal):
 1. (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_domain_cap) = (cap = capability.DomainCap) proof (prove)
goal (1 subgoal):
 1. ccap_relation cap cap' \<Longrightarrow> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_domain_cap) = (cap = capability.DomainCap) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccap_relation cap cap'; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_domain_cap\<rbrakk> \<Longrightarrow> cap = capability.DomainCap
 2. \<lbrakk>ccap_relation cap cap'; cap = capability.DomainCap\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_domain_cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap cap'; cap = capability.DomainCap\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_domain_cap proof (prove)
goal:
No subgoals!