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