theory Invariants_H

lemma tcb_space_clear:
  "\<lbrakk> tcb_cte_cases (y - x) = Some (getF, setF);
     is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s;
     ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v;
     \<lbrakk> x = y; getF = tcbCTable; setF = tcbCTable_update \<rbrakk> \<Longrightarrow> P
    \<rbrakk> \<Longrightarrow> P" apply (cases "x = y") apply simp apply (clarsimp simp: ps_clear_def) apply (drule_tac a=y in equals0D) apply (simp add: domI) apply (subgoal_tac "\<exists>z. y = x + z \<and> z < 2 ^ tcbBlockSizeBits") apply (elim exE conjE) apply (frule(1) is_aligned_no_wrap'[rotated, rotated]) apply (simp add: word_bits_conv objBits_defs) apply (erule notE, subst field_simps, rule word_plus_mono_right) apply (drule word_le_minus_one_leq,simp,erule is_aligned_no_wrap') apply (simp add: word_bits_conv) apply (simp add: objBits_defs) apply (rule_tac x="y - x" in exI) apply (simp add: tcb_cte_cases_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; \<lbrakk>x = y; getF = tcbCTable; setF = tcbCTable_update\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; \<lbrakk>x = y; getF = tcbCTable; setF = tcbCTable_update\<rbrakk> \<Longrightarrow> P; x = y\<rbrakk> \<Longrightarrow> P
 2. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; \<lbrakk>x = y; getF = tcbCTable; setF = tcbCTable_update\<rbrakk> \<Longrightarrow> P; x \<noteq> y\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; \<lbrakk>x = y; getF = tcbCTable; setF = tcbCTable_update\<rbrakk> \<Longrightarrow> P; x \<noteq> y\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ({x..x + 2 ^ tcbBlockSizeBits - 1} - {x}) \<inter> dom (ksPSpace s) = {}; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; x \<noteq> y\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; x \<noteq> y; y \<notin> ({x..x + 2 ^ tcbBlockSizeBits - 1} - {x}) \<inter> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; x \<noteq> y; x \<le> y \<longrightarrow> \<not> y \<le> x + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; x \<noteq> y; x \<le> y \<longrightarrow> \<not> y \<le> x + 2 ^ tcbBlockSizeBits - 1; \<exists>z. y = x + z \<and> z < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> P
 2. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; x \<noteq> y; x \<le> y \<longrightarrow> \<not> y \<le> x + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> \<exists>z. y = x + z \<and> z < 2 ^ tcbBlockSizeBits proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; x \<noteq> y; x \<le> y \<longrightarrow> \<not> y \<le> x + 2 ^ tcbBlockSizeBits - 1; y = x + z; z < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> P
 2. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; x \<noteq> y; x \<le> y \<longrightarrow> \<not> y \<le> x + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> \<exists>z. y = x + z \<and> z < 2 ^ tcbBlockSizeBits proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; x \<noteq> y; x \<le> y \<longrightarrow> \<not> y \<le> x + 2 ^ tcbBlockSizeBits - 1; y = x + z; z < 2 ^ tcbBlockSizeBits; x \<le> x + z\<rbrakk> \<Longrightarrow> P
 2. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; x \<noteq> y; x \<le> y \<longrightarrow> \<not> y \<le> x + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> \<exists>z. y = x + z \<and> z < 2 ^ tcbBlockSizeBits proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>tcb_cte_cases z = Some (getF, setF); is_aligned x 9; ksPSpace s x = Some (KOTCB tcb); ksPSpace s (x + z) = Some v; z \<noteq> 0; \<not> x + z \<le> 0x1FF + x; y = x + z; z < 0x200; x \<le> x + z\<rbrakk> \<Longrightarrow> P
 2. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; x \<noteq> y; x \<le> y \<longrightarrow> \<not> y \<le> x + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> \<exists>z. y = x + z \<and> z < 2 ^ tcbBlockSizeBits proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>tcb_cte_cases z = Some (getF, setF); is_aligned x 9; ksPSpace s x = Some (KOTCB tcb); ksPSpace s (x + z) = Some v; z \<noteq> 0; y = x + z; z < 0x200; x \<le> x + z\<rbrakk> \<Longrightarrow> z \<le> 0x1FF
 2. \<And>z. \<lbrakk>tcb_cte_cases z = Some (getF, setF); is_aligned x 9; ksPSpace s x = Some (KOTCB tcb); ksPSpace s (x + z) = Some v; z \<noteq> 0; y = x + z; z < 0x200; x \<le> x + z\<rbrakk> \<Longrightarrow> x \<le> x + 0x1FF
 3. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; x \<noteq> y; x \<le> y \<longrightarrow> \<not> y \<le> x + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> \<exists>z. y = x + z \<and> z < 2 ^ tcbBlockSizeBits proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>tcb_cte_cases z = Some (getF, setF); ksPSpace s x = Some (KOTCB tcb); ksPSpace s (x + z) = Some v; z \<noteq> 0; y = x + z; z < 0x200; x \<le> x + z\<rbrakk> \<Longrightarrow> 0x1FF < 2 ^ 9
 2. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; x \<noteq> y; x \<le> y \<longrightarrow> \<not> y \<le> x + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> \<exists>z. y = x + z \<and> z < 2 ^ tcbBlockSizeBits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x tcbBlockSizeBits; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; x \<noteq> y; x \<le> y \<longrightarrow> \<not> y \<le> x + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> \<exists>z. y = x + z \<and> z < 2 ^ tcbBlockSizeBits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x 9; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; x \<noteq> y; x \<le> y \<longrightarrow> \<not> y \<le> 0x1FF + x\<rbrakk> \<Longrightarrow> \<exists>z. y = x + z \<and> z < 0x200 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_cte_cases (y - x) = Some (getF, setF); is_aligned x 9; ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; x \<noteq> y; x \<le> y \<longrightarrow> \<not> y \<le> 0x1FF + x\<rbrakk> \<Longrightarrow> y = x + (y - x) \<and> y - x < 0x200 proof (prove)
goal:
No subgoals!