IsabelleLight/new_tactics.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-2010                                 *)
   9 (* ========================================================================= *)
  10 (* FILE         : new_tactics.ml                                             *)
  11 (* DESCRIPTION  : Various tactics to facilitate procedural-style users.      *)
  12 (*                Mostly inspired by Isabelle's similar tactics.             *)
  13 (* LAST MODIFIED: October 2012                                               *)
  14 (* ========================================================================= *)
  15
  16 (* ------------------------------------------------------------------------- *)
  17 (* e_all : tactic -> goalstack                                               *)
  18 (* Same as "e" but applies tactic to ALL subgoals.                           *)
  19 (* ------------------------------------------------------------------------- *)
  20
  21 let e_all tac =
  22   let c = (count_goals()) in
  23   let rec f i = (
  24     if (i = 0)
  25     then (!current_goalstack)
  26     else let _ = e tac in let _ = r 1 in f (i-1)
  27    ) in f c;;
  28
  29
  30 (* ------------------------------------------------------------------------- *)
  31 (* ROTATE_N_TAC:                                                             *)
  32 (* Rotates assumptions N times.                                              *)
  33 (* ------------------------------------------------------------------------- *)
  34 (* Pops the entire assumption list doing nothing (K ALL_TAC) then maps       *)
  35 (* LABEL_TAC to the rotated list of assumptions. The list is reversed so as  *)
  36 (* to match the external order. The result is applied to (asl,w) so as to    *)
  37 (* obtain the resulting goalstate as required by the tactic type.            *)
  38 (* ------------------------------------------------------------------------- *)
  39
  40 let (ROTATE_N_TAC :int->tactic) =
  41   fun n (asl,w) ->
  42     let rotateasm = fun (asl) -> (tl asl)@[hd asl] in
  43     (POP_ASSUM_LIST(K ALL_TAC) THEN
  44        MAP_EVERY (fun (s,th) -> LABEL_TAC s th) (funpow n rotateasm (rev asl)))
  45       (asl,w);;
  46
  47
  48 (* ------------------------------------------------------------------------- *)
  49 (* ROTATE_TAC:                                                               *)
  50 (* Rotates assumptions once.                                                 *)
  51 (* ------------------------------------------------------------------------- *)
  52
  53 let (ROTATE_TAC :tactic) = (ROTATE_N_TAC 1);;
  54
  55
  56
  57 (* ------------------------------------------------------------------------- *)
  58 (* DRULE_N_TAC:                                                              *)
  59 (* Applies an inference rule to Nth assumption only.                         *)
  60 (* Like drule for HOL Light's inference rules without matching.              *)
  61 (* ------------------------------------------------------------------------- *)
  62 (* Works like RULE_ASSUM_TAC except it numbers the assumption list with      *)
  63 (* num_list and only applies the rule to the Nth assumption.                 *)
  64 (* ------------------------------------------------------------------------- *)
  65
  66 let (DRULE_N_TAC :int->(thm->thm)->tactic) =
  67   fun n rule (asl,w) -> (POP_ASSUM_LIST(K ALL_TAC) THEN
  68                            MAP_EVERY (fun (i,(s,th)) -> LABEL_TAC s (if (i=n) then (rule th) else th))
  69                            (num_list(rev asl))) (asl,w);;
  70
  71
  72
  73 (* ------------------------------------------------------------------------- *)
  74 (* FRULE_N_TAC:                                                              *)
  75 (* Applies an inference rule to Nth assumption only then adds the result as  *)
  76 (* a new assumption.                                                         *)
  77 (* Like frule for HOL Light's inference rules without matching.              *)
  78 (* ------------------------------------------------------------------------- *)
  79 (* Works like DRULE_N_TAC except it leaves the assumption intact and         *)
  80 (* adds the result as a new assumption.                                      *)
  81 (* ------------------------------------------------------------------------- *)
  82
  83 let (FRULE_N_TAC :int->(thm->thm)->tactic) =
  84   fun n rule (asl,w) -> (
  85     let asmlist = num_list(rev asl) in
  86     let (_,asm_n) = try assoc n asmlist with Failure _ ->
  87       failwith("FRULE_N_TAC: didn't find assumption "^string_of_int(n)) in
  88     ASSUME_TAC (rule asm_n)) (asl,w);;
  89
  90
  91
  92 (* ------------------------------------------------------------------------- *)
  93 (* FRULE_MN_TAC:                                                       *)
  94 (* Applies an inference rule (such as MP) to the Mth and Nth assumptions and *)
  95 (* adds the result as a new assumption.                                      *)
  96 (* ------------------------------------------------------------------------- *)
  97 (* Numbers the assumption list, finds the Mth and Nth assumptions, applies   *)
  98 (* the rule to them and adds the result as a new assumption.                 *)
  99 (* ------------------------------------------------------------------------- *)
 100
 101 let (FRULE_MN_TAC :int->int->(thm->thm->thm)->tactic) =
 102 fun  m n rule (asl,w) -> (
 103   let asmlist = num_list(rev asl) in
 104   let (_,asm_m) = try assoc m asmlist with Failure _ ->
 105     failwith("FRULE_MN_TAC: didn't find assumption "^string_of_int(m)) in
 106   let (_,asm_n) = try assoc n asmlist with Failure _ ->
 107     failwith("FRULE_MN_TAC: didn't find assumption "^string_of_int(n)) in
 108   ASSUME_TAC (rule asm_m asm_n)) (asl,w);;
 109
 110
 111
 112
 113 (* ------------------------------------------------------------------------- *)
 114 (* ----------------------- SIMP TACTICS START HERE!! ----------------------- *)
 115 (* ------------------------------------------------------------------------- *)
 116
 117 (* ------------------------------------------------------------------------- *)
 118 (* GENERAL_ASM_TAC: (thm list -> thm -> thm) -> thm list -> tactic           *)
 119 (* General function that uses a rewrite rule to rewrite the assumptions.     *)
 120 (* Each assumption is rewritten using the rest of the assumptions and the    *)
 121 (* given list of theorems.                                                   *)
 122 (* ------------------------------------------------------------------------- *)
 123 (* A filter is applied to ensure that the assumption is not used to rewrite  *)
 124 (* itself.                                                                   *)
 125 (* ------------------------------------------------------------------------- *)
 126
 127 let GENERAL_ASM_TAC = fun rule thl (asl,w) ->
 128   let asm = map snd asl in
 129   (POP_ASSUM_LIST(K ALL_TAC) THEN
 130      MAP_EVERY (fun (s,th) -> LABEL_TAC s
 131          (rule ((filter (fun x -> not (th = x)) asm) @ thl) th)
 132                ) (rev asl)) (asl,w);;
 133
 134 (* ------------------------------------------------------------------------- *)
 135 (* Using the above GENERAL_ASSUM_TAC, we define 4 tactics to rewrite         *)
 136 (* assumptions based on the 4 rewrite rules available in HOL Light.          *)
 137 (* ------------------------------------------------------------------------- *)
 138
 139 let REWRITE_ASM_TAC,ONCE_REWRITE_ASM_TAC,PURE_REWRITE_ASM_TAC,
 140   PURE_ONCE_REWRITE_ASM_TAC =
 141   GENERAL_ASM_TAC REWRITE_RULE,
 142   GENERAL_ASM_TAC ONCE_REWRITE_RULE,
 143   GENERAL_ASM_TAC PURE_REWRITE_RULE,
 144   GENERAL_ASM_TAC PURE_ONCE_REWRITE_RULE;;
 145
 146 (* ------------------------------------------------------------------------- *)
 147 (* And for simplification.                                                   *)
 148 (* ------------------------------------------------------------------------- *)
 149
 150 let SIMP_ASM_TAC,ONCE_SIMP_ASM_TAC,PURE_SIMP_ASM_TAC =
 151   GENERAL_ASM_TAC SIMP_RULE,
 152   GENERAL_ASM_TAC ONCE_SIMP_RULE,
 153   GENERAL_ASM_TAC PURE_SIMP_RULE;;
 154
 155 (* ------------------------------------------------------------------------- *)
 156 (* FULL_REWRITE_TAC : thm list -> tactic                                     *)
 157 (* simp             : thm list -> tactic                                     *)
 158 (* Similar to Isabelle's simp. Rewrites assumptions then rewrites goal       *)
 159 (* using the assumptions.                                                    *)
 160 (* ------------------------------------------------------------------------- *)
 161
 162 let FULL_REWRITE_TAC thl =
 163   REWRITE_ASM_TAC thl THEN ASM_SIMP_TAC thl;;
 164
 165 let simp = FULL_REWRITE_TAC;;
 166
 167 (* ------------------------------------------------------------------------- *)
 168 (* FULL_SIMP_TAC : thm list -> tactic                                        *)
 169 (* Hybrid simplifier. Uses HOL Light's SIMP_TAC then FULL_REWRITE_TAC.       *)
 170 (* ------------------------------------------------------------------------- *)
 171
 172 let FULL_SIMP_TAC thl =
 173   SIMP_TAC thl THEN REWRITE_ASM_TAC thl THEN ASM_REWRITE_TAC thl;;
 174
 175
 176
 177 (* ------------------------------------------------------------------------- *)
 178 (* assumption (tactic):                                                      *)
 179 (* Shortcut to match an assumption to the goal as Isabelle's "assumption".   *)
 180 (* ------------------------------------------------------------------------- *)
 181
 182 let assumption = FIRST_ASSUM MATCH_ACCEPT_TAC;;
 183
 184
 185 (* ------------------------------------------------------------------------- *)
 186 (* ALL_UNIFY_ACCEPT_TAC (term list -> thm -> tactic):                        *)
 187 (* Altered UNIFY_ACCEPT_TAC. Uses INSTANTIATE_ALL instead of INSTANTIATE.    *)
 188 (* ------------------------------------------------------------------------- *)
 189 (* This allows for some valid instantiations that weren't otherwise allowed. *)
 190 (* eg After using allE, the `a` metavariable can't be instantiated otherwise.*)
 191 (* ------------------------------------------------------------------------- *)
 192
 193 let ALL_UNIFY_ACCEPT_TAC mvs th (asl,w) =
 194   let insts = term_unify mvs (concl th) w in
 195   ([],insts),[],
 196   let th' = INSTANTIATE_ALL insts th in
 197   fun i [] -> INSTANTIATE_ALL i th';;
 198
 199
 200
 201 (* ------------------------------------------------------------------------- *)
 202 (* meta_assumption (term list -> tactic):                                    *)
 203 (* Shortcut to match an assumption to the goal as Isabelle's "assumption".   *)
 204 (* This version also tries unification by instantiation of meta-variables    *)
 205 (* which, unfortunately, need to be given manually in a list.                *)
 206 (* ------------------------------------------------------------------------- *)
 207 (* Invalid instantiations may be produced.                                   *)
 208 (* eg g `!x:num. (?a:num. R a x) ==> (?y. R y x)`;;                          *)
 209 (*    e GEN_TAC;;                                                            *)
 210 (*    e (rule impI);;                                                        *)
 211 (*    e (rule exI);;                                                         *)
 212 (*    e (FIRST_X_ASSUM (X_CHOOSE_TAC `b:num`));;                             *)
 213 (*    e (meta_assumption [`a:num`]);;                                        *)
 214 (* This succeeds but top_thm() is unable to reconstruct the theorem.         *)
 215 (* ------------------------------------------------------------------------- *)
 216
 217 let meta_assumption mvs = (FIRST_ASSUM MATCH_ACCEPT_TAC) ORELSE
 218                       (FIRST_ASSUM (ALL_UNIFY_ACCEPT_TAC mvs));;
 219
 220
 221 (* ------------------------------------------------------------------------- *)
 222 (* Shortcut for interactive proofs so that you don't have to enumerate       *)
 223 (* metavariables.                                                            *)
 224 (* ------------------------------------------------------------------------- *)
 225
 226 let ema () = (e o meta_assumption o top_metas o p) ()  ;;
 227
 228
 229 (* ------------------------------------------------------------------------- *)
 230 (* X_MATCH_CHOOSE_TAC : (term -> tactic)                                     *)
 231 (* Version of X_CHOOSE_TAC with type matching.                               *)
 232 (* ------------------------------------------------------------------------- *)
 233 (* If the variable given as an argument has a vartype then its type is       *)
 234 (* instantiated to the type of the existentially quantified variable.        *)
 235 (* Usefull so that the user need not specify the type for his variable.      *)
 236 (* It is still acceptable if the user does specify it.                       *)
 237 (* ------------------------------------------------------------------------- *)
 238
 239 let (X_MATCH_CHOOSE_TAC: term -> thm_tactic) =
 240   fun x' xth ->
 241     try let xtm = concl xth in
 242         let x,bod = dest_exists xtm in
 243         let x'type = type_of x' in
 244         let x'' = if (is_vartype x'type) then
 245           inst (type_match x'type (type_of x) []) x'
 246         else x' in
 247         let pat = vsubst[x'',x] bod in
 248         let xth' = ASSUME pat in
 249         fun (asl,w) ->
 250           let avoids = itlist (union o frees o concl o snd) asl
 251                               (union (frees w) (thm_frees xth)) in
 252           if mem x' avoids then failwith "X_CHOOSE_TAC" else
 253           null_meta,[("",xth')::asl,w],
 254           fun i [th] -> CHOOSE(x'',INSTANTIATE_ALL i xth) th
 255     with Failure _ -> failwith "X_CHOOSE_TAC";;
 256
 257
 258
 259
 260 (* ------------------------------------------------------------------------- *)
 261 (* exE : (term -> tactic)                                                    *)
 262 (* Existential elimination tactic (since we are unable to accommodate        *)
 263 (* erule exE with the current meta_rule system because of lack of meta-level *)
 264 (* quantification).                                                          *)
 265 (* ------------------------------------------------------------------------- *)
 266
 267 let exE = FIRST_X_ASSUM o X_MATCH_CHOOSE_TAC;;
 268
 269
 270 (* ------------------------------------------------------------------------- *)
 271 (* allI : (term -> tactic)                                                   *)
 272 (* Universal introduction tactic (since we are unable to accommodate         *)
 273 (* rule allI with the current meta_rule system because of lack of meta-level *)
 274 (* quantification).                                                          *)
 275 (* ------------------------------------------------------------------------- *)
 276 (* (+) We can use X_GEN_TAC to allow the user to give his own term, but      *)
 277 (* this is rarely useful in procedural style proofs.                         *)
 278 (* ------------------------------------------------------------------------- *)
 279
 280 let allI = GEN_TAC;;
 281
 282
 283 (* ------------------------------------------------------------------------- *)
 284 (* qed : (unit -> thm)                                                       *)
 285 (* Reconstructs the theorem at the end of an interactive proof.              *)
 286 (* May fail if an incorrect metavariable instantiation has occured during the*)
 287 (* proof.                                                                    *)
 288 (* ------------------------------------------------------------------------- *)
 289 (* (+) There are plans to upgrade this for better accommodation of proofs    *)
 290 (* containing meta-level implication (see meta_rules.ml and gmm).            *)
 291 (* ------------------------------------------------------------------------- *)
 292
 293 let qed = top_thm;;
 294
 295
 296 (* ------------------------------------------------------------------------- *)
 297 (* ASM_STRUCT_CASES_TAC : (thm_tactic)                                       *)
 298 (* Replacement/fix of STRUCT_CASES_TAC where each case is added as an        *)
 299 (* assumption like ASM_CASES_TAC does for booleans.                          *)
 300 (* ------------------------------------------------------------------------- *)
 301
 302 let ASM_STRUCT_CASES_TAC =
 303     REPEAT_TCL STRIP_THM_THEN ASSUME_TAC;;
 304
 305 (* ------------------------------------------------------------------------- *)
 306 (* case_tac : (term -> tactic)                                               *)
 307 (* Isabelle's case_tac for splitting cases.                                  *)
 308 (* ------------------------------------------------------------------------- *)
 309
 310 let (case_tac:term->tactic) =
 311   fun tm ((_,w) as g) ->
 312     let trymatch = fun tm1 tm2 ->
 313       try ( let inst = term_match (gl_frees g) tm1 tm2 in
 314             if (is_var tm1)
 315             then match inst with
 316                 [],[],_ -> true
 317               | _  -> false
 318             else true )
 319       with Failure _ -> false in
 320     let tm' = try (find_term (trymatch tm) w)
 321       with Failure _ -> tm in
 322     let ty = (fst o dest_type o type_of) tm' in
 323     let thm = try (cases ty)
 324       with Failure _ -> failwith ("case_tac: Failed to find cases theorem for type \"" ^ ty ^ "\".") in
 325     ASM_STRUCT_CASES_TAC (ISPEC tm' thm) g;;
 326
 327
 328 (* ------------------------------------------------------------------------- *)
 329 (* gen_case_tac : tactic                                                     *)
 330 (* Case split on the leading universal quantifier of the goal.               *)
 331 (* ------------------------------------------------------------------------- *)
 332
 333 let (gen_case_tac:tactic) =
 334   fun ((_,w) as g) ->
 335     case_tac ((fst o dest_forall) w) g;;
 336
 337
 338 (* ------------------------------------------------------------------------- *)
 339 (* subgoal_tac : (term -> tactic)                                            *)
 340 (* Introduces a new subgoal which gets added as an assumption.               *)
 341 (* Isabelle's subgoal_tac.                                                   *)
 342 (* ------------------------------------------------------------------------- *)
 343
 344 let subgoal_tac = fun tm -> SUBGOAL_THEN tm ASSUME_TAC;;
 345
 346
 347 (* ------------------------------------------------------------------------- *)
 348 (* meson : (thm list -> tactic)                                              *)
 349 (* Lower-case shortcut for ASM_MESON_TAC                                     *)
 350 (* ------------------------------------------------------------------------- *)
 351
 352 let meson = ASM_MESON_TAC;;
 353