1 (* ========================================================================= *)
\r
2 (* Formalization of Electromagnetic Optics *)
\r
4 (* (c) Copyright, Sanaz Khan Afshar & Vincent Aravantinos 2011-14 *)
\r
5 (* Hardware Verification Group, *)
\r
6 (* Concordia University *)
\r
8 (* Contact: <s_khanaf@encs.concordia.ca> *)
\r
9 (* <vincent@encs.concordia.ca> *)
\r
11 (* This file deals with various utilities. *)
\r
12 (* ========================================================================= *)
\r
14 Format.set_margin 154;;
\r
16 let CHANGED_RULE r thm =
\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
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
34 let exn_to_bool f x = try ignore (f x); true with _ -> false;;
\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
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
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
51 let try_or_id f x = try f x with _ -> x;;
\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
58 repeat (CHANGED_RULE UNDISCH_ALL o try_or_id SPEC_ALL)
\r
59 o REWRITE_RULE[IMP_CONJ];;
\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
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
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
74 let LET_SIMP_TAC = REWRITE_TAC[LET_DEF;LET_END_DEF];;
\r
76 let distrib fs x = map (fun f -> f x) fs;;
\r
78 let DISTRIB ttacs x = EVERY (distrib ttacs x);;
\r
79 let LET_DEFs = CONJ LET_DEF LET_END_DEF;;
\r
81 let GEQ_IMP x = GEN_ALL (MATCH_MP EQ_IMP (SPEC_ALL x));;
\r