theory CSpaceInv_AI

lemma replaceable_cap_range:
 "replaceable s p cap c \<Longrightarrow> cap_range cap \<subseteq> cap_range c" apply (simp add: replaceable_def) apply (elim disjE,simp_all) apply (clarsimp simp: cap_range_def) apply (case_tac cap,simp_all add: is_cap_simps cap_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. replaceable s p cap c \<Longrightarrow> cap_range cap \<subseteq> cap_range c proof (prove)
goal (1 subgoal):
 1. c = cap \<or> \<not> is_final_cap' c s \<and> cap = NullCap \<and> replaceable_non_final_arch_cap s p cap c \<or> is_final_cap' c s \<and> (\<forall>p\<in>zobj_refs c - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<forall>a b. (a, b) \<in> cte_refs c (interrupt_irq_node s) \<and> ((a, b) \<in> cte_refs cap (interrupt_irq_node s) \<longrightarrow> (\<exists>cp. appropriate_cte_cap cp c \<and> \<not> appropriate_cte_cap cp cap)) \<longrightarrow> ((a, b) \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) (a, b) s) \<and> ((a, b) = p \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs c \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range c) \<and> (is_master_reply_cap c \<longrightarrow> cap = NullCap) \<and> (is_reply_cap c \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap c \<longrightarrow> tcb_cap_valid c p s \<longrightarrow> tcb_cap_valid cap p s) \<and> \<not> is_untyped_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_reply_cap cap \<and> cap \<noteq> IRQControlCap \<and> (cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class c \<and> cap_is_device cap = cap_is_device c) \<and> replaceable_final_arch_cap s p cap c \<Longrightarrow> cap_range cap \<subseteq> cap_range c proof (prove)
goal (2 subgoals):
 1. \<not> is_final_cap' c s \<and> cap = NullCap \<and> replaceable_non_final_arch_cap s p cap c \<Longrightarrow> cap_range NullCap \<subseteq> cap_range c
 2. is_final_cap' c s \<and> (\<forall>p\<in>zobj_refs c - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<forall>a b. (a, b) \<in> cte_refs c (interrupt_irq_node s) \<and> ((a, b) \<in> cte_refs cap (interrupt_irq_node s) \<longrightarrow> (\<exists>cp. appropriate_cte_cap cp c \<and> \<not> appropriate_cte_cap cp cap)) \<longrightarrow> ((a, b) \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) (a, b) s) \<and> ((a, b) = p \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs c \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range c) \<and> (is_master_reply_cap c \<longrightarrow> cap = NullCap) \<and> (is_reply_cap c \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap c \<longrightarrow> tcb_cap_valid c p s \<longrightarrow> tcb_cap_valid cap p s) \<and> \<not> is_untyped_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_reply_cap cap \<and> cap \<noteq> IRQControlCap \<and> (cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class c \<and> cap_is_device cap = cap_is_device c) \<and> replaceable_final_arch_cap s p cap c \<Longrightarrow> cap_range cap \<subseteq> cap_range c proof (prove)
goal (1 subgoal):
 1. is_final_cap' c s \<and> (\<forall>p\<in>zobj_refs c - zobj_refs cap. obj_at (Not \<circ> live) p s) \<and> (\<forall>a b. (a, b) \<in> cte_refs c (interrupt_irq_node s) \<and> ((a, b) \<in> cte_refs cap (interrupt_irq_node s) \<longrightarrow> (\<exists>cp. appropriate_cte_cap cp c \<and> \<not> appropriate_cte_cap cp cap)) \<longrightarrow> ((a, b) \<noteq> p \<longrightarrow> cte_wp_at ((=) NullCap) (a, b) s) \<and> ((a, b) = p \<longrightarrow> cap = NullCap)) \<and> gen_obj_refs cap \<subseteq> gen_obj_refs c \<and> (cap \<noteq> NullCap \<longrightarrow> cap_range cap = cap_range c) \<and> (is_master_reply_cap c \<longrightarrow> cap = NullCap) \<and> (is_reply_cap c \<longrightarrow> cap = NullCap) \<and> (\<not> is_master_reply_cap c \<longrightarrow> tcb_cap_valid c p s \<longrightarrow> tcb_cap_valid cap p s) \<and> \<not> is_untyped_cap cap \<and> \<not> is_master_reply_cap cap \<and> \<not> is_reply_cap cap \<and> cap \<noteq> IRQControlCap \<and> (cap \<noteq> NullCap \<longrightarrow> cap_class cap = cap_class c \<and> cap_is_device cap = cap_is_device c) \<and> replaceable_final_arch_cap s p cap c \<Longrightarrow> cap_range cap \<subseteq> cap_range c proof (prove)
goal:
No subgoals!