Boyer_Moore/struct_equal.ml

   1 (******************************************************************************)
   2 (* FILE          : struct_equal.ml                                            *)
   3 (* DESCRIPTION   : Proof procedure for simplifying an equation between two    *)
   4 (*                 data-structures of the same type.                          *)
   5 (*                                                                            *)
   6 (* READS FILES   : <none>                                                     *)
   7 (* WRITES FILES  : <none>                                                     *)
   8 (*                                                                            *)
   9 (* AUTHOR        : R.J.Boulton & T.F.Melham                                   *)
  10 (* DATE          : 4th June 1992                                              *)
  11 (*                                                                            *)
  12 (* LAST MODIFIED : R.J.Boulton                                                *)
  13 (* DATE          : 14th October 1992                                          *)
  14 (*                                                                            *)
  15 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh)                *)
  16 (* DATE          : 2008                                                       *)
  17 (******************************************************************************)
  18
  19 let subst_occs =
  20   let rec subst_occs slist tm =
  21     let applic,noway = partition (fun (i,(t,x)) -> aconv tm x) slist in
  22     let sposs = map (fun (l,z) -> let l1,l2 = partition ((=) 1) l in
  23                                   (l1,z),(l2,z)) applic in
  24     let racts,rrest = unzip sposs in
  25     let acts = filter (fun t -> not (fst t = [])) racts in
  26     let trest = map (fun (n,t) -> (map (C (-) 1) n,t)) rrest in
  27     let urest = filter (fun t -> not (fst t = [])) trest in
  28     let tlist = urest @ noway in
  29       if acts = [] then
  30       if is_comb tm then
  31         let l,r = dest_comb tm in
  32         let l',s' = subst_occs tlist l in
  33         let r',s'' = subst_occs s' r in
  34         mk_comb(l',r'),s''
  35       else if is_abs tm then
  36         let bv,bod = dest_abs tm in
  37         let gv = genvar(type_of bv) in
  38         let nbod = vsubst[gv,bv] bod in
  39         let tm',s' = subst_occs tlist nbod in
  40         alpha bv (mk_abs(gv,tm')),s'
  41       else
  42         tm,tlist
  43     else
  44       let tm' = (fun (n,(t,x)) -> subst[t,x] tm) (hd acts) in
  45       tm',tlist in
  46   fun ilist slist tm -> fst(subst_occs (zip ilist slist) tm);;
  47
  48 let GSUBS substfn ths th =
  49    let ls = map (lhs o concl) ths
  50        in let vars = map (genvar o type_of) ls
  51        in let w = substfn (List.combine ls vars) (concl th)
  52    in SUBST (List.combine ths vars) w th ;;
  53
  54 let SUBS_OCCS nlths th =
  55    try (let (nll, ths) = unzip nlths
  56    in GSUBS (subst_occs nll) ths th
  57    ) with Failure _ -> failwith "SUBS_OCCS";;
  58
  59 (*----------------------------------------------------------------------------*)
  60 (* VAR_NOT_EQ_STRUCT_OF_VAR_CONV : (thm # thm list # thm list) -> conv        *)
  61 (*                                                                            *)
  62 (* Proof method developed through discussion between                          *)
  63 (* R. Boulton, T. Melham and A. Pitts.                                        *)
  64 (*                                                                            *)
  65 (* This conversion can be used to prove that a variable is not equal to a     *)
  66 (* structure containing that variable as a proper subterm. The structures are *)
  67 (* restricted to applications of constructors from a single recursive type.   *)
  68 (* The leaf nodes must be either variables or 0-ary constructors of the type. *)
  69 (*                                                                            *)
  70 (* The theorems taken as arguments are the induction, distinctness and        *)
  71 (* injectivity theorems for the recursive type, as proved by the functions:   *)
  72 (*                                                                            *)
  73 (*    prove_induction_thm                                                     *)
  74 (*    prove_constructors_distinct                                             *)
  75 (*    prove_constructors_one_one                                              *)
  76 (*                                                                            *)
  77 (* Since the latter two functions may fail, the distinctness and injectivity  *)
  78 (* theorems are passed around as lists of conjuncts, so that a failure        *)
  79 (* results in an empty list.                                                  *)
  80 (*                                                                            *)
  81 (* Examples of input terms:                                                   *)
  82 (*                                                                            *)
  83 (*    ~(l = CONS h l)                                                         *)
  84 (*    ~(CONS h1 (CONS h2 l) = l)                                              *)
  85 (*    ~(n = SUC(SUC(SUC n)))                                                  *)
  86 (*    ~(t = TWO (ONE u) (THREE v (ONE t) (TWO u (ONE t))))                    *)
  87 (*                                                                            *)
  88 (* where the last example is for the type defined by:                         *)
  89 (*                                                                            *)
  90 (*    test = ZERO | ONE test | TWO test test | THREE test test test           *)
  91 (*                                                                            *)
  92 (* The procedure works by first generalising the structure to eliminate any   *)
  93 (* irrelevant substructures. If the variable occurs more than once in the     *)
  94 (* structure the more deeply nested occurrences are replaced by new variables *)
  95 (* because multiple occurrences of the variable prevent the induction from    *)
  96 (* working. The generalised term for the last example is:                     *)
  97 (*                                                                            *)
  98 (*    TWO a (THREE v (ONE t) b)                                               *)
  99 (*                                                                            *)
 100 (* The procedure then forms a conjunction of the inequalities for this term   *)
 101 (* and all of its `rotations':                                                *)
 102 (*                                                                            *)
 103 (*    !t. (!a v b. ~(t = TWO a (THREE v (ONE t) b))) /\                       *)
 104 (*        (!a v b. ~(t = THREE v (ONE (TWO a t)) b)) /\                       *)
 105 (*        (!a v b. ~(t = ONE (TWO a (THREE v t b))))                          *)
 106 (*                                                                            *)
 107 (* This can be proved by a straightforward structural induction. The reason   *)
 108 (* for including the rotations is that the induction hypothesis required for  *)
 109 (* the proof of the original generalised term is the rotation of it.          *)
 110 (*                                                                            *)
 111 (* The procedure could be optimised by detecting duplicated rotations. For    *)
 112 (* example it is not necessary to prove:                                      *)
 113 (*                                                                            *)
 114 (*    !n. ~(n = SUC(SUC(SUC n))) /\                                           *)
 115 (*        ~(n = SUC(SUC(SUC n))) /\                                           *)
 116 (*        ~(n = SUC(SUC(SUC n)))                                              *)
 117 (*                                                                            *)
 118 (* in order to prove "~(n = SUC(SUC(SUC n)))" because the structure is its    *)
 119 (* own rotations. It is sufficient to prove:                                  *)
 120 (*                                                                            *)
 121 (*    !n. ~(n = SUC(SUC(SUC n)))                                              *)
 122 (*                                                                            *)
 123 (* The procedure currently uses backwards proof. It would probably be more    *)
 124 (* efficient to use forwards proof.                                           *)
 125 (*----------------------------------------------------------------------------*)
 126
 127 let VAR_NOT_EQ_STRUCT_OF_VAR_CONV =
 128 try( let number_list l =
 129     let rec number_list' n l =
 130        if (l = [])
 131        then []
 132        else (hd l,n)::(number_list' (n + 1) (tl l))
 133     in number_list' 1 l
 134  in  let name = fst o dest_const
 135  in  let occurrences constrs v st =
 136         let rec occurrences' v st path =
 137            if (not (type_of st = type_of v)) then []
 138            else if (st = v) then [rev path]
 139            else if (is_var st) then []
 140            else let (f,args) =
 141                   (check ( ((can (C assoc constrs)) o name o fst) )) (strip_comb st)
 142 (* Boulton was using hashI here... but I don't know why *)
 143                 in  flat (map (fun (arg,n) -> occurrences' v arg (n::path))
 144                                  (number_list args))
 145         in occurrences' v st []
 146  in  let min_length l =
 147         let rec min_length' (x,n) l =
 148            if (l = [])
 149            then x
 150            else if (length (hd l) < n)
 151                 then min_length' (hd l,length (hd l)) (tl l)
 152                 else min_length' (x,n) (tl l)
 153         in if (l = [])
 154            then failwith "min_length"
 155            else min_length' (hd l,length (hd l)) (tl l)
 156  in  let rec generalise (st,occ) =
 157         let rec replace_side_structs (n,argn',binding) m args =
 158            if (args = [])
 159            then ([],[])
 160            else let m' = m + 1
 161                 and arg = hd args
 162                 in  let (rest,bind) =
 163                        replace_side_structs (n,argn',binding) m' (tl args)
 164                 in  if (m' = n) then ((argn'::rest),(binding @ bind))
 165                     else if (is_var arg) then ((arg::rest),((arg,arg)::bind))
 166                     else let var = genvar (type_of arg)
 167                          in  ((var::rest),((var,arg)::bind))
 168         in if (occ = [])
 169            then (st,[])
 170            else let (f,args) = strip_comb st
 171                 and (n::occ') = occ
 172                 in  let (argn',binding) = generalise (el (n-1) args,occ')
 173                 in  let (args',bind) =
 174                            replace_side_structs (n,argn',binding) 0 args
 175                 in  (list_mk_comb (f,args'),bind)
 176  in  let rec constr_apps v (st,occ) =
 177         let rec replace_argn (n,argn') m args =
 178            if (args = [])
 179            then []
 180            else let m' = m + 1
 181                 in  if (m' = n)
 182                     then argn'::(tl args)
 183                     else (hd args)::(replace_argn (n,argn') m' (tl args))
 184         in if (occ = [])
 185            then []
 186            else let (f,args) = strip_comb st
 187                 and (n::occ') = occ
 188                 in  let args' = replace_argn (n,v) 0 args
 189                 in  (list_mk_comb (f,args'))::(constr_apps v (el (n-1) args,occ'))
 190  in  let rotations l =
 191         let rec rotations' l n =
 192            if (n < 1)
 193            then []
 194            else l::(rotations' ((tl l) @ [hd l]) (n - 1))
 195         in rotations' l (length l)
 196  in  let two_constrs = (hash (fst o strip_comb) (fst o strip_comb)) o
 197                        dest_eq o dest_neg o snd o strip_forall o concl
 198  in  let flip (x,y) = (y,x)
 199  in  let DEPTH_SYM = GEN_ALL o NOT_EQ_SYM o SPEC_ALL
 200  in  let rec arg_types ty =
 201         try (match (dest_type ty) with
 202          | ("fun",[argty;rest]) ->  argty::(arg_types rest)
 203          | _ -> [])
 204         with Failure _ -> []
 205  in  let name_and_args = ((hash I) arg_types) o dest_const
 206  in
 207  fun (induction,distincts,oneOnes) ->
 208  let half_distincts = map (fun th -> ((hash name) name) (two_constrs th), th) distincts
 209  in  let distincts = half_distincts @ (map ((hash flip) DEPTH_SYM) half_distincts)
 210  in  let ind_goals =
 211         (conjuncts o fst o dest_imp o snd o dest_forall o concl) induction
 212  in  let constrs =
 213         map (name_and_args o fst o strip_comb o rand o snd o strip_forall o
 214              snd o (splitlist dest_imp) o snd o strip_forall) ind_goals
 215  in
 216  fun tm ->
 217  (let (l,r) = dest_eq (dest_neg tm)
 218   in  let (flipped,v,st) =
 219          if (is_var l)
 220          then if (is_var r) then failwith "" else (false,l,r)
 221          else if (is_var r)
 222               then (true,r,l)
 223               else failwith ""
 224   in  let occ = min_length (occurrences constrs v st)
 225   in  let (st',bind) = generalise (st,occ)
 226   in  let (vars,subterms) = List.split bind
 227   in  let apps = constr_apps v (st',occ)
 228   in  let rotats =
 229          map (end_itlist (fun t1 t2 -> subst [(t2,v)] t1)) (rotations apps)
 230   in  let uneqs = map (mk_neg o (curry mk_eq v)) rotats
 231   in  let conj =
 232          mk_forall (v,list_mk_conj (map (curry list_mk_forall vars) uneqs))
 233   in  let th1 =
 234          prove (conj,INDUCT_TAC_ induction THEN
 235                      ASM_REWRITE_TAC (oneOnes @ (map snd distincts)))
 236   in  let th2 = (hd o CONJUNCTS o (SPEC v)) th1
 237   in  let th3 = SPECL subterms th2
 238   in  let th4 = if flipped then (NOT_EQ_SYM th3) else th3
 239   in  EQT_INTRO (CONV_RULE (C ALPHA tm) th4)
 240  )) with Failure _ -> failwith "VAR_NOT_EQ_STRUCT_OF_VAR_CONV";;
 241
 242 (*----------------------------------------------------------------------------*)
 243 (* CONJS_CONV : conv -> conv                                                  *)
 244 (*                                                                            *)
 245 (* Written by T.F.Melham.                                                     *)
 246 (* Modified by R.J.Boulton.                                                   *)
 247 (*                                                                            *)
 248 (* Apply a given conversion to a sequence of conjuncts.                       *)
 249 (*                                                                            *)
 250 (* * need to check T case                                                     *)
 251 (* * need to flatten conjuncts on RHS                                         *)
 252 (*----------------------------------------------------------------------------*)
 253
 254 let CONJS_CONV =
 255 try(
 256    let is st th = try(fst(dest_const(rand(concl th))) = st) with Failure _ -> false
 257    in  let v1 = genvar `:bool` and v2 = genvar `:bool`
 258    in  let fthm1 =
 259           let th1 = ASSUME (mk_eq(v1,`F`))
 260           in  let cnj = mk_conj(v1,v2)
 261           in  let th1 = DISCH cnj (EQ_MP th1 (CONJUNCT1 (ASSUME cnj)))
 262           in  let th2 = DISCH `F` (CONTR cnj (ASSUME `F`))
 263           in  DISCH (mk_eq(v1,`F`)) (IMP_ANTISYM_RULE th1 th2)
 264    in  let fthm2 = CONV_RULE(ONCE_DEPTH_CONV(REWR_CONV CONJ_SYM)) fthm1
 265    in  let fandr th tm = MP (INST [(lhs(concl th),v1);(tm,v2)] fthm1) th
 266    in  let fandl th tm = MP (INST [(lhs(concl th),v1);(tm,v2)] fthm2) th
 267    in  let tthm1 =
 268           let th1 = ASSUME (mk_eq(v1,`T`))
 269           in  let th2 = SUBS_OCCS [[2],th1] (REFL (mk_conj(v1,v2)))
 270           in  DISCH (mk_eq(v1,`T`)) (ONCE_REWRITE_RULE [] th2)
 271    in  let tthm2 = CONV_RULE(ONCE_DEPTH_CONV(REWR_CONV CONJ_SYM)) tthm1
 272    in  let tandr th tm = MP (INST [(lhs(concl th),v1);(tm,v2)] tthm1) th
 273    in  let tandl th tm = MP (INST [(lhs(concl th),v1);(tm,v2)] tthm2) th
 274    in  let rec cconv conv tm =
 275           (let (c,cs) = dest_conj tm
 276            in  let cth = conv c
 277            in  if (is "F" cth) then fandr cth cs else
 278                let csth = cconv conv cs
 279                in  if (is "F" csth) then fandl csth c
 280                    else if (is "T" cth) then TRANS (tandr cth cs) csth
 281                    else if (is "T" csth) then TRANS (tandl csth c) cth
 282                    else try (MK_COMB((AP_TERM `(/\)` cth),csth)) with Failure _ -> conv tm )
 283    in  fun conv tm -> cconv conv tm) with Failure _ -> failwith "CONJS_CONV";;
 284
 285 (*----------------------------------------------------------------------------*)
 286 (* ONE_STEP_RECTY_EQ_CONV : (thm # thm list # thm list) -> conv -> conv       *)
 287 (*                                                                            *)
 288 (* Single step conversion for equality between structures of a single         *)
 289 (* recursive type.                                                            *)
 290 (*                                                                            *)
 291 (* Based on code written by T.F.Melham.                                       *)
 292 (*                                                                            *)
 293 (* The theorems taken as arguments are the induction, distinctness and        *)
 294 (* injectivity theorems for the recursive type, as proved by the functions:   *)
 295 (*                                                                            *)
 296 (*    prove_induction_thm                                                     *)
 297 (*    prove_constructors_distinct                                             *)
 298 (*    prove_constructors_one_one                                              *)
 299 (*                                                                            *)
 300 (* Since the latter two functions may fail, the distinctness and injectivity  *)
 301 (* theorems are passed around as lists of conjuncts.                          *)
 302 (*                                                                            *)
 303 (* If one side of the equation is a variable and that variable appears in the *)
 304 (* other side (nested in a structure) the equation is proved false.           *)
 305 (*                                                                            *)
 306 (* If the top-level constructors on the two sides of the equation are         *)
 307 (* distinct the equation is proved false.                                     *)
 308 (*                                                                            *)
 309 (* If the top-level constructors on the two sides of the equation are the     *)
 310 (* same a conjunction of equations is generated, one equation for each        *)
 311 (* argument of the constructor. The conversion given as argument is then      *)
 312 (* applied to each conjunct. If any of the applications of this conversion    *)
 313 (* fail, so will the entire call.                                             *)
 314 (*                                                                            *)
 315 (* In other conditions the function fails.                                    *)
 316 (*----------------------------------------------------------------------------*)
 317 (* Taken from HOL90 *)
 318
 319 let ONE_STEP_RECTY_EQ_CONV (induction,distincts,oneOnes) =
 320    let NOT_EQ_CONV =
 321           EQF_INTRO o EQT_ELIM o
 322           (VAR_NOT_EQ_STRUCT_OF_VAR_CONV (induction,distincts,oneOnes)) o
 323           mk_neg
 324    in  let INJ_REW = GEN_REWRITE_CONV I oneOnes
 325 (* Deleted empty_rewrites - GEN_REWRITE_CONV different in hol light - hope it works *)
 326    in  let ths1 = map SPEC_ALL distincts
 327    in  let ths2 = map (GEN_ALL o EQF_INTRO o NOT_EQ_SYM) ths1
 328    in  let dths = ths2 @ (map (GEN_ALL o EQF_INTRO) ths1)
 329    in  let DIST_REW = GEN_REWRITE_CONV I dths
 330    in  fun conv -> NOT_EQ_CONV ORELSEC
 331                   DIST_REW ORELSEC
 332                   (INJ_REW THENC (CONJS_CONV conv)) ORELSEC
 333                   (fun tm -> failwith "ONE_STEP_RECTY_EQ_CONV")
 334
 335 (*----------------------------------------------------------------------------*)
 336 (* RECTY_EQ_CONV : (thm # thm list # thm list) -> conv                        *)
 337 (*                                                                            *)
 338 (* Function to simplify as far as possible an equation between two structures *)
 339 (* of some type, the type being specified by the triple of theorems. The      *)
 340 (* structures may involve variables. The result may be a conjunction of       *)
 341 (* equations simpler than the original.                                       *)
 342 (*----------------------------------------------------------------------------*)
 343
 344 let RECTY_EQ_CONV (induction,distincts,oneOnes) =
 345 try (
 346    let one_step_conv = ONE_STEP_RECTY_EQ_CONV (induction,distincts,oneOnes)
 347    and REFL_CONV tm =
 348       let (l,r) = dest_eq tm
 349       in  if (l = r)
 350           then EQT_INTRO (REFL l)
 351           else failwith "REFL_CONV"
 352    in  let rec conv tm =
 353           (one_step_conv conv ORELSEC REFL_CONV ORELSEC ALL_CONV) tm
 354    in  fun tm -> conv tm ) with Failure _ -> failwith "RECTY_EQ_CONV";;