theory RangeMap

lemma ran_range_map_of:
  "\<lbrakk> monotonic_key_ranges xs \<rbrakk> \<Longrightarrow>
   ran (range_map_of xs) = set (filter (\<lambda>((start, end), v). start < end) xs)" apply (induct xs) apply (fastforce simp: range_map_of_def) apply (clarsimp simp: range_map_of_def monotonic_key_ranges_alt_def list_all_iff) apply (subst ran_add_if) apply (subst not_in_domIff[where f="lookup_map_of _ _"]) apply (subst dom_range_map_of[unfolded range_map_of_def]) apply (fastforce simp: disjnt_def in_range.simps) apply (clarsimp simp: ran_def restrict_map_def in_range.simps) apply (drule sym) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monotonic_key_ranges xs \<Longrightarrow> ran (range_map_of xs) = set (filter (\<lambda>((start, end), v). start < end) xs) proof (prove)
goal (2 subgoals):
 1. monotonic_key_ranges [] \<Longrightarrow> ran (range_map_of []) = set (filter (\<lambda>((start, end), v). start < end) [])
 2. \<And>a xs. \<lbrakk>monotonic_key_ranges xs \<Longrightarrow> ran (range_map_of xs) = set (filter (\<lambda>((start, end), v). start < end) xs); monotonic_key_ranges (a # xs)\<rbrakk> \<Longrightarrow> ran (range_map_of (a # xs)) = set (filter (\<lambda>((start, end), v). start < end) (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>monotonic_key_ranges xs \<Longrightarrow> ran (range_map_of xs) = set (filter (\<lambda>((start, end), v). start < end) xs); monotonic_key_ranges (a # xs)\<rbrakk> \<Longrightarrow> ran (range_map_of (a # xs)) = set (filter (\<lambda>((start, end), v). start < end) (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba xs. \<lbrakk>ran (lookup_map_of in_range xs) = {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}; a \<le> b; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>_. start \<le> end) xa; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start', end') \<Rightarrow> \<lambda>_. b \<le> start') xa; list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') xs\<rbrakk> \<Longrightarrow> (a < b \<longrightarrow> ran (\<lambda>x. if in_range (a, b) x then Some ((a, b), ba) else lookup_map_of in_range xs x) = insert ((a, b), ba) {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}) \<and> (a = b \<longrightarrow> ran (\<lambda>x. if in_range (b, b) x then Some ((b, b), ba) else lookup_map_of in_range xs x) = {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba xs. \<lbrakk>ran (lookup_map_of in_range xs) = {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}; a \<le> b; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>_. start \<le> end) xa; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start', end') \<Rightarrow> \<lambda>_. b \<le> start') xa; list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') xs\<rbrakk> \<Longrightarrow> \<forall>x. in_range (a, b) x \<longrightarrow> lookup_map_of in_range xs x = None
 2. \<And>a b ba xs. \<lbrakk>ran (lookup_map_of in_range xs) = {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}; a \<le> b; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>_. start \<le> end) xa; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start', end') \<Rightarrow> \<lambda>_. b \<le> start') xa; list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') xs\<rbrakk> \<Longrightarrow> (a < b \<longrightarrow> ran ((\<lambda>x. Some ((a, b), ba)) |` Collect (in_range (a, b))) \<union> ran (lookup_map_of in_range xs) = insert ((a, b), ba) {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}) \<and> (a = b \<longrightarrow> ran (\<lambda>x. if in_range (b, b) x then Some ((b, b), ba) else lookup_map_of in_range xs x) = {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba xs. \<lbrakk>ran (lookup_map_of in_range xs) = {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}; a \<le> b; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>_. start \<le> end) xa; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start', end') \<Rightarrow> \<lambda>_. b \<le> start') xa; list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') xs\<rbrakk> \<Longrightarrow> \<forall>x. in_range (a, b) x \<longrightarrow> x \<notin> dom (lookup_map_of in_range xs)
 2. \<And>a b ba xs. \<lbrakk>ran (lookup_map_of in_range xs) = {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}; a \<le> b; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>_. start \<le> end) xa; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start', end') \<Rightarrow> \<lambda>_. b \<le> start') xa; list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') xs\<rbrakk> \<Longrightarrow> (a < b \<longrightarrow> ran ((\<lambda>x. Some ((a, b), ba)) |` Collect (in_range (a, b))) \<union> ran (lookup_map_of in_range xs) = insert ((a, b), ba) {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}) \<and> (a = b \<longrightarrow> ran (\<lambda>x. if in_range (b, b) x then Some ((b, b), ba) else lookup_map_of in_range xs x) = {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba xs. \<lbrakk>ran (lookup_map_of in_range xs) = {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}; a \<le> b; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>_. start \<le> end) xa; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start', end') \<Rightarrow> \<lambda>_. b \<le> start') xa; list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') xs\<rbrakk> \<Longrightarrow> \<forall>x. in_range (a, b) x \<longrightarrow> x \<notin> \<Union> (set (map (Collect \<circ> in_range \<circ> fst) xs))
 2. \<And>a b ba xs. \<lbrakk>ran (lookup_map_of in_range xs) = {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}; a \<le> b; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>_. start \<le> end) xa; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start', end') \<Rightarrow> \<lambda>_. b \<le> start') xa; list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') xs\<rbrakk> \<Longrightarrow> (a < b \<longrightarrow> ran ((\<lambda>x. Some ((a, b), ba)) |` Collect (in_range (a, b))) \<union> ran (lookup_map_of in_range xs) = insert ((a, b), ba) {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}) \<and> (a = b \<longrightarrow> ran (\<lambda>x. if in_range (b, b) x then Some ((b, b), ba) else lookup_map_of in_range xs x) = {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba xs. \<lbrakk>ran (lookup_map_of in_range xs) = {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}; a \<le> b; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>_. start \<le> end) xa; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start', end') \<Rightarrow> \<lambda>_. b \<le> start') xa; list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') xs\<rbrakk> \<Longrightarrow> (a < b \<longrightarrow> ran ((\<lambda>x. Some ((a, b), ba)) |` Collect (in_range (a, b))) \<union> ran (lookup_map_of in_range xs) = insert ((a, b), ba) {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}) \<and> (a = b \<longrightarrow> ran (\<lambda>x. if in_range (b, b) x then Some ((b, b), ba) else lookup_map_of in_range xs x) = {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba xs. \<lbrakk>{b. \<exists>a. lookup_map_of in_range xs a = Some b} = {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}; a \<le> b; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>_. start \<le> end) xa; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start', end') \<Rightarrow> \<lambda>_. b \<le> start') xa; list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') xs\<rbrakk> \<Longrightarrow> (a < b \<longrightarrow> {bb. \<exists>aa. (a \<le> aa \<and> aa < b \<longrightarrow> ((a, b), ba) = bb) \<and> a \<le> aa \<and> aa < b} \<union> {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa} = insert ((a, b), ba) {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}) \<and> (a = b \<longrightarrow> {bb. \<exists>a. (b \<le> a \<and> a < b \<longrightarrow> ((b, b), ba) = bb) \<and> ((b \<le> a \<longrightarrow> \<not> a < b) \<longrightarrow> lookup_map_of in_range xs a = Some bb)} = {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba xs. \<lbrakk>a \<le> b; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>_. start \<le> end) xa; \<forall>x\<in>set xs. case x of (x, xa) \<Rightarrow> (case x of (start', end') \<Rightarrow> \<lambda>_. b \<le> start') xa; list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') xs; {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa} = {b. \<exists>a. lookup_map_of in_range xs a = Some b}\<rbrakk> \<Longrightarrow> (a < b \<longrightarrow> {bb. \<exists>aa. (a \<le> aa \<and> aa < b \<longrightarrow> ((a, b), ba) = bb) \<and> a \<le> aa \<and> aa < b} \<union> {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa} = insert ((a, b), ba) {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa}) \<and> (a = b \<longrightarrow> {bb. \<exists>a. (b \<le> a \<and> a < b \<longrightarrow> ((b, b), ba) = bb) \<and> ((b \<le> a \<longrightarrow> \<not> a < b) \<longrightarrow> lookup_map_of in_range xs a = Some bb)} = {x \<in> set xs. case x of (x, xa) \<Rightarrow> (case x of (start, end) \<Rightarrow> \<lambda>v. start < end) xa})