1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Author: Thomas C. Hales *)
7 (* ========================================================================== *)
10 (* ------------------------------------------------------------------ *)
11 (* LOCAL DEFINITIONS , from Jordan curve lib_ext.ml *)
12 (* ------------------------------------------------------------------ *)
16 module type Local_definition_type = sig
22 module Local_definition : Local_definition_type = struct
24 let local_defs = ref ([]:(string * (string * term)) list);;
26 let add_interface (sym,tm) =
27 if (can (assoc sym) (!the_overload_skeletons)) then
28 (overload_interface (sym,tm))
29 else (override_interface(sym,tm));;
31 let local_definition package_name tm =
32 let list_mk_forall(vars,bod) = itlist (curry mk_forall) vars bod in
33 let avs,bod = strip_forall tm in
34 let l,r = try dest_eq bod
35 with Failure _ -> failwith "new_local_definition: Not an equation" in
36 let lv,largs = strip_comb l in
37 let cname,ty = dest_var lv in
38 let cname' = package_name^"'"^cname in
39 let lv' = mk_var(cname',ty) in
40 let l' = list_mk_comb(lv',largs) in
41 let bod' = mk_eq(l',r) in
42 let tm'= list_mk_forall(avs,bod') in
43 let thm = new_definition tm' in
44 let _ = (local_defs := (package_name,(cname,lv'))::(!local_defs)) in
45 let _ = add_interface(cname,lv') in
48 let reduce_local_interface(package_name) =
49 map (reduce_interface o snd)
50 (filter (fun x -> ((fst x) = package_name)) !local_defs);;
52 let mk_local_interface(package_name) =
53 map (add_interface o snd)
54 (filter (fun x -> ((fst x) = package_name)) !local_defs);;
57 (* adapted from HOL Light code, true if it is a local def. *)
61 let tm' = snd(strip_forall tm) in
62 try let th,th' = tryfind (fun th -> th,PART_MATCH I th tm')
64 (can (PART_MATCH I th') (concl th))
65 with Failure _ -> false;;