theory Invariants_H

lemma ps_clear_def2:
  "p \<le> p + 1 \<Longrightarrow> ps_clear p n s = ({p + 1 .. p + (1 << n) - 1} \<inter> dom (ksPSpace s) = {})" apply (simp add: ps_clear_def) apply safe apply (drule_tac a=x in equals0D) apply clarsimp apply (drule mp, simp) apply (erule disjE) apply simp apply clarsimp apply (drule_tac a=x in equals0D) apply clarsimp apply (case_tac "p + 1 \<le> x") apply clarsimp apply (simp add: linorder_not_le) apply (drule plus_one_helper, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<le> p + 1 \<Longrightarrow> ps_clear p n s = ({p + 1..p + (1 << n) - 1} \<inter> dom (ksPSpace s) = {}) proof (prove)
goal (1 subgoal):
 1. p \<le> p + 1 \<Longrightarrow> (({p..p + 2 ^ n - 1} - {p}) \<inter> dom (ksPSpace s) = {}) = ({p + 1..p + 2 ^ n - 1} \<inter> dom (ksPSpace s) = {}) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>p \<le> p + 1; ({p..p + 2 ^ n - 1} - {p}) \<inter> dom (ksPSpace s) = {}; x \<in> {p + 1..p + 2 ^ n - 1}; ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> x \<in> {}
 2. \<And>x y. \<lbrakk>p \<le> p + 1; {p + 1..p + 2 ^ n - 1} \<inter> dom (ksPSpace s) = {}; x \<in> {p..p + 2 ^ n - 1}; x \<notin> {}; x \<notin> {}; ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> x = p proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>p \<le> p + 1; x \<in> {p + 1..p + 2 ^ n - 1}; ksPSpace s x = Some y; x \<notin> ({p..p + 2 ^ n - 1} - {p}) \<inter> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> x \<in> {}
 2. \<And>x y. \<lbrakk>p \<le> p + 1; {p + 1..p + 2 ^ n - 1} \<inter> dom (ksPSpace s) = {}; x \<in> {p..p + 2 ^ n - 1}; x \<notin> {}; x \<notin> {}; ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> x = p proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>p \<le> p + 1; ksPSpace s x = Some y; p \<le> x \<longrightarrow> x = p \<or> x \<notin> dom (ksPSpace s); p + 1 \<le> x; x \<le> p + 2 ^ n - 1\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>p \<le> p + 1; {p + 1..p + 2 ^ n - 1} \<inter> dom (ksPSpace s) = {}; x \<in> {p..p + 2 ^ n - 1}; x \<notin> {}; x \<notin> {}; ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> x = p proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>p \<le> p + 1; ksPSpace s x = Some y; p + 1 \<le> x; x \<le> p + 2 ^ n - 1; x = p \<or> x \<notin> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>p \<le> p + 1; {p + 1..p + 2 ^ n - 1} \<inter> dom (ksPSpace s) = {}; x \<in> {p..p + 2 ^ n - 1}; x \<notin> {}; x \<notin> {}; ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> x = p proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>p \<le> p + 1; ksPSpace s x = Some y; p + 1 \<le> x; x \<le> p + 2 ^ n - 1; x = p\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>p \<le> p + 1; ksPSpace s x = Some y; p + 1 \<le> x; x \<le> p + 2 ^ n - 1; x \<notin> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> False
 3. \<And>x y. \<lbrakk>p \<le> p + 1; {p + 1..p + 2 ^ n - 1} \<inter> dom (ksPSpace s) = {}; x \<in> {p..p + 2 ^ n - 1}; x \<notin> {}; x \<notin> {}; ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> x = p proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>p \<le> p + 1; ksPSpace s x = Some y; p + 1 \<le> x; x \<le> p + 2 ^ n - 1; x \<notin> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>p \<le> p + 1; {p + 1..p + 2 ^ n - 1} \<inter> dom (ksPSpace s) = {}; x \<in> {p..p + 2 ^ n - 1}; x \<notin> {}; x \<notin> {}; ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> x = p proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>p \<le> p + 1; {p + 1..p + 2 ^ n - 1} \<inter> dom (ksPSpace s) = {}; x \<in> {p..p + 2 ^ n - 1}; x \<notin> {}; x \<notin> {}; ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> x = p proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>p \<le> p + 1; x \<in> {p..p + 2 ^ n - 1}; x \<notin> {}; x \<notin> {}; ksPSpace s x = Some y; x \<notin> {p + 1..p + 2 ^ n - 1} \<inter> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> x = p proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>p \<le> p + 1; ksPSpace s x = Some y; p + 1 \<le> x \<longrightarrow> x \<notin> dom (ksPSpace s); p \<le> x; x \<le> p + 2 ^ n - 1\<rbrakk> \<Longrightarrow> x = p proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>p \<le> p + 1; ksPSpace s x = Some y; p + 1 \<le> x \<longrightarrow> x \<notin> dom (ksPSpace s); p \<le> x; x \<le> p + 2 ^ n - 1; p + 1 \<le> x\<rbrakk> \<Longrightarrow> x = p
 2. \<And>x y. \<lbrakk>p \<le> p + 1; ksPSpace s x = Some y; p + 1 \<le> x \<longrightarrow> x \<notin> dom (ksPSpace s); p \<le> x; x \<le> p + 2 ^ n - 1; \<not> p + 1 \<le> x\<rbrakk> \<Longrightarrow> x = p proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>p \<le> p + 1; ksPSpace s x = Some y; p + 1 \<le> x \<longrightarrow> x \<notin> dom (ksPSpace s); p \<le> x; x \<le> p + 2 ^ n - 1; \<not> p + 1 \<le> x\<rbrakk> \<Longrightarrow> x = p proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>p \<le> p + 1; ksPSpace s x = Some y; p \<le> x; x \<le> p + 2 ^ n - 1; x < p + 1\<rbrakk> \<Longrightarrow> x = p proof (prove)
goal:
No subgoals!