theory SR_lemmas_C

lemma cap_get_tag_isCap_unfolded_H_cap:
  shows "ccap_relation (capability.ThreadCap v0) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_thread_cap)"
  and "ccap_relation (capability.NullCap) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_null_cap)"
  and "ccap_relation (capability.NotificationCap v4 v5 v6 v7) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_notification_cap) "
  and "ccap_relation (capability.EndpointCap v8 v9 v10 v10b v11 v12) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_endpoint_cap)"
  and "ccap_relation (capability.IRQHandlerCap v13) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_irq_handler_cap)"
  and "ccap_relation (capability.IRQControlCap) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_irq_control_cap)"
  and "ccap_relation (capability.Zombie v14 v15 v16) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_zombie_cap)"
  and "ccap_relation (capability.ReplyCap v17 v18 vr18b) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_reply_cap)"
  and "ccap_relation (capability.UntypedCap v100 v19 v20 v20b) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_untyped_cap)"
  and "ccap_relation (capability.CNodeCap v21 v22 v23 v24) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_cnode_cap)"
  and "ccap_relation (capability.DomainCap) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_domain_cap)"

  and "ccap_relation (capability.ArchObjectCap arch_capability.ASIDControlCap) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_asid_control_cap)"
  and "ccap_relation (capability.ArchObjectCap (arch_capability.ASIDPoolCap v28 v29)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_asid_pool_cap)"
  and "ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap v30 v31)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_page_table_cap)"
  and "ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap v32 v33)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_page_directory_cap)"

  and "\<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap v101 v34 v35 v36 v37)) cap'; v36=ARMSmallPage\<rbrakk>  \<Longrightarrow> (cap_get_tag cap' = scast cap_small_frame_cap)"
  and "\<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap v102 v38 v39 v40 v41)) cap'; v40\<noteq>ARMSmallPage\<rbrakk>  \<Longrightarrow> (cap_get_tag cap' = scast cap_frame_cap)"
  and "ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap v42 v43)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_page_directory_cap)"
  and "ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap v44 v45)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_page_directory_cap)" apply (simp add: cap_get_tag_isCap cap_get_tag_isCap_ArchObject isCap_simps) apply (frule cap_get_tag_isCap(2), simp) apply (simp add: cap_get_tag_isCap cap_get_tag_isCap_ArchObject isCap_simps pageSize_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((((ccap_relation (capability.ThreadCap v0) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) &&& (ccap_relation capability.NullCap cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_null_cap)) &&& (ccap_relation (capability.NotificationCap v4 v5 v6 v7) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap) &&& (ccap_relation (capability.EndpointCap v8 v9 v10 v10b v11 v12) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap)) &&& ((ccap_relation (capability.IRQHandlerCap v13) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap) &&& (ccap_relation capability.IRQControlCap cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap)) &&& (ccap_relation (capability.Zombie v14 v15 v16) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap) &&& (ccap_relation (capability.ReplyCap v17 v18 vr18b) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_reply_cap) &&& (ccap_relation (capability.UntypedCap v100 v19 v20 v20b) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap)) &&& (((ccap_relation (capability.CNodeCap v21 v22 v23 v24) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap) &&& (ccap_relation capability.DomainCap cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_domain_cap)) &&& (ccap_relation (capability.ArchObjectCap arch_capability.ASIDControlCap) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap) &&& (ccap_relation (capability.ArchObjectCap (arch_capability.ASIDPoolCap v28 v29)) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap) &&& (ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap v30 v31)) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap)) &&& ((ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap v32 v33)) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) &&& (\<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap v101 v34 v35 v36 v37)) cap'; v36 = Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap)) &&& (\<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap v102 v38 v39 v40 v41)) cap'; v40 \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_frame_cap) &&& (ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap v42 v43)) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) &&& (ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap v44 v45)) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) proof (prove)
goal (18 subgoals):
 1. ccap_relation capability.NullCap cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_null_cap
 2. ccap_relation (capability.NotificationCap v4 v5 v6 v7) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap
 3. ccap_relation (capability.EndpointCap v8 v9 v10 v10b v11 v12) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap
 4. ccap_relation (capability.IRQHandlerCap v13) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap
 5. ccap_relation capability.IRQControlCap cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap
 6. ccap_relation (capability.Zombie v14 v15 v16) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap
 7. ccap_relation (capability.ReplyCap v17 v18 vr18b) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_reply_cap
 8. ccap_relation (capability.UntypedCap v100 v19 v20 v20b) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap
 9. ccap_relation (capability.CNodeCap v21 v22 v23 v24) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap
 10. ccap_relation capability.DomainCap cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_domain_cap
A total of 18 subgoals... proof (prove)
goal (17 subgoals):
 1. ccap_relation (capability.NotificationCap v4 v5 v6 v7) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap
 2. ccap_relation (capability.EndpointCap v8 v9 v10 v10b v11 v12) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap
 3. ccap_relation (capability.IRQHandlerCap v13) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap
 4. ccap_relation capability.IRQControlCap cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap
 5. ccap_relation (capability.Zombie v14 v15 v16) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap
 6. ccap_relation (capability.ReplyCap v17 v18 vr18b) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_reply_cap
 7. ccap_relation (capability.UntypedCap v100 v19 v20 v20b) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap
 8. ccap_relation (capability.CNodeCap v21 v22 v23 v24) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap
 9. ccap_relation capability.DomainCap cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_domain_cap
 10. ccap_relation (capability.ArchObjectCap arch_capability.ASIDControlCap) cap' \<Longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap
A total of 17 subgoals... proof (prove)
goal:
No subgoals!