Boyer_Moore/main.ml

   1 (******************************************************************************)
   2 (* FILE          : main.ml                                                    *)
   3 (* DESCRIPTION   : The main functions for the Boyer-Moore-style prover.       *)
   4 (*                                                                            *)
   5 (* READS FILES   : <none>                                                     *)
   6 (* WRITES FILES  : <none>                                                     *)
   7 (*                                                                            *)
   8 (* AUTHOR        : R.J.Boulton                                                *)
   9 (* DATE          : 27th June 1991                                             *)
  10 (*                                                                            *)
  11 (* LAST MODIFIED : R.J.Boulton                                                *)
  12 (* DATE          : 13th October 1992                                          *)
  13 (*                                                                            *)
  14 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh)                *)
  15 (* DATE          : July 2009                                                  *)
  16 (******************************************************************************)
  17
  18 (*----------------------------------------------------------------------------*)
  19 (* BOYER_MOORE : conv                                                         *)
  20 (*                                                                            *)
  21 (* Boyer-Moore-style automatic theorem prover.                                *)
  22 (* Given a term "tm", attempts to prove |- tm.                                *)
  23 (*----------------------------------------------------------------------------*)
  24
  25 let BOYER_MOORE_MESON tm =
  26 my_gen_terms := [];
  27 counterexamples := 0;
  28 proof_print_depth := 0;
  29 bm_steps := (0,0);
  30 try  (proof_print_newline
  31      (FILTERED_WATERFALL
  32          [taut_heuristic;
  33           clausal_form_heuristic;
  34           setify_heuristic;
  35           meson_heuristic;
  36           subst_heuristic;
  37           HL_simplify_heuristic;
  38           use_equality_heuristic;
  39           generalize_heuristic_ext;
  40           irrelevance_heuristic]
  41          induction_heuristic []
  42          (tm,false))
  43  ) with Failure _ -> failwith "BOYER_MOORE";;
  44
  45 let BOYER_MOORE_GEN tm =
  46 my_gen_terms := [];
  47 counterexamples := 0;
  48  proof_print_depth := 0;
  49 bm_steps := (0,0);
  50 try  (proof_print_newline
  51      (FILTERED_WATERFALL
  52          [taut_heuristic;
  53           clausal_form_heuristic;
  54           setify_heuristic;
  55           subst_heuristic;
  56           HL_simplify_heuristic;
  57           use_equality_heuristic;
  58           generalize_heuristic_ext;
  59           irrelevance_heuristic]
  60          induction_heuristic []
  61          (tm,false))
  62  ) with Failure _ -> failwith "BOYER_MOORE";;
  63
  64 let BOYER_MOORE_EXT tm =
  65 my_gen_terms := [];
  66 counterexamples := 0;
  67  proof_print_depth := 0;
  68 bm_steps := (0,0);
  69 try  (proof_print_newline
  70      (FILTERED_WATERFALL
  71          [taut_heuristic;
  72           clausal_form_heuristic;
  73           setify_heuristic;
  74           subst_heuristic;
  75           use_equality_heuristic;
  76           HL_simplify_heuristic;
  77 (*          meson_heuristic; *)
  78           generalize_heuristic;
  79           irrelevance_heuristic]
  80          induction_heuristic []
  81          (tm,false))
  82  ) with Failure _ -> failwith "BOYER_MOORE";;
  83
  84 let BOYER_MOORE tm =
  85 counterexamples := 0;
  86 my_gen_terms := [];
  87  proof_print_depth := 0;
  88 bm_steps := (0,0);
  89 try  (proof_print_newline
  90      (WATERFALL
  91          [clausal_form_heuristic;
  92           subst_heuristic;
  93           simplify_heuristic;
  94           use_equality_heuristic;
  95           generalize_heuristic;
  96           irrelevance_heuristic]
  97          induction_heuristic
  98          (tm,false))
  99  ) with Failure _ -> failwith "BOYER_MOORE";;
 100
 101 (*----------------------------------------------------------------------------*)
 102 (* BOYER_MOORE_CONV : conv                                                    *)
 103 (*                                                                            *)
 104 (* Boyer-Moore-style automatic theorem prover.                                *)
 105 (* Given a term "tm", attempts to prove |- tm = T.                            *)
 106 (*----------------------------------------------------------------------------*)
 107
 108 let BOYER_MOORE_CONV tm =
 109 try (EQT_INTRO (BOYER_MOORE tm)) with Failure _ -> failwith "BOYER_MOORE_CONV";;
 110
 111 (*----------------------------------------------------------------------------*)
 112 (* HEURISTIC_TAC :                                                            *)
 113 (*    ((term # bool) -> ((term # bool) list # proof)) list -> tactic          *)
 114 (*                                                                            *)
 115 (* Tactic to do automatic proof using a list of heuristics. The tactic will   *)
 116 (* fail if it thinks the goal is not a theorem. Otherwise it will either      *)
 117 (* prove the goal, or return as subgoals the conjectures it couldn't handle.  *)
 118 (*                                                                            *)
 119 (* If the `proof_printing' flag is set to true, the tactic displays each new  *)
 120 (* conjecture it generates, prints blank lines between subconjectures which   *)
 121 (* resulted from a split, and prints a final blank line when it can do no     *)
 122 (* more.                                                                      *)
 123 (*                                                                            *)
 124 (* Given a goal, the tactic constructs an implication from it, so that the    *)
 125 (* hypotheses are made available. It then tries to prove this implication.    *)
 126 (* When it can do no more, the function splits the clauses that it couldn't   *)
 127 (* prove into disjuncts. The last disjunct is assumed to be a conclusion, and *)
 128 (* the rest are taken to be hypotheses. These new goals are returned together *)
 129 (* with a proof of the original goal.                                         *)
 130 (*                                                                            *)
 131 (* The proof takes a list of theorems for the subgoals and discharges the     *)
 132 (* hypotheses so that the theorems are in clausal form. These clauses are     *)
 133 (* then used to prove the implication that was constructed from the original  *)
 134 (* goal. Finally the antecedants of this implication are undischarged to give *)
 135 (* a theorem for the original goal.                                           *)
 136 (*----------------------------------------------------------------------------*)
 137
 138 let HEURISTIC_TAC heuristics (asl,w) =
 139  proof_print_depth := 0; try
 140  (let negate tm = if (is_neg tm) then (rand tm) else (mk_neg tm)
 141   and NEG_DISJ_DISCH tm th =
 142      if (is_neg tm)
 143      then DISJ_DISCH (rand tm) th
 144      else CONV_RULE (REWR_CONV IMP_DISJ_THM) (DISCH tm th)
 145   in  let tm = list_mk_imp (asl,w)
 146   in  let tree = proof_print_newline
 147                     (waterfall (clausal_form_heuristic::heuristics) (tm,false))
 148   in  let tml = map fst (fringe_of_clause_tree tree)
 149   in  let disjsl = map disj_list tml
 150   in  let goals = map (fun disjs -> (map negate (butlast disjs),last disjs)) disjsl
 151   in  let proof thl =
 152          let thl' = map (fun (th,goal)-> itlist NEG_DISJ_DISCH (fst goal) th)
 153                            (lcombinep (thl,goals))
 154          in  funpow (length asl) UNDISCH (prove_clause_tree tree thl')
 155   in  (goals,proof)
 156  ) with Failure _ -> failwith "HEURISTIC_TAC";;
 157
 158 (*----------------------------------------------------------------------------*)
 159 (* BOYER_MOORE_TAC : tactic                                                   *)
 160 (*                                                                            *)
 161 (* Tactic to do automatic proof using Boyer & Moore's heuristics. The tactic  *)
 162 (* will fail if it thinks the goal is not a theorem. Otherwise it will either *)
 163 (* prove the goal, or return as subgoals the conjectures it couldn't handle.  *)
 164 (*----------------------------------------------------------------------------*)
 165
 166 let BOYER_MOORE_TAC aslw =
 167 try (HEURISTIC_TAC
 168      [subst_heuristic;
 169       simplify_heuristic;
 170       use_equality_heuristic;
 171       generalize_heuristic;
 172       irrelevance_heuristic;
 173       induction_heuristic]
 174     aslw
 175  ) with Failure _ -> failwith "BOYER_MOORE_TAC";;
 176
 177 (*----------------------------------------------------------------------------*)
 178 (* BM_SIMPLIFY_TAC : tactic                                                   *)
 179 (*                                                                            *)
 180 (* Tactic to do automatic simplification using Boyer & Moore's heuristics.    *)
 181 (* The tactic will fail if it thinks the goal is not a theorem. Otherwise, it *)
 182 (* will either prove the goal or return the simplified conjectures as         *)
 183 (* subgoals.                                                                  *)
 184 (*----------------------------------------------------------------------------*)
 185
 186 let BM_SIMPLIFY_TAC aslw =
 187  try (HEURISTIC_TAC [subst_heuristic;simplify_heuristic] aslw
 188  ) with Failure _ -> failwith "BM_SIMPLIFY_TAC";;
 189
 190 (*----------------------------------------------------------------------------*)
 191 (* BM_INDUCT_TAC : tactic                                                     *)
 192 (*                                                                            *)
 193 (* Tactic which attempts to do a SINGLE induction using Boyer & Moore's       *)
 194 (* heuristics. The cases of the induction are returned as subgoals.           *)
 195 (*----------------------------------------------------------------------------*)
 196
 197 let BM_INDUCT_TAC aslw =
 198 try  (let induct = ref true
 199   in  let once_induction_heuristic x =
 200          if !induct then (induct := false; induction_heuristic x) else failwith ""
 201   in  HEURISTIC_TAC [once_induction_heuristic] aslw
 202  ) with Failure _ -> failwith "BM_INDUCT_TAC";;