kings-crown/FVELER_Isabelle huggingface dataset:
theory ADT_IF

lemma irq_state_inv_triv:
  assumes irq_state: "\<And>P. f \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace>"
  assumes irq_masks: "\<And>P. f \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace>"
  shows "f \<lbrace>irq_state_inv st\<rbrace>" apply (clarsimp simp: valid_def irq_state_inv_def) apply (rule use_valid[OF _ irq_state], assumption) apply (erule use_valid[OF _ irq_masks]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irq_state_inv st\<rbrace> f \<lbrace>\<lambda>_. irq_state_inv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); irq_state_of_state st \<le> irq_state_of_state s; irq_masks_of_state s = irq_masks_of_state st; next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state st) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state st)\<rbrakk> \<Longrightarrow> irq_state_of_state st \<le> irq_state_of_state b \<and> irq_masks_of_state b = irq_masks_of_state st \<and> next_irq_state (Suc (irq_state_of_state b)) (irq_masks_of_state b) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); irq_state_of_state st \<le> irq_state_of_state s; irq_masks_of_state s = irq_masks_of_state st; next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state st) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state st)\<rbrakk> \<Longrightarrow> irq_state_of_state st \<le> irq_state_of_state s \<and> irq_masks_of_state b = irq_masks_of_state st \<and> next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state b) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>irq_state_of_state st \<le> irq_state_of_state s; irq_masks_of_state s = irq_masks_of_state st; next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state st) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state st)\<rbrakk> \<Longrightarrow> irq_state_of_state st \<le> irq_state_of_state s \<and> irq_masks_of_state s = irq_masks_of_state st \<and> next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state s) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state s) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma OR_choiceE_wp:
  assumes a: "\<And>s. \<lbrace>P and (=) s\<rbrace> b \<lbrace>\<lambda> r s'. (r \<longrightarrow> P' s) \<and> (\<not> r \<longrightarrow> P'' s)\<rbrace>"
  assumes b: "\<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
  assumes c: "\<lbrace>P''\<rbrace> g \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
  shows "\<lbrace>P\<rbrace> OR_choiceE b f g \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>" apply (simp add: OR_choiceE_def) apply (wp b c | wpc)+ apply (clarsimp simp: mk_ef_def wrap_ext_bool_det_ext_ext_def) apply (drule a[simplified valid_def, rule_format, rotated]) apply simp apply (fastforce split: prod.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> OR_choiceE b f g \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE ex <- liftE get;
(rv, uu_) <- liftE (select_f (mk_ef (wrap_ext_bool b ex)));
if rv then f else g
odE \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> \<forall>x\<in>fst (mk_ef (wrap_ext_bool b s)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (xa \<longrightarrow> P' s) \<and> (\<not> xa \<longrightarrow> P'' s) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>P s; (x, xa) \<in> fst (b s)\<rbrakk> \<Longrightarrow> (x \<longrightarrow> P' s) \<and> (\<not> x \<longrightarrow> P'' s) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa. P s \<Longrightarrow> (P and (=) (?s30 s x xa)) s
 2. \<And>s x xa. \<lbrakk>P s; case (x, xa) of (r, s') \<Rightarrow> (r \<longrightarrow> P' (?s30 s x xa)) \<and> (\<not> r \<longrightarrow> P'' (?s30 s x xa))\<rbrakk> \<Longrightarrow> (x \<longrightarrow> P' s) \<and> (\<not> x \<longrightarrow> P'' s) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>P s; case (x, xa) of (r, s') \<Rightarrow> (r \<longrightarrow> P' s) \<and> (\<not> r \<longrightarrow> P'' s)\<rbrakk> \<Longrightarrow> (x \<longrightarrow> P' s) \<and> (\<not> x \<longrightarrow> P'' s) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma validE_validE_E':
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -, \<lbrace>E\<rbrace>" apply (rule validE_validE_E) apply (rule hoare_post_impErr) apply assumption apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>?Q2\<rbrace>, \<lbrace>?E2\<rbrace>
 2. \<And>rv s. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; ?Q2 rv s\<rbrakk> \<Longrightarrow> True
 3. \<And>e s. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; ?E2 e s\<rbrakk> \<Longrightarrow> E e s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; Q rv s\<rbrakk> \<Longrightarrow> True
 2. \<And>e s. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; E e s\<rbrakk> \<Longrightarrow> E e s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma rec_del_irq_state_inv:
  "\<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace>
   rec_del call
   \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>" apply (rule hoare_post_impErr) apply (rule use_spec) apply (rule rec_del_irq_state_inv') apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del call \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del call \<lbrace>?Q\<rbrace>, \<lbrace>?E\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> irq_state_inv st s
 3. \<And>e s. ?E e s \<Longrightarrow> irq_state_next st s proof (prove)
goal (3 subgoals):
 1. \<And>s. s \<turnstile> \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> rec_del call \<lbrace>?Q\<rbrace>, \<lbrace>?E\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> irq_state_inv st s
 3. \<And>e s. ?E e s \<Longrightarrow> irq_state_next st s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. (case call of FinaliseSlotCall x y \<Rightarrow> y \<or> fst rv \<longrightarrow> snd rv = NullCap | _ \<Rightarrow> True) \<and> domain_sep_inv False sta s \<and> irq_state_inv st s \<Longrightarrow> irq_state_inv st s
 2. \<And>e s. irq_state_next st s \<Longrightarrow> irq_state_next st s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma cap_delete_irq_state_inv':
  "\<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace>
   cap_delete slot
   \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>" by (wpsimp wp: rec_del_irq_state_inv simp: cap_delete_def) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> cap_delete slot \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
theory ADT_IF

lemma finalise_slot_irq_state_inv:
  "\<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace>
   finalise_slot p e
   \<lbrace>\<lambda>_ s. irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>" by (wpsimp wp: rec_del_irq_state_inv[folded validE_R_def] simp: finalise_slot_def) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irq_state_inv st and domain_sep_inv False sta and K (irq_is_recurring irq st)\<rbrace> finalise_slot p e \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
theory ADT_IF

lemma checked_insert_irq_state_of_state[wp]:
  "check_cap_at a b (check_cap_at c d (cap_insert e f g)) \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace>" by (wp | simp add: check_cap_at_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> check_cap_at a b (check_cap_at c d (cap_insert e f g)) \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
theory ADT_IF

lemma irq_state_inv_invoke_domain[wp]:
  "invoke_domain a b \<lbrace>irq_state_inv st\<rbrace>" apply (simp add: irq_state_inv_def[abs_def]) apply (rule hoare_pre) apply wps apply (wp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irq_state_inv st\<rbrace> invoke_domain a b \<lbrace>\<lambda>_. irq_state_inv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. irq_state_of_state st \<le> irq_state_of_state s \<and> irq_masks_of_state s = irq_masks_of_state st \<and> next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state s) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state s)\<rbrace> invoke_domain a b \<lbrace>\<lambda>_ s. irq_state_of_state st \<le> irq_state_of_state s \<and> irq_masks_of_state s = irq_masks_of_state st \<and> next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state s) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> invoke_domain a b \<lbrace>\<lambda>_ s. irq_state_of_state st \<le> irq_state_of_state s \<and> irq_masks_of_state s = irq_masks_of_state st \<and> next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state s) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state s)\<rbrace>
 2. \<And>s. irq_state_of_state st \<le> irq_state_of_state s \<and> irq_masks_of_state s = irq_masks_of_state st \<and> next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state s) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state s) \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P4 prev_s\<rbrace> invoke_domain a b \<lbrace>\<lambda>rv s'. irq_state_of_state st \<le> irq_state_of_state prev_s \<and> irq_masks_of_state prev_s = irq_masks_of_state st \<and> next_irq_state (Suc (irq_state_of_state prev_s)) (irq_masks_of_state prev_s) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state prev_s)\<rbrace>
 2. \<And>s. irq_state_of_state st \<le> irq_state_of_state s \<and> irq_masks_of_state s = irq_masks_of_state st \<and> next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state s) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state s) \<Longrightarrow> ?P4 s s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma do_reply_transfer_irq_state_inv_triv[wp]:
  "do_reply_transfer a b c d \<lbrace>irq_state_inv st\<rbrace>" by (wp irq_state_inv_triv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irq_state_inv st\<rbrace> do_reply_transfer a b c d \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>
theory ADT_IF

lemma set_domain_irq_state_inv_triv[wp]:
  "set_domain a b \<lbrace>irq_state_inv st\<rbrace>" by (wp irq_state_inv_triv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irq_state_inv st\<rbrace> set_domain a b \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>
theory ADT_IF

lemma use_validE_E:
  "\<lbrakk> (Inl r, s') \<in> fst (fa s); \<lbrace>P\<rbrace> fa -, \<lbrace>Q\<rbrace>; P s \<rbrakk> \<Longrightarrow> Q r s'" by (fastforce simp: validE_E_def validE_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(Inl r, s') \<in> fst (fa s); \<lbrace>P\<rbrace> fa -, \<lbrace>Q\<rbrace>; P s\<rbrakk> \<Longrightarrow> Q r s'
theory ADT_IF

lemma invoke_irq_control_noErr[wp]:
  "\<lbrace>\<top>\<rbrace> invoke_irq_control a -,\<lbrace>\<lambda>rv s :: det_state. Q rv s\<rbrace>" by (cases a; wpsimp simp: arch_invoke_irq_control_noErr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> invoke_irq_control a -, \<lbrace>Q\<rbrace>
theory ADT_IF

lemma invoke_untyped_irq_state_inv:
  "\<lbrace>irq_state_inv st and K (irq_is_recurring irq st)\<rbrace>
   invoke_untyped ui
   \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>" apply (cases ui, simp add: invoke_untyped_def mapM_x_def[symmetric]) apply (rule hoare_pre) apply (wp mapM_x_wp' whenE_wp reset_untyped_cap_irq_state_inv[where irq=irq]
         | rule irq_state_inv_triv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irq_state_inv st and K (irq_is_recurring irq st)\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8. ui = Retype x1 x2 x3 x4 x5 x6 x7 x8 \<Longrightarrow> \<lbrace>irq_state_inv st and (\<lambda>y. irq_is_recurring irq st)\<rbrace> doE y <- whenE x2 (reset_untyped_cap x1);
liftE (do cap <- get_cap x1;
y <- set_cap (UntypedCap x8 x3 (bits_of cap) (unat (x4 + (word_of_nat (length x7) << obj_bits_api x5 x6) - x3))) x1;
orefs <- retype_region x4 (length x7) x6 x5 x8;
y <- init_arch_objects x5 x4 (length x7) x6 orefs;
mapM_x (create_cap x5 x6 x1 x8) (zip x7 orefs)
od)
odE \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8. ui = Retype x1 x2 x3 x4 x5 x6 x7 x8 \<Longrightarrow> \<lbrace>?Q1 x1 x2 x3 x4 x5 x6 x7 x8\<rbrace> doE y <- whenE x2 (reset_untyped_cap x1);
liftE (do cap <- get_cap x1;
y <- set_cap (UntypedCap x8 x3 (bits_of cap) (unat (x4 + (word_of_nat (length x7) << obj_bits_api x5 x6) - x3))) x1;
orefs <- retype_region x4 (length x7) x6 x5 x8;
y <- init_arch_objects x5 x4 (length x7) x6 orefs;
mapM_x (create_cap x5 x6 x1 x8) (zip x7 orefs)
od)
odE \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>x1 x2 x3 x4 x5 x6 x7 x8 s. \<lbrakk>ui = Retype x1 x2 x3 x4 x5 x6 x7 x8; (irq_state_inv st and (\<lambda>y. irq_is_recurring irq st)) s\<rbrakk> \<Longrightarrow> ?Q1 x1 x2 x3 x4 x5 x6 x7 x8 s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma schedule_if_irq_state_inv:
  "schedule_if tc \<lbrace>irq_state_inv st\<rbrace>" by (wp irq_state_inv_triv
      | simp add: schedule_if_def activate_thread_def
      | wpc
      | wp (once) hoare_drop_imps)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irq_state_inv st\<rbrace> schedule_if tc \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>
theory ADT_IF

lemma irq_measure_if_inv:
  assumes irq_state:
    "\<And>st. \<lbrace>P st\<rbrace> f \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>,-"
  shows
    "\<lbrace>\<lambda>s. irq_measure_if_inv st s \<and> (irq_state_inv s s \<longrightarrow> P s s)\<rbrace> f \<lbrace>\<lambda>_. irq_measure_if_inv st\<rbrace>, -" apply (clarsimp simp: valid_def validE_R_def validE_def) apply (simp add: irq_measure_if_inv_def) apply (erule order_trans[rotated]) apply (simp add: irq_state_inv_refl) apply (drule use_validE_R, rule irq_state, assumption) apply (auto simp: irq_state_inv_def irq_measure_if_inv_def Let_def irq_measure_if_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. irq_measure_if_inv st s \<and> (irq_state_inv s s \<longrightarrow> P s s)\<rbrace> f \<lbrace>\<lambda>_. irq_measure_if_inv st\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s b r. \<lbrakk>(Inr r, b) \<in> fst (f s); irq_measure_if_inv st s; irq_state_inv s s \<longrightarrow> P s s\<rbrakk> \<Longrightarrow> irq_measure_if_inv st b proof (prove)
goal (1 subgoal):
 1. \<And>s b r. \<lbrakk>(Inr r, b) \<in> fst (f s); irq_measure_if s \<le> irq_measure_if st; irq_state_inv s s \<longrightarrow> P s s\<rbrakk> \<Longrightarrow> irq_measure_if b \<le> irq_measure_if st proof (prove)
goal (1 subgoal):
 1. \<And>s b r. \<lbrakk>(Inr r, b) \<in> fst (f s); irq_state_inv s s \<longrightarrow> P s s\<rbrakk> \<Longrightarrow> irq_measure_if b \<le> irq_measure_if s proof (prove)
goal (1 subgoal):
 1. \<And>s b r. \<lbrakk>(Inr r, b) \<in> fst (f s); P s s\<rbrakk> \<Longrightarrow> irq_measure_if b \<le> irq_measure_if s proof (prove)
goal (1 subgoal):
 1. \<And>s b r. \<lbrakk>P s s; irq_state_inv s b\<rbrakk> \<Longrightarrow> irq_measure_if b \<le> irq_measure_if s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma irq_measure_if_inv_old:
  assumes irq_state:
    "\<And>st. \<lbrace>irq_state_inv st and Q\<rbrace> f \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, -"
  shows
    "\<lbrace>irq_measure_if_inv st and Q\<rbrace> f \<lbrace>\<lambda>_. irq_measure_if_inv st\<rbrace>, -" by (wpsimp wp: irq_measure_if_inv irq_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irq_measure_if_inv st and Q\<rbrace> f \<lbrace>\<lambda>_. irq_measure_if_inv st\<rbrace>, -
theory ADT_IF

lemma irq_measure_if_inv':
  assumes irq_state:
    "\<And>st. \<lbrace>P st\<rbrace> f \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>"
  shows
    "\<lbrace>\<lambda>s. irq_measure_if_inv st s \<and> (irq_state_inv s s \<longrightarrow> P s s)\<rbrace> f \<lbrace>\<lambda>_. irq_measure_if_inv st\<rbrace>" apply (clarsimp simp: valid_def irq_measure_if_inv_def irq_state_inv_refl) apply (erule le_trans[rotated]) apply (drule(1) use_valid[OF _ irq_state]) apply (clarsimp simp: irq_measure_if_def Let_def irq_state_inv_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. irq_measure_if_inv st s \<and> (irq_state_inv s s \<longrightarrow> P s s)\<rbrace> f \<lbrace>\<lambda>_. irq_measure_if_inv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); irq_measure_if s \<le> irq_measure_if st; P s s\<rbrakk> \<Longrightarrow> irq_measure_if b \<le> irq_measure_if st proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s s\<rbrakk> \<Longrightarrow> irq_measure_if b \<le> irq_measure_if s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s s; irq_state_inv s b\<rbrakk> \<Longrightarrow> irq_measure_if b \<le> irq_measure_if s proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>P s s; irq_state_of_state s \<le> irq_state_of_state b; irq_masks_of_state b = irq_masks_of_state s; next_irq_state (Suc (irq_state_of_state b)) (irq_masks_of_state s) = next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state s)\<rbrakk> \<Longrightarrow> next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state s) - Suc (irq_state_of_state b) \<le> next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state s) - Suc (irq_state_of_state s) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma irq_measure_if_inv_old':
  assumes irq_state:
    "\<And>st. \<lbrace>irq_state_inv st and Q\<rbrace> f \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>"
  shows
    "\<lbrace>irq_measure_if_inv st and Q\<rbrace> f \<lbrace>\<lambda>_. irq_measure_if_inv st\<rbrace>" by (wpsimp wp: irq_measure_if_inv' irq_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irq_measure_if_inv st and Q\<rbrace> f \<lbrace>\<lambda>_. irq_measure_if_inv st\<rbrace>
theory ADT_IF

lemma irq_state_inv_irq_is_recurring:
  "irq_state_inv sta s \<Longrightarrow> irq_is_recurring irq sta = irq_is_recurring irq s" by (clarsimp simp: irq_is_recurring_def irq_state_inv_def is_irq_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_state_inv sta s \<Longrightarrow> irq_is_recurring irq sta = irq_is_recurring irq s
theory ADT_IF

lemma schedule_if_irq_measure_if:
  "(r, b) \<in> fst (schedule_if uc i_s) \<Longrightarrow> irq_measure_if b \<le> irq_measure_if i_s" apply (fold irq_measure_if_inv_def) apply (erule use_valid[OF _ irq_measure_if_inv'] | wp schedule_if_irq_state_inv | simp)+ apply (simp add: irq_measure_if_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (r, b) \<in> fst (schedule_if uc i_s) \<Longrightarrow> irq_measure_if b \<le> irq_measure_if i_s proof (prove)
goal (1 subgoal):
 1. (r, b) \<in> fst (schedule_if uc i_s) \<Longrightarrow> irq_measure_if_inv i_s b proof (prove)
goal (1 subgoal):
 1. irq_measure_if_inv i_s i_s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma schedule_if_next_irq_state_of_state:
  "(r, b) \<in> fst (schedule_if uc i_s) \<Longrightarrow> next_irq_state_of_state b = next_irq_state_of_state i_s" apply (erule use_valid) apply (rule_tac Q="\<lambda>_. irq_state_inv i_s" in hoare_strengthen_post) apply (wp schedule_if_irq_state_inv) apply (auto simp: irq_state_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (r, b) \<in> fst (schedule_if uc i_s) \<Longrightarrow> next_irq_state_of_state b = next_irq_state_of_state i_s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P\<rbrace> schedule_if uc \<lbrace>\<lambda>a b. next_irq_state_of_state b = next_irq_state_of_state i_s\<rbrace>
 2. ?P i_s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P\<rbrace> schedule_if uc \<lbrace>\<lambda>_. irq_state_inv i_s\<rbrace>
 2. \<And>rv s. irq_state_inv i_s s \<Longrightarrow> next_irq_state_of_state s = next_irq_state_of_state i_s
 3. ?P i_s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. irq_state_inv i_s s \<Longrightarrow> next_irq_state_of_state s = next_irq_state_of_state i_s
 2. irq_state_inv i_s i_s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma next_irq_state_of_state_triv:
  assumes masks: "\<And>P. f \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace>"
  assumes sta: "\<And>P. f \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace>"
  shows "f \<lbrace>\<lambda>s. P (next_irq_state_of_state s)\<rbrace>" apply (clarsimp simp: valid_def) apply (frule (1) use_valid[OF _ masks]) apply (erule (1) use_valid[OF _ sta]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (next_irq_state_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (next_irq_state_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P (next_irq_state_of_state s); (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> P (next_irq_state_of_state b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P (next_irq_state_of_state s); (a, b) \<in> fst (f s); P (next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state b))\<rbrakk> \<Longrightarrow> P (next_irq_state_of_state b) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma interrupted_modes_KernelEntry[simp]:
  "interrupted_modes (KernelEntry e) = (e = Interrupt)" by (case_tac e, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. interrupted_modes (KernelEntry e) = (e = Interrupt)
theory ADT_IF

lemma rah4:
  "b < a \<Longrightarrow> 4 * (a - Suc b) + 3 < 4 * (a - b)" by (simp add: Suc_le_lessD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b < a \<Longrightarrow> 4 * (a - Suc b) + 3 < 4 * (a - b)