(******************************************************************************)
(* FILE : main.ml *)
(* DESCRIPTION : The main functions for the Boyer-Moore-style prover. *)
(* *)
(* READS FILES : <none> *)
(* WRITES FILES : <none> *)
(* *)
(* AUTHOR : R.J.Boulton *)
(* DATE : 27th June 1991 *)
(* *)
(* LAST MODIFIED : R.J.Boulton *)
(* DATE : 13th October 1992 *)
(* *)
(* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh) *)
(* DATE : July 2009 *)
(******************************************************************************)
(*----------------------------------------------------------------------------*)
(* BOYER_MOORE : conv *)
(* *)
(* Boyer-Moore-style automatic theorem prover. *)
(* Given a term "tm", attempts to prove |- tm. *)
(*----------------------------------------------------------------------------*)
let BOYER_MOORE_MESON tm =
my_gen_terms := [];
counterexamples := 0;
proof_print_depth := 0;
bm_steps := (0,0);
try (proof_print_newline
(FILTERED_WATERFALL
[taut_heuristic;
clausal_form_heuristic;
setify_heuristic;
meson_heuristic;
subst_heuristic;
HL_simplify_heuristic;
use_equality_heuristic;
generalize_heuristic_ext;
irrelevance_heuristic]
induction_heuristic []
(tm,false))
) with Failure _ -> failwith "BOYER_MOORE";;
let BOYER_MOORE_GEN tm =
my_gen_terms := [];
counterexamples := 0;
proof_print_depth := 0;
bm_steps := (0,0);
try (proof_print_newline
(FILTERED_WATERFALL
[taut_heuristic;
clausal_form_heuristic;
setify_heuristic;
subst_heuristic;
HL_simplify_heuristic;
use_equality_heuristic;
generalize_heuristic_ext;
irrelevance_heuristic]
induction_heuristic []
(tm,false))
) with Failure _ -> failwith "BOYER_MOORE";;
let BOYER_MOORE_EXT tm =
my_gen_terms := [];
counterexamples := 0;
proof_print_depth := 0;
bm_steps := (0,0);
try (proof_print_newline
(FILTERED_WATERFALL
[taut_heuristic;
clausal_form_heuristic;
setify_heuristic;
subst_heuristic;
use_equality_heuristic;
HL_simplify_heuristic;
(* meson_heuristic; *)
generalize_heuristic;
irrelevance_heuristic]
induction_heuristic []
(tm,false))
) with Failure _ -> failwith "BOYER_MOORE";;
let BOYER_MOORE tm =
counterexamples := 0;
my_gen_terms := [];
proof_print_depth := 0;
bm_steps := (0,0);
try (proof_print_newline
(WATERFALL
[clausal_form_heuristic;
subst_heuristic;
simplify_heuristic;
use_equality_heuristic;
generalize_heuristic;
irrelevance_heuristic]
induction_heuristic
(tm,false))
) with Failure _ -> failwith "BOYER_MOORE";;
(*----------------------------------------------------------------------------*)
(* BOYER_MOORE_CONV : conv *)
(* *)
(* Boyer-Moore-style automatic theorem prover. *)
(* Given a term "tm", attempts to prove |- tm = T. *)
(*----------------------------------------------------------------------------*)
let BOYER_MOORE_CONV tm =
try (EQT_INTRO (BOYER_MOORE tm)) with Failure _ -> failwith "BOYER_MOORE_CONV";;
(*----------------------------------------------------------------------------*)
(* HEURISTIC_TAC : *)
(* ((term # bool) -> ((term # bool) list # proof)) list -> tactic *)
(* *)
(* Tactic to do automatic proof using a list of heuristics. The tactic will *)
(* fail if it thinks the goal is not a theorem. Otherwise it will either *)
(* prove the goal, or return as subgoals the conjectures it couldn't handle. *)
(* *)
(* If the `proof_printing' flag is set to true, the tactic displays each new *)
(* conjecture it generates, prints blank lines between subconjectures which *)
(* resulted from a split, and prints a final blank line when it can do no *)
(* more. *)
(* *)
(* Given a goal, the tactic constructs an implication from it, so that the *)
(* hypotheses are made available. It then tries to prove this implication. *)
(* When it can do no more, the function splits the clauses that it couldn't *)
(* prove into disjuncts. The last disjunct is assumed to be a conclusion, and *)
(* the rest are taken to be hypotheses. These new goals are returned together *)
(* with a proof of the original goal. *)
(* *)
(* The proof takes a list of theorems for the subgoals and discharges the *)
(* hypotheses so that the theorems are in clausal form. These clauses are *)
(* then used to prove the implication that was constructed from the original *)
(* goal. Finally the antecedants of this implication are undischarged to give *)
(* a theorem for the original goal. *)
(*----------------------------------------------------------------------------*)
let HEURISTIC_TAC heuristics (asl,w) =
proof_print_depth := 0; try
(let negate tm = if (is_neg tm) then (rand tm) else (mk_neg tm)
and NEG_DISJ_DISCH tm th =
if (is_neg tm)
then DISJ_DISCH (rand tm) th
else CONV_RULE (REWR_CONV IMP_DISJ_THM) (DISCH tm th)
in let tm = list_mk_imp (asl,w)
in let tree = proof_print_newline
(waterfall (clausal_form_heuristic::heuristics) (tm,false))
in let tml = map fst (fringe_of_clause_tree tree)
in let disjsl = map disj_list tml
in let goals = map (fun disjs -> (map negate (butlast disjs),last disjs)) disjsl
in let proof thl =
let thl' = map (fun (th,goal)-> itlist NEG_DISJ_DISCH (fst goal) th)
(lcombinep (thl,goals))
in funpow (length asl) UNDISCH (prove_clause_tree tree thl')
in (goals,proof)
) with Failure _ -> failwith "HEURISTIC_TAC";;
(*----------------------------------------------------------------------------*)
(* BOYER_MOORE_TAC : tactic *)
(* *)
(* Tactic to do automatic proof using Boyer & Moore's heuristics. The tactic *)
(* will fail if it thinks the goal is not a theorem. Otherwise it will either *)
(* prove the goal, or return as subgoals the conjectures it couldn't handle. *)
(*----------------------------------------------------------------------------*)
let BOYER_MOORE_TAC aslw =
try (HEURISTIC_TAC
[subst_heuristic;
simplify_heuristic;
use_equality_heuristic;
generalize_heuristic;
irrelevance_heuristic;
induction_heuristic]
aslw
) with Failure _ -> failwith "BOYER_MOORE_TAC";;
(*----------------------------------------------------------------------------*)
(* BM_SIMPLIFY_TAC : tactic *)
(* *)
(* Tactic to do automatic simplification using Boyer & Moore's heuristics. *)
(* The tactic will fail if it thinks the goal is not a theorem. Otherwise, it *)
(* will either prove the goal or return the simplified conjectures as *)
(* subgoals. *)
(*----------------------------------------------------------------------------*)
let BM_SIMPLIFY_TAC aslw =
try (HEURISTIC_TAC [subst_heuristic;simplify_heuristic] aslw
) with Failure _ -> failwith "BM_SIMPLIFY_TAC";;
(*----------------------------------------------------------------------------*)
(* BM_INDUCT_TAC : tactic *)
(* *)
(* Tactic which attempts to do a SINGLE induction using Boyer & Moore's *)
(* heuristics. The cases of the induction are returned as subgoals. *)
(*----------------------------------------------------------------------------*)
let BM_INDUCT_TAC aslw =
try (let induct = ref true
in let once_induction_heuristic x =
if !induct then (induct := false; induction_heuristic x) else failwith ""
in HEURISTIC_TAC [once_induction_heuristic] aslw
) with Failure _ -> failwith "BM_INDUCT_TAC";;