theory CNodeInv_AI

lemma cte_at_replicate_zbits:
  "\<And>(s::'state_ext state) oref zb n.
    \<lbrakk> s \<turnstile> cap.Zombie oref zb n \<rbrakk> \<Longrightarrow> cte_at (oref, replicate (zombie_cte_bits zb) False) s" apply (clarsimp simp: valid_cap_def obj_at_def is_tcb is_cap_table
                 split: option.split_asm) apply (rule cte_wp_at_tcbI, simp) apply (fastforce simp add: tcb_cap_cases_def tcb_cnode_index_def to_bl_1) apply simp apply (subgoal_tac "replicate x2 False \<in> dom cs") apply safe[1] apply (rule cte_wp_at_cteI, fastforce) apply (simp add: well_formed_cnode_n_def length_set_helper) apply simp apply simp apply (clarsimp simp: well_formed_cnode_n_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s oref zb n. s \<turnstile> Zombie oref zb n \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, replicate (zombie_cte_bits zb) False) s proof (prove)
goal (2 subgoals):
 1. \<And>s oref n tcb. \<lbrakk>cap_aligned (Zombie oref None n); n \<le> 5; kheap s oref = Some (TCB tcb)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, [False, False, False]) s
 2. \<And>s oref n x2 cs. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, replicate x2 False) s proof (prove)
goal (3 subgoals):
 1. \<And>s oref n tcb. \<lbrakk>cap_aligned (Zombie oref None n); n \<le> 5; kheap s oref = Some (TCB tcb)\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd (oref, [False, False, False])) = Some (?getF32 s oref n tcb, ?setF32 s oref n tcb)
 2. \<And>s oref n tcb. \<lbrakk>cap_aligned (Zombie oref None n); n \<le> 5; kheap s oref = Some (TCB tcb)\<rbrakk> \<Longrightarrow> True
 3. \<And>s oref n x2 cs. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, replicate x2 False) s proof (prove)
goal (2 subgoals):
 1. \<And>s oref n tcb. \<lbrakk>cap_aligned (Zombie oref None n); n \<le> 5; kheap s oref = Some (TCB tcb)\<rbrakk> \<Longrightarrow> True
 2. \<And>s oref n x2 cs. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, replicate x2 False) s proof (prove)
goal (1 subgoal):
 1. \<And>s oref n x2 cs. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, replicate x2 False) s proof (prove)
goal (2 subgoals):
 1. \<And>s oref n x2 cs. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs; replicate x2 False \<in> dom cs\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, replicate x2 False) s
 2. \<And>s oref n x2 cs. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs\<rbrakk> \<Longrightarrow> replicate x2 False \<in> dom cs proof (prove)
goal (2 subgoals):
 1. \<And>s oref n x2 cs y. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs; cs (replicate x2 False) = Some y\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (oref, replicate x2 False) s
 2. \<And>s oref n x2 cs. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs\<rbrakk> \<Longrightarrow> replicate x2 False \<in> dom cs proof (prove)
goal (4 subgoals):
 1. \<And>s oref n x2 cs y. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs; cs (replicate x2 False) = Some y\<rbrakk> \<Longrightarrow> well_formed_cnode_n x2 cs
 2. \<And>s oref n x2 cs y. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs; cs (replicate x2 False) = Some y\<rbrakk> \<Longrightarrow> cs (snd (oref, replicate x2 False)) = Some (?cte55 s oref n x2 cs y)
 3. \<And>s oref n x2 cs y. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs; cs (replicate x2 False) = Some y\<rbrakk> \<Longrightarrow> True
 4. \<And>s oref n x2 cs. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs\<rbrakk> \<Longrightarrow> replicate x2 False \<in> dom cs proof (prove)
goal (3 subgoals):
 1. \<And>s oref n x2 cs y. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs; cs (replicate x2 False) = Some y\<rbrakk> \<Longrightarrow> cs (snd (oref, replicate x2 False)) = Some (?cte55 s oref n x2 cs y)
 2. \<And>s oref n x2 cs y. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs; cs (replicate x2 False) = Some y\<rbrakk> \<Longrightarrow> True
 3. \<And>s oref n x2 cs. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs\<rbrakk> \<Longrightarrow> replicate x2 False \<in> dom cs proof (prove)
goal (2 subgoals):
 1. \<And>s oref n x2 cs y. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs; cs (replicate x2 False) = Some y\<rbrakk> \<Longrightarrow> True
 2. \<And>s oref n x2 cs. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs\<rbrakk> \<Longrightarrow> replicate x2 False \<in> dom cs proof (prove)
goal (1 subgoal):
 1. \<And>s oref n x2 cs. \<lbrakk>cap_aligned (Zombie oref (Some x2) n); n \<le> 2 ^ x2; 0 < x2; kheap s oref = Some (CNode x2 cs); well_formed_cnode_n x2 cs\<rbrakk> \<Longrightarrow> replicate x2 False \<in> dom cs proof (prove)
goal:
No subgoals!