theory Invariants_H

lemma ps_clearI:
  "\<lbrakk> is_aligned p n; (1 :: word32) < 2 ^ n;
     \<And>x. \<lbrakk> x > p; x \<le> p + 2 ^ n - 1 \<rbrakk> \<Longrightarrow> ksPSpace s x = None \<rbrakk>
      \<Longrightarrow> ps_clear p n s" apply (subgoal_tac "p \<le> p + 1") apply (simp add: ps_clear_def2) apply (rule ccontr, erule nonemptyE, clarsimp) apply (drule word_leq_le_minus_one[where x="z + 1" for z]) apply clarsimp apply simp apply (erule is_aligned_get_word_bits) apply (erule(1) is_aligned_no_wrap') apply simp done

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