theory CSpaceInv_AI

lemma tcb_cap_valid_update_free_index[simp]:
  "tcb_cap_valid (cap\<lparr>free_index:=a\<rparr>) slot s = tcb_cap_valid cap slot s" apply (rule iffI) apply (clarsimp simp: tcb_cap_valid_def) apply (intro conjI impI allI) apply (clarsimp simp: tcb_at_def pred_tcb_at_def is_tcb_def obj_at_def
                   dest!: get_tcb_SomeD) apply (clarsimp simp: tcb_cap_cases_def free_index_update_def is_cap_simps
                          is_nondevice_page_cap_simps
                   dest!: is_valid_vtable_root_is_arch_cap
                   split: if_splits cap.split_asm Structures_A.thread_state.split_asm) apply (clarsimp simp: pred_tcb_at_def obj_at_def is_cap_simps free_index_update_def
                         is_nondevice_page_cap_simps
                  split: cap.split_asm) apply (clarsimp simp: tcb_cap_valid_def) apply (intro conjI impI allI) apply (clarsimp simp: tcb_at_def pred_tcb_at_def is_tcb_def obj_at_def
                  dest!: get_tcb_SomeD) apply (clarsimp simp: tcb_cap_cases_def free_index_update_def is_cap_simps
                         is_nondevice_page_cap_simps
                  dest!: is_valid_vtable_root_is_arch_cap
                  split: if_splits cap.split_asm Structures_A.thread_state.split_asm) apply (clarsimp simp: pred_tcb_at_def obj_at_def is_cap_simps free_index_update_def
                        valid_ipc_buffer_cap_def
                 split: cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cap_valid (free_index_update (\<lambda>_. a) cap) slot s = tcb_cap_valid cap slot s proof (prove)
goal (2 subgoals):
 1. tcb_cap_valid (free_index_update (\<lambda>_. a) cap) slot s \<Longrightarrow> tcb_cap_valid cap slot s
 2. tcb_cap_valid cap slot s \<Longrightarrow> tcb_cap_valid (free_index_update (\<lambda>_. a) cap) slot s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcb_at (fst slot) s; st_tcb_at (\<lambda>st. case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) st (free_index_update (\<lambda>_. a) cap)) (fst slot) s; snd slot = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst slot) s \<longrightarrow> valid_ipc_buffer_cap (free_index_update (\<lambda>_. a) cap) (tcb_ipc_buffer tcb))\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) st cap) (fst slot) s \<and> (snd slot = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst slot) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))
 2. tcb_cap_valid cap slot s \<Longrightarrow> tcb_cap_valid (free_index_update (\<lambda>_. a) cap) slot s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>tcb_at (fst slot) s; st_tcb_at (\<lambda>st. case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) st (free_index_update (\<lambda>_. a) cap)) (fst slot) s; snd slot = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst slot) s \<longrightarrow> valid_ipc_buffer_cap (free_index_update (\<lambda>_. a) cap) (tcb_ipc_buffer tcb))\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) st cap) (fst slot) s
 2. \<And>tcb. \<lbrakk>tcb_at (fst slot) s; st_tcb_at (\<lambda>st. case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) st (free_index_update (\<lambda>_. a) cap)) (fst slot) s; snd slot = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst slot) s \<longrightarrow> valid_ipc_buffer_cap (free_index_update (\<lambda>_. a) cap) (tcb_ipc_buffer tcb)); snd slot = tcb_cnode_index 4; ko_at (TCB tcb) (fst slot) s\<rbrakk> \<Longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)
 3. tcb_cap_valid cap slot s \<Longrightarrow> tcb_cap_valid (free_index_update (\<lambda>_. a) cap) slot s proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrakk>snd slot = tcb_cnode_index 4 \<longrightarrow> valid_ipc_buffer_cap (free_index_update (\<lambda>_. a) cap) (tcb_ipc_buffer tcb); kheap s (fst slot) = Some (TCB tcb); case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) (itcb_state (tcb_to_itcb tcb)) (free_index_update (\<lambda>_. a) cap)\<rbrakk> \<Longrightarrow> case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) (itcb_state (tcb_to_itcb tcb)) cap
 2. \<And>tcb. \<lbrakk>tcb_at (fst slot) s; st_tcb_at (\<lambda>st. case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) st (free_index_update (\<lambda>_. a) cap)) (fst slot) s; snd slot = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst slot) s \<longrightarrow> valid_ipc_buffer_cap (free_index_update (\<lambda>_. a) cap) (tcb_ipc_buffer tcb)); snd slot = tcb_cnode_index 4; ko_at (TCB tcb) (fst slot) s\<rbrakk> \<Longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)
 3. tcb_cap_valid cap slot s \<Longrightarrow> tcb_cap_valid (free_index_update (\<lambda>_. a) cap) slot s proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>tcb_at (fst slot) s; st_tcb_at (\<lambda>st. case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) st (free_index_update (\<lambda>_. a) cap)) (fst slot) s; snd slot = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst slot) s \<longrightarrow> valid_ipc_buffer_cap (free_index_update (\<lambda>_. a) cap) (tcb_ipc_buffer tcb)); snd slot = tcb_cnode_index 4; ko_at (TCB tcb) (fst slot) s\<rbrakk> \<Longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)
 2. tcb_cap_valid cap slot s \<Longrightarrow> tcb_cap_valid (free_index_update (\<lambda>_. a) cap) slot s proof (prove)
goal (1 subgoal):
 1. tcb_cap_valid cap slot s \<Longrightarrow> tcb_cap_valid (free_index_update (\<lambda>_. a) cap) slot s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_at (fst slot) s; st_tcb_at (\<lambda>st. case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) st cap) (fst slot) s; snd slot = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst slot) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) st (free_index_update (\<lambda>_. a) cap)) (fst slot) s \<and> (snd slot = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst slot) s \<longrightarrow> valid_ipc_buffer_cap (free_index_update (\<lambda>_. a) cap) (tcb_ipc_buffer tcb))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcb_at (fst slot) s; st_tcb_at (\<lambda>st. case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) st cap) (fst slot) s; snd slot = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst slot) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) st (free_index_update (\<lambda>_. a) cap)) (fst slot) s
 2. \<And>tcb. \<lbrakk>tcb_at (fst slot) s; st_tcb_at (\<lambda>st. case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) st cap) (fst slot) s; snd slot = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst slot) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)); snd slot = tcb_cnode_index 4; ko_at (TCB tcb) (fst slot) s\<rbrakk> \<Longrightarrow> valid_ipc_buffer_cap (free_index_update (\<lambda>_. a) cap) (tcb_ipc_buffer tcb) proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>snd slot = tcb_cnode_index 4 \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb); kheap s (fst slot) = Some (TCB tcb); case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) (itcb_state (tcb_to_itcb tcb)) cap\<rbrakk> \<Longrightarrow> case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) (itcb_state (tcb_to_itcb tcb)) (free_index_update (\<lambda>_. a) cap)
 2. \<And>tcb. \<lbrakk>tcb_at (fst slot) s; st_tcb_at (\<lambda>st. case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) st cap) (fst slot) s; snd slot = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst slot) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)); snd slot = tcb_cnode_index 4; ko_at (TCB tcb) (fst slot) s\<rbrakk> \<Longrightarrow> valid_ipc_buffer_cap (free_index_update (\<lambda>_. a) cap) (tcb_ipc_buffer tcb) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>tcb_at (fst slot) s; st_tcb_at (\<lambda>st. case tcb_cap_cases (snd slot) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst slot) st cap) (fst slot) s; snd slot = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst slot) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)); snd slot = tcb_cnode_index 4; ko_at (TCB tcb) (fst slot) s\<rbrakk> \<Longrightarrow> valid_ipc_buffer_cap (free_index_update (\<lambda>_. a) cap) (tcb_ipc_buffer tcb) proof (prove)
goal:
No subgoals!