kings-crown/FVELER_Isabelle huggingface dataset:
theory EmptyFail_AI

lemma spec_empty_fail_bindE:
  "\<lbrakk>spec_empty_fail f s; \<And>x. empty_fail (g x)\<rbrakk>
    \<Longrightarrow> spec_empty_fail (f >>=E g) s" by (fastforce simp: bindE_def lift_def split: sum.splits intro: spec_empty_fail_bind)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec_empty_fail f s; \<And>x. empty_fail (g x)\<rbrakk> \<Longrightarrow> spec_empty_fail (f >>=E g) s
theory EmptyFail_AI

lemma spec_empty_fail_bind':
  "\<lbrakk>spec_empty_fail f s; \<And>x s'. (x, s') \<in> fst (f s) \<Longrightarrow> spec_empty_fail (g x) s'\<rbrakk>
    \<Longrightarrow> spec_empty_fail (f >>= g) s" by (fastforce simp: bind_def spec_empty_fail_def image_def split_def split_paired_Bex intro: prod_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec_empty_fail f s; \<And>x s'. (x, s') \<in> fst (f s) \<Longrightarrow> spec_empty_fail (g x) s'\<rbrakk> \<Longrightarrow> spec_empty_fail (f >>= g) s
theory EmptyFail_AI

lemma spec_empty_fail_bindE':
  "\<lbrakk>spec_empty_fail f s; \<And>x s'. (Inr x, s') \<in> fst (f s) \<Longrightarrow> spec_empty_fail (g x) s'\<rbrakk>
    \<Longrightarrow> spec_empty_fail (f >>=E g) s" apply (simp add: bindE_def) apply (rule spec_empty_fail_bind') apply simp apply (clarsimp simp: lift_def split: sum.splits | rule conjI | wp drop_spec_empty_fail)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec_empty_fail f s; \<And>x s'. (Inr x, s') \<in> fst (f s) \<Longrightarrow> spec_empty_fail (g x) s'\<rbrakk> \<Longrightarrow> spec_empty_fail (f >>=E g) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec_empty_fail f s; \<And>x s'. (Inr x, s') \<in> fst (f s) \<Longrightarrow> spec_empty_fail (g x) s'\<rbrakk> \<Longrightarrow> spec_empty_fail (f >>= lift g) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>spec_empty_fail f s; \<And>x s'. (Inr x, s') \<in> fst (f s) \<Longrightarrow> spec_empty_fail (g x) s'\<rbrakk> \<Longrightarrow> spec_empty_fail f s
 2. \<And>x s'. \<lbrakk>spec_empty_fail f s; \<And>x s'. (Inr x, s') \<in> fst (f s) \<Longrightarrow> spec_empty_fail (g x) s'; (x, s') \<in> fst (f s)\<rbrakk> \<Longrightarrow> spec_empty_fail (lift g x) s' proof (prove)
goal (1 subgoal):
 1. \<And>x s'. \<lbrakk>spec_empty_fail f s; \<And>x s'. (Inr x, s') \<in> fst (f s) \<Longrightarrow> spec_empty_fail (g x) s'; (x, s') \<in> fst (f s)\<rbrakk> \<Longrightarrow> spec_empty_fail (lift g x) s' proof (prove)
goal:
No subgoals!
theory EmptyFail_AI

lemma spec_empty_returnOk: "spec_empty_fail (returnOk x) s" apply (rule drop_spec_empty_fail) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_empty_fail (returnOk x) s proof (prove)
goal (1 subgoal):
 1. empty_fail (returnOk x) proof (prove)
goal:
No subgoals!
theory EmptyFail_AI

lemma spec_empty_whenE: "spec_empty_fail f s \<Longrightarrow> spec_empty_fail (whenE P f) s" apply (simp add: whenE_def) apply (clarsimp simp: spec_empty_returnOk) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_empty_fail f s \<Longrightarrow> spec_empty_fail (whenE P f) s proof (prove)
goal (1 subgoal):
 1. spec_empty_fail f s \<Longrightarrow> \<not> P \<longrightarrow> spec_empty_fail (returnOk ()) s proof (prove)
goal:
No subgoals!
theory EmptyFail_AI

lemma use_spec_empty_fail: "(\<And>s. spec_empty_fail f s) \<Longrightarrow> empty_fail f" apply (simp add: empty_fail_def spec_empty_fail_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. spec_empty_fail f s) \<Longrightarrow> empty_fail f proof (prove)
goal:
No subgoals!
theory EmptyFail_AI

lemma get_extra_cptrs_empty_fail[wp]:
  fixes a b
  shows "empty_fail (get_extra_cptrs a b :: (cap_ref list, 'state_ext) s_monad)" apply (simp add: get_extra_cptrs_def) apply (cases a) apply (simp | wp loadWord_empty_fail load_word_offs_empty_fail)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (get_extra_cptrs a b) proof (prove)
goal (1 subgoal):
 1. empty_fail (rec_option (\<lambda>mi. return []) (\<lambda>buf mi. liftM (map data_to_cptr) (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)])) a b) proof (prove)
goal (2 subgoals):
 1. a = None \<Longrightarrow> empty_fail (rec_option (\<lambda>mi. return []) (\<lambda>buf mi. liftM (map data_to_cptr) (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)])) a b)
 2. \<And>aa. a = Some aa \<Longrightarrow> empty_fail (rec_option (\<lambda>mi. return []) (\<lambda>buf mi. liftM (map data_to_cptr) (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)])) a b) proof (prove)
goal:
No subgoals!
theory EmptyFail_AI

lemma decode_read_registers_empty_fail[wp]:
  "empty_fail (decode_read_registers data (ThreadCap p))" by (simp add: decode_read_registers_def split: list.splits cap.splits | wp | intro allI impI conjI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (decode_read_registers data (ThreadCap p))
theory EmptyFail_AI

lemma decode_write_registers_empty_fail[wp]:
  "empty_fail (decode_write_registers data (ThreadCap p))" by (simp add: decode_write_registers_def split: list.splits cap.splits | wp | intro allI impI conjI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (decode_write_registers data (ThreadCap p))
theory EmptyFail_AI

lemma decode_copy_registers_empty_fail[wp]:
  "empty_fail (decode_copy_registers data (ThreadCap p) ec)" by (simp add: decode_copy_registers_def split: list.splits cap.splits | wp | intro allI impI conjI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (decode_copy_registers data (ThreadCap p) ec)
theory EmptyFail_AI

lemma alternative_empty_fail[wp]:
  "empty_fail f \<or> empty_fail g \<Longrightarrow> empty_fail (f \<sqinter> g)" by (auto simp: alternative_def empty_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<or> empty_fail g \<Longrightarrow> empty_fail (f \<sqinter> g)
theory EmptyFail_AI

lemma OR_choice_empty_fail[wp]:
  "\<lbrakk>empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> empty_fail (OR_choice c f g)" by (simp add: OR_choice_def mk_ef_def split_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> empty_fail (OR_choice c f g)
theory EmptyFail_AI

lemma OR_choiceE_empty_fail[wp]:
  "\<lbrakk>empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> empty_fail (OR_choiceE c f g)" by (simp add: OR_choiceE_def mk_ef_def split_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail f; empty_fail g\<rbrakk> \<Longrightarrow> empty_fail (OR_choiceE c f g)
theory EmptyFail_AI

lemma rec_del_empty_fail[wp]:
  "empty_fail (rec_del call :: (bool * cap, 'state_ext) p_monad)" apply (simp add: empty_fail_def) apply (rule allI) apply (rule rec_del_spec_empty_fail[simplified spec_empty_fail_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (rec_del call) proof (prove)
goal (1 subgoal):
 1. \<forall>s. fst (rec_del call s) = {} \<longrightarrow> snd (rec_del call s) proof (prove)
goal (1 subgoal):
 1. \<And>s. fst (rec_del call s) = {} \<longrightarrow> snd (rec_del call s) proof (prove)
goal:
No subgoals!
theory EmptyFail_AI

lemma cap_revoke_empty_fail[wp]:
  "\<And>slot. empty_fail (cap_revoke slot :: (unit, 'state_ext) p_monad)" apply (simp add: empty_fail_def) apply (rule allI) apply (rule cap_revoke_spec_empty_fail[simplified spec_empty_fail_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>slot. empty_fail (cap_revoke slot) proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<forall>s. fst (cap_revoke slot s) = {} \<longrightarrow> snd (cap_revoke slot s) proof (prove)
goal (1 subgoal):
 1. \<And>slot s. fst (cap_revoke slot s) = {} \<longrightarrow> snd (cap_revoke slot s) proof (prove)
goal:
No subgoals!
theory EmptyFail_AI

lemma schedule_empty_fail'[intro!, wp, simp]:
  "empty_fail (schedule :: (unit,det_ext) s_monad)" apply (simp add: schedule_def schedule_switch_thread_fastfail_def) apply (wp | clarsimp split: scheduler_action.splits|
            intro impI conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail schedule proof (prove)
goal (1 subgoal):
 1. empty_fail (do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> ct = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- if ct \<noteq> it then return (target_prio < ct_prio) else return True;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od) (do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od)
od) proof (prove)
goal:
No subgoals!
theory EmptyFail_AI

lemma call_kernel_empty_fail': "empty_fail (call_kernel a :: (unit,unit) s_monad)" apply (simp add: call_kernel_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (call_kernel a) proof (prove)
goal (1 subgoal):
 1. empty_fail (do y <- handle_event a <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od));
y <- schedule;
activate_thread
od) proof (prove)
goal:
No subgoals!
theory EmptyFail_AI

lemma call_kernel_empty_fail: "empty_fail (call_kernel a :: (unit,det_ext) s_monad)" apply (simp add: call_kernel_def) by (wp|simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (call_kernel a) proof (prove)
goal (1 subgoal):
 1. empty_fail (do y <- handle_event a <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od));
y <- schedule;
activate_thread
od)
theory ArchEmptyFail_AI

lemma decode_tcb_invocation_empty_fail[wp]:
  "empty_fail (decode_tcb_invocation a b (ThreadCap p) d e)" by (simp add: decode_tcb_invocation_def split: invocation_label.splits | wp | wpc | intro conjI impI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (decode_tcb_invocation a b (ThreadCap p) d e)
theory BCorres2_AI

lemma update_restart_pc_bcorres[wp]:
  "bcorres (update_restart_pc t) (update_restart_pc t)" by (wp
      | clarsimp simp: update_restart_pc_def as_user_def bind_select_f_bind'
                split: prod.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (update_restart_pc t) (update_restart_pc t)
theory BCorres2_AI

lemma ef_mk_ef: "empty_fail f \<Longrightarrow> mk_ef (f s) = f s" apply (clarsimp simp add: empty_fail_def mk_ef_def) apply (drule_tac x=s in spec) apply (case_tac "f s") apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> mk_ef (f s) = f s proof (prove)
goal (1 subgoal):
 1. \<forall>s. fst (f s) = {} \<longrightarrow> snd (f s) \<Longrightarrow> (fst (f s), fst (f s) = {} \<or> snd (f s)) = f s proof (prove)
goal (1 subgoal):
 1. fst (f s) = {} \<longrightarrow> snd (f s) \<Longrightarrow> (fst (f s), fst (f s) = {} \<or> snd (f s)) = f s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>fst (f s) = {} \<longrightarrow> snd (f s); f s = (a, b)\<rbrakk> \<Longrightarrow> (fst (f s), fst (f s) = {} \<or> snd (f s)) = f s proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma all_but_obvious: "all_but_exst (\<lambda>a b c d e f g h i.
                    x = \<lparr>kheap = a, cdt = b, is_original_cap = c,
                     cur_thread = d, idle_thread = e,
                     machine_state = f, interrupt_irq_node = g,
                     interrupt_states = h, arch_state = i, exst = (exst x)\<rparr>) x" apply (simp add: all_but_exst_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. all_but_exst (\<lambda>a b c d e f g h i. x = \<lparr>kheap = a, cdt = b, is_original_cap = c, cur_thread = d, idle_thread = e, machine_state = f, interrupt_irq_node = g, interrupt_states = h, arch_state = i, exst = exst x\<rparr>) x proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma bluh: assumes a: "x =
        \<lparr>kheap = kheap ba, cdt = cdt ba,
           is_original_cap = is_original_cap ba,
           cur_thread = cur_thread ba, idle_thread = idle_thread ba,
           machine_state = machine_state ba,
           interrupt_irq_node = interrupt_irq_node ba,
           interrupt_states = interrupt_states ba,
           arch_state = arch_state ba, exst = exst x\<rparr>"
     shows "x\<lparr>exst := exst ba\<rparr> = ba" apply (subst a) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x\<lparr>exst := exst ba\<rparr> = ba proof (prove)
goal (1 subgoal):
 1. \<lparr>kheap = kheap ba, cdt = cdt ba, is_original_cap = is_original_cap ba, cur_thread = cur_thread ba, idle_thread = idle_thread ba, machine_state = machine_state ba, interrupt_irq_node = interrupt_irq_node ba, interrupt_states = interrupt_states ba, arch_state = arch_state ba, exst = exst x\<rparr>\<lparr>exst := exst ba\<rparr> = ba proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma valid_cs_trans_state[simp]: "valid_cs a b (trans_state g s) = valid_cs a b s" by(simp add: valid_cs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_cs a b (trans_state g s) = valid_cs a b s
theory BCorres2_AI

lemma valid_tcb_state[simp]: "valid_tcb_state a (trans_state g s) = valid_tcb_state a s" by (simp add: valid_tcb_state_def split: thread_state.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_tcb_state a (trans_state g s) = valid_tcb_state a s
theory BCorres2_AI

lemma valid_bound_ntfn[simp]: "valid_bound_ntfn a (trans_state g s) = valid_bound_ntfn a s" by (simp add: valid_bound_ntfn_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_bound_ntfn a (trans_state g s) = valid_bound_ntfn a s
theory BCorres2_AI

lemma valid_arch_tcb_trans[simp]: "valid_arch_tcb t (trans_state g s) = valid_arch_tcb t s" by (auto elim: valid_arch_tcb_pspaceI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_tcb t (trans_state g s) = valid_arch_tcb t s
theory BCorres2_AI

lemma valid_tcb_trans_state[simp]: "valid_tcb a b (trans_state g s) = valid_tcb a b s" apply (simp add: valid_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_tcb a b (trans_state g s) = valid_tcb a b s proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma valid_ep_trans_state[simp]: "valid_ep a (trans_state g s) = valid_ep a s" apply (simp add: valid_ep_def split: endpoint.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ep a (trans_state g s) = valid_ep a s proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma valid_ntfn_trans_state[simp]: "valid_ntfn a (trans_state g s) = valid_ntfn a s" apply (simp add: valid_ntfn_def split: ntfn.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ntfn a (trans_state g s) = valid_ntfn a s proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma dxo_ex: "((),x :: det_ext state) \<in> fst (do_extended_op f s) \<Longrightarrow>
       \<exists>e :: det_ext. x = (trans_state (\<lambda>_. e) s)" apply (clarsimp simp add: do_extended_op_def
                            bind_def gets_def in_monad
                            select_f_def mk_ef_def
                            trans_state_update'
                            wrap_ext_op_det_ext_ext_def) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((), x) \<in> fst (do_extended_op f s) \<Longrightarrow> \<exists>e. x = trans_state (\<lambda>_. e) s proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>((), b) \<in> fst (f s); x = s\<lparr>exst := exst b\<rparr>\<rbrakk> \<Longrightarrow> \<exists>e. s\<lparr>exst := exst b\<rparr> = s\<lparr>exst := e\<rparr> proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma lift_inv: "(\<And>s g. P (trans_state g s) = P s) \<Longrightarrow>
       \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>" apply (clarsimp simp add: valid_def) apply (drule ex_st) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s g. P (trans_state g s) = P s) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>s g. P (trans_state g s) = P s; P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> P b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>s g. P (trans_state g s) = P s; P s; \<exists>e. b = trans_state (\<lambda>_. e) s\<rbrakk> \<Longrightarrow> P b proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma obj_at[wp]: "I (obj_at a b)" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at a b\<rbrace> f \<lbrace>\<lambda>_. obj_at a b\<rbrace>
theory BCorres2_AI

lemma st_tcb_at[wp]: "I (st_tcb_at a b)" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at a b\<rbrace> f \<lbrace>\<lambda>_. st_tcb_at a b\<rbrace>
theory BCorres2_AI

lemma valid_obj[wp]: "I (valid_obj a b)" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_obj a b\<rbrace> f \<lbrace>\<lambda>_. valid_obj a b\<rbrace>
theory BCorres2_AI

lemma valid_pspace[wp]: "I (valid_pspace)" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace\<rbrace> f \<lbrace>\<lambda>_. valid_pspace\<rbrace>
theory BCorres2_AI

lemma valid_mdb[wp]: "I valid_mdb" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb\<rbrace> f \<lbrace>\<lambda>_. valid_mdb\<rbrace>
theory BCorres2_AI

lemma valid_ioc[wp]: "I valid_ioc" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> f \<lbrace>\<lambda>_. valid_ioc\<rbrace>
theory BCorres2_AI

lemma valid_idle[wp]: "I valid_idle" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> f \<lbrace>\<lambda>_. valid_idle\<rbrace>
theory BCorres2_AI

lemma if_unsafe_then_cap[wp]: "I if_unsafe_then_cap" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> f \<lbrace>\<lambda>_. if_unsafe_then_cap\<rbrace>
theory BCorres2_AI

lemma valid_reply_caps[wp]: "I valid_reply_caps" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps\<rbrace> f \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>
theory BCorres2_AI

lemma valid_reply_masters[wp]: "I valid_reply_masters" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters\<rbrace> f \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>
theory BCorres2_AI

lemma valid_global_refs[wp]: "I valid_global_refs" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs\<rbrace> f \<lbrace>\<lambda>_. valid_global_refs\<rbrace>
theory BCorres2_AI

lemma valid_arch_state[wp]: "I valid_arch_state" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<rbrace> f \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
theory BCorres2_AI

lemma valid_irq_node[wp]: "I valid_irq_node" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_node\<rbrace> f \<lbrace>\<lambda>_. valid_irq_node\<rbrace>
theory BCorres2_AI

lemma valid_irq_handlers[wp]: "I valid_irq_handlers" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers\<rbrace> f \<lbrace>\<lambda>_. valid_irq_handlers\<rbrace>
theory BCorres2_AI

lemma valid_machine_state[wp]: "I valid_machine_state" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> f \<lbrace>\<lambda>_. valid_machine_state\<rbrace>
theory BCorres2_AI

lemma valid_vspace_objs[wp]: "I valid_vspace_objs" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs\<rbrace> f \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>
theory BCorres2_AI

lemma valid_arch_caps[wp]: "I valid_arch_caps" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps\<rbrace> f \<lbrace>\<lambda>_. valid_arch_caps\<rbrace>
theory BCorres2_AI

lemma valid_global_objs[wp]: "I valid_global_objs" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_objs\<rbrace> f \<lbrace>\<lambda>_. valid_global_objs\<rbrace>
theory BCorres2_AI

lemma valid_global_vspace_mappings[wp]: "I valid_global_vspace_mappings" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_vspace_mappings\<rbrace> f \<lbrace>\<lambda>_. valid_global_vspace_mappings\<rbrace>
theory BCorres2_AI

lemma valid_kernel_mappings[wp]: "I valid_kernel_mappings" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_kernel_mappings\<rbrace> f \<lbrace>\<lambda>_. valid_kernel_mappings\<rbrace>
theory BCorres2_AI

lemma equal_kernel_mappings[wp]: "I equal_kernel_mappings" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>equal_kernel_mappings\<rbrace> f \<lbrace>\<lambda>_. equal_kernel_mappings\<rbrace>
theory BCorres2_AI

lemma valid_asid_map[wp]: "I valid_asid_map" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> f \<lbrace>\<lambda>_. valid_asid_map\<rbrace>
theory BCorres2_AI

lemma pspace_in_kernel_window[wp]: "I pspace_in_kernel_window" by (rule lift_inv,simp)

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

lemma cap_refs_in_kernel_window[wp]: "I cap_refs_in_kernel_window" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window\<rbrace> f \<lbrace>\<lambda>_. cap_refs_in_kernel_window\<rbrace>
theory BCorres2_AI

lemma cur_tcb[wp]: "I cur_tcb" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb\<rbrace> f \<lbrace>\<lambda>_. cur_tcb\<rbrace>
theory BCorres2_AI

lemma  valid_objs[wp]: "I (valid_objs)" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> f \<lbrace>\<lambda>_. valid_objs\<rbrace>
theory BCorres2_AI

lemma pspace_aligned[wp]: "I (pspace_aligned)" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> f \<lbrace>\<lambda>_. pspace_aligned\<rbrace>
theory BCorres2_AI

lemma pspace_distinct[wp]: "I (pspace_distinct)" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct\<rbrace> f \<lbrace>\<lambda>_. pspace_distinct\<rbrace>
theory BCorres2_AI

lemma caps_of_state[wp]: "I (\<lambda>s. P (caps_of_state s))" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>