1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory RangeMap_Test
8imports
9  Lib.RangeMap
10  Main
11begin
12
13section \<open>Examples for RangeMap\<close>
14
15experiment begin
16
17subsection \<open>Basic usage\<close>
18
19local_setup \<open>
20RangeMap.define_map
21  (* Specification of names to generate. "name_opts_default" generates qualified names
22     starting with the given string i.e. "test_map.foo". *)
23  (RangeMap.name_opts_default "test_map")
24
25  (* List of ((start key, end key), value).
26     Key ranges include the start but not the end points. *)
27  [((@{cterm "1::nat"}, @{cterm "2::nat"}), @{cterm "True"}),
28   ((@{cterm "2::nat"}, @{cterm "3::nat"}), @{cterm "False"}),
29   ((@{cterm "5::nat"}, @{cterm "8::nat"}), @{cterm "True \<and> False"}),
30   (* Key ranges are allowed to be empty, such as this one *)
31   ((@{cterm "8::nat"}, @{cterm "8::nat"}), @{cterm "True \<or> False"}),
32   (* Test for input preservation; see below *)
33   ((@{cterm "if True then 8::nat else undefined"}, @{cterm "6 + 7 :: nat"}),
34    @{cterm "False \<longrightarrow> True"})
35  ]
36
37  (* Key and value types. *)
38  @{typ nat} @{typ bool}
39  (* Key comparison solver. This should be a conversion that converts
40     key comparisons to True or False. *)
41  (Simplifier.rewrite @{context})
42\<close>
43print_theorems
44
45text \<open>
46  Generated definitions for lookup tree and list:
47\<close>
48thm test_map.tree_def test_map.list_def
49
50text \<open>
51  Lookup theorems:
52\<close>
53thm test_map.lookups
54
55text \<open>
56  We also get lookup theorems for the start of each range (if nonempty).
57  These can be useful simplifier equations in some scenarios.
58\<close>
59thm test_map.start_lookups
60
61text \<open>
62  Test that user-provided key terms are preserved verbatim.
63\<close>
64ML \<open>
65@{assert}
66  (Thm.prop_of @{thm test_map.lookups(5)[where x=x]}
67   = @{term "Trueprop (((if True then 8 else undefined) \<le> x \<and> x < 6 + 7)
68             = (RangeMap.lookup_range_tree test_map.tree x
69                = Some ((if True then 8 else undefined, 6 + 7), False \<longrightarrow> True)))"});
70\<close>
71
72text \<open>
73  The domain is just the union of all key ranges.
74  In practice, maps tend to have many contiguous ranges. RangeMap also
75  generates a "compact" domain theorem that merges adjacent ranges.
76\<close>
77thm test_map.domain test_map.domain_compact
78
79
80subsection \<open>Test that empty maps are supported\<close>
81
82local_setup \<open>
83RangeMap.define_map
84  (RangeMap.name_opts_default "empty_test")
85  []
86  @{typ int} @{typ int}
87  Thm.reflexive (* unused *)
88\<close>
89print_theorems
90
91
92subsection \<open>Stress testing\<close>
93ML \<open>
94fun range_map_test_legendre n =
95  let fun P q x = if q*q > x then true else x mod q <> 0 andalso P (q+1) x;
96  in (1 upto n)
97     |> map (fn k => ((k*k, (k+1)*(k+1)), hd (filter (P 2) (k*k+1 upto (k+1)*(k+1))))) end;
98
99fun range_map_test_legendre_ct T n =
100  let fun cterm_of_num T n = Thm.cterm_of @{context} (HOLogic.mk_number T n);
101  in range_map_test_legendre n
102     |> map (fn ((ks, ke), v) => ((cterm_of_num T ks, cterm_of_num T ke), cterm_of_num T v)) end;
103\<close>
104
105local_setup \<open>
106RangeMap.define_map
107  (RangeMap.name_opts_default "legendre_10")
108  (range_map_test_legendre_ct @{typ nat} 10)
109  @{typ nat} @{typ nat}
110  (FP_Eval.eval_conv @{context} (FP_Eval.make_rules @{thms rel_simps} []))
111\<close>
112
113local_setup \<open>
114RangeMap.define_map
115  (RangeMap.name_opts_default "legendre_100")
116  (range_map_test_legendre_ct @{typ nat} 100)
117  @{typ nat} @{typ nat}
118  (FP_Eval.eval_conv @{context} (FP_Eval.make_rules @{thms rel_simps} []))
119\<close>
120
121local_setup \<open>
122RangeMap.define_map
123  (RangeMap.name_opts_default "legendre_1000")
124  (range_map_test_legendre_ct @{typ nat} 1000)
125  @{typ nat} @{typ nat}
126  (FP_Eval.eval_conv @{context} (FP_Eval.make_rules @{thms rel_simps} []))
127\<close>
128
129(* Example of proof using range map *)
130lemma legendre_100_values:
131  "RangeMap.lookup_range_tree legendre_100.tree k = Some ((start, end), v)
132   \<Longrightarrow> start < v \<and> v < end"
133  (* Convert to list and expand *)
134  apply (subst (asm) legendre_100.tree_list_lookup_eq)
135  apply (drule RangeMap.range_map_of_Some)
136  apply (clarsimp simp: legendre_100.list_def)
137  apply linarith
138  done
139
140end
141
142end
143