theory CSpace_AI

lemma cte_at_cref_len:
  "\<lbrakk>cte_at (p, c) s; cte_at (p, c') s\<rbrakk> \<Longrightarrow> length c = length c'" apply (clarsimp simp: cte_at_cases) apply (erule disjE) prefer 2 apply (clarsimp simp: tcb_cap_cases_length) apply clarsimp apply (drule (1) wf_cs_nD) apply (drule (1) wf_cs_nD) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) (p, c) s; cte_wp_at (\<lambda>_. True) (p, c') s\<rbrakk> \<Longrightarrow> length c = length c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<exists>sz fun. kheap s p = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> c \<in> dom fun) \<or> (\<exists>tcb. kheap s p = Some (TCB tcb)) \<and> c \<in> dom tcb_cap_cases; (\<exists>sz fun. kheap s p = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> c' \<in> dom fun) \<or> (\<exists>tcb. kheap s p = Some (TCB tcb)) \<and> c' \<in> dom tcb_cap_cases\<rbrakk> \<Longrightarrow> length c = length c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<exists>sz fun. kheap s p = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> c' \<in> dom fun) \<or> (\<exists>tcb. kheap s p = Some (TCB tcb)) \<and> c' \<in> dom tcb_cap_cases; \<exists>sz fun. kheap s p = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> c \<in> dom fun\<rbrakk> \<Longrightarrow> length c = length c'
 2. \<lbrakk>(\<exists>sz fun. kheap s p = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> c' \<in> dom fun) \<or> (\<exists>tcb. kheap s p = Some (TCB tcb)) \<and> c' \<in> dom tcb_cap_cases; (\<exists>tcb. kheap s p = Some (TCB tcb)) \<and> c \<in> dom tcb_cap_cases\<rbrakk> \<Longrightarrow> length c = length c' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<exists>sz fun. kheap s p = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> c' \<in> dom fun) \<or> (\<exists>tcb. kheap s p = Some (TCB tcb)) \<and> c' \<in> dom tcb_cap_cases; (\<exists>tcb. kheap s p = Some (TCB tcb)) \<and> c \<in> dom tcb_cap_cases\<rbrakk> \<Longrightarrow> length c = length c'
 2. \<lbrakk>(\<exists>sz fun. kheap s p = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> c' \<in> dom fun) \<or> (\<exists>tcb. kheap s p = Some (TCB tcb)) \<and> c' \<in> dom tcb_cap_cases; \<exists>sz fun. kheap s p = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> c \<in> dom fun\<rbrakk> \<Longrightarrow> length c = length c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<exists>sz fun. kheap s p = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> c' \<in> dom fun) \<or> (\<exists>tcb. kheap s p = Some (TCB tcb)) \<and> c' \<in> dom tcb_cap_cases; \<exists>sz fun. kheap s p = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> c \<in> dom fun\<rbrakk> \<Longrightarrow> length c = length c' proof (prove)
goal (1 subgoal):
 1. \<And>sz fun y ya. \<lbrakk>kheap s p = Some (CNode sz fun); well_formed_cnode_n sz fun; fun c = Some y; fun c' = Some ya\<rbrakk> \<Longrightarrow> length c = length c' proof (prove)
goal (1 subgoal):
 1. \<And>sz fun y ya. \<lbrakk>kheap s p = Some (CNode sz fun); well_formed_cnode_n sz fun; fun c' = Some ya; length c = sz\<rbrakk> \<Longrightarrow> length c = length c' proof (prove)
goal (1 subgoal):
 1. \<And>sz fun y ya. \<lbrakk>kheap s p = Some (CNode sz fun); well_formed_cnode_n sz fun; length c = sz; length c' = sz\<rbrakk> \<Longrightarrow> length c = length c' proof (prove)
goal:
No subgoals!