theory Invariants_AI

lemma valid_untyped_T:
  "valid_untyped c =
  (\<lambda>s. \<forall>T p. \<not>typ_at T p s \<or> typ_range p T \<inter> untyped_range c = {} \<or>
         (typ_range p T \<subseteq> untyped_range c \<and> typ_range p T \<inter> usable_untyped_range c = {}))" apply (simp add: valid_untyped_def obj_range_T obj_at_def) apply (rule ext) apply (rule iffI) apply clarsimp apply (elim allE) apply (erule(1) impE)+ apply fastforce apply clarsimp apply (elim allE disjE) apply (erule(1) impE) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_untyped c = (\<lambda>s. \<forall>T p. \<not> typ_at T p s \<or> typ_range p T \<inter> untyped_range c = {} \<or> typ_range p T \<subseteq> untyped_range c \<and> typ_range p T \<inter> usable_untyped_range c = {}) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<forall>p obj. kheap s p = Some obj \<longrightarrow> typ_range p (a_type obj) \<inter> untyped_range c \<noteq> {} \<longrightarrow> typ_range p (a_type obj) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range p (a_type obj) = {}) = (\<lambda>s. \<forall>T p. (\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> T) \<or> typ_range p T \<inter> untyped_range c = {} \<or> typ_range p T \<subseteq> untyped_range c \<and> typ_range p T \<inter> usable_untyped_range c = {}) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>p obj. kheap s p = Some obj \<longrightarrow> typ_range p (a_type obj) \<inter> untyped_range c \<noteq> {} \<longrightarrow> typ_range p (a_type obj) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range p (a_type obj) = {}) = (\<forall>T p. (\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> T) \<or> typ_range p T \<inter> untyped_range c = {} \<or> typ_range p T \<subseteq> untyped_range c \<and> typ_range p T \<inter> usable_untyped_range c = {}) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<forall>p obj. kheap s p = Some obj \<longrightarrow> typ_range p (a_type obj) \<inter> untyped_range c \<noteq> {} \<longrightarrow> typ_range p (a_type obj) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range p (a_type obj) = {} \<Longrightarrow> \<forall>T p. (\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> T) \<or> typ_range p T \<inter> untyped_range c = {} \<or> typ_range p T \<subseteq> untyped_range c \<and> typ_range p T \<inter> usable_untyped_range c = {}
 2. \<And>s. \<forall>T p. (\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> T) \<or> typ_range p T \<inter> untyped_range c = {} \<or> typ_range p T \<subseteq> untyped_range c \<and> typ_range p T \<inter> usable_untyped_range c = {} \<Longrightarrow> \<forall>p obj. kheap s p = Some obj \<longrightarrow> typ_range p (a_type obj) \<inter> untyped_range c \<noteq> {} \<longrightarrow> typ_range p (a_type obj) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range p (a_type obj) = {} proof (prove)
goal (2 subgoals):
 1. \<And>s p ko. \<lbrakk>\<forall>p obj. kheap s p = Some obj \<longrightarrow> typ_range p (a_type obj) \<inter> untyped_range c \<noteq> {} \<longrightarrow> typ_range p (a_type obj) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range p (a_type obj) = {}; typ_range p (a_type ko) \<inter> usable_untyped_range c \<noteq> {}; typ_range p (a_type ko) \<inter> untyped_range c \<noteq> {}; kheap s p = Some ko\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<forall>T p. (\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> T) \<or> typ_range p T \<inter> untyped_range c = {} \<or> typ_range p T \<subseteq> untyped_range c \<and> typ_range p T \<inter> usable_untyped_range c = {} \<Longrightarrow> \<forall>p obj. kheap s p = Some obj \<longrightarrow> typ_range p (a_type obj) \<inter> untyped_range c \<noteq> {} \<longrightarrow> typ_range p (a_type obj) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range p (a_type obj) = {} proof (prove)
goal (2 subgoals):
 1. \<And>s p ko. \<lbrakk>typ_range p (a_type ko) \<inter> usable_untyped_range c \<noteq> {}; typ_range p (a_type ko) \<inter> untyped_range c \<noteq> {}; kheap s p = Some ko; kheap s (?p22 s p ko) = Some (?obj23 s p ko) \<longrightarrow> typ_range (?p22 s p ko) (a_type (?obj23 s p ko)) \<inter> untyped_range c \<noteq> {} \<longrightarrow> typ_range (?p22 s p ko) (a_type (?obj23 s p ko)) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range (?p22 s p ko) (a_type (?obj23 s p ko)) = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<forall>T p. (\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> T) \<or> typ_range p T \<inter> untyped_range c = {} \<or> typ_range p T \<subseteq> untyped_range c \<and> typ_range p T \<inter> usable_untyped_range c = {} \<Longrightarrow> \<forall>p obj. kheap s p = Some obj \<longrightarrow> typ_range p (a_type obj) \<inter> untyped_range c \<noteq> {} \<longrightarrow> typ_range p (a_type obj) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range p (a_type obj) = {} proof (prove)
goal (2 subgoals):
 1. \<And>s p ko. \<lbrakk>typ_range p (a_type ko) \<inter> usable_untyped_range c \<noteq> {}; typ_range p (a_type ko) \<inter> untyped_range c \<noteq> {}; kheap s p = Some ko; typ_range p (a_type ko) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range p (a_type ko) = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<forall>T p. (\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> T) \<or> typ_range p T \<inter> untyped_range c = {} \<or> typ_range p T \<subseteq> untyped_range c \<and> typ_range p T \<inter> usable_untyped_range c = {} \<Longrightarrow> \<forall>p obj. kheap s p = Some obj \<longrightarrow> typ_range p (a_type obj) \<inter> untyped_range c \<noteq> {} \<longrightarrow> typ_range p (a_type obj) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range p (a_type obj) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>T p. (\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> T) \<or> typ_range p T \<inter> untyped_range c = {} \<or> typ_range p T \<subseteq> untyped_range c \<and> typ_range p T \<inter> usable_untyped_range c = {} \<Longrightarrow> \<forall>p obj. kheap s p = Some obj \<longrightarrow> typ_range p (a_type obj) \<inter> untyped_range c \<noteq> {} \<longrightarrow> typ_range p (a_type obj) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range p (a_type obj) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s p obj. \<lbrakk>\<forall>T p. (\<forall>ko. kheap s p = Some ko \<longrightarrow> a_type ko \<noteq> T) \<or> typ_range p T \<inter> untyped_range c = {} \<or> typ_range p T \<subseteq> untyped_range c \<and> typ_range p T \<inter> usable_untyped_range c = {}; kheap s p = Some obj; typ_range p (a_type obj) \<inter> untyped_range c \<noteq> {}\<rbrakk> \<Longrightarrow> typ_range p (a_type obj) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range p (a_type obj) = {} proof (prove)
goal (3 subgoals):
 1. \<And>s p obj. \<lbrakk>kheap s p = Some obj; typ_range p (a_type obj) \<inter> untyped_range c \<noteq> {}; kheap s (?p52 s p obj) = Some (?ko55 s p obj) \<longrightarrow> a_type (?ko55 s p obj) \<noteq> ?T51 s p obj\<rbrakk> \<Longrightarrow> typ_range p (a_type obj) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range p (a_type obj) = {}
 2. \<And>s p obj. \<lbrakk>kheap s p = Some obj; typ_range p (a_type obj) \<inter> untyped_range c \<noteq> {}; typ_range (?p52 s p obj) (?T51 s p obj) \<inter> untyped_range c = {}\<rbrakk> \<Longrightarrow> typ_range p (a_type obj) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range p (a_type obj) = {}
 3. \<And>s p obj. \<lbrakk>kheap s p = Some obj; typ_range p (a_type obj) \<inter> untyped_range c \<noteq> {}; typ_range (?p52 s p obj) (?T51 s p obj) \<subseteq> untyped_range c \<and> typ_range (?p52 s p obj) (?T51 s p obj) \<inter> usable_untyped_range c = {}\<rbrakk> \<Longrightarrow> typ_range p (a_type obj) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range p (a_type obj) = {} proof (prove)
goal (3 subgoals):
 1. \<And>s p obj. \<lbrakk>kheap s p = Some obj; typ_range p (a_type obj) \<inter> untyped_range c \<noteq> {}; a_type obj \<noteq> ?T51 s p obj\<rbrakk> \<Longrightarrow> typ_range p (a_type obj) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range p (a_type obj) = {}
 2. \<And>s p obj. \<lbrakk>kheap s p = Some obj; typ_range p (a_type obj) \<inter> untyped_range c \<noteq> {}; typ_range p (?T51 s p obj) \<inter> untyped_range c = {}\<rbrakk> \<Longrightarrow> typ_range p (a_type obj) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range p (a_type obj) = {}
 3. \<And>s p obj. \<lbrakk>kheap s p = Some obj; typ_range p (a_type obj) \<inter> untyped_range c \<noteq> {}; typ_range p (?T51 s p obj) \<subseteq> untyped_range c \<and> typ_range p (?T51 s p obj) \<inter> usable_untyped_range c = {}\<rbrakk> \<Longrightarrow> typ_range p (a_type obj) \<subseteq> untyped_range c \<and> usable_untyped_range c \<inter> typ_range p (a_type obj) = {} proof (prove)
goal:
No subgoals!