theory CSpace_C

lemma cap_get_capIsPhysical_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       Call cap_get_capIsPhysical_'proc
       \<lbrace>\<acute>ret__unsigned_long = from_bool (get_capIsPhysical_CL (cap_lift \<^bsup>s\<^esup>cap))\<rbrace>" apply vcg apply (clarsimp simp: get_capIsPhysical_CL_def) apply (intro impI conjI) apply (clarsimp simp: cap_lifts pageBitsForSize_def
                                          cap_lift_asid_control_cap word_sle_def
                                          cap_lift_irq_control_cap cap_lift_null_cap
                                          mask_def objBits_simps cap_lift_domain_cap
                                          ptr_add_assertion_positive
                                   dest!: sym [where t = "cap_get_tag cap" for cap]
                                   split: vmpage_size.splits)+ 
  (* XXX: slow. there should be a rule for this *)
   by (case_tac "cap_lift cap", simp_all, case_tac a, auto simp: cap_lift_def cap_tag_defs Let_def
                  cap_small_frame_cap_lift_def cap_frame_cap_lift_def
                  cap_endpoint_cap_lift_def cap_notification_cap_lift_def
                  cap_cnode_cap_lift_def cap_thread_cap_lift_def
                  cap_zombie_cap_lift_def cap_page_table_cap_lift_def
                  cap_page_directory_cap_lift_def cap_asid_pool_cap_lift_def
                  Let_def cap_untyped_cap_lift_def  split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call cap_get_capIsPhysical_'proc \<lbrace>\<acute>ret__unsigned_long = from_bool (get_capIsPhysical_CL (cap_lift \<^bsup>s\<^esup>cap))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<forall>ret__unsigned. ret__unsigned = cap_get_tag cap \<longrightarrow> (cap_untyped_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) true = from_bool (get_capIsPhysical_CL (cap_lift cap))) \<and> (cap_untyped_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_endpoint_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) true = from_bool (get_capIsPhysical_CL (cap_lift cap))) \<and> (cap_endpoint_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_notification_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) true = from_bool (get_capIsPhysical_CL (cap_lift cap))) \<and> (cap_notification_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_cnode_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) true = from_bool (get_capIsPhysical_CL (cap_lift cap))) \<and> (cap_cnode_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_thread_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) true = from_bool (get_capIsPhysical_CL (cap_lift cap))) \<and> (cap_thread_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_zombie_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) true = from_bool (get_capIsPhysical_CL (cap_lift cap))) \<and> (cap_zombie_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_domain_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) false = from_bool (get_capIsPhysical_CL (cap_lift cap))) \<and> (cap_domain_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_reply_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) false = from_bool (get_capIsPhysical_CL (cap_lift cap))) \<and> (cap_reply_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_irq_control_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) false = from_bool (get_capIsPhysical_CL (cap_lift cap))) \<and> (cap_irq_control_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_irq_handler_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) false = from_bool (get_capIsPhysical_CL (cap_lift cap))) \<and> (cap_irq_handler_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = cap_get_tag cap \<longrightarrow> (cap_small_frame_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) true = from_bool (get_capIsPhysical_CL (cap_lift cap))) \<and> (cap_small_frame_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_frame_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) true = from_bool (get_capIsPhysical_CL (cap_lift cap))) \<and> (cap_frame_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_page_table_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) true = from_bool (get_capIsPhysical_CL (cap_lift cap))) \<and> (cap_page_table_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_page_directory_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) true = from_bool (get_capIsPhysical_CL (cap_lift cap))) \<and> (cap_page_directory_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_asid_pool_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) true = from_bool (get_capIsPhysical_CL (cap_lift cap))) \<and> (cap_asid_pool_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> (cap_asid_control_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) false = from_bool (get_capIsPhysical_CL (cap_lift cap))) \<and> (cap_asid_control_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) false = from_bool (get_capIsPhysical_CL (cap_lift cap))))))))))))))))))) proof (prove)
goal (1 subgoal):
 1. \<And>cap. (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<longrightarrow> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_notification_cap \<longrightarrow> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_notification_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap \<longrightarrow> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_cnode_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap \<longrightarrow> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_thread_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_domain_cap \<longrightarrow> \<not> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_domain_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_reply_cap \<longrightarrow> \<not> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_reply_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap \<longrightarrow> \<not> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> \<not> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap \<longrightarrow> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_page_table_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap \<longrightarrow> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap \<longrightarrow> \<not> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)))))))))))))))) proof (prove)
goal (16 subgoals):
 1. \<And>cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<Longrightarrow> case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True
 2. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap\<rbrakk> \<Longrightarrow> case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True
 3. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_notification_cap\<rbrakk> \<Longrightarrow> case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True
 4. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_notification_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap\<rbrakk> \<Longrightarrow> case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True
 5. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_notification_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_cnode_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap\<rbrakk> \<Longrightarrow> case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True
 6. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_notification_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_cnode_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_thread_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap\<rbrakk> \<Longrightarrow> case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True
 7. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_notification_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_cnode_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_thread_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_domain_cap\<rbrakk> \<Longrightarrow> \<not> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)
 8. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_notification_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_cnode_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_thread_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_domain_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_reply_cap\<rbrakk> \<Longrightarrow> \<not> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)
 9. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_notification_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_cnode_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_thread_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_domain_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_reply_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap\<rbrakk> \<Longrightarrow> \<not> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)
 10. \<And>cap. \<lbrakk>cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_notification_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_cnode_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_thread_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_zombie_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_domain_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_reply_cap; cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap\<rbrakk> \<Longrightarrow> \<not> (case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True)
A total of 16 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap_lift cap \<noteq> Some (Cap_untyped_cap (cap_untyped_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_endpoint_cap (cap_endpoint_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_notification_cap (cap_notification_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_cnode_cap (cap_cnode_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_thread_cap (cap_thread_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_zombie_cap (cap_zombie_cap_lift cap)); cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_domain_cap; cap_lift cap \<noteq> Some (Cap_reply_cap (cap_reply_cap_lift cap)); cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap; cap_lift cap \<noteq> Some (Cap_irq_handler_cap (cap_irq_handler_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_small_frame_cap (cap_small_frame_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_frame_cap (cap_frame_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_page_table_cap (cap_page_table_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_page_directory_cap (cap_page_directory_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_asid_pool_cap (cap_asid_pool_cap_lift cap)); case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap_lift cap \<noteq> Some (Cap_untyped_cap (cap_untyped_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_endpoint_cap (cap_endpoint_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_notification_cap (cap_notification_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_cnode_cap (cap_cnode_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_thread_cap (cap_thread_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_zombie_cap (cap_zombie_cap_lift cap)); cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_domain_cap; cap_lift cap \<noteq> Some (Cap_reply_cap (cap_reply_cap_lift cap)); cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap; cap_lift cap \<noteq> Some (Cap_irq_handler_cap (cap_irq_handler_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_small_frame_cap (cap_small_frame_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_frame_cap (cap_frame_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_page_table_cap (cap_page_table_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_page_directory_cap (cap_page_directory_cap_lift cap)); cap_lift cap \<noteq> Some (Cap_asid_pool_cap (cap_asid_pool_cap_lift cap)); case cap_lift cap of None \<Rightarrow> False | Some Cap_null_cap \<Rightarrow> False | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> False | Some Cap_asid_control_cap \<Rightarrow> False | Some Cap_irq_control_cap \<Rightarrow> False | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> False | Some Cap_domain_cap \<Rightarrow> False | Some _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> False