1open HolKernel Parse boolLib bossLib
2
3val _ = new_theory "location";
4
5val _ = Datatype `
6 locn = <| row : num;  col : num; offset : num |>`;
7
8val _ = Datatype `
9  locs = Locs locn locn
10`
11
12val default_loc_def = Define`
13  default_loc = <| row := 1; col := 1; offset := 0 |>`;
14
15val start_loc_def = Define`
16  start_loc = (default_loc,default_loc)`;
17
18val unknown_loc_def = Define`
19  unknown_loc = Locs <| row := 0; col := 0; offset := 0 |>
20                     <| row := 0; col := 0; offset := 0 |>`;
21val merge_locs_def = Define`
22  merge_locs (Locs l1 l2) (Locs l3 l4) = Locs l1 l4
23`;
24
25val merge_list_locs_def = Define`
26  (merge_list_locs [] = unknown_loc) /\
27  (merge_list_locs (h :: []) = h) /\
28  (merge_list_locs (h1 :: h2 :: []) = merge_locs h1 h2) /\
29  (merge_list_locs (h1 :: h2 :: t) = merge_list_locs (h1 :: t))`;
30
31(* for debugging *)
32
33val map_loc_def = Define`
34  (map_loc [] _ = []) /\
35  (map_loc (h :: t) n =
36    (h, Locs <| row := n; col := 0; offset := 0 |>
37             <| row := n; col := 1; offset := 0 |>) :: map_loc t (n+1))
38`;
39
40
41val merge_locs_assoc = Q.store_thm(
42  "merge_locs_assoc[simp]",
43  ���(merge_locs (merge_locs l1 l2) l3 = merge_locs l1 l3) ���
44   (merge_locs l1 (merge_locs l2 l3) = merge_locs l1 l3)���,
45  map_every Cases_on [`l1`, `l2`, `l3`] >>
46  simp[merge_locs_def]);
47
48val merge_list_locs_2 = Q.store_thm(
49  "merge_list_locs_2[simp]",
50  ������h1 h2 t.
51     merge_list_locs (h1 :: h2 :: t) = merge_list_locs (merge_locs h1 h2 :: t)���,
52  Induct_on ���t��� >> simp[merge_list_locs_def]);
53
54val merge_list_locs_nested = Q.store_thm(
55  "merge_list_locs_nested[simp]",
56  ������h t1 t2. merge_list_locs (merge_list_locs (h::t1) :: t2) =
57             merge_list_locs (h :: t1 ++ t2)���,
58  Induct_on ���t1��� >> simp[merge_list_locs_def]);
59
60val merge_list_locs_sing = Q.store_thm(
61  "merge_list_locs_sing[simp]",
62  ���merge_list_locs [h] = h���,
63  simp[merge_list_locs_def]);
64
65val merge_locs_idem = Q.store_thm(
66  "merge_locs_idem[simp]",
67  ���merge_locs l l = l���,
68  Cases_on ���l��� >> simp[merge_locs_def]);
69
70val _ = export_theory();
71