kings-crown/FVELER_Isabelle huggingface dataset:
theory Untyped_AI

lemma cte_wp_at_wellformed_strengthen:
  "cte_at p s \<and> valid_objs s \<longrightarrow> cte_wp_at wellformed_cap p s" apply (clarsimp simp: cte_wp_at_caps_of_state) apply (frule (1) caps_of_state_valid_cap) apply (simp add: valid_cap_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>_. True) p s \<and> valid_objs s \<longrightarrow> cte_wp_at wellformed_cap p s proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>valid_objs s; caps_of_state s p = Some cap\<rbrakk> \<Longrightarrow> wellformed_cap cap proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>valid_objs s; caps_of_state s p = Some cap; s \<turnstile> cap\<rbrakk> \<Longrightarrow> wellformed_cap cap proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma get_cap_cte_wp_at_P:
  "\<lbrace>cte_wp_at P p\<rbrace> get_cap p \<lbrace>\<lambda>rv s. cte_wp_at (%c. c = rv) p s \<and> P rv\<rbrace>" apply (rule hoare_weaken_pre) apply (rule get_cap_wp) apply (clarsimp simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P p\<rbrace> get_cap p \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. c = rv) p s \<and> P rv\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_cap p \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. c = rv) p s \<and> P rv\<rbrace>
 2. \<And>s. cte_wp_at P p s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at P p s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) p s \<longrightarrow> cte_wp_at (\<lambda>c. c = cap) p s \<and> P cap proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma is_cnode_mask:
  "is_cnode_cap (mask_cap m c) = is_cnode_cap c" by (case_tac c, simp_all add: mask_cap_def cap_rights_update_def is_cap_simps split:bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_cnode_cap (mask_cap m c) = is_cnode_cap c
theory Untyped_AI

lemma Suc_length_not_empty:
  "length xs = length xs' \<Longrightarrow> Suc 0 \<le> length xs' = (xs \<noteq> [])" by (fastforce simp: le_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs = length xs' \<Longrightarrow> (Suc 0 \<le> length xs') = (xs \<noteq> [])
theory Untyped_AI

lemma caps_of_state_valid:
  "\<lbrakk>invs s; caps_of_state s p = Some cap \<rbrakk> \<Longrightarrow> s \<turnstile> cap" apply (rule cte_wp_valid_cap) apply (simp add: cte_wp_at_caps_of_state) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; caps_of_state s p = Some cap\<rbrakk> \<Longrightarrow> s \<turnstile> cap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; caps_of_state s p = Some cap\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) ?p s
 2. \<lbrakk>invs s; caps_of_state s p = Some cap\<rbrakk> \<Longrightarrow> valid_objs s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; caps_of_state s p = Some cap\<rbrakk> \<Longrightarrow> valid_objs s proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma mask_CNodeD:
  "mask_cap M' cap = cap.CNodeCap r bits g \<Longrightarrow>
  cap = cap.CNodeCap r bits g" by (cases cap, auto simp: mask_cap_def cap_rights_update_def split:bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mask_cap M' cap = CNodeCap r bits g \<Longrightarrow> cap = CNodeCap r bits g
theory Untyped_AI

lemma unat_2p_sub_1:
  "k < len_of TYPE('a)
  \<Longrightarrow> unat (2 ^ k - 1 :: 'a :: len word) = unat (2 ^ k :: 'a word) - 1" by (simp add: unat_minus_one)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. k < LENGTH('a) \<Longrightarrow> unat (2 ^ k - 1) = unat (2 ^ k) - 1
theory Untyped_AI

lemma compute_free_index_wp:
  "\<lbrace>\<top>\<rbrace> const_on_failure idx
   (doE y \<leftarrow> ensure_no_children slot;
        returnOk (0::nat)
    odE)
   \<lbrace>\<lambda>rv s. rv \<le> idx\<rbrace>" apply (rule hoare_pre) apply (wp const_on_failure_wp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> const_on_failure idx (doE y <- ensure_no_children slot;
returnOk 0
odE) \<lbrace>\<lambda>rv s. rv \<le> idx\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> const_on_failure idx (doE y <- ensure_no_children slot;
returnOk 0
odE) \<lbrace>\<lambda>rv s. rv \<le> idx\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> idx \<le> idx \<and> True \<and> 0 \<le> idx proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma map_ensure_empty_cte_wp_at:
  "\<lbrace>cte_wp_at P p\<rbrace> mapME_x ensure_empty xs \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace>,-" unfolding mapME_x_def sequenceE_x_def by (induct xs; wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P p\<rbrace> mapME_x ensure_empty xs \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P p\<rbrace> foldr (\<lambda>x y. doE _ <- x;
y
odE) (map ensure_empty xs) (returnOk ()) \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace>, -
theory Untyped_AI

lemma ensure_no_children_sp:
  "\<lbrace>P\<rbrace> ensure_no_children slot \<lbrace>\<lambda>rv s. descendants_of slot (cdt s) = {} \<and> P s\<rbrace>,-" apply (simp add: ensure_no_children_descendants) apply (clarsimp simp: valid_def validE_def validE_R_def split_def in_monad
                        | rule conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> ensure_no_children slot \<lbrace>\<lambda>rv s. descendants_of slot (cdt s) = {} \<and> P s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> \<lambda>s. if descendants_of slot (cdt s) = {} then returnOk () s else throwError RevokeFirst s \<lbrace>\<lambda>rv s. descendants_of slot (cdt s) = {} \<and> P s\<rbrace>, - proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma data_to_obj_type_inv:
  "\<lbrace>P\<rbrace> data_to_obj_type v \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: data_to_obj_type_def) apply (intro conjI impI; wpsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> data_to_obj_type v \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. (data_to_nat v = 4 \<longrightarrow> \<lbrace>P\<rbrace> returnOk CapTableObject \<lbrace>\<lambda>rv. P\<rbrace>) \<and> (data_to_nat v \<noteq> 4 \<longrightarrow> (data_to_nat v = 3 \<longrightarrow> \<lbrace>P\<rbrace> returnOk NotificationObject \<lbrace>\<lambda>rv. P\<rbrace>) \<and> (data_to_nat v \<noteq> 3 \<longrightarrow> (data_to_nat v = 2 \<longrightarrow> \<lbrace>P\<rbrace> returnOk EndpointObject \<lbrace>\<lambda>rv. P\<rbrace>) \<and> (data_to_nat v \<noteq> 2 \<longrightarrow> (data_to_nat v = Suc 0 \<longrightarrow> \<lbrace>P\<rbrace> returnOk TCBObject \<lbrace>\<lambda>rv. P\<rbrace>) \<and> (data_to_nat v \<noteq> Suc 0 \<longrightarrow> (data_to_nat v = 0 \<longrightarrow> \<lbrace>P\<rbrace> returnOk Untyped \<lbrace>\<lambda>rv. P\<rbrace>) \<and> (0 < data_to_nat v \<longrightarrow> \<lbrace>P\<rbrace> case arch_data_to_obj_type (data_to_nat v - 5) of None \<Rightarrow> throwError (InvalidArgument 0) | Some tp \<Rightarrow> returnOk (ArchObject tp) \<lbrace>\<lambda>rv. P\<rbrace>))))) proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma data_to_obj_type_inv2 [wp]:
  "\<lbrace>P\<rbrace> data_to_obj_type v \<lbrace>\<lambda>rv. P\<rbrace>,-" by (wp data_to_obj_type_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> data_to_obj_type v \<lbrace>\<lambda>rv. P\<rbrace>, -
theory Untyped_AI

lemma get_cap_gets:
  "\<lbrace>valid_objs\<rbrace>
    get_cap ptr
   \<lbrace>\<lambda>rv s. \<exists>cref msk. cte_wp_at (\<lambda>cap. rv = mask_cap msk cap) cref s\<rbrace>" apply (wp get_cap_wp) apply (intro allI impI) apply (rule_tac x=ptr in exI) apply (rule_tac x=UNIV in exI) apply (simp add: cte_wp_at_caps_of_state) apply (frule (1) caps_of_state_valid_cap) apply (clarsimp simp add: valid_cap_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> get_cap ptr \<lbrace>\<lambda>rv s. \<exists>cref msk. cte_wp_at (\<lambda>cap. rv = mask_cap msk cap) cref s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) ptr s \<longrightarrow> (\<exists>cref msk. cte_wp_at (\<lambda>capa. cap = mask_cap msk capa) cref s) proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>valid_objs s; cte_wp_at ((=) cap) ptr s\<rbrakk> \<Longrightarrow> \<exists>cref msk. cte_wp_at (\<lambda>capa. cap = mask_cap msk capa) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>valid_objs s; cte_wp_at ((=) cap) ptr s\<rbrakk> \<Longrightarrow> \<exists>msk. cte_wp_at (\<lambda>capa. cap = mask_cap msk capa) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>valid_objs s; cte_wp_at ((=) cap) ptr s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>capa. cap = mask_cap UNIV capa) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>valid_objs s; caps_of_state s ptr = Some cap\<rbrakk> \<Longrightarrow> cap = mask_cap UNIV cap proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>valid_objs s; caps_of_state s ptr = Some cap; s \<turnstile> cap\<rbrakk> \<Longrightarrow> cap = mask_cap UNIV cap proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma strengthen_imp_ex2: "(P \<longrightarrow> Q x y) \<Longrightarrow> (P \<longrightarrow> (\<exists>x y. Q x y))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P \<longrightarrow> Q x y \<Longrightarrow> P \<longrightarrow> (\<exists>x y. Q x y)
theory Untyped_AI

lemma p2_minus:
  "sz < len_of TYPE('a) \<Longrightarrow>
   of_nat (2 ^ len_of TYPE('a) - 2 ^ sz) = ((mask (len_of TYPE('a)) && ~~ mask sz):: 'a :: len word)" apply (rule word_unat.Rep_inverse') apply (simp add: mask_out_sub_mask) apply (simp add: unat_sub word_and_le2 mask_and_mask) apply (simp add: min_def mask_def word_size unat_minus) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> word_of_nat (2 ^ LENGTH('a) - 2 ^ sz) = mask LENGTH('a) && ~~ mask sz proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> unat (mask LENGTH('a) && ~~ mask sz) = 2 ^ LENGTH('a) - 2 ^ sz proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> unat (- 1 - mask sz) = 2 ^ LENGTH('a) - 2 ^ sz proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> unat (- 1) - unat (mask sz) = 2 ^ LENGTH('a) - 2 ^ sz proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma le_mask_le_2p:
  "\<lbrakk>idx \<le> unat ((ptr::machine_word) && mask sz);sz < word_bits\<rbrakk> \<Longrightarrow> idx < 2^ sz" apply (erule le_less_trans) apply (rule unat_less_helper) apply simp apply (rule le_less_trans) apply (rule word_and_le1) apply (simp add: mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> unat (ptr && mask sz); sz < word_bits\<rbrakk> \<Longrightarrow> idx < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. sz < word_bits \<Longrightarrow> unat (ptr && mask sz) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. sz < word_bits \<Longrightarrow> ptr && mask sz < word_of_nat (2 ^ sz) proof (prove)
goal (1 subgoal):
 1. sz < word_bits \<Longrightarrow> ptr && mask sz < 2 ^ sz proof (prove)
goal (2 subgoals):
 1. sz < word_bits \<Longrightarrow> ptr && mask sz \<le> ?y4
 2. sz < word_bits \<Longrightarrow> ?y4 < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. sz < word_bits \<Longrightarrow> mask sz < 2 ^ sz proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma diff_neg_mask[simp]:
  "ptr - (ptr && ~~ mask sz) = (ptr && mask sz)" apply (subst word_plus_and_or_coroll2[symmetric,where w = "mask sz" and t = ptr]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr - (ptr && ~~ mask sz) = ptr && mask sz proof (prove)
goal (1 subgoal):
 1. (ptr && mask sz) + (ptr && ~~ mask sz) - (ptr && ~~ mask sz) = ptr && mask sz proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma check_children_wp:
  "\<lbrace>\<lambda>s. if descendants_of slot (cdt s) = {} then Q True s else Q False s \<rbrace>
   const_on_failure False
    (doE y \<leftarrow> ensure_no_children slot;
    returnOk True
    odE) \<lbrace>Q\<rbrace>" including no_pre apply (clarsimp simp: const_on_failure_def ensure_no_children_descendants bindE_assoc) apply wp apply (clarsimp simp: valid_def validE_def if_splits) apply (intro conjI impI) apply (clarsimp simp: in_monad free_index_of_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if descendants_of slot (cdt s) = {} then Q True s else Q False s\<rbrace> const_on_failure False (doE y <- ensure_no_children slot;
returnOk True
odE) \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if descendants_of slot (cdt s) = {} then Q True s else Q False s\<rbrace> const_on_failure False (doE y <- ensure_no_children slot;
returnOk True
odE) \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (descendants_of slot (cdt s) = {} \<longrightarrow> Q True s) \<and> (descendants_of slot (cdt s) \<noteq> {} \<longrightarrow> Q False s)\<rbrace> doE y <- \<lambda>s. if descendants_of slot (cdt s) = {} then returnOk () s else throwError RevokeFirst s;
returnOk True
odE <catch> (\<lambda>x. return False) \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (descendants_of slot (cdt s) = {} \<longrightarrow> Q True s) \<and> (descendants_of slot (cdt s) \<noteq> {} \<longrightarrow> Q False s)\<rbrace> \<lambda>s. if descendants_of slot (cdt s) = {} then returnOk () s else throwError RevokeFirst s \<lbrace>\<lambda>y. Q True\<rbrace>, \<lbrace>\<lambda>x. Q False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (descendants_of slot (cdt s) = {} \<longrightarrow> Q True s \<longrightarrow> (\<forall>x\<in>fst (returnOk () s). case x of (Inl e, s') \<Rightarrow> Q False s' | (Inr ra, s') \<Rightarrow> Q True s')) \<and> (descendants_of slot (cdt s) \<noteq> {} \<longrightarrow> Q False s \<longrightarrow> (\<forall>x\<in>fst (throwError RevokeFirst s). case x of (Inl e, s') \<Rightarrow> Q False s' | (Inr ra, s') \<Rightarrow> Q True s')) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>descendants_of slot (cdt s) = {}; Q True s\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (returnOk () s). case x of (Inl e, s') \<Rightarrow> Q False s' | (Inr ra, s') \<Rightarrow> Q True s'
 2. \<And>s. \<lbrakk>descendants_of slot (cdt s) \<noteq> {}; Q False s\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (throwError RevokeFirst s). case x of (Inl e, s') \<Rightarrow> Q False s' | (Inr ra, s') \<Rightarrow> Q True s' proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma alignUp_eq:
  "\<lbrakk>is_aligned (w :: 'a :: len word) sz; a \<le> 2^ sz; us \<le> sz; sz < len_of TYPE('a);
    alignUp (w + a) us = w\<rbrakk>
   \<Longrightarrow> a = 0" apply (clarsimp simp: alignUp_plus[OF is_aligned_weaken]) apply (rule ccontr) apply (drule alignUp_is_aligned_nz[rotated -1,where x = "2^ sz"]) apply (rule is_aligned_weaken[OF is_aligned_triv2]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned w sz; a \<le> 2 ^ sz; us \<le> sz; sz < LENGTH('a); alignUp (w + a) us = w\<rbrakk> \<Longrightarrow> a = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned w sz; a \<le> 2 ^ sz; us \<le> sz; sz < LENGTH('a); alignUp a us = 0\<rbrakk> \<Longrightarrow> a = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned w sz; a \<le> 2 ^ sz; us \<le> sz; sz < LENGTH('a); alignUp a us = 0; a \<noteq> 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned w sz; a \<le> 2 ^ sz; us \<le> sz; sz < LENGTH('a); alignUp a us = 0\<rbrakk> \<Longrightarrow> is_aligned (2 ^ sz) ?n5
 2. \<lbrakk>is_aligned w sz; a \<le> 2 ^ sz; us \<le> sz; sz < LENGTH('a); alignUp a us = 0\<rbrakk> \<Longrightarrow> ?n5 < LENGTH('a)
 3. \<lbrakk>is_aligned w sz; a \<le> 2 ^ sz; us \<le> sz; sz < LENGTH('a); alignUp a us = 0\<rbrakk> \<Longrightarrow> a \<le> 2 ^ sz
 4. \<lbrakk>is_aligned w sz; a \<le> 2 ^ sz; us \<le> sz; sz < LENGTH('a); alignUp a us = 0; alignUp a ?n5 \<noteq> 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned w sz; a \<le> 2 ^ sz; us \<le> sz; sz < LENGTH('a); alignUp a us = 0\<rbrakk> \<Longrightarrow> ?n5 \<le> sz
 2. \<lbrakk>is_aligned w sz; a \<le> 2 ^ sz; us \<le> sz; sz < LENGTH('a); alignUp a us = 0\<rbrakk> \<Longrightarrow> ?n5 < LENGTH('a)
 3. \<lbrakk>is_aligned w sz; a \<le> 2 ^ sz; us \<le> sz; sz < LENGTH('a); alignUp a us = 0\<rbrakk> \<Longrightarrow> a \<le> 2 ^ sz
 4. \<lbrakk>is_aligned w sz; a \<le> 2 ^ sz; us \<le> sz; sz < LENGTH('a); alignUp a us = 0; alignUp a ?n5 \<noteq> 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma map_ensure_empty_wp:
  "\<lbrace> \<lambda>s. (\<forall>x\<in>set xs. cte_wp_at ((=) NullCap) x s) \<longrightarrow> P () s \<rbrace>
      mapME_x ensure_empty xs \<lbrace>P\<rbrace>, -" by (rule hoare_post_imp_R, rule map_ensure_empty, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>x\<in>set xs. cte_wp_at ((=) NullCap) x s) \<longrightarrow> P () s\<rbrace> mapME_x ensure_empty xs \<lbrace>P\<rbrace>, -
theory Untyped_AI

lemma cases_imp_eq:
  "((P \<longrightarrow> Q \<longrightarrow> R) \<and> (\<not> P \<longrightarrow> Q \<longrightarrow> S)) = (Q \<longrightarrow> (P \<longrightarrow> R) \<and> (\<not> P \<longrightarrow> S))" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((P \<longrightarrow> Q \<longrightarrow> R) \<and> (\<not> P \<longrightarrow> Q \<longrightarrow> S)) = (Q \<longrightarrow> (P \<longrightarrow> R) \<and> (\<not> P \<longrightarrow> S))
theory Untyped_AI

lemma of_nat_shiftR:
  "a < 2 ^ word_bits \<Longrightarrow>
   unat (of_nat (shiftR a b)::machine_word) = unat ((of_nat a :: machine_word) >> b)" apply (subst shiftr_div_2n') apply (clarsimp simp: shiftR_nat) apply (subst unat_of_nat_eq[where 'a=machine_word_len]) apply (simp only: word_bits_def) apply (erule le_less_trans[OF div_le_dividend]) apply (subst unat_of_nat_eq[where 'a=machine_word_len]) apply (simp only: word_bits_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a < 2 ^ word_bits \<Longrightarrow> unat (word_of_nat (shiftR a b)) = unat (word_of_nat a >> b) proof (prove)
goal (1 subgoal):
 1. a < 2 ^ word_bits \<Longrightarrow> unat (word_of_nat (shiftR a b)) = unat (word_of_nat a) div 2 ^ b proof (prove)
goal (1 subgoal):
 1. a < 2 ^ word_bits \<Longrightarrow> unat (word_of_nat (a div 2 ^ b)) = unat (word_of_nat a) div 2 ^ b proof (prove)
goal (2 subgoals):
 1. a < 2 ^ word_bits \<Longrightarrow> a div 2 ^ b < 2 ^ LENGTH(32)
 2. a < 2 ^ word_bits \<Longrightarrow> a div 2 ^ b = unat (word_of_nat a) div 2 ^ b proof (prove)
goal (2 subgoals):
 1. a < 2 ^ LENGTH(32) \<Longrightarrow> a div 2 ^ b < 2 ^ LENGTH(32)
 2. a < 2 ^ word_bits \<Longrightarrow> a div 2 ^ b = unat (word_of_nat a) div 2 ^ b proof (prove)
goal (1 subgoal):
 1. a < 2 ^ word_bits \<Longrightarrow> a div 2 ^ b = unat (word_of_nat a) div 2 ^ b proof (prove)
goal (2 subgoals):
 1. a < 2 ^ word_bits \<Longrightarrow> a < 2 ^ LENGTH(32)
 2. a < 2 ^ word_bits \<Longrightarrow> a div 2 ^ b = a div 2 ^ b proof (prove)
goal (1 subgoal):
 1. a < 2 ^ word_bits \<Longrightarrow> a div 2 ^ b = a div 2 ^ b proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma valid_untypedD:
  "\<lbrakk> s \<turnstile> UntypedCap dev ptr bits idx; kheap s p = Some ko; pspace_aligned s\<rbrakk> \<Longrightarrow>
   obj_range p ko \<inter> cap_range (UntypedCap dev ptr bits idx) \<noteq> {} \<longrightarrow>
      obj_range p ko  \<subseteq> cap_range (UntypedCap dev ptr bits idx)
      \<and> obj_range p ko \<inter> usable_untyped_range (UntypedCap dev ptr bits idx) = {}" by (clarsimp simp: valid_untyped_def valid_cap_def cap_range_def obj_range_def)
     (meson order_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> UntypedCap dev ptr bits idx; kheap s p = Some ko; pspace_aligned s\<rbrakk> \<Longrightarrow> obj_range p ko \<inter> cap_range (UntypedCap dev ptr bits idx) \<noteq> {} \<longrightarrow> obj_range p ko \<subseteq> cap_range (UntypedCap dev ptr bits idx) \<and> obj_range p ko \<inter> usable_untyped_range (UntypedCap dev ptr bits idx) = {}
theory Untyped_AI

lemma pspace_no_overlap_detype:
  "\<lbrakk> s \<turnstile> UntypedCap dev ptr bits idx; pspace_aligned s; valid_objs s \<rbrakk>
     \<Longrightarrow> pspace_no_overlap_range_cover ptr bits (detype {ptr .. ptr + 2 ^ bits - 1} s)" apply (drule(2) pspace_no_overlap_detype'[rotated]) apply (drule valid_cap_aligned) apply (clarsimp simp: cap_aligned_def field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> UntypedCap dev ptr bits idx; pspace_aligned s; valid_objs s\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr bits) (detype {ptr..ptr + 2 ^ bits - 1} s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> UntypedCap dev ptr bits idx; valid_objs s; pspace_no_overlap {ptr..ptr + 2 ^ bits - 1} (detype {ptr..ptr + 2 ^ bits - 1} s)\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr bits) (detype {ptr..ptr + 2 ^ bits - 1} s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_no_overlap {ptr..ptr + 2 ^ bits - 1} (detype {ptr..ptr + 2 ^ bits - 1} s); cap_aligned (UntypedCap dev ptr bits idx)\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr bits) (detype {ptr..ptr + 2 ^ bits - 1} s) proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma zip_take_length[simp]:
  "zip (take (length ys) xs) ys = zip xs ys" apply (induct xs arbitrary: ys) apply simp apply (case_tac ys) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zip (take (length ys) xs) ys = zip xs ys proof (prove)
goal (2 subgoals):
 1. \<And>ys. zip (take (length ys) []) ys = zip [] ys
 2. \<And>a xs ys. (\<And>ys. zip (take (length ys) xs) ys = zip xs ys) \<Longrightarrow> zip (take (length ys) (a # xs)) ys = zip (a # xs) ys proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys. (\<And>ys. zip (take (length ys) xs) ys = zip xs ys) \<Longrightarrow> zip (take (length ys) (a # xs)) ys = zip (a # xs) ys proof (prove)
goal (2 subgoals):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. zip (take (length ys) xs) ys = zip xs ys; ys = []\<rbrakk> \<Longrightarrow> zip (take (length ys) (a # xs)) ys = zip (a # xs) ys
 2. \<And>a xs ys aa list. \<lbrakk>\<And>ys. zip (take (length ys) xs) ys = zip xs ys; ys = aa # list\<rbrakk> \<Longrightarrow> zip (take (length ys) (a # xs)) ys = zip (a # xs) ys proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys aa list. \<lbrakk>\<And>ys. zip (take (length ys) xs) ys = zip xs ys; ys = aa # list\<rbrakk> \<Longrightarrow> zip (take (length ys) (a # xs)) ys = zip (a # xs) ys proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma int_not_empty_subsetD:
  "\<lbrakk> A\<inter> B = {}; A\<noteq> {};B\<noteq> {}\<rbrakk> \<Longrightarrow> \<not> A \<subset> B \<and> \<not> B\<subset> A \<and> \<not> A = B" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<inter> B = {}; A \<noteq> {}; B \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> A \<subset> B \<and> \<not> B \<subset> A \<and> A \<noteq> B
theory Untyped_AI

lemma subset_not_psubset: " A \<subseteq> B \<Longrightarrow> \<not> B \<subset> A" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B \<Longrightarrow> \<not> B \<subset> A