kings-crown/FVELER_Isabelle huggingface dataset:
theory CNodeInv_AI

lemma suspend_makes_halted[wp]:
  "\<lbrace>valid_objs\<rbrace> IpcCancel_A.suspend thread \<lbrace>\<lambda>_. st_tcb_at halted thread\<rbrace>" unfolding IpcCancel_A.suspend_def by (wp hoare_strengthen_post [OF sts_st_tcb_at]
    | clarsimp elim!: pred_tcb_weakenE)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> suspend thread \<lbrace>\<lambda>_. st_tcb_at halted thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> do cancel_ipc thread;
state <- get_thread_state thread;
if state = Running then update_restart_pc thread else return ();
set_thread_state thread Inactive;
do_extended_op (tcb_sched_action tcb_sched_dequeue thread)
od \<lbrace>\<lambda>_. st_tcb_at halted thread\<rbrace>
theory CNodeInv_AI

lemma empty_slot_emptyable[wp]:
  "\<lbrace>emptyable sl and cte_at slot'\<rbrace> empty_slot slot' opt \<lbrace>\<lambda>rv. emptyable sl\<rbrace>" apply (rule hoare_assume_pre) apply (rule hoare_weaken_pre) apply (simp add: emptyable_def) apply (subst imp_conv_disj)+ apply (wp hoare_vcg_disj_lift | simp add: tcb_at_typ)+ apply (simp add: is_cap_simps emptyable_def tcb_at_typ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>emptyable sl and cte_wp_at (\<lambda>_. True) slot'\<rbrace> empty_slot slot' opt \<lbrace>\<lambda>rv. emptyable sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (emptyable sl and cte_wp_at (\<lambda>_. True) slot') s \<Longrightarrow> \<lbrace>emptyable sl and cte_wp_at (\<lambda>_. True) slot'\<rbrace> empty_slot slot' opt \<lbrace>\<lambda>rv. emptyable sl\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (emptyable sl and cte_wp_at (\<lambda>_. True) slot') s \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> empty_slot slot' opt \<lbrace>\<lambda>rv. emptyable sl\<rbrace>
 2. \<And>s sa. \<lbrakk>(emptyable sl and cte_wp_at (\<lambda>_. True) slot') s; (emptyable sl and cte_wp_at (\<lambda>_. True) slot') sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. (tcb_at (fst sl) s \<and> snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) s) \<and> cte_wp_at (\<lambda>_. True) slot' s \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> empty_slot slot' opt \<lbrace>\<lambda>rv s. tcb_at (fst sl) s \<and> snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) s\<rbrace>
 2. \<And>s sa. \<lbrakk>(emptyable sl and cte_wp_at (\<lambda>_. True) slot') s; (emptyable sl and cte_wp_at (\<lambda>_. True) slot') sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. (tcb_at (fst sl) s \<and> snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) s) \<and> cte_wp_at (\<lambda>_. True) slot' s \<Longrightarrow> \<lbrace>?Q6 s (?s6 s)\<rbrace> empty_slot slot' opt \<lbrace>\<lambda>rv s. \<not> (tcb_at (fst sl) s \<and> snd sl = tcb_cnode_index 2) \<or> st_tcb_at halted (fst sl) s\<rbrace>
 2. \<And>s sa. \<lbrakk>(emptyable sl and cte_wp_at (\<lambda>_. True) slot') s; (emptyable sl and cte_wp_at (\<lambda>_. True) slot') sa\<rbrakk> \<Longrightarrow> ?Q6 s (?s6 s) sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>emptyable sl s \<and> cte_wp_at (\<lambda>_. True) slot' s; emptyable sl sa \<and> cte_wp_at (\<lambda>_. True) slot' sa\<rbrakk> \<Longrightarrow> typ_at ATCB (fst sl) sa \<longrightarrow> snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) sa proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cap_delete_one_emptyable[wp]:
  "\<lbrace>invs and emptyable sl and cte_at sl'\<rbrace> cap_delete_one sl' \<lbrace>\<lambda>_. emptyable sl\<rbrace>" apply (simp add: cap_delete_one_def unless_def is_final_cap_def) apply (wpsimp wp: get_cap_wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable sl and cte_wp_at (\<lambda>_. True) sl'\<rbrace> cap_delete_one sl' \<lbrace>\<lambda>_. emptyable sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable sl and cte_wp_at (\<lambda>_. True) sl'\<rbrace> do cap <- get_cap sl';
when (cap \<noteq> NullCap) (do final <- gets (is_final_cap' cap);
y <- fast_finalise cap final;
empty_slot sl' NullCap
od)
od \<lbrace>\<lambda>_. emptyable sl\<rbrace> proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma reply_cancel_ipc_emptyable[wp]:
  "\<lbrace>invs and emptyable sl and valid_mdb\<rbrace> reply_cancel_ipc ptr \<lbrace>\<lambda>_. emptyable sl\<rbrace>" apply (simp add: reply_cancel_ipc_def) apply (wp select_inv hoare_drop_imps | simp add: Ball_def)+ apply (wp hoare_vcg_all_lift hoare_convert_imp thread_set_Pmdb
              thread_set_invs_trivial thread_set_emptyable thread_set_cte_at
         | simp add: tcb_cap_cases_def descendants_of_cte_at)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable sl and valid_mdb\<rbrace> reply_cancel_ipc ptr \<lbrace>\<lambda>_. emptyable sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable sl and valid_mdb\<rbrace> do y <- thread_set (tcb_fault_update (\<lambda>_. None)) ptr;
cap <- get_cap (ptr, tcb_cnode_index 2);
descs <- gets (descendants_of (ptr, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>a b. descs = {(a, b)});
select descs >>= cap_delete_one
od)
od \<lbrace>\<lambda>_. emptyable sl\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P24\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) ptr \<lbrace>\<lambda>rv s. \<forall>a b. (a, b) \<in> descendants_of (ptr, tcb_cnode_index 2) (cdt s) \<longrightarrow> invs s \<and> emptyable sl s \<and> cte_wp_at (\<lambda>_. True) (a, b) s\<rbrace>
 2. \<lbrace>?P'24\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) ptr \<lbrace>\<lambda>rv s. descendants_of (ptr, tcb_cnode_index 2) (cdt s) = {} \<longrightarrow> emptyable sl s\<rbrace>
 3. \<And>s. (invs and emptyable sl and valid_mdb) s \<Longrightarrow> ?P24 s \<and> ?P'24 s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma suspend_emptyable[wp]:
  "\<lbrace>invs and emptyable sl and valid_mdb\<rbrace> suspend l \<lbrace>\<lambda>_. emptyable sl\<rbrace>" apply (simp add: IpcCancel_A.suspend_def) apply (wp|simp)+ apply (wp emptyable_lift sts_st_tcb_at_cases)+ apply (wpsimp wp: set_thread_state_cte_wp_at)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable sl and valid_mdb\<rbrace> suspend l \<lbrace>\<lambda>_. emptyable sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable sl and valid_mdb\<rbrace> do y <- cancel_ipc l;
state <- get_thread_state l;
y <- if state = Running then update_restart_pc l else return ();
y <- set_thread_state l Inactive;
do_extended_op (tcb_sched_action tcb_sched_dequeue l)
od \<lbrace>\<lambda>_. emptyable sl\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>state. \<lbrace>?B3 () state ()\<rbrace> set_thread_state l Inactive \<lbrace>\<lambda>yb. emptyable sl\<rbrace>
 2. \<And>y state. \<lbrace>?B2 y state\<rbrace> if state = Running then update_restart_pc l else return () \<lbrace>?B3 y state\<rbrace>
 3. \<And>y. \<lbrace>?B1 y\<rbrace> get_thread_state l \<lbrace>?B2 y\<rbrace>
 4. \<lbrace>?Q\<rbrace> cancel_ipc l \<lbrace>?B1\<rbrace>
 5. \<And>s. (invs and emptyable sl and valid_mdb) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>state t s. st_tcb_at halted t s \<Longrightarrow> (l = t \<longrightarrow> halted Inactive) \<and> (l \<noteq> t \<longrightarrow> st_tcb_at halted t s)
 2. \<And>y state. \<lbrace>?B2 y state\<rbrace> if state = Running then update_restart_pc l else return () \<lbrace>\<lambda>a. emptyable sl\<rbrace>
 3. \<And>y. \<lbrace>?B1 y\<rbrace> get_thread_state l \<lbrace>?B2 y\<rbrace>
 4. \<lbrace>?Q\<rbrace> cancel_ipc l \<lbrace>?B1\<rbrace>
 5. \<And>s. (invs and emptyable sl and valid_mdb) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma finalise_cap_not_reply_master:
  "\<And>rv s' cap sl (s::'state_ext state).
    (Inr rv, s') \<in> fst (liftE (finalise_cap cap sl) s) \<Longrightarrow> \<not> is_master_reply_cap (fst rv)" by (simp add: Inr_in_liftE_simp finalise_cap_not_reply_master_unlifted)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>rv s' cap sl s. (Inr rv, s') \<in> fst (liftE (finalise_cap cap sl) s) \<Longrightarrow> \<not> is_master_reply_cap (fst rv)
theory CNodeInv_AI

lemma cte_wp_at_emptyableD:
  "\<And>P. \<lbrakk> cte_wp_at (\<lambda>c. c = cap) p s; valid_objs s; \<And>cap. P cap \<Longrightarrow> \<not> is_master_reply_cap cap \<rbrakk> \<Longrightarrow>
   P cap \<longrightarrow> emptyable p s" apply (simp add: emptyable_def) apply (clarsimp simp add: obj_at_def is_tcb) apply (erule(1) valid_objsE) apply (clarsimp simp: cte_wp_at_cases valid_obj_def valid_tcb_def
                        tcb_cap_cases_def pred_tcb_at_def obj_at_def
                 split: Structures_A.thread_state.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>cte_wp_at (\<lambda>c. c = cap) p s; valid_objs s; \<And>cap. P cap \<Longrightarrow> \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> P cap \<longrightarrow> emptyable p s proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>cte_wp_at (\<lambda>c. c = cap) p s; valid_objs s; \<And>cap. P cap \<Longrightarrow> \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> P cap \<longrightarrow> tcb_at (fst p) s \<and> snd p = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst p) s proof (prove)
goal (1 subgoal):
 1. \<And>P tcb. \<lbrakk>cte_wp_at (\<lambda>c. c = cap) p s; valid_objs s; \<And>cap. P cap \<Longrightarrow> \<not> is_master_reply_cap cap; P cap; snd p = tcb_cnode_index 2; kheap s (fst p) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> st_tcb_at halted (fst p) s proof (prove)
goal (1 subgoal):
 1. \<And>P tcb. \<lbrakk>cte_wp_at (\<lambda>c. c = cap) p s; \<And>cap. P cap \<Longrightarrow> \<not> is_master_reply_cap cap; P cap; snd p = tcb_cnode_index 2; kheap s (fst p) = Some (TCB tcb); valid_obj (fst p) (TCB tcb) s\<rbrakk> \<Longrightarrow> st_tcb_at halted (fst p) s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cte_wp_at_not_reply_master:
  "\<And>a b s. \<lbrakk> tcb_at a s \<longrightarrow> b \<noteq> tcb_cnode_index 2; cte_at (a, b) s;
              valid_objs s; valid_reply_masters s \<rbrakk>
   \<Longrightarrow> cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) (a, b) s" by (fastforce simp: valid_reply_masters_def cte_wp_at_caps_of_state
                     is_cap_simps valid_cap_def is_master_reply_cap_to_def
               dest: caps_of_state_valid_cap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>a b s. \<lbrakk>tcb_at a s \<longrightarrow> b \<noteq> tcb_cnode_index 2; cte_wp_at (\<lambda>_. True) (a, b) s; valid_objs s; valid_reply_masters s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) (a, b) s
theory CNodeInv_AI

lemma appropriate_Zombie:
  "\<And>ptr zbits n. appropriate_cte_cap (cap.Zombie ptr zbits n)
                     = (\<lambda>cap. cap_irqs cap = {})" by (rule ext, simp add: appropriate_cte_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ptr zbits n. appropriate_cte_cap (Zombie ptr zbits n) = (\<lambda>cap. cap_irqs cap = {})
theory CNodeInv_AI

lemma no_cap_to_obj_with_diff_ref_eqE:
  "\<lbrakk> no_cap_to_obj_with_diff_ref cap S s;
        obj_refs cap' = obj_refs cap; table_cap_ref cap' = table_cap_ref cap;
        S \<subseteq> S' \<rbrakk>
      \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' S' s" by (auto simp add: no_cap_to_obj_with_diff_ref_def Ball_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_cap_to_obj_with_diff_ref cap S s; obj_refs cap' = obj_refs cap; table_cap_ref cap' = table_cap_ref cap; S \<subseteq> S'\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' S' s
theory CNodeInv_AI

lemma context_conjI': "\<lbrakk>P; P \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q \<and> P" apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P; P \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q \<and> P proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma real_cte_at_not_tcb:
  "real_cte_at sl s \<Longrightarrow> \<not> tcb_at (fst sl) s" apply (simp add: tcb_at_typ obj_at_def) apply (clarsimp simp: is_cap_table_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. real_cte_at sl s \<Longrightarrow> \<not> tcb_at (fst sl) s proof (prove)
goal (1 subgoal):
 1. \<exists>ko. kheap s (fst sl) = Some ko \<and> is_cap_table (length (snd sl)) ko \<Longrightarrow> \<forall>ko. kheap s (fst sl) = Some ko \<longrightarrow> a_type ko \<noteq> ATCB proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cap_delete_invs[wp]:
  "\<And>ptr.
    \<lbrace>invs and emptyable ptr :: 'state_ext state \<Rightarrow> bool\<rbrace>
      cap_delete ptr
    \<lbrace>\<lambda>rv. invs\<rbrace>" unfolding cap_delete_def apply (rule hoare_pre, wp rec_del_invs) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ptr. \<lbrace>invs and emptyable ptr\<rbrace> cap_delete ptr \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ptr. \<lbrace>invs and emptyable ptr\<rbrace> doE rec_del (CTEDeleteCall ptr True);
returnOk ()
odE \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ptr s. (invs and emptyable ptr) s \<Longrightarrow> (invs and valid_rec_del_call (CTEDeleteCall ptr True) and (\<lambda>s. \<not> exposed_rdcall (CTEDeleteCall ptr True) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (CTEDeleteCall ptr True)) s) and emptyable (slot_rdcall (CTEDeleteCall ptr True)) and (\<lambda>s. case CTEDeleteCall ptr True of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) s \<and> (invs and valid_rec_del_call (CTEDeleteCall ptr True) and (\<lambda>s. \<not> exposed_rdcall (CTEDeleteCall ptr True) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (CTEDeleteCall ptr True)) s) and emptyable (slot_rdcall (CTEDeleteCall ptr True)) and (\<lambda>s. case CTEDeleteCall ptr True of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cap_delete_tcb[wp]:
 "\<And>t ptr. \<lbrace>tcb_at t :: 'state_ext state \<Rightarrow> bool\<rbrace> cap_delete ptr \<lbrace>\<lambda>rv. tcb_at t\<rbrace>" unfolding cap_delete_def by (simp add: tcb_at_typ | wp rec_del_typ_at)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>t ptr. \<lbrace>tcb_at t\<rbrace> cap_delete ptr \<lbrace>\<lambda>rv. tcb_at t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t ptr. \<lbrace>tcb_at t\<rbrace> doE rec_del (CTEDeleteCall ptr True);
returnOk ()
odE \<lbrace>\<lambda>rv. tcb_at t\<rbrace>
theory CNodeInv_AI

lemma cap_delete_valid_cap:
  "\<And>c p. \<lbrace>valid_cap c :: 'state_ext state \<Rightarrow> bool\<rbrace> cap_delete p \<lbrace>\<lambda>_. valid_cap c\<rbrace>" unfolding cap_delete_def by (wp valid_cap_typ rec_del_typ_at | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>c p. \<lbrace>valid_cap c\<rbrace> cap_delete p \<lbrace>\<lambda>_. valid_cap c\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>c p. \<lbrace>valid_cap c\<rbrace> doE rec_del (CTEDeleteCall p True);
returnOk ()
odE \<lbrace>\<lambda>_. valid_cap c\<rbrace>
theory CNodeInv_AI

lemma cap_delete_cte_at:
  "\<And>c p. \<lbrace>cte_at c :: 'state_ext state \<Rightarrow> bool\<rbrace> cap_delete p \<lbrace>\<lambda>_. cte_at c\<rbrace>" unfolding cap_delete_def by (wp rec_del_cte_at | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>c p. \<lbrace>cte_wp_at (\<lambda>_. True) c\<rbrace> cap_delete p \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) c\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>c p. \<lbrace>cte_wp_at (\<lambda>_. True) c\<rbrace> doE rec_del (CTEDeleteCall p True);
returnOk ()
odE \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) c\<rbrace>
theory CNodeInv_AI

lemma cap_delete_typ_at:
  "\<And>P T p cref. \<lbrace>\<lambda>s::'state_ext state. P (typ_at T p s)\<rbrace> cap_delete cref \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" unfolding cap_delete_def by (wp rec_del_typ_at | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P T p cref. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> cap_delete cref \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P T p cref. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> doE rec_del (CTEDeleteCall cref True);
returnOk ()
odE \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>
theory CNodeInv_AI

lemma cap_swap_fd_st_tcb_at[wp]:
  "\<lbrace>pred_tcb_at proj P t\<rbrace> cap_swap_for_delete sl sl' \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>" unfolding cap_swap_for_delete_def by (wp, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t\<rbrace> cap_swap_for_delete sl sl' \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t\<rbrace> when (sl \<noteq> sl') $ do cap1 <- get_cap sl;
cap2 <- get_cap sl';
cap_swap cap1 sl cap2 sl'
od \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>
theory CNodeInv_AI

lemma cases2 [case_names pos_pos neg_pos pos_neg neg_neg]:
  "\<lbrakk> \<lbrakk>p; q\<rbrakk> \<Longrightarrow> R; \<lbrakk>\<not> p; q\<rbrakk> \<Longrightarrow> R; \<lbrakk>p; \<not> q\<rbrakk> \<Longrightarrow> R; \<lbrakk>\<not> p; \<not> q\<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>p; q\<rbrakk> \<Longrightarrow> R; \<lbrakk>\<not> p; q\<rbrakk> \<Longrightarrow> R; \<lbrakk>p; \<not> q\<rbrakk> \<Longrightarrow> R; \<lbrakk>\<not> p; \<not> q\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory CNodeInv_AI

lemma rpo_measure_simps[simp]:
  "rpo_measure x (Some (y, n)) = (if y = Some x then n - 1 else n)" by (simp add: rpo_measure_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rpo_measure x (Some (y, n)) = (if y = Some x then n - 1 else n)
theory CNodeInv_AI

lemma rpo_trans:
  "\<lbrakk> revoke_progress_ord mapa mapb; revoke_progress_ord mapb mapc \<rbrakk>
     \<Longrightarrow> revoke_progress_ord mapa mapc" apply (simp add: revoke_progress_ord_def) apply (elim disjE, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>revoke_progress_ord mapa mapb; revoke_progress_ord mapb mapc\<rbrakk> \<Longrightarrow> revoke_progress_ord mapa mapc proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mapa = mapb \<or> (\<Sum>x\<in>dom mapb. rpo_measure x (mapb x)) < (\<Sum>x\<in>dom mapa. rpo_measure x (mapa x)); mapb = mapc \<or> (\<Sum>x\<in>dom mapc. rpo_measure x (mapc x)) < (\<Sum>x\<in>dom mapb. rpo_measure x (mapb x))\<rbrakk> \<Longrightarrow> mapa = mapc \<or> (\<Sum>x\<in>dom mapc. rpo_measure x (mapc x)) < (\<Sum>x\<in>dom mapa. rpo_measure x (mapa x)) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma rpo_delta:
  assumes x: "\<And>x. x \<notin> S \<Longrightarrow> mapa x = mapb x"
  assumes F: "finite S" "finite (dom mapa)" "finite (dom mapb)"
  assumes y:
    "(mapb, mapa) \<in> measure (\<lambda>mp. \<Sum>x \<in> S \<inter> dom mp. rpo_measure x (mp x))"
  shows "revoke_progress_ord mapa mapb" proof - have P: "(dom mapa - S) = (dom mapb - S)" by (fastforce simp: x) have Q: "(\<Sum>x \<in> dom mapa - S. rpo_measure x (mapa x))
            = (\<Sum>x \<in> dom mapb - S. rpo_measure x (mapb x))" apply (rule sum.cong) apply (simp add: P) apply (simp add: x) done show ?thesis using y apply (simp add: revoke_progress_ord_def) apply (rule disjI2) apply (fastforce simp: fold_Int_sub F Q) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. revoke_progress_ord mapa mapb proof (state)
goal (1 subgoal):
 1. revoke_progress_ord mapa mapb proof (prove)
goal (1 subgoal):
 1. dom mapa - S = dom mapb - S proof (state)
this:
dom mapa - S = dom mapb - S

goal (1 subgoal):
 1. revoke_progress_ord mapa mapb proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>dom mapa - S. rpo_measure x (mapa x)) = (\<Sum>x\<in>dom mapb - S. rpo_measure x (mapb x)) proof (prove)
goal (2 subgoals):
 1. dom mapa - S = dom mapb - S
 2. \<And>x. x \<in> dom mapb - S \<Longrightarrow> rpo_measure x (mapa x) = rpo_measure x (mapb x) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> dom mapb - S \<Longrightarrow> rpo_measure x (mapa x) = rpo_measure x (mapb x) proof (prove)
goal:
No subgoals! proof (state)
this:
(\<Sum>x\<in>dom mapa - S. rpo_measure x (mapa x)) = (\<Sum>x\<in>dom mapb - S. rpo_measure x (mapb x))

goal (1 subgoal):
 1. revoke_progress_ord mapa mapb proof (prove)
goal (1 subgoal):
 1. revoke_progress_ord mapa mapb proof (prove)
using this:
(mapb, mapa) \<in> measure (\<lambda>mp. \<Sum>x\<in>S \<inter> dom mp. rpo_measure x (mp x))

goal (1 subgoal):
 1. revoke_progress_ord mapa mapb proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>S \<inter> dom mapb. rpo_measure x (mapb x)) < (\<Sum>x\<in>S \<inter> dom mapa. rpo_measure x (mapa x)) \<Longrightarrow> mapa = mapb \<or> (\<Sum>x\<in>dom mapb. rpo_measure x (mapb x)) < (\<Sum>x\<in>dom mapa. rpo_measure x (mapa x)) proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>S \<inter> dom mapb. rpo_measure x (mapb x)) < (\<Sum>x\<in>S \<inter> dom mapa. rpo_measure x (mapa x)) \<Longrightarrow> (\<Sum>x\<in>dom mapb. rpo_measure x (mapb x)) < (\<Sum>x\<in>dom mapa. rpo_measure x (mapa x)) proof (prove)
goal:
No subgoals! proof (state)
this:
revoke_progress_ord mapa mapb

goal:
No subgoals!