theory RangeMap

lemma lookup_range_tree_list_monotonic:
  "fst (lookup_range_tree_valid tree) \<Longrightarrow>
   monotonic_key_ranges (lookup_range_tree_to_list tree)" apply (induct tree) apply simp apply (clarsimp simp: monotonic_key_ranges_alt_def list_pairwise_append
                  split: prod.splits option.splits) apply (fastforce dest: lookup_range_tree_valid_empty lookup_range_tree_to_list_range)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (lookup_range_tree_valid tree) \<Longrightarrow> monotonic_key_ranges (lookup_range_tree_to_list tree) proof (prove)
goal (2 subgoals):
 1. fst (lookup_range_tree_valid Leaf) \<Longrightarrow> monotonic_key_ranges (lookup_range_tree_to_list Leaf)
 2. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>fst (lookup_range_tree_valid tree1) \<Longrightarrow> monotonic_key_ranges (lookup_range_tree_to_list tree1); fst (lookup_range_tree_valid tree2) \<Longrightarrow> monotonic_key_ranges (lookup_range_tree_to_list tree2); fst (lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2))\<rbrakk> \<Longrightarrow> monotonic_key_ranges (lookup_range_tree_to_list (Node x1 x2 x3 tree1 tree2)) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>fst (lookup_range_tree_valid tree1) \<Longrightarrow> monotonic_key_ranges (lookup_range_tree_to_list tree1); fst (lookup_range_tree_valid tree2) \<Longrightarrow> monotonic_key_ranges (lookup_range_tree_to_list tree2); fst (lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2))\<rbrakk> \<Longrightarrow> monotonic_key_ranges (lookup_range_tree_to_list (Node x1 x2 x3 tree1 tree2)) proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2 tree1 tree2 x1a x1b. \<lbrakk>lookup_range_tree_valid tree1 = (True, None); lookup_range_tree_valid tree2 = (True, None); list_all (\<lambda>((start, end), uu_). start \<le> end) (lookup_range_tree_to_list tree1); list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') (lookup_range_tree_to_list tree1); list_all (\<lambda>((start, end), uu_). start \<le> end) (lookup_range_tree_to_list tree2); list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') (lookup_range_tree_to_list tree2); x1a; x1b; x1 \<le> x2\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (lookup_range_tree_to_list tree2). \<forall>a. (\<exists>b x2. x = ((a, b), x2)) \<longrightarrow> x2 \<le> a) \<and> (\<forall>x\<in>set (lookup_range_tree_to_list tree1). \<forall>a b. (\<exists>x2. x = ((a, b), x2)) \<longrightarrow> b \<le> x1 \<and> (\<forall>x\<in>set (lookup_range_tree_to_list tree2). \<forall>a. (\<exists>b x2. x = ((a, b), x2)) \<longrightarrow> b \<le> a))
 2. \<And>x1 x2 tree1 tree2 x1a x1b x1c x2d. \<lbrakk>list_all (\<lambda>((start, end), uu_). start \<le> end) (lookup_range_tree_to_list tree1); list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') (lookup_range_tree_to_list tree1); list_all (\<lambda>((start, end), uu_). start \<le> end) (lookup_range_tree_to_list tree2); list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') (lookup_range_tree_to_list tree2); lookup_range_tree_valid tree1 = (True, Some (x1c, x2d)); lookup_range_tree_valid tree2 = (True, None); x1a; x1b; x1 \<le> x2; x2d \<le> x1\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (lookup_range_tree_to_list tree2). \<forall>a. (\<exists>b x2. x = ((a, b), x2)) \<longrightarrow> x2 \<le> a) \<and> (\<forall>x\<in>set (lookup_range_tree_to_list tree1). \<forall>a b. (\<exists>x2. x = ((a, b), x2)) \<longrightarrow> b \<le> x1 \<and> (\<forall>x\<in>set (lookup_range_tree_to_list tree2). \<forall>a. (\<exists>b x2. x = ((a, b), x2)) \<longrightarrow> b \<le> a))
 3. \<And>x1 x2 tree1 tree2 x1a x1b x1c x2d. \<lbrakk>list_all (\<lambda>((start, end), uu_). start \<le> end) (lookup_range_tree_to_list tree1); list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') (lookup_range_tree_to_list tree1); list_all (\<lambda>((start, end), uu_). start \<le> end) (lookup_range_tree_to_list tree2); list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') (lookup_range_tree_to_list tree2); lookup_range_tree_valid tree1 = (True, None); lookup_range_tree_valid tree2 = (True, Some (x1c, x2d)); x1a; x1b; x1 \<le> x2; x2 \<le> x1c\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (lookup_range_tree_to_list tree2). \<forall>a. (\<exists>b x2. x = ((a, b), x2)) \<longrightarrow> x2 \<le> a) \<and> (\<forall>x\<in>set (lookup_range_tree_to_list tree1). \<forall>a b. (\<exists>x2. x = ((a, b), x2)) \<longrightarrow> b \<le> x1 \<and> (\<forall>x\<in>set (lookup_range_tree_to_list tree2). \<forall>a. (\<exists>b x2. x = ((a, b), x2)) \<longrightarrow> b \<le> a))
 4. \<And>x1 x2 tree1 tree2 x1a x1b x1c x2d x1d x2f. \<lbrakk>list_all (\<lambda>((start, end), uu_). start \<le> end) (lookup_range_tree_to_list tree1); list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') (lookup_range_tree_to_list tree1); list_all (\<lambda>((start, end), uu_). start \<le> end) (lookup_range_tree_to_list tree2); list_pairwise (\<lambda>((start, end), uu_) ((start', end'), uu_). end \<le> start') (lookup_range_tree_to_list tree2); lookup_range_tree_valid tree1 = (True, Some (x1d, x2f)); lookup_range_tree_valid tree2 = (True, Some (x1c, x2d)); x1a; x1b; x1 \<le> x2; x2f \<le> x1; x2 \<le> x1c\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (lookup_range_tree_to_list tree2). \<forall>a. (\<exists>b x2. x = ((a, b), x2)) \<longrightarrow> x2 \<le> a) \<and> (\<forall>x\<in>set (lookup_range_tree_to_list tree1). \<forall>a b. (\<exists>x2. x = ((a, b), x2)) \<longrightarrow> b \<le> x1 \<and> (\<forall>x\<in>set (lookup_range_tree_to_list tree2). \<forall>a. (\<exists>b x2. x = ((a, b), x2)) \<longrightarrow> b \<le> a)) proof (prove)
goal:
No subgoals!
flex-flex pairs:
\<lambda>:000 :001 :002 :003. ?v371 :000 :001 :002 :003 True True \<equiv>\<^sup>? \<lambda>:000 :001 :002 :003. ?v361 :000 :001 :002 :003 True True