theory Finalise_DR

lemma opt_cap_cnode:
  "\<lbrakk> kheap s y = Some (CNode sz cn); y \<noteq> idle_thread s; well_formed_cnode_n sz cn \<rbrakk>
    \<Longrightarrow> (opt_cap (y, node) (transform s) = Some cap)
           = (\<exists>v cap'. transform_cslot_ptr (y, v) = (y, node)
                   \<and> cn v = Some cap' \<and> cap = transform_cap cap')" apply clarsimp apply (simp add: opt_cap_def slots_of_def
                   transform_def transform_objects_def restrict_map_def
                   transform_cnode_contents_def option_map_join_def
                   transform_cslot_ptr_def object_slots_def
                   nat_split_conv_to_if
            split: option.split) apply (case_tac "sz = 0") apply (clarsimp, rule conjI) apply (metis nat_to_bl_id2 option.distinct(1) wf_cs_nD) apply (metis (full_types) nat_to_bl_to_bin nat_to_bl_id2
                             option.inject wf_cs_nD)  (* slow 20s *)
  (* "sz \<noteq> 0" *)
   apply (clarsimp, rule conjI) apply (metis nat_to_bl_id2 option.distinct(1) wf_cs_nD) apply (metis (full_types) nat_to_bl_to_bin nat_to_bl_id2
                            option.inject wf_cs_nD)  (* slow 30s *)
   done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s y = Some (kernel_object.CNode sz cn); y \<noteq> idle_thread s; well_formed_cnode_n sz cn\<rbrakk> \<Longrightarrow> (opt_cap (y, node) (transform s) = Some cap) = (\<exists>v cap'. transform_cslot_ptr (y, v) = (y, node) \<and> cn v = Some cap' \<and> cap = transform_cap cap') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s y = Some (kernel_object.CNode sz cn); y \<noteq> idle_thread s; well_formed_cnode_n sz cn\<rbrakk> \<Longrightarrow> (opt_cap (y, node) (transform s) = Some cap) = (\<exists>v. transform_cslot_ptr (y, v) = (y, node) \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s y = Some (kernel_object.CNode sz cn); y \<noteq> idle_thread s; well_formed_cnode_n sz cn\<rbrakk> \<Longrightarrow> (nat_to_bl 0 node = None \<longrightarrow> (nat_to_bl sz node = None \<longrightarrow> (sz = 0 \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap')))) \<and> (\<forall>x2. nat_to_bl sz node = Some x2 \<longrightarrow> (sz = 0 \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))))) \<and> (\<forall>x2. nat_to_bl 0 node = Some x2 \<longrightarrow> (nat_to_bl sz node = None \<longrightarrow> (sz = 0 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap')))) \<and> (\<forall>x2a. nat_to_bl sz node = Some x2a \<longrightarrow> (sz = 0 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<exists>z. cn x2a = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s y = Some (kernel_object.CNode sz cn); y \<noteq> idle_thread s; well_formed_cnode_n sz cn; sz = 0\<rbrakk> \<Longrightarrow> (nat_to_bl 0 node = None \<longrightarrow> (nat_to_bl sz node = None \<longrightarrow> (sz = 0 \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap')))) \<and> (\<forall>x2. nat_to_bl sz node = Some x2 \<longrightarrow> (sz = 0 \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))))) \<and> (\<forall>x2. nat_to_bl 0 node = Some x2 \<longrightarrow> (nat_to_bl sz node = None \<longrightarrow> (sz = 0 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap')))) \<and> (\<forall>x2a. nat_to_bl sz node = Some x2a \<longrightarrow> (sz = 0 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<exists>z. cn x2a = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap')))))
 2. \<lbrakk>kheap s y = Some (kernel_object.CNode sz cn); y \<noteq> idle_thread s; well_formed_cnode_n sz cn; sz \<noteq> 0\<rbrakk> \<Longrightarrow> (nat_to_bl 0 node = None \<longrightarrow> (nat_to_bl sz node = None \<longrightarrow> (sz = 0 \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap')))) \<and> (\<forall>x2. nat_to_bl sz node = Some x2 \<longrightarrow> (sz = 0 \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))))) \<and> (\<forall>x2. nat_to_bl 0 node = Some x2 \<longrightarrow> (nat_to_bl sz node = None \<longrightarrow> (sz = 0 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap')))) \<and> (\<forall>x2a. nat_to_bl sz node = Some x2a \<longrightarrow> (sz = 0 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<exists>z. cn x2a = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>kheap s y = Some (kernel_object.CNode 0 cn); y \<noteq> idle_thread s; well_formed_cnode_n 0 cn; sz = 0\<rbrakk> \<Longrightarrow> nat_to_bl 0 node = None \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap'))
 2. \<lbrakk>kheap s y = Some (kernel_object.CNode 0 cn); y \<noteq> idle_thread s; well_formed_cnode_n 0 cn; sz = 0\<rbrakk> \<Longrightarrow> \<forall>x2. nat_to_bl 0 node = Some x2 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))
 3. \<lbrakk>kheap s y = Some (kernel_object.CNode sz cn); y \<noteq> idle_thread s; well_formed_cnode_n sz cn; sz \<noteq> 0\<rbrakk> \<Longrightarrow> (nat_to_bl 0 node = None \<longrightarrow> (nat_to_bl sz node = None \<longrightarrow> (sz = 0 \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap')))) \<and> (\<forall>x2. nat_to_bl sz node = Some x2 \<longrightarrow> (sz = 0 \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))))) \<and> (\<forall>x2. nat_to_bl 0 node = Some x2 \<longrightarrow> (nat_to_bl sz node = None \<longrightarrow> (sz = 0 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap')))) \<and> (\<forall>x2a. nat_to_bl sz node = Some x2a \<longrightarrow> (sz = 0 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<exists>z. cn x2a = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s y = Some (kernel_object.CNode 0 cn); y \<noteq> idle_thread s; well_formed_cnode_n 0 cn; sz = 0\<rbrakk> \<Longrightarrow> \<forall>x2. nat_to_bl 0 node = Some x2 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))
 2. \<lbrakk>kheap s y = Some (kernel_object.CNode sz cn); y \<noteq> idle_thread s; well_formed_cnode_n sz cn; sz \<noteq> 0\<rbrakk> \<Longrightarrow> (nat_to_bl 0 node = None \<longrightarrow> (nat_to_bl sz node = None \<longrightarrow> (sz = 0 \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap')))) \<and> (\<forall>x2. nat_to_bl sz node = Some x2 \<longrightarrow> (sz = 0 \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))))) \<and> (\<forall>x2. nat_to_bl 0 node = Some x2 \<longrightarrow> (nat_to_bl sz node = None \<longrightarrow> (sz = 0 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap')))) \<and> (\<forall>x2a. nat_to_bl sz node = Some x2a \<longrightarrow> (sz = 0 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<exists>z. cn x2a = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s y = Some (kernel_object.CNode sz cn); y \<noteq> idle_thread s; well_formed_cnode_n sz cn; sz \<noteq> 0\<rbrakk> \<Longrightarrow> (nat_to_bl 0 node = None \<longrightarrow> (nat_to_bl sz node = None \<longrightarrow> (sz = 0 \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap')))) \<and> (\<forall>x2. nat_to_bl sz node = Some x2 \<longrightarrow> (sz = 0 \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))))) \<and> (\<forall>x2. nat_to_bl 0 node = Some x2 \<longrightarrow> (nat_to_bl sz node = None \<longrightarrow> (sz = 0 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap')))) \<and> (\<forall>x2a. nat_to_bl sz node = Some x2a \<longrightarrow> (sz = 0 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<exists>z. cn x2a = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s y = Some (kernel_object.CNode sz cn); y \<noteq> idle_thread s; well_formed_cnode_n sz cn; sz \<noteq> 0\<rbrakk> \<Longrightarrow> (nat_to_bl 0 node = None \<longrightarrow> (nat_to_bl sz node = None \<longrightarrow> (sz = 0 \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap')))) \<and> (\<forall>x2. nat_to_bl sz node = Some x2 \<longrightarrow> (sz = 0 \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))))) \<and> (\<forall>x2. nat_to_bl 0 node = Some x2 \<longrightarrow> (nat_to_bl sz node = None \<longrightarrow> (sz = 0 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap')))) \<and> (\<forall>x2a. nat_to_bl sz node = Some x2a \<longrightarrow> (sz = 0 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))) \<and> (0 < sz \<longrightarrow> (\<exists>z. cn x2a = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap'))))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s y = Some (kernel_object.CNode sz cn); y \<noteq> idle_thread s; well_formed_cnode_n sz cn; 0 < sz\<rbrakk> \<Longrightarrow> nat_to_bl sz node = None \<longrightarrow> (\<forall>v. nat (bl_to_bin v) = node \<longrightarrow> (\<forall>cap'. cn v = Some cap' \<longrightarrow> cap \<noteq> transform_cap cap'))
 2. \<lbrakk>kheap s y = Some (kernel_object.CNode sz cn); y \<noteq> idle_thread s; well_formed_cnode_n sz cn; 0 < sz\<rbrakk> \<Longrightarrow> \<forall>x2. nat_to_bl sz node = Some x2 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s y = Some (kernel_object.CNode sz cn); y \<noteq> idle_thread s; well_formed_cnode_n sz cn; 0 < sz\<rbrakk> \<Longrightarrow> \<forall>x2. nat_to_bl sz node = Some x2 \<longrightarrow> (\<exists>z. cn x2 = Some z \<and> transform_cap z = cap) = (\<exists>v. nat (bl_to_bin v) = node \<and> (\<exists>cap'. cn v = Some cap' \<and> cap = transform_cap cap')) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!