theory Invariants_H

lemma in_magnitude_check:
  "\<lbrakk> is_aligned x n; (1 :: word32) < 2 ^ n; ksPSpace s x = Some y \<rbrakk> \<Longrightarrow>
   ((v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s))
     = (s' = s \<and> ps_clear x n s)" apply (rule iffI) apply (clarsimp simp: magnitudeCheck_def in_monad lookupAround2_None2
                         lookupAround2_char2
                  split: option.split_asm) apply (erule(1) ps_clearI) apply simp apply (erule(1) ps_clearI) apply (simp add: linorder_not_less) apply (drule word_leq_le_minus_one[where x="2 ^ n"]) apply (clarsimp simp: power_overflow) apply (drule word_l_diffs) apply simp apply (simp add: field_simps) apply clarsimp apply (erule is_aligned_get_word_bits) apply (erule(1) ps_clear_lookupAround2) apply simp apply (simp add: is_aligned_no_overflow) apply (clarsimp simp add: magnitudeCheck_def in_monad
                      split: option.split_asm) apply simp apply (simp add: power_overflow) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> ((v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s)) = (s' = s \<and> ps_clear x n s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; (v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s)\<rbrakk> \<Longrightarrow> s' = s \<and> ps_clear x n s
 2. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; s' = s \<and> ps_clear x n s\<rbrakk> \<Longrightarrow> (v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; \<forall>y>x. ksPSpace s y = None; s' = s\<rbrakk> \<Longrightarrow> ps_clear x n s
 2. \<And>x2 ya. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; x < x2; \<not> x2 - x < 2 ^ n; \<forall>z. x < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; s' = s\<rbrakk> \<Longrightarrow> ps_clear x n s
 3. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; s' = s \<and> ps_clear x n s\<rbrakk> \<Longrightarrow> (v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; \<forall>y>x. ksPSpace s y = None; s' = s; x < xa; xa \<le> x + 2 ^ n - 1\<rbrakk> \<Longrightarrow> ksPSpace s xa = None
 2. \<And>x2 ya. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; x < x2; \<not> x2 - x < 2 ^ n; \<forall>z. x < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; s' = s\<rbrakk> \<Longrightarrow> ps_clear x n s
 3. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; s' = s \<and> ps_clear x n s\<rbrakk> \<Longrightarrow> (v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal (2 subgoals):
 1. \<And>x2 ya. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; x < x2; \<not> x2 - x < 2 ^ n; \<forall>z. x < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; s' = s\<rbrakk> \<Longrightarrow> ps_clear x n s
 2. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; s' = s \<and> ps_clear x n s\<rbrakk> \<Longrightarrow> (v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal (2 subgoals):
 1. \<And>x2 ya xa. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; x < x2; \<not> x2 - x < 2 ^ n; \<forall>z. x < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; s' = s; x < xa; xa \<le> x + 2 ^ n - 1\<rbrakk> \<Longrightarrow> ksPSpace s xa = None
 2. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; s' = s \<and> ps_clear x n s\<rbrakk> \<Longrightarrow> (v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal (2 subgoals):
 1. \<And>x2 ya xa. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; x < x2; 2 ^ n \<le> x2 - x; \<forall>z. x < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; s' = s; x < xa; xa \<le> x + 2 ^ n - 1\<rbrakk> \<Longrightarrow> ksPSpace s xa = None
 2. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; s' = s \<and> ps_clear x n s\<rbrakk> \<Longrightarrow> (v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal (3 subgoals):
 1. \<And>x2 ya xa. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; x < x2; \<forall>z. x < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; s' = s; x < xa; xa \<le> x + 2 ^ n - 1\<rbrakk> \<Longrightarrow> 2 ^ n \<noteq> 0
 2. \<And>x2 ya xa. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; x < x2; \<forall>z. x < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; s' = s; x < xa; xa \<le> x + 2 ^ n - 1; 2 ^ n - 1 < x2 - x\<rbrakk> \<Longrightarrow> ksPSpace s xa = None
 3. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; s' = s \<and> ps_clear x n s\<rbrakk> \<Longrightarrow> (v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal (2 subgoals):
 1. \<And>x2 ya xa. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; x < x2; \<forall>z. x < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; s' = s; x < xa; xa \<le> x + 2 ^ n - 1; 2 ^ n - 1 < x2 - x\<rbrakk> \<Longrightarrow> ksPSpace s xa = None
 2. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; s' = s \<and> ps_clear x n s\<rbrakk> \<Longrightarrow> (v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal (3 subgoals):
 1. \<And>x2 ya xa. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; x < x2; \<forall>z. x < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; s' = s; x < xa; xa \<le> x + 2 ^ n - 1\<rbrakk> \<Longrightarrow> x \<le> x2
 2. \<And>x2 ya xa. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; x < x2; \<forall>z. x < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; s' = s; x < xa; xa \<le> x + 2 ^ n - 1; 2 ^ n - 1 + x < x2\<rbrakk> \<Longrightarrow> ksPSpace s xa = None
 3. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; s' = s \<and> ps_clear x n s\<rbrakk> \<Longrightarrow> (v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal (2 subgoals):
 1. \<And>x2 ya xa. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; x < x2; \<forall>z. x < z \<and> z < x2 \<longrightarrow> ksPSpace s z = None; ksPSpace s x2 = Some ya; s' = s; x < xa; xa \<le> x + 2 ^ n - 1; 2 ^ n - 1 + x < x2\<rbrakk> \<Longrightarrow> ksPSpace s xa = None
 2. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; s' = s \<and> ps_clear x n s\<rbrakk> \<Longrightarrow> (v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; s' = s \<and> ps_clear x n s\<rbrakk> \<Longrightarrow> (v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some y; s' = s; ps_clear x n s\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; s' = s; ps_clear x n s; is_aligned x n; n < LENGTH(32)\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s)
 2. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; s' = s; ps_clear x n s; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; s' = s; is_aligned x n; n < LENGTH(32)\<rbrakk> \<Longrightarrow> x \<le> x
 2. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; s' = s; is_aligned x n; n < LENGTH(32)\<rbrakk> \<Longrightarrow> x \<le> x + 2 ^ n - 1
 3. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; s' = s; is_aligned x n; n < LENGTH(32); fst (lookupAround2 x (ksPSpace s)) = Some (x, y); case snd (lookupAround2 x (ksPSpace s)) of None \<Rightarrow> True | Some xa \<Rightarrow> 2 ^ n \<le> xa - x\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s)
 4. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; s' = s; ps_clear x n s; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; s' = s; is_aligned x n; n < LENGTH(32)\<rbrakk> \<Longrightarrow> x \<le> x + 2 ^ n - 1
 2. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; s' = s; is_aligned x n; n < LENGTH(32); fst (lookupAround2 x (ksPSpace s)) = Some (x, y); case snd (lookupAround2 x (ksPSpace s)) of None \<Rightarrow> True | Some xa \<Rightarrow> 2 ^ n \<le> xa - x\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s)
 3. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; s' = s; ps_clear x n s; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; s' = s; is_aligned x n; n < LENGTH(32); fst (lookupAround2 x (ksPSpace s)) = Some (x, y); case snd (lookupAround2 x (ksPSpace s)) of None \<Rightarrow> True | Some xa \<Rightarrow> 2 ^ n \<le> xa - x\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s)
 2. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; s' = s; ps_clear x n s; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; is_aligned x n; n < 32; fst (lookupAround2 x (ksPSpace s)) = Some (x, y); snd (lookupAround2 x (ksPSpace s)) = Some x2; 2 ^ n \<le> x2 - x; x2 - x < 2 ^ n\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; s' = s; ps_clear x n s; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 < 2 ^ n; ksPSpace s x = Some y; s' = s; ps_clear x n s; x = 0; LENGTH(32) \<le> n\<rbrakk> \<Longrightarrow> ((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s) proof (prove)
goal:
No subgoals!