theory Retype_C

lemma typ_bytes_cpspace_relation_clift_gptr:
assumes "cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState (s::kernel_state))) hp"
  and "is_aligned ptr bits" "bits < word_bits"
  and "pspace_aligned' s"
  and "kernel_data_refs \<inter> {ptr ..+ 2^bits} = {}"
  and "ptr_span (ptr' :: 'a ptr) \<subseteq> kernel_data_refs"
  and "typ_uinfo_t TYPE('a :: mem_type) \<noteq> typ_uinfo_t TYPE(8 word)"
 shows "clift (hrs_htd_update (typ_region_bytes ptr bits) hp)
    ptr'
  = (clift hp) ptr'"
  (is "?lhs = ?rhs ptr'") using assms apply - apply (case_tac "ptr' \<notin> dom ?rhs") apply (frule contra_subsetD[OF typ_region_bytes_dom[where ptr = ptr and bits = bits], rotated]) apply simp apply fastforce apply (clarsimp simp: liftt_if hrs_htd_update_def split_def split: if_splits) apply (simp add: h_t_valid_typ_region_bytes) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) ptr' = clift hp ptr' proof (prove)
using this:
cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp
is_aligned ptr bits
bits < word_bits
pspace_aligned' s
kernel_data_refs \<inter> {ptr..+2 ^ bits} = {}
ptr_span ptr' \<subseteq> kernel_data_refs
typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word)

goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) ptr' = clift hp ptr' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; kernel_data_refs \<inter> {ptr..+2 ^ bits} = {}; ptr_span ptr' \<subseteq> kernel_data_refs; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (typ_region_bytes ptr bits) hp) ptr' = clift hp ptr' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; kernel_data_refs \<inter> {ptr..+2 ^ bits} = {}; ptr_span ptr' \<subseteq> kernel_data_refs; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); ptr' \<notin> dom (clift hp)\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (typ_region_bytes ptr bits) hp) ptr' = clift hp ptr'
 2. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; kernel_data_refs \<inter> {ptr..+2 ^ bits} = {}; ptr_span ptr' \<subseteq> kernel_data_refs; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); \<not> ptr' \<notin> dom (clift hp)\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (typ_region_bytes ptr bits) hp) ptr' = clift hp ptr' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; kernel_data_refs \<inter> {ptr..+2 ^ bits} = {}; ptr_span ptr' \<subseteq> kernel_data_refs; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); ptr' \<notin> dom (clift hp)\<rbrakk> \<Longrightarrow> typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word)
 2. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; kernel_data_refs \<inter> {ptr..+2 ^ bits} = {}; ptr_span ptr' \<subseteq> kernel_data_refs; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); ptr' \<notin> dom (clift hp); ptr' \<notin> dom (clift (hrs_htd_update (typ_region_bytes ptr bits) hp))\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (typ_region_bytes ptr bits) hp) ptr' = clift hp ptr'
 3. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; kernel_data_refs \<inter> {ptr..+2 ^ bits} = {}; ptr_span ptr' \<subseteq> kernel_data_refs; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); \<not> ptr' \<notin> dom (clift hp)\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (typ_region_bytes ptr bits) hp) ptr' = clift hp ptr' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; kernel_data_refs \<inter> {ptr..+2 ^ bits} = {}; ptr_span ptr' \<subseteq> kernel_data_refs; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); ptr' \<notin> dom (clift hp); ptr' \<notin> dom (clift (hrs_htd_update (typ_region_bytes ptr bits) hp))\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (typ_region_bytes ptr bits) hp) ptr' = clift hp ptr'
 2. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; kernel_data_refs \<inter> {ptr..+2 ^ bits} = {}; ptr_span ptr' \<subseteq> kernel_data_refs; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); \<not> ptr' \<notin> dom (clift hp)\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (typ_region_bytes ptr bits) hp) ptr' = clift hp ptr' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; kernel_data_refs \<inter> {ptr..+2 ^ bits} = {}; ptr_span ptr' \<subseteq> kernel_data_refs; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); \<not> ptr' \<notin> dom (clift hp)\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (typ_region_bytes ptr bits) hp) ptr' = clift hp ptr' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; kernel_data_refs \<inter> {ptr..+2 ^ bits} = {}; ptr_span ptr' \<subseteq> kernel_data_refs; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); snd hp \<Turnstile>\<^sub>t ptr'\<rbrakk> \<Longrightarrow> typ_region_bytes ptr bits (snd hp) \<Turnstile>\<^sub>t ptr' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; kernel_data_refs \<inter> {ptr..+2 ^ bits} = {}; ptr_span ptr' \<subseteq> kernel_data_refs; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); snd hp \<Turnstile>\<^sub>t ptr'\<rbrakk> \<Longrightarrow> ptr_span ptr' \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal:
No subgoals!