kings-crown/FVELER_Isabelle huggingface dataset:
theory Move_C

lemma word_sandwich2:
  fixes a b :: "'a::len word"
  assumes "0 < a"
  assumes "a <= b"
  shows "b - a < b" using assms less_le_trans word_diff_less by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b - a < b proof (prove)
using this:
0 < a
a \<le> b
\<lbrakk>?x < ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x < ?z
\<lbrakk>0 < ?n; 0 < ?m; ?n \<le> ?m\<rbrakk> \<Longrightarrow> ?m - ?n < ?m

goal (1 subgoal):
 1. b - a < b
theory Move_C

lemma unat_and_mask_less_2p:
  fixes w :: "'a::len word"
  shows "m < LENGTH('a) \<Longrightarrow> unat (w && mask m) < 2 ^ m" by (simp add: unat_less_helper  and_mask_less')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m < LENGTH('a) \<Longrightarrow> unat (w && mask m) < 2 ^ m
theory Move_C

lemma unat_shiftr_less_2p:
  fixes w :: "'a::len word"
  shows "n + m = LENGTH('a) \<Longrightarrow> unat (w >> n) < 2 ^ m" by (cases "n = 0"; simp add: unat_less_helper shiftr_less_t2n3)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n + m = LENGTH('a) \<Longrightarrow> unat (w >> n) < 2 ^ m
theory Move_C

lemma nat_div_less_mono:
  fixes m n :: nat
  shows "m div d < n div d \<Longrightarrow> m < n" by (meson div_le_mono not_less)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m div d < n div d \<Longrightarrow> m < n
theory Move_C

lemma word_shiftr_less_mono:
  fixes w :: "'a::len word"
  shows "w >> n < v >> n \<Longrightarrow> w < v" by (auto simp: word_less_nat_alt shiftr_div_2n' elim: nat_div_less_mono)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w >> n < v >> n \<Longrightarrow> w < v
theory Move_C

lemma word_shiftr_less_mask:
  fixes w :: "'a::len word"
  shows "(w >> n < v >> n) \<longleftrightarrow> (w && ~~mask n < v && ~~mask n)" by (metis (mono_tags) le_shiftr mask_shift shiftr_eq_neg_mask_eq word_le_less_eq word_le_not_less)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (w >> n < v >> n) = (w && ~~ mask n < v && ~~ mask n)
theory Move_C

lemma word_shiftr_le_mask:
  fixes w :: "'a::len word"
  shows "(w >> n \<le> v >> n) \<longleftrightarrow> (w && ~~mask n \<le> v && ~~mask n)" by (metis (mono_tags) le_shiftr mask_shift shiftr_eq_neg_mask_eq word_le_less_eq word_le_not_less)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (w >> n \<le> v >> n) = (w && ~~ mask n \<le> v && ~~ mask n)
theory Move_C

lemma word_shiftr_eq_mask:
  fixes w :: "'a::len word"
  shows "(w >> n = v >> n) \<longleftrightarrow> (w && ~~mask n = v && ~~mask n)" by (metis (mono_tags) mask_shift shiftr_eq_neg_mask_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (w >> n = v >> n) = (w && ~~ mask n = v && ~~ mask n)
theory Move_C

lemma if_if_if_same_output:
  "(if c1 then if c2 then t else f else if c3 then t else f) = (if c1 \<and> c2 \<or> \<not>c1 \<and> c3 then t else f)" by (simp split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if c1 then if c2 then t else f else if c3 then t else f) = (if c1 \<and> c2 \<or> \<not> c1 \<and> c3 then t else f)
theory Move_C

lemma unat_ucast_prio_mask_simp[simp]:
  "unat (ucast (p::priority) && mask m :: machine_word) = unat (p && mask m)" by (simp add: ucast_and_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (UCAST(8 \<rightarrow> 32) p && mask m) = unat (p && mask m)
theory Move_C

lemma unat_ucast_prio_shiftr_simp[simp]:
  "unat (ucast (p::priority) >> n :: machine_word) = unat (p >> n)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (UCAST(8 \<rightarrow> 32) p >> n) = unat (p >> n)
theory Move_C

lemma from_bool_to_bool_and_1 [simp]:
  assumes r_size: "1 < size r"
  shows "from_bool (to_bool (r && 1)) = r && 1" proof - from r_size have "r && 1 < 2" by (simp add: and_mask_less_size [where n=1, unfolded mask_def, simplified]) thus ?thesis by (fastforce simp add: from_bool_def to_bool_def dest: word_less_cases) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. from_bool (to_bool (r && 1)) = r && 1 proof (state)
goal (1 subgoal):
 1. from_bool (to_bool (r && 1)) = r && 1 proof (chain)
picking this:
1 < size r proof (prove)
using this:
1 < size r

goal (1 subgoal):
 1. r && 1 < 2 proof (state)
this:
r && 1 < 2

goal (1 subgoal):
 1. from_bool (to_bool (r && 1)) = r && 1 proof (prove)
using this:
r && 1 < 2

goal (1 subgoal):
 1. from_bool (to_bool (r && 1)) = r && 1 proof (state)
this:
from_bool (to_bool (r && 1)) = r && 1

goal:
No subgoals!
theory Move_C

lemma wb_gt_2:
  "2 < word_bits" by (simp add: word_bits_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 < word_bits
theory Move_C

lemma inj_on_option_map:
 "inj_on (map_option f o m) (dom m) \<Longrightarrow> inj_on m (dom m)" by (simp add: inj_on_imageI2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj_on (map_option f \<circ> m) (dom m) \<Longrightarrow> inj_on m (dom m)
theory Move_C

lemma of_bool_inject[simp]: "of_bool a = of_bool b \<longleftrightarrow> a=b" by (cases a) (cases b, simp_all)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (of_bool a = of_bool b) = (a = b)
theory Move_C

lemma shiftr_and_eq_shiftl:
  fixes w x y :: "'a::len word"
  assumes r: "(w >> n) && x = y"
  shows "w && (x << n) = (y << n)" using assms proof - { fix i assume i: "i < LENGTH('a)" hence "test_bit (w && (x << n)) i \<longleftrightarrow> test_bit (y << n) i" using word_eqD[where x="i-n", OF r] by (cases "n \<le> i") (auto simp: nth_shiftl nth_shiftr) } thus ?thesis using word_eq_iff by blast qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w && (x << n) = y << n proof (prove)
using this:
(w >> n) && x = y

goal (1 subgoal):
 1. w && (x << n) = y << n proof (state)
goal (1 subgoal):
 1. (w >> n) && x = y \<Longrightarrow> w && (x << n) = y << n proof (state)
goal (1 subgoal):
 1. (w >> n) && x = y \<Longrightarrow> w && (x << n) = y << n proof (state)
goal (1 subgoal):
 1. (w >> n) && x = y \<Longrightarrow> w && (x << n) = y << n proof (state)
this:
i < LENGTH('a)

goal (1 subgoal):
 1. (w >> n) && x = y \<Longrightarrow> w && (x << n) = y << n proof (prove)
using this:
i < LENGTH('a)

goal (1 subgoal):
 1. (w && (x << n)) !! i = (y << n) !! i proof (prove)
using this:
i < LENGTH('a)
((w >> n) && x) !! (i - n) = y !! (i - n)

goal (1 subgoal):
 1. (w && (x << n)) !! i = (y << n) !! i proof (state)
this:
(w && (x << n)) !! i = (y << n) !! i

goal (1 subgoal):
 1. (w >> n) && x = y \<Longrightarrow> w && (x << n) = y << n proof (state)
this:
?i2 < LENGTH('a) \<Longrightarrow> (w && (x << n)) !! ?i2 = (y << n) !! ?i2

goal (1 subgoal):
 1. (w >> n) && x = y \<Longrightarrow> w && (x << n) = y << n proof (prove)
using this:
?i2 < LENGTH('a) \<Longrightarrow> (w && (x << n)) !! ?i2 = (y << n) !! ?i2

goal (1 subgoal):
 1. w && (x << n) = y << n proof (prove)
using this:
?i2 < LENGTH('a) \<Longrightarrow> (w && (x << n)) !! ?i2 = (y << n) !! ?i2
(?x = ?y) = (\<forall>n<LENGTH(?'a). ?x !! n = ?y !! n)

goal (1 subgoal):
 1. w && (x << n) = y << n proof (state)
this:
w && (x << n) = y << n

goal:
No subgoals!
theory Move_C

lemma sign_extend_0[simp]:
  "sign_extend a 0 = 0" by (simp add: sign_extend_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sign_extend a 0 = 0
theory Move_C

lemma mask_shiftr_times_simp:
  "\<lbrakk>x > n;is_aligned p n\<rbrakk> \<Longrightarrow> (p && mask x >> n) * (2^n) = (p && mask x)" apply (subst mult.commute) apply (simp add: shiftl_t2n[symmetric]) by (simp add: is_aligned_andI1 is_aligned_shiftr_shiftl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < x; is_aligned p n\<rbrakk> \<Longrightarrow> (p && mask x >> n) * 2 ^ n = p && mask x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < x; is_aligned p n\<rbrakk> \<Longrightarrow> 2 ^ n * (p && mask x >> n) = p && mask x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < x; is_aligned p n\<rbrakk> \<Longrightarrow> p && mask x >> n << n = p && mask x
theory Move_C

lemma name_seq_bound_helper:
  "(\<not> CP n \<and> (\<forall>n' < n. CP n'))
    \<Longrightarrow> (if \<exists>n. \<not> CP n
            then simpl_sequence c' (map f [0 ..< (LEAST n. \<not> CP n)])
            else c) = (simpl_sequence c' (map f [0 ..< n]))" apply (simp add: exI[where x=n]) apply (subst Least_equality[where x=n], simp_all) apply (rule ccontr, simp add: linorder_not_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> CP n \<and> (\<forall>n'<n. CP n') \<Longrightarrow> (if \<exists>n. \<not> CP n then simpl_sequence c' (map f [0..<LEAST n. \<not> CP n]) else c) = simpl_sequence c' (map f [0..<n]) proof (prove)
goal (1 subgoal):
 1. \<not> CP n \<and> (\<forall>n'<n. CP n') \<Longrightarrow> simpl_sequence c' (map f [0..<LEAST n. \<not> CP n]) = simpl_sequence c' (map f [0..<n]) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<not> CP n \<and> (\<forall>n'<n. CP n'); \<not> CP y\<rbrakk> \<Longrightarrow> n \<le> y proof (prove)
goal:
No subgoals!
theory Move_C

lemma bool_protectD:
  "bool_protect P \<Longrightarrow> P" unfolding bool_protect_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bool_protect P \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> P
theory Move_C

lemma bool_protectI:
  "P \<Longrightarrow> bool_protect P" unfolding bool_protect_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> bool_protect P proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> P
theory Move_C

lemma shiftr_le_mask:
  fixes w :: "'a::len word"
  shows "w >> n \<le> mask (LENGTH('a) - n)" by (metis and_mask_eq_iff_shiftr_0 le_mask_iff shiftr_mask_eq word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w >> n \<le> mask (LENGTH('a) - n)
theory Move_C

lemma ucast_shiftr:
  "UCAST('a::len \<rightarrow> 'b::len) w >> n = UCAST('a \<rightarrow> 'b) ((w && mask LENGTH('b)) >> n)" by (word_eqI_solve dest: bit_imp_le_length)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST('a \<rightarrow> 'b) w >> n = UCAST('a \<rightarrow> 'b) (w && mask LENGTH('b) >> n)
theory Move_C

lemma mask_eq_ucast_shiftr:
  assumes mask: "w && mask LENGTH('b) = w"
  shows "UCAST('a::len \<rightarrow> 'b::len) w >> n = UCAST('a \<rightarrow> 'b) (w >> n)" by (rule ucast_shiftr[where 'a='a and 'b='b, of w n, simplified mask])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST('a \<rightarrow> 'b) w >> n = UCAST('a \<rightarrow> 'b) (w >> n)
theory Move_C

lemma mask_eq_ucast_shiftl:
  assumes "w && mask (LENGTH('a) - n) = w"
  shows "UCAST('a::len \<rightarrow> 'b::len) w << n = UCAST('a \<rightarrow> 'b) (w << n)" apply (rule subst[where P="\<lambda>c. ucast c << n = ucast (c << n)", OF assms]) by word_eqI_solve

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST('a \<rightarrow> 'b) w << n = UCAST('a \<rightarrow> 'b) (w << n) proof (prove)
goal (1 subgoal):
 1. UCAST('a \<rightarrow> 'b) (w && mask (LENGTH('a) - n)) << n = UCAST('a \<rightarrow> 'b) (w && mask (LENGTH('a) - n) << n)
theory Move_C

lemma mask_le_mono:
  "m \<le> n \<Longrightarrow> mask m \<le> (mask n::'a::len word)" by (rule mask_mono)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> mask m \<le> mask n
theory Move_C

lemma word_and_mask_eq_le_mono:
  "w && mask m = w \<Longrightarrow> m \<le> n \<Longrightarrow> w && mask n = w" apply (simp add: and_mask_eq_iff_le_mask) by (erule order.trans, erule mask_le_mono)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w && mask m = w; m \<le> n\<rbrakk> \<Longrightarrow> w && mask n = w proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<le> mask m; m \<le> n\<rbrakk> \<Longrightarrow> w \<le> mask n
theory Move_C

lemma word_not_exists_nth:
  "(w::'a::len word) = 0 \<Longrightarrow> \<forall>i<LENGTH('a). \<not> w !! i" by (clarsimp simp: nth_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w = 0 \<Longrightarrow> \<forall>i<LENGTH('a). \<not> w !! i
theory Move_C

lemma word_eq_cast_unsigned:
  "(x = y) = (UCAST ('a signed \<rightarrow> ('a :: len)) x = ucast y)" by (simp add: word_eq_iff nth_ucast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x = y) = (UCAST('a signed \<rightarrow> 'a) x = UCAST('a signed \<rightarrow> 'a) y)
theory Move_C

lemma ran_tcb_cte_cases:
  "ran tcb_cte_cases =
   {(Structures_H.tcbCTable, tcbCTable_update),
    (Structures_H.tcbVTable, tcbVTable_update),
    (Structures_H.tcbReply, tcbReply_update),
    (Structures_H.tcbCaller, tcbCaller_update),
    (tcbIPCBufferFrame, tcbIPCBufferFrame_update)}" by (auto simp add: tcb_cte_cases_def cteSizeBits_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ran tcb_cte_cases = {(tcbCTable, tcbCTable_update), (tcbVTable, tcbVTable_update), (tcbReply, tcbReply_update), (tcbCaller, tcbCaller_update), (tcbIPCBufferFrame, tcbIPCBufferFrame_update)}
theory Move_C

lemma user_data_at_ko:
  "typ_at' UserDataT p s \<Longrightarrow> ko_at' UserData p s" apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def projectKOs) apply (case_tac ko, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_at' UserDataT p s \<Longrightarrow> ko_at' UserData p s proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); koTypeOf ko = UserDataT; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ko = KOUserData \<and> is_aligned p (objBitsKO KOUserData) \<and> ps_clear p (objBitsKO KOUserData) s proof (prove)
goal:
No subgoals!
theory Move_C

lemma map_to_ko_atI:
  "\<lbrakk>(projectKO_opt \<circ>\<^sub>m ksPSpace s) x = Some v;
    pspace_aligned' s; pspace_distinct' s\<rbrakk>
   \<Longrightarrow> ko_at' v x s" apply (clarsimp simp: map_comp_Some_iff) apply (erule (2) aligned_distinct_obj_atI') apply (simp add: project_inject) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(projectKO_opt \<circ>\<^sub>m ksPSpace s) x = Some v; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> ko_at' v x s proof (prove)
goal (1 subgoal):
 1. \<And>k'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; ksPSpace s x = Some k'; projectKO_opt k' = Some v\<rbrakk> \<Longrightarrow> ko_at' v x s proof (prove)
goal (1 subgoal):
 1. \<And>k'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; projectKO_opt k' = Some v\<rbrakk> \<Longrightarrow> k' = injectKOS v proof (prove)
goal:
No subgoals!
theory Move_C

lemma map_to_ko_atI':
  "\<lbrakk>(projectKO_opt \<circ>\<^sub>m (ksPSpace s)) x = Some v; invs' s\<rbrakk> \<Longrightarrow> ko_at' v x s" apply (clarsimp simp: map_comp_Some_iff) apply (erule aligned_distinct_obj_atI') apply clarsimp apply clarsimp apply (simp add: project_inject) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(projectKO_opt \<circ>\<^sub>m ksPSpace s) x = Some v; invs' s\<rbrakk> \<Longrightarrow> ko_at' v x s proof (prove)
goal (1 subgoal):
 1. \<And>k'. \<lbrakk>invs' s; ksPSpace s x = Some k'; projectKO_opt k' = Some v\<rbrakk> \<Longrightarrow> ko_at' v x s proof (prove)
goal (3 subgoals):
 1. \<And>k'. \<lbrakk>invs' s; projectKO_opt k' = Some v\<rbrakk> \<Longrightarrow> pspace_aligned' s
 2. \<And>k'. \<lbrakk>invs' s; projectKO_opt k' = Some v\<rbrakk> \<Longrightarrow> pspace_distinct' s
 3. \<And>k'. \<lbrakk>invs' s; projectKO_opt k' = Some v\<rbrakk> \<Longrightarrow> k' = injectKOS v proof (prove)
goal (2 subgoals):
 1. \<And>k'. \<lbrakk>invs' s; projectKO_opt k' = Some v\<rbrakk> \<Longrightarrow> pspace_distinct' s
 2. \<And>k'. \<lbrakk>invs' s; projectKO_opt k' = Some v\<rbrakk> \<Longrightarrow> k' = injectKOS v proof (prove)
goal (1 subgoal):
 1. \<And>k'. \<lbrakk>invs' s; projectKO_opt k' = Some v\<rbrakk> \<Longrightarrow> k' = injectKOS v proof (prove)
goal:
No subgoals!
theory Move_C

lemma map_to_ko_at_updI':
  "\<And>x x' y y' y''.
   \<lbrakk> (projectKO_opt \<circ>\<^sub>m (ksPSpace s)) x = Some y;
     valid_pspace' s; ko_at' y' x' s;
     objBitsKO (injectKO y') = objBitsKO y''; x \<noteq> x' \<rbrakk> \<Longrightarrow>
   ko_at' y x (s\<lparr>ksPSpace := (ksPSpace s)(x' \<mapsto> y'')\<rparr>)" by (fastforce simp: obj_at'_def projectKOs objBitsKO_def ps_clear_upd
               dest: map_to_ko_atI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>x x' y y' y''. \<lbrakk>(projectKO_opt \<circ>\<^sub>m ksPSpace s) x = Some y; valid_pspace' s; ko_at' y' x' s; objBitsKO (injectKOS y') = objBitsKO y''; x \<noteq> x'\<rbrakk> \<Longrightarrow> ko_at' y x (s\<lparr>ksPSpace := (ksPSpace s)(x' \<mapsto> y'')\<rparr>)
theory Move_C

lemma ps_clear_upd_None:
  "ksPSpace s y = None \<Longrightarrow>
    ps_clear x n (ksPSpace_update (\<lambda>a. (ksPSpace s)(y := None)) s') = ps_clear x n s" by (rule iffI | clarsimp elim!: ps_clear_domE | fastforce)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ksPSpace s y = None \<Longrightarrow> ps_clear x n (s'\<lparr>ksPSpace := (ksPSpace s)(y := None)\<rparr>) = ps_clear x n s
theory Move_C

lemma tcbFault_submonad_args:
  "submonad_args (thread_fetch tcbFault t) (thread_replace tcbFault_update t)
                 (tcb_at' t)" apply (rule thread_submonad_args) apply (case_tac v, simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. submonad_args (thread_fetch tcbFault t) (thread_replace tcbFault_update t) (tcb_at' t) proof (prove)
goal (3 subgoals):
 1. \<And>f v. tcbFault (tcbFault_update f v) = f (tcbFault v)
 2. \<And>f1 f2 v. tcbFault_update f1 (tcbFault_update f2 v) = tcbFault_update (f1 \<circ> f2) v
 3. \<And>f v. tcbFault_update (\<lambda>_. tcbFault v) v = v proof (prove)
goal:
No subgoals!
theory Move_C

lemma threadGet_stateAssert_gets:
  "threadGet ext t = do stateAssert (tcb_at' t) []; gets (thread_fetch ext t) od" apply (rule is_stateAssert_gets [OF _ _ empty_fail_threadGet no_fail_threadGet]) apply (clarsimp intro!: obj_at_ko_at'[where P="\<lambda>tcb :: tcb. True", simplified]
           | wp threadGet_wp)+ apply (clarsimp simp: obj_at'_def thread_fetch_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. threadGet ext t = do stateAssert (tcb_at' t) [];
gets (thread_fetch ext t)
od proof (prove)
goal (3 subgoals):
 1. \<forall>s. \<lbrace>(=) s\<rbrace> threadGet ext t \<lbrace>\<lambda>_. (=) s\<rbrace>
 2. \<lbrace>\<lambda>_. True\<rbrace> threadGet ext t \<lbrace>\<lambda>_. tcb_at' t\<rbrace>
 3. \<lbrace>tcb_at' t\<rbrace> threadGet ext t \<lbrace>\<lambda>rv s. thread_fetch ext t s = rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<Longrightarrow> \<exists>tcb. ko_at' tcb t s \<and> thread_fetch ext t s = ext tcb proof (prove)
goal:
No subgoals!
theory Move_C

lemma threadGet_tcbFault_submonad_fn:
  "threadGet tcbFault t =
   submonad_fn (thread_fetch tcbFault t) (thread_replace tcbFault_update t)
               (tcb_at' t) get" apply (rule ext) apply (clarsimp simp: submonad_fn_def bind_assoc split_def) apply (subst threadGet_stateAssert_gets, simp) apply (rule bind_apply_cong [OF refl]) apply (clarsimp simp: in_monad bind_def gets_def get_def return_def
                        submonad_args.args(3) [OF tcbFault_submonad_args]
                        select_f_def modify_def put_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. threadGet tcbFault t = submonad_fn (thread_fetch tcbFault t) (thread_replace tcbFault_update t) (tcb_at' t) get proof (prove)
goal (1 subgoal):
 1. \<And>x. threadGet tcbFault t x = submonad_fn (thread_fetch tcbFault t) (thread_replace tcbFault_update t) (tcb_at' t) get x proof (prove)
goal (1 subgoal):
 1. \<And>x. threadGet tcbFault t x = (do y <- stateAssert (tcb_at' t) [];
substate <- gets (thread_fetch tcbFault t);
p <- select_f (get substate);
y <- modify (thread_replace tcbFault_update t (snd p));
return (fst p)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x. (do y <- stateAssert (tcb_at' t) [];
gets (thread_fetch tcbFault t)
od) x = (do y <- stateAssert (tcb_at' t) [];
substate <- gets (thread_fetch tcbFault t);
p <- select_f (get substate);
y <- modify (thread_replace tcbFault_update t (snd p));
return (fst p)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x rv st. (rv, st) \<in> fst (stateAssert (tcb_at' t) [] x) \<Longrightarrow> gets (thread_fetch tcbFault t) st = (do substate <- gets (thread_fetch tcbFault t);
p <- select_f (get substate);
y <- modify (thread_replace tcbFault_update t (snd p));
return (fst p)
od) st proof (prove)
goal:
No subgoals!
theory Move_C

lemma asUser_obj_at_notQ:
  "\<lbrace>obj_at' (Not \<circ> tcbQueued) t\<rbrace>
   asUser t (setRegister r v)
   \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace>" apply (simp add: asUser_def) apply (rule hoare_seq_ext)+ apply (simp add: split_def) apply (rule threadSet_obj_at'_really_strongest) apply (wp threadGet_wp |rule gets_inv|wpc|clarsimp)+ apply (clarsimp simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (Not \<circ> tcbQueued) t\<rbrace> asUser t (setRegister r v) \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (Not \<circ> tcbQueued) t\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
(a, uc') <- select_f (setRegister r v uc);
threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) t
od \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>uc x. \<lbrace>?B3 uc x\<rbrace> case x of (a, uc') \<Rightarrow> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) t \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace>
 2. \<And>uc. \<lbrace>?B uc\<rbrace> select_f (setRegister r v uc) \<lbrace>?B3 uc\<rbrace>
 3. \<lbrace>obj_at' (Not \<circ> tcbQueued) t\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>?B\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>uc x. \<lbrace>?B3 uc x\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd x) (tcbArch tcb)) tcb) t \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace>
 2. \<And>uc. \<lbrace>?B uc\<rbrace> select_f (setRegister r v uc) \<lbrace>?B3 uc\<rbrace>
 3. \<lbrace>obj_at' (Not \<circ> tcbQueued) t\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>?B\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>uc. \<lbrace>?B uc\<rbrace> select_f (setRegister r v uc) \<lbrace>\<lambda>x s. tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = t then (Not \<circ> tcbQueued) (tcbArch_update (\<lambda>_. atcbContextSet (snd x) (tcbArch obj)) obj) else (Not \<circ> tcbQueued) obj) t s\<rbrace>
 2. \<lbrace>obj_at' (Not \<circ> tcbQueued) t\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>?B\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>obj_at' (Not \<circ> tcbQueued) t s; tcb_at' t s\<rbrakk> \<Longrightarrow> \<exists>tcb. ko_at' tcb t s \<and> ((\<exists>b. ((), b) \<in> fst (setRegister r v (atcbContextGet (tcbArch tcb)))) \<longrightarrow> obj_at' (\<lambda>obj. \<not> tcbQueued obj) t s) proof (prove)
goal:
No subgoals!
theory Move_C

lemma empty_fail_asUser[iff]:
  "empty_fail m \<Longrightarrow> empty_fail (asUser t m)" apply (simp add: asUser_def split_def) apply (intro empty_fail_bind, simp_all) apply (simp add: select_f_def empty_fail_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail m \<Longrightarrow> empty_fail (asUser t m) proof (prove)
goal (1 subgoal):
 1. empty_fail m \<Longrightarrow> empty_fail (do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (m uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x. empty_fail m \<Longrightarrow> empty_fail (select_f (m x)) proof (prove)
goal:
No subgoals!