theory ArchVSpaceEntries_AI

lemma pde_range_interD:
 "pde_range pde p \<inter> pde_range pde' p' \<noteq> {}
  \<Longrightarrow> pde \<noteq> InvalidPDE \<and> pde' \<noteq> InvalidPDE
      \<and> p && ~~ mask 4 = p' && ~~ mask 4" apply (drule int_not_emptyD) apply (case_tac pde,simp_all split:if_splits) apply (case_tac pde',simp_all split:if_splits) apply (case_tac pde',simp_all split:if_splits) apply clarsimp apply (case_tac pde', simp_all split:if_splits) apply (case_tac pde', simp_all split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pde_range pde p \<inter> pde_range pde' p' \<noteq> {} \<Longrightarrow> pde \<noteq> InvalidPDE \<and> pde' \<noteq> InvalidPDE \<and> p && ~~ mask 4 = p' && ~~ mask 4 proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> pde_range pde p \<and> x \<in> pde_range pde' p' \<Longrightarrow> pde \<noteq> InvalidPDE \<and> pde' \<noteq> InvalidPDE \<and> p && ~~ mask 4 = p' && ~~ mask 4 proof (prove)
goal (4 subgoals):
 1. \<And>x21 x22 x23. \<lbrakk>p \<in> pde_range pde' p'; pde = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> pde' \<noteq> InvalidPDE \<and> p && ~~ mask 4 = p' && ~~ mask 4
 2. \<And>x31 x32 x33 x34. \<lbrakk>p \<in> pde_range pde' p'; pde = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> pde' \<noteq> InvalidPDE \<and> p && ~~ mask 4 = p' && ~~ mask 4
 3. \<And>x41 x42 x43. \<lbrakk>pde = SuperSectionPDE x41 x42 x43; is_aligned p 4; \<exists>x. x && ~~ mask 4 = p \<and> x \<in> pde_range pde' p'\<rbrakk> \<Longrightarrow> pde' \<noteq> InvalidPDE \<and> p = p' && ~~ mask 4
 4. \<And>x41 x42 x43. \<lbrakk>pde = SuperSectionPDE x41 x42 x43; \<not> is_aligned p 4; p \<in> pde_range pde' p'\<rbrakk> \<Longrightarrow> pde' \<noteq> InvalidPDE \<and> p && ~~ mask 4 = p' && ~~ mask 4 proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 x34. \<lbrakk>p \<in> pde_range pde' p'; pde = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> pde' \<noteq> InvalidPDE \<and> p && ~~ mask 4 = p' && ~~ mask 4
 2. \<And>x41 x42 x43. \<lbrakk>pde = SuperSectionPDE x41 x42 x43; is_aligned p 4; \<exists>x. x && ~~ mask 4 = p \<and> x \<in> pde_range pde' p'\<rbrakk> \<Longrightarrow> pde' \<noteq> InvalidPDE \<and> p = p' && ~~ mask 4
 3. \<And>x41 x42 x43. \<lbrakk>pde = SuperSectionPDE x41 x42 x43; \<not> is_aligned p 4; p \<in> pde_range pde' p'\<rbrakk> \<Longrightarrow> pde' \<noteq> InvalidPDE \<and> p && ~~ mask 4 = p' && ~~ mask 4 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43. \<lbrakk>pde = SuperSectionPDE x41 x42 x43; is_aligned p 4; \<exists>x. x && ~~ mask 4 = p \<and> x \<in> pde_range pde' p'\<rbrakk> \<Longrightarrow> pde' \<noteq> InvalidPDE \<and> p = p' && ~~ mask 4
 2. \<And>x41 x42 x43. \<lbrakk>pde = SuperSectionPDE x41 x42 x43; \<not> is_aligned p 4; p \<in> pde_range pde' p'\<rbrakk> \<Longrightarrow> pde' \<noteq> InvalidPDE \<and> p && ~~ mask 4 = p' && ~~ mask 4 proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x. \<lbrakk>pde = SuperSectionPDE x41 x42 x43; x \<in> pde_range pde' p'; p = x && ~~ mask 4\<rbrakk> \<Longrightarrow> pde' \<noteq> InvalidPDE \<and> x && ~~ mask 4 = p' && ~~ mask 4
 2. \<And>x41 x42 x43. \<lbrakk>pde = SuperSectionPDE x41 x42 x43; \<not> is_aligned p 4; p \<in> pde_range pde' p'\<rbrakk> \<Longrightarrow> pde' \<noteq> InvalidPDE \<and> p && ~~ mask 4 = p' && ~~ mask 4 proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43. \<lbrakk>pde = SuperSectionPDE x41 x42 x43; \<not> is_aligned p 4; p \<in> pde_range pde' p'\<rbrakk> \<Longrightarrow> pde' \<noteq> InvalidPDE \<and> p && ~~ mask 4 = p' && ~~ mask 4 proof (prove)
goal:
No subgoals!