kings-crown/FVELER_Isabelle huggingface dataset:
theory Invariants_AI

lemma valid_cs_sizeE [elim]:
  assumes "valid_cs_size sz cs"
  and     "\<lbrakk> sz < word_bits - cte_level_bits; dom cs = {x. length x = sz};
            obj_bits (CNode sz cs) = cte_level_bits + sz\<rbrakk>
           \<Longrightarrow> R"
  shows "R" using assms by (auto simp: valid_cs_size_def well_formed_cnode_n_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R proof (prove)
using this:
valid_cs_size sz cs
\<lbrakk>sz < word_bits - cte_level_bits; dom cs = {x. length x = sz}; obj_bits (CNode sz cs) = cte_level_bits + sz\<rbrakk> \<Longrightarrow> R

goal (1 subgoal):
 1. R
theory Invariants_AI

lemma valid_obj_sizes:
  assumes vp: "valid_objs s"
  and     ko: "ko \<in> ran (kheap s)"
  shows   "obj_bits ko < word_bits" proof (cases ko) case CNode thus ?thesis using vp ko by (auto dest!: valid_objs_valid_cs_size) next case (ArchObj ako) show ?thesis using ArchObj by (simp only: valid_arch_sizes) qed (auto elim: valid_pspaceE
          simp: valid_arch_sizes[unfolded word_bits_conv] word_bits_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_bits ko < word_bits proof (state)
goal (5 subgoals):
 1. \<And>x11 x12. ko = CNode x11 x12 \<Longrightarrow> obj_bits ko < word_bits
 2. \<And>x2. ko = TCB x2 \<Longrightarrow> obj_bits ko < word_bits
 3. \<And>x3. ko = Endpoint x3 \<Longrightarrow> obj_bits ko < word_bits
 4. \<And>x4. ko = Notification x4 \<Longrightarrow> obj_bits ko < word_bits
 5. \<And>x5. ko = ArchObj x5 \<Longrightarrow> obj_bits ko < word_bits proof (state)
this:
ko = CNode x11_ x12_

goal (5 subgoals):
 1. \<And>x11 x12. ko = CNode x11 x12 \<Longrightarrow> obj_bits ko < word_bits
 2. \<And>x2. ko = TCB x2 \<Longrightarrow> obj_bits ko < word_bits
 3. \<And>x3. ko = Endpoint x3 \<Longrightarrow> obj_bits ko < word_bits
 4. \<And>x4. ko = Notification x4 \<Longrightarrow> obj_bits ko < word_bits
 5. \<And>x5. ko = ArchObj x5 \<Longrightarrow> obj_bits ko < word_bits proof (prove)
using this:
ko = CNode x11_ x12_

goal (1 subgoal):
 1. obj_bits ko < word_bits proof (prove)
using this:
ko = CNode x11_ x12_
valid_objs s
ko \<in> ran (kheap s)

goal (1 subgoal):
 1. obj_bits ko < word_bits proof (state)
this:
obj_bits ko < word_bits

goal (4 subgoals):
 1. \<And>x2. ko = TCB x2 \<Longrightarrow> obj_bits ko < word_bits
 2. \<And>x3. ko = Endpoint x3 \<Longrightarrow> obj_bits ko < word_bits
 3. \<And>x4. ko = Notification x4 \<Longrightarrow> obj_bits ko < word_bits
 4. \<And>x5. ko = ArchObj x5 \<Longrightarrow> obj_bits ko < word_bits proof (state)
goal (4 subgoals):
 1. \<And>x2. ko = TCB x2 \<Longrightarrow> obj_bits ko < word_bits
 2. \<And>x3. ko = Endpoint x3 \<Longrightarrow> obj_bits ko < word_bits
 3. \<And>x4. ko = Notification x4 \<Longrightarrow> obj_bits ko < word_bits
 4. \<And>x5. ko = ArchObj x5 \<Longrightarrow> obj_bits ko < word_bits proof (state)
this:
ko = ArchObj ako

goal (4 subgoals):
 1. \<And>x2. ko = TCB x2 \<Longrightarrow> obj_bits ko < word_bits
 2. \<And>x3. ko = Endpoint x3 \<Longrightarrow> obj_bits ko < word_bits
 3. \<And>x4. ko = Notification x4 \<Longrightarrow> obj_bits ko < word_bits
 4. \<And>x5. ko = ArchObj x5 \<Longrightarrow> obj_bits ko < word_bits proof (prove)
goal (1 subgoal):
 1. obj_bits ko < word_bits proof (prove)
using this:
ko = ArchObj ako

goal (1 subgoal):
 1. obj_bits ko < word_bits proof (state)
this:
obj_bits ko < word_bits

goal (3 subgoals):
 1. \<And>x2. ko = TCB x2 \<Longrightarrow> obj_bits ko < word_bits
 2. \<And>x3. ko = Endpoint x3 \<Longrightarrow> obj_bits ko < word_bits
 3. \<And>x4. ko = Notification x4 \<Longrightarrow> obj_bits ko < word_bits
theory Invariants_AI

lemma valid_pspace_obj_sizes:
  assumes vp: "valid_pspace s"
  and     ko: "ko \<in> ran (kheap s)"
  shows   "obj_bits ko < word_bits" using assms by - (rule valid_obj_sizes, auto simp: valid_pspace_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_bits ko < word_bits proof (prove)
using this:
valid_pspace s
ko \<in> ran (kheap s)

goal (1 subgoal):
 1. obj_bits ko < word_bits
theory Invariants_AI

lemma valid_objs_replicate:
  assumes aligned: "pspace_aligned s"
  assumes valid: "valid_objs s"
  and     dom:   "x \<in> dom (kheap s)"
  shows   "to_bl x = (take (word_bits - (obj_bits (the (kheap s x)))) (to_bl x)) @
                     replicate (obj_bits (the (kheap s x))) False" proof - let ?a = "obj_bits (the (kheap s x))" from aligned have "is_aligned x ?a" using dom unfolding pspace_aligned_def .. thus ?thesis proof (rule is_aligned_replicate[where 'a=machine_word_len, folded word_bits_def]) show "obj_bits (the (kheap s x)) \<le> word_bits" by (rule order_less_imp_le, rule valid_obj_sizes [OF _ dom_ran]) fact+ qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl x = take (word_bits - obj_bits (the (kheap s x))) (to_bl x) @ replicate (obj_bits (the (kheap s x))) False proof (state)
goal (1 subgoal):
 1. to_bl x = take (word_bits - obj_bits (the (kheap s x))) (to_bl x) @ replicate (obj_bits (the (kheap s x))) False proof (state)
goal (1 subgoal):
 1. to_bl x = take (word_bits - obj_bits (the (kheap s x))) (to_bl x) @ replicate (obj_bits (the (kheap s x))) False proof (chain)
picking this:
pspace_aligned s proof (prove)
using this:
pspace_aligned s

goal (1 subgoal):
 1. is_aligned x (obj_bits (the (kheap s x))) proof (prove)
using this:
pspace_aligned s
x \<in> dom (kheap s)

goal (1 subgoal):
 1. is_aligned x (obj_bits (the (kheap s x))) proof (prove)
using this:
\<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x)))
x \<in> dom (kheap s)

goal (1 subgoal):
 1. is_aligned x (obj_bits (the (kheap s x))) proof (state)
this:
is_aligned x (obj_bits (the (kheap s x)))

goal (1 subgoal):
 1. to_bl x = take (word_bits - obj_bits (the (kheap s x))) (to_bl x) @ replicate (obj_bits (the (kheap s x))) False proof (prove)
using this:
is_aligned x (obj_bits (the (kheap s x)))

goal (1 subgoal):
 1. to_bl x = take (word_bits - obj_bits (the (kheap s x))) (to_bl x) @ replicate (obj_bits (the (kheap s x))) False proof (state)
goal (1 subgoal):
 1. obj_bits (the (kheap s x)) \<le> word_bits proof (prove)
goal (1 subgoal):
 1. obj_bits (the (kheap s x)) \<le> word_bits proof (state)
this:
obj_bits (the (kheap s x)) \<le> word_bits

goal:
No subgoals! proof (state)
this:
to_bl x = take (word_bits - obj_bits (the (kheap s x))) (to_bl x) @ replicate (obj_bits (the (kheap s x))) False

goal:
No subgoals!
theory Invariants_AI

lemma valid_pspace_replicate:
  assumes "valid_pspace s"
  and     "x \<in> dom (kheap s)"
  shows   "to_bl x = (take (word_bits - (obj_bits (the (kheap s x)))) (to_bl x)) @
                     replicate (obj_bits (the (kheap s x))) False" using assms by - (rule valid_objs_replicate, auto simp: valid_pspace_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl x = take (word_bits - obj_bits (the (kheap s x))) (to_bl x) @ replicate (obj_bits (the (kheap s x))) False proof (prove)
using this:
valid_pspace s
x \<in> dom (kheap s)

goal (1 subgoal):
 1. to_bl x = take (word_bits - obj_bits (the (kheap s x))) (to_bl x) @ replicate (obj_bits (the (kheap s x))) False
theory Invariants_AI

lemma valid_objs_captable_dom_length:
  assumes "valid_objs s"
  assumes "CNode sz ct \<in> ran (kheap s)"
  assumes ct: "ct y \<noteq> None"
  shows "length y < word_bits - cte_level_bits" proof - have "valid_cs_size sz ct" by (rule valid_objs_valid_cs_size) fact+ thus ?thesis using ct by (auto simp: valid_cs_size_def well_formed_cnode_n_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length y < word_bits - cte_level_bits proof (state)
goal (1 subgoal):
 1. length y < word_bits - cte_level_bits proof (prove)
goal (1 subgoal):
 1. valid_cs_size sz ct proof (state)
this:
valid_cs_size sz ct

goal (1 subgoal):
 1. length y < word_bits - cte_level_bits proof (prove)
using this:
valid_cs_size sz ct

goal (1 subgoal):
 1. length y < word_bits - cte_level_bits proof (prove)
using this:
valid_cs_size sz ct
ct y \<noteq> None

goal (1 subgoal):
 1. length y < word_bits - cte_level_bits proof (state)
this:
length y < word_bits - cte_level_bits

goal:
No subgoals!
theory Invariants_AI

lemma valid_pspace_captable_dom_length:
  assumes "valid_pspace s"
  and     "CNode sz ct \<in> ran (kheap s)"
  and     "ct y \<noteq> None"
  shows "length y < word_bits - cte_level_bits" using assms by - (rule valid_objs_captable_dom_length, auto simp: valid_pspace_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length y < word_bits - cte_level_bits proof (prove)
using this:
valid_pspace s
CNode sz ct \<in> ran (kheap s)
ct y \<noteq> None

goal (1 subgoal):
 1. length y < word_bits - cte_level_bits
theory Invariants_AI

lemma valid_objs_replicate':
  assumes valid: "valid_objs s"
  and   aligned: "pspace_aligned s"
  and     dom:   "x \<in> dom (kheap s)"
  and      l1:   "l1 = word_bits - (obj_bits (the (kheap s x)))"
  and      l2:   "l2 = (obj_bits (the (kheap s x)))"
  and      yv:   "y = (to_bl x)"
  shows   "to_bl x = (take l1 y) @ replicate l2 False" by ((subst l1 l2 yv)+, rule valid_objs_replicate) fact+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl x = take l1 y @ replicate l2 False
theory Invariants_AI

lemma valid_pspace_replicate':
  assumes valid: "valid_pspace s"
  and     dom:   "x \<in> dom (kheap s)"
  and      l1:   "l1 = word_bits - (obj_bits (the (kheap s x)))"
  and      l2:   "l2 = (obj_bits (the (kheap s x)))"
  and      yv:   "y = (to_bl x)"
  shows   "to_bl x = (take l1 y) @ replicate l2 False" by ((subst l1 l2 yv)+, rule valid_pspace_replicate) fact+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl x = take l1 y @ replicate l2 False
theory Invariants_AI

lemma pspace_replicate_dom:
  assumes "valid_pspace s"
  and pv: "kheap s (of_bl x) = Some (CNode sz ct)"
  shows   "replicate (obj_bits (CNode sz ct) - cte_level_bits) False \<in> dom ct" proof - have "valid_cs_size sz ct" by (rule valid_cs_sizeI) fact+ thus ?thesis by (rule valid_cs_sizeE) simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. replicate (obj_bits (CNode sz ct) - cte_level_bits) False \<in> dom ct proof (state)
goal (1 subgoal):
 1. replicate (obj_bits (CNode sz ct) - cte_level_bits) False \<in> dom ct proof (prove)
goal (1 subgoal):
 1. valid_cs_size sz ct proof (state)
this:
valid_cs_size sz ct

goal (1 subgoal):
 1. replicate (obj_bits (CNode sz ct) - cte_level_bits) False \<in> dom ct proof (prove)
using this:
valid_cs_size sz ct

goal (1 subgoal):
 1. replicate (obj_bits (CNode sz ct) - cte_level_bits) False \<in> dom ct proof (state)
this:
replicate (obj_bits (CNode sz ct) - cte_level_bits) False \<in> dom ct

goal:
No subgoals!
theory Invariants_AI

lemma obj_at_valid_objsE:
  "\<lbrakk> obj_at P p s; valid_objs s;
    \<And>ko. \<lbrakk> kheap s p = Some ko; P ko; valid_obj p ko s \<rbrakk> \<Longrightarrow> Q
  \<rbrakk> \<Longrightarrow> Q" by (auto simp: valid_objs_def obj_at_def dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at P p s; valid_objs s; \<And>ko. \<lbrakk>kheap s p = Some ko; P ko; valid_obj p ko s\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
theory Invariants_AI

lemma cap_table_at_cte_at:
  "\<lbrakk> cap_table_at cbits ptr s; length offset = cbits \<rbrakk>
  \<Longrightarrow> cte_at (ptr, offset) s" apply (clarsimp simp: obj_at_def cte_wp_at_cases is_cap_table
                        well_formed_cnode_n_def length_set_helper) apply (rule domD, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_table_at cbits ptr s; length offset = cbits\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (ptr, offset) s proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<lbrakk>cbits = length offset; kheap s ptr = Some (CNode (length offset) cs); dom cs = {x. length x = length offset}\<rbrakk> \<Longrightarrow> \<exists>cap. cs offset = Some cap proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma pred_tcb_weakenE:
  "\<lbrakk> pred_tcb_at proj P t s; \<And>tcb . P (proj tcb) \<Longrightarrow> P' (proj tcb) \<rbrakk> \<Longrightarrow> pred_tcb_at proj P' t s" by (auto simp: pred_tcb_at_def elim: obj_at_weakenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pred_tcb_at proj P t s; \<And>tcb. P (proj tcb) \<Longrightarrow> P' (proj tcb)\<rbrakk> \<Longrightarrow> pred_tcb_at proj P' t s
theory Invariants_AI

lemma pred_tcb_at_pure:
  "pred_tcb_at g (\<lambda>a. P) (f s) s = (tcb_at (f s) s \<and> P)" unfolding pred_tcb_at_def apply (clarsimp simp add: obj_at_def) apply (rule iffI) apply clarsimp apply (auto simp: is_tcb_def split: kernel_object.splits)[1] apply clarsimp apply (case_tac ko; simp_all) apply (auto simp: is_tcb_def split: kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pred_tcb_at g (\<lambda>a. P) (f s) s = (tcb_at (f s) s \<and> P) proof (prove)
goal (1 subgoal):
 1. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P) (f s) s = (tcb_at (f s) s \<and> P) proof (prove)
goal (1 subgoal):
 1. (\<exists>ko. kheap s (f s) = Some ko \<and> (\<exists>tcb. ko = TCB tcb) \<and> P) = ((\<exists>ko. kheap s (f s) = Some ko \<and> is_tcb ko) \<and> P) proof (prove)
goal (2 subgoals):
 1. \<exists>ko. kheap s (f s) = Some ko \<and> (\<exists>tcb. ko = TCB tcb) \<and> P \<Longrightarrow> (\<exists>ko. kheap s (f s) = Some ko \<and> is_tcb ko) \<and> P
 2. (\<exists>ko. kheap s (f s) = Some ko \<and> is_tcb ko) \<and> P \<Longrightarrow> \<exists>ko. kheap s (f s) = Some ko \<and> (\<exists>tcb. ko = TCB tcb) \<and> P proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>kheap s (f s) = Some (TCB tcb); P\<rbrakk> \<Longrightarrow> is_tcb (TCB tcb)
 2. (\<exists>ko. kheap s (f s) = Some ko \<and> is_tcb ko) \<and> P \<Longrightarrow> \<exists>ko. kheap s (f s) = Some ko \<and> (\<exists>tcb. ko = TCB tcb) \<and> P proof (prove)
goal (1 subgoal):
 1. (\<exists>ko. kheap s (f s) = Some ko \<and> is_tcb ko) \<and> P \<Longrightarrow> \<exists>ko. kheap s (f s) = Some ko \<and> (\<exists>tcb. ko = TCB tcb) \<and> P proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>P; kheap s (f s) = Some ko; is_tcb ko\<rbrakk> \<Longrightarrow> \<exists>tcb. ko = TCB tcb proof (prove)
goal (4 subgoals):
 1. \<And>ko x11 x12. \<lbrakk>P; kheap s (f s) = Some (CNode x11 x12); is_tcb (CNode x11 x12); ko = CNode x11 x12\<rbrakk> \<Longrightarrow> False
 2. \<And>ko x3. \<lbrakk>P; kheap s (f s) = Some (Endpoint x3); is_tcb (Endpoint x3); ko = Endpoint x3\<rbrakk> \<Longrightarrow> False
 3. \<And>ko x4. \<lbrakk>P; kheap s (f s) = Some (Notification x4); is_tcb (Notification x4); ko = Notification x4\<rbrakk> \<Longrightarrow> False
 4. \<And>ko x5. \<lbrakk>P; kheap s (f s) = Some (ArchObj x5); is_tcb (ArchObj x5); ko = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma st_tcb_weakenE:
  "\<lbrakk> st_tcb_at P t s; \<And>st . P st \<Longrightarrow> P' st \<rbrakk> \<Longrightarrow> st_tcb_at P' t s" by (auto simp: pred_tcb_weakenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at P t s; \<And>st. P st \<Longrightarrow> P' st\<rbrakk> \<Longrightarrow> st_tcb_at P' t s
theory Invariants_AI

lemma pred_tcb_at_tcb_at:
  "pred_tcb_at proj P t s \<Longrightarrow> tcb_at t s" by (auto simp: tcb_at_def pred_tcb_at_def obj_at_def is_tcb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pred_tcb_at proj P t s \<Longrightarrow> tcb_at t s
theory Invariants_AI

lemma st_tcb_at_opeqI:
  "\<lbrakk> st_tcb_at ((=) st) t s ; test st \<rbrakk> \<Longrightarrow> st_tcb_at test t s" by (fastforce simp add: pred_tcb_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at ((=) st) t s; test st\<rbrakk> \<Longrightarrow> st_tcb_at test t s
theory Invariants_AI

lemma cte_wp_at_weakenE:
  "\<lbrakk> cte_wp_at P t s; \<And>c. P c \<Longrightarrow> P' c \<rbrakk> \<Longrightarrow> cte_wp_at P' t s" by (simp add: cte_wp_at_def) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P t s; \<And>c. P c \<Longrightarrow> P' c\<rbrakk> \<Longrightarrow> cte_wp_at P' t s
theory Invariants_AI

lemma le_minus_minus:
  "\<lbrakk> a \<le> b - c; (c :: ('a :: len) word) \<le> b \<rbrakk> \<Longrightarrow> c \<le> b - a" by (simp add: word_le_nat_alt unat_sub)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b - c; c \<le> b\<rbrakk> \<Longrightarrow> c \<le> b - a
theory Invariants_AI

lemma tcb_at_cte_at:
  "\<lbrakk> tcb_at t s; ref \<in> dom tcb_cap_cases \<rbrakk> \<Longrightarrow> cte_at (t, ref) s" by (clarsimp simp: obj_at_def cte_wp_at_cases is_tcb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_at t s; ref \<in> dom tcb_cap_cases\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (t, ref) s
theory Invariants_AI

lemma cte_at_cases:
  "cte_at t s = ((\<exists>sz fun. kheap s (fst t) = Some (CNode sz fun) \<and>
                        well_formed_cnode_n sz fun \<and>
                        (snd t) \<in> dom fun) \<or>
                (\<exists>tcb. kheap s (fst t) = Some (TCB tcb) \<and>
                         (snd t \<in> dom tcb_cap_cases)))" by (auto simp add: cte_wp_at_cases dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>_. True) t s = ((\<exists>sz fun. kheap s (fst t) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> snd t \<in> dom fun) \<or> (\<exists>tcb. kheap s (fst t) = Some (TCB tcb) \<and> snd t \<in> dom tcb_cap_cases))
theory Invariants_AI

lemma cte_atE [consumes 1, case_names CNode TCB, elim?]:
  assumes cat: "cte_at t s"
  and     rct: "\<And>sz fun. \<lbrakk>kheap s (fst t) = Some (CNode sz fun); snd t \<in> dom fun\<rbrakk> \<Longrightarrow> R"
  and    rtcb: "\<And>tcb. \<lbrakk>kheap s (fst t) = Some (TCB tcb); snd t \<in> dom tcb_cap_cases \<rbrakk> \<Longrightarrow> R"
  shows "R" using cat by (auto simp: cte_at_cases intro: rct rtcb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R proof (prove)
using this:
cte_wp_at (\<lambda>_. True) t s

goal (1 subgoal):
 1. R
theory Invariants_AI

lemma cte_wp_at_cteI:
  "\<lbrakk>kheap s (fst t) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd t) = Some cte; P cte\<rbrakk>
  \<Longrightarrow> cte_wp_at P t s" by (auto simp: cte_wp_at_cases dom_def well_formed_cnode_n_def length_set_helper)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s (fst t) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd t) = Some cte; P cte\<rbrakk> \<Longrightarrow> cte_wp_at P t s
theory Invariants_AI

lemma cte_wp_at_tcbI:
  "\<lbrakk>kheap s (fst t) = Some (TCB tcb); tcb_cap_cases (snd t) = Some (getF, setF); P (getF tcb) \<rbrakk>
  \<Longrightarrow> cte_wp_at P t s" by (auto simp: cte_wp_at_cases dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s (fst t) = Some (TCB tcb); tcb_cap_cases (snd t) = Some (getF, setF); P (getF tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P t s
theory Invariants_AI

lemma ko_at_obj_congD:
  "\<lbrakk> ko_at k1 p s; ko_at k2 p s \<rbrakk> \<Longrightarrow> k1 = k2" unfolding obj_at_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at k1 p s; ko_at k2 p s\<rbrakk> \<Longrightarrow> k1 = k2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>ko. kheap s p = Some ko \<and> k1 = ko; \<exists>ko. kheap s p = Some ko \<and> k2 = ko\<rbrakk> \<Longrightarrow> k1 = k2
theory Invariants_AI

lemma not_obj_at_strengthen:
  "obj_at (Not \<circ> P) p s \<Longrightarrow> \<not> obj_at P p s" by (clarsimp simp: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at (Not \<circ> P) p s \<Longrightarrow> \<not> obj_at P p s
theory Invariants_AI

lemma not_pred_tcb_at_strengthen:
  "pred_tcb_at proj (Not \<circ> P) p s \<Longrightarrow> \<not> pred_tcb_at proj P p s" apply (simp add: pred_tcb_at_def) apply (strengthen not_obj_at_strengthen) apply (fastforce simp add: comp_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pred_tcb_at proj (Not \<circ> P) p s \<Longrightarrow> \<not> pred_tcb_at proj P p s proof (prove)
goal (1 subgoal):
 1. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb))) p s \<Longrightarrow> \<not> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (proj (tcb_to_itcb tcb))) p s proof (prove)
goal (1 subgoal):
 1. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> \<not> P (proj (tcb_to_itcb tcb))) p s \<Longrightarrow> obj_at (Not \<circ> (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (proj (tcb_to_itcb tcb)))) p s proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma valid_cte_at_typ:
  assumes P: "\<And>T p. \<lbrace>typ_at T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at T p\<rbrace>"
  shows      "\<lbrace>cte_at c\<rbrace> f \<lbrace>\<lambda>rv. cte_at c\<rbrace>" unfolding cte_at_typ apply (rule hoare_vcg_disj_lift [OF P]) apply (rule hoare_vcg_conj_lift [OF P]) apply (rule hoare_vcg_prop) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) c\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>_. True) c\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. typ_at (ACapTable (length (snd c))) (fst c) s \<or> typ_at ATCB (fst c) s \<and> snd c \<in> dom tcb_cap_cases\<rbrace> f \<lbrace>\<lambda>rv s. typ_at (ACapTable (length (snd c))) (fst c) s \<or> typ_at ATCB (fst c) s \<and> snd c \<in> dom tcb_cap_cases\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. typ_at ATCB (fst c) s \<and> snd c \<in> dom tcb_cap_cases\<rbrace> f \<lbrace>\<lambda>rv s. typ_at ATCB (fst c) s \<and> snd c \<in> dom tcb_cap_cases\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. snd c \<in> dom tcb_cap_cases\<rbrace> f \<lbrace>\<lambda>rv s. snd c \<in> dom tcb_cap_cases\<rbrace> proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma length_helper:
  "\<exists>y. length y = n" apply (rule_tac x="replicate n x" in exI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>y. length y = n proof (prove)
goal (1 subgoal):
 1. length (replicate n x) = n proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma pspace_typ_at:
  "kheap s p = Some obj \<Longrightarrow> \<exists>T. typ_at T p s" by (clarsimp simp: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s p = Some obj \<Longrightarrow> \<exists>T. typ_at T p s
theory Invariants_AI

lemma obj_bits_T:
  "obj_bits v = obj_bits_type (a_type v)" apply (cases v, simp_all add: obj_bits_type_def a_type_def) apply (rule aobj_bits_T) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_bits v = obj_bits_type (a_type v) proof (prove)
goal (1 subgoal):
 1. \<And>x5. v = ArchObj x5 \<Longrightarrow> arch_kobj_size x5 = arch_obj_bits_type (aa_type x5) proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma obj_range_T:
  "obj_range p v = typ_range p (a_type v)" by (simp add: obj_range_def typ_range_def obj_bits_T)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_range p v = typ_range p (a_type v)