kings-crown/FVELER_Isabelle huggingface dataset:
theory Finalise_DR

lemma no_cdt_loop_mloop:
  "no_mloop m \<Longrightarrow> m x \<noteq> Some x" apply (rule notI) apply (simp add: no_mloop_def cdt_parent_rel_def del: split_paired_All) apply (drule_tac x=x in spec) apply (erule notE, rule r_into_trancl) apply (simp add: is_cdt_parent_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_mloop m \<Longrightarrow> m x \<noteq> Some x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_mloop m; m x = Some x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p. (p, p) \<notin> {(p, c). CSpaceAcc_A.is_cdt_parent m p c}\<^sup>+; m x = Some x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m x = Some x; (x, x) \<notin> {(p, c). CSpaceAcc_A.is_cdt_parent m p c}\<^sup>+\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m x = Some x \<Longrightarrow> (x, x) \<in> {(p, c). CSpaceAcc_A.is_cdt_parent m p c} proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma set_cdt_list_modify:
  "set_cdt_list c = modify (\<lambda>s. s \<lparr> cdt_list := c \<rparr>)" by (simp add: set_cdt_list_def modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_cdt_list c = modify (cdt_list_update (\<lambda>_. c))
theory Finalise_DR

lemma finalise_zombie:
  "is_zombie cap \<Longrightarrow> finalise_cap cap final
        = do assert final; return (cap, cap.NullCap) od" by (clarsimp simp add: is_cap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_zombie cap \<Longrightarrow> CSpace_A.finalise_cap cap final = do assert final;
return (cap, cap.NullCap)
od
theory Finalise_DR

lemma corres_assert_rhs:
  "(F \<Longrightarrow> corres_underlying sr False False r P P' f (g ()))
    \<Longrightarrow> corres_underlying sr False False r P (\<lambda>s. F \<longrightarrow> P' s) f (assert F >>= g)" by (cases F, simp_all add: corres_fail)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (F \<Longrightarrow> corres_underlying sr False False r P P' f (g ())) \<Longrightarrow> corres_underlying sr False False r P (\<lambda>s. F \<longrightarrow> P' s) f (assert F >>= g)
theory Finalise_DR

lemma corres_drop_cutMon:
  "corres_underlying sr False False r P P' f g
     \<Longrightarrow> corres_underlying sr False False r P P' f (cutMon Q g)" apply (simp add: corres_underlying_def cutMon_def fail_def
            split: if_split) apply (clarsimp simp: split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr False False r P P' f g \<Longrightarrow> corres_underlying sr False False r P P' f (cutMon Q g) proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (g s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<Longrightarrow> \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> Q s' \<longrightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (g s'). \<exists>(ra, t)\<in>fst (f s). (t, t') \<in> sr \<and> r ra r') proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma corres_drop_cutMon_bind:
  "corres_underlying sr False False r P P' f (g >>= h)
     \<Longrightarrow> corres_underlying sr False False r P P' f (cutMon Q g >>= h)" apply (simp add: corres_underlying_def cutMon_def fail_def bind_def
            split: if_split) apply (clarsimp simp: split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr False False r P P' f (g >>= h) \<Longrightarrow> corres_underlying sr False False r P P' f (cutMon Q g >>= h) proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>y\<in>fst (g s'). \<forall>x\<in>fst (case y of (x, xa) \<Rightarrow> h x xa). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<Longrightarrow> \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> Q s' \<longrightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>y\<in>fst (g s'). \<forall>(r', t')\<in>fst (case y of (x, xa) \<Rightarrow> h x xa). \<exists>(ra, t)\<in>fst (f s). (t, t') \<in> sr \<and> r ra r') proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma underlying_memory_irq_state_independent[intro!, simp]:
  "underlying_memory (s\<lparr>irq_state := f (irq_state s)\<rparr>)
   = underlying_memory s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. underlying_memory (s\<lparr>irq_state := f (irq_state s)\<rparr>) = underlying_memory s
theory Finalise_DR

lemma get_tcb_mrs_irq_state_independent[intro!, simp]:
  "get_tcb_mrs (s\<lparr>irq_state := f (irq_state s)\<rparr>)
   = get_tcb_mrs s" by (auto simp: get_tcb_mrs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_tcb_mrs (s\<lparr>irq_state := f (irq_state s)\<rparr>) = get_tcb_mrs s
theory Finalise_DR

lemma transform_full_intent_irq_state_independent[intro!, simp]:
  "transform_full_intent (s\<lparr>irq_state := f (irq_state s)\<rparr>)
   = transform_full_intent s" by (rule ext, rule ext, simp add: transform_full_intent_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_full_intent (s\<lparr>irq_state := f (irq_state s)\<rparr>) = transform_full_intent s
theory Finalise_DR

lemma transform_tcb_irq_state_independent[intro!, simp]:
  "transform_tcb (s\<lparr>irq_state := f (irq_state s)\<rparr>)
   = transform_tcb s" by (rule ext, rule ext, rule ext, simp add: transform_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_tcb (s\<lparr>irq_state := f (irq_state s)\<rparr>) = transform_tcb s
theory Finalise_DR

lemma transform_object_irq_state_independent[intro!, simp]:
  "transform_object (s \<lparr> irq_state := f (irq_state s) \<rparr>)
   = transform_object s" by (rule ext, rule ext, rule ext,
      simp add: transform_object_def
           cong: option.case_cong
           split: Structures_A.kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_object (s\<lparr>irq_state := f (irq_state s)\<rparr>) = transform_object s
theory Finalise_DR

lemma transform_objects_irq_state_independent[intro!, simp]:
  "transform_objects (s \<lparr> machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr> \<rparr>)
   = transform_objects s" by (simp add: transform_objects_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_objects (update_machine (machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>) s) = transform_objects s
theory Finalise_DR

lemma transform_irq_state_independent[intro!, simp]:
  "transform (s \<lparr> machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr> \<rparr>)
   = transform s" by (simp add: transform_def transform_current_thread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform (update_machine (machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>) s) = transform s
theory Finalise_DR

lemma transform_work_units_independent[intro!, simp]:
  "transform (s \<lparr> work_units_completed := f (work_units_completed s) \<rparr>)
   = transform s" apply (simp add: transform_def transform_current_thread_def transform_objects_def transform_cdt_def transform_asid_table_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform (work_units_completed_update (\<lambda>_. f (work_units_completed s)) s) = transform s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma transform_work_units_then_irq_state_independent[intro!, simp]:
  "transform (s \<lparr> work_units_completed := g (work_units_completed s) \<rparr>
                \<lparr> machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr>\<rparr>) =
   transform s" apply (simp add: transform_def transform_current_thread_def transform_objects_def transform_cdt_def transform_asid_table_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform (update_machine (machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>) (work_units_completed_update (\<lambda>_. g (work_units_completed s)) s)) = transform s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma throw_or_return_preemption_corres:
  "dcorres (dc \<oplus> dc) P P'
       (Monads_D.throw \<sqinter> returnOk ())
       preemption_point" apply (simp add: preemption_point_def) apply (auto simp: preemption_point_def o_def gets_def liftE_def whenE_def getActiveIRQ_def
                    corres_underlying_def select_def bind_def get_def bindE_def select_f_def modify_def
                    alternative_def throwError_def returnOk_def return_def lift_def
                    put_def do_machine_op_def
                    update_work_units_def wrap_ext_bool_det_ext_ext_def work_units_limit_def
                    work_units_limit_reached_def OR_choiceE_def reset_work_units_def mk_ef_def
           split: option.splits kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) P P' (throw \<sqinter> returnOk ()) Exceptions_A.preemption_point proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) P P' (throw \<sqinter> returnOk ()) (doE y <- liftE update_work_units;
OR_choiceE work_units_limit_reached (doE y <- liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (\<lambda>y. throwError ())
odE) (returnOk ())
odE) proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma cutMon_fail:
  "cutMon P fail = fail" by (simp add: cutMon_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cutMon P fail = fail
theory Finalise_DR

lemma invs_weak_valid_mdb:
  "invs s \<longrightarrow> weak_valid_mdb s" by (simp add: weak_valid_mdb_def invs_def valid_mdb_def valid_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<longrightarrow> weak_valid_mdb s
theory Finalise_DR

lemma invs_valid_idle_strg:
  "invs s \<longrightarrow> valid_idle s" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<longrightarrow> valid_idle s
theory Finalise_DR

lemma cutMon_validE_R_drop:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> cutMon R f \<lbrace>Q\<rbrace>,-" by (simp add: validE_R_def validE_def cutMon_valid_drop)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - \<Longrightarrow> \<lbrace>P\<rbrace> cutMon R f \<lbrace>Q\<rbrace>, -
theory Finalise_DR

lemma preemption_point_idle_thread[wp]: "\<lbrace> \<lambda>s. P (idle_thread s) \<rbrace> preemption_point \<lbrace> \<lambda>_ s. P (idle_thread s) \<rbrace>" apply (simp add: preemption_point_def OR_choiceE_def) apply (wpsimp wp: hoare_drop_imps dxo_wp_weak[where P="\<lambda>s. P (idle_thread s)"]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> Exceptions_A.preemption_point \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> doE y <- liftE (do_extended_op update_work_units);
ex <- liftE get;
(rv, uu_) <- liftE (select_f (mk_ef (wrap_ext_bool work_units_limit_reached ex)));
if rv then doE y <- liftE (do_extended_op reset_work_units);
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (\<lambda>y. throwError ())
odE else returnOk ()
odE \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma rec_del_idle_thread[wp]:
  "\<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> rec_del args \<lbrace>\<lambda>rv s::'a::state_ext state. P (idle_thread s)\<rbrace>" by (wp rec_del_preservation)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> rec_del args \<lbrace>\<lambda>rv s. P (idle_thread s)\<rbrace>
theory Finalise_DR

lemma transform_work_units_completed_update[simp]: "transform (s\<lparr> work_units_completed := a \<rparr>) = transform s" by (auto simp: transform_def transform_cdt_def transform_current_thread_def transform_asid_table_def transform_objects_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform (work_units_completed_update (\<lambda>_. a) s) = transform s
theory Finalise_DR

lemma zombie_is_cap_toE_pre2:
  "\<lbrakk> s \<turnstile> cap.Zombie ptr zbits n; m < n \<rbrakk>
     \<Longrightarrow> (ptr, nat_to_cref (zombie_cte_bits zbits) m) \<in> cte_refs (cap.Zombie ptr zbits n) irqn" apply (clarsimp simp add: valid_cap_def cap_aligned_def) apply (clarsimp split: option.split_asm) apply (simp add: unat_of_bl_nat_to_cref) apply (simp add: nat_to_cref_def word_bits_conv) apply (simp add: unat_of_bl_nat_to_cref) apply (simp add: nat_to_cref_def word_bits_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> Zombie ptr zbits n; m < n\<rbrakk> \<Longrightarrow> (ptr, nat_to_cref (zombie_cte_bits zbits) m) \<in> cte_refs (Zombie ptr zbits n) irqn proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < n; is_aligned ptr (case zbits of None \<Rightarrow> obj_bits (TCB undefined) | Some x \<Rightarrow> cte_level_bits + x); (case zbits of None \<Rightarrow> obj_bits (TCB undefined) | Some x \<Rightarrow> cte_level_bits + x) < word_bits; case zbits of None \<Rightarrow> tcb_at ptr s \<and> n \<le> 5 | Some b \<Rightarrow> cap_table_at b ptr s \<and> n \<le> 2 ^ b \<and> b \<noteq> 0\<rbrakk> \<Longrightarrow> length (nat_to_cref (zombie_cte_bits zbits) m) = zombie_cte_bits zbits \<and> unat (of_bl (nat_to_cref (zombie_cte_bits zbits) m)) < n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>9 < word_bits; m < n; zbits = None; is_aligned ptr 9; tcb_at ptr s; n \<le> 5\<rbrakk> \<Longrightarrow> length (nat_to_cref 3 m) = 3 \<and> unat (of_bl (nat_to_cref 3 m)) < n
 2. \<And>x2. \<lbrakk>cte_level_bits + x2 < word_bits; m < n; zbits = Some x2; is_aligned ptr (cte_level_bits + x2); cap_table_at x2 ptr s; n \<le> 2 ^ x2; 0 < x2\<rbrakk> \<Longrightarrow> length (nat_to_cref x2 m) = x2 \<and> unat (of_bl (nat_to_cref x2 m)) < n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>9 < word_bits; m < n; zbits = None; is_aligned ptr 9; tcb_at ptr s; n \<le> 5\<rbrakk> \<Longrightarrow> length (nat_to_cref 3 m) = 3
 2. \<And>x2. \<lbrakk>cte_level_bits + x2 < word_bits; m < n; zbits = Some x2; is_aligned ptr (cte_level_bits + x2); cap_table_at x2 ptr s; n \<le> 2 ^ x2; 0 < x2\<rbrakk> \<Longrightarrow> length (nat_to_cref x2 m) = x2 \<and> unat (of_bl (nat_to_cref x2 m)) < n proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>cte_level_bits + x2 < word_bits; m < n; zbits = Some x2; is_aligned ptr (cte_level_bits + x2); cap_table_at x2 ptr s; n \<le> 2 ^ x2; 0 < x2\<rbrakk> \<Longrightarrow> length (nat_to_cref x2 m) = x2 \<and> unat (of_bl (nat_to_cref x2 m)) < n proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>cte_level_bits + x2 < word_bits; m < n; zbits = Some x2; is_aligned ptr (cte_level_bits + x2); cap_table_at x2 ptr s; n \<le> 2 ^ x2; 0 < x2\<rbrakk> \<Longrightarrow> length (nat_to_cref x2 m) = x2 proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma corres_note_assumption:
  "\<lbrakk> F; corres_underlying sr fl fl' r P P' f g \<rbrakk>
        \<Longrightarrow> corres_underlying sr fl fl' r (\<lambda>s. F \<longrightarrow> P s) P' f g" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F; corres_underlying sr fl fl' r P P' f g\<rbrakk> \<Longrightarrow> corres_underlying sr fl fl' r (\<lambda>s. F \<longrightarrow> P s) P' f g
theory Finalise_DR

lemma nat_split_conv_to_if:
  "(case n of 0 \<Rightarrow> a | Suc nat' \<Rightarrow> f nat') = (if n = 0 then a else f (n - 1))" by (auto split: nat.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case n of 0 \<Rightarrow> a | Suc nat' \<Rightarrow> f nat') = (if n = 0 then a else f (n - 1))
theory Finalise_DR

lemma preemption_point_valid_etcbs[wp]: "\<lbrace> valid_etcbs \<rbrace> preemption_point \<lbrace> \<lambda>_. valid_etcbs \<rbrace>" apply (clarsimp simp: preemption_point_def) apply (auto simp: valid_def o_def gets_def liftE_def whenE_def getActiveIRQ_def
                    corres_underlying_def select_def bind_def get_def bindE_def select_f_def modify_def
                    alternative_def throwError_def returnOk_def return_def lift_def
                    put_def do_machine_op_def
                    update_work_units_def wrap_ext_bool_det_ext_ext_def work_units_limit_def
                    work_units_limit_reached_def OR_choiceE_def reset_work_units_def mk_ef_def
           split: option.splits kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> Exceptions_A.preemption_point \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> doE y <- liftE update_work_units;
OR_choiceE work_units_limit_reached (doE y <- liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (\<lambda>y. throwError ())
odE) (returnOk ())
odE \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma rec_del_valid_etcbs[wp]:
  "\<lbrace> valid_etcbs \<rbrace> rec_del args \<lbrace>\<lambda>_. valid_etcbs \<rbrace>" by (wp rec_del_preservation | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> rec_del args \<lbrace>\<lambda>_. valid_etcbs\<rbrace>
theory CNode_DR

lemma corres_assert_lhs:
  "(F \<Longrightarrow> corres_underlying sr False False r P P' (f ()) g)
    \<Longrightarrow> corres_underlying sr False False r (\<lambda>s. F \<and> P s) P' (assert F >>= f) g" by (cases F; simp add: corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (F \<Longrightarrow> corres_underlying sr False False r P P' (f ()) g) \<Longrightarrow> corres_underlying sr False False r (\<lambda>s. F \<and> P s) P' (assert F >>= f) g
theory CNode_DR

lemma ex_cte_cap_to_not_idle:
  "\<lbrakk> ex_cte_cap_wp_to P p s; valid_global_refs s;
           valid_idle s; valid_irq_node s \<rbrakk> \<Longrightarrow> fst p \<noteq> idle_thread s" apply (cases p) apply (clarsimp simp: ex_cte_cap_wp_to_def cte_wp_at_caps_of_state) apply (drule(1) valid_global_refsD2) apply (case_tac cap, simp_all add: cap_range_def global_refs_def) apply (rename_tac word) apply (clarsimp simp: valid_idle_def valid_irq_node_def pred_tcb_at_def
                        obj_at_def is_cap_table_def) apply (drule_tac x=word in spec, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ex_cte_cap_wp_to P p s; valid_global_refs s; valid_idle s; valid_irq_node s\<rbrakk> \<Longrightarrow> fst p \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>ex_cte_cap_wp_to P p s; valid_global_refs s; valid_idle s; valid_irq_node s; p = (a, b)\<rbrakk> \<Longrightarrow> fst p \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<And>b aa ba cap. \<lbrakk>valid_global_refs s; valid_idle s; valid_irq_node s; p = (idle_thread s, b); caps_of_state s (aa, ba) = Some cap; P cap; (idle_thread s, b) \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b aa ba cap. \<lbrakk>valid_global_refs s; valid_idle s; valid_irq_node s; p = (idle_thread s, b); P cap; (idle_thread s, b) \<in> cte_refs cap (interrupt_irq_node s); global_refs s \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap x10. \<lbrakk>valid_global_refs s; valid_idle s; valid_irq_node s; p = (interrupt_irq_node s x10, []); P (IRQHandlerCap x10); idle_thread s = interrupt_irq_node s x10; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cap word. \<lbrakk>valid_global_refs s; valid_idle s; valid_irq_node s; p = (interrupt_irq_node s word, []); P (IRQHandlerCap word); idle_thread s = interrupt_irq_node s word; cap = IRQHandlerCap word\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>word tcb. \<lbrakk>valid_global_refs s; p = (idle_thread_ptr, []); P (IRQHandlerCap word); idle_thread s = idle_thread_ptr; interrupt_irq_node s word = idle_thread_ptr; inj (interrupt_irq_node s); \<forall>irq. \<exists>ko. kheap s (interrupt_irq_node s irq) = Some ko \<and> (case ko of kernel_object.CNode sz cs \<Rightarrow> 0 = sz \<and> well_formed_cnode_n 0 cs | _ \<Rightarrow> False); kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CNode_DR

lemma option_return_modify_modify:
  "case_option (return ()) (\<lambda>x. modify (f x))
       = (\<lambda>opt. modify (case_option id f opt))" by (auto split: option.split simp: modify_id_return)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. case_option (return ()) (\<lambda>x. modify (f x)) = (\<lambda>opt. modify (case opt of None \<Rightarrow> id | Some x \<Rightarrow> f x))
theory CNode_DR

lemma update_cdt_modify:
  "update_cdt f = modify (cdt_update f)" apply (simp add: update_cdt_def set_cdt_modify gets_fold_into_modify) apply (rule ext, simp add: simpler_modify_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_cdt f = modify (cdt_update f) proof (prove)
goal (1 subgoal):
 1. modify (\<lambda>s. s\<lparr>cdt := f (cdt s)\<rparr>) = modify (cdt_update f) proof (prove)
goal:
No subgoals!