kings-crown/FVELER_Isabelle huggingface dataset:
theory CNodeInv_R

lemma spec_corres_symb_exec_l_Ex:
  assumes x: "\<And>rv. (rv, s) \<in> fst (f s) \<Longrightarrow> spec_corres s r (Q rv) P' (g rv) h"
  shows      "spec_corres s r (\<lambda>s. \<exists>rv. Q rv s \<and> (rv, s) \<in> fst (f s)) P'
                              (do rv \<leftarrow> f; g rv od) h" proof - have y: "\<And>rv. corres r (\<lambda>s'. s' = s \<and> Q rv s \<and> (rv, s) \<in> fst (f s)) P' (g rv) h" apply (rule corres_req) defer apply (rule corres_guard_imp,
            erule x[unfolded spec_corres_def]) apply simp+ done show ?thesis unfolding spec_corres_def apply (rule corres_guard_imp,
           rule corres_symb_exec_l_Ex,
           rule y) apply simp+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_corres s r (\<lambda>s. \<exists>rv. Q rv s \<and> (rv, s) \<in> fst (f s)) P' (f >>= g) h proof (state)
goal (1 subgoal):
 1. spec_corres s r (\<lambda>s. \<exists>rv. Q rv s \<and> (rv, s) \<in> fst (f s)) P' (f >>= g) h proof (prove)
goal (1 subgoal):
 1. \<And>rv. corres r (\<lambda>s'. s' = s \<and> Q rv s \<and> (rv, s) \<in> fst (f s)) P' (g rv) h proof (prove)
goal (2 subgoals):
 1. \<And>rv sa s'. \<lbrakk>(sa, s') \<in> state_relation; sa = s \<and> Q rv s \<and> (rv, s) \<in> fst (f s); P' s'\<rbrakk> \<Longrightarrow> ?F rv
 2. \<And>rv. ?F rv \<Longrightarrow> corres r (\<lambda>s'. s' = s \<and> Q rv s \<and> (rv, s) \<in> fst (f s)) P' (g rv) h proof (prove)
goal (2 subgoals):
 1. \<And>rv. ?F rv \<Longrightarrow> corres r (\<lambda>s'. s' = s \<and> Q rv s \<and> (rv, s) \<in> fst (f s)) P' (g rv) h
 2. \<And>rv sa s'. \<lbrakk>(sa, s') \<in> state_relation; sa = s \<and> Q rv s \<and> (rv, s) \<in> fst (f s); P' s'\<rbrakk> \<Longrightarrow> ?F rv proof (prove)
goal (3 subgoals):
 1. \<And>rv sa. \<lbrakk>(rv, s) \<in> fst (f s); sa = s \<and> Q rv s \<and> (rv, s) \<in> fst (f s)\<rbrakk> \<Longrightarrow> (Q rv and (=) s) sa
 2. \<And>rv sa. \<lbrakk>(rv, s) \<in> fst (f s); P' sa\<rbrakk> \<Longrightarrow> P' sa
 3. \<And>rv sa s'. \<lbrakk>(sa, s') \<in> state_relation; sa = s \<and> Q rv s \<and> (rv, s) \<in> fst (f s); P' s'\<rbrakk> \<Longrightarrow> (rv, s) \<in> fst (f s) proof (prove)
goal:
No subgoals! proof (state)
this:
corres r (\<lambda>s'. s' = s \<and> Q ?rv s \<and> (?rv, s) \<in> fst (f s)) P' (g ?rv) h

goal (1 subgoal):
 1. spec_corres s r (\<lambda>s. \<exists>rv. Q rv s \<and> (rv, s) \<in> fst (f s)) P' (f >>= g) h proof (prove)
goal (1 subgoal):
 1. spec_corres s r (\<lambda>s. \<exists>rv. Q rv s \<and> (rv, s) \<in> fst (f s)) P' (f >>= g) h proof (prove)
goal (1 subgoal):
 1. corres r ((\<lambda>s. \<exists>rv. Q rv s \<and> (rv, s) \<in> fst (f s)) and (=) s) P' (f >>= g) h proof (prove)
goal (2 subgoals):
 1. \<And>sa. ((\<lambda>s. \<exists>rv. Q rv s \<and> (rv, s) \<in> fst (f s)) and (=) s) sa \<Longrightarrow> \<exists>rv. (sa = s \<and> Q rv s \<and> (rv, s) \<in> fst (f s)) \<and> (rv, sa) \<in> fst (f sa)
 2. \<And>s. P' s \<Longrightarrow> P' s proof (prove)
goal:
No subgoals! proof (state)
this:
spec_corres s r (\<lambda>s. \<exists>rv. Q rv s \<and> (rv, s) \<in> fst (f s)) P' (f >>= g) h

goal:
No subgoals!
theory CNodeInv_R

lemma spec_corres_symb_exec_r_All:
  assumes nf: "\<And>rv. no_fail (Q' rv) g"
  assumes x: "\<And>rv. spec_corres s r P (Q' rv) f (h rv)"
  shows      "spec_corres s r P (\<lambda>s. (\<forall>p \<in> fst (g s). snd p = s \<and> Q' (fst p) s) \<and> (\<exists>rv. Q' rv s))
                              f (do rv \<leftarrow> g; h rv od)" unfolding spec_corres_def apply (rule corres_guard_imp,
         rule corres_symb_exec_r_All,
         rule nf,
         rule x[unfolded spec_corres_def]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_corres s r P (\<lambda>s. (\<forall>p\<in>fst (g s). snd p = s \<and> Q' (fst p) s) \<and> (\<exists>rv. Q' rv s)) f (g >>= h) proof (prove)
goal (1 subgoal):
 1. corres r (P and (=) s) (\<lambda>s. (\<forall>p\<in>fst (g s). snd p = s \<and> Q' (fst p) s) \<and> (\<exists>rv. Q' rv s)) f (g >>= h) proof (prove)
goal (2 subgoals):
 1. \<And>sa. (P and (=) s) sa \<Longrightarrow> (P and (=) s) sa
 2. \<And>s. (\<forall>p\<in>fst (g s). snd p = s \<and> Q' (fst p) s) \<and> (\<exists>rv. Q' rv s) \<Longrightarrow> (\<forall>p\<in>fst (g s). snd p = s \<and> Q' (fst p) s) \<and> (\<exists>rv. Q' rv s) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma state_relation_cap_relation:
  "\<lbrakk> (s, s') \<in> state_relation; cte_wp_at ((=) cap) p s;
     cte_wp_at' ((=) cte) (cte_map p) s';
     valid_objs s; pspace_distinct' s'; pspace_aligned' s' \<rbrakk>
     \<Longrightarrow> cap_relation cap (cteCap cte)" apply (cases p, clarsimp simp: state_relation_def) apply (drule(3) pspace_relation_cte_wp_at) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at ((=) cap) p s; cte_wp_at' ((=) cte) (cte_map p) s'; valid_objs s; pspace_distinct' s'; pspace_aligned' s'\<rbrakk> \<Longrightarrow> cap_relation cap (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) cap) (a, b) s; cte_wp_at' ((=) cte) (cte_map (a, b)) s'; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; p = (a, b); pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'\<rbrakk> \<Longrightarrow> cap_relation cap (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) cap) (a, b) s; cte_wp_at' ((=) cte) (cte_map (a, b)) s'; valid_objs s; pspace_distinct' s'; pspace_aligned' s'; p = (a, b); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; cte_wp_at' (\<lambda>cte. cap_relation cap (cteCap cte)) (cte_map (a, b)) s'\<rbrakk> \<Longrightarrow> cap_relation cap (cteCap cte) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma descendants_of_empty_state_relation:
  "\<lbrakk> (s, s') \<in> state_relation; cte_at p s \<rbrakk> \<Longrightarrow>
    (descendants_of p (cdt s) = {}) = (descendants_of' (cte_map p) (ctes_of s') = {})" apply (clarsimp simp only: state_relation_def cdt_relation_def swp_def) apply (drule spec, drule(1) mp) apply (fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; cte_wp_at (\<lambda>_. True) p s\<rbrakk> \<Longrightarrow> (descendants_of p (cdt s) = {}) = (descendants_of' (cte_map p) (ctes_of s') = {}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); \<forall>c. cte_wp_at (\<lambda>_. True) c s \<longrightarrow> cte_map ` descendants_of c (cdt s) = descendants_of' (cte_map c) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'\<rbrakk> \<Longrightarrow> (descendants_of p (cdt s) = {}) = (descendants_of' (cte_map p) (ctes_of s') = {}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) (ctes_of s')\<rbrakk> \<Longrightarrow> (descendants_of p (cdt s) = {}) = (descendants_of' (cte_map p) (ctes_of s') = {}) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma threadSet_st_tcb_at2:
  assumes x: "\<forall>tcb. P (tcbState tcb) \<longrightarrow> P (tcbState (f tcb))"
  shows      "\<lbrace>st_tcb_at' P t\<rbrace> threadSet f t' \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>" including no_pre apply (simp add: threadSet_def pred_tcb_at'_def) apply (wp setObject_tcb_strongest) apply (rule hoare_strengthen_post, rule getObject_tcb_sp) apply (clarsimp simp: obj_at'_def x) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t\<rbrace> threadSet f t' \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t\<rbrace> threadSet f t' \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>ko. P (tcbState ko)) t\<rbrace> do tcb <- getObject t';
setObject t' (f tcb)
od \<lbrace>\<lambda>rv. obj_at' (\<lambda>ko. P (tcbState ko)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>ko. P (tcbState ko)) t\<rbrace> getObject t' \<lbrace>\<lambda>tcb s. if t' = t then P (tcbState (f tcb)) else obj_at' (\<lambda>ko. P (tcbState ko)) t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (obj_at' (\<lambda>ko. P (tcbState ko)) t and ko_at' rv t') s \<Longrightarrow> if t' = t then P (tcbState (f rv)) else obj_at' (\<lambda>ko. P (tcbState ko)) t s proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma (in mdb_move) [intro!]:
  shows "mdb_chain_0 m" using valid by (auto simp: valid_mdb_ctes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chain_0 m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. mdb_chain_0 m
theory CNodeInv_R

lemma (in mdb_move) sameRegionAs_parent_eq:
  "sameRegionAs cap cap' = sameRegionAs cap src_cap" using parency unfolding weak_derived'_def by (simp add: sameRegionAs_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameRegionAs cap cap' = global.sameRegionAs cap src_cap proof (prove)
using this:
weak_derived' src_cap cap'

goal (1 subgoal):
 1. global.sameRegionAs cap cap' = global.sameRegionAs cap src_cap proof (prove)
using this:
capMasterCap src_cap = capMasterCap cap' \<and> capBadge src_cap = capBadge cap' \<and> capASID src_cap = capASID cap' \<and> cap_asid_base' src_cap = cap_asid_base' cap' \<and> cap_vptr' src_cap = cap_vptr' cap' \<and> (isReplyCap src_cap \<longrightarrow> capTCBPtr src_cap = capTCBPtr cap' \<and> capReplyMaster src_cap = capReplyMaster cap')

goal (1 subgoal):
 1. global.sameRegionAs cap cap' = global.sameRegionAs cap src_cap
theory CNodeInv_R

lemma (in mdb_move) m'_cap:
  "m' p = Some (CTE c node) \<Longrightarrow>
  if p = src then c = NullCap
  else if p = dest then c = cap'
  else \<exists>node'. m p = Some (CTE c node')" using src dest neq apply (simp add: m'_def n_def) apply (auto simp add: modify_map_if split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m' p = Some (CTE c node) \<Longrightarrow> if p = src then c = capability.NullCap else if p = dest then c = cap' else \<exists>node'. m p = Some (CTE c node') proof (prove)
using this:
m src = Some (CTE src_cap src_node)
m dest = Some (CTE capability.NullCap old_dest_node)
src \<noteq> dest

goal (1 subgoal):
 1. m' p = Some (CTE c node) \<Longrightarrow> if p = src then c = capability.NullCap else if p = dest then c = cap' else \<exists>node'. m p = Some (CTE c node') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m dest (cteCap_update (\<lambda>_. cap'))) src (cteCap_update (\<lambda>_. capability.NullCap))) dest (cteMDBNode_update (\<lambda>m. src_node))) src (cteMDBNode_update (\<lambda>m. nullMDBNode))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) p = Some (CTE c node); m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); src \<noteq> dest\<rbrakk> \<Longrightarrow> (p = dest \<longrightarrow> c = cap') \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> c = capability.NullCap) \<and> (p \<noteq> src \<longrightarrow> (\<exists>node'. m p = Some (CTE c node')))) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma m_from_prev_src:
  "m \<turnstile> mdbPrev src_node \<leadsto> p = (mdbPrev src_node \<noteq> 0 \<and> p = src)" apply (insert src) apply (rule iffI) apply (clarsimp simp: mdb_next_unfold) apply (rule conjI, clarsimp) apply (erule dlistEp, clarsimp) apply clarsimp apply (clarsimp simp: mdb_next_unfold) apply (erule dlistEp, clarsimp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> mdbPrev src_node \<leadsto> p = (mdbPrev src_node \<noteq> 0 \<and> p = src) proof (prove)
goal (1 subgoal):
 1. m src = Some (CTE src_cap src_node) \<Longrightarrow> m \<turnstile> mdbPrev src_node \<leadsto> p = (mdbPrev src_node \<noteq> 0 \<and> p = src) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m \<turnstile> mdbPrev src_node \<leadsto> p\<rbrakk> \<Longrightarrow> mdbPrev src_node \<noteq> 0 \<and> p = src
 2. \<lbrakk>m src = Some (CTE src_cap src_node); mdbPrev src_node \<noteq> 0 \<and> p = src\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node \<leadsto> p proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>m src = Some (CTE src_cap src_node); m (mdbPrev src_node) = Some z; p = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> mdbPrev src_node \<noteq> 0 \<and> mdbNext (cteMDBNode z) = src
 2. \<lbrakk>m src = Some (CTE src_cap src_node); mdbPrev src_node \<noteq> 0 \<and> p = src\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node \<leadsto> p proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>m src = Some (CTE src_cap src_node); m (mdbPrev src_node) = Some z; p = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) = src
 2. \<lbrakk>m src = Some (CTE src_cap src_node); mdbPrev src_node \<noteq> 0 \<and> p = src\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node \<leadsto> p proof (prove)
goal (2 subgoals):
 1. \<And>z cte'. \<lbrakk>m (mdbPrev src_node) = Some z; p = mdbNext (cteMDBNode z); m (mdbPrev (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbNext (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode z) = src
 2. \<lbrakk>m src = Some (CTE src_cap src_node); mdbPrev src_node \<noteq> 0 \<and> p = src\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node \<leadsto> p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); mdbPrev src_node \<noteq> 0 \<and> p = src\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node \<leadsto> p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); mdbPrev src_node \<noteq> 0; p = src\<rbrakk> \<Longrightarrow> \<exists>z. m (mdbPrev src_node) = Some z \<and> src = mdbNext (cteMDBNode z) proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>mdbPrev src_node \<noteq> 0; p = src; m (mdbPrev (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbNext (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> \<exists>z. m (mdbPrev src_node) = Some z \<and> src = mdbNext (cteMDBNode z) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma m'_swp_eq:
  "m' \<turnstile> p \<leadsto> p' = m \<turnstile> s_d_swap p src dest \<leadsto> s_d_swap p' src dest" by (auto simp add: m'_next_eq s_d_swap_def m_to_src m_from_prev_src)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m' \<turnstile> p \<leadsto> p' = m \<turnstile> s_d_swap p src dest \<leadsto> s_d_swap p' src dest
theory CNodeInv_R

lemma m'_tranclD:
  "m' \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> m \<turnstile> s_d_swap p src dest \<leadsto>\<^sup>+ s_d_swap p' src dest" apply (erule trancl.induct) apply (fastforce simp: m'_swp_eq) apply (fastforce simp: m'_swp_eq intro: trancl_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m' \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> m \<turnstile> s_d_swap p src dest \<leadsto>\<^sup>+ s_d_swap p' src dest proof (prove)
goal (2 subgoals):
 1. \<And>a b. m' \<turnstile> a \<leadsto> b \<Longrightarrow> m \<turnstile> s_d_swap a src dest \<leadsto>\<^sup>+ s_d_swap b src dest
 2. \<And>a b c. \<lbrakk>m' \<turnstile> a \<leadsto>\<^sup>+ b; m \<turnstile> s_d_swap a src dest \<leadsto>\<^sup>+ s_d_swap b src dest; m' \<turnstile> b \<leadsto> c\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swap a src dest \<leadsto>\<^sup>+ s_d_swap c src dest proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>m' \<turnstile> a \<leadsto>\<^sup>+ b; m \<turnstile> s_d_swap a src dest \<leadsto>\<^sup>+ s_d_swap b src dest; m' \<turnstile> b \<leadsto> c\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swap a src dest \<leadsto>\<^sup>+ s_d_swap c src dest proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma m_tranclD:
  "m \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> m' \<turnstile> s_d_swap p src dest \<leadsto>\<^sup>+ s_d_swap p' src dest" apply (erule trancl.induct) apply (fastforce simp: m'_swp_eq) apply (fastforce simp: m'_swp_eq intro: trancl_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> m' \<turnstile> s_d_swap p src dest \<leadsto>\<^sup>+ s_d_swap p' src dest proof (prove)
goal (2 subgoals):
 1. \<And>a b. m \<turnstile> a \<leadsto> b \<Longrightarrow> m' \<turnstile> s_d_swap a src dest \<leadsto>\<^sup>+ s_d_swap b src dest
 2. \<And>a b c. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>+ b; m' \<turnstile> s_d_swap a src dest \<leadsto>\<^sup>+ s_d_swap b src dest; m \<turnstile> b \<leadsto> c\<rbrakk> \<Longrightarrow> m' \<turnstile> s_d_swap a src dest \<leadsto>\<^sup>+ s_d_swap c src dest proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>+ b; m' \<turnstile> s_d_swap a src dest \<leadsto>\<^sup>+ s_d_swap b src dest; m \<turnstile> b \<leadsto> c\<rbrakk> \<Longrightarrow> m' \<turnstile> s_d_swap a src dest \<leadsto>\<^sup>+ s_d_swap c src dest proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma m'_trancl_eq:
  "m' \<turnstile> p \<leadsto>\<^sup>+ p' = m \<turnstile> s_d_swap p src dest \<leadsto>\<^sup>+ s_d_swap p' src dest" by (auto dest: m_tranclD m'_tranclD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m' \<turnstile> p \<leadsto>\<^sup>+ p' = m \<turnstile> s_d_swap p src dest \<leadsto>\<^sup>+ s_d_swap p' src dest
theory CNodeInv_R

lemma m'_rtrancl_eq:
  "m' \<turnstile> p \<leadsto>\<^sup>* p' = m \<turnstile> s_d_swap p src dest \<leadsto>\<^sup>* s_d_swap p' src dest" by (auto simp: rtrancl_eq_or_trancl m'_trancl_eq s_d_swap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m' \<turnstile> p \<leadsto>\<^sup>* p' = m \<turnstile> s_d_swap p src dest \<leadsto>\<^sup>* s_d_swap p' src dest
theory CNodeInv_R

lemma m_cap:
  "m p = Some (CTE c node) \<Longrightarrow>
  if p = src then \<exists>node'. c = src_cap \<and> m' dest = Some (CTE cap' node')
  else if p = dest then \<exists>node'. c = NullCap  \<and> m' src = Some (CTE NullCap node')
  else \<exists>node'. m' p = Some (CTE c node')" apply (auto simp: src dest) apply (auto simp: m'_def n_def src dest modify_map_if neq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m p = Some (CTE c node) \<Longrightarrow> if p = src then \<exists>node'. c = src_cap \<and> m' dest = Some (CTE cap' node') else if p = dest then \<exists>node'. c = capability.NullCap \<and> m' src = Some (CTE capability.NullCap node') else \<exists>node'. m' p = Some (CTE c node') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = dest; old_dest_node = node; c = capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>node'. m' src = Some (CTE capability.NullCap node')
 2. \<lbrakk>src \<noteq> dest; p = src; src_cap = c; src_node = node\<rbrakk> \<Longrightarrow> \<exists>node'. m' dest = Some (CTE cap' node')
 3. \<lbrakk>m p = Some (CTE c node); p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>node'. m' p = Some (CTE c node') proof (prove)
goal:
No subgoals!