theory RangeMap

lemma combine_contiguous_ranges_rev_correct:
  "monotonic_key_ranges xs \<Longrightarrow>
   Union (set (map (Collect o in_range o fst) xs))
    = Union (set (map (Collect o in_range) (combine_contiguous_ranges_rev (map fst xs))))" 
  (* FIXME: cleanup *)
   apply (induct xs rule: monotonic_key_ranges.induct) subgoal supply combine_contiguous_ranges_rev.simps[simp del] apply (clarsimp simp: combine_contiguous_ranges_rev.simps(1)[where xs="_#_"]
                      split: list.splits) apply (drule(1) combine_contiguous_ranges_rev_head_helper) apply simp apply (rule refl) apply (fastforce dest: atLeastLessThan_union_contiguous monotonic_ranges_each_valid) done apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monotonic_key_ranges xs \<Longrightarrow> \<Union> (set (map (Collect \<circ> in_range \<circ> fst) xs)) = \<Union> (set (map (Collect \<circ> in_range) (combine_contiguous_ranges_rev (map fst xs)))) proof (prove)
goal (1 subgoal):
 1. monotonic_key_ranges xs \<Longrightarrow> \<Union> (set (map (Collect \<circ> in_range \<circ> fst) xs)) = \<Union> (set (map (Collect \<circ> in_range) (combine_contiguous_ranges_rev (map fst xs)))) proof (prove)
goal (3 subgoals):
 1. \<And>start end uu_ start' end' v' kvs. \<lbrakk>monotonic_key_ranges (((start', end'), v') # kvs) \<Longrightarrow> \<Union> (set (map (Collect \<circ> in_range \<circ> fst) (((start', end'), v') # kvs))) = \<Union> (set (map (Collect \<circ> in_range) (combine_contiguous_ranges_rev (map fst (((start', end'), v') # kvs))))); monotonic_key_ranges (((start, end), uu_) # ((start', end'), v') # kvs)\<rbrakk> \<Longrightarrow> \<Union> (set (map (Collect \<circ> in_range \<circ> fst) (((start, end), uu_) # ((start', end'), v') # kvs))) = \<Union> (set (map (Collect \<circ> in_range) (combine_contiguous_ranges_rev (map fst (((start, end), uu_) # ((start', end'), v') # kvs)))))
 2. \<And>start end uv_. monotonic_key_ranges [((start, end), uv_)] \<Longrightarrow> \<Union> (set (map (Collect \<circ> in_range \<circ> fst) [((start, end), uv_)])) = \<Union> (set (map (Collect \<circ> in_range) (combine_contiguous_ranges_rev (map fst [((start, end), uv_)]))))
 3. monotonic_key_ranges [] \<Longrightarrow> \<Union> (set (map (Collect \<circ> in_range \<circ> fst) [])) = \<Union> (set (map (Collect \<circ> in_range) (combine_contiguous_ranges_rev (map fst [])))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monotonic_key_ranges (((start'_, end'_), v'_) # kvs_) \<Longrightarrow> \<Union> (set (map (Collect \<circ> in_range \<circ> fst) (((start'_, end'_), v'_) # kvs_))) = \<Union> (set (map (Collect \<circ> in_range) (combine_contiguous_ranges_rev (map fst (((start'_, end'_), v'_) # kvs_))))); monotonic_key_ranges (((start_, end_), uu_) # ((start'_, end'_), v'_) # kvs_)\<rbrakk> \<Longrightarrow> \<Union> (set (map (Collect \<circ> in_range \<circ> fst) (((start_, end_), uu_) # ((start'_, end'_), v'_) # kvs_))) = \<Union> (set (map (Collect \<circ> in_range) (combine_contiguous_ranges_rev (map fst (((start_, end_), uu_) # ((start'_, end'_), v'_) # kvs_))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monotonic_key_ranges (((start'_, end'_), v'_) # kvs_) \<Longrightarrow> \<Union> (set (map (Collect \<circ> in_range \<circ> fst) (((start'_, end'_), v'_) # kvs_))) = \<Union> (set (map (Collect \<circ> in_range) (combine_contiguous_ranges_rev (map fst (((start'_, end'_), v'_) # kvs_))))); monotonic_key_ranges (((start_, end_), uu_) # ((start'_, end'_), v'_) # kvs_)\<rbrakk> \<Longrightarrow> \<Union> (set (map (Collect \<circ> in_range \<circ> fst) (((start_, end_), uu_) # ((start'_, end'_), v'_) # kvs_))) = \<Union> (set (map (Collect \<circ> in_range) (combine_contiguous_ranges_rev (map fst (((start_, end_), uu_) # ((start'_, end'_), v'_) # kvs_))))) proof (prove)
goal (1 subgoal):
 1. \<And>b x22. \<lbrakk>{start'_..<end'_} \<union> (\<Union>x\<in>set kvs_. {fst (fst x)..<snd (fst x)}) = {end_..<b} \<union> (\<Union>x\<in>set x22. {fst x..<snd x}); start_ \<le> end_; end_ \<le> start'_; monotonic_key_ranges (((start'_, end'_), v'_) # kvs_); combine_contiguous_ranges_rev ((start'_, end'_) # map fst kvs_) = (end_, b) # x22\<rbrakk> \<Longrightarrow> {start_..<end_} \<union> ({end_..<b} \<union> (\<Union>x\<in>set x22. {fst x..<snd x})) = {start_..<b} \<union> (\<Union>x\<in>set x22. {fst x..<snd x}) proof (prove)
goal (3 subgoals):
 1. \<And>b x22. \<lbrakk>{start'_..<end'_} \<union> (\<Union>x\<in>set kvs_. {fst (fst x)..<snd (fst x)}) = {end_..<b} \<union> (\<Union>x\<in>set x22. {fst x..<snd x}); start_ \<le> end_; end_ \<le> start'_; monotonic_key_ranges (((start'_, end'_), v'_) # kvs_)\<rbrakk> \<Longrightarrow> (start'_, end'_) # map fst kvs_ = map fst (((start'_, end'_), v'_) # kvs_)
 2. \<And>b x22. \<lbrakk>{start'_..<end'_} \<union> (\<Union>x\<in>set kvs_. {fst (fst x)..<snd (fst x)}) = {end_..<b} \<union> (\<Union>x\<in>set x22. {fst x..<snd x}); start_ \<le> end_; end_ \<le> start'_; monotonic_key_ranges (((start'_, end'_), v'_) # kvs_)\<rbrakk> \<Longrightarrow> (start'_, end'_) # map fst kvs_ = (?start28 b x22, ?end28 b x22) # ?ks_tl28 b x22
 3. \<And>b x22. \<lbrakk>{start'_..<end'_} \<union> (\<Union>x\<in>set kvs_. {fst (fst x)..<snd (fst x)}) = {end_..<b} \<union> (\<Union>x\<in>set x22. {fst x..<snd x}); start_ \<le> end_; end_ \<le> start'_; monotonic_key_ranges (((start'_, end'_), v'_) # kvs_); ?start28 b x22 = end_ \<and> ?end28 b x22 \<le> b\<rbrakk> \<Longrightarrow> {start_..<end_} \<union> ({end_..<b} \<union> (\<Union>x\<in>set x22. {fst x..<snd x})) = {start_..<b} \<union> (\<Union>x\<in>set x22. {fst x..<snd x}) proof (prove)
goal (2 subgoals):
 1. \<And>b x22. \<lbrakk>{start'_..<end'_} \<union> (\<Union>x\<in>set kvs_. {fst (fst x)..<snd (fst x)}) = {end_..<b} \<union> (\<Union>x\<in>set x22. {fst x..<snd x}); start_ \<le> end_; end_ \<le> start'_; monotonic_key_ranges (((start'_, end'_), v'_) # kvs_)\<rbrakk> \<Longrightarrow> (start'_, end'_) # map fst kvs_ = (?start28 b x22, ?end28 b x22) # ?ks_tl28 b x22
 2. \<And>b x22. \<lbrakk>{start'_..<end'_} \<union> (\<Union>x\<in>set kvs_. {fst (fst x)..<snd (fst x)}) = {end_..<b} \<union> (\<Union>x\<in>set x22. {fst x..<snd x}); start_ \<le> end_; end_ \<le> start'_; monotonic_key_ranges (((start'_, end'_), v'_) # kvs_); ?start28 b x22 = end_ \<and> ?end28 b x22 \<le> b\<rbrakk> \<Longrightarrow> {start_..<end_} \<union> ({end_..<b} \<union> (\<Union>x\<in>set x22. {fst x..<snd x})) = {start_..<b} \<union> (\<Union>x\<in>set x22. {fst x..<snd x}) proof (prove)
goal (1 subgoal):
 1. \<And>b x22. \<lbrakk>{start'_..<end'_} \<union> (\<Union>x\<in>set kvs_. {fst (fst x)..<snd (fst x)}) = {end_..<b} \<union> (\<Union>x\<in>set x22. {fst x..<snd x}); start_ \<le> end_; end_ \<le> start'_; monotonic_key_ranges (((start'_, end'_), v'_) # kvs_); start'_ = end_ \<and> end'_ \<le> b\<rbrakk> \<Longrightarrow> {start_..<end_} \<union> ({end_..<b} \<union> (\<Union>x\<in>set x22. {fst x..<snd x})) = {start_..<b} \<union> (\<Union>x\<in>set x22. {fst x..<snd x}) proof (prove)
goal:
No subgoals! proof (prove)
goal (2 subgoals):
 1. \<And>start end uv_. monotonic_key_ranges [((start, end), uv_)] \<Longrightarrow> \<Union> (set (map (Collect \<circ> in_range \<circ> fst) [((start, end), uv_)])) = \<Union> (set (map (Collect \<circ> in_range) (combine_contiguous_ranges_rev (map fst [((start, end), uv_)]))))
 2. monotonic_key_ranges [] \<Longrightarrow> \<Union> (set (map (Collect \<circ> in_range \<circ> fst) [])) = \<Union> (set (map (Collect \<circ> in_range) (combine_contiguous_ranges_rev (map fst [])))) proof (prove)
goal:
No subgoals!