theory CSpace_AI

lemma untyped_inc_update_free_index:
  "\<lbrakk>m src = Some cap; m' = m (src \<mapsto> (max_free_index_update cap));
    untyped_inc c m\<rbrakk> \<Longrightarrow>
   untyped_inc c m'" apply (unfold untyped_inc_def) apply (intro allI impI) apply (drule_tac x = p in spec) apply (drule_tac x = p' in spec) apply (case_tac "p = src") apply (simp del:fun_upd_apply split_paired_All) apply (clarsimp split:if_splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some cap; m' = m(src \<mapsto> max_free_index_update cap); untyped_inc c m\<rbrakk> \<Longrightarrow> untyped_inc c m' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some cap; m' = m(src \<mapsto> max_free_index_update cap); \<forall>p p' ca c'. m p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> m p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' c \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p c \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p c \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' c \<and> usable_untyped_range c' = {} \<or> p = p')\<rbrakk> \<Longrightarrow> \<forall>p p' ca c'. m' p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> m' p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' c \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p c \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p c \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' c \<and> usable_untyped_range c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' ca c'. \<lbrakk>m src = Some cap; m' = m(src \<mapsto> max_free_index_update cap); \<forall>p p' ca c'. m p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> m p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' c \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p c \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p c \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' c \<and> usable_untyped_range c' = {} \<or> p = p'); m' p = Some ca; is_untyped_cap ca; m' p' = Some c'; is_untyped_cap c'\<rbrakk> \<Longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' c \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p c \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p c \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' c \<and> usable_untyped_range c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' ca c'. \<lbrakk>m src = Some cap; m' = m(src \<mapsto> max_free_index_update cap); m' p = Some ca; is_untyped_cap ca; m' p' = Some c'; is_untyped_cap c'; \<forall>p' ca c'. m p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> m p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' c \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p c \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p c \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' c \<and> usable_untyped_range c' = {} \<or> p = p')\<rbrakk> \<Longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' c \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p c \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p c \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' c \<and> usable_untyped_range c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' ca c'. \<lbrakk>m src = Some cap; m' = m(src \<mapsto> max_free_index_update cap); m' p = Some ca; is_untyped_cap ca; m' p' = Some c'; is_untyped_cap c'; \<forall>ca c'. m p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> m p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' c \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p c \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p c \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' c \<and> usable_untyped_range c' = {} \<or> p = p')\<rbrakk> \<Longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' c \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p c \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p c \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' c \<and> usable_untyped_range c' = {} \<or> p = p') proof (prove)
goal (2 subgoals):
 1. \<And>p p' ca c'. \<lbrakk>m src = Some cap; m' = m(src \<mapsto> max_free_index_update cap); m' p = Some ca; is_untyped_cap ca; m' p' = Some c'; is_untyped_cap c'; \<forall>ca c'. m p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> m p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' c \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p c \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p c \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' c \<and> usable_untyped_range c' = {} \<or> p = p'); p = src\<rbrakk> \<Longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' c \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p c \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p c \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' c \<and> usable_untyped_range c' = {} \<or> p = p')
 2. \<And>p p' ca c'. \<lbrakk>m src = Some cap; m' = m(src \<mapsto> max_free_index_update cap); m' p = Some ca; is_untyped_cap ca; m' p' = Some c'; is_untyped_cap c'; \<forall>ca c'. m p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> m p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' c \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p c \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p c \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' c \<and> usable_untyped_range c' = {} \<or> p = p'); p \<noteq> src\<rbrakk> \<Longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' c \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p c \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p c \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' c \<and> usable_untyped_range c' = {} \<or> p = p') proof (prove)
goal (2 subgoals):
 1. \<And>p p' ca c'. \<lbrakk>m src = Some cap; m' = m(src \<mapsto> max_free_index_update cap); (m(src \<mapsto> max_free_index_update cap)) src = Some ca; is_untyped_cap ca; (m(src \<mapsto> max_free_index_update cap)) p' = Some c'; is_untyped_cap c'; is_untyped_cap cap \<longrightarrow> (\<forall>c'. m p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range cap \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range cap \<or> untyped_range cap \<inter> untyped_range c' = {}) \<and> (untyped_range cap \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p' c \<and> untyped_range cap \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range cap \<longrightarrow> p' \<in> descendants_of src c \<and> untyped_range c' \<inter> usable_untyped_range cap = {}) \<and> (untyped_range cap = untyped_range c' \<longrightarrow> p' \<in> descendants_of src c \<and> usable_untyped_range cap = {} \<or> src \<in> descendants_of p' c \<and> usable_untyped_range c' = {} \<or> src = p')); p = src\<rbrakk> \<Longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> src \<in> descendants_of p' c \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of src c \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of src c \<and> usable_untyped_range ca = {} \<or> src \<in> descendants_of p' c \<and> usable_untyped_range c' = {} \<or> src = p')
 2. \<And>p p' ca c'. \<lbrakk>m src = Some cap; m' = m(src \<mapsto> max_free_index_update cap); m' p = Some ca; is_untyped_cap ca; m' p' = Some c'; is_untyped_cap c'; \<forall>ca c'. m p = Some ca \<longrightarrow> is_untyped_cap ca \<longrightarrow> m p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' c \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p c \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p c \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' c \<and> usable_untyped_range c' = {} \<or> p = p'); p \<noteq> src\<rbrakk> \<Longrightarrow> (untyped_range ca \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range ca \<or> untyped_range ca \<inter> untyped_range c' = {}) \<and> (untyped_range ca \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' c \<and> untyped_range ca \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range ca \<longrightarrow> p' \<in> descendants_of p c \<and> untyped_range c' \<inter> usable_untyped_range ca = {}) \<and> (untyped_range ca = untyped_range c' \<longrightarrow> p' \<in> descendants_of p c \<and> usable_untyped_range ca = {} \<or> p \<in> descendants_of p' c \<and> usable_untyped_range c' = {} \<or> p = p') proof (prove)
goal:
No subgoals!