theory Invariants_H

lemma untyped_incD':
  "\<lbrakk> m p = Some (CTE c n); isUntypedCap c;
     m p' = Some (CTE c' n'); isUntypedCap c'; untyped_inc' m \<rbrakk> \<Longrightarrow>
   (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and>
   (untypedRange c \<subset> untypedRange c' \<longrightarrow> (p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {})) \<and>
   (untypedRange c' \<subset> untypedRange c \<longrightarrow> (p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {})) \<and>
   (untypedRange c = untypedRange c' \<longrightarrow> (p' \<in> descendants_of' p m \<and> usableUntypedRange c = {}
   \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p'))" unfolding untyped_inc'_def apply (drule_tac x = p in spec) apply (drule_tac x = p' in spec) apply (elim allE impE) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE c n); isUntypedCap c; m p' = Some (CTE c' n'); isUntypedCap c'; untyped_inc' m\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE c n); isUntypedCap c; m p' = Some (CTE c' n'); isUntypedCap c'; \<forall>p p' c c' n n'. m p = Some (CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> m p' = Some (CTE c' n') \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p')\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE c n); isUntypedCap c; m p' = Some (CTE c' n'); isUntypedCap c'; \<forall>p' c c' n n'. m p = Some (CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> m p' = Some (CTE c' n') \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p')\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE c n); isUntypedCap c; m p' = Some (CTE c' n'); isUntypedCap c'; \<forall>c c' n n'. m p = Some (CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> m p' = Some (CTE c' n') \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p')\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m p = Some (CTE c n); isUntypedCap c; m p' = Some (CTE c' n'); isUntypedCap c'\<rbrakk> \<Longrightarrow> m p = Some (CTE ?c4 ?n6)
 2. \<lbrakk>m p = Some (CTE c n); isUntypedCap c; m p' = Some (CTE c' n'); isUntypedCap c'\<rbrakk> \<Longrightarrow> isUntypedCap ?c4
 3. \<lbrakk>m p = Some (CTE c n); isUntypedCap c; m p' = Some (CTE c' n'); isUntypedCap c'\<rbrakk> \<Longrightarrow> m p' = Some (CTE ?c'5 ?n'7)
 4. \<lbrakk>m p = Some (CTE c n); isUntypedCap c; m p' = Some (CTE c' n'); isUntypedCap c'\<rbrakk> \<Longrightarrow> isUntypedCap ?c'5
 5. \<lbrakk>m p = Some (CTE c n); isUntypedCap c; m p' = Some (CTE c' n'); isUntypedCap c'; (untypedRange ?c4 \<subseteq> untypedRange ?c'5 \<or> untypedRange ?c'5 \<subseteq> untypedRange ?c4 \<or> untypedRange ?c4 \<inter> untypedRange ?c'5 = {}) \<and> (untypedRange ?c4 \<subset> untypedRange ?c'5 \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange ?c4 \<inter> usableUntypedRange ?c'5 = {}) \<and> (untypedRange ?c'5 \<subset> untypedRange ?c4 \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange ?c'5 \<inter> usableUntypedRange ?c4 = {}) \<and> (untypedRange ?c4 = untypedRange ?c'5 \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange ?c4 = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange ?c'5 = {} \<or> p = p')\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal:
No subgoals!