kings-crown/FVELER_Isabelle huggingface dataset:
theory CorresK_Lemmas

lemma corres_throwError_str [corresK_concrete_rER]:
  "corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r \<top> \<top> (throwError a) (throw b)"
  "corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r \<top> \<top> (throwError a) (throwError b)" by (simp add: corres_underlyingK_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r (\<lambda>_. True) (\<lambda>_. True) (throwError a) (throw b) &&& corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r (\<lambda>_. True) (\<lambda>_. True) (throwError a) (throwError b)
theory CorresK_Lemmas

lemma F_all2_pointwise[simp]:
  "F_all2 (\<lambda>x y _ _. F x y) xs ys = list_all2 F xs ys" apply (rule iffI) apply (clarsimp simp: F_all2_def) subgoal for F' apply (rule list_all2_induct_suffixeq[where Q=F']; simp) apply (drule_tac x=x in spec) apply (drule_tac x=y in spec) apply fastforce done apply (clarsimp simp:F_all2_def) apply (rule_tac x=F in exI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. F_all2 (\<lambda>x y _ _. F x y) xs ys = list_all2 F xs ys proof (prove)
goal (2 subgoals):
 1. F_all2 (\<lambda>x y _ _. F x y) xs ys \<Longrightarrow> list_all2 F xs ys
 2. list_all2 F xs ys \<Longrightarrow> F_all2 (\<lambda>x y _ _. F x y) xs ys proof (prove)
goal (2 subgoals):
 1. \<And>F'. \<lbrakk>\<forall>x y. F' x y \<longrightarrow> (\<exists>xs. Ex (list_all2 F' xs)) \<longrightarrow> F x y; list_all2 F' xs ys\<rbrakk> \<Longrightarrow> list_all2 F xs ys
 2. list_all2 F xs ys \<Longrightarrow> F_all2 (\<lambda>x y _ _. F x y) xs ys proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x y. F' x y \<longrightarrow> (\<exists>xs. Ex (list_all2 F' xs)) \<longrightarrow> F x y; list_all2 F' xs ys\<rbrakk> \<Longrightarrow> list_all2 F xs ys proof (prove)
goal (1 subgoal):
 1. \<And>x xsa y ysa. \<lbrakk>\<forall>x y. F' x y \<longrightarrow> (\<exists>xs. Ex (list_all2 F' xs)) \<longrightarrow> F x y; list_all2 F' xs ys; list_all2 F' xsa ysa; F' x y; list_all2 F xsa ysa; suffix (x # xsa) xs; suffix (y # ysa) ys\<rbrakk> \<Longrightarrow> F x y proof (prove)
goal (1 subgoal):
 1. \<And>x xsa y ysa. \<lbrakk>list_all2 F' xs ys; list_all2 F' xsa ysa; F' x y; list_all2 F xsa ysa; suffix (x # xsa) xs; suffix (y # ysa) ys; \<forall>y. F' x y \<longrightarrow> (\<exists>xs. Ex (list_all2 F' xs)) \<longrightarrow> F x y\<rbrakk> \<Longrightarrow> F x y proof (prove)
goal (1 subgoal):
 1. \<And>x xsa y ysa. \<lbrakk>list_all2 F' xs ys; list_all2 F' xsa ysa; F' x y; list_all2 F xsa ysa; suffix (x # xsa) xs; suffix (y # ysa) ys; F' x y \<longrightarrow> (\<exists>xs. Ex (list_all2 F' xs)) \<longrightarrow> F x y\<rbrakk> \<Longrightarrow> F x y proof (prove)
goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. list_all2 F xs ys \<Longrightarrow> F_all2 (\<lambda>x y _ _. F x y) xs ys proof (prove)
goal (1 subgoal):
 1. list_all2 F xs ys \<Longrightarrow> \<exists>F'. (\<forall>x y. F' x y \<longrightarrow> (\<exists>xs. Ex (list_all2 F' xs)) \<longrightarrow> F x y) \<and> list_all2 F' xs ys proof (prove)
goal (1 subgoal):
 1. list_all2 F xs ys \<Longrightarrow> (\<forall>x y. F x y \<longrightarrow> (\<exists>xs. Ex (list_all2 F xs)) \<longrightarrow> F x y) \<and> list_all2 F xs ys proof (prove)
goal:
No subgoals!
theory CorresK_Lemmas

lemma F_all2_list:
   "F xs ys \<Longrightarrow> \<exists>F'. (\<forall>xs ys. (F xs ys = list_all2 F' xs ys)) \<Longrightarrow> F_all2 (\<lambda>_ _ xs ys. F xs ys) xs ys" apply (clarsimp simp: F_all2_def) apply (rule_tac x=F' in exI) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F xs ys; \<exists>F'. \<forall>xs ys. F xs ys = list_all2 F' xs ys\<rbrakk> \<Longrightarrow> F_all2 (\<lambda>_ _. F) xs ys proof (prove)
goal (1 subgoal):
 1. \<And>F'. \<lbrakk>list_all2 F' xs ys; \<forall>xs ys. F xs ys = list_all2 F' xs ys\<rbrakk> \<Longrightarrow> \<exists>F'a. ((\<exists>x. Ex (F'a x)) \<longrightarrow> (\<forall>xs ys. list_all2 F'a xs ys \<longrightarrow> list_all2 F' xs ys)) \<and> list_all2 F'a xs ys proof (prove)
goal (1 subgoal):
 1. \<And>F'. \<lbrakk>list_all2 F' xs ys; \<forall>xs ys. F xs ys = list_all2 F' xs ys\<rbrakk> \<Longrightarrow> ((\<exists>x. Ex (F' x)) \<longrightarrow> (\<forall>xs ys. list_all2 F' xs ys \<longrightarrow> list_all2 F' xs ys)) \<and> list_all2 F' xs ys
theory CorresK_Lemmas

lemma list_all2_conjD:
  "list_all2 (\<lambda>x y. Q x y \<and> P x y) xs ys \<Longrightarrow> list_all2 Q xs ys \<and> list_all2 P xs ys" by (induct rule: list_all2_induct; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_all2 (\<lambda>x y. Q x y \<and> P x y) xs ys \<Longrightarrow> list_all2 Q xs ys \<and> list_all2 P xs ys
theory CorresK_Lemmas

lemma list_all_mem_subset:
  "list_all (\<lambda>y. y \<in> set xs) ys = (set ys \<subseteq> set xs)" by (induct ys; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_all (\<lambda>y. y \<in> set xs) ys = (set ys \<subseteq> set xs)
theory CorresK_Lemmas

lemma F_all2_conjI:
  "F_all2 F xs ys \<Longrightarrow> F_all2 F' xs ys \<Longrightarrow>
    F_all2 (\<lambda>x y xs ys. F x y xs ys \<and> F' x y xs ys) xs ys" apply (clarsimp simp: F_all2_def) apply (rule_tac x="\<lambda>x y. F'a x y \<and> F'aa x y" in exI) by (auto dest: list_all2_conjD intro: list_all2_conj)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F_all2 F xs ys; F_all2 F' xs ys\<rbrakk> \<Longrightarrow> F_all2 (\<lambda>x y xs ys. F x y xs ys \<and> F' x y xs ys) xs ys proof (prove)
goal (1 subgoal):
 1. \<And>F'a F'aa. \<lbrakk>\<forall>x y. F'a x y \<longrightarrow> (\<forall>xs ys. list_all2 F'a xs ys \<longrightarrow> F x y xs ys); list_all2 F'a xs ys; \<forall>x y. F'aa x y \<longrightarrow> (\<forall>xs ys. list_all2 F'aa xs ys \<longrightarrow> F' x y xs ys); list_all2 F'aa xs ys\<rbrakk> \<Longrightarrow> \<exists>F'a. (\<forall>x y. F'a x y \<longrightarrow> (\<forall>xs ys. list_all2 F'a xs ys \<longrightarrow> F x y xs ys \<and> F' x y xs ys)) \<and> list_all2 F'a xs ys proof (prove)
goal (1 subgoal):
 1. \<And>F'a F'aa. \<lbrakk>\<forall>x y. F'a x y \<longrightarrow> (\<forall>xs ys. list_all2 F'a xs ys \<longrightarrow> F x y xs ys); list_all2 F'a xs ys; \<forall>x y. F'aa x y \<longrightarrow> (\<forall>xs ys. list_all2 F'aa xs ys \<longrightarrow> F' x y xs ys); list_all2 F'aa xs ys\<rbrakk> \<Longrightarrow> (\<forall>x y. F'a x y \<and> F'aa x y \<longrightarrow> (\<forall>xs ys. list_all2 (\<lambda>x y. F'a x y \<and> F'aa x y) xs ys \<longrightarrow> F x y xs ys \<and> F' x y xs ys)) \<and> list_all2 (\<lambda>x y. F'a x y \<and> F'aa x y) xs ys
theory CorresK_Lemmas

lemma corresK_discard_rv:
  assumes A[corresK]: "corres_underlyingK sr nf nf' F r' P P' a c"
  shows "corres_underlyingK sr nf nf' F dc P P' (do x \<leftarrow> a; return () od) (do x \<leftarrow> c; return () od)" by corresKsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlyingK sr nf nf' F dc P P' (do x <- a;
return ()
od) (do x <- c;
return ()
od)
theory CorresK_Lemmas

lemma corresK_mapM_mapM_x:
  assumes "corres_underlyingK sr nf nf' F r' P P' (mapM f as) (mapM f' cs)"
  shows "corres_underlyingK sr nf nf' F dc P P' (mapM_x f as) (mapM_x f' cs)" unfolding mapM_x_mapM by (rule corresK_discard_rv, rule assms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlyingK sr nf nf' F dc P P' (mapM_x f as) (mapM_x f' cs) proof (prove)
goal (1 subgoal):
 1. corres_underlyingK sr nf nf' F dc P P' (do x <- mapM f as;
return ()
od) (do x <- mapM f' cs;
return ()
od)
theory CorresK_Lemmas

lemma corresK_subst_both: "g' = f' \<Longrightarrow> g = f \<Longrightarrow>
  corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow>
  corres_underlyingK sr nf nf' F r P P' g g'" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' = f'; g = f; corres_underlyingK sr nf nf' F r P P' f f'\<rbrakk> \<Longrightarrow> corres_underlyingK sr nf nf' F r P P' g g'
theory CorresK_Lemmas

lemma if_fun_true: "(if A then B else (\<lambda>_. True)) = (\<lambda>s. (A  \<longrightarrow> B s))" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if A then B else (\<lambda>_. True)) = (\<lambda>s. A \<longrightarrow> B s)
theory CorresK_Lemmas

lemma corresK_Id:
  "(nf' \<Longrightarrow> no_fail P' g) \<Longrightarrow>
    corres_underlyingK Id nf nf' (f = g \<and> (\<forall>rv. r rv rv)) r (\<lambda>_. True) P' f g" apply (rule corresK_assume_guard) apply (rule corres_Id;simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (nf' \<Longrightarrow> no_fail P' g) \<Longrightarrow> corres_underlyingK Id nf nf' (f = g \<and> (\<forall>rv. r rv rv)) r (\<lambda>_. True) P' f g proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nf' \<Longrightarrow> no_fail P' g; f = g \<and> (\<forall>rv. r rv rv)\<rbrakk> \<Longrightarrow> corres_underlying Id nf nf' r (\<lambda>_. True) P' f g proof (prove)
goal:
No subgoals!
theory CorresK_Lemmas

lemma corresK_unit_rv_eq_any[corresK_concrete_r]:
  "corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow>
    corres_underlyingK sr nf nf' F
      (\<lambda>(x :: unit) (y :: unit). x = y) P P' f f'" apply (clarsimp simp add: corres_underlyingK_def) apply (erule corres_rel_imp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow> corres_underlyingK sr nf nf' F (=) P P' f f' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F; corres_underlying sr nf nf' r P P' f f'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (\<lambda>x y. True) P P' f f' proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>F; r x y\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!
theory CorresK_Lemmas

lemma corresK_unit_rv_dc_any[corresK_concrete_r]:
  "corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow>
    corres_underlyingK sr nf nf' F
      (\<lambda>(x :: unit) (y :: unit). dc x y) P P' f f'" apply (clarsimp simp add: corres_underlyingK_def) apply (erule corres_rel_imp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow> corres_underlyingK sr nf nf' F dc P P' f f' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F; corres_underlying sr nf nf' r P P' f f'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (\<lambda>x y. True) P P' f f' proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>F; r x y\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!
theory Bits_R

lemma throwE_R: "\<lbrace>\<top>\<rbrace> throw f \<lbrace>P\<rbrace>,-" by (simp add: validE_R_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> throw f \<lbrace>P\<rbrace>, -
theory Bits_R

lemma withoutFailure_wp [wp]:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> withoutFailure f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> withoutFailure f \<lbrace>Q\<rbrace>,-"
  "\<lbrace>\<top>\<rbrace> withoutFailure f -,\<lbrace>E\<rbrace>" by (auto simp: validE_R_def validE_E_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> withoutFailure f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>) &&& (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> withoutFailure f \<lbrace>Q\<rbrace>, -) &&& \<lbrace>\<lambda>_. True\<rbrace> withoutFailure f -, \<lbrace>E\<rbrace>
theory Bits_R

lemma no_fail_typeError [simp, wp]:
  "no_fail \<bottom> (typeError xs ko)" by (simp add: typeError_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. False) (typeError xs ko)
theory Bits_R

lemma isCap_simps:
  "isZombie v = (\<exists>v0 v1 v2. v = Zombie v0 v1 v2)"
  "isArchObjectCap v = (\<exists>v0. v = ArchObjectCap v0)"
  "isThreadCap v = (\<exists>v0. v = ThreadCap v0)"
  "isCNodeCap v = (\<exists>v0 v1 v2 v3. v = CNodeCap v0 v1 v2 v3)"
  "isNotificationCap v = (\<exists>v0 v1 v2 v3. v = NotificationCap v0 v1 v2 v3)"
  "isEndpointCap v = (\<exists>v0 v1 v2 v3 v4 v5. v = EndpointCap v0 v1 v2 v3 v4 v5)"
  "isUntypedCap v = (\<exists>d v0 v1 f. v = UntypedCap d v0 v1 f)"
  "isReplyCap v = (\<exists>v0 v1 v2. v = ReplyCap v0 v1 v2)"
  "isIRQControlCap v = (v = IRQControlCap)"
  "isIRQHandlerCap v = (\<exists>v0. v = IRQHandlerCap v0)"
  "isNullCap v = (v = NullCap)"
  "isDomainCap v = (v = DomainCap)"
  "isPageCap w = (\<exists>d v0 v1 v2 v3. w = PageCap d v0 v1 v2 v3)"
  "isPageTableCap w = (\<exists>v0 v1. w = PageTableCap v0 v1)"
  "isPageDirectoryCap w = (\<exists>v0 v1. w = PageDirectoryCap v0 v1)"
  "isASIDControlCap w = (w = ASIDControlCap)"
  "isASIDPoolCap w = (\<exists>v0 v1. w = ASIDPoolCap v0 v1)"
  "isArchPageCap cap = (\<exists>d ref rghts sz data. cap = ArchObjectCap (PageCap d ref rghts sz data))" by (auto simp: isCap_defs split: capability.splits arch_capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((isZombie v = (\<exists>v0 v1 v2. v = capability.Zombie v0 v1 v2) &&& isArchObjectCap v = (\<exists>v0. v = capability.ArchObjectCap v0)) &&& isThreadCap v = (\<exists>v0. v = capability.ThreadCap v0) &&& isCNodeCap v = (\<exists>v0 v1 v2 v3. v = capability.CNodeCap v0 v1 v2 v3)) &&& (isNotificationCap v = (\<exists>v0 v1 v2 v3. v = capability.NotificationCap v0 v1 v2 v3) &&& isEndpointCap v = (\<exists>v0 v1 v2 v3 v4 v5. v = capability.EndpointCap v0 v1 v2 v3 v4 v5)) &&& isUntypedCap v = (\<exists>d v0 v1 f. v = capability.UntypedCap d v0 v1 f) &&& isReplyCap v = (\<exists>v0 v1 v2. v = capability.ReplyCap v0 v1 v2) &&& isIRQControlCap v = (v = capability.IRQControlCap)) &&& ((isIRQHandlerCap v = (\<exists>v0. v = capability.IRQHandlerCap v0) &&& isNullCap v = (v = capability.NullCap)) &&& isDomainCap v = (v = capability.DomainCap) &&& isPageCap w = (\<exists>d v0 v1 v2 v3. w = arch_capability.PageCap d v0 v1 v2 v3)) &&& (isPageTableCap w = (\<exists>v0 v1. w = arch_capability.PageTableCap v0 v1) &&& isPageDirectoryCap w = (\<exists>v0 v1. w = arch_capability.PageDirectoryCap v0 v1)) &&& isASIDControlCap w = (w = arch_capability.ASIDControlCap) &&& isASIDPoolCap w = (\<exists>v0 v1. w = arch_capability.ASIDPoolCap v0 v1) &&& isArchPageCap cap = (\<exists>d ref rghts sz data. cap = capability.ArchObjectCap (arch_capability.PageCap d ref rghts sz data))
theory Bits_R

lemma untyped_not_null [simp]:
  "\<not> isUntypedCap NullCap" by (simp add: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> isUntypedCap capability.NullCap
theory Bits_R

lemma projectKO_tcb:
  "(projectKO_opt ko = Some t) = (ko = KOTCB t)" by (cases ko) (auto simp: projectKO_opts_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (projectKO_opt ko = Some t) = (ko = KOTCB t)
theory Bits_R

lemma projectKO_cte:
  "(projectKO_opt ko = Some t) = (ko = KOCTE t)" by (cases ko) (auto simp: projectKO_opts_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (projectKO_opt ko = Some t) = (ko = KOCTE t)
theory Bits_R

lemma projectKO_ep:
  "(projectKO_opt ko = Some t) = (ko = KOEndpoint t)" by (cases ko) (auto simp: projectKO_opts_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (projectKO_opt ko = Some t) = (ko = KOEndpoint t)
theory Bits_R

lemma projectKO_ntfn:
  "(projectKO_opt ko = Some t) = (ko = KONotification t)" by (cases ko) (auto simp: projectKO_opts_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (projectKO_opt ko = Some t) = (ko = KONotification t)
theory Bits_R

lemma projectKO_ASID:
  "(projectKO_opt ko = Some t) = (ko = KOArch (KOASIDPool t))" by (cases ko)
     (auto simp: projectKO_opts_defs split: arch_kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (projectKO_opt ko = Some t) = (ko = KOArch (KOASIDPool t))
theory Bits_R

lemma projectKO_PTE:
  "(projectKO_opt ko = Some t) = (ko = KOArch (KOPTE t))" by (cases ko)
     (auto simp: projectKO_opts_defs split: arch_kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (projectKO_opt ko = Some t) = (ko = KOArch (KOPTE t))
theory Bits_R

lemma projectKO_PDE:
  "(projectKO_opt ko = Some t) = (ko = KOArch (KOPDE t))" by (cases ko)
     (auto simp: projectKO_opts_defs split: arch_kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (projectKO_opt ko = Some t) = (ko = KOArch (KOPDE t))
theory Bits_R

lemma projectKO_user_data:
  "(projectKO_opt ko = Some (t :: user_data)) = (ko = KOUserData)" by (cases ko)
     (auto simp: projectKO_opts_defs split: arch_kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (projectKO_opt ko = Some t) = (ko = KOUserData)
theory Bits_R

lemma projectKO_user_data_device:
  "(projectKO_opt ko = Some (t :: user_data_device)) = (ko = KOUserDataDevice)" by (cases ko)
     (auto simp: projectKO_opts_defs split: arch_kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (projectKO_opt ko = Some t) = (ko = KOUserDataDevice)
theory Bits_R

lemma capAligned_epI:
  "ep_at' p s \<Longrightarrow> capAligned (EndpointCap p a b c d e)" apply (clarsimp simp: obj_at'_real_def capAligned_def
                        objBits_simps word_bits_def) apply (drule ko_wp_at_norm) apply clarsimp apply (drule ko_wp_at_aligned) apply (simp add: objBits_simps' projectKOs capUntypedPtr_def isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep_at' p s \<Longrightarrow> capAligned (capability.EndpointCap p a b c d e) proof (prove)
goal (1 subgoal):
 1. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) p s \<Longrightarrow> is_aligned (global.capUntypedPtr (capability.EndpointCap p a b c d e)) epSizeBits \<and> epSizeBits < 32 proof (prove)
goal (1 subgoal):
 1. \<exists>ko. (\<exists>obj. projectKO_opt ko = Some obj) \<and> ko_wp_at' ((=) ko) p s \<Longrightarrow> is_aligned (global.capUntypedPtr (capability.EndpointCap p a b c d e)) epSizeBits \<and> epSizeBits < 32 proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>ko_wp_at' ((=) ko) p s; projectKO_opt ko = Some obj\<rbrakk> \<Longrightarrow> is_aligned (global.capUntypedPtr (capability.EndpointCap p a b c d e)) epSizeBits \<and> epSizeBits < 32 proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>projectKO_opt ko = Some obj; is_aligned p (objBitsKO ko)\<rbrakk> \<Longrightarrow> is_aligned (global.capUntypedPtr (capability.EndpointCap p a b c d e)) epSizeBits \<and> epSizeBits < 32 proof (prove)
goal:
No subgoals!
theory Bits_R

lemma capAligned_ntfnI:
  "ntfn_at' p s \<Longrightarrow> capAligned (NotificationCap p a b c)" apply (clarsimp simp: obj_at'_real_def capAligned_def
                        objBits_simps word_bits_def capUntypedPtr_def isCap_simps) apply (fastforce dest: ko_wp_at_norm
                  dest!: ko_wp_at_aligned simp: objBits_simps' projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ntfn_at' p s \<Longrightarrow> capAligned (capability.NotificationCap p a b c) proof (prove)
goal (1 subgoal):
 1. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) p s \<Longrightarrow> is_aligned p ntfnSizeBits \<and> ntfnSizeBits < 32 proof (prove)
goal:
No subgoals!
theory Bits_R

lemma capAligned_tcbI:
  "tcb_at' p s \<Longrightarrow> capAligned (ThreadCap p)" apply (clarsimp simp: obj_at'_real_def capAligned_def
                        objBits_simps word_bits_def capUntypedPtr_def isCap_simps) apply (fastforce dest: ko_wp_at_norm
                  dest!: ko_wp_at_aligned simp: objBits_simps' projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at' p s \<Longrightarrow> capAligned (capability.ThreadCap p) proof (prove)
goal (1 subgoal):
 1. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) p s \<Longrightarrow> is_aligned p tcbBlockSizeBits \<and> tcbBlockSizeBits < 32 proof (prove)
goal:
No subgoals!
theory Bits_R

lemma obj_at_valid_objs':
  "\<lbrakk> obj_at' P p s; valid_objs' s \<rbrakk> \<Longrightarrow>
  \<exists>k. P k \<and>
      ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko)
       \<longrightarrow> valid_obj' (injectKO k) s)" apply (drule obj_at_ko_at') apply clarsimp apply (rule_tac x=ko in exI) apply clarsimp apply (erule (1) ko_at_valid_objs') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' P p s; valid_objs' s\<rbrakk> \<Longrightarrow> \<exists>k. P k \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko) \<longrightarrow> valid_obj' (injectKO k) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs' s; \<exists>ko. ko_at' ko p s \<and> P ko\<rbrakk> \<Longrightarrow> \<exists>k. P k \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko) \<longrightarrow> valid_obj' (injectKO k) s) proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>valid_objs' s; ko_at' ko p s; P ko\<rbrakk> \<Longrightarrow> \<exists>k. P k \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko) \<longrightarrow> valid_obj' (injectKO k) s) proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>valid_objs' s; ko_at' ko p s; P ko\<rbrakk> \<Longrightarrow> P ko \<and> ((\<forall>koa. projectKO_opt koa = Some ko \<longrightarrow> injectKO ko = koa) \<longrightarrow> valid_obj' (injectKO ko) s) proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>valid_objs' s; ko_at' ko p s; P ko; \<forall>koa. projectKO_opt koa = Some ko \<longrightarrow> injectKO ko = koa\<rbrakk> \<Longrightarrow> valid_obj' (injectKO ko) s proof (prove)
goal (1 subgoal):
 1. \<And>ko koa. \<lbrakk>valid_objs' s; P ko; \<forall>koa. projectKO_opt koa = Some ko \<longrightarrow> injectKO ko = koa; projectKO_opt koa = Some ko\<rbrakk> \<Longrightarrow> injectKO ko = koa proof (prove)
goal:
No subgoals!
theory Bits_R

lemma tcb_in_valid_state':
  "\<lbrakk> st_tcb_at' P t s; valid_objs' s \<rbrakk> \<Longrightarrow> \<exists>st. P st \<and> valid_tcb_state' st s" apply (clarsimp simp: pred_tcb_at'_def) apply (drule obj_at_valid_objs') apply fastforce apply (clarsimp simp: projectKOs) apply (fastforce simp add: valid_obj'_def valid_tcb'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' P t s; valid_objs' s\<rbrakk> \<Longrightarrow> \<exists>st. P st \<and> valid_tcb_state' st s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' (\<lambda>ko. P (tcbState ko)) t s; valid_objs' s\<rbrakk> \<Longrightarrow> \<exists>st. P st \<and> valid_tcb_state' st s proof (prove)
goal (2 subgoals):
 1. valid_objs' s \<Longrightarrow> valid_objs' s
 2. \<lbrakk>valid_objs' s; \<exists>k. P (tcbState k) \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko) \<longrightarrow> valid_obj' (injectKO k) s)\<rbrakk> \<Longrightarrow> \<exists>st. P st \<and> valid_tcb_state' st s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs' s; \<exists>k. P (tcbState k) \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko) \<longrightarrow> valid_obj' (injectKO k) s)\<rbrakk> \<Longrightarrow> \<exists>st. P st \<and> valid_tcb_state' st s proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>valid_objs' s; P (tcbState k); valid_obj' (KOTCB k) s\<rbrakk> \<Longrightarrow> \<exists>st. P st \<and> valid_tcb_state' st s proof (prove)
goal:
No subgoals!
theory Bits_R

lemma getCurThread_corres [corres]: "corres (=) \<top> \<top> (gets cur_thread) getCurThread" by (simp add: getCurThread_def curthread_relation)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) (\<lambda>_. True) (gets cur_thread) getCurThread
theory Bits_R

lemma gct_wp [wp]: "\<lbrace>\<lambda>s. P (ksCurThread s) s\<rbrace> getCurThread \<lbrace>P\<rbrace>" by (unfold getCurThread_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s) s\<rbrace> getCurThread \<lbrace>P\<rbrace>