theory RangeMap

theorem lookup_range_tree_to_list_of:
  fixes tree :: "('a::linorder, 'b) RangeTree"
  shows "fst (lookup_range_tree_valid tree) \<Longrightarrow>
         lookup_range_tree tree = range_map_of (lookup_range_tree_to_list tree)" unfolding range_map_of_def proof (induct tree) case Leaf show ?case by (fastforce simp: range_map_of_def) next case (Node start "end" v treeL treeR) have valid_children:
      "fst (lookup_range_tree_valid treeL)"
      "fst (lookup_range_tree_valid treeR)" using Node.prems fst_lookup_range_tree_validD by auto have eq_children:
      "lookup_range_tree treeL = lookup_map_of in_range (lookup_range_tree_to_list treeL)"
      "lookup_range_tree treeR = lookup_map_of in_range (lookup_range_tree_to_list treeR)" using Node.hyps valid_children by auto have treeL1_disjoint:
      "lookup_map_disjoint_keys in_range (lookup_range_tree_to_list treeL @ [((start, end), v)])" using Node.prems by (fastforce dest!: lookup_range_tree_list_monotonic monotonic_key_ranges_disjoint
                    simp: disjoint_key_ranges_def lookup_map_disjoint_keys_def list_pairwise_append) { fix x :: 'a have lookup_list_reorder:
        "lookup_map_of in_range (lookup_range_tree_to_list (Node start end v treeL treeR)) x
         = lookup_map_of in_range
                         ([((start, end), v)]
                           @ lookup_range_tree_to_list treeL
                           @ lookup_range_tree_to_list treeR) x" using lookup_range_tree_to_list.simps(2) append_assoc
              lookup_map_of_append_commute[OF treeL1_disjoint]
              lookup_map_of_append_cong[OF _ refl] by metis have branch_eq_lookup_append[symmetric]:
        "lookup_map_of in_range (lookup_range_tree_to_list treeL @ lookup_range_tree_to_list treeR) x
         = (if x < start then lookup_map_of in_range (lookup_range_tree_to_list treeL) x
                         else lookup_map_of in_range (lookup_range_tree_to_list treeR) x)" apply (simp only: lookup_map_of_append_to_map_add flip: eq_children) apply (rule map_add_alt_cond'[THEN fun_cong]) using Node.prems apply (fastforce dest: lookup_range_tree_Some split: prod.splits)+ done have case_ext:
        "lookup_range_tree (Node start end v treeL treeR) x
         = lookup_map_of in_range (lookup_range_tree_to_list (Node start end v treeL treeR)) x" apply (simp only: lookup_range_tree.simps
                          lookup_list_reorder eq_children branch_eq_lookup_append
                    flip: in_range.simps) by (simp only: lookup_map_of.simps append.simps) } then show ?case by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (lookup_range_tree_valid tree) \<Longrightarrow> lookup_range_tree tree = range_map_of (lookup_range_tree_to_list tree) proof (prove)
goal (1 subgoal):
 1. fst (lookup_range_tree_valid tree) \<Longrightarrow> lookup_range_tree tree = lookup_map_of in_range (lookup_range_tree_to_list tree) proof (state)
goal (2 subgoals):
 1. fst (lookup_range_tree_valid Leaf) \<Longrightarrow> lookup_range_tree Leaf = lookup_map_of in_range (lookup_range_tree_to_list Leaf)
 2. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>fst (lookup_range_tree_valid tree1) \<Longrightarrow> lookup_range_tree tree1 = lookup_map_of in_range (lookup_range_tree_to_list tree1); fst (lookup_range_tree_valid tree2) \<Longrightarrow> lookup_range_tree tree2 = lookup_map_of in_range (lookup_range_tree_to_list tree2); fst (lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2))\<rbrakk> \<Longrightarrow> lookup_range_tree (Node x1 x2 x3 tree1 tree2) = lookup_map_of in_range (lookup_range_tree_to_list (Node x1 x2 x3 tree1 tree2)) proof (state)
this:
fst (lookup_range_tree_valid Leaf)

goal (2 subgoals):
 1. fst (lookup_range_tree_valid Leaf) \<Longrightarrow> lookup_range_tree Leaf = lookup_map_of in_range (lookup_range_tree_to_list Leaf)
 2. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>fst (lookup_range_tree_valid tree1) \<Longrightarrow> lookup_range_tree tree1 = lookup_map_of in_range (lookup_range_tree_to_list tree1); fst (lookup_range_tree_valid tree2) \<Longrightarrow> lookup_range_tree tree2 = lookup_map_of in_range (lookup_range_tree_to_list tree2); fst (lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2))\<rbrakk> \<Longrightarrow> lookup_range_tree (Node x1 x2 x3 tree1 tree2) = lookup_map_of in_range (lookup_range_tree_to_list (Node x1 x2 x3 tree1 tree2)) proof (prove)
goal (1 subgoal):
 1. lookup_range_tree Leaf = lookup_map_of in_range (lookup_range_tree_to_list Leaf) proof (state)
this:
lookup_range_tree Leaf = lookup_map_of in_range (lookup_range_tree_to_list Leaf)

goal (1 subgoal):
 1. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>fst (lookup_range_tree_valid tree1) \<Longrightarrow> lookup_range_tree tree1 = lookup_map_of in_range (lookup_range_tree_to_list tree1); fst (lookup_range_tree_valid tree2) \<Longrightarrow> lookup_range_tree tree2 = lookup_map_of in_range (lookup_range_tree_to_list tree2); fst (lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2))\<rbrakk> \<Longrightarrow> lookup_range_tree (Node x1 x2 x3 tree1 tree2) = lookup_map_of in_range (lookup_range_tree_to_list (Node x1 x2 x3 tree1 tree2)) proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>fst (lookup_range_tree_valid tree1) \<Longrightarrow> lookup_range_tree tree1 = lookup_map_of in_range (lookup_range_tree_to_list tree1); fst (lookup_range_tree_valid tree2) \<Longrightarrow> lookup_range_tree tree2 = lookup_map_of in_range (lookup_range_tree_to_list tree2); fst (lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2))\<rbrakk> \<Longrightarrow> lookup_range_tree (Node x1 x2 x3 tree1 tree2) = lookup_map_of in_range (lookup_range_tree_to_list (Node x1 x2 x3 tree1 tree2)) proof (state)
this:
fst (lookup_range_tree_valid treeL) \<Longrightarrow> lookup_range_tree treeL = lookup_map_of in_range (lookup_range_tree_to_list treeL)
fst (lookup_range_tree_valid treeR) \<Longrightarrow> lookup_range_tree treeR = lookup_map_of in_range (lookup_range_tree_to_list treeR)
fst (lookup_range_tree_valid (Node start end v treeL treeR))

goal (1 subgoal):
 1. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>fst (lookup_range_tree_valid tree1) \<Longrightarrow> lookup_range_tree tree1 = lookup_map_of in_range (lookup_range_tree_to_list tree1); fst (lookup_range_tree_valid tree2) \<Longrightarrow> lookup_range_tree tree2 = lookup_map_of in_range (lookup_range_tree_to_list tree2); fst (lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2))\<rbrakk> \<Longrightarrow> lookup_range_tree (Node x1 x2 x3 tree1 tree2) = lookup_map_of in_range (lookup_range_tree_to_list (Node x1 x2 x3 tree1 tree2)) proof (prove)
goal (1 subgoal):
 1. fst (lookup_range_tree_valid treeL) &&& fst (lookup_range_tree_valid treeR) proof (prove)
using this:
fst (lookup_range_tree_valid (Node start end v treeL treeR))
fst (lookup_range_tree_valid (Node ?start ?end ?v ?l ?r)) \<Longrightarrow> fst (lookup_range_tree_valid ?l) \<and> fst (lookup_range_tree_valid ?r)

goal (1 subgoal):
 1. fst (lookup_range_tree_valid treeL) &&& fst (lookup_range_tree_valid treeR) proof (state)
this:
fst (lookup_range_tree_valid treeL)
fst (lookup_range_tree_valid treeR)

goal (1 subgoal):
 1. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>fst (lookup_range_tree_valid tree1) \<Longrightarrow> lookup_range_tree tree1 = lookup_map_of in_range (lookup_range_tree_to_list tree1); fst (lookup_range_tree_valid tree2) \<Longrightarrow> lookup_range_tree tree2 = lookup_map_of in_range (lookup_range_tree_to_list tree2); fst (lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2))\<rbrakk> \<Longrightarrow> lookup_range_tree (Node x1 x2 x3 tree1 tree2) = lookup_map_of in_range (lookup_range_tree_to_list (Node x1 x2 x3 tree1 tree2)) proof (prove)
goal (1 subgoal):
 1. lookup_range_tree treeL = lookup_map_of in_range (lookup_range_tree_to_list treeL) &&& lookup_range_tree treeR = lookup_map_of in_range (lookup_range_tree_to_list treeR) proof (prove)
using this:
fst (lookup_range_tree_valid treeL) \<Longrightarrow> lookup_range_tree treeL = lookup_map_of in_range (lookup_range_tree_to_list treeL)
fst (lookup_range_tree_valid treeR) \<Longrightarrow> lookup_range_tree treeR = lookup_map_of in_range (lookup_range_tree_to_list treeR)
fst (lookup_range_tree_valid treeL)
fst (lookup_range_tree_valid treeR)

goal (1 subgoal):
 1. lookup_range_tree treeL = lookup_map_of in_range (lookup_range_tree_to_list treeL) &&& lookup_range_tree treeR = lookup_map_of in_range (lookup_range_tree_to_list treeR) proof (state)
this:
lookup_range_tree treeL = lookup_map_of in_range (lookup_range_tree_to_list treeL)
lookup_range_tree treeR = lookup_map_of in_range (lookup_range_tree_to_list treeR)

goal (1 subgoal):
 1. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>fst (lookup_range_tree_valid tree1) \<Longrightarrow> lookup_range_tree tree1 = lookup_map_of in_range (lookup_range_tree_to_list tree1); fst (lookup_range_tree_valid tree2) \<Longrightarrow> lookup_range_tree tree2 = lookup_map_of in_range (lookup_range_tree_to_list tree2); fst (lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2))\<rbrakk> \<Longrightarrow> lookup_range_tree (Node x1 x2 x3 tree1 tree2) = lookup_map_of in_range (lookup_range_tree_to_list (Node x1 x2 x3 tree1 tree2)) proof (prove)
goal (1 subgoal):
 1. lookup_map_disjoint_keys in_range (lookup_range_tree_to_list treeL @ [((start, end), v)]) proof (prove)
using this:
fst (lookup_range_tree_valid (Node start end v treeL treeR))

goal (1 subgoal):
 1. lookup_map_disjoint_keys in_range (lookup_range_tree_to_list treeL @ [((start, end), v)]) proof (state)
this:
lookup_map_disjoint_keys in_range (lookup_range_tree_to_list treeL @ [((start, end), v)])

goal (1 subgoal):
 1. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>fst (lookup_range_tree_valid tree1) \<Longrightarrow> lookup_range_tree tree1 = lookup_map_of in_range (lookup_range_tree_to_list tree1); fst (lookup_range_tree_valid tree2) \<Longrightarrow> lookup_range_tree tree2 = lookup_map_of in_range (lookup_range_tree_to_list tree2); fst (lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2))\<rbrakk> \<Longrightarrow> lookup_range_tree (Node x1 x2 x3 tree1 tree2) = lookup_map_of in_range (lookup_range_tree_to_list (Node x1 x2 x3 tree1 tree2)) proof (state)
this:
lookup_map_disjoint_keys in_range (lookup_range_tree_to_list treeL @ [((start, end), v)])

goal (1 subgoal):
 1. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>fst (lookup_range_tree_valid tree1) \<Longrightarrow> lookup_range_tree tree1 = lookup_map_of in_range (lookup_range_tree_to_list tree1); fst (lookup_range_tree_valid tree2) \<Longrightarrow> lookup_range_tree tree2 = lookup_map_of in_range (lookup_range_tree_to_list tree2); fst (lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2))\<rbrakk> \<Longrightarrow> lookup_range_tree (Node x1 x2 x3 tree1 tree2) = lookup_map_of in_range (lookup_range_tree_to_list (Node x1 x2 x3 tree1 tree2)) proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>fst (lookup_range_tree_valid tree1) \<Longrightarrow> lookup_range_tree tree1 = lookup_map_of in_range (lookup_range_tree_to_list tree1); fst (lookup_range_tree_valid tree2) \<Longrightarrow> lookup_range_tree tree2 = lookup_map_of in_range (lookup_range_tree_to_list tree2); fst (lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2))\<rbrakk> \<Longrightarrow> lookup_range_tree (Node x1 x2 x3 tree1 tree2) = lookup_map_of in_range (lookup_range_tree_to_list (Node x1 x2 x3 tree1 tree2)) proof (prove)
goal (1 subgoal):
 1. lookup_map_of in_range (lookup_range_tree_to_list (Node start end v treeL treeR)) x = lookup_map_of in_range ([((start, end), v)] @ lookup_range_tree_to_list treeL @ lookup_range_tree_to_list treeR) x proof (prove)
using this:
lookup_range_tree_to_list (Node ?start ?end ?v ?lt ?rt) = lookup_range_tree_to_list ?lt @ [((?start, ?end), ?v)] @ lookup_range_tree_to_list ?rt
(?xs @ ?ys) @ ?zs = ?xs @ ?ys @ ?zs
lookup_map_of in_range (lookup_range_tree_to_list treeL @ [((start, end), v)]) = lookup_map_of in_range ([((start, end), v)] @ lookup_range_tree_to_list treeL)
lookup_map_of ?eq ?xs = lookup_map_of ?eq ?xs' \<Longrightarrow> lookup_map_of ?eq (?xs @ ?ys) = lookup_map_of ?eq (?xs' @ ?ys)

goal (1 subgoal):
 1. lookup_map_of in_range (lookup_range_tree_to_list (Node start end v treeL treeR)) x = lookup_map_of in_range ([((start, end), v)] @ lookup_range_tree_to_list treeL @ lookup_range_tree_to_list treeR) x proof (state)
this:
lookup_map_of in_range (lookup_range_tree_to_list (Node start end v treeL treeR)) x = lookup_map_of in_range ([((start, end), v)] @ lookup_range_tree_to_list treeL @ lookup_range_tree_to_list treeR) x

goal (1 subgoal):
 1. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>fst (lookup_range_tree_valid tree1) \<Longrightarrow> lookup_range_tree tree1 = lookup_map_of in_range (lookup_range_tree_to_list tree1); fst (lookup_range_tree_valid tree2) \<Longrightarrow> lookup_range_tree tree2 = lookup_map_of in_range (lookup_range_tree_to_list tree2); fst (lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2))\<rbrakk> \<Longrightarrow> lookup_range_tree (Node x1 x2 x3 tree1 tree2) = lookup_map_of in_range (lookup_range_tree_to_list (Node x1 x2 x3 tree1 tree2)) proof (prove)
goal (1 subgoal):
 1. lookup_map_of in_range (lookup_range_tree_to_list treeL @ lookup_range_tree_to_list treeR) x = (if x < start then lookup_map_of in_range (lookup_range_tree_to_list treeL) x else lookup_map_of in_range (lookup_range_tree_to_list treeR) x) proof (prove)
goal (1 subgoal):
 1. (lookup_range_tree treeR ++ lookup_range_tree treeL) x = (if x < start then lookup_range_tree treeL x else lookup_range_tree treeR x) proof (prove)
goal (2 subgoals):
 1. \<And>x. lookup_range_tree treeR x \<noteq> None \<Longrightarrow> \<not> x < start
 2. \<And>x. lookup_range_tree treeL x \<noteq> None \<Longrightarrow> x < start proof (prove)
using this:
fst (lookup_range_tree_valid (Node start end v treeL treeR))

goal (2 subgoals):
 1. \<And>x. lookup_range_tree treeR x \<noteq> None \<Longrightarrow> \<not> x < start
 2. \<And>x. lookup_range_tree treeL x \<noteq> None \<Longrightarrow> x < start proof (prove)
goal:
No subgoals! proof (state)
this:
(if x < start then lookup_map_of in_range (lookup_range_tree_to_list treeL) x else lookup_map_of in_range (lookup_range_tree_to_list treeR) x) = lookup_map_of in_range (lookup_range_tree_to_list treeL @ lookup_range_tree_to_list treeR) x

goal (1 subgoal):
 1. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>fst (lookup_range_tree_valid tree1) \<Longrightarrow> lookup_range_tree tree1 = lookup_map_of in_range (lookup_range_tree_to_list tree1); fst (lookup_range_tree_valid tree2) \<Longrightarrow> lookup_range_tree tree2 = lookup_map_of in_range (lookup_range_tree_to_list tree2); fst (lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2))\<rbrakk> \<Longrightarrow> lookup_range_tree (Node x1 x2 x3 tree1 tree2) = lookup_map_of in_range (lookup_range_tree_to_list (Node x1 x2 x3 tree1 tree2)) proof (prove)
goal (1 subgoal):
 1. lookup_range_tree (Node start end v treeL treeR) x = lookup_map_of in_range (lookup_range_tree_to_list (Node start end v treeL treeR)) x proof (prove)
goal (1 subgoal):
 1. (if in_range (start, end) x then Some ((start, end), v) else lookup_map_of in_range (lookup_range_tree_to_list treeL @ lookup_range_tree_to_list treeR) x) = lookup_map_of in_range ([((start, end), v)] @ lookup_range_tree_to_list treeL @ lookup_range_tree_to_list treeR) x proof (state)
this:
lookup_range_tree (Node start end v treeL treeR) x = lookup_map_of in_range (lookup_range_tree_to_list (Node start end v treeL treeR)) x

goal (1 subgoal):
 1. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>fst (lookup_range_tree_valid tree1) \<Longrightarrow> lookup_range_tree tree1 = lookup_map_of in_range (lookup_range_tree_to_list tree1); fst (lookup_range_tree_valid tree2) \<Longrightarrow> lookup_range_tree tree2 = lookup_map_of in_range (lookup_range_tree_to_list tree2); fst (lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2))\<rbrakk> \<Longrightarrow> lookup_range_tree (Node x1 x2 x3 tree1 tree2) = lookup_map_of in_range (lookup_range_tree_to_list (Node x1 x2 x3 tree1 tree2)) proof (state)
this:
lookup_range_tree (Node start end v treeL treeR) ?x2 = lookup_map_of in_range (lookup_range_tree_to_list (Node start end v treeL treeR)) ?x2

goal (1 subgoal):
 1. \<And>x1 x2 x3 tree1 tree2. \<lbrakk>fst (lookup_range_tree_valid tree1) \<Longrightarrow> lookup_range_tree tree1 = lookup_map_of in_range (lookup_range_tree_to_list tree1); fst (lookup_range_tree_valid tree2) \<Longrightarrow> lookup_range_tree tree2 = lookup_map_of in_range (lookup_range_tree_to_list tree2); fst (lookup_range_tree_valid (Node x1 x2 x3 tree1 tree2))\<rbrakk> \<Longrightarrow> lookup_range_tree (Node x1 x2 x3 tree1 tree2) = lookup_map_of in_range (lookup_range_tree_to_list (Node x1 x2 x3 tree1 tree2)) proof (chain)
picking this:
lookup_range_tree (Node start end v treeL treeR) ?x2 = lookup_map_of in_range (lookup_range_tree_to_list (Node start end v treeL treeR)) ?x2 proof (prove)
using this:
lookup_range_tree (Node start end v treeL treeR) ?x2 = lookup_map_of in_range (lookup_range_tree_to_list (Node start end v treeL treeR)) ?x2

goal (1 subgoal):
 1. lookup_range_tree (Node start end v treeL treeR) = lookup_map_of in_range (lookup_range_tree_to_list (Node start end v treeL treeR)) proof (state)
this:
lookup_range_tree (Node start end v treeL treeR) = lookup_map_of in_range (lookup_range_tree_to_list (Node start end v treeL treeR))

goal:
No subgoals!