Update from HH
[Emf193/.git] / 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