kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_AI

lemma irq_state_independent_AI[intro!, simp]:
  "\<lbrakk>\<And>s f. P (s\<lparr>machine_state := machine_state s
              \<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) = P s\<rbrakk>
   \<Longrightarrow> irq_state_independent_A P" by (simp add: irq_state_independent_A_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s f. P (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) = P s) \<Longrightarrow> irq_state_independent_A P
theory CSpace_AI

lemma irq_state_independent_A_conjI[intro!]:
  "\<lbrakk>irq_state_independent_A P; irq_state_independent_A Q\<rbrakk>
   \<Longrightarrow> irq_state_independent_A (P and Q)"
  "\<lbrakk>irq_state_independent_A P; irq_state_independent_A Q\<rbrakk>
   \<Longrightarrow> irq_state_independent_A (\<lambda>s. P s \<and> Q s)" by (auto simp: irq_state_independent_A_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>irq_state_independent_A P; irq_state_independent_A Q\<rbrakk> \<Longrightarrow> irq_state_independent_A (P and Q)) &&& (\<lbrakk>irq_state_independent_A P; irq_state_independent_A Q\<rbrakk> \<Longrightarrow> irq_state_independent_A (\<lambda>s. P s \<and> Q s))
theory CSpace_AI

lemma gets_machine_state_modify:
  "do x \<leftarrow> gets machine_state;
       u \<leftarrow> modify (machine_state_update (\<lambda>y. x));
       f x
   od =
   gets machine_state >>= f" by (simp add: bind_def split_def simpler_gets_def simpler_modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- gets machine_state;
u <- modify (machine_state_update (\<lambda>y. x));
f x
od = gets machine_state >>= f
theory CSpace_AI

lemma OR_choiceE_weak_wp:
  "\<lbrace>P\<rbrace> f \<sqinter> g \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> OR_choiceE b f g \<lbrace>Q\<rbrace>" apply (fastforce simp add: OR_choiceE_def alternative_def valid_def bind_def
                    select_f_def gets_def return_def get_def liftE_def lift_def bindE_def
          split: option.splits if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<sqinter> g \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> OR_choiceE b f g \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma preemption_point_inv:
  fixes P :: "'state_ext state \<Rightarrow> bool"
  shows
    "\<lbrakk>irq_state_independent_A P; \<And>f s. P (trans_state f s) = P s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> preemption_point \<lbrace>\<lambda>_. P\<rbrace>" apply (intro impI conjI | simp add: preemption_point_def o_def
       | wp hoare_post_imp[OF _ getActiveIRQ_wp] OR_choiceE_weak_wp
       | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>irq_state_independent_A P; \<And>f s. P (trans_state f s) = P s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> preemption_point \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma get_cap_valid [wp]:
  "\<lbrace> valid_objs \<rbrace> get_cap addr \<lbrace> valid_cap \<rbrace>" apply (wp get_cap_wp) apply (auto dest: cte_wp_at_valid_objs_valid_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> get_cap addr \<lbrace>valid_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) addr s \<longrightarrow> s \<turnstile> cap proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma get_cap_wellformed:
  "\<lbrace>valid_objs\<rbrace> get_cap slot \<lbrace>\<lambda>cap s. wellformed_cap cap\<rbrace>" apply (rule hoare_strengthen_post, rule get_cap_valid) apply (simp add: valid_cap_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> get_cap slot \<lbrace>\<lambda>cap s. wellformed_cap cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. s \<turnstile> rv \<Longrightarrow> wellformed_cap rv proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma update_cdt_cdt:
  "\<lbrace>\<lambda>s. valid_mdb (cdt_update (\<lambda>_. (m (cdt s))) s)\<rbrace> update_cdt m \<lbrace>\<lambda>_. valid_mdb\<rbrace>" by (simp add: update_cdt_def set_cdt_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_mdb (s\<lparr>cdt := m (cdt s)\<rparr>)\<rbrace> update_cdt m \<lbrace>\<lambda>_. valid_mdb\<rbrace>
theory CSpace_AI

lemma unpleasant_helper:
  "(\<forall>a b. (\<exists>c. a = f c \<and> b = g c \<and> P c) \<longrightarrow> Q a b) = (\<forall>c. P c \<longrightarrow> Q (f c) (g c))" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>a b. (\<exists>c. a = f c \<and> b = g c \<and> P c) \<longrightarrow> Q a b) = (\<forall>c. P c \<longrightarrow> Q (f c) (g c))
theory CSpace_AI

lemma get_object_det:
  "(r,s') \<in> fst (get_object p s) \<Longrightarrow> get_object p s = ({(r,s)}, False)" by (auto simp: in_monad get_object_def bind_def gets_def get_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (r, s') \<in> fst (get_object p s) \<Longrightarrow> get_object p s = ({(r, s)}, False)
theory CSpace_AI

lemma get_object_at_obj:
  "\<lbrakk> (r,s') \<in> fst (get_object p s); P r \<rbrakk> \<Longrightarrow> obj_at P p s" by (auto simp: get_object_def obj_at_def in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(r, s') \<in> fst (get_object p s); P r\<rbrakk> \<Longrightarrow> obj_at P p s
theory CSpace_AI

lemma get_cap_cte_at:
  "(r,s') \<in> fst (get_cap p s) \<Longrightarrow> cte_at p s" unfolding cte_at_def by (auto dest: get_cap_det)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (r, s') \<in> fst (get_cap p s) \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (1 subgoal):
 1. (r, s') \<in> fst (get_cap p s) \<Longrightarrow> \<exists>cap. fst (get_cap p s) = {(cap, s)}
theory CSpace_AI

lemma resolve_address_bits_cte_at:
  "\<lbrace> valid_objs and valid_cap (fst args) \<rbrace>
  resolve_address_bits args
  \<lbrace>\<lambda>rv. cte_at (fst rv)\<rbrace>, -" apply (rule hoare_post_imp_R, rule resolve_address_bits_real_cte_at) apply (erule real_cte_at_cte) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_cap (fst args)\<rbrace> resolve_address_bits args \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>_. True) (fst rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>rv s. real_cte_at (fst rv) s \<Longrightarrow> cte_wp_at (\<lambda>_. True) (fst rv) s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma lookup_slot_real_cte_at_wp [wp]:
  "\<lbrace> valid_objs \<rbrace> lookup_slot_for_thread t addr \<lbrace>\<lambda>rv. real_cte_at (fst rv)\<rbrace>,-" apply (simp add: lookup_slot_for_thread_def) apply wp apply (rule resolve_address_bits_real_cte_at) apply simp apply wp apply clarsimp apply (erule(1) objs_valid_tcb_ctable) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_slot_for_thread t addr \<lbrace>\<lambda>rv. real_cte_at (fst rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> doE tcb <- liftE (gets_the (get_tcb t));
resolve_address_bits (tcb_ctable tcb, addr)
odE \<lbrace>\<lambda>rv. real_cte_at (fst rv)\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> resolve_address_bits (tcb_ctable tcb, addr) \<lbrace>\<lambda>rv. real_cte_at (fst rv)\<rbrace>, -
 2. \<lbrace>?P'\<rbrace> liftE (gets_the (get_tcb t)) \<lbrace>?B1\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. valid_objs s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> liftE (gets_the (get_tcb t)) \<lbrace>\<lambda>tcb. valid_objs and valid_cap (fst (tcb_ctable tcb, addr))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. valid_objs s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>tcb. valid_objs and valid_cap (tcb_ctable tcb)\<rbrace>
 2. \<And>s. valid_objs s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (valid_objs and valid_cap (tcb_ctable (the (get_tcb t s)))) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>valid_objs s; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_ctable y proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma lookup_slot_cte_at_wp[wp]:
  "\<lbrace> valid_objs \<rbrace> lookup_slot_for_thread t addr \<lbrace>\<lambda>rv. cte_at (fst rv)\<rbrace>,-" by (strengthen real_cte_at_cte, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_slot_for_thread t addr \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>_. True) (fst rv)\<rbrace>, -
theory CSpace_AI

lemma len_drop_lemma:
  assumes drop: "drop (n - length ys) xs = ys"
  assumes l: "n = length xs"
  shows "length ys \<le> n" proof - from drop have "length (drop (n - length ys) xs) = length ys" by simp with l have "length ys = n - (n - length ys)" by simp thus ?thesis by arith qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length ys \<le> n proof (state)
goal (1 subgoal):
 1. length ys \<le> n proof (chain)
picking this:
drop (n - length ys) xs = ys proof (prove)
using this:
drop (n - length ys) xs = ys

goal (1 subgoal):
 1. length (drop (n - length ys) xs) = length ys proof (state)
this:
length (drop (n - length ys) xs) = length ys

goal (1 subgoal):
 1. length ys \<le> n proof (chain)
picking this:
n = length xs
length (drop (n - length ys) xs) = length ys proof (prove)
using this:
n = length xs
length (drop (n - length ys) xs) = length ys

goal (1 subgoal):
 1. length ys = n - (n - length ys) proof (state)
this:
length ys = n - (n - length ys)

goal (1 subgoal):
 1. length ys \<le> n proof (prove)
using this:
length ys = n - (n - length ys)

goal (1 subgoal):
 1. length ys \<le> n proof (state)
this:
length ys \<le> n

goal:
No subgoals!
theory CSpace_AI

lemma drop_postfix_eq:
  "n = length xs \<Longrightarrow> (drop (n - length ys) xs = ys) = (\<exists>zs. xs = zs @ ys)" by (auto dest: drop_postfixD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n = length xs \<Longrightarrow> (drop (n - length ys) xs = ys) = (\<exists>zs. xs = zs @ ys)
theory CSpace_AI

lemma postfix_dropD:
  "xs = zs @ ys \<Longrightarrow> drop (length xs - length ys) xs = ys" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xs = zs @ ys \<Longrightarrow> drop (length xs - length ys) xs = ys
theory CSpace_AI

lemma of_bl_take:
  "length xs < len_of TYPE('a) \<Longrightarrow> of_bl (take n xs) = ((of_bl xs) >> (length xs - n) :: ('a :: len) word)" apply (clarsimp simp: bang_eq and_bang test_bit_of_bl
                        rev_take conj_comms nth_shiftr) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs < LENGTH('a) \<Longrightarrow> of_bl (take n xs) = of_bl xs >> length xs - n proof (prove)
goal (1 subgoal):
 1. \<And>na. length xs < LENGTH('a) \<Longrightarrow> (na < n \<and> na < length xs \<and> na < LENGTH('a) \<and> rev xs ! (length xs - n + na)) = (rev xs ! (length xs - n + na) \<and> length xs - n + na < length xs \<and> length xs - n + na < LENGTH('a)) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma gets_the_tcb_get_cap:
  "tcb_at t s \<Longrightarrow> liftM tcb_ctable (gets_the (get_tcb t)) s = get_cap (t, tcb_cnode_index 0) s" apply (clarsimp simp add: tcb_at_def liftM_def bind_def assert_opt_def
                            gets_the_def simpler_gets_def return_def) apply (clarsimp    dest!: get_tcb_SomeD
                  simp add: get_cap_def tcb_cnode_map_def
                            get_object_def bind_def simpler_gets_def
                            return_def assert_def fail_def assert_opt_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at t s \<Longrightarrow> liftM tcb_ctable (gets_the (get_tcb t)) s = get_cap (t, tcb_cnode_index 0) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. get_tcb t s = Some tcb \<Longrightarrow> ({(tcb_ctable tcb, s)}, False) = get_cap (t, tcb_cnode_index 0) s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma upd_other_cte_wp_at:
  "\<lbrakk> cte_wp_at P p s; fst p \<noteq> ptr \<rbrakk> \<Longrightarrow>
  cte_wp_at P p (kheap_update (\<lambda>ps. (kheap s)(ptr \<mapsto> ko)) s)" by (auto elim!: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P p s; fst p \<noteq> ptr\<rbrakk> \<Longrightarrow> cte_wp_at P p (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ko)\<rparr>)
theory CSpace_AI

lemma get_cap_cte_wp_at:
  "\<lbrace>\<top>\<rbrace> get_cap p \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = rv) p\<rbrace>" apply (wp get_cap_wp) apply (clarsimp elim!: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_cap p \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = rv) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) p s \<longrightarrow> cte_wp_at (\<lambda>c. c = cap) p s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma get_cap_sp:
  "\<lbrace>P\<rbrace> get_cap p \<lbrace>\<lambda>rv. P and cte_wp_at (\<lambda>c. c = rv) p\<rbrace>" by (wp get_cap_cte_wp_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_cap p \<lbrace>\<lambda>rv. P and cte_wp_at (\<lambda>c. c = rv) p\<rbrace>
theory CSpace_AI

lemma wf_cs_nD:
  "\<lbrakk> f x = Some y; well_formed_cnode_n n f \<rbrakk> \<Longrightarrow> length x = n" unfolding well_formed_cnode_n_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f x = Some y; well_formed_cnode_n n f\<rbrakk> \<Longrightarrow> length x = n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f x = Some y; dom f = {x. length x = n}\<rbrakk> \<Longrightarrow> length x = n
theory CSpace_AI

lemma set_cdt_valid_pspace:
  "\<lbrace>valid_pspace\<rbrace> set_cdt m \<lbrace>\<lambda>_. valid_pspace\<rbrace>" unfolding set_cdt_def apply simp apply wp apply (erule valid_pspace_eqI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace\<rbrace> set_cdt m \<lbrace>\<lambda>_. valid_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace\<rbrace> do s <- get;
put $ s\<lparr>cdt := m\<rparr>
od \<lbrace>\<lambda>_. valid_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace\<rbrace> do s <- get;
put (s\<lparr>cdt := m\<rparr>)
od \<lbrace>\<lambda>_. valid_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_pspace s \<Longrightarrow> valid_pspace (s\<lparr>cdt := m\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. kheap s = kheap (s\<lparr>cdt := m\<rparr>) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma cte_at_pspace:
  "cte_wp_at P p s \<Longrightarrow> \<exists>ko. kheap s (fst p) = Some ko" by (auto simp: cte_wp_at_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at P p s \<Longrightarrow> \<exists>ko. kheap s (fst p) = Some ko
theory CSpace_AI

lemma tcb_cap_cases_length:
  "x \<in> dom tcb_cap_cases \<Longrightarrow> length x = 3" by (auto simp add: tcb_cap_cases_def tcb_cnode_index_def to_bl_1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> dom tcb_cap_cases \<Longrightarrow> length x = 3
theory CSpace_AI

lemma well_formed_cnode_invsI:
  "\<lbrakk> valid_objs s; kheap s x = Some (CNode sz cs) \<rbrakk>
      \<Longrightarrow> well_formed_cnode_n sz cs" apply (erule(1) valid_objsE) apply (clarsimp simp: well_formed_cnode_n_def valid_obj_def valid_cs_def valid_cs_size_def
                        length_set_helper) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; kheap s x = Some (CNode sz cs)\<rbrakk> \<Longrightarrow> well_formed_cnode_n sz cs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = Some (CNode sz cs); valid_obj x (CNode sz cs) s\<rbrakk> \<Longrightarrow> well_formed_cnode_n sz cs proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma set_cap_cte_eq:
  "(x,t) \<in> fst (set_cap c p' s) \<Longrightarrow>
  cte_at p' s \<and> cte_wp_at P p t = (if p = p' then P c else cte_wp_at P p s)" apply (cases p) apply (cases p') apply (auto simp: set_cap_def2 split_def in_monad cte_wp_at_cases
                    get_object_def set_object_def wf_cs_upd
             split: Structures_A.kernel_object.splits if_split_asm
                    option.splits,
         auto simp: tcb_cap_cases_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, t) \<in> fst (set_cap c p' s) \<Longrightarrow> cte_wp_at (\<lambda>_. True) p' s \<and> cte_wp_at P p t = (if p = p' then P c else cte_wp_at P p s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(x, t) \<in> fst (set_cap c p' s); p = (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p' s \<and> cte_wp_at P p t = (if p = p' then P c else cte_wp_at P p s) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>(x, t) \<in> fst (set_cap c p' s); p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p' s \<and> cte_wp_at P p t = (if p = p' then P c else cte_wp_at P p s) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma descendants_of_cte_at:
  "\<lbrakk> p \<in> descendants_of x (cdt s); valid_mdb s \<rbrakk>
  \<Longrightarrow> cte_at p s" apply (simp add: descendants_of_def) apply (drule tranclD2) apply (clarsimp simp: cdt_parent_defs valid_mdb_def mdb_cte_at_def
                  simp del: split_paired_All) apply (fastforce elim: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> descendants_of x (cdt s); valid_mdb s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdt s \<Turnstile> x \<rightarrow> p; valid_mdb s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; \<exists>z. cdt s \<Turnstile> x \<rightarrow>* z \<and> cdt s \<Turnstile> z \<leadsto> p\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>p c. cdt s c = Some p \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) p s \<and> cte_wp_at ((\<noteq>) NullCap) c s; (x, a, b) \<in> {(p, c). cdt s c = Some p}\<^sup>*; cdt s p = Some (a, b); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma descendants_of_cte_at2:
  "\<lbrakk> p \<in> descendants_of x (cdt s); valid_mdb s \<rbrakk>
  \<Longrightarrow> cte_at x s" apply (simp add: descendants_of_def) apply (drule tranclD) apply (clarsimp simp: cdt_parent_defs valid_mdb_def mdb_cte_at_def
                  simp del: split_paired_All) apply (fastforce elim: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> descendants_of x (cdt s); valid_mdb s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) x s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdt s \<Turnstile> x \<rightarrow> p; valid_mdb s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) x s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; \<exists>z. cdt s \<Turnstile> x \<leadsto> z \<and> cdt s \<Turnstile> z \<rightarrow>* p\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) x s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>p c. cdt s c = Some p \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) p s \<and> cte_wp_at ((\<noteq>) NullCap) c s; cdt s (a, b) = Some x; ((a, b), p) \<in> {(p, c). cdt s c = Some p}\<^sup>*; untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) x s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma in_set_cap_cte_at:
  "(x, s') \<in> fst (set_cap c p' s) \<Longrightarrow> cte_at p s' = cte_at p s" by (fastforce simp: cte_at_cases set_cap_def split_def wf_cs_upd
                     in_monad get_object_def set_object_def
               split: Structures_A.kernel_object.splits if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, s') \<in> fst (set_cap c p' s) \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s' = cte_wp_at (\<lambda>_. True) p s
theory CSpace_AI

lemma in_set_cap_cte_at_swp:
  "(x, s') \<in> fst (set_cap c p' s) \<Longrightarrow> swp cte_at s' = swp cte_at s" by (simp add: swp_def in_set_cap_cte_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, s') \<in> fst (set_cap c p' s) \<Longrightarrow> swp (cte_wp_at (\<lambda>_. True)) s' = swp (cte_wp_at (\<lambda>_. True)) s
theory CSpace_AI

lemma take_to_bl_len:
  fixes a :: "'a::len word"
  fixes b :: "'a::len word"
  assumes t: "take x (to_bl a) = take y (to_bl b)"
  assumes x: "x \<le> size a"
  assumes y: "y \<le> size b"
  shows "x = y" proof - from t have "length (take x (to_bl a)) = length (take y (to_bl b))" by simp also from x have "length (take x (to_bl a)) = x" by (simp add: word_size) also from y have "length (take y (to_bl b)) = y" by (simp add: word_size) finally show ?thesis . qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x = y proof (state)
goal (1 subgoal):
 1. x = y proof (chain)
picking this:
take x (to_bl a) = take y (to_bl b) proof (prove)
using this:
take x (to_bl a) = take y (to_bl b)

goal (1 subgoal):
 1. length (take x (to_bl a)) = length (take y (to_bl b)) proof (state)
this:
length (take x (to_bl a)) = length (take y (to_bl b))

goal (1 subgoal):
 1. x = y proof (state)
this:
length (take x (to_bl a)) = length (take y (to_bl b))

goal (1 subgoal):
 1. x = y proof (chain)
picking this:
x \<le> size a proof (prove)
using this:
x \<le> size a

goal (1 subgoal):
 1. length (take x (to_bl a)) = x proof (state)
this:
length (take x (to_bl a)) = x

goal (1 subgoal):
 1. x = y proof (state)
this:
length (take x (to_bl a)) = x

goal (1 subgoal):
 1. x = y proof (chain)
picking this:
y \<le> size b proof (prove)
using this:
y \<le> size b

goal (1 subgoal):
 1. length (take y (to_bl b)) = y proof (state)
this:
length (take y (to_bl b)) = y

goal (1 subgoal):
 1. x = y proof (chain)
picking this:
x = y proof (prove)
using this:
x = y

goal (1 subgoal):
 1. x = y proof (state)
this:
x = y

goal:
No subgoals!