theory RWHelper_DP

lemma strong_write_estimate_via_sep:
  assumes sep_valid: "\<And>obj Q. \<lbrace>\<lambda>s. < P \<and>* Q > s \<rbrace>
    f \<lbrace>\<lambda>r s. < P' \<and>* Q > s \<rbrace>"
  and sep_heap_dom: "sep_heap_dom P m"
  and sep_heap_dom': "sep_heap_dom P' m"
  and sep_irq_node_dom' : "sep_irq_node_dom P' m'"
  and sep_spec: "sep_map_spec P' state"
  shows "IsStrongSepWritingEstimateOf f (\<lambda>s. < P \<and>* Q> s)
    (\<lambda>s.  sep_heap (sep_state_projection s)) m (\<lambda>s. sep_heap state)" apply (clarsimp simp: valid_def IsStrongSepWritingEstimateOf_def) apply (drule sep_conj_spec) apply clarsimp apply (drule use_valid[OF _ sep_valid]) apply simp apply (rule conjI) apply simp apply (drule sep_map_dom_predicate[OF sep_heap_dom' sep_irq_node_dom']) apply (drule sep_specD[OF sep_spec]) apply (case_tac state,simp) apply (rule ext,clarsimp simp:restrict_map_def) apply (drule sep_conj_spec_value) apply (rule sep_heap_dom) apply simp apply (drule(1) sep_conj_spec_value[OF _ sep_heap_dom']) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. IsStrongSepWritingEstimateOf f (cdl.lift (P \<and>* Q)) (cdl.lift sep_heap) m (\<lambda>s. sep_heap state) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>cdl.lift (P \<and>* Q) s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b |` m = sep_heap state \<and> cdl.lift sep_heap b |` (UNIV - m) = cdl.lift sep_heap s |` (UNIV - m) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<exists>s'. cdl.lift (P \<and>* (=) s') s\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b |` m = sep_heap state \<and> cdl.lift sep_heap b |` (UNIV - m) = cdl.lift sep_heap s |` (UNIV - m) proof (prove)
goal (1 subgoal):
 1. \<And>s a b s'. \<lbrakk>(a, b) \<in> fst (f s); cdl.lift (P \<and>* (=) s') s\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b |` m = sep_heap state \<and> cdl.lift sep_heap b |` (UNIV - m) = cdl.lift sep_heap s |` (UNIV - m) proof (prove)
goal (2 subgoals):
 1. \<And>s a b s'. cdl.lift (P \<and>* (=) s') s \<Longrightarrow> cdl.lift (P \<and>* ?Q16 s a b s') s
 2. \<And>s a b s'. \<lbrakk>cdl.lift (P \<and>* (=) s') s; cdl.lift (P' \<and>* ?Q16 s a b s') b\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b |` m = sep_heap state \<and> cdl.lift sep_heap b |` (UNIV - m) = cdl.lift sep_heap s |` (UNIV - m) proof (prove)
goal (1 subgoal):
 1. \<And>s a b s'. \<lbrakk>cdl.lift (P \<and>* (=) s') s; cdl.lift (P' \<and>* (=) s') b\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b |` m = sep_heap state \<and> cdl.lift sep_heap b |` (UNIV - m) = cdl.lift sep_heap s |` (UNIV - m) proof (prove)
goal (2 subgoals):
 1. \<And>s a b s'. \<lbrakk>cdl.lift (P \<and>* (=) s') s; cdl.lift (P' \<and>* (=) s') b\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b |` m = sep_heap state
 2. \<And>s a b s'. \<lbrakk>cdl.lift (P \<and>* (=) s') s; cdl.lift (P' \<and>* (=) s') b\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b |` (UNIV - m) = cdl.lift sep_heap s |` (UNIV - m) proof (prove)
goal (2 subgoals):
 1. \<And>s b s'. \<lbrakk>cdl.lift (P \<and>* (=) s') s; cdl.lift (P' \<and>* (=) s') b\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b |` m = sep_heap state
 2. \<And>s a b s'. \<lbrakk>cdl.lift (P \<and>* (=) s') s; cdl.lift (P' \<and>* (=) s') b\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b |` (UNIV - m) = cdl.lift sep_heap s |` (UNIV - m) proof (prove)
goal (2 subgoals):
 1. \<And>s b s'. \<lbrakk>cdl.lift (P \<and>* (=) s') s; P' (SepState (cdl.lift sep_heap b |` m) (cdl.lift sep_irq_node b |` m'))\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b |` m = sep_heap state
 2. \<And>s a b s'. \<lbrakk>cdl.lift (P \<and>* (=) s') s; cdl.lift (P' \<and>* (=) s') b\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b |` (UNIV - m) = cdl.lift sep_heap s |` (UNIV - m) proof (prove)
goal (2 subgoals):
 1. \<And>s b s'. \<lbrakk>cdl.lift (P \<and>* (=) s') s; state = SepState (cdl.lift sep_heap b |` m) (cdl.lift sep_irq_node b |` m')\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b |` m = sep_heap state
 2. \<And>s a b s'. \<lbrakk>cdl.lift (P \<and>* (=) s') s; cdl.lift (P' \<and>* (=) s') b\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b |` (UNIV - m) = cdl.lift sep_heap s |` (UNIV - m) proof (prove)
goal (1 subgoal):
 1. \<And>s a b s'. \<lbrakk>cdl.lift (P \<and>* (=) s') s; cdl.lift (P' \<and>* (=) s') b\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b |` (UNIV - m) = cdl.lift sep_heap s |` (UNIV - m) proof (prove)
goal (1 subgoal):
 1. \<And>s b s' a ba. \<lbrakk>cdl.lift (P \<and>* (=) s') s; cdl.lift (P' \<and>* (=) s') b; (a, ba) \<notin> m\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b (a, ba) = cdl.lift sep_heap s (a, ba) proof (prove)
goal (3 subgoals):
 1. \<And>s b s' a ba. \<lbrakk>cdl.lift (P' \<and>* (=) s') b; (a, ba) \<notin> m\<rbrakk> \<Longrightarrow> sep_heap_dom P (?m34 s b s' a ba)
 2. \<And>s b s' a ba. \<lbrakk>cdl.lift (P' \<and>* (=) s') b; (a, ba) \<notin> m\<rbrakk> \<Longrightarrow> ?p34 s b s' a ba \<notin> ?m34 s b s' a ba
 3. \<And>s b s' a ba. \<lbrakk>cdl.lift (P' \<and>* (=) s') b; (a, ba) \<notin> m; sep_heap s' (?p34 s b s' a ba) = (cdl.lift sep_heap s |` (UNIV - ?m34 s b s' a ba)) (?p34 s b s' a ba)\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b (a, ba) = cdl.lift sep_heap s (a, ba) proof (prove)
goal (2 subgoals):
 1. \<And>s b s' a ba. \<lbrakk>cdl.lift (P' \<and>* (=) s') b; (a, ba) \<notin> m\<rbrakk> \<Longrightarrow> ?p34 s b s' a ba \<notin> m
 2. \<And>s b s' a ba. \<lbrakk>cdl.lift (P' \<and>* (=) s') b; (a, ba) \<notin> m; sep_heap s' (?p34 s b s' a ba) = (cdl.lift sep_heap s |` (UNIV - m)) (?p34 s b s' a ba)\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b (a, ba) = cdl.lift sep_heap s (a, ba) proof (prove)
goal (1 subgoal):
 1. \<And>s b s' a ba. \<lbrakk>cdl.lift (P' \<and>* (=) s') b; (a, ba) \<notin> m; sep_heap s' (a, ba) = (cdl.lift sep_heap s |` (UNIV - m)) (a, ba)\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b (a, ba) = cdl.lift sep_heap s (a, ba) proof (prove)
goal (1 subgoal):
 1. \<And>s b s' a ba. \<lbrakk>(a, ba) \<notin> m; sep_heap s' (a, ba) = (cdl.lift sep_heap s |` (UNIV - m)) (a, ba); sep_heap s' (a, ba) = (cdl.lift sep_heap b |` (UNIV - m)) (a, ba)\<rbrakk> \<Longrightarrow> cdl.lift sep_heap b (a, ba) = cdl.lift sep_heap s (a, ba) proof (prove)
goal:
No subgoals!