1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory RangeMap
8imports
9  FastMap
10  FP_Eval
11  MkTermAntiquote
12begin
13
14text \<open>
15  Efficient rules and tactics for working with range maps.
16  A range map partitions the key space into sorted disjoint ranges.
17  This is useful for, e.g. representing program heaps, allowing one to quickly
18  look up which object covers any given address.
19
20  Features:
21    \<^item> Define a binary lookup tree for any lookup table (requires linorder keys)
22    \<^item> Conversion between lookup trees and lists
23    \<^item> Pre-computation of lookup results and domain/range sets
24
25  See RangeMap_Tests for examples.
26\<close>
27
28section \<open>Preliminaries: generalised lookup lists\<close>
29
30definition lookup_upd :: "('k \<Rightarrow> 'l \<Rightarrow> bool) \<Rightarrow> ('l \<Rightarrow> 'k \<times> 'v) \<Rightarrow> 'k \<Rightarrow> 'v \<Rightarrow> ('l \<Rightarrow> 'k \<times> 'v)"
31  where
32  "lookup_upd eq f k v \<equiv> \<lambda>x. if eq k x then (k, v) else f x"
33
34fun lookup_map_of :: "('k \<Rightarrow> 'l \<Rightarrow> bool) \<Rightarrow> ('k \<times> 'v) list \<Rightarrow> ('l \<Rightarrow> ('k \<times> 'v) option)"
35  where
36    "lookup_map_of eq [] = Map.empty"
37  | "lookup_map_of eq ((k, v)#kvs) = (\<lambda>x. if eq k x then Some (k, v) else lookup_map_of eq kvs x)"
38
39lemma map_of_to_lookup_map_of:
40  "map_of kvs = map_option snd o lookup_map_of (=) kvs"
41  by (induct kvs; auto)
42
43lemma lookup_map_of_Some:
44  "lookup_map_of eq kvs k = Some (k', v') \<Longrightarrow> (k', v') \<in> set kvs \<and> eq k' k"
45  by (induct kvs; fastforce split: if_splits)
46
47lemma lookup_map_of_None:
48  "lookup_map_of eq kvs k = None \<Longrightarrow> \<forall>(k', v') \<in> set kvs. \<not> eq k' k"
49  by (induct kvs; fastforce split: if_splits)
50
51
52subsection \<open>Distinct ordered pairs of list elements\<close>
53
54fun list_pairwise :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
55  where
56  "list_pairwise P [] = True"
57| "list_pairwise P (x#xs) = ((\<forall>y \<in> set xs. P x y) \<and> list_pairwise P xs)"
58
59lemma list_pairwise_as_indices:
60  "list_pairwise P xs = (\<forall>i j. i < j \<and> j < length xs \<longrightarrow> P (xs ! i) (xs ! j))"
61  apply (induct xs)
62   apply simp
63  apply (rule iffI)
64   apply clarsimp
65   apply (case_tac "i = 0")
66    apply simp
67   apply simp
68   apply (drule_tac x="i - 1" in spec, drule_tac x="j - 1" in spec)
69   apply simp
70   apply linarith
71  apply simp
72  apply (rule conjI)
73   apply clarsimp
74   apply (subst (asm) in_set_conv_nth, erule exE)
75   apply (rename_tac j)
76   apply (drule_tac x="0" in spec, drule_tac x="j + 1" in spec)
77   apply simp
78  apply clarsimp
79  apply (drule_tac x="i + 1" in spec, drule_tac x="j + 1" in spec)
80  apply simp
81  done
82
83lemma list_pairwise_snoc:
84  "list_pairwise P (xs @ [x]) = ((\<forall>y \<in> set xs. P y x) \<and> list_pairwise P xs)"
85  by (induct xs; auto)
86
87lemma list_pairwise_append:
88  "list_pairwise P (xs @ ys) =
89   (list_pairwise P xs \<and> list_pairwise P ys \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. P x y))"
90  by (induct xs; auto)
91
92lemma index_rev_rev_eq:
93  fixes i :: nat and n :: nat
94  shows "i < n \<Longrightarrow> n - (n - i - 1) - 1 = i"
95  by simp
96
97lemma list_pairwise_rev:
98  "list_pairwise P (rev xs) = list_pairwise (swp P) xs"
99  apply (simp add: list_pairwise_as_indices swp_def)
100  apply (case_tac "xs = []")
101   apply simp
102  apply (rule iffI)
103   apply (intro allI impI)
104   apply (drule_tac x="length xs - j - 1" in spec, drule_tac x="length xs - i - 1" in spec)
105   apply (clarsimp simp: rev_nth)
106  apply (clarsimp simp: rev_nth)
107  done
108
109lemma list_pairwise_imp:
110  "\<lbrakk> \<And>i j. \<lbrakk> i < j; P (xs ! i) (xs ! j) \<rbrakk> \<Longrightarrow> Q (xs ! i) (xs ! j) \<rbrakk> \<Longrightarrow>
111   list_pairwise P xs \<Longrightarrow> list_pairwise Q xs"
112  by (simp add: list_pairwise_as_indices)
113
114lemma list_pairwise_imp_weak:
115  "\<lbrakk> \<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs; P x y \<rbrakk> \<Longrightarrow> Q x y \<rbrakk> \<Longrightarrow>
116   list_pairwise P xs \<Longrightarrow> list_pairwise Q xs"
117  by (simp add: list_pairwise_as_indices)
118
119lemma list_pairwise_commute:
120  "symp P \<Longrightarrow> list_pairwise P (xs @ ys) = list_pairwise P (ys @ xs)"
121  by (fastforce simp: list_pairwise_append symp_def)
122
123
124subsection \<open>Predicate for disjoint keys\<close>
125
126definition lookup_map_disjoint_keys :: "('k \<Rightarrow> 'x \<Rightarrow> bool) \<Rightarrow> ('k \<times> 'v) list \<Rightarrow> bool"
127  where
128  "lookup_map_disjoint_keys eq =
129     list_pairwise (\<lambda>(k, _) (k', _). disjnt (Collect (eq k)) (Collect (eq k')))"
130
131lemma ran_lookup_map_of:
132  "ran (lookup_map_of eq []) = {}"
133  "ran (lookup_map_of eq ((k, v)#kvs)) =
134     (if Collect (eq k) \<noteq> {} then {(k, v)} else {})
135     \<union> ran (lookup_map_of eq kvs |` Collect (not (eq k)))"
136  by (auto simp: ran_def restrict_map_def pred_neg_def)
137
138lemma ran_lookup_map_of_disjoint:
139  "ran (lookup_map_of eq []) = {}"
140  "\<forall>(k', v') \<in> set kvs. \<forall>x. eq k x \<longrightarrow> \<not>eq k' x
141   \<Longrightarrow> ran (lookup_map_of eq ((k, v)#kvs)) =
142         (if Collect (eq k) \<noteq> {} then {(k, v)} else {})
143         \<union> ran (lookup_map_of eq kvs)"
144  apply simp
145
146  apply (subst ran_lookup_map_of)
147  apply (clarsimp simp: restrict_map_def pred_neg_def)
148  apply (rule arg_cong[where f="insert _"])
149  apply (force simp: ran_def dest: lookup_map_of_Some)
150  done
151
152
153locale RangeMap begin
154
155section \<open>Range maps as lookup lists\<close>
156
157text \<open>
158  Helper for proofs and some automation. This predicate is normally not
159  visible to end users.
160
161  Note that we use [start, end) ranges. This fits well with 0-based
162  memory addressing semantics, but such ranges cannot cover the
163  maximum key value (if there is one).
164\<close>
165fun in_range :: "('k::linorder \<times> 'k) \<Rightarrow> 'k \<Rightarrow> bool"
166  where
167  "in_range (start, end) k = (start \<le> k \<and> k < end)"
168
169declare in_range.simps[simp del]
170declare in_range.simps[THEN iffD1, dest]
171
172lemma Collect_in_range_atLeastLessThan[simp]:
173  "Collect (in_range r) = {fst r ..< snd r}"
174  by (cases r; fastforce simp: in_range.simps ord_class.atLeastLessThan_iff)
175
176definition "range_map_of \<equiv> lookup_map_of in_range"
177
178lemmas range_map_of_Some' =
179  lookup_map_of_Some[where eq=in_range, folded range_map_of_def]
180lemmas range_map_of_Some =
181  range_map_of_Some'[where k'="(start', end')" for start' end', simplified in_range.simps]
182
183lemma range_map_of_SomeD:
184  "range_map_of kvs k = Some ((start, end), v) \<Longrightarrow>
185   ((start, end), v) \<in> set kvs \<and> start \<le> k \<and> k < end"
186  by (fastforce simp: in_range.simps dest: range_map_of_Some')
187
188subsection \<open>Disjoint and monotonic key ranges\<close>
189
190definition disjoint_key_ranges :: "(('k::linorder \<times> 'k) \<times> 'v) list \<Rightarrow> bool"
191  where
192  "disjoint_key_ranges = lookup_map_disjoint_keys in_range"
193
194fun monotonic_key_ranges :: "(('k::linorder \<times> 'k) \<times> 'v) list \<Rightarrow> bool"
195  where
196    "monotonic_key_ranges (((start, end), _) # ((start', end'), v') # kvs) =
197       (start \<le> end \<and> end \<le> start' \<and> monotonic_key_ranges (((start', end'), v') # kvs))"
198  | "monotonic_key_ranges [((start, end), _)] = (start \<le> end)"
199  | "monotonic_key_ranges [] = True"
200
201lemma monotonic_key_ranges_alt_def:
202  "monotonic_key_ranges kvs =
203     (list_all (\<lambda>((start, end), _). start \<le> end) kvs
204      \<and> list_pairwise (\<lambda>((start, end), _) ((start', end'), _). end \<le> start') kvs)"
205  apply (induct kvs rule: monotonic_key_ranges.induct)
206    apply auto
207  done
208
209lemma monotonic_key_ranges_disjoint:
210  "monotonic_key_ranges kvs \<Longrightarrow> disjoint_key_ranges kvs"
211  apply (simp add: monotonic_key_ranges_alt_def
212                   disjoint_key_ranges_def lookup_map_disjoint_keys_def disjnt_def)
213  apply (induct kvs; fastforce)
214  done
215
216
217section \<open>Search trees for ranges\<close>
218
219text \<open>
220  Binary search tree. This is largely an implementation detail, so we
221  choose the structure to make automation easier (e.g. separate fields
222  for the keys and value).
223
224  We could reuse HOL.Tree instead, but the proofs would need changing.
225
226  NB: this is not the same as "range trees" in the data structures
227      literature, but just ordinary search trees.
228\<close>
229datatype ('k, 'v) RangeTree =
230    Leaf
231  | Node 'k 'k 'v "('k, 'v) RangeTree" "('k, 'v) RangeTree"
232
233primrec lookup_range_tree :: "('k::linorder, 'v) RangeTree \<Rightarrow> 'k \<Rightarrow> (('k \<times> 'k) \<times> 'v) option"
234  where
235    "lookup_range_tree Leaf x = None"
236  | "lookup_range_tree (Node start end v l r) x =
237       (if start \<le> x \<and> x < end then Some ((start, end), v)
238        else if x < start then lookup_range_tree l x
239        else lookup_range_tree r x)"
240
241text \<open>
242  Predicate for well-formed search trees.
243  This states that the ranges are disjoint and appear in ascending order,
244  and all ranges have correctly ordered key pairs.
245  It also returns the lowest and highest keys in the tree (or None for empty trees).
246\<close>
247primrec lookup_range_tree_valid ::
248        "('k::linorder, 'v) RangeTree \<Rightarrow> bool \<times> ('k \<times> 'k) option"
249  where
250    "lookup_range_tree_valid Leaf = (True, None)"
251  | "lookup_range_tree_valid (Node start end v lt rt) =
252       (let (lt_valid, lt_range) = lookup_range_tree_valid lt;
253            (rt_valid, rt_range) = lookup_range_tree_valid rt;
254            lt_low = (case lt_range of None \<Rightarrow> start | Some (low, high) \<Rightarrow> low);
255            rt_high = (case rt_range of None \<Rightarrow> end | Some (low, high) \<Rightarrow> high)
256        in (lt_valid \<and> rt_valid \<and> start \<le> end \<and>
257            (case lt_range of None \<Rightarrow> True | Some (low, high) \<Rightarrow> high \<le> start) \<and>
258            (case rt_range of None \<Rightarrow> True | Some (low, high) \<Rightarrow> end \<le> low),
259            Some (lt_low, rt_high)))"
260
261lemma lookup_range_tree_valid_empty:
262  "lookup_range_tree_valid tree = (True, None) \<Longrightarrow> tree = Leaf"
263  apply (induct tree)
264   apply simp
265  apply (fastforce split: prod.splits option.splits if_splits)
266  done
267
268lemma lookup_range_tree_valid_range:
269  "lookup_range_tree_valid tree = (True, Some (low, high)) \<Longrightarrow> low \<le> high"
270  apply (induct tree arbitrary: low high)
271   apply simp
272  apply (fastforce split: prod.splits option.splits if_splits)
273  done
274
275lemma lookup_range_tree_valid_in_range:
276  "lookup_range_tree_valid tree = (True, Some (low, high)) \<Longrightarrow>
277   lookup_range_tree tree k = Some ((start, end), v) \<Longrightarrow>
278   in_range (start, end) k \<and> low \<le> start \<and> end \<le> high"
279  apply (induct tree arbitrary: k v low high)
280   apply simp
281  apply (fastforce simp: in_range.simps
282                   split: prod.splits option.splits if_split_asm
283                   dest: lookup_range_tree_valid_empty lookup_range_tree_valid_range)
284  done
285
286lemma lookup_range_tree_valid_in_range_None:
287  "lookup_range_tree_valid tree = (True, Some (low, high)) \<Longrightarrow>
288   \<not> in_range (low, high) k \<Longrightarrow>
289   lookup_range_tree tree k = None"
290  apply (erule contrapos_np)
291  apply (fastforce simp: in_range.simps dest: lookup_range_tree_valid_in_range)
292  done
293
294text \<open>
295  Flatten a lookup tree into an assoc-list.
296  As long as the tree is well-formed, both forms are equivalent.
297\<close>
298primrec lookup_range_tree_to_list :: "('k, 'v) RangeTree \<Rightarrow> (('k \<times> 'k) \<times> 'v) list"
299  where
300    "lookup_range_tree_to_list Leaf = []"
301  | "lookup_range_tree_to_list (Node start end v lt rt) =
302        lookup_range_tree_to_list lt @ [((start, end), v)] @ lookup_range_tree_to_list rt"
303
304lemma lookup_range_tree_to_list_range:
305  "lookup_range_tree_valid tree = (True, Some (low, high)) \<Longrightarrow>
306   ((start, end), v) \<in> set (lookup_range_tree_to_list tree) \<Longrightarrow>
307   low \<le> start \<and> start \<le> end \<and> end \<le> high"
308  apply (induct tree arbitrary: start "end" v low high)
309   apply simp
310  apply (fastforce split: prod.splits option.splits if_split_asm
311                   dest: lookup_range_tree_valid_empty lookup_range_tree_valid_range)
312  done
313
314lemma monotonic_ranges_each_valid:
315  "monotonic_key_ranges xs \<Longrightarrow> ((start, end), v) \<in> set xs \<Longrightarrow> start \<le> end"
316  by (fastforce simp: monotonic_key_ranges_alt_def list_all_iff)
317
318lemma lookup_range_tree_list_monotonic:
319  "fst (lookup_range_tree_valid tree) \<Longrightarrow>
320   monotonic_key_ranges (lookup_range_tree_to_list tree)"
321  apply (induct tree)
322   apply simp
323  apply (clarsimp simp: monotonic_key_ranges_alt_def list_pairwise_append
324                  split: prod.splits option.splits)
325     apply (fastforce dest: lookup_range_tree_valid_empty lookup_range_tree_to_list_range)+
326  done
327
328lemma lookup_map_of_append_to_map_add:
329  "lookup_map_of eq (xs @ ys) = lookup_map_of eq ys ++ lookup_map_of eq xs"
330  unfolding map_add_def
331  apply (induct xs)
332   apply simp
333  apply (rule ext)
334  apply (clarsimp split: option.splits)
335  done
336
337lemma lookup_map_of_append_cong:
338  "\<lbrakk> lookup_map_of eq xs = lookup_map_of eq xs';
339     lookup_map_of eq ys = lookup_map_of eq ys'
340   \<rbrakk> \<Longrightarrow> lookup_map_of eq (xs @ ys) = lookup_map_of eq (xs' @ ys')"
341  by (simp add: lookup_map_of_append_to_map_add)
342
343lemma lookup_map_of_append1_commute:
344  "lookup_map_disjoint_keys eq (xs @ [y]) \<Longrightarrow>
345   lookup_map_of eq (xs @ [y]) = lookup_map_of eq ([y] @ xs)"
346  apply (induct xs arbitrary: y)
347   apply simp
348  apply (rule ext)
349  apply clarify
350  apply (simp add: disjnt_def lookup_map_disjoint_keys_def flip: Collect_conj_eq)
351  done
352
353lemma Cons_to_append:
354  "x # xs = [x] @ xs"
355  by simp
356
357lemma lookup_map_of_append_commute:
358  "lookup_map_disjoint_keys eq (xs @ ys) \<Longrightarrow>
359   lookup_map_of eq (xs @ ys) = lookup_map_of eq (ys @ xs)"
360  (* FIXME: cleanup... *)
361  apply (induct xs arbitrary: ys)
362   apply simp
363  apply (subst Cons_to_append, subst append_assoc)
364  apply (subst lookup_map_of_append1_commute[symmetric])
365   apply (simp only: lookup_map_disjoint_keys_def)
366   apply (subst list_pairwise_commute)
367    apply (fastforce intro: sympI disjnt_sym)
368   apply simp
369  apply (rule_tac t="lookup_map_of eq (ys @ a # xs)" and s="lookup_map_of eq ((ys @ [a]) @ xs)" in subst)
370   apply simp
371  apply (subst append_assoc, drule meta_spec, erule meta_mp)
372  apply simp
373  apply (subst (asm) Cons_to_append, subst append_assoc[symmetric])
374  apply (simp only: lookup_map_disjoint_keys_def)
375  apply (subst list_pairwise_commute)
376   apply (fastforce intro: sympI disjnt_sym)
377  apply simp
378  done
379
380lemma map_add_alt_cond:
381  "\<lbrakk>\<And>x. g x \<noteq> None \<Longrightarrow> \<not> cond x; \<And>x. f x \<noteq> None \<Longrightarrow> cond x\<rbrakk> \<Longrightarrow>
382   f ++ g = (\<lambda>x. if cond x then f x else g x)"
383  by (fastforce simp: map_add_def split: option.splits)
384
385lemma map_add_alt_cond':
386  "\<lbrakk>\<And>x. f x \<noteq> None \<Longrightarrow> \<not> cond x; \<And>x. g x \<noteq> None \<Longrightarrow> cond x\<rbrakk> \<Longrightarrow>
387   f ++ g = (\<lambda>x. if cond x then g x else f x)"
388  by (fastforce simp: map_add_def split: option.splits)
389
390
391lemma fst_lookup_range_tree_validD:
392  "fst (lookup_range_tree_valid (Node start end v l r)) \<Longrightarrow>
393   fst (lookup_range_tree_valid l) \<and> fst (lookup_range_tree_valid r)"
394  by (simp split: option.splits prod.splits)
395
396lemma lookup_range_tree_Some:
397  "lookup_range_tree tree k = Some ((start, end), v) \<Longrightarrow>
398   fst (lookup_range_tree_valid tree) \<Longrightarrow>
399   in_range (start, end) k
400   \<and> (\<exists>low high. lookup_range_tree_valid tree = (True, Some (low, high))
401                  \<and> low \<le> start \<and> end \<le> high)"
402  apply (cases "lookup_range_tree_valid tree")
403  apply clarsimp
404  apply (rename_tac r, case_tac r)
405   apply (fastforce dest: lookup_range_tree_valid_empty)
406  apply (fastforce dest: lookup_range_tree_valid_in_range)
407  done
408
409text \<open>Conversion between RangeTrees and lookup lists\<close>
410
411theorem lookup_range_tree_to_list_of:
412  fixes tree :: "('a::linorder, 'b) RangeTree"
413  shows "fst (lookup_range_tree_valid tree) \<Longrightarrow>
414         lookup_range_tree tree = range_map_of (lookup_range_tree_to_list tree)"
415unfolding range_map_of_def
416proof (induct tree)
417  case Leaf
418    show ?case
419      by (fastforce simp: range_map_of_def)
420  next case (Node start "end" v treeL treeR)
421    have valid_children:
422      "fst (lookup_range_tree_valid treeL)"
423      "fst (lookup_range_tree_valid treeR)"
424      using Node.prems fst_lookup_range_tree_validD by auto
425
426    have eq_children:
427      "lookup_range_tree treeL = lookup_map_of in_range (lookup_range_tree_to_list treeL)"
428      "lookup_range_tree treeR = lookup_map_of in_range (lookup_range_tree_to_list treeR)"
429      using Node.hyps valid_children by auto
430
431    have treeL1_disjoint:
432      "lookup_map_disjoint_keys in_range (lookup_range_tree_to_list treeL @ [((start, end), v)])"
433      using Node.prems
434      by (fastforce dest!: lookup_range_tree_list_monotonic monotonic_key_ranges_disjoint
435                    simp: disjoint_key_ranges_def lookup_map_disjoint_keys_def list_pairwise_append)
436
437    {
438      fix x :: 'a
439      have lookup_list_reorder:
440        "lookup_map_of in_range (lookup_range_tree_to_list (Node start end v treeL treeR)) x
441         = lookup_map_of in_range
442                         ([((start, end), v)]
443                           @ lookup_range_tree_to_list treeL
444                           @ lookup_range_tree_to_list treeR) x"
445        using lookup_range_tree_to_list.simps append_assoc
446              lookup_map_of_append_commute[OF treeL1_disjoint]
447              lookup_map_of_append_cong[OF _ refl]
448        by metis
449
450      have branch_eq_lookup_append[symmetric]:
451        "lookup_map_of in_range (lookup_range_tree_to_list treeL @ lookup_range_tree_to_list treeR) x
452         = (if x < start then lookup_map_of in_range (lookup_range_tree_to_list treeL) x
453                         else lookup_map_of in_range (lookup_range_tree_to_list treeR) x)"
454        apply (simp only: lookup_map_of_append_to_map_add flip: eq_children)
455        apply (rule map_add_alt_cond'[THEN fun_cong])
456         using Node.prems
457         apply (fastforce dest: lookup_range_tree_Some split: prod.splits)+
458        done
459
460      have case_ext:
461        "lookup_range_tree (Node start end v treeL treeR) x
462         = lookup_map_of in_range (lookup_range_tree_to_list (Node start end v treeL treeR)) x"
463        apply (simp only: lookup_range_tree.simps
464                          lookup_list_reorder eq_children branch_eq_lookup_append
465                    flip: in_range.simps)
466        by (simp only: lookup_map_of.simps append.simps)
467    }
468    then show ?case by auto
469qed
470
471(* Top-level rule for converting to lookup list. *)
472lemma lookup_range_tree_to_list_of_gen:
473  "\<lbrakk> fst (lookup_range_tree_valid tree);
474     lookup_range_tree_to_list tree = binds
475   \<rbrakk> \<Longrightarrow> lookup_range_tree tree = range_map_of binds
476         \<and> monotonic_key_ranges binds"
477  using lookup_range_tree_to_list_of
478  apply (fastforce dest: lookup_range_tree_list_monotonic)
479  done
480
481
482subsection \<open>Domain and range\<close>
483
484lemma dom_range_map_of:
485  "dom (range_map_of xs) =
486     Union (set (map (Collect o in_range o fst) xs))"
487  by (induct xs; fastforce simp: range_map_of_def in_range.simps)
488
489lemma Collect_in_range_rewrite:
490  "Collect o in_range o fst = (\<lambda>((start, end), v). {start ..< end})"
491  by (fastforce simp: in_range.simps)
492
493lemma ran_add_if:
494  "\<lbrakk> \<forall>x. P x \<longrightarrow> z x = None \<rbrakk>
495   \<Longrightarrow> ran (\<lambda>x. if P x then y x else z x) = ran (y |` Collect P) \<union> ran z"
496  by (auto simp: ran_def restrict_map_def)
497
498text \<open>
499  Key ranges are often contiguous. We can generate a more compact domain spec
500  that takes this into account. We define a function, combine_contiguous_ranges,
501  then evaluate it over the input keys.
502\<close>
503lemma atLeastLessThan_union_contiguous:
504  "\<lbrakk>(l::'a::linorder) \<le> m; m \<le> u\<rbrakk> \<Longrightarrow> {l..<m} \<union> {m..<u} = {l..<u}"
505  "\<lbrakk>(l::'a::linorder) \<le> m; m \<le> u\<rbrakk> \<Longrightarrow> ({l..<m} \<union> {m..<u}) \<union> x = {l..<u} \<union> x"
506  "\<lbrakk>(l::'a::linorder) \<le> m; m \<le> u\<rbrakk> \<Longrightarrow> {l..<m} \<union> ({m..<u} \<union> x) = {l..<u} \<union> x"
507  by (auto simp: ivl_disj_un)
508
509(* This is the one we want to evaluate *)
510fun combine_contiguous_ranges :: "('a::linorder \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list"
511  where
512    "combine_contiguous_ranges ((start, end) # (start', end') # xs) =
513       (if end = start' then combine_contiguous_ranges ((start, end') # xs) else
514          (start, end) # combine_contiguous_ranges ((start', end') # xs))"
515  | "combine_contiguous_ranges xs = xs"
516
517(* This one seems to be easier to verify *)
518fun combine_contiguous_ranges_rev :: "('a::linorder \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list"
519  where
520    "combine_contiguous_ranges_rev ((start, end) # xs) =
521       (case combine_contiguous_ranges_rev xs of
522            (start', end') # xs' \<Rightarrow> if end = start' then (start, end') # xs' else
523                                      (start, end) # (start', end') # xs'
524          | [] \<Rightarrow> [(start, end)])"
525  | "combine_contiguous_ranges_rev [] = []"
526
527lemma combine_contiguous_ranges_both:
528  "combine_contiguous_ranges xs = combine_contiguous_ranges_rev xs"
529  apply (induct xs rule: length_induct)
530  apply (case_tac xs)
531   apply clarsimp
532  apply (rename_tac xs')
533  apply (case_tac xs')
534   apply clarsimp
535  apply (clarsimp split: list.splits)
536  done
537
538lemma combine_contiguous_ranges_rev_head_helper:
539  "\<lbrakk> combine_contiguous_ranges_rev ks = ((start', end') # ks_tl');
540     monotonic_key_ranges kvs; ks = map fst kvs; ks = (start, end) # ks_tl
541   \<rbrakk> \<Longrightarrow>
542   start = start' \<and> end \<le> end'"
543  (* FIXME: cleanup *)
544  apply (induct kvs arbitrary: ks start "end" start' end' ks_tl ks_tl'
545                rule: monotonic_key_ranges.induct)
546    apply (clarsimp simp del: combine_contiguous_ranges_rev.simps)
547    apply (drule_tac x="(start', end') # map fst kvs" in meta_spec)
548    apply (drule_tac x="start'" in meta_spec)
549    apply (drule_tac x="end'" in meta_spec)
550    apply (clarsimp simp del: combine_contiguous_ranges_rev.simps)
551    apply (simp only: combine_contiguous_ranges_rev.simps(1)[where xs = "_#_"])
552    apply (fastforce dest: monotonic_ranges_each_valid split: list.splits if_splits)
553   apply auto
554  done
555
556lemma combine_contiguous_ranges_rev_correct:
557  "monotonic_key_ranges xs \<Longrightarrow>
558   Union (set (map (Collect o in_range o fst) xs))
559    = Union (set (map (Collect o in_range) (combine_contiguous_ranges_rev (map fst xs))))"
560  (* FIXME: cleanup *)
561  apply (induct xs rule: monotonic_key_ranges.induct)
562    subgoal
563      supply combine_contiguous_ranges_rev.simps[simp del]
564      apply (clarsimp simp: combine_contiguous_ranges_rev.simps(1)[where xs="_#_"]
565                      split: list.splits)
566      apply (drule(1) combine_contiguous_ranges_rev_head_helper)
567        apply simp
568       apply (rule refl)
569      apply (fastforce dest: atLeastLessThan_union_contiguous monotonic_ranges_each_valid)
570      done
571   apply auto
572  done
573
574lemmas combine_contiguous_ranges_correct =
575  combine_contiguous_ranges_rev_correct[folded combine_contiguous_ranges_both]
576
577text \<open>
578  @{const ran} is simpler. Every entry that can be a lookup result
579  (i.e. its key range is nonempty) is part of the range.
580\<close>
581
582lemma ran_range_map_of:
583  "\<lbrakk> monotonic_key_ranges xs \<rbrakk> \<Longrightarrow>
584   ran (range_map_of xs) = set (filter (\<lambda>((start, end), v). start < end) xs)"
585  apply (induct xs)
586   apply (fastforce simp: range_map_of_def)
587  apply (clarsimp simp: range_map_of_def monotonic_key_ranges_alt_def list_all_iff)
588  apply (subst ran_add_if)
589   apply (subst not_in_domIff[where f="lookup_map_of _ _"])
590   apply (subst dom_range_map_of[unfolded range_map_of_def])
591   apply (fastforce simp: disjnt_def in_range.simps)
592  apply (clarsimp simp: ran_def restrict_map_def in_range.simps)
593  apply (drule sym)
594  by auto
595
596
597subsection \<open>Generating lookup rules\<close>
598
599lemma lookup_map_of_single:
600  "\<lbrakk> lookup_map_disjoint_keys eq binds;
601     (k, v) \<in> set binds; eq k x \<rbrakk>
602   \<Longrightarrow> lookup_map_of eq binds x = Some (k, v)"
603  by (induct binds;
604      fastforce simp: lookup_map_disjoint_keys_def disjnt_def)
605
606lemma range_map_of_single':
607  "\<lbrakk> disjoint_key_ranges binds;
608     ((start, end), v) \<in> set binds; in_range (start, end) k \<rbrakk>
609   \<Longrightarrow> range_map_of binds k = Some ((start, end), v)"
610  unfolding range_map_of_def disjoint_key_ranges_def
611  by (fastforce intro: lookup_map_of_single)
612
613lemmas range_map_of_single = range_map_of_single'[unfolded in_range.simps, OF _ _ conjI]
614
615lemma range_map_of_lookups__gen_all':
616  "\<lbrakk> m = range_map_of binds; disjoint_key_ranges binds \<rbrakk> \<Longrightarrow>
617   list_all (\<lambda>((start, end), v). \<forall>k. in_range (start, end) k = (m k = Some ((start, end), v))) binds"
618  by (fastforce simp: list_all_iff intro: range_map_of_single' dest: range_map_of_Some')
619
620lemmas range_map_of_lookups__gen_all =
621  range_map_of_lookups__gen_all'
622    [OF _ monotonic_key_ranges_disjoint, simplified in_range.simps]
623
624text \<open>
625  We also generate equations for the useful special case of
626  looking up the start key of each range.
627\<close>
628
629lemma range_map_of_start:
630  "\<lbrakk> disjoint_key_ranges binds; ((start, end), v) \<in> set binds; start < end \<rbrakk>
631   \<Longrightarrow> range_map_of binds start = Some ((start, end), v)"
632  by (fastforce simp: in_range.simps intro: range_map_of_single)
633
634lemma range_map_of_start_lookups__gen_all':
635  "\<lbrakk> m = range_map_of binds; disjoint_key_ranges binds \<rbrakk> \<Longrightarrow>
636   list_all (\<lambda>((start, end), v). start < end \<longrightarrow> m start = Some ((start, end), v)) binds"
637  by (fastforce simp: list_all_iff intro: range_map_of_start)
638
639lemmas range_map_of_start_lookups__gen_all =
640  range_map_of_start_lookups__gen_all'[OF _ monotonic_key_ranges_disjoint]
641
642lemmas list_all_dest = FastMap.list_all_dest
643
644
645subsection \<open>Setup for automation\<close>
646
647definition quote :: "'a \<Rightarrow> 'a"
648  where unquote: "quote x \<equiv> x"
649lemma hold_quote:
650  "quote x = quote x" by simp
651
652text \<open>Like @{thm spec} without eta expansion\<close>
653lemma spec_FO:
654  "All P \<Longrightarrow> P x" by simp
655ML_val \<open>@{assert} (not (Thm.eq_thm_prop (@{thm spec}, @{thm spec_FO})))\<close>
656
657text \<open>
658  Install tree lookup simp rules that don't depend on
659  @{thm if_cong}/@{thm if_weak_cong} being set up correctly.
660\<close>
661lemma lookup_range_tree_simps':
662  "lookup_range_tree Leaf x = None"
663  "\<lbrakk> start \<le> x; x < end \<rbrakk> \<Longrightarrow>
664     lookup_range_tree (Node start end v l r) x = Some ((start, end), v)"
665  "\<lbrakk> x < start \<rbrakk> \<Longrightarrow>
666     lookup_range_tree (Node start end v l r) x = lookup_range_tree l x"
667  "\<lbrakk> start \<le> end; end \<le> x \<rbrakk> \<Longrightarrow>
668     lookup_range_tree (Node start end v l r) x = lookup_range_tree r x"
669  by auto
670
671end
672
673declare RangeMap.lookup_range_tree_simps'[simp]
674
675ML \<open>
676structure RangeMap = struct
677
678val $$ = uncurry Thm.apply;
679infix 9 $$;
680
681(* Like "OF", but first order, and resolving thms must not have extra prems *)
682fun FO_OF (thm, []) = thm
683  | FO_OF (thm, res::ress) = let
684      val (prem1, _) = Thm.dest_implies (Thm.cprop_of thm);
685      val inst = Thm.first_order_match (prem1, Thm.cprop_of res);
686      val thm' = Thm.instantiate inst thm;
687      in FO_OF (Thm.implies_elim thm' res, ress) end;
688infix 0 FO_OF;
689
690(* Applies conversion to a whole thm *)
691fun conv_prop conv thm =
692  let val next = conv (Thm.cprop_of thm);
693  in if Thm.is_reflexive next then thm else Thm.equal_elim next thm end;
694
695(* Like HOLogic.mk_list but for cterms *)
696fun mk_list ctxt T = let
697  val Nil = Const (@{const_name Nil}, HOLogic.listT T)
698            |> Thm.cterm_of ctxt;
699  val Cons = Const (@{const_name Cons}, T --> HOLogic.listT T --> HOLogic.listT T)
700             |> Thm.cterm_of ctxt;
701  in fn xs => fold_rev (fn x => fn xs => Cons $$ x $$ xs) xs Nil end;
702
703(* Build RangeTree cterm *)
704fun build_range_tree ctxt kT vT = let
705  val treeT = Type (@{type_name RangeMap.RangeTree}, [kT, vT]);
706  val leaf = Const (@{const_name RangeMap.Leaf}, treeT) |> Thm.cterm_of ctxt;
707  val node = Const (@{const_name RangeMap.Node}, kT-->kT-->vT-->treeT-->treeT-->treeT)
708             |> Thm.cterm_of ctxt;
709  fun build [] = leaf
710    | build kvs = let
711          val (kvs1, ((ks, ke), v) :: kvs2) = chop (length kvs div 2) kvs;
712          in node $$ ks $$ ke $$ v $$ build kvs1 $$ build kvs2
713          end;
714  in build end;
715
716(* Build lookup list cterm *)
717fun build_lookup_list ctxt kT vT = let
718  val key_rangeT = HOLogic.mk_prodT (kT, kT);
719  val key_Pair = Const (@{const_name Pair}, kT --> kT --> key_rangeT)
720                 |> Thm.cterm_of ctxt;
721  val elemT = HOLogic.mk_prodT (key_rangeT, vT);
722  val elem_Pair = Const (@{const_name Pair}, key_rangeT --> vT --> elemT)
723                  |> Thm.cterm_of ctxt;
724  fun elem ((ks, ke), v) = elem_Pair $$ (key_Pair $$ ks $$ ke) $$ v;
725  in mk_list ctxt elemT o map elem end;
726
727(* Quote all keys and values to prevent unwanted rewriting *)
728fun quote_elems ctxt kT vT =
729  let fun quote T = Const (@{const_name RangeMap.quote}, T-->T) |> Thm.cterm_of ctxt;
730  in map (fn ((ks, ke), v) => ((quote kT $$ ks, quote kT $$ ke), quote vT $$ v)) end;
731
732(* Check whether conversion is valid and its result lies in a given list *)
733fun is_conv_to terms (src, conv) =
734      Thm.term_of (Thm.lhs_of conv) aconv Thm.term_of src andalso
735      exists (fn term => Thm.term_of (Thm.rhs_of conv) aconv term) terms;
736
737(* Checking generated lookup rules *)
738fun check_generated_thms desc templates thms =
739      if length thms <> length templates then
740        raise THM ("RangeMap internal error: generated " ^ string_of_int (length thms) ^
741                   " thms for " ^ desc ^ ", but expected " ^ string_of_int (length templates),
742                   0, thms)
743      else case filter (fn (thm, template) => not (Thm.prop_of thm aconv template))
744                       (thms ~~ templates) of
745               [] => ()
746             | bads => raise THM ("RangeMap internal error: wrong format for " ^ desc,
747                                  0, map fst bads);
748
749(* Common FP_Eval configuration. We use hold_quote everywhere to avoid
750   descending into user input terms *)
751fun fp_eval_conv' ctxt rules congs =
752  FP_Eval.eval_conv ctxt (FP_Eval.make_rules rules (congs @ @{thms RangeMap.hold_quote}));
753
754fun unquote_conv ctxt = FP_Eval.eval_conv ctxt (FP_Eval.make_rules @{thms RangeMap.unquote} []);
755val unquote_thm = Conv.fconv_rule o unquote_conv;
756
757(* Helper for targeted beta reduction *)
758fun beta_conversion_thm conv_where =
759      conv_prop (conv_where (Thm.beta_conversion false));
760
761(* Pre-compute key comparison results.
762   This allows us to report errors early and avoid cluttering
763   other proofs with the user-supplied key ordering semantics. *)
764fun compare_keys ctxt kT solver elems =
765  let val but_last = split_last #> fst;
766      val elem_pairs = if null elems then [] else but_last elems ~~ tl elems;
767      val cmpT = kT --> kT --> @{typ bool};
768      val eqT = Thm.cterm_of ctxt (Const (@{const_name HOL.eq}, cmpT));
769      val lessT = Thm.cterm_of ctxt (Const (@{const_name less}, cmpT));
770      val less_eqT = Thm.cterm_of ctxt (Const (@{const_name less_eq}, cmpT));
771
772      (* Monotonicity: required to be True always *)
773      val monotonic_cmps =
774              map (fn ((ks, ke), _) => less_eqT $$ ks $$ ke) elems
775            @ map (fn (((_, ke), _), ((ks', _), _)) => less_eqT $$ ke $$ ks') elem_pairs;
776
777      val monotonic_results = map solver monotonic_cmps;
778      val _ = case filter (not o is_conv_to [@{term True}])
779                          (monotonic_cmps ~~ monotonic_results) of
780                  [] => ()
781                | ((_, bad)::_) =>
782                    raise THM ("RangeMap: failed to solve key constraint", 0, [bad]);
783
784      (* Determine whether ranges are adjacent.
785         Allowed to be False, used for generating compact domain thm. *)
786      val adj_eq_cmps =
787            map (fn (((_, ke), _), ((ks', _), _)) => eqT $$ ke $$ ks') elem_pairs;
788
789      val adj_eq_results = map solver adj_eq_cmps;
790      val _ = case filter (not o is_conv_to [@{term True}, @{term False}])
791                          (adj_eq_cmps ~~ adj_eq_results) of
792                  [] => ()
793                | ((_, bad)::_) =>
794                    raise THM ("RangeMap: failed to solve key constraint", 0, [bad]);
795
796      (* Determine whether each key range is nonempty.
797         Allowed to be False, used for generating range thm. *)
798      val nonempty_cmps =
799              map (fn ((ks, ke), _) => lessT $$ ks $$ ke) elems;
800
801      val nonempty_results = map solver nonempty_cmps;
802      val _ = case filter (not o is_conv_to [@{term True}, @{term False}])
803                          (nonempty_cmps ~~ nonempty_results) of
804                  [] => ()
805                | ((_, bad)::_) =>
806                    raise THM ("RangeMap: failed to solve key range emptyiness", 0, [bad]);
807
808  in (monotonic_results, adj_eq_results, nonempty_results) end;
809
810(*** Generate various theorems and conversions ***)
811
812fun gen__lookup_range_tree_valid ctxt tree_const tree_def key_cmps =
813  let val prop =
814        @{mk_term "Trueprop (fst (RangeMap.lookup_range_tree_valid ?tree))" (tree)} tree_const
815        |> Thm.cterm_of ctxt;
816      val rules = FP_Eval.make_rules
817                    (@{thms RangeMap.lookup_range_tree_valid.simps
818                            simp_thms prod.sel prod.case option.case Let_def if_True if_False}
819                     @ [tree_def] @ key_cmps)
820                    @{thms if_weak_cong FP_Eval.let_weak_cong' option.case_cong_weak
821                           RangeMap.hold_quote};
822  in Goal.init prop
823     |> (FP_Eval.eval_tac ctxt rules 1
824         THEN resolve_tac ctxt @{thms TrueI} 1)
825     |> Seq.hd
826     |> Goal.finish ctxt
827  end;
828
829fun gen__lookup_range_tree_to_list ctxt tree_const tree_def list_const list_def =
830  let val prop =
831        @{mk_term "Trueprop (RangeMap.lookup_range_tree_to_list ?tree = ?list)" (tree, list)}
832          (tree_const, list_const)
833        |> Thm.cterm_of ctxt;
834      val rules = FP_Eval.make_rules
835                    (@{thms RangeMap.lookup_range_tree_to_list.simps append.simps}
836                     @ [list_def, tree_def])
837                    @{thms RangeMap.hold_quote};
838  in Goal.init prop
839     |> (FP_Eval.eval_tac ctxt rules 1
840         THEN resolve_tac ctxt @{thms refl} 1)
841     |> Seq.hd
842     |> Goal.finish ctxt
843  end;
844
845fun gen__range_lookups ctxt tree_list_lookup_eq_thm list_def list_monotonic_thm =
846  (@{thm RangeMap.range_map_of_lookups__gen_all}
847      FO_OF [tree_list_lookup_eq_thm, list_monotonic_thm])
848  |> Conv.fconv_rule (fp_eval_conv' ctxt
849                        (@{thms RangeMap.list_all_dest prod.case} @ [list_def]) [])
850  |> HOLogic.conj_elims ctxt
851  |> map (fn t => (@{thm RangeMap.spec_FO} FO_OF [t])
852                  |> beta_conversion_thm Conv.arg_conv (* beta reduce result of spec thm *))
853  |> map (Conv.fconv_rule (fp_eval_conv' ctxt @{thms RangeMap.in_range.simps} []));
854
855fun expected__range_lookups tree_const elems =
856  elems
857  |> map (fn ((ks, ke), v) =>
858            @{mk_term "Trueprop ((?s \<le> ?x \<and> ?x < ?e)
859                                 = (RangeMap.lookup_range_tree ?tree ?x = Some ((?s, ?e), ?v)))"
860                       (tree, s, e, v)}
861              (tree_const, Thm.term_of ks, Thm.term_of ke, Thm.term_of v));
862
863fun gen__start_lookups ctxt
864      tree_list_lookup_eq_thm list_def list_monotonic_thm key_range_nonempty_thms =
865  (@{thm RangeMap.range_map_of_start_lookups__gen_all}
866      FO_OF [tree_list_lookup_eq_thm, list_monotonic_thm])
867  |> Conv.fconv_rule (fp_eval_conv' ctxt
868                        (@{thms RangeMap.list_all_dest prod.case simp_thms}
869                         @ [list_def] @ key_range_nonempty_thms)
870                        [])
871  |> HOLogic.conj_elims ctxt;
872
873fun expected__start_lookups tree_const elems key_range_nonempty_thms =
874  elems ~~ key_range_nonempty_thms
875  |> filter (fn (_, cmp) => Thm.term_of (Thm.rhs_of cmp) = @{term True})
876  |> map fst
877  |> map (fn ((ks, ke), v) =>
878            @{mk_term "Trueprop (RangeMap.lookup_range_tree ?tree ?s = Some ((?s, ?e), ?v))"
879                       (tree, s, e, v)}
880              (tree_const, Thm.term_of ks, Thm.term_of ke, Thm.term_of v));
881
882fun gen__domain_thm ctxt tree_const tree_list_lookup_eq_thm =
883  @{mk_term "dom (RangeMap.lookup_range_tree ?tree)" (tree)} tree_const
884  |> Thm.cterm_of ctxt
885  |> fp_eval_conv' ctxt ([tree_list_lookup_eq_thm] @ @{thms RangeMap.dom_range_map_of}) [];
886
887fun gen__compact_domain_thm ctxt domain_thm list_def list_monotonic_thm key_adj_equal_thms =
888  domain_thm
889  |> Conv.fconv_rule
890      ((* First, invoke @{const RangeMap.combine_contiguous_ranges} *)
891       (fp_eval_conv' ctxt
892          [(@{thm RangeMap.combine_contiguous_ranges_correct} FO_OF [list_monotonic_thm])] [])
893       then_conv
894       (* Now evaluate combine_contiguous_ranges. We can't expand the
895          lookup list definition before using "combine_contiguous_ranges_correct",
896          so this is split into a subsequent eval step. *)
897       (fp_eval_conv' ctxt
898                ([list_def]
899                 @ @{thms RangeMap.combine_contiguous_ranges.simps prod.case list.map prod.sel
900                          rel_simps simp_thms if_True if_False
901                          RangeMap.Collect_in_range_atLeastLessThan o_apply}
902                 @ key_adj_equal_thms)
903                @{thms if_weak_cong})
904      );
905
906fun gen__range_thm ctxt
907      tree_const tree_list_lookup_eq_thm list_def list_monotonic_thm key_range_nonempty_thms =
908  @{mk_term "ran (RangeMap.lookup_range_tree ?tree)" (tree)} tree_const
909  |> Thm.cterm_of ctxt
910  |> (fp_eval_conv' ctxt
911            ([tree_list_lookup_eq_thm]
912             @ [@{thm RangeMap.ran_range_map_of} FO_OF [list_monotonic_thm]])
913            []
914      then_conv
915      fp_eval_conv' ctxt
916            ([list_def] @ key_range_nonempty_thms
917             @ @{thms filter.simps prod.case simp_thms if_True if_False})
918            @{thms if_weak_cong prod.case_cong_weak}
919      (* if range turns out to contain all elements, collapse back into list *)
920      then_conv
921      fp_eval_conv' ctxt [Thm.symmetric list_def] []
922     );
923
924(*** User interface ***)
925
926(* Choosing names for the const and its theorems. The constant will be named with
927   map_name; Local_Theory.define may also add extra names (e.g. <map_name>_def) *)
928type name_opts = {
929    tree_const: binding,
930    tree_def: binding,
931    list_const: binding,
932    list_def: binding,
933    tree_valid_thm: binding,
934    tree_to_list_thm: binding,
935    tree_list_lookup_eq_thm: binding,
936    list_monotonic_thm: binding,
937    range_lookup_thms: binding,
938    start_lookup_thms: binding,
939    domain_thm: binding,
940    compact_domain_thm: binding,
941    range_thm: binding
942};
943
944fun name_opts_default (base_name: string): name_opts =
945  let val qual = Binding.qualify_name true (Binding.name base_name);
946  in {
947    tree_const = qual "tree",
948    tree_def = Thm.def_binding (qual "tree"),
949    list_const = qual "list",
950    list_def = Thm.def_binding (qual "list"),
951    tree_valid_thm = qual "tree_valid",
952    tree_to_list_thm = qual "tree_to_list",
953    tree_list_lookup_eq_thm = qual "tree_list_lookup_eq",
954    list_monotonic_thm = qual "list_monotonic",
955    range_lookup_thms = qual "lookups",
956    start_lookup_thms = qual "start_lookups",
957    domain_thm = qual "domain",
958    compact_domain_thm = qual "domain_compact",
959    range_thm = qual "range"
960  } end;
961
962(* Top level *)
963fun define_map
964      (name_opts: name_opts)
965      (elems: ((cterm * cterm) * cterm) list)
966      (kT: typ)
967      (vT: typ)
968      (key_cmp_solver: conv)
969      ctxt =
970  let
971    fun msg x = "RangeMap: " ^ Binding.print (#tree_const name_opts) ^ ": " ^ x;
972    val tracing_msg = tracing o msg;
973
974    (* check input types *)
975    val _ = elems
976            |> app (fn ((ks, ke), v) =>
977                  if Thm.typ_of_cterm ks <> kT
978                  then raise TYPE (msg "key has wrong type", [kT], [Thm.term_of ks])
979                  else if Thm.typ_of_cterm ke <> kT
980                  then raise TYPE (msg "key has wrong type", [kT], [Thm.term_of ke])
981                  else if Thm.typ_of_cterm v <> vT
982                  then raise TYPE (msg "value has wrong type", [vT], [Thm.term_of v])
983                  else ());
984
985    (* quote all input keys and values *)
986    val quoted_elems = quote_elems ctxt kT vT elems;
987    (* unquote when computing key comparisons *)
988    val quoted_key_cmp_solver = unquote_conv ctxt then_conv key_cmp_solver;
989
990    (* less verbose "notes"; also unquotes user input *)
991    fun notes ctxt thmss =
992          Local_Theory.notes
993            (map (fn (bind, thms) => ((bind, []), [(map (unquote_thm ctxt) thms, [])])) thmss) ctxt
994          |> snd;
995
996    val _ = tracing_msg "evaluating key comparisons";
997    val start = Timing.start ();
998    val (key_mono_thms, key_adj_eq_thms, key_range_nonempty_thms) =
999           compare_keys ctxt kT quoted_key_cmp_solver quoted_elems;
1000    val _ = tracing_msg ("done: " ^ Timing.message (Timing.result start));
1001
1002    val _ = tracing_msg "defining tree";
1003    val start = Timing.start ();
1004    val quoted_tree = build_range_tree ctxt kT vT quoted_elems;
1005    val unquote_tree_eqn = unquote_conv ctxt quoted_tree;
1006    val unquoted_tree = Thm.rhs_of unquote_tree_eqn;
1007    val ((tree_const, (_, tree_def)), ctxt) =
1008          ctxt |> Local_Theory.define
1009              ((#tree_const name_opts, NoSyn),
1010               ((#tree_def name_opts, []), Thm.term_of unquoted_tree));
1011    val quoted_tree_def = Thm.transitive tree_def (Thm.symmetric unquote_tree_eqn);
1012    val _ = tracing_msg ("done: " ^ Timing.message (Timing.result start));
1013
1014    val _ = tracing_msg "defining lookup list";
1015    val start = Timing.start ();
1016    val quoted_list = build_lookup_list ctxt kT vT quoted_elems;
1017    val unquote_list_eqn = unquote_conv ctxt quoted_list;
1018    val unquoted_list = Thm.rhs_of unquote_list_eqn;
1019    val ((list_const, (_, list_def)), ctxt) =
1020          ctxt |> Local_Theory.define
1021              ((#list_const name_opts, NoSyn),
1022               ((#list_def name_opts, []), Thm.term_of unquoted_list));
1023    val quoted_list_def = Thm.transitive list_def (Thm.symmetric unquote_list_eqn);
1024    val _ = tracing_msg ("done: " ^ Timing.message (Timing.result start));
1025
1026    val _ = tracing_msg "proving tree validity";
1027    val start = Timing.start ();
1028    val tree_valid_thm =
1029          gen__lookup_range_tree_valid ctxt tree_const quoted_tree_def key_mono_thms;
1030    val ctxt = notes ctxt
1031          [(#tree_valid_thm name_opts, [tree_valid_thm])];
1032    val _ = tracing_msg ("done: " ^ Timing.message (Timing.result start));
1033
1034    val _ = tracing_msg "proving tree and list correspondence";
1035    val start = Timing.start ();
1036    val tree_to_list_thm =
1037          gen__lookup_range_tree_to_list ctxt
1038                tree_const quoted_tree_def
1039                list_const quoted_list_def;
1040    val list_properties =
1041          @{thm RangeMap.lookup_range_tree_to_list_of_gen}
1042            FO_OF [tree_valid_thm, tree_to_list_thm];
1043    val [tree_list_lookup_eq_thm, list_monotonic_thm] =
1044          HOLogic.conj_elims ctxt list_properties;
1045    val ctxt = notes ctxt
1046          [(#tree_to_list_thm name_opts, [tree_to_list_thm]),
1047           (#tree_list_lookup_eq_thm name_opts, [tree_list_lookup_eq_thm]),
1048           (#list_monotonic_thm name_opts, [list_monotonic_thm])];
1049    val _ = tracing_msg ("done: " ^ Timing.message (Timing.result start));
1050
1051    val _ = tracing_msg "generating lookup rules";
1052    val start = Timing.start ();
1053    val tree_range_lookups =
1054          if null elems then [] else
1055          gen__range_lookups ctxt tree_list_lookup_eq_thm quoted_list_def list_monotonic_thm
1056          |> tap (check_generated_thms "range lookup rule"
1057                    (expected__range_lookups tree_const quoted_elems));
1058    val tree_start_lookups =
1059          if null elems then [] else
1060          gen__start_lookups ctxt
1061              tree_list_lookup_eq_thm quoted_list_def list_monotonic_thm key_range_nonempty_thms
1062          |> tap (check_generated_thms "start lookup rule"
1063                    (expected__start_lookups tree_const quoted_elems key_range_nonempty_thms));
1064    val ctxt = notes ctxt
1065          [(#range_lookup_thms name_opts, tree_range_lookups),
1066           (#start_lookup_thms name_opts, tree_start_lookups)];
1067    val _ = tracing_msg ("done: " ^ Timing.message (Timing.result start));
1068
1069    val _ = tracing_msg "calculating domain and range";
1070    val domain_thm = gen__domain_thm ctxt tree_const tree_list_lookup_eq_thm;
1071    val compact_domain_thm =
1072          gen__compact_domain_thm ctxt
1073              domain_thm quoted_list_def list_monotonic_thm key_adj_eq_thms;
1074    val domain_thm' = (* remove internal "in_range" *)
1075          domain_thm
1076          |> Conv.fconv_rule (fp_eval_conv' ctxt @{thms RangeMap.Collect_in_range_rewrite} []);
1077    val range_thm =
1078          gen__range_thm ctxt tree_const
1079              tree_list_lookup_eq_thm quoted_list_def list_monotonic_thm key_range_nonempty_thms;
1080    val ctxt = notes ctxt
1081          [(#domain_thm name_opts, [domain_thm']),
1082           (#compact_domain_thm name_opts, [compact_domain_thm]),
1083           (#range_thm name_opts, [range_thm])];
1084    val _ = tracing_msg ("done: " ^ Timing.message (Timing.result start));
1085  in ctxt end;
1086
1087end;
1088\<close>
1089
1090end