theory Eval_CAMKES_CDL

lemma label_over_ptr_range_fp_eval:
  assumes "RangeMap.monotonic_key_ranges binds"
      and "\<And>x. label_spec x = map_option snd (RangeMap.range_map_of binds x)"
  shows
   "(\<forall>oref \<in> ptr_range (obj_id :: cdl_object_id) sz.
       case label_spec oref of Some l \<Rightarrow> P l | None \<Rightarrow> False)
     = (case RangeMap.range_map_of binds obj_id of
          Some ((obj_id', obj_end), l) \<Rightarrow>
             if obj_id' = obj_id \<and> obj_end = obj_id + 2^sz \<comment> \<open> = ptr_range\<close>
             then P l \<comment> \<open>this is the case we care about, the rest is just fluff\<close>
             else (label_over_ptr_range_FAILED (ptr_range obj_id sz)
                     (\<lambda>oref. case label_spec oref of Some l \<Rightarrow> P l | None \<Rightarrow> False))
        | None \<Rightarrow> (label_over_ptr_range_FAILED (ptr_range obj_id sz)
                     (\<lambda>oref. case label_spec oref of Some l \<Rightarrow> P l | None \<Rightarrow> False)))" apply (simp only: label_over_ptr_range_FAILED_def) 
  (* rewrite "P l" in RHS *)
   apply (subst option.case_cong[where ?f2.0="case_prod _", OF refl refl]) apply (clarsimp simp only:) apply wpfix apply (subst if_cong[OF refl _ refl]) apply (clarsimp simp only:) apply (erule label_over_ptr_range[OF assms, symmetric]) apply (rule refl) 
  (* now both sides are identical in all cases *)
   apply (fastforce simp only: split: option.splits if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some l \<Rightarrow> P l) = (case RangeMap.range_map_of binds obj_id of None \<Rightarrow> label_over_ptr_range_FAILED (ptr_range obj_id sz) (\<lambda>oref. case label_spec oref of None \<Rightarrow> False | Some l \<Rightarrow> P l) | Some ((obj_id', obj_end), l) \<Rightarrow> if obj_id' = obj_id \<and> obj_end = obj_id + 2 ^ sz then P l else label_over_ptr_range_FAILED (ptr_range obj_id sz) (\<lambda>oref. case label_spec oref of None \<Rightarrow> False | Some l \<Rightarrow> P l)) proof (prove)
goal (1 subgoal):
 1. (\<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some l \<Rightarrow> P l) = (case RangeMap.range_map_of binds obj_id of None \<Rightarrow> \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some l \<Rightarrow> P l | Some ((obj_id', obj_end), l) \<Rightarrow> if obj_id' = obj_id \<and> obj_end = obj_id + 2 ^ sz then P l else \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some l \<Rightarrow> P l) proof (prove)
goal (1 subgoal):
 1. (\<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some l \<Rightarrow> P l) = (case RangeMap.range_map_of binds obj_id of None \<Rightarrow> \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some l \<Rightarrow> P l | Some ((obj_id', obj_end), l) \<Rightarrow> if obj_id' = obj_id \<and> obj_end = obj_id + 2 ^ sz then P l else \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some l \<Rightarrow> P l) proof (prove)
goal (2 subgoals):
 1. \<And>x2. RangeMap.range_map_of binds obj_id = Some x2 \<Longrightarrow> (case x2 of ((obj_id', obj_end), l) \<Rightarrow> if obj_id' = obj_id \<and> obj_end = obj_id + 2 ^ sz then P l else \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x) = ?g2.0 x2
 2. (\<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x) = (case RangeMap.range_map_of binds obj_id of None \<Rightarrow> \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x | Some x \<Rightarrow> ?g2.0 x) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. RangeMap.range_map_of binds obj_id = Some ((a, b), ba) \<Longrightarrow> (if a = obj_id \<and> b = obj_id + 2 ^ sz then P ba else \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x) = ?g2.0 ((a, b), ba)
 2. (\<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x) = (case RangeMap.range_map_of binds obj_id of None \<Rightarrow> \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x | Some x \<Rightarrow> ?g2.0 x) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. RangeMap.range_map_of binds obj_id = Some ((a, b), ba) \<Longrightarrow> (if a = obj_id \<and> b = obj_id + 2 ^ sz then P ba else \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x) = ?g2.6 a b (a, b) ba ((a, b), ba)
 2. (\<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x) = (case RangeMap.range_map_of binds obj_id of None \<Rightarrow> \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x | Some x1 \<Rightarrow> ?g2.6 (fst (fst x1)) (snd (fst x1)) (fst x1) (snd x1) x1) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba. \<lbrakk>RangeMap.range_map_of binds obj_id = Some ((a, b), ba); a = obj_id \<and> b = obj_id + 2 ^ sz\<rbrakk> \<Longrightarrow> P ba = ?u8 a b ba
 2. \<And>a b ba. RangeMap.range_map_of binds obj_id = Some ((a, b), ba) \<Longrightarrow> (if a = obj_id \<and> b = obj_id + 2 ^ sz then ?u8 a b ba else \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x) = ?g2.9 a a b b ba (a, b) ba ((a, b), ba)
 3. (\<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x) = (case RangeMap.range_map_of binds obj_id of None \<Rightarrow> \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x | Some x1 \<Rightarrow> ?g2.6 (fst (fst x1)) (snd (fst x1)) (fst x1) (snd x1) x1)
flex-flex pairs:
\<lambda>a b ba. ?g2.9 a a b b ba (a, b) ba ((a, b), ba) \<equiv>\<^sup>? \<lambda>a b ba. ?g2.6 a b (a, b) ba ((a, b), ba) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba. RangeMap.range_map_of binds obj_id = Some ((obj_id, obj_id + 2 ^ sz), ba) \<Longrightarrow> P ba = ?u8 obj_id (obj_id + 2 ^ sz) ba
 2. \<And>a b ba. RangeMap.range_map_of binds obj_id = Some ((a, b), ba) \<Longrightarrow> (if a = obj_id \<and> b = obj_id + 2 ^ sz then ?u8 a b ba else \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x) = ?g2.9 a a b b ba (a, b) ba ((a, b), ba)
 3. (\<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x) = (case RangeMap.range_map_of binds obj_id of None \<Rightarrow> \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x | Some x1 \<Rightarrow> ?g2.6 (fst (fst x1)) (snd (fst x1)) (fst x1) (snd x1) x1)
flex-flex pairs:
\<lambda>a b ba. ?g2.9 a a b b ba (a, b) ba ((a, b), ba) \<equiv>\<^sup>? \<lambda>a b ba. ?g2.6 a b (a, b) ba ((a, b), ba) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. RangeMap.range_map_of binds obj_id = Some ((a, b), ba) \<Longrightarrow> (if a = obj_id \<and> b = obj_id + 2 ^ sz then \<forall>oref\<in>ptr_range a sz. case label_spec oref of None \<Rightarrow> False | Some l \<Rightarrow> P l else \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x) = ?g2.9 a a b b ba (a, b) ba ((a, b), ba)
 2. (\<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x) = (case RangeMap.range_map_of binds obj_id of None \<Rightarrow> \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x | Some x1 \<Rightarrow> ?g2.6 (fst (fst x1)) (snd (fst x1)) (fst x1) (snd x1) x1)
flex-flex pairs:
\<lambda>a b ba. ?g2.9 a a b b ba (a, b) ba ((a, b), ba) \<equiv>\<^sup>? \<lambda>a b ba. ?g2.6 a b (a, b) ba ((a, b), ba) proof (prove)
goal (1 subgoal):
 1. (\<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x) = (case RangeMap.range_map_of binds obj_id of None \<Rightarrow> \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x | Some x1 \<Rightarrow> if fst (fst x1) = obj_id \<and> snd (fst x1) = obj_id + 2 ^ sz then \<forall>oref\<in>ptr_range (fst (fst x1)) sz. case label_spec oref of None \<Rightarrow> False | Some l \<Rightarrow> P l else \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some a \<Rightarrow> P a) proof (prove)
goal (1 subgoal):
 1. (\<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x) = (case RangeMap.range_map_of binds obj_id of None \<Rightarrow> \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some x \<Rightarrow> P x | Some x1 \<Rightarrow> if fst (fst x1) = obj_id \<and> snd (fst x1) = obj_id + 2 ^ sz then \<forall>oref\<in>ptr_range (fst (fst x1)) sz. case label_spec oref of None \<Rightarrow> False | Some l \<Rightarrow> P l else \<forall>oref\<in>ptr_range obj_id sz. case label_spec oref of None \<Rightarrow> False | Some a \<Rightarrow> P a) proof (prove)
goal:
No subgoals!