Boyer_Moore/induction.ml

   1 (******************************************************************************)
   2 (* FILE          : induction.ml                                               *)
   3 (* DESCRIPTION   : Induction.                                                 *)
   4 (*                                                                            *)
   5 (* READS FILES   : <none>                                                     *)
   6 (* WRITES FILES  : <none>                                                     *)
   7 (*                                                                            *)
   8 (* AUTHOR        : R.J.Boulton                                                *)
   9 (* DATE          : 26th June 1991                                             *)
  10 (*                                                                            *)
  11 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh)                *)
  12 (* DATE          : 2008                                                       *)
  13 (******************************************************************************)
  14
  15 let (CONV_OF_RCONV: conv -> conv) =
  16   let rec get_bv tm =
  17     if is_abs tm then bndvar tm
  18     else if is_comb tm then
  19          try get_bv (rand tm) with Failure _ -> get_bv (rator tm)
  20     else failwith "" in
  21   fun conv tm ->
  22   let v = get_bv tm in
  23   let th1 = conv tm in
  24   let th2 = ONCE_DEPTH_CONV (GEN_ALPHA_CONV v) (rhs(concl th1)) in
  25   TRANS th1 th2;;
  26
  27 let (CONV_OF_THM: thm -> conv) =
  28   CONV_OF_RCONV o REWR_CONV;;
  29
  30 let RIGHT_IMP_FORALL_CONV = CONV_OF_THM RIGHT_IMP_FORALL_THM;;
  31 (* Does this work?? *)
  32
  33 (*----------------------------------------------------------------------------*)
  34 (* is_rec_const_app : term -> bool                                            *)
  35 (*                                                                            *)
  36 (* This function returns true if the term it is given is an application of a  *)
  37 (* currently known recursive function constant.                               *)
  38 (*----------------------------------------------------------------------------*)
  39
  40 let is_rec_const_app tm =
  41 try (let (f,args) = strip_comb tm
  42   in  let (n,defs) = (get_def o fst o dest_const) f
  43   in  (n > 0) &
  44       ((length o snd o strip_comb o lhs o concl o snd o hd) defs = length args)
  45  ) with Failure _ -> false;;
  46
  47
  48 (*----------------------------------------------------------------------------*)
  49 (* possible_inductions : term -> (term list # term list)                      *)
  50 (*                                                                            *)
  51 (* Function to compute two lists of variables on which induction could be     *)
  52 (* performed. The first list of variables for which the induction is unflawed *)
  53 (* and the second is of variables for which the induction is flawed.          *)
  54 (*                                                                            *)
  55 (* From a list of applications of recursive functions, the arguments are      *)
  56 (* split into those that are in a recursive argument position and those that  *)
  57 (* are not. Possible inductions are on the variables in the recursive         *)
  58 (* argument positions, but if the variable also appears in a non-recursive    *)
  59 (* argument position then the induction is flawed.                            *)
  60 (*----------------------------------------------------------------------------*)
  61
  62 let possible_inductions tm =
  63    let apps = find_bm_terms is_rec_const_app tm
  64    in  let (rec_args,other_args) =
  65           List.split (map (fun app -> let (f,args) = strip_comb app
  66                             in  let name = fst (dest_const f)
  67                             in  let n = (fst o get_def) name
  68                             in  remove_el n args) apps)
  69    in  let vars = setify (filter is_var rec_args)
  70    in  let others = setify (flat other_args)
  71    in  partition (fun v -> not (mem v others)) vars;;
  72
  73 (*----------------------------------------------------------------------------*)
  74 (* DEPTH_FORALL_CONV : conv -> conv                                           *)
  75 (*                                                                            *)
  76 (* Given a term of the form "!x1 ... xn. t", this function applies the        *)
  77 (* argument conversion to "t".                                                *)
  78 (*----------------------------------------------------------------------------*)
  79
  80 let rec DEPTH_FORALL_CONV conv tm =
  81    if (is_forall tm)
  82    then RAND_CONV (ABS_CONV (DEPTH_FORALL_CONV conv)) tm
  83    else conv tm;;
  84
  85 (*----------------------------------------------------------------------------*)
  86 (* induction_heuristic : (term # bool) -> ((term # bool) list # proof)        *)
  87 (*                                                                            *)
  88 (* Heuristic for induction. It performs one of the possible unflawed          *)
  89 (* inductions on a clause, or failing that, one of the flawed inductions.     *)
  90 (* The heuristic fails if no inductions are possible.                         *)
  91 (*                                                                            *)
  92 (* Having obtained a variable on which to perform induction, the function     *)
  93 (* computes the name of the top-level type constructor in the type of the     *)
  94 (* variable. The appropriate induction theorem is then obtained from the      *)
  95 (* shell environment. The theorem is specialised for the argument clause and  *)
  96 (* beta-reduction is performed at the appropriate places.                     *)
  97 (*                                                                            *)
  98 (* The resulting theorem will be of the form:                                 *)
  99 (*                                                                            *)
 100 (*    |- (case1 /\ ... /\ casen) ==> (!x. f[x])                         ( * ) *)
 101 (*                                                                            *)
 102 (* So, if we can establish casei for each i, we shall have |- !x. f[x]. When  *)
 103 (* specialised with the induction variable, this theorem has the original     *)
 104 (* clause as its conclusion. Each casei is of one of these forms:             *)
 105 (*                                                                            *)
 106 (*    !x1 ... xn. s ==> (!y1 ... ym. t)                                       *)
 107 (*    !x1 ... xn. t                                                           *)
 108 (*                                                                            *)
 109 (* where the yi's do not appear in s. We simplify the casei's that have the   *)
 110 (* first form by proving theorems like:                                       *)
 111 (*                                                                            *)
 112 (*    |- (!x1 ... xn. s ==> (!y1 ... ym. t)) =                                *)
 113 (*       (!x1 ... xn y1 ... ym. s ==> t)                                      *)
 114 (*                                                                            *)
 115 (* For consistency, theorems of the form |- (!x1 ... xn. t) = (!x1 ... xn. t) *)
 116 (* are proved for the casei's that have the second form. The bodies of the    *)
 117 (* right-hand sides of these equations are returned as the new goal clauses.  *)
 118 (* A body that is an implication is taken to be an inductive step and so is   *)
 119 (* returned paired with true. Bodies that are not implications are paired     *)
 120 (* with false.                                                                *)
 121 (*                                                                            *)
 122 (* The proof of the original clause from these new clauses proceeds as        *)
 123 (* follows. The universal quantifications that were stripped from the         *)
 124 (* right-hand sides are restored by generalizing the theorems. From the       *)
 125 (* equations we can then obtain theorems for the left-hand sides. These are   *)
 126 (* conjoined and used to satisfy the antecedant of the theorem ( * ). As      *)
 127 (* described above, specialising the resulting theorem gives a theorem for    *)
 128 (* the original clause.                                                       *)
 129 (*----------------------------------------------------------------------------*)
 130
 131 let induction_heuristic (tm,(ind:bool)) =
 132 try
 133  (let (unflawed,flawed) = possible_inductions tm
 134   in  let var = try (hd unflawed) with Failure _ -> (hd flawed)
 135   in  let ty_name = fst (dest_type (type_of var))
 136   in  let induct_thm = (sys_shell_info ty_name).induct
 137   in  let P = mk_abs (var,tm)
 138   in  let th1 = ISPEC P induct_thm
 139   in  let th2 =
 140          CONV_RULE
 141             (ONCE_DEPTH_CONV
 142                 (fun tm -> if (rator tm = P) then BETA_CONV tm else failwith "")) th1
 143   in  let new_goals = conj_list (rand (rator (concl th2)))
 144   in  let ths =
 145          map (REPEATC (DEPTH_FORALL_CONV RIGHT_IMP_FORALL_CONV)) new_goals
 146   in  let (varsl,tml) = List.split (map (strip_forall o rhs o concl) ths)
 147   in  let proof thl =
 148          let thl' = map (uncurry GENL) (lcombinep (varsl,thl))
 149          in  let thl'' = map (fun (eq,th) -> EQ_MP (SYM eq) th) (lcombinep (ths,thl'))
 150          in  SPEC var (MP th2 (LIST_CONJ thl''))
 151   in  (map (fun tm -> (tm,((is_imp tm) & (not (is_neg tm))))) tml,
 152        apply_proof proof tml)
 153  ) with Failure _ -> failwith "induction_heuristic";;