theory Detype_AI

lemma INV_9[detype_invs_lemmas]: "if_unsafe_then_cap (detype (untyped_range cap) s)" apply (insert ifunsafe) apply (simp add: if_unsafe_then_cap_def ex_cte_cap_wp_to_def) apply (erule allEI, rule impI) apply (erule allEI) apply (clarsimp del: exE) apply (erule exEI) apply clarsimp apply (frule(1) non_null_caps) apply (frule non_null_present [OF cte_wp_at_weakenE]) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. if_unsafe_then_cap (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. if_unsafe_then_cap s \<Longrightarrow> if_unsafe_then_cap (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>aa ba. cte_wp_at (\<lambda>c. appropriate_cte_cap cap c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (aa, ba) s) \<Longrightarrow> \<forall>a. a \<notin> untyped_range cap \<longrightarrow> (\<forall>b capa. caps_of_state s (a, b) = Some capa \<longrightarrow> capa \<noteq> NullCap \<longrightarrow> (\<exists>aa. (\<exists>ba. cte_wp_at (\<lambda>c. appropriate_cte_cap capa c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (aa, ba) s) \<and> aa \<notin> untyped_range cap)) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<forall>b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>aa ba. cte_wp_at (\<lambda>c. appropriate_cte_cap cap c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (aa, ba) s); a \<notin> untyped_range cap\<rbrakk> \<Longrightarrow> \<forall>b capa. caps_of_state s (a, b) = Some capa \<longrightarrow> capa \<noteq> NullCap \<longrightarrow> (\<exists>aa. (\<exists>ba. cte_wp_at (\<lambda>c. appropriate_cte_cap capa c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (aa, ba) s) \<and> aa \<notin> untyped_range cap) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<notin> untyped_range cap; \<forall>cap. caps_of_state s (a, b) = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>aa ba. cte_wp_at (\<lambda>c. appropriate_cte_cap cap c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (aa, ba) s)\<rbrakk> \<Longrightarrow> \<forall>capa. caps_of_state s (a, b) = Some capa \<longrightarrow> capa \<noteq> NullCap \<longrightarrow> (\<exists>aa. (\<exists>ba. cte_wp_at (\<lambda>c. appropriate_cte_cap capa c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (aa, ba) s) \<and> aa \<notin> untyped_range cap) proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>a \<notin> untyped_range cap; \<exists>aa ba. cte_wp_at (\<lambda>c. appropriate_cte_cap capa c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (aa, ba) s; caps_of_state s (a, b) = Some capa; capa \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>ba. cte_wp_at (\<lambda>c. appropriate_cte_cap capa c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (aa, ba) s) \<and> aa \<notin> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>a b capa x. \<lbrakk>a \<notin> untyped_range cap; caps_of_state s (a, b) = Some capa; capa \<noteq> NullCap; \<exists>ba. cte_wp_at (\<lambda>c. appropriate_cte_cap capa c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (x, ba) s\<rbrakk> \<Longrightarrow> (\<exists>ba. cte_wp_at (\<lambda>c. appropriate_cte_cap capa c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (x, ba) s) \<and> x \<notin> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>a b capa x ba. \<lbrakk>a \<notin> untyped_range cap; caps_of_state s (a, b) = Some capa; capa \<noteq> NullCap; cte_wp_at (\<lambda>c. appropriate_cte_cap capa c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (x, ba) s; x \<in> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b capa x ba. \<lbrakk>a \<notin> untyped_range cap; caps_of_state s (a, b) = Some capa; capa \<noteq> NullCap; cte_wp_at (\<lambda>c. appropriate_cte_cap capa c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (x, ba) s; x \<in> untyped_range cap; fst (a, b) \<notin> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b capa x ba c. \<lbrakk>a \<notin> untyped_range cap; caps_of_state s (a, b) = Some capa; capa \<noteq> NullCap; cte_wp_at (\<lambda>c. appropriate_cte_cap capa c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (x, ba) s; x \<in> untyped_range cap; fst (a, b) \<notin> untyped_range cap; appropriate_cte_cap capa c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> NullCap \<noteq> c
 2. \<And>a b capa x ba. \<lbrakk>a \<notin> untyped_range cap; caps_of_state s (a, b) = Some capa; capa \<noteq> NullCap; cte_wp_at (\<lambda>c. appropriate_cte_cap capa c \<and> (a, b) \<in> cte_refs c (interrupt_irq_node s)) (x, ba) s; x \<in> untyped_range cap; fst (a, b) \<notin> untyped_range cap; fst (x, ba) \<notin> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!