theory CNodeInv_AI

lemma word_and_bl_proof:
  "\<lbrakk> invs s; kheap s x = Some (CNode sz cs);
     unat (of_bl y :: machine_word) = 0; unat (of_bl z :: machine_word) = 0;
     y \<in> dom cs; z \<in> dom cs \<rbrakk> \<Longrightarrow> y = z" apply (simp add: unat_eq_0) apply (frule invs_valid_objs, erule(1) valid_objsE) apply (clarsimp simp: valid_obj_def valid_cs_def
                        valid_cs_size_def well_formed_cnode_n_def) apply (rule word_same_bl_memo_unify_word_type[where 'a=machine_word_len]) apply simp apply simp apply (simp add: word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; kheap s x = Some (CNode sz cs); unat (of_bl y) = 0; unat (of_bl z) = 0; y \<in> dom cs; z \<in> dom cs\<rbrakk> \<Longrightarrow> y = z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; kheap s x = Some (CNode sz cs); of_bl y = 0; of_bl z = 0; y \<in> dom cs; z \<in> dom cs\<rbrakk> \<Longrightarrow> y = z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; kheap s x = Some (CNode sz cs); of_bl y = 0; of_bl z = 0; y \<in> dom cs; z \<in> dom cs; valid_obj x (CNode sz cs) s\<rbrakk> \<Longrightarrow> y = z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; kheap s x = Some (CNode (length y) cs); of_bl y = 0; of_bl z = 0; length z = length y; sz = length y; \<forall>cap\<in>ran cs. s \<turnstile> cap; length y < word_bits - cte_level_bits; dom cs = {x. length x = length y}\<rbrakk> \<Longrightarrow> y = z proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invs s; kheap s x = Some (CNode (length y) cs); of_bl y = 0; of_bl z = 0; length z = length y; sz = length y; \<forall>cap\<in>ran cs. s \<turnstile> cap; length y < word_bits - cte_level_bits; dom cs = {x. length x = length y}\<rbrakk> \<Longrightarrow> of_bl y = of_bl z
 2. \<lbrakk>invs s; kheap s x = Some (CNode (length y) cs); of_bl y = 0; of_bl z = 0; length z = length y; sz = length y; \<forall>cap\<in>ran cs. s \<turnstile> cap; length y < word_bits - cte_level_bits; dom cs = {x. length x = length y}\<rbrakk> \<Longrightarrow> length y = length z
 3. \<lbrakk>invs s; kheap s x = Some (CNode (length y) cs); of_bl y = 0; of_bl z = 0; length z = length y; sz = length y; \<forall>cap\<in>ran cs. s \<turnstile> cap; length y < word_bits - cte_level_bits; dom cs = {x. length x = length y}\<rbrakk> \<Longrightarrow> length y \<le> LENGTH(32) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; kheap s x = Some (CNode (length y) cs); of_bl y = 0; of_bl z = 0; length z = length y; sz = length y; \<forall>cap\<in>ran cs. s \<turnstile> cap; length y < word_bits - cte_level_bits; dom cs = {x. length x = length y}\<rbrakk> \<Longrightarrow> length y = length z
 2. \<lbrakk>invs s; kheap s x = Some (CNode (length y) cs); of_bl y = 0; of_bl z = 0; length z = length y; sz = length y; \<forall>cap\<in>ran cs. s \<turnstile> cap; length y < word_bits - cte_level_bits; dom cs = {x. length x = length y}\<rbrakk> \<Longrightarrow> length y \<le> LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; kheap s x = Some (CNode (length y) cs); of_bl y = 0; of_bl z = 0; length z = length y; sz = length y; \<forall>cap\<in>ran cs. s \<turnstile> cap; length y < word_bits - cte_level_bits; dom cs = {x. length x = length y}\<rbrakk> \<Longrightarrow> length y \<le> LENGTH(32) proof (prove)
goal:
No subgoals!