theory Recycle_C

lemma user_data_at_rf_sr_dom_s:
  "\<lbrakk> typ_at' UserDataT x s; (s, s') \<in> rf_sr \<rbrakk>
    \<Longrightarrow> {x ..+ 2 ^ pageBits} \<times> {SIndexVal, SIndexTyp 0}
    \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))" apply (drule rf_sr_heap_user_data_relation) apply (drule user_data_at_ko) apply (erule_tac x=x in cmap_relationE1) apply (simp only: heap_to_user_data_def Let_def ko_at_projectKO_opt) apply simp apply (drule h_t_valid_clift) apply (simp add: h_t_valid_dom_s pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at' UserDataT x s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> {x..+2 ^ pageBits} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at' UserDataT x s; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation\<rbrakk> \<Longrightarrow> {x..+2 ^ pageBits} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; ko_at' UserData x s\<rbrakk> \<Longrightarrow> {x..+2 ^ pageBits} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (2 subgoals):
 1. ko_at' UserData x s \<Longrightarrow> heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) x = Some ?y4
 2. \<And>y'. \<lbrakk>ko_at' UserData x s; heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) x = Some ?y4; cuser_user_data_relation ?y4 y'; cslift s' (PTR(user_data_C) x) = Some y'\<rbrakk> \<Longrightarrow> {x..+2 ^ pageBits} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (2 subgoals):
 1. ko_at' UserData x s \<Longrightarrow> map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState s)) x) (Some UserData) = Some ?y4
 2. \<And>y'. \<lbrakk>ko_at' UserData x s; heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) x = Some ?y4; cuser_user_data_relation ?y4 y'; cslift s' (PTR(user_data_C) x) = Some y'\<rbrakk> \<Longrightarrow> {x..+2 ^ pageBits} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>ko_at' UserData x s; heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) x = Some (byte_to_word_heap (underlying_memory (ksMachineState s)) x); cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) x) y'; cslift s' (PTR(user_data_C) x) = Some y'\<rbrakk> \<Longrightarrow> {x..+2 ^ pageBits} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>ko_at' UserData x s; heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)) x = Some (byte_to_word_heap (underlying_memory (ksMachineState s)) x); cuser_user_data_relation (byte_to_word_heap (underlying_memory (ksMachineState s)) x) y'; s' \<Turnstile>\<^sub>c PTR(user_data_C) x\<rbrakk> \<Longrightarrow> {x..+2 ^ pageBits} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal:
No subgoals!