theory CNodeInv_R

lemma trancl_cap_upd:
  "m sl = Some (CTE cap' mdbnode) \<Longrightarrow>
  m (sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto>\<^sup>+ p' = m \<turnstile> p \<leadsto>\<^sup>+ p'" apply (rule iffI) apply (erule trancl_induct) apply (fastforce simp: mdb_next_cap_upd simp del: fun_upd_apply) apply (fastforce simp: mdb_next_cap_upd simp del: fun_upd_apply elim: trancl_trans) apply (erule trancl_induct) apply (fastforce simp: mdb_next_cap_upd simp del: fun_upd_apply) apply (fastforce simp: mdb_next_cap_upd simp del: fun_upd_apply elim: trancl_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m sl = Some (CTE cap' mdbnode) \<Longrightarrow> m(sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto>\<^sup>+ p' = m \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m sl = Some (CTE cap' mdbnode); m(sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'
 2. \<lbrakk>m sl = Some (CTE cap' mdbnode); m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m(sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>m sl = Some (CTE cap' mdbnode); m(sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto> y\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>m sl = Some (CTE cap' mdbnode); m(sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto>\<^sup>+ y; m(sl \<mapsto> CTE cap mdbnode) \<turnstile> y \<leadsto> z; m \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z
 3. \<lbrakk>m sl = Some (CTE cap' mdbnode); m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m(sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>m sl = Some (CTE cap' mdbnode); m(sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto>\<^sup>+ y; m(sl \<mapsto> CTE cap mdbnode) \<turnstile> y \<leadsto> z; m \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ z
 2. \<lbrakk>m sl = Some (CTE cap' mdbnode); m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m(sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m sl = Some (CTE cap' mdbnode); m \<turnstile> p \<leadsto>\<^sup>+ p'\<rbrakk> \<Longrightarrow> m(sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>m sl = Some (CTE cap' mdbnode); m \<turnstile> p \<leadsto> y\<rbrakk> \<Longrightarrow> m(sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>m sl = Some (CTE cap' mdbnode); m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m(sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m(sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m sl = Some (CTE cap' mdbnode); m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m(sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m(sl \<mapsto> CTE cap mdbnode) \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal:
No subgoals!