theory Detype_C

lemma ctes_of_is_aligned:
  fixes s :: "kernel_state"
  assumes ks: "ctes_of s p = Some cte"
  shows "is_aligned p (objBits cte)" proof - have "cte_wp_at' ((=) cte) p s" using ks by (clarsimp simp: cte_wp_at_ctes_of) thus ?thesis apply (simp add: cte_wp_at_cases' objBits_simps' cte_level_bits_def) apply (erule disjE) apply simp apply clarsimp apply (drule_tac y = n in aligned_add_aligned [where m = 4]) apply (simp add: tcb_cte_cases_def is_aligned_def split: if_split_asm) apply (simp add: word_bits_conv) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p (objBits cte) proof (state)
goal (1 subgoal):
 1. is_aligned p (objBits cte) proof (prove)
goal (1 subgoal):
 1. cte_wp_at' ((=) cte) p s proof (prove)
using this:
ctes_of s p = Some cte

goal (1 subgoal):
 1. cte_wp_at' ((=) cte) p s proof (state)
this:
cte_wp_at' ((=) cte) p s

goal (1 subgoal):
 1. is_aligned p (objBits cte) proof (prove)
using this:
cte_wp_at' ((=) cte) p s

goal (1 subgoal):
 1. is_aligned p (objBits cte) proof (prove)
goal (1 subgoal):
 1. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> ps_clear p 4 s \<or> (\<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> cte = getF tcb \<and> ps_clear (p - n) 9 s)) \<Longrightarrow> is_aligned p 4 proof (prove)
goal (2 subgoals):
 1. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p 4 \<and> ps_clear p 4 s \<Longrightarrow> is_aligned p 4
 2. \<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> cte = getF tcb \<and> ps_clear (p - n) 9 s) \<Longrightarrow> is_aligned p 4 proof (prove)
goal (1 subgoal):
 1. \<exists>n tcb. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) 9 \<and> (\<exists>getF. (\<exists>setF. tcb_cte_cases n = Some (getF, setF)) \<and> cte = getF tcb \<and> ps_clear (p - n) 9 s) \<Longrightarrow> is_aligned p 4 proof (prove)
goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); is_aligned (p - n) 9; tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (p - n) 9 s\<rbrakk> \<Longrightarrow> is_aligned p 4 proof (prove)
goal (3 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (p - n) 9 s\<rbrakk> \<Longrightarrow> is_aligned n 4
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (p - n) 9 s\<rbrakk> \<Longrightarrow> 4 \<le> 9
 3. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (p - n) 9 s; is_aligned (p - n + n) 4\<rbrakk> \<Longrightarrow> is_aligned p 4 proof (prove)
goal (2 subgoals):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (p - n) 9 s\<rbrakk> \<Longrightarrow> 4 \<le> 9
 2. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (p - n) 9 s; is_aligned (p - n + n) 4\<rbrakk> \<Longrightarrow> is_aligned p 4 proof (prove)
goal (1 subgoal):
 1. \<And>n tcb getF setF. \<lbrakk>ksPSpace s (p - n) = Some (KOTCB tcb); tcb_cte_cases n = Some (getF, setF); cte = getF tcb; ps_clear (p - n) 9 s; is_aligned (p - n + n) 4\<rbrakk> \<Longrightarrow> is_aligned p 4 proof (prove)
goal:
No subgoals! proof (state)
this:
is_aligned p (objBits cte)

goal:
No subgoals!