1 (* ========================================================================= *)
3 (* Isabelle/Procedural style additions and other user-friendly shortcuts. *)
5 (* Petros Papapanagiotou, Jacques Fleuriot *)
6 (* Center of Intelligent Systems and their Applications *)
7 (* University of Edinburgh *)
9 (* ========================================================================= *)
10 (* FILE : support.ml *)
11 (* DESCRIPTION : Support functions and various shortcuts. *)
12 (* LAST MODIFIED: October 2012 *)
13 (* ========================================================================= *)
15 (* ------------------------------------------------------------------------- *)
16 (* Functions to deal with triplets: *)
17 (* ------------------------------------------------------------------------- *)
19 let fst3 (x,_,_) = x;;
20 let snd3 (_,x,_) = x;;
21 let thd3 (_,_,x) = x;;
24 (*----------------------------------------------------------------------------*)
25 (* num_list : a' list -> (a' * int) list *)
27 (* Numbers a list of elements, *)
28 (* e.g. [`a`;`b`;`c`] ---> [(0,`a`);(1,`b`);(2,`c`)]. *)
29 (*----------------------------------------------------------------------------*)
32 let rec number_list' n l =
34 else (n,hd l)::(number_list' (n + 1) (tl l))
38 (* ------------------------------------------------------------------------- *)
39 (* list_match_first: (a' -> b') -> a' list -> b' *)
40 (* Tries to apply a function to the members of a list. Returns the result *)
41 (* from the first member that succeeds. *)
42 (* ------------------------------------------------------------------------- *)
44 let rec list_match_first f alist =
45 if (alist = []) then failwith "list_match_first: No matches!"
46 else try f (hd alist) with Failure _ -> list_match_first f (tl alist);;
49 (* ------------------------------------------------------------------------- *)
50 (* terms_match: term list -> term -> term list -> instantiation *)
51 (* Tries to apply term_match to the first possible term in a list. *)
52 (* Returns the insantiation. *)
53 (* ------------------------------------------------------------------------- *)
55 let (terms_match: term list -> term -> term list -> instantiation ) =
56 fun consts key tlist ->
57 try (list_match_first (term_match consts key) tlist)
58 with Failure _ -> failwith "terms_match: No terms match!";;
61 (* ------------------------------------------------------------------------- *)
62 (* thm_mk_primed_vars: term list -> thm -> thm *)
63 (* Renames all free variables in a theorem to avoid specified and constant *)
65 (* ------------------------------------------------------------------------- *)
67 let thm_mk_primed_vars avoids thm =
68 let fvars = thm_frees thm in
69 let new_vars = map (mk_primed_var avoids) fvars in
70 let insts = List.combine new_vars fvars in
74 (* ------------------------------------------------------------------------- *)
75 (* gl_frees: goal -> term list *)
76 (* Finds the free variables in a subgoal (assumptions and goal). *)
77 (* ------------------------------------------------------------------------- *)
79 let gl_frees : goal -> term list =
80 fun (asl,w) -> itlist (union o thm_frees o snd) asl (frees w);;
83 (* ------------------------------------------------------------------------- *)
84 (* ADD_HYP: thm -> thm -> thm *)
85 (* Trivially adds the hypotheses of a theorem to the premises of another. *)
86 (* ------------------------------------------------------------------------- *)
87 (* (+) Used in the justification of erule and drule to add the eliminated *)
88 (* assumption to the proven subgoals. *)
89 (* (+) Could have been based on ADD_ASSUM but it's more convenient this way. *)
90 (* ------------------------------------------------------------------------- *)
92 let ADD_HYP hyp_thm thm = CONJUNCT2 (CONJ hyp_thm thm);;
95 (* ------------------------------------------------------------------------- *)
96 (* DISCHL: term list -> thm -> thm *)
97 (* Applies DISCH for several terms. *)
98 (* ------------------------------------------------------------------------- *)
100 let rec (DISCHL: term list -> thm -> thm) =
102 if (tms = []) then thm
103 else DISCH (hd tms) (DISCHL (tl tms) thm);;
106 (* ------------------------------------------------------------------------- *)
108 (* Print a list of theorems (for debugging). *)
109 (* ------------------------------------------------------------------------- *)
112 map (fun thm -> ( print_thm thm ; print_newline ())) thl;;
115 (* ------------------------------------------------------------------------- *)
117 (* Print a list of terms (for debugging). *)
118 (* ------------------------------------------------------------------------- *)
121 map (fun tm -> ( print_term tm ; print_newline ())) tml;;
124 (* ------------------------------------------------------------------------- *)
125 (* print_varandtype, show_types, hide_types: *)
126 (* Prints the type after each variable. Useful for "debugging" type issues. *)
127 (* ------------------------------------------------------------------------- *)
129 (* http://code.google.com/p/flyspeck/wiki/TipsAndTricks#Investigating_Types *)
130 (* ------------------------------------------------------------------------- *)
132 let print_varandtype fmt tm =
133 let hop,args = strip_comb tm in
135 and ty = type_of hop in
136 if is_var hop & args = [] then
137 (pp_print_string fmt "(";
138 pp_print_string fmt s;
139 pp_print_string fmt ":";
140 pp_print_type fmt ty;
141 pp_print_string fmt ")")
144 let show_types,hide_types =
145 (fun () -> install_user_printer ("Show Types",print_varandtype)),
146 (fun () -> try delete_user_printer "Show Types"
147 with Failure _ -> failwith ("hide_types: "^
148 "Types are already hidden."));;
151 (* ------------------------------------------------------------------------- *)
152 (* count_goals : unit -> int *)
153 (* Shortcut to count the subgoals in the current goalstate. *)
154 (* ------------------------------------------------------------------------- *)
157 if (!current_goalstack = []) then 0 else
158 ( let _,gls,_ = hd !current_goalstack in length gls );;
162 (* ------------------------------------------------------------------------- *)
163 (* top_asms : goalstack -> (string * thm) list *)
164 (* Shortcut to get the assumption list of the top goal of a given goalstack. *)
165 (* ------------------------------------------------------------------------- *)
167 let top_asms (gs:goalstack) = (fst o hd o snd3 o hd) gs;;
170 (* ------------------------------------------------------------------------- *)
171 (* top_metas : goalstack -> term list *)
172 (* Returns the list of metavariables in the current goalstate. *)
173 (* ------------------------------------------------------------------------- *)
175 let top_metas (gs:goalstack) = (fst o fst3 o hd) gs;;
178 (* ------------------------------------------------------------------------- *)
179 (* top_inst : goalstack -> instantiation *)
180 (* Returns the metavariable instantiations in the current goalstate. *)
181 (* ------------------------------------------------------------------------- *)
183 let top_inst (gs:goalstack) = (snd o fst3 o hd) gs;;
186 (* ------------------------------------------------------------------------- *)
187 (* print_goalstack_all : *)
188 (* Alternative goalstack printer that always prints all subgoals. *)
189 (* Also prints list of metavariables with their types. *)
190 (* ------------------------------------------------------------------------- *)
191 (* Original printer only prints more than one subgoals iff they were *)
192 (* generated by the last step. Otherwise it only prints the 'active' subgoal.*)
193 (* Replace by #install_printer print_goalstack_all;; *)
194 (* Revert to original by #install_printer print_goalstack;; *)
195 (* ------------------------------------------------------------------------- *)
197 let (print_goalstack_all:goalstack->unit) =
198 let print_goalstate k gs =
199 let ((mvs,_),gl,_) = gs in
201 let s = if n = 0 then "No subgoals" else
202 (string_of_int k)^" subgoal"^(if k > 1 then "s" else "")
203 ^" ("^(string_of_int n)^" total)" in
204 let print_mv v = print_string " `" ;
205 print_varandtype std_formatter v ;
207 print_string s; print_newline();
208 if (length mvs > 0) then (
209 print_string "Metas:" ; let _ = map print_mv mvs in () ; print_newline()
211 if gl = [] then () else
212 do_list (print_goal o C el gl) (rev(0--(k-1))) in
214 if l = [] then print_string "Empty goalstack"
216 let (_,gl,_ as gs) = hd l in
217 print_goalstate (length gl) gs;;
220 (* ------------------------------------------------------------------------- *)
221 (* print_goalstack : *)
222 (* Upgrade to print_goalstack that also prints a list of metavariables with *)
224 (* ------------------------------------------------------------------------- *)
226 let (print_goalstack:goalstack->unit) =
227 let print_goalstate k gs =
228 let ((mvs,_),gl,_) = gs in
230 let s = if n = 0 then "No subgoals" else
231 (string_of_int k)^" subgoal"^(if k > 1 then "s" else "")
232 ^" ("^(string_of_int n)^" total)" in
233 let print_mv v = print_string " `" ;
234 print_varandtype std_formatter v ;
236 print_string s; print_newline();
237 if (length mvs > 0) then (
238 print_string "Metas:" ; let _ = map print_mv mvs in () ; print_newline()
240 if gl = [] then () else
241 do_list (print_goal o C el gl) (rev(0--(k-1))) in
243 if l = [] then print_string "Empty goalstack"
244 else if tl l = [] then
245 let (_,gl,_ as gs) = hd l in
248 let (_,gl,_ as gs) = hd l
249 and (_,gl0,_) = hd(tl l) in
250 let p = length gl - length gl0 in
251 let p' = if p < 1 then 1 else p + 1 in
252 print_goalstate p' gs;;
254 #install_printer print_goalstack;;