tacticlib.ml

   1 (* ========================================================================= *)\r
   2 (*               Formalization of Electromagnetic Optics                     *)\r
   3 (*                                                                           *)\r
   4 (*            (c) Copyright, Sanaz Khan Afshar & Vincent Aravantinos 2011-14 *)\r
   5 (*                           Hardware Verification Group,                    *)\r
   6 (*                           Concordia University                            *)\r
   7 (*                                                                           *)\r
   8 (*                Contact:   <s_khanaf@encs.concordia.ca>                    *)\r
   9 (*                           <vincent@encs.concordia.ca>                     *)\r
  10 (*                                                                           *)\r
  11 (* This file deals with various utilities.                                   *)\r
  12 (* ========================================================================= *)\r
  13 \r
  14 Format.set_margin 154;;\r
  15 \r
  16 let CHANGED_RULE r thm =\r
  17   let thm' = r thm in\r
  18   if equals_thm thm thm' then failwith "CHANGED_RULE" else thm';;\r
  19 let MAP_ASSUMPTIONS f = REPEAT (POP_ASSUM (MP_TAC o f)) THEN REPEAT DISCH_TAC;;\r
  20 let REMOVE_LETS =\r
  21   REPEAT LET_TAC THEN MAP_ASSUMPTIONS (repeat (CONV_RULE let_CONV));;\r
  22 let REWRITE_ASSUMPTIONS xs = MAP_ASSUMPTIONS (REWRITE_RULE xs);;\r
  23 let REWRITE_EVERYWHERE xs =\r
  24   REWRITE_TAC xs THEN MAP_ASSUMPTIONS (REWRITE_RULE xs);;\r
  25 let ON_FIRST_GOAL ?(out_of=2) x =\r
  26   let rec ( * ) n x = if n<=1 then [] else x :: (n-1) * x in\r
  27   x :: out_of * ALL_TAC;;\r
  28 let STRIP_ASSUMPTIONS = REPEAT (POP_ASSUM MP_TAC) THEN REPEAT STRIP_TAC;;\r
  29 let DESTRUCT_PAIR_TAC p =\r
  30   CHOOSE_THEN (CHOOSE_THEN (fun x -> PURE_REWRITE_TAC[x]))\r
  31     (ISPEC p PAIR_SURJECTIVE);;\r
  32 let MAP_ANTECEDENT f = DISCH_THEN (MP_TAC o f);;\r
  33 \r
  34 let exn_to_bool f x = try ignore (f x); true with _ -> false;;\r
  35 \r
  36 let strip_parentheses s =\r
  37   if s.[0] = '(' && s.[String.length s-1] = ')'\r
  38   then String.sub s 1 (String.length s-2)\r
  39   else s;;\r
  40 let contains_sub_term_name name t =\r
  41   exn_to_bool (find_term (fun x -> ((=) name o strip_parentheses o\r
  42     string_of_term) x)) t;;\r
  43 \r
  44 let REAL_SIMP_TAC thms =\r
  45         ASM_REWRITE_TAC ([REAL_MUL_LZERO;REAL_MUL_RZERO;REAL_MUL_RID;REAL_MUL_LID;\r
  46     REAL_ADD_LID;REAL_ADD_RID;REAL_SUB_RZERO;REAL_NEG_0] @ thms);;\r
  47 let COMPLEX_SIMPLIFY_TAC =\r
  48   ASM_REWRITE_TAC[COMPLEX_ADD_LID;COMPLEX_MUL_LID;COMPLEX_MUL_LZERO;\r
  49     COMPLEX_MUL_RZERO;COMPLEX_SUB_LZERO;COMPLEX_SUB_RZERO;COMPLEX_NEG_0 ];; \r
  50 \r
  51 let try_or_id f x = try f x with _ -> x;;\r
  52 \r
  53 let SINGLE f x = f [x];;\r
  54 let ASSUME_CONSEQUENCES x =\r
  55   ASM (MAP_EVERY (fun y -> try ASSUME_TAC (MATCH_MP x y) with _ -> ALL_TAC))\r
  56     [];;\r
  57 let STRIP_RULE =\r
  58   repeat (CHANGED_RULE UNDISCH_ALL o try_or_id SPEC_ALL)\r
  59     o REWRITE_RULE[IMP_CONJ];;\r
  60 \r
  61 let CSQS xs x = map (try_or_id (MATCH_MP x)) xs;; \r
  62 let CSQS_THEN xs x ttac = MAP_EVERY ttac (CSQS xs x);;\r
  63 let ASM_CSQS_THEN x = ASSUM_LIST o C (C CSQS_THEN x);;\r
  64 \r
  65 let ASM_CSQ_THEN ?(remove=false) ?(match_=true) x ttac =\r
  66   (if remove then FIRST_X_ASSUM else FIRST_ASSUM)\r
  67     (ttac o (if match_ then MATCH_MP else MP) x);;\r
  68 \r
  69 let ASM_CSQS_THEN x ttac =\r
  70   (* looks absurd, eh? But needed in order to control the execution flow *)\r
  71   let ttac x y = ttac x y in \r
  72   REPEAT_TCL (fun y z -> ASM_CSQ_THEN z y ORELSE ttac z) ttac x;;\r
  73 \r
  74 let LET_SIMP_TAC = REWRITE_TAC[LET_DEF;LET_END_DEF];;\r
  75 \r
  76 let distrib fs x = map (fun f -> f x) fs;;\r
  77 \r
  78 let DISTRIB ttacs x = EVERY (distrib ttacs x);;\r
  79 let LET_DEFs = CONJ LET_DEF LET_END_DEF;;\r
  80 \r
  81 let GEQ_IMP x = GEN_ALL (MATCH_MP EQ_IMP (SPEC_ALL x));;\r