kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeapPre_AI

lemma arch_obj_pred_a_type[intro, simp]: "arch_obj_pred (\<lambda>ko. a_type ko = AArch T)" by (auto simp add: arch_obj_pred_defs a_type_def split: kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_obj_pred (\<lambda>ko. a_type ko = AArch T)
theory KHeapPre_AI

lemma arch_obj_pred_fun_lift: "arch_obj_pred (\<lambda>ko. F (arch_obj_fun_lift P N ko))" by (simp add: arch_obj_pred_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_obj_pred (\<lambda>ko. F (arch_obj_fun_lift P N ko))
theory KHeapPre_AI

lemma arch_obj_pred_const_conjI[intro]:
  "arch_obj_pred P \<Longrightarrow>
    arch_obj_pred P' \<Longrightarrow>
    arch_obj_pred (\<lambda>ko. P ko \<and> P' ko)" apply (simp only: arch_obj_pred_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arch_obj_pred P; arch_obj_pred P'\<rbrakk> \<Longrightarrow> arch_obj_pred (\<lambda>ko. P ko \<and> P' ko) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ko ko'. non_arch_obj ko \<longrightarrow> non_arch_obj ko' \<longrightarrow> P ko = P ko'; \<forall>ko ko'. non_arch_obj ko \<longrightarrow> non_arch_obj ko' \<longrightarrow> P' ko = P' ko'\<rbrakk> \<Longrightarrow> \<forall>ko ko'. non_arch_obj ko \<longrightarrow> non_arch_obj ko' \<longrightarrow> (P ko \<and> P' ko) = (P ko' \<and> P' ko') proof (prove)
goal:
No subgoals!
theory KHeapPre_AI

lemma arch_obj_pred_fI:
  "(\<And>x. arch_obj_pred (P x)) \<Longrightarrow> arch_obj_pred (\<lambda>ko. f (\<lambda>x :: 'a :: type. P x ko))" apply (simp only: arch_obj_pred_def) apply (intro allI impI) apply (rule arg_cong[where f=f]) by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. arch_obj_pred (P x)) \<Longrightarrow> arch_obj_pred (\<lambda>ko. f (\<lambda>x. P x ko)) proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<forall>ko ko'. non_arch_obj ko \<longrightarrow> non_arch_obj ko' \<longrightarrow> P x ko = P x ko') \<Longrightarrow> \<forall>ko ko'. non_arch_obj ko \<longrightarrow> non_arch_obj ko' \<longrightarrow> f (\<lambda>x. P x ko) = f (\<lambda>x. P x ko') proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>\<And>x. \<forall>ko ko'. non_arch_obj ko \<longrightarrow> non_arch_obj ko' \<longrightarrow> P x ko = P x ko'; non_arch_obj ko; non_arch_obj ko'\<rbrakk> \<Longrightarrow> f (\<lambda>x. P x ko) = f (\<lambda>x. P x ko') proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>\<And>x. \<forall>ko ko'. non_arch_obj ko \<longrightarrow> non_arch_obj ko' \<longrightarrow> P x ko = P x ko'; non_arch_obj ko; non_arch_obj ko'\<rbrakk> \<Longrightarrow> (\<lambda>x. P x ko) = (\<lambda>x. P x ko')
theory KHeapPre_AI

lemma set_object_typ_at [wp]:
  "\<lbrace>\<lambda>s. P (typ_at T p' s)\<rbrace>
  set_object p ko \<lbrace>\<lambda>rv s. P (typ_at T p' s)\<rbrace>" apply (simp add: set_object_def get_object_def) apply wp apply clarsimp apply (erule rsubst [where P=P]) apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p' s)\<rbrace> set_object p ko \<lbrace>\<lambda>rv s. P (typ_at T p' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p' s)\<rbrace> do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = a_type ko);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)
od \<lbrace>\<lambda>rv s. P (typ_at T p' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (typ_at T p' s) \<Longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> a_type (the (kheap s p)) = a_type ko \<longrightarrow> P (typ_at T p' (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>P (typ_at T p' s); kheap s p = Some y; a_type y = a_type ko\<rbrakk> \<Longrightarrow> P (typ_at T p' (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>kheap s p = Some y; a_type y = a_type ko\<rbrakk> \<Longrightarrow> typ_at T p' s = typ_at T p' (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!
theory KHeapPre_AI

lemma set_object_neg_ko:
  "\<lbrace>not ko_at ko' p' and K (p = p' \<longrightarrow> ko \<noteq> ko')\<rbrace>
  set_object p ko
  \<lbrace>\<lambda>_ s. \<not> ko_at ko' p' s\<rbrace>" apply (simp add: set_object_def get_object_def) apply wp apply (simp add: pred_neg_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>not ko_at ko' p' and K (p = p' \<longrightarrow> ko \<noteq> ko')\<rbrace> set_object p ko \<lbrace>\<lambda>_ s. \<not> ko_at ko' p' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>not ko_at ko' p' and (\<lambda>y. p = p' \<longrightarrow> ko \<noteq> ko')\<rbrace> do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = a_type ko);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)
od \<lbrace>\<lambda>_ s. \<not> ko_at ko' p' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (not ko_at ko' p' and (\<lambda>y. p = p' \<longrightarrow> ko \<noteq> ko')) s \<Longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> a_type (the (kheap s p)) = a_type ko \<longrightarrow> \<not> ko_at ko' p' (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>) proof (prove)
goal:
No subgoals!
theory KHeapPre_AI

lemma get_tcb_at: "tcb_at t s \<Longrightarrow> (\<exists>tcb. get_tcb t s = Some tcb)" by (simp add: tcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at t s \<Longrightarrow> \<exists>tcb. get_tcb t s = Some tcb
theory KHeapPre_AI

lemma typ_at_same_type:
  assumes "typ_at T p s" "a_type k = a_type ko" "kheap s p' = Some ko"
  shows "typ_at T p (s\<lparr>kheap := (kheap s)(p' \<mapsto> k)\<rparr>)" using assms by (clarsimp simp: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_at T p (s\<lparr>kheap := (kheap s)(p' \<mapsto> k)\<rparr>) proof (prove)
using this:
typ_at T p s
a_type k = a_type ko
kheap s p' = Some ko

goal (1 subgoal):
 1. typ_at T p (s\<lparr>kheap := (kheap s)(p' \<mapsto> k)\<rparr>)
theory KHeapPre_AI

lemma hoare_to_pure_kheap_upd:
  assumes hoare[rule_format]:
    "\<And>f. (\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace>
      f \<lbrace>\<lambda>r s. P (typ_at (AArch T) p s)\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
  assumes typ_eq: "a_type k = a_type ko"
  assumes valid: "P (s :: ('z :: state_ext) state)"
  assumes at: "ko_at ko p s"
  shows "P (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)" apply (rule use_valid[where f="
      do
        s' <- get;
        assert (s' = s);
        (modify (\<lambda>s. s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>));
        return undefined
      od", OF _ hoare valid]) apply (fastforce simp add: simpler_modify_def get_def bind_def
                             assert_def return_def[abs_def] fail_def)[1] apply wp apply (insert typ_eq at) apply clarsimp apply (erule_tac P=P in rsubst) by (auto simp add: obj_at_def a_type_def split: kernel_object.splits if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) proof (prove)
goal (2 subgoals):
 1. (?r, s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) \<in> fst ((do s' <- get;
assert (s' = s);
modify (\<lambda>s. s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>);
return undefined
od) s)
 2. \<And>P pa T. \<lbrace>\<lambda>s. P (typ_at (AArch T) pa s)\<rbrace> do s' <- get;
assert (s' = s);
modify (\<lambda>s. s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>);
return undefined
od \<lbrace>\<lambda>r s. P (typ_at (AArch T) pa s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P pa T. \<lbrace>\<lambda>s. P (typ_at (AArch T) pa s)\<rbrace> do s' <- get;
assert (s' = s);
modify (\<lambda>s. s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>);
return undefined
od \<lbrace>\<lambda>r s. P (typ_at (AArch T) pa s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P pa T sa. P (typ_at (AArch T) pa sa) \<Longrightarrow> sa = s \<longrightarrow> P (typ_at (AArch T) pa (sa\<lparr>kheap := (kheap sa)(p \<mapsto> k)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>P pa T sa. \<lbrakk>P (typ_at (AArch T) pa sa); a_type k = a_type ko; ko_at ko p s\<rbrakk> \<Longrightarrow> sa = s \<longrightarrow> P (typ_at (AArch T) pa (sa\<lparr>kheap := (kheap sa)(p \<mapsto> k)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>P pa T. \<lbrakk>P (typ_at (AArch T) pa s); a_type k = a_type ko; ko_at ko p s\<rbrakk> \<Longrightarrow> P (typ_at (AArch T) pa (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>P pa T. \<lbrakk>a_type k = a_type ko; ko_at ko p s\<rbrakk> \<Longrightarrow> typ_at (AArch T) pa s = typ_at (AArch T) pa (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>)
theory KHeapPre_AI

lemma set_object_wp:
  "\<lbrace>\<lambda>s. Q (s\<lparr> kheap := (kheap s) (p \<mapsto> v)\<rparr>) \<rbrace> set_object p v \<lbrace>\<lambda>_. Q\<rbrace>" apply (simp add: set_object_def get_object_def) apply wp apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (s\<lparr>kheap := (kheap s)(p \<mapsto> v)\<rparr>)\<rbrace> set_object p v \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (s\<lparr>kheap := (kheap s)(p \<mapsto> v)\<rparr>)\<rbrace> do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = a_type v);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> v)\<rparr>)
od \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. Q (s\<lparr>kheap := (kheap s)(p \<mapsto> v)\<rparr>) \<Longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> a_type (the (kheap s p)) = a_type v \<longrightarrow> Q (s\<lparr>kheap := (kheap s)(p \<mapsto> v)\<rparr>) proof (prove)
goal:
No subgoals!
theory KHeapPre_AI

lemma get_object_wp:
  "\<lbrace>\<lambda>s. \<forall>ko. ko_at ko p s \<longrightarrow> Q ko s\<rbrace> get_object p \<lbrace>Q\<rbrace>" apply (clarsimp simp: get_object_def) apply wp apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ko. ko_at ko p s \<longrightarrow> Q ko s\<rbrace> get_object p \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ko. ko_at ko p s \<longrightarrow> Q ko s\<rbrace> do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>ko. ko_at ko p s \<longrightarrow> Q ko s \<Longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> Q (the (kheap s p)) s proof (prove)
goal:
No subgoals!
theory KHeapPre_AI

lemma hoare_strengthen_pre_via_assert_forward:
  assumes pos: "\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
  assumes rel: "\<And>s. S s \<Longrightarrow> P s \<or> N s"
  assumes neg: "\<lbrace> N \<rbrace> f \<lbrace> \<bottom>\<bottom> \<rbrace>"
  shows "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>" apply (rule hoare_weaken_pre) apply (rule hoare_strengthen_post) apply (rule hoare_vcg_disj_lift[OF pos neg]) apply simp apply (erule rel) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> f \<lbrace>Q\<rbrace>
 2. \<And>s. S s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> f \<lbrace>?Q3\<rbrace>
 2. \<And>rv s. ?Q3 rv s \<Longrightarrow> Q rv s
 3. \<And>s. S s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. Q rv s \<or> False \<Longrightarrow> Q rv s
 2. \<And>s. S s \<Longrightarrow> P s \<or> N s proof (prove)
goal (1 subgoal):
 1. \<And>s. S s \<Longrightarrow> P s \<or> N s proof (prove)
goal:
No subgoals!
theory KHeapPre_AI

lemma hoare_set_object_weaken_pre:
  assumes "\<lbrace>P\<rbrace> set_object p v \<lbrace>\<lambda>_. Q\<rbrace>"
  shows "\<lbrace>\<lambda>s. \<forall>ko. ko_at ko p s \<longrightarrow> (a_type v = a_type ko) \<longrightarrow> P s\<rbrace>
         set_object p v
         \<lbrace>\<lambda>_. Q\<rbrace>" apply (rule hoare_strengthen_pre_via_assert_forward
                [OF assms, where N="\<lambda>s. \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko \<noteq> a_type v"]) apply fastforce apply (simp add: set_object_def) apply (rule hoare_seq_ext[OF _ get_object_sp]) apply (rule hoare_seq_ext[OF _ assert_sp]) apply (fastforce intro: hoare_weaken_pre[OF hoare_pre_cont]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ko. ko_at ko p s \<longrightarrow> a_type v = a_type ko \<longrightarrow> P s\<rbrace> set_object p v \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<forall>ko. ko_at ko p s \<longrightarrow> a_type v = a_type ko \<longrightarrow> P s \<Longrightarrow> P s \<or> (\<forall>ko. ko_at ko p s \<longrightarrow> a_type ko \<noteq> a_type v)
 2. \<lbrace>\<lambda>s. \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko \<noteq> a_type v\<rbrace> set_object p v \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko \<noteq> a_type v\<rbrace> set_object p v \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko \<noteq> a_type v\<rbrace> do kobj <- get_object p;
y <- assert (a_type kobj = a_type v);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> v)\<rparr>)
od \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>kobj. \<lbrace>(\<lambda>s. \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko \<noteq> a_type v) and ko_at kobj p\<rbrace> do y <- assert (a_type kobj = a_type v);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> v)\<rparr>)
od \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>kobj y. \<lbrace>\<lambda>s. ((\<lambda>s. \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko \<noteq> a_type v) and ko_at kobj p) s \<and> a_type kobj = a_type v\<rbrace> do s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> v)\<rparr>)
od \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma obj_at_split: "(obj_at (P xo) p s \<and> (Q xo)) = obj_at (\<lambda>ko. P xo ko \<and> Q xo) p s" by (auto simp: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (obj_at (P xo) p s \<and> Q xo) = obj_at (\<lambda>ko. P xo ko \<and> Q xo) p s
theory ArchKHeap_AI

lemma valid_vspace_objs_lift:
  assumes x: "\<And>P. \<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup s)\<rbrace>"
  assumes y: "\<And>ako p. \<lbrace>\<lambda>s. \<not> ko_at (ArchObj ako) p s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> ko_at (ArchObj ako) p s\<rbrace>"
  assumes z: "\<And>p T. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>rv. typ_at (AArch T) p\<rbrace>"
  shows      "\<lbrace>valid_vspace_objs\<rbrace> f \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>" apply (simp add: valid_vspace_objs_def) apply (rule hoare_vcg_all_lift, wp hoare_convert_imp[OF x]; (rule hoare_vcg_all_lift | assumption)) apply (rule hoare_convert_imp[OF y]) apply (rule valid_vspace_obj_typ[OF z]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs\<rbrace> f \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s)\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p ao. \<lbrace>\<lambda>s. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s\<rbrace> f \<lbrace>\<lambda>rv s. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p ao. \<lbrace>valid_vspace_obj ao\<rbrace> f \<lbrace>\<lambda>rv. valid_vspace_obj ao\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma vspace_obj_imp: "non_arch_obj ko \<Longrightarrow> non_vspace_obj ko" apply (cases ko; clarsimp) apply (rename_tac ako) apply (case_tac ako, auto simp: non_arch_obj_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. non_arch_obj ko \<Longrightarrow> non_vspace_obj ko proof (prove)
goal (1 subgoal):
 1. \<And>x5. \<lbrakk>non_arch_obj (ArchObj x5); ko = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ako. \<lbrakk>non_arch_obj (ArchObj ako); ko = ArchObj ako\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma non_vspace_objs[intro]:
  "non_vspace_obj (Endpoint ep)"
  "non_vspace_obj (CNode sz cnode_contents)"
  "non_vspace_obj (TCB tcb)"
  "non_vspace_obj (Notification notification)" by (auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (non_vspace_obj (Endpoint ep) &&& non_vspace_obj (CNode sz cnode_contents)) &&& non_vspace_obj (TCB tcb) &&& non_vspace_obj (Notification notification)
theory ArchKHeap_AI

lemma vspace_obj_predE:
  "\<lbrakk>vspace_obj_pred P; non_vspace_obj ko; non_vspace_obj ko'\<rbrakk> \<Longrightarrow> P ko = P ko'" apply (unfold vspace_obj_pred_def) apply (erule allE[where ?x="ko"]) apply (erule allE[where ?x="ko'"]) by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vspace_obj_pred P; non_vspace_obj ko; non_vspace_obj ko'\<rbrakk> \<Longrightarrow> P ko = P ko' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ko ko'. non_vspace_obj ko \<longrightarrow> non_vspace_obj ko' \<longrightarrow> P ko = P ko'; non_vspace_obj ko; non_vspace_obj ko'\<rbrakk> \<Longrightarrow> P ko = P ko' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>non_vspace_obj ko; non_vspace_obj ko'; \<forall>ko'. non_vspace_obj ko \<longrightarrow> non_vspace_obj ko' \<longrightarrow> P ko = P ko'\<rbrakk> \<Longrightarrow> P ko = P ko' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>non_vspace_obj ko; non_vspace_obj ko'; non_vspace_obj ko \<longrightarrow> non_vspace_obj ko' \<longrightarrow> P ko = P ko'\<rbrakk> \<Longrightarrow> P ko = P ko'
theory ArchKHeap_AI

lemma vspace_pred_imp: "vspace_obj_pred P \<Longrightarrow> arch_obj_pred P" apply (clarsimp simp: arch_obj_pred_def) apply (rule vspace_obj_predE) apply simp apply (rule vspace_obj_imp, assumption)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vspace_obj_pred P \<Longrightarrow> arch_obj_pred P proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>vspace_obj_pred P; non_arch_obj ko; non_arch_obj ko'\<rbrakk> \<Longrightarrow> P ko = P ko' proof (prove)
goal (3 subgoals):
 1. \<And>ko ko'. \<lbrakk>vspace_obj_pred P; non_arch_obj ko; non_arch_obj ko'\<rbrakk> \<Longrightarrow> vspace_obj_pred P
 2. \<And>ko ko'. \<lbrakk>vspace_obj_pred P; non_arch_obj ko; non_arch_obj ko'\<rbrakk> \<Longrightarrow> non_vspace_obj ko
 3. \<And>ko ko'. \<lbrakk>vspace_obj_pred P; non_arch_obj ko; non_arch_obj ko'\<rbrakk> \<Longrightarrow> non_vspace_obj ko' proof (prove)
goal (2 subgoals):
 1. \<And>ko ko'. \<lbrakk>vspace_obj_pred P; non_arch_obj ko; non_arch_obj ko'\<rbrakk> \<Longrightarrow> non_vspace_obj ko
 2. \<And>ko ko'. \<lbrakk>vspace_obj_pred P; non_arch_obj ko; non_arch_obj ko'\<rbrakk> \<Longrightarrow> non_vspace_obj ko' proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma vspace_obj_pred_a_type[intro, simp]: "vspace_obj_pred (\<lambda>ko. a_type ko = AArch T)" by (auto simp add: vspace_obj_pred_defs a_type_def
           split: kernel_object.splits arch_kernel_obj.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vspace_obj_pred (\<lambda>ko. a_type ko = AArch T)
theory ArchKHeap_AI

lemma vspace_obj_pred_fun_lift: "vspace_obj_pred (\<lambda>ko. F (vspace_obj_fun_lift P N ko))" by (auto simp: vspace_obj_pred_defs vspace_obj_fun_lift_def
           split: kernel_object.splits arch_kernel_obj.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vspace_obj_pred (\<lambda>ko. F (vspace_obj_fun_lift P N ko))
theory ArchKHeap_AI

lemma vspace_obj_pred_const_conjI[intro]:
  "vspace_obj_pred P \<Longrightarrow>
    vspace_obj_pred P' \<Longrightarrow>
    vspace_obj_pred (\<lambda>ko. P ko \<and> P' ko)" apply (simp only: vspace_obj_pred_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vspace_obj_pred P; vspace_obj_pred P'\<rbrakk> \<Longrightarrow> vspace_obj_pred (\<lambda>ko. P ko \<and> P' ko) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ko ko'. non_vspace_obj ko \<longrightarrow> non_vspace_obj ko' \<longrightarrow> P ko = P ko'; \<forall>ko ko'. non_vspace_obj ko \<longrightarrow> non_vspace_obj ko' \<longrightarrow> P' ko = P' ko'\<rbrakk> \<Longrightarrow> \<forall>ko ko'. non_vspace_obj ko \<longrightarrow> non_vspace_obj ko' \<longrightarrow> (P ko \<and> P' ko) = (P ko' \<and> P' ko') proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma vspace_obj_pred_fI:
  "(\<And>x. vspace_obj_pred (P x)) \<Longrightarrow> vspace_obj_pred (\<lambda>ko. f (\<lambda>x :: 'a :: type. P x ko))" apply (simp only: vspace_obj_pred_def) apply (intro allI impI) apply (rule arg_cong[where f=f]) by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. vspace_obj_pred (P x)) \<Longrightarrow> vspace_obj_pred (\<lambda>ko. f (\<lambda>x. P x ko)) proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<forall>ko ko'. non_vspace_obj ko \<longrightarrow> non_vspace_obj ko' \<longrightarrow> P x ko = P x ko') \<Longrightarrow> \<forall>ko ko'. non_vspace_obj ko \<longrightarrow> non_vspace_obj ko' \<longrightarrow> f (\<lambda>x. P x ko) = f (\<lambda>x. P x ko') proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>\<And>x. \<forall>ko ko'. non_vspace_obj ko \<longrightarrow> non_vspace_obj ko' \<longrightarrow> P x ko = P x ko'; non_vspace_obj ko; non_vspace_obj ko'\<rbrakk> \<Longrightarrow> f (\<lambda>x. P x ko) = f (\<lambda>x. P x ko') proof (prove)
goal (1 subgoal):
 1. \<And>ko ko'. \<lbrakk>\<And>x. \<forall>ko ko'. non_vspace_obj ko \<longrightarrow> non_vspace_obj ko' \<longrightarrow> P x ko = P x ko'; non_vspace_obj ko; non_vspace_obj ko'\<rbrakk> \<Longrightarrow> (\<lambda>x. P x ko) = (\<lambda>x. P x ko')
theory ArchKHeap_AI

lemma pspace_in_kernel_window_atyp_lift:
  assumes atyp_inv: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
  assumes arch_inv: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. pspace_in_kernel_window s\<rbrace> f \<lbrace>\<lambda>rv s. pspace_in_kernel_window s\<rbrace>" by (rule pspace_in_kernel_window_atyp_lift_strong[OF atyp_inv arch_inv])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> f \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>
theory ArchKHeap_AI

lemma cap_refs_in_kernel_window_arch_update[simp]:
  "arm_kernel_vspace (f (arch_state s)) = arm_kernel_vspace (arch_state s)
     \<Longrightarrow> cap_refs_in_kernel_window (arch_state_update f s) = cap_refs_in_kernel_window s" by (simp add: cap_refs_in_kernel_window_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arm_kernel_vspace (f (arch_state s)) = arm_kernel_vspace (arch_state s) \<Longrightarrow> cap_refs_in_kernel_window (arch_state_update f s) = cap_refs_in_kernel_window s