theory Detype_AI

lemma zombies_final_detype[detype_invs_lemmas]: "zombies_final (detype (untyped_range cap) s)" apply (insert zombies_final) apply (simp add: zombies_final_def final_cap_at_eq) apply (elim allEI) apply (rule impI, erule conjE, drule(1) mp) apply (elim exEI conjE conjI allEI) apply (rule impI, elim conjE) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zombies_final (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. zombies_final s \<Longrightarrow> zombies_final (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<forall>a b. cte_wp_at is_zombie (a, b) s \<longrightarrow> (\<exists>cp. cte_wp_at (\<lambda>cap. cap = cp) (a, b) s \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>aa ba. cte_wp_at (\<lambda>_. True) (aa, ba) s \<and> (aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> cte_wp_at (\<lambda>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {}) (aa, ba) s)) \<Longrightarrow> \<forall>a b. cte_wp_at is_zombie (a, b) s \<and> a \<notin> untyped_range cap \<longrightarrow> (\<exists>cp. cte_wp_at (\<lambda>cap. cap = cp) (a, b) s \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>aa ba. cte_wp_at (\<lambda>_. True) (aa, ba) s \<and> aa \<notin> untyped_range cap \<and> (aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> cte_wp_at (\<lambda>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {}) (aa, ba) s)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. cte_wp_at is_zombie (a, b) s \<longrightarrow> (\<exists>cp. cte_wp_at (\<lambda>cap. cap = cp) (a, b) s \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>aa ba. cte_wp_at (\<lambda>_. True) (aa, ba) s \<and> (aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> cte_wp_at (\<lambda>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {}) (aa, ba) s)) \<Longrightarrow> cte_wp_at is_zombie (a, b) s \<and> a \<notin> untyped_range cap \<longrightarrow> (\<exists>cp. cte_wp_at (\<lambda>cap. cap = cp) (a, b) s \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>aa ba. cte_wp_at (\<lambda>_. True) (aa, ba) s \<and> aa \<notin> untyped_range cap \<and> (aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> cte_wp_at (\<lambda>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {}) (aa, ba) s)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at is_zombie (a, b) s; a \<notin> untyped_range cap; \<exists>cp. cte_wp_at (\<lambda>cap. cap = cp) (a, b) s \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>aa ba. cte_wp_at (\<lambda>_. True) (aa, ba) s \<and> (aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> cte_wp_at (\<lambda>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {}) (aa, ba) s)\<rbrakk> \<Longrightarrow> \<exists>cp. cte_wp_at (\<lambda>cap. cap = cp) (a, b) s \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>aa ba. cte_wp_at (\<lambda>_. True) (aa, ba) s \<and> aa \<notin> untyped_range cap \<and> (aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> cte_wp_at (\<lambda>cap. gen_obj_refs cp \<inter> gen_obj_refs cap = {}) (aa, ba) s) proof (prove)
goal (1 subgoal):
 1. \<And>a b x aa ba. \<lbrakk>cte_wp_at is_zombie (a, b) s; a \<notin> untyped_range cap; cte_wp_at (\<lambda>_. True) (aa, ba) s \<and> (aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> cte_wp_at (\<lambda>cap. gen_obj_refs x \<inter> gen_obj_refs cap = {}) (aa, ba) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (aa, ba) s \<and> aa \<notin> untyped_range cap \<and> (aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> cte_wp_at (\<lambda>cap. gen_obj_refs x \<inter> gen_obj_refs cap = {}) (aa, ba) s proof (prove)
goal (1 subgoal):
 1. \<And>a b x aa ba. \<lbrakk>cte_wp_at is_zombie (a, b) s; a \<notin> untyped_range cap; cte_wp_at (\<lambda>_. True) (aa, ba) s \<and> (aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> cte_wp_at (\<lambda>cap. gen_obj_refs x \<inter> gen_obj_refs cap = {}) (aa, ba) s; cte_wp_at (\<lambda>_. True) (aa, ba) s; aa \<notin> untyped_range cap; aa = a \<longrightarrow> ba \<noteq> b\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. gen_obj_refs x \<inter> gen_obj_refs cap = {}) (aa, ba) s proof (prove)
goal:
No subgoals!