IsabelleLight/support.ml

   1 (* ========================================================================= *)
   2 (*                              Isabelle Light                               *)
   3 (*   Isabelle/Procedural style additions and other user-friendly shortcuts.  *)
   4 (*                                                                           *)
   5 (*                   Petros Papapanagiotou, Jacques Fleuriot                 *)
   6 (*              Center of Intelligent Systems and their Applications         *)
   7 (*                          University of Edinburgh                          *)
   8 (*                                 2009-2012                                 *)
   9 (* ========================================================================= *)
  10 (* FILE         : support.ml                                                 *)
  11 (* DESCRIPTION  : Support functions and various shortcuts.                   *)
  12 (* LAST MODIFIED: October 2012                                               *)
  13 (* ========================================================================= *)
  14
  15 (* ------------------------------------------------------------------------- *)
  16 (* Functions to deal with triplets:                                          *)
  17 (* ------------------------------------------------------------------------- *)
  18
  19 let fst3 (x,_,_) = x;;
  20 let snd3 (_,x,_) = x;;
  21 let thd3 (_,_,x) = x;;
  22
  23
  24 (*----------------------------------------------------------------------------*)
  25 (* num_list : a' list -> (a' * int) list                                      *)
  26 (*                                                                            *)
  27 (* Numbers a list of elements,                                                *)
  28 (* e.g. [`a`;`b`;`c`] ---> [(0,`a`);(1,`b`);(2,`c`)].                         *)
  29 (*----------------------------------------------------------------------------*)
  30
  31 let num_list l =
  32    let rec number_list' n l =
  33       if ( l = [] ) then []
  34       else (n,hd l)::(number_list' (n + 1) (tl l))
  35    in number_list' 0 l;;
  36
  37
  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 (* ------------------------------------------------------------------------- *)
  43
  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);;
  47
  48
  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 (* ------------------------------------------------------------------------- *)
  54
  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!";;
  59
  60
  61 (* ------------------------------------------------------------------------- *)
  62 (* thm_mk_primed_vars: term list -> thm -> thm                               *)
  63 (* Renames all free variables in a theorem to avoid specified and constant   *)
  64 (* names.                                                                    *)
  65 (* ------------------------------------------------------------------------- *)
  66
  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
  71   INST insts thm;;
  72
  73
  74 (* ------------------------------------------------------------------------- *)
  75 (* gl_frees: goal -> term list                                               *)
  76 (* Finds the free variables in a subgoal (assumptions and goal).             *)
  77 (* ------------------------------------------------------------------------- *)
  78
  79 let gl_frees : goal -> term list =
  80   fun (asl,w) -> itlist (union o thm_frees o snd) asl (frees w);;
  81
  82
  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 (* ------------------------------------------------------------------------- *)
  91
  92 let ADD_HYP hyp_thm thm = CONJUNCT2 (CONJ hyp_thm thm);;
  93
  94
  95 (* ------------------------------------------------------------------------- *)
  96 (* DISCHL: term list -> thm -> thm                                           *)
  97 (* Applies DISCH for several terms.                                          *)
  98 (* ------------------------------------------------------------------------- *)
  99
 100 let rec (DISCHL: term list -> thm -> thm) =
 101   fun tms thm ->
 102     if (tms = []) then thm
 103         else DISCH (hd tms) (DISCHL (tl tms) thm);;
 104
 105
 106 (* ------------------------------------------------------------------------- *)
 107 (* print_thl:                                                                *)
 108 (* Print a list of theorems (for debugging).                                 *)
 109 (* ------------------------------------------------------------------------- *)
 110
 111 let print_thl thl =
 112   map (fun thm -> ( print_thm thm ; print_newline ())) thl;;
 113
 114
 115 (* ------------------------------------------------------------------------- *)
 116 (* print_tml:                                                                *)
 117 (* Print a list of terms (for debugging).                                    *)
 118 (* ------------------------------------------------------------------------- *)
 119
 120 let print_tml tml =
 121     map (fun tm -> ( print_term tm ; print_newline ())) tml;;
 122
 123
 124 (* ------------------------------------------------------------------------- *)
 125 (* print_varandtype, show_types, hide_types:                                 *)
 126 (* Prints the type after each variable.  Useful for "debugging" type issues. *)
 127 (* ------------------------------------------------------------------------- *)
 128 (* Source:                                                                   *)
 129 (* http://code.google.com/p/flyspeck/wiki/TipsAndTricks#Investigating_Types  *)
 130 (* ------------------------------------------------------------------------- *)
 131
 132 let print_varandtype fmt tm =
 133   let hop,args = strip_comb tm in
 134   let s = name_of hop
 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 ")")
 142   else fail() ;;
 143
 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."));;
 149
 150
 151 (* ------------------------------------------------------------------------- *)
 152 (* count_goals : unit -> int                                                 *)
 153 (* Shortcut to count the subgoals in the current goalstate.                  *)
 154 (* ------------------------------------------------------------------------- *)
 155
 156 let count_goals () =
 157   if (!current_goalstack = []) then 0 else
 158   ( let _,gls,_ = hd !current_goalstack in length gls );;
 159
 160
 161
 162 (* ------------------------------------------------------------------------- *)
 163 (* top_asms : goalstack -> (string * thm) list                               *)
 164 (* Shortcut to get the assumption list of the top goal of a given goalstack. *)
 165 (* ------------------------------------------------------------------------- *)
 166
 167 let top_asms (gs:goalstack) = (fst o hd o snd3 o hd) gs;;
 168
 169
 170 (* ------------------------------------------------------------------------- *)
 171 (* top_metas : goalstack -> term list                                        *)
 172 (* Returns the list of metavariables in the current goalstate.               *)
 173 (* ------------------------------------------------------------------------- *)
 174
 175 let top_metas (gs:goalstack) = (fst o fst3 o hd) gs;;
 176
 177
 178 (* ------------------------------------------------------------------------- *)
 179 (* top_inst : goalstack -> instantiation                                     *)
 180 (* Returns the metavariable instantiations in the current goalstate.         *)
 181 (* ------------------------------------------------------------------------- *)
 182
 183 let top_inst (gs:goalstack) = (snd o fst3 o hd) gs;;
 184
 185
 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 (* ------------------------------------------------------------------------- *)
 196
 197 let (print_goalstack_all:goalstack->unit) =
 198   let print_goalstate k gs =
 199     let ((mvs,_),gl,_) = gs in
 200     let n = length gl 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 ;
 206                      print_string "`;" in
 207     print_string s; print_newline();
 208     if (length mvs > 0) then (
 209       print_string "Metas:" ; let _ = map print_mv mvs in () ; print_newline()
 210     ) ;
 211     if gl = [] then () else
 212     do_list (print_goal o C el gl) (rev(0--(k-1))) in
 213   fun l ->
 214     if l = [] then print_string "Empty goalstack"
 215     else
 216       let (_,gl,_ as gs) = hd l in
 217       print_goalstate (length gl) gs;;
 218
 219
 220 (* ------------------------------------------------------------------------- *)
 221 (* print_goalstack :                                                         *)
 222 (* Upgrade to print_goalstack that also prints a list of metavariables with  *)
 223 (* their types.                                                              *)
 224 (* ------------------------------------------------------------------------- *)
 225
 226 let (print_goalstack:goalstack->unit) =
 227   let print_goalstate k gs =
 228     let ((mvs,_),gl,_) = gs in
 229     let n = length gl 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 ;
 235                      print_string "`;" in
 236     print_string s; print_newline();
 237     if (length mvs > 0) then (
 238       print_string "Metas:" ; let _ = map print_mv mvs in () ; print_newline()
 239     ) ;
 240     if gl = [] then () else
 241     do_list (print_goal o C el gl) (rev(0--(k-1))) in
 242   fun l ->
 243     if l = [] then print_string "Empty goalstack"
 244     else if tl l = [] then
 245       let (_,gl,_ as gs) = hd l in
 246       print_goalstate 1 gs
 247     else
 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;;
 253
 254 #install_printer print_goalstack;;
 255
 256
 257