theory RWHelper_DP

lemma ReadingEstimateOf_inter:
  "\<lbrakk>IsReadingEstimateOf a f r; IsReadingEstimateOf b f r \<rbrakk> \<Longrightarrow> IsReadingEstimateOf (a \<inter> b) f r" apply (clarsimp simp:IsReadingEstimateOf_def) apply (drule_tac x = s in spec) apply (drule_tac x = "(\<lambda>ptr. if ptr\<in>(b - a) then (s' ptr) else (s ptr))" in spec) apply (drule_tac x = "(\<lambda>ptr. if ptr\<in>(b - a) then (s' ptr) else (s ptr))" in spec) apply (drule_tac x = s' in spec) apply (erule impE) apply (simp add:eq_on_def) apply (erule impE) apply (simp add:eq_on_def) apply (rule eq_on_trans) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>IsReadingEstimateOf a f r; IsReadingEstimateOf b f r\<rbrakk> \<Longrightarrow> IsReadingEstimateOf (a \<inter> b) f r proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>s s'. eq_on a s s' \<longrightarrow> eq_on r (f s) (f s'); \<forall>s s'. eq_on b s s' \<longrightarrow> eq_on r (f s) (f s'); eq_on (a \<inter> b) s s'\<rbrakk> \<Longrightarrow> eq_on r (f s) (f s') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>s s'. eq_on b s s' \<longrightarrow> eq_on r (f s) (f s'); eq_on (a \<inter> b) s s'; \<forall>s'. eq_on a s s' \<longrightarrow> eq_on r (f s) (f s')\<rbrakk> \<Longrightarrow> eq_on r (f s) (f s') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>eq_on (a \<inter> b) s s'; \<forall>s'. eq_on a s s' \<longrightarrow> eq_on r (f s) (f s'); \<forall>s'a. eq_on b (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr) s'a \<longrightarrow> eq_on r (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr)) (f s'a)\<rbrakk> \<Longrightarrow> eq_on r (f s) (f s') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>eq_on (a \<inter> b) s s'; \<forall>s'a. eq_on b (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr) s'a \<longrightarrow> eq_on r (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr)) (f s'a); eq_on a s (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr) \<longrightarrow> eq_on r (f s) (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr))\<rbrakk> \<Longrightarrow> eq_on r (f s) (f s') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>eq_on (a \<inter> b) s s'; eq_on a s (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr) \<longrightarrow> eq_on r (f s) (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr)); eq_on b (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr) s' \<longrightarrow> eq_on r (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr)) (f s')\<rbrakk> \<Longrightarrow> eq_on r (f s) (f s') proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>eq_on (a \<inter> b) s s'; eq_on b (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr) s' \<longrightarrow> eq_on r (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr)) (f s')\<rbrakk> \<Longrightarrow> eq_on a s (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr)
 2. \<And>s s'. \<lbrakk>eq_on (a \<inter> b) s s'; eq_on b (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr) s' \<longrightarrow> eq_on r (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr)) (f s'); eq_on r (f s) (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr))\<rbrakk> \<Longrightarrow> eq_on r (f s) (f s') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>eq_on (a \<inter> b) s s'; eq_on b (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr) s' \<longrightarrow> eq_on r (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr)) (f s'); eq_on r (f s) (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr))\<rbrakk> \<Longrightarrow> eq_on r (f s) (f s') proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>eq_on (a \<inter> b) s s'; eq_on r (f s) (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr))\<rbrakk> \<Longrightarrow> eq_on b (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr) s'
 2. \<And>s s'. \<lbrakk>eq_on (a \<inter> b) s s'; eq_on r (f s) (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr)); eq_on r (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr)) (f s')\<rbrakk> \<Longrightarrow> eq_on r (f s) (f s') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>eq_on (a \<inter> b) s s'; eq_on r (f s) (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr)); eq_on r (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr)) (f s')\<rbrakk> \<Longrightarrow> eq_on r (f s) (f s') proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>eq_on (a \<inter> b) s s'; eq_on r (f s) (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr)); eq_on r (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr)) (f s')\<rbrakk> \<Longrightarrow> eq_on r (f s) (?sa24 s s')
 2. \<And>s s'. \<lbrakk>eq_on (a \<inter> b) s s'; eq_on r (f s) (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr)); eq_on r (f (\<lambda>ptr. if ptr \<in> b - a then s' ptr else s ptr)) (f s')\<rbrakk> \<Longrightarrow> eq_on r (?sa24 s s') (f s') proof (prove)
goal:
No subgoals!