theory RangeMap

lemma combine_contiguous_ranges_rev_head_helper:
  "\<lbrakk> combine_contiguous_ranges_rev ks = ((start', end') # ks_tl');
     monotonic_key_ranges kvs; ks = map fst kvs; ks = (start, end) # ks_tl
   \<rbrakk> \<Longrightarrow>
   start = start' \<and> end \<le> end'" 
  (* FIXME: cleanup *)
   apply (induct kvs arbitrary: ks start "end" start' end' ks_tl ks_tl'
                rule: monotonic_key_ranges.induct) apply (clarsimp simp del: combine_contiguous_ranges_rev.simps) apply (drule_tac x="(start', end') # map fst kvs" in meta_spec) apply (drule_tac x="start'" in meta_spec) apply (clarsimp simp del: combine_contiguous_ranges_rev.simps) apply (simp only: combine_contiguous_ranges_rev.simps(1)[where xs = "_#_"]) apply (fastforce dest: monotonic_ranges_each_valid split: list.splits if_splits) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>combine_contiguous_ranges_rev ks = (start', end') # ks_tl'; monotonic_key_ranges kvs; ks = map fst kvs; ks = (start, end) # ks_tl\<rbrakk> \<Longrightarrow> start = start' \<and> end \<le> end' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>combine_contiguous_ranges_rev ks = (start', end') # ks_tl'; monotonic_key_ranges kvs; ks = map fst kvs; ks = (start, end) # ks_tl\<rbrakk> \<Longrightarrow> start = start' \<and> end \<le> end' proof (prove)
goal (3 subgoals):
 1. \<And>start end uu_ start' end' v' kvs ks starta enda start'a end'a ks_tl ks_tl'. \<lbrakk>\<And>ks start end start'a end'a ks_tl ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ks = (start'a, end'a) # ks_tl'; monotonic_key_ranges (((start', end'), v') # kvs); ks = map fst (((start', end'), v') # kvs); ks = (start, end) # ks_tl\<rbrakk> \<Longrightarrow> start = start'a \<and> end \<le> end'a; combine_contiguous_ranges_rev ks = (start'a, end'a) # ks_tl'; monotonic_key_ranges (((start, end), uu_) # ((start', end'), v') # kvs); ks = map fst (((start, end), uu_) # ((start', end'), v') # kvs); ks = (starta, enda) # ks_tl\<rbrakk> \<Longrightarrow> starta = start'a \<and> enda \<le> end'a
 2. \<And>start end uv_ ks starta enda start' end' ks_tl ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ks = (start', end') # ks_tl'; monotonic_key_ranges [((start, end), uv_)]; ks = map fst [((start, end), uv_)]; ks = (starta, enda) # ks_tl\<rbrakk> \<Longrightarrow> starta = start' \<and> enda \<le> end'
 3. \<And>ks start end start' end' ks_tl ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ks = (start', end') # ks_tl'; monotonic_key_ranges []; ks = map fst []; ks = (start, end) # ks_tl\<rbrakk> \<Longrightarrow> start = start' \<and> end \<le> end' proof (prove)
goal (3 subgoals):
 1. \<And>start end start' end' v' kvs start'a end'a ks_tl'. \<lbrakk>\<And>ks start start'a end'a ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ((start', end') # map fst kvs) = (start'a, end'a) # ks_tl'; start = start'; ks = (start', end') # map fst kvs\<rbrakk> \<Longrightarrow> start' = start'a \<and> end' \<le> end'a; combine_contiguous_ranges_rev ((start, end) # (start', end') # map fst kvs) = (start'a, end'a) # ks_tl'; start \<le> end; end \<le> start'; monotonic_key_ranges (((start', end'), v') # kvs)\<rbrakk> \<Longrightarrow> start = start'a \<and> end \<le> end'a
 2. \<And>start end uv_ ks starta enda start' end' ks_tl ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ks = (start', end') # ks_tl'; monotonic_key_ranges [((start, end), uv_)]; ks = map fst [((start, end), uv_)]; ks = (starta, enda) # ks_tl\<rbrakk> \<Longrightarrow> starta = start' \<and> enda \<le> end'
 3. \<And>ks start end start' end' ks_tl ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ks = (start', end') # ks_tl'; monotonic_key_ranges []; ks = map fst []; ks = (start, end) # ks_tl\<rbrakk> \<Longrightarrow> start = start' \<and> end \<le> end' proof (prove)
goal (3 subgoals):
 1. \<And>start end start' end' v' kvs start'a end'a ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ((start, end) # (start', end') # map fst kvs) = (start'a, end'a) # ks_tl'; start \<le> end; end \<le> start'; monotonic_key_ranges (((start', end'), v') # kvs); \<And>start start'a end'a ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ((start', end') # map fst kvs) = (start'a, end'a) # ks_tl'; start = start'; (start', end') # map fst kvs = (start', end') # map fst kvs\<rbrakk> \<Longrightarrow> start' = start'a \<and> end' \<le> end'a\<rbrakk> \<Longrightarrow> start = start'a \<and> end \<le> end'a
 2. \<And>start end uv_ ks starta enda start' end' ks_tl ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ks = (start', end') # ks_tl'; monotonic_key_ranges [((start, end), uv_)]; ks = map fst [((start, end), uv_)]; ks = (starta, enda) # ks_tl\<rbrakk> \<Longrightarrow> starta = start' \<and> enda \<le> end'
 3. \<And>ks start end start' end' ks_tl ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ks = (start', end') # ks_tl'; monotonic_key_ranges []; ks = map fst []; ks = (start, end) # ks_tl\<rbrakk> \<Longrightarrow> start = start' \<and> end \<le> end' proof (prove)
goal (3 subgoals):
 1. \<And>start end start' end' v' kvs start'a end'a ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ((start, end) # (start', end') # map fst kvs) = (start'a, end'a) # ks_tl'; start \<le> end; end \<le> start'; monotonic_key_ranges (((start', end'), v') # kvs); \<And>start'a end'a ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ((start', end') # map fst kvs) = (start'a, end'a) # ks_tl'; start' = start'; (start', end') # map fst kvs = (start', end') # map fst kvs\<rbrakk> \<Longrightarrow> start' = start'a \<and> end' \<le> end'a\<rbrakk> \<Longrightarrow> start = start'a \<and> end \<le> end'a
 2. \<And>start end uv_ ks starta enda start' end' ks_tl ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ks = (start', end') # ks_tl'; monotonic_key_ranges [((start, end), uv_)]; ks = map fst [((start, end), uv_)]; ks = (starta, enda) # ks_tl\<rbrakk> \<Longrightarrow> starta = start' \<and> enda \<le> end'
 3. \<And>ks start end start' end' ks_tl ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ks = (start', end') # ks_tl'; monotonic_key_ranges []; ks = map fst []; ks = (start, end) # ks_tl\<rbrakk> \<Longrightarrow> start = start' \<and> end \<le> end' proof (prove)
goal (3 subgoals):
 1. \<And>start end start' end' v' kvs start'a end'a ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ((start, end) # (start', end') # map fst kvs) = (start'a, end'a) # ks_tl'; start \<le> end; end \<le> start'; monotonic_key_ranges (((start', end'), v') # kvs); \<And>start'a end'a ks_tl'. combine_contiguous_ranges_rev ((start', end') # map fst kvs) = (start'a, end'a) # ks_tl' \<Longrightarrow> start' = start'a \<and> end' \<le> end'a\<rbrakk> \<Longrightarrow> start = start'a \<and> end \<le> end'a
 2. \<And>start end uv_ ks starta enda start' end' ks_tl ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ks = (start', end') # ks_tl'; monotonic_key_ranges [((start, end), uv_)]; ks = map fst [((start, end), uv_)]; ks = (starta, enda) # ks_tl\<rbrakk> \<Longrightarrow> starta = start' \<and> enda \<le> end'
 3. \<And>ks start end start' end' ks_tl ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ks = (start', end') # ks_tl'; monotonic_key_ranges []; ks = map fst []; ks = (start, end) # ks_tl\<rbrakk> \<Longrightarrow> start = start' \<and> end \<le> end' proof (prove)
goal (3 subgoals):
 1. \<And>start end start' end' v' kvs start'a end'a ks_tl'. \<lbrakk>(case combine_contiguous_ranges_rev ((start', end') # map fst kvs) of [] \<Rightarrow> [(start, end)] | (start', end') # xs' \<Rightarrow> if end = start' then (start, end') # xs' else (start, end) # (start', end') # xs') = (start'a, end'a) # ks_tl'; start \<le> end; end \<le> start'; monotonic_key_ranges (((start', end'), v') # kvs); \<And>start'a end'a ks_tl'. combine_contiguous_ranges_rev ((start', end') # map fst kvs) = (start'a, end'a) # ks_tl' \<Longrightarrow> start' = start'a \<and> end' \<le> end'a\<rbrakk> \<Longrightarrow> start = start'a \<and> end \<le> end'a
 2. \<And>start end uv_ ks starta enda start' end' ks_tl ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ks = (start', end') # ks_tl'; monotonic_key_ranges [((start, end), uv_)]; ks = map fst [((start, end), uv_)]; ks = (starta, enda) # ks_tl\<rbrakk> \<Longrightarrow> starta = start' \<and> enda \<le> end'
 3. \<And>ks start end start' end' ks_tl ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ks = (start', end') # ks_tl'; monotonic_key_ranges []; ks = map fst []; ks = (start, end) # ks_tl\<rbrakk> \<Longrightarrow> start = start' \<and> end \<le> end' proof (prove)
goal (2 subgoals):
 1. \<And>start end uv_ ks starta enda start' end' ks_tl ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ks = (start', end') # ks_tl'; monotonic_key_ranges [((start, end), uv_)]; ks = map fst [((start, end), uv_)]; ks = (starta, enda) # ks_tl\<rbrakk> \<Longrightarrow> starta = start' \<and> enda \<le> end'
 2. \<And>ks start end start' end' ks_tl ks_tl'. \<lbrakk>combine_contiguous_ranges_rev ks = (start', end') # ks_tl'; monotonic_key_ranges []; ks = map fst []; ks = (start, end) # ks_tl\<rbrakk> \<Longrightarrow> start = start' \<and> end \<le> end'