theory Untyped_R

lemma bluhr_descendants_of':
  "mdb_insert_again_child (ctes_of s') parent parent_cap pmdb site site_cap site_node cap s
   \<Longrightarrow>
   descendants_of' x
           (modify_map
             (modify_map
               (\<lambda>c. if c = site
                    then Some (CTE cap (MDB (mdbNext pmdb) parent True True))
                    else ctes_of s' c)
               (mdbNext pmdb)
               (if mdbNext pmdb = 0 then id
                else cteMDBNode_update (mdbPrev_update (\<lambda>x. site))))
             parent (cteMDBNode_update (mdbNext_update (\<lambda>x. site))))
     = (if parent \<in> descendants_of' x (ctes_of s') \<or> x = parent
        then descendants_of' x (ctes_of s') \<union> {site}
        else descendants_of' x (ctes_of s'))" apply (subst modify_map_com) apply (case_tac x, rename_tac node, case_tac node, clarsimp) apply (subst blarg_descendants_of') apply (erule mdb_insert_again_child.descendants) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_insert_again_child (ctes_of s') parent parent_cap pmdb site site_cap site_node cap s \<Longrightarrow> descendants_of' x (modify_map (modify_map (\<lambda>c. if c = site then Some (CTE cap (MDB (mdbNext pmdb) parent True True)) else ctes_of s' c) (mdbNext pmdb) (if mdbNext pmdb = 0 then id else cteMDBNode_update (mdbPrev_update (\<lambda>x. site)))) parent (cteMDBNode_update (mdbNext_update (\<lambda>x. site)))) = (if parent \<in> descendants_of' x (ctes_of s') \<or> x = parent then descendants_of' x (ctes_of s') \<union> {site} else descendants_of' x (ctes_of s')) proof (prove)
goal (2 subgoals):
 1. \<And>x. mdb_insert_again_child (ctes_of s') parent parent_cap pmdb site site_cap site_node cap s \<Longrightarrow> cteMDBNode_update (mdbNext_update (\<lambda>x. site)) ((if mdbNext pmdb = 0 then id else cteMDBNode_update (mdbPrev_update (\<lambda>x. site))) x) = (if mdbNext pmdb = 0 then id else cteMDBNode_update (mdbPrev_update (\<lambda>x. site))) (cteMDBNode_update (mdbNext_update (\<lambda>x. site)) x)
 2. mdb_insert_again_child (ctes_of s') parent parent_cap pmdb site site_cap site_node cap s \<Longrightarrow> descendants_of' x (modify_map (modify_map (\<lambda>c. if c = site then Some (CTE cap (MDB (mdbNext pmdb) parent True True)) else ctes_of s' c) parent (cteMDBNode_update (mdbNext_update (\<lambda>x. site)))) (mdbNext pmdb) (if mdbNext pmdb = 0 then id else cteMDBNode_update (mdbPrev_update (\<lambda>x. site)))) = (if parent \<in> descendants_of' x (ctes_of s') \<or> x = parent then descendants_of' x (ctes_of s') \<union> {site} else descendants_of' x (ctes_of s')) proof (prove)
goal (1 subgoal):
 1. mdb_insert_again_child (ctes_of s') parent parent_cap pmdb site site_cap site_node cap s \<Longrightarrow> descendants_of' x (modify_map (modify_map (\<lambda>c. if c = site then Some (CTE cap (MDB (mdbNext pmdb) parent True True)) else ctes_of s' c) parent (cteMDBNode_update (mdbNext_update (\<lambda>x. site)))) (mdbNext pmdb) (if mdbNext pmdb = 0 then id else cteMDBNode_update (mdbPrev_update (\<lambda>x. site)))) = (if parent \<in> descendants_of' x (ctes_of s') \<or> x = parent then descendants_of' x (ctes_of s') \<union> {site} else descendants_of' x (ctes_of s')) proof (prove)
goal (1 subgoal):
 1. mdb_insert_again_child (ctes_of s') parent parent_cap pmdb site site_cap site_node cap s \<Longrightarrow> descendants_of' x (modify_map (\<lambda>c. if c = site then Some (CTE cap (MDB (mdbNext pmdb) parent True True)) else ctes_of s' c) parent (cteMDBNode_update (mdbNext_update (\<lambda>x. site)))) = (if parent \<in> descendants_of' x (ctes_of s') \<or> x = parent then descendants_of' x (ctes_of s') \<union> {site} else descendants_of' x (ctes_of s')) proof (prove)
goal:
No subgoals!