Boyer_Moore/support.ml

   1 (******************************************************************************)
   2 (* FILE          : support.ml                                                 *)
   3 (* DESCRIPTION   : Miscellaneous supporting definitions for Boyer-Moore       *)
   4 (*                 style prover in HOL.                                       *)
   5 (*                                                                            *)
   6 (* READS FILES   : <none>                                                     *)
   7 (* WRITES FILES  : <none>                                                     *)
   8 (*                                                                            *)
   9 (* AUTHOR        : R.J.Boulton                                                *)
  10 (* DATE          : 6th June 1991                                              *)
  11 (*                                                                            *)
  12 (* LAST MODIFIED : R.J.Boulton                                                *)
  13 (* DATE          : 21st June 1991                                             *)
  14 (*                                                                            *)
  15 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh)                *)
  16 (* DATE          : 2008                                                       *)
  17 (******************************************************************************)
  18
  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;;
  30
  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);;
  36
  37 let CONTRAPOS =
  38   let a = `a:bool` and b = `b:bool` in
  39   let pth = ITAUT `(a ==> b) ==> (~b ==> ~a)` in
  40   fun th ->
  41     try let P,Q = dest_imp(concl th) in
  42         MP (INST [P,a; Q,b] pth) th
  43     with Failure _ -> failwith "CONTRAPOS";;
  44
  45 let NOT_EQ_SYM =
  46   let pth = GENL [`a:A`; `b:A`]
  47     (CONTRAPOS(DISCH_ALL(SYM(ASSUME`a:A = b`))))
  48   and aty = `:A` in
  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";;
  52
  53
  54 let hash f g (x,y) = (f x,g y);;
  55 let hashI f (x,y) = hash f I (x,y);;
  56
  57 let fst3 (x,_,_) = x;;
  58 let snd3 (_,x,_) = x;;
  59 let thd3 (_,_,x) = x;;
  60
  61 let lcombinep (x,y) = List.combine x y;;
  62 let lcount x l = length ( filter ((=) x) l );;
  63
  64
  65 let list_mk_imp (tms,tm) =
  66      if (tms = []) then tm
  67      else try itlist (fun p q -> mk_imp (p,q)) tms tm with Failure _ -> failwith "list_mk_imp";;
  68
  69 let INDUCT_TAC_ thm = MATCH_MP_TAC thm THEN
  70   CONJ_TAC THENL [ALL_TAC; GEN_TAC THEN GEN_TAC THEN DISCH_TAC] ;;
  71
  72 (*--------------------------------------------------------------------------*)
  73 (* distinct : ''a list -> bool                                              *)
  74 (*                                                                          *)
  75 (* Checks whether the elements of a list are all distinct.                  *)
  76 (*--------------------------------------------------------------------------*)
  77
  78 let rec distinct x =
  79      if (x = []) then true
  80      else not (mem (hd x) (tl x)) & distinct (tl x);;
  81
  82
  83 (*----------------------------------------------------------------------------*)
  84 (* Discriminator functions for T (true) and F (false)                         *)
  85 (*----------------------------------------------------------------------------*)
  86
  87 let is_T = let T = `T` in fun tm -> tm = T
  88 and is_F = let F = `F` in fun tm -> tm = F;;
  89
  90 (*--------------------------------------------------------------------------*)
  91 (* conj_list : term -> term list                                            *)
  92 (*                                                                          *)
  93 (* Splits a conjunction into conjuncts. Only recursively splits the right   *)
  94 (* conjunct.                                                                *)
  95 (*--------------------------------------------------------------------------*)
  96
  97 let rec conj_list tm =
  98    try(
  99    let (tm1,tm2) = dest_conj tm
 100    in  tm1::(conj_list tm2)
 101    ) with Failure _ -> [tm];;
 102
 103 (*--------------------------------------------------------------------------*)
 104 (* disj_list : term -> term list                                            *)
 105 (*                                                                          *)
 106 (* Splits a disjunction into disjuncts. Only recursively splits the right   *)
 107 (* disjunct.                                                                *)
 108 (*--------------------------------------------------------------------------*)
 109
 110 let rec disj_list tm =
 111    try(
 112    let (tm1,tm2) = dest_disj tm
 113    in  tm1::(disj_list tm2)
 114   ) with Failure _ -> [tm];;
 115
 116 (*----------------------------------------------------------------------------*)
 117 (* number_list : * list -> ( * # int) list                                     *)
 118 (*                                                                            *)
 119 (* Numbers a list of elements,                                                *)
 120 (* e.g. [`a`;`b`;`c`] ---> [(`a`,1);(`b`,2);(`c`,3)].                         *)
 121 (*----------------------------------------------------------------------------*)
 122
 123 let number_list l =
 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;;
 128
 129 (*----------------------------------------------------------------------------*)
 130 (* insert_on_snd : ( * # int) -> ( * # int) list -> ( * # int) list              *)
 131 (*                                                                            *)
 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 (*----------------------------------------------------------------------------*)
 136
 137 let rec insert_on_snd (x,n) l =
 138    if (l = [])
 139    then [(x,n)]
 140    else let h = hd l
 141         in  if (n < snd h)
 142             then (x,n)::l
 143             else h::(insert_on_snd (x,n) (tl l));;
 144
 145 (*----------------------------------------------------------------------------*)
 146 (* sort_on_snd : ( * # int) list -> ( * # int) list                             *)
 147 (*                                                                            *)
 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 (*----------------------------------------------------------------------------*)
 152
 153 let rec sort_on_snd l =
 154    if (l = [])
 155    then []
 156    else (insert_on_snd (hd l) (sort_on_snd (tl l)));;
 157
 158 (*----------------------------------------------------------------------------*)
 159 (* conj_list : term -> term list                                              *)
 160 (*                                                                            *)
 161 (* Splits a conjunction into conjuncts. Only recursively splits the right     *)
 162 (* conjunct.                                                                  *)
 163 (*----------------------------------------------------------------------------*)
 164
 165 let rec conj_list tm =
 166    try
 167       (let (tm1,tm2) = dest_conj tm
 168        in  tm1::(conj_list tm2))
 169    with Failure _ -> [tm];;
 170
 171 (*----------------------------------------------------------------------------*)
 172 (* disj_list : term -> term list                                              *)
 173 (*                                                                            *)
 174 (* Splits a disjunction into disjuncts. Only recursively splits the right     *)
 175 (* disjunct.                                                                  *)
 176 (*----------------------------------------------------------------------------*)
 177
 178 let rec disj_list tm =
 179    try
 180       (let (tm1,tm2) = dest_disj tm
 181        in  tm1::(disj_list tm2))
 182    with Failure _ -> [tm];;
 183
 184 (*----------------------------------------------------------------------------*)
 185 (* find_bm_terms : (term -> bool) -> term -> term list                        *)
 186 (*                                                                            *)
 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 (*----------------------------------------------------------------------------*)
 192
 193 let find_bm_terms p tm =
 194  try
 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' ) )
 199       in accum [] p tm
 200  ) with Failure _ -> failwith "find_bm_terms";;
 201
 202 (*----------------------------------------------------------------------------*)
 203 (* remove_el : int -> * list -> ( * # * list)                                 *)
 204 (*                                                                            *)
 205 (* Removes a specified (by numerical position) element from a list.           *)
 206 (*----------------------------------------------------------------------------*)
 207
 208 let rec remove_el n l =
 209    if ((l = []) or (n < 1))
 210    then failwith "remove_el"
 211    else if (n = 1)
 212         then (hd l,tl l)
 213         else let (x,l') = remove_el (n - 1) (tl l)
 214              in  (x,(hd l)::l');;
 215