1.1 --- a/src/HOL/Tools/meson.ML Thu Mar 29 11:12:03 2007 +0200
1.2 +++ b/src/HOL/Tools/meson.ML Thu Mar 29 11:12:39 2007 +0200
1.3 @@ -25,7 +25,7 @@
1.4 val depth_prolog_tac : thm list -> tactic
1.5 val gocls : thm list -> thm list
1.6 val skolemize_prems_tac : thm list -> int -> tactic
1.7 - val MESON : (thm list -> tactic) -> int -> tactic
1.8 + val MESON : (thm list -> thm list) -> (thm list -> tactic) -> int -> tactic
1.9 val best_meson_tac : (thm -> int) -> int -> tactic
1.10 val safe_best_meson_tac : int -> tactic
1.11 val depth_meson_tac : int -> tactic
1.12 @@ -546,13 +546,14 @@
1.13 let val defs = filter (can dest_equals) (#hyps (crep_thm st))
1.14 in PRIMITIVE (LocalDefs.expand defs) st end;
1.15
1.16 -(*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions*)
1.17 -fun MESON cltac i st =
1.18 +(*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions.
1.19 + Function mkcl converts theorems to clauses.*)
1.20 +fun MESON mkcl cltac i st =
1.21 SELECT_GOAL
1.22 (EVERY [rtac ccontr 1,
1.23 METAHYPS (fn negs =>
1.24 EVERY1 [skolemize_prems_tac negs,
1.25 - METAHYPS (cltac o make_clauses)]) 1,
1.26 + METAHYPS (cltac o mkcl)]) 1,
1.27 expand_defs_tac]) i st
1.28 handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
1.29
1.30 @@ -560,7 +561,8 @@
1.31
1.32 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
1.33 fun best_meson_tac sizef =
1.34 - MESON (fn cls =>
1.35 + MESON make_clauses
1.36 + (fn cls =>
1.37 THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
1.38 (has_fewer_prems 1, sizef)
1.39 (prolog_step_tac (make_horns cls) 1));
1.40 @@ -573,8 +575,8 @@
1.41 (** Depth-first search version **)
1.42
1.43 val depth_meson_tac =
1.44 - MESON (fn cls => EVERY [resolve_tac (gocls cls) 1,
1.45 - depth_prolog_tac (make_horns cls)]);
1.46 + MESON make_clauses
1.47 + (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]);
1.48
1.49
1.50 (** Iterative deepening version **)
1.51 @@ -593,7 +595,7 @@
1.52 fun iter_deepen_prolog_tac horns =
1.53 ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
1.54
1.55 -fun iter_deepen_meson_tac ths = MESON
1.56 +fun iter_deepen_meson_tac ths = MESON make_clauses
1.57 (fn cls =>
1.58 case (gocls (cls@ths)) of
1.59 [] => no_tac (*no goal clauses*)