theory Example_Valid_StateH

lemma pspace_distinct'_split:
  notes less_1_simp[simp del] shows
  "(\<forall>(y, ko) \<in> graph_of (ksPSpace ks). (x \<le> y \<or> y + (1 << objBitsKO ko) - 1 < x)
        \<and> y \<le> y + (1 << objBitsKO ko) - 1)
    \<Longrightarrow> pspace_distinct' (ks \<lparr>ksPSpace := restrict_map (ksPSpace ks) {..< x}\<rparr>)
    \<Longrightarrow> pspace_distinct' (ks \<lparr>ksPSpace := restrict_map (ksPSpace ks) {x ..}\<rparr>)
    \<Longrightarrow> pspace_distinct' ks" apply (clarsimp simp: pspace_distinct'_def) apply (drule bspec, erule graph_ofI, clarsimp) apply (simp add: Ball_def) apply (drule_tac x=xa in spec)+ apply (erule disjE) apply (simp add: domI) apply (thin_tac "P \<longrightarrow> Q" for P Q) apply (simp add: ps_clear_def) apply (erule trans[rotated]) apply auto[1] apply (clarsimp simp add: domI) apply (drule mp, erule(1) order_le_less_trans) apply (thin_tac "P \<longrightarrow> Q" for P Q) apply (simp add: ps_clear_def) apply (erule trans[rotated]) apply auto[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>(y, ko)\<in>graph_of (ksPSpace ks). (x \<le> y \<or> y + (1 << objBitsKO ko) - 1 < x) \<and> y \<le> y + (1 << objBitsKO ko) - 1; pspace_distinct' (ks\<lparr>ksPSpace := ksPSpace ks |` {..<x}\<rparr>); pspace_distinct' (ks\<lparr>ksPSpace := ksPSpace ks |` {x..}\<rparr>)\<rbrakk> \<Longrightarrow> pspace_distinct' ks proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>\<forall>xa\<in>graph_of (ksPSpace ks). case xa of (y, ko) \<Rightarrow> (x \<le> y \<or> y + 2 ^ objBitsKO ko - 1 < x) \<and> y \<le> y + 2 ^ objBitsKO ko - 1; \<forall>xa\<in>dom (ksPSpace ks) \<inter> {..<x}. ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {..<x}\<rparr>); \<forall>xa\<in>dom (ksPSpace ks) \<inter> {x..}. ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {x..}\<rparr>); ksPSpace ks xa = Some y\<rbrakk> \<Longrightarrow> ps_clear xa (objBitsKO y) ks proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>\<forall>xa\<in>dom (ksPSpace ks) \<inter> {..<x}. ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {..<x}\<rparr>); \<forall>xa\<in>dom (ksPSpace ks) \<inter> {x..}. ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {x..}\<rparr>); ksPSpace ks xa = Some y; x \<le> xa \<or> xa + 2 ^ objBitsKO y - 1 < x; xa \<le> xa + 2 ^ objBitsKO y - 1\<rbrakk> \<Longrightarrow> ps_clear xa (objBitsKO y) ks proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>\<forall>xa. xa \<in> dom (ksPSpace ks) \<and> xa < x \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {..<x}\<rparr>); \<forall>xa. xa \<in> dom (ksPSpace ks) \<and> x \<le> xa \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {x..}\<rparr>); ksPSpace ks xa = Some y; x \<le> xa \<or> xa + 2 ^ objBitsKO y - 1 < x; xa \<le> xa + 2 ^ objBitsKO y - 1\<rbrakk> \<Longrightarrow> ps_clear xa (objBitsKO y) ks proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>ksPSpace ks xa = Some y; x \<le> xa \<or> xa + 2 ^ objBitsKO y - 1 < x; xa \<le> xa + 2 ^ objBitsKO y - 1; xa \<in> dom (ksPSpace ks) \<and> xa < x \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {..<x}\<rparr>); xa \<in> dom (ksPSpace ks) \<and> x \<le> xa \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {x..}\<rparr>)\<rbrakk> \<Longrightarrow> ps_clear xa (objBitsKO y) ks proof (prove)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>ksPSpace ks xa = Some y; xa \<le> xa + 2 ^ objBitsKO y - 1; xa \<in> dom (ksPSpace ks) \<and> xa < x \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {..<x}\<rparr>); xa \<in> dom (ksPSpace ks) \<and> x \<le> xa \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {x..}\<rparr>); x \<le> xa\<rbrakk> \<Longrightarrow> ps_clear xa (objBitsKO y) ks
 2. \<And>xa y. \<lbrakk>ksPSpace ks xa = Some y; xa \<le> xa + 2 ^ objBitsKO y - 1; xa \<in> dom (ksPSpace ks) \<and> xa < x \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {..<x}\<rparr>); xa \<in> dom (ksPSpace ks) \<and> x \<le> xa \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {x..}\<rparr>); xa + 2 ^ objBitsKO y - 1 < x\<rbrakk> \<Longrightarrow> ps_clear xa (objBitsKO y) ks proof (prove)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>ksPSpace ks xa = Some y; xa \<le> xa + 2 ^ objBitsKO y - 1; xa < x \<longrightarrow> ps_clear xa (objBitsKO y) (ks\<lparr>ksPSpace := ksPSpace ks |` {..<x}\<rparr>); ps_clear xa (objBitsKO y) (ks\<lparr>ksPSpace := ksPSpace ks |` {x..}\<rparr>); x \<le> xa\<rbrakk> \<Longrightarrow> ps_clear xa (objBitsKO y) ks
 2. \<And>xa y. \<lbrakk>ksPSpace ks xa = Some y; xa \<le> xa + 2 ^ objBitsKO y - 1; xa \<in> dom (ksPSpace ks) \<and> xa < x \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {..<x}\<rparr>); xa \<in> dom (ksPSpace ks) \<and> x \<le> xa \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {x..}\<rparr>); xa + 2 ^ objBitsKO y - 1 < x\<rbrakk> \<Longrightarrow> ps_clear xa (objBitsKO y) ks proof (prove)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>ksPSpace ks xa = Some y; xa \<le> xa + 2 ^ objBitsKO y - 1; ps_clear xa (objBitsKO y) (ks\<lparr>ksPSpace := ksPSpace ks |` {x..}\<rparr>); x \<le> xa\<rbrakk> \<Longrightarrow> ps_clear xa (objBitsKO y) ks
 2. \<And>xa y. \<lbrakk>ksPSpace ks xa = Some y; xa \<le> xa + 2 ^ objBitsKO y - 1; xa \<in> dom (ksPSpace ks) \<and> xa < x \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {..<x}\<rparr>); xa \<in> dom (ksPSpace ks) \<and> x \<le> xa \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {x..}\<rparr>); xa + 2 ^ objBitsKO y - 1 < x\<rbrakk> \<Longrightarrow> ps_clear xa (objBitsKO y) ks proof (prove)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>ksPSpace ks xa = Some y; xa \<le> xa + 2 ^ objBitsKO y - 1; ({xa..xa + 2 ^ objBitsKO y - 1} - {xa}) \<inter> (dom (ksPSpace ks) \<inter> {x..}) = {}; x \<le> xa\<rbrakk> \<Longrightarrow> ({xa..xa + 2 ^ objBitsKO y - 1} - {xa}) \<inter> dom (ksPSpace ks) = {}
 2. \<And>xa y. \<lbrakk>ksPSpace ks xa = Some y; xa \<le> xa + 2 ^ objBitsKO y - 1; xa \<in> dom (ksPSpace ks) \<and> xa < x \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {..<x}\<rparr>); xa \<in> dom (ksPSpace ks) \<and> x \<le> xa \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {x..}\<rparr>); xa + 2 ^ objBitsKO y - 1 < x\<rbrakk> \<Longrightarrow> ps_clear xa (objBitsKO y) ks proof (prove)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>ksPSpace ks xa = Some y; xa \<le> xa + 2 ^ objBitsKO y - 1; x \<le> xa\<rbrakk> \<Longrightarrow> ({xa..xa + 2 ^ objBitsKO y - 1} - {xa}) \<inter> dom (ksPSpace ks) = ({xa..xa + 2 ^ objBitsKO y - 1} - {xa}) \<inter> (dom (ksPSpace ks) \<inter> {x..})
 2. \<And>xa y. \<lbrakk>ksPSpace ks xa = Some y; xa \<le> xa + 2 ^ objBitsKO y - 1; xa \<in> dom (ksPSpace ks) \<and> xa < x \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {..<x}\<rparr>); xa \<in> dom (ksPSpace ks) \<and> x \<le> xa \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {x..}\<rparr>); xa + 2 ^ objBitsKO y - 1 < x\<rbrakk> \<Longrightarrow> ps_clear xa (objBitsKO y) ks proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>ksPSpace ks xa = Some y; xa \<le> xa + 2 ^ objBitsKO y - 1; xa \<in> dom (ksPSpace ks) \<and> xa < x \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {..<x}\<rparr>); xa \<in> dom (ksPSpace ks) \<and> x \<le> xa \<longrightarrow> ps_clear xa (objBitsKO (the (ksPSpace ks xa))) (ks\<lparr>ksPSpace := ksPSpace ks |` {x..}\<rparr>); xa + 2 ^ objBitsKO y - 1 < x\<rbrakk> \<Longrightarrow> ps_clear xa (objBitsKO y) ks proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>ksPSpace ks xa = Some y; xa \<le> xa + 2 ^ objBitsKO y - 1; xa < x \<longrightarrow> ps_clear xa (objBitsKO y) (ks\<lparr>ksPSpace := ksPSpace ks |` {..<x}\<rparr>); x \<le> xa \<longrightarrow> ps_clear xa (objBitsKO y) (ks\<lparr>ksPSpace := ksPSpace ks |` {x..}\<rparr>); xa + 2 ^ objBitsKO y - 1 < x\<rbrakk> \<Longrightarrow> ps_clear xa (objBitsKO y) ks proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>ksPSpace ks xa = Some y; xa \<le> xa + 2 ^ objBitsKO y - 1; x \<le> xa \<longrightarrow> ps_clear xa (objBitsKO y) (ks\<lparr>ksPSpace := ksPSpace ks |` {x..}\<rparr>); xa + 2 ^ objBitsKO y - 1 < x; ps_clear xa (objBitsKO y) (ks\<lparr>ksPSpace := ksPSpace ks |` {..<x}\<rparr>)\<rbrakk> \<Longrightarrow> ps_clear xa (objBitsKO y) ks proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>ksPSpace ks xa = Some y; xa \<le> xa + 2 ^ objBitsKO y - 1; xa + 2 ^ objBitsKO y - 1 < x; ps_clear xa (objBitsKO y) (ks\<lparr>ksPSpace := ksPSpace ks |` {..<x}\<rparr>)\<rbrakk> \<Longrightarrow> ps_clear xa (objBitsKO y) ks proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>ksPSpace ks xa = Some y; xa \<le> xa + 2 ^ objBitsKO y - 1; xa + 2 ^ objBitsKO y - 1 < x; ({xa..xa + 2 ^ objBitsKO y - 1} - {xa}) \<inter> (dom (ksPSpace ks) \<inter> {..<x}) = {}\<rbrakk> \<Longrightarrow> ({xa..xa + 2 ^ objBitsKO y - 1} - {xa}) \<inter> dom (ksPSpace ks) = {} proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>ksPSpace ks xa = Some y; xa \<le> xa + 2 ^ objBitsKO y - 1; xa + 2 ^ objBitsKO y - 1 < x\<rbrakk> \<Longrightarrow> ({xa..xa + 2 ^ objBitsKO y - 1} - {xa}) \<inter> dom (ksPSpace ks) = ({xa..xa + 2 ^ objBitsKO y - 1} - {xa}) \<inter> (dom (ksPSpace ks) \<inter> {..<x}) proof (prove)
goal:
No subgoals!