1 (******************************************************************************)
2 (* FILE : support.ml *)
3 (* DESCRIPTION : Miscellaneous supporting definitions for Boyer-Moore *)
4 (* style prover in HOL. *)
6 (* READS FILES : <none> *)
7 (* WRITES FILES : <none> *)
9 (* AUTHOR : R.J.Boulton *)
10 (* DATE : 6th June 1991 *)
12 (* LAST MODIFIED : R.J.Boulton *)
13 (* DATE : 21st June 1991 *)
15 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh) *)
17 (******************************************************************************)
19 let SUBST thl pat th =
20 let eqs,vs = unzip thl in
21 let gvs = map (genvar o type_of) vs in
22 let gpat = subst (zip gvs vs) pat in
23 let ls,rs = unzip (map (dest_eq o concl) eqs) in
24 let ths = map (ASSUME o mk_eq) (zip gvs rs) in
25 let th1 = ASSUME gpat in
26 let th2 = SUBS ths th1 in
27 let th3 = itlist DISCH (map concl ths) (DISCH gpat th2) in
28 let th4 = INST (zip ls gvs) th3 in
29 MP (rev_itlist (C MP) eqs th4) th;;
31 let SUBST_CONV thvars template tm =
32 let thms,vars = unzip thvars in
33 let gvs = map (genvar o type_of) vars in
34 let gtemplate = subst (zip gvs vars) template in
35 SUBST (zip thms gvs) (mk_eq(template,gtemplate)) (REFL tm);;
38 let a = `a:bool` and b = `b:bool` in
39 let pth = ITAUT `(a ==> b) ==> (~b ==> ~a)` in
41 try let P,Q = dest_imp(concl th) in
42 MP (INST [P,a; Q,b] pth) th
43 with Failure _ -> failwith "CONTRAPOS";;
46 let pth = GENL [`a:A`; `b:A`]
47 (CONTRAPOS(DISCH_ALL(SYM(ASSUME`a:A = b`))))
49 fun th -> try let l,r = dest_eq(dest_neg(concl th)) in
50 MP (SPECL [r; l] (INST_TYPE [type_of l,aty] pth)) th
51 with Failure _ -> failwith "NOT_EQ_SYM";;
54 let hash f g (x,y) = (f x,g y);;
55 let hashI f (x,y) = hash f I (x,y);;
57 let fst3 (x,_,_) = x;;
58 let snd3 (_,x,_) = x;;
59 let thd3 (_,_,x) = x;;
61 let lcombinep (x,y) = List.combine x y;;
62 let lcount x l = length ( filter ((=) x) l );;
65 let list_mk_imp (tms,tm) =
67 else try itlist (fun p q -> mk_imp (p,q)) tms tm with Failure _ -> failwith "list_mk_imp";;
69 let INDUCT_TAC_ thm = MATCH_MP_TAC thm THEN
70 CONJ_TAC THENL [ALL_TAC; GEN_TAC THEN GEN_TAC THEN DISCH_TAC] ;;
72 (*--------------------------------------------------------------------------*)
73 (* distinct : ''a list -> bool *)
75 (* Checks whether the elements of a list are all distinct. *)
76 (*--------------------------------------------------------------------------*)
80 else not (mem (hd x) (tl x)) & distinct (tl x);;
83 (*----------------------------------------------------------------------------*)
84 (* Discriminator functions for T (true) and F (false) *)
85 (*----------------------------------------------------------------------------*)
87 let is_T = let T = `T` in fun tm -> tm = T
88 and is_F = let F = `F` in fun tm -> tm = F;;
90 (*--------------------------------------------------------------------------*)
91 (* conj_list : term -> term list *)
93 (* Splits a conjunction into conjuncts. Only recursively splits the right *)
95 (*--------------------------------------------------------------------------*)
97 let rec conj_list tm =
99 let (tm1,tm2) = dest_conj tm
100 in tm1::(conj_list tm2)
101 ) with Failure _ -> [tm];;
103 (*--------------------------------------------------------------------------*)
104 (* disj_list : term -> term list *)
106 (* Splits a disjunction into disjuncts. Only recursively splits the right *)
108 (*--------------------------------------------------------------------------*)
110 let rec disj_list tm =
112 let (tm1,tm2) = dest_disj tm
113 in tm1::(disj_list tm2)
114 ) with Failure _ -> [tm];;
116 (*----------------------------------------------------------------------------*)
117 (* number_list : * list -> ( * # int) list *)
119 (* Numbers a list of elements, *)
120 (* e.g. [`a`;`b`;`c`] ---> [(`a`,1);(`b`,2);(`c`,3)]. *)
121 (*----------------------------------------------------------------------------*)
124 let rec number_list' n l =
125 if ( l = [] ) then []
126 else (hd l,n)::(number_list' (n + 1) (tl l))
127 in number_list' 1 l;;
129 (*----------------------------------------------------------------------------*)
130 (* insert_on_snd : ( * # int) -> ( * # int) list -> ( * # int) list *)
132 (* Insert a numbered element into an ordered list, *)
133 (* e.g. insert_on_snd (`c`,3) [(`a`,1);(`b`,2);(`d`,4)] ---> *)
134 (* [(`a`,1); (`b`,2); (`c`,3); (`d`,4)] *)
135 (*----------------------------------------------------------------------------*)
137 let rec insert_on_snd (x,n) l =
143 else h::(insert_on_snd (x,n) (tl l));;
145 (*----------------------------------------------------------------------------*)
146 (* sort_on_snd : ( * # int) list -> ( * # int) list *)
148 (* Sort a list of pairs, of which the second component is an integer, *)
149 (* e.g. sort_on_snd [(`c`,3);(`d`,4);(`a`,1);(`b`,2)] ---> *)
150 (* [(`a`,1); (`b`,2); (`c`,3); (`d`,4)] *)
151 (*----------------------------------------------------------------------------*)
153 let rec sort_on_snd l =
156 else (insert_on_snd (hd l) (sort_on_snd (tl l)));;
158 (*----------------------------------------------------------------------------*)
159 (* conj_list : term -> term list *)
161 (* Splits a conjunction into conjuncts. Only recursively splits the right *)
163 (*----------------------------------------------------------------------------*)
165 let rec conj_list tm =
167 (let (tm1,tm2) = dest_conj tm
168 in tm1::(conj_list tm2))
169 with Failure _ -> [tm];;
171 (*----------------------------------------------------------------------------*)
172 (* disj_list : term -> term list *)
174 (* Splits a disjunction into disjuncts. Only recursively splits the right *)
176 (*----------------------------------------------------------------------------*)
178 let rec disj_list tm =
180 (let (tm1,tm2) = dest_disj tm
181 in tm1::(disj_list tm2))
182 with Failure _ -> [tm];;
184 (*----------------------------------------------------------------------------*)
185 (* find_bm_terms : (term -> bool) -> term -> term list *)
187 (* Function to find all subterms in a term that satisfy a given predicate p, *)
188 (* breaking down terms as if they were Boyer-Moore logic expressions. *)
189 (* In particular, the operator of a function application is only processed if *)
190 (* it is of zero arity, i.e. there are no arguments. *)
191 (*----------------------------------------------------------------------------*)
193 let find_bm_terms p tm =
195 (let rec accum tml p tm =
196 let tml' = if (p tm) then (tm::tml) else tml
197 in ( let args = snd (strip_comb tm)
198 in ( try ( rev_itlist (fun tm tml -> accum tml p tm) args tml' ) with Failure _ -> tml' ) )
200 ) with Failure _ -> failwith "find_bm_terms";;
202 (*----------------------------------------------------------------------------*)
203 (* remove_el : int -> * list -> ( * # * list) *)
205 (* Removes a specified (by numerical position) element from a list. *)
206 (*----------------------------------------------------------------------------*)
208 let rec remove_el n l =
209 if ((l = []) or (n < 1))
210 then failwith "remove_el"
213 else let (x,l') = remove_el (n - 1) (tl l)