MESON tactical takes an additional argument: the clausification function.
authorpaulson
Thu Mar 29 11:12:39 2007 +0200 (2007-03-29)
changeset 22546c40d7ab8cbc5
parent 22545 bd72c625c930
child 22547 c3290f4382e4
MESON tactical takes an additional argument: the clausification function.
src/HOL/Tools/meson.ML
     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*)