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