# HG changeset patch # User wenzelm # Date 1187301830 -7200 # Node ID e170cee91c66a036b167c7a094486f3b7d562ee7 # Parent 91d8937992127fdad4b4c476b0caed4406ae2b53 proper signature for Meson; diff -r 91d893799212 -r e170cee91c66 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Thu Aug 16 21:52:08 2007 +0200 +++ b/src/HOL/Tools/meson.ML Fri Aug 17 00:03:50 2007 +0200 @@ -11,35 +11,42 @@ FUNCTION nodups -- if done to goal clauses too! *) -signature BASIC_MESON = +signature MESON = sig - val size_of_subgoals : thm -> int - val make_cnf : thm list -> thm -> thm list - val finish_cnf : thm list -> thm list - val make_nnf : thm -> thm - val make_nnf1 : thm -> thm - val skolemize : thm -> thm - val make_clauses : thm list -> thm list - val make_horns : thm list -> thm list - val best_prolog_tac : (thm -> int) -> thm list -> tactic - val depth_prolog_tac : thm list -> tactic - val gocls : thm list -> thm list - val skolemize_prems_tac : thm list -> int -> tactic - val MESON : (thm list -> thm list) -> (thm list -> tactic) -> int -> tactic - val best_meson_tac : (thm -> int) -> int -> tactic - val safe_best_meson_tac : int -> tactic - val depth_meson_tac : int -> tactic - val prolog_step_tac' : thm list -> int -> tactic - val iter_deepen_prolog_tac : thm list -> tactic - val iter_deepen_meson_tac : thm list -> int -> tactic - val meson_tac : int -> tactic - val negate_head : thm -> thm - val select_literal : int -> thm -> thm - val skolemize_tac : int -> tactic + val term_pair_of: indexname * (typ * 'a) -> term * 'a + val first_order_resolve: thm -> thm -> thm + val flexflex_first_order: thm -> thm + val size_of_subgoals: thm -> int + val make_cnf: thm list -> thm -> thm list + val finish_cnf: thm list -> thm list + val generalize: thm -> thm + val make_nnf: thm -> thm + val make_nnf1: thm -> thm + val skolemize: thm -> thm + val is_fol_term: theory -> term -> bool + val make_clauses: thm list -> thm list + val make_horns: thm list -> thm list + val best_prolog_tac: (thm -> int) -> thm list -> tactic + val depth_prolog_tac: thm list -> tactic + val gocls: thm list -> thm list + val skolemize_prems_tac: thm list -> int -> tactic + val MESON: (thm list -> thm list) -> (thm list -> tactic) -> int -> tactic + val best_meson_tac: (thm -> int) -> int -> tactic + val safe_best_meson_tac: int -> tactic + val depth_meson_tac: int -> tactic + val prolog_step_tac': thm list -> int -> tactic + val iter_deepen_prolog_tac: thm list -> tactic + val iter_deepen_meson_tac: thm list -> int -> tactic + val make_meta_clause: thm -> thm + val make_meta_clauses: thm list -> thm list + val meson_claset_tac: thm list -> claset -> int -> tactic + val meson_tac: int -> tactic + val negate_head: thm -> thm + val select_literal: int -> thm -> thm + val skolemize_tac: int -> tactic end - -structure Meson = +structure Meson: MESON = struct val not_conjD = thm "meson_not_conjD"; @@ -82,31 +89,31 @@ in thA RS (cterm_instantiate ct_pairs thB) end handle _ => raise THM ("first_order_resolve", 0, [thA,thB]); -fun flexflex_first_order th = +fun flexflex_first_order th = case (tpairs_of th) of [] => th | pairs => - let val thy = theory_of_thm th - val (tyenv,tenv) = - foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs - val t_pairs = map term_pair_of (Vartab.dest tenv) - val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th - in th' end - handle THM _ => th; + let val thy = theory_of_thm th + val (tyenv,tenv) = + foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs + val t_pairs = map term_pair_of (Vartab.dest tenv) + val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th + in th' end + handle THM _ => th; (*raises exception if no rules apply -- unlike RL*) -fun tryres (th, rls) = +fun tryres (th, rls) = let fun tryall [] = raise THM("tryres", 0, th::rls) | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls) in tryall rls end; - + (*Permits forward proof from rules that discharge assumptions. The supplied proof state st, e.g. from conj_forward, should have the form "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q" and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*) fun forward_res nf st = let fun forward_tacf [prem] = rtac (nf prem) 1 - | forward_tacf prems = + | forward_tacf prems = error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^ string_of_thm st ^ "\nPremises:\n" ^ @@ -126,9 +133,9 @@ | has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q | has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p | has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p - | has _ = false + | has _ = false in has end; - + (**** Clause handling ****) @@ -143,11 +150,11 @@ (*** Tautology Checking ***) -fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) = +fun signed_lits_aux (Const ("op |", _) $ P $ Q) (poslits, neglits) = signed_lits_aux Q (signed_lits_aux P (poslits, neglits)) | signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits) | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits); - + fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]); (*Literals like X=X are tautologous*) @@ -161,14 +168,14 @@ orelse exists (member (op aconv) neglits) (HOLogic.false_const :: poslits) end - handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*) + handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*) (*** To remove trivial negated equality literals from clauses ***) (*They are typically functional reflexivity axioms and are the converses of injectivity equivalences*) - + val not_refl_disj_D = thm"meson_not_refl_disj_D"; (*Is either term a Var that does not properly occur in the other term?*) @@ -179,25 +186,25 @@ fun refl_clause_aux 0 th = th | refl_clause_aux n th = case HOLogic.dest_Trueprop (concl_of th) of - (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) => + (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) => refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*) - | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) => - if eliminable(t,u) - then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*) - else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*) - | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm) - | _ => (*not a disjunction*) th; + | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) => + if eliminable(t,u) + then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*) + else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*) + | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm) + | _ => (*not a disjunction*) th; -fun notequal_lits_count (Const ("op |", _) $ P $ Q) = +fun notequal_lits_count (Const ("op |", _) $ P $ Q) = notequal_lits_count P + notequal_lits_count Q | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1 | notequal_lits_count _ = 0; (*Simplify a clause by applying reflexivity to its negated equality literals*) -fun refl_clause th = +fun refl_clause th = let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th)) in zero_var_indexes (refl_clause_aux neqs th) end - handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*) + handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*) (*** The basic CNF transformation ***) @@ -210,22 +217,22 @@ (*Estimate the number of clauses in order to detect infeasible theorems*) fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t - | signed_nclauses b (Const("op &",_) $ t $ u) = + | signed_nclauses b (Const("op &",_) $ t $ u) = if b then sum (signed_nclauses b t) (signed_nclauses b u) else prod (signed_nclauses b t) (signed_nclauses b u) - | signed_nclauses b (Const("op |",_) $ t $ u) = + | signed_nclauses b (Const("op |",_) $ t $ u) = if b then prod (signed_nclauses b t) (signed_nclauses b u) else sum (signed_nclauses b t) (signed_nclauses b u) - | signed_nclauses b (Const("op -->",_) $ t $ u) = + | signed_nclauses b (Const("op -->",_) $ t $ u) = if b then prod (signed_nclauses (not b) t) (signed_nclauses b u) else sum (signed_nclauses (not b) t) (signed_nclauses b u) - | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) = + | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) = if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*) - if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u)) - (prod (signed_nclauses (not b) u) (signed_nclauses b t)) - else sum (prod (signed_nclauses b t) (signed_nclauses b u)) - (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u)) - else 1 + if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u)) + (prod (signed_nclauses (not b) u) (signed_nclauses b t)) + else sum (prod (signed_nclauses b t) (signed_nclauses b u)) + (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u)) + else 1 | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t | signed_nclauses _ _ = 1; (* literal *) @@ -247,12 +254,12 @@ (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*) fun resop nf [prem] = resolve_tac (nf prem) 1; -(*Any need to extend this list with +(*Any need to extend this list with "HOL.type_class","HOL.eq_class","ProtoPure.term"?*) -val has_meta_conn = +val has_meta_conn = exists_Const (member (op =) ["==", "==>", "all", "prop"] o #1); -fun apply_skolem_ths (th, rls) = +fun apply_skolem_ths (th, rls) = let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls) | tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls) in tryall rls end; @@ -262,28 +269,28 @@ Eliminates existential quantifiers using skoths: Skolemization theorems.*) fun cnf skoths (th,ths) = let fun cnf_aux (th,ths) = - if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*) - else if not (has_conns ["All","Ex","op &"] (prop_of th)) - then th::ths (*no work to do, terminate*) - else case head_of (HOLogic.dest_Trueprop (concl_of th)) of - Const ("op &", _) => (*conjunction*) - cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths)) - | Const ("All", _) => (*universal quantifier*) - cnf_aux (freeze_spec th, ths) - | Const ("Ex", _) => - (*existential quantifier: Insert Skolem functions*) - cnf_aux (apply_skolem_ths (th,skoths), ths) - | Const ("op |", _) => - (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using - all combinations of converting P, Q to CNF.*) - let val tac = - (METAHYPS (resop cnf_nil) 1) THEN - (fn st' => st' |> METAHYPS (resop cnf_nil) 1) - in Seq.list_of (tac (th RS disj_forward)) @ ths end - | _ => (*no work to do*) th::ths + if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*) + else if not (has_conns ["All","Ex","op &"] (prop_of th)) + then th::ths (*no work to do, terminate*) + else case head_of (HOLogic.dest_Trueprop (concl_of th)) of + Const ("op &", _) => (*conjunction*) + cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths)) + | Const ("All", _) => (*universal quantifier*) + cnf_aux (freeze_spec th, ths) + | Const ("Ex", _) => + (*existential quantifier: Insert Skolem functions*) + cnf_aux (apply_skolem_ths (th,skoths), ths) + | Const ("op |", _) => + (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using + all combinations of converting P, Q to CNF.*) + let val tac = + (METAHYPS (resop cnf_nil) 1) THEN + (fn st' => st' |> METAHYPS (resop cnf_nil) 1) + in Seq.list_of (tac (th RS disj_forward)) @ ths end + | _ => (*no work to do*) th::ths and cnf_nil th = cnf_aux (th,[]) - in - if too_many_clauses (concl_of th) + in + if too_many_clauses (concl_of th) then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths) else cnf_aux (th,ths) end; @@ -292,7 +299,7 @@ | all_names _ = []; fun new_names n [] = [] - | new_names n (x::xs) = + | new_names n (x::xs) = if String.isPrefix "mes_" x then (x, radixstring(26,"A",n)) :: new_names (n+1) xs else new_names n xs; @@ -302,7 +309,7 @@ let val old_names = all_names (prop_of th) in Drule.rename_bvars (new_names 0 old_names) th end; -(*Convert all suitable free variables to schematic variables, +(*Convert all suitable free variables to schematic variables, but don't discharge assumptions.*) fun generalize th = Thm.varifyT (forall_elim_vars 0 (nice_names (forall_intr_frees th))); @@ -317,9 +324,9 @@ (*Forward proof, passing extra assumptions as theorems to the tactic*) fun forward_res2 nf hyps st = case Seq.pull - (REPEAT - (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) - st) + (REPEAT + (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) + st) of SOME(th,_) => th | NONE => raise THM("forward_res2", 0, [st]); @@ -328,7 +335,7 @@ fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc) handle THM _ => tryres(th,rls) handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2), - [disj_FalseD1, disj_FalseD2, asm_rl]) + [disj_FalseD1, disj_FalseD2, asm_rl]) handle THM _ => th; (*Remove duplicate literals, if there are any*) @@ -340,12 +347,12 @@ (**** Generation of contrapositives ****) -fun is_left (Const ("Trueprop", _) $ +fun is_left (Const ("Trueprop", _) $ (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _)) = true | is_left _ = false; - + (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*) -fun assoc_right th = +fun assoc_right th = if is_left (prop_of th) then assoc_right (th RS disj_assoc) else th; @@ -369,34 +376,34 @@ fun has_bool (Type("bool",_)) = true | has_bool (Type(_, Ts)) = exists has_bool Ts | has_bool _ = false; - -(*Is the string the name of a connective? Really only | and Not can remain, - since this code expects to be called on a clause form.*) + +(*Is the string the name of a connective? Really only | and Not can remain, + since this code expects to be called on a clause form.*) val is_conn = member (op =) - ["Trueprop", "op &", "op |", "op -->", "Not", + ["Trueprop", "op &", "op |", "op -->", "Not", "All", "Ex", "Ball", "Bex"]; -(*True if the term contains a function--not a logical connective--where the type +(*True if the term contains a function--not a logical connective--where the type of any argument contains bool.*) -val has_bool_arg_const = +val has_bool_arg_const = exists_Const (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T)); -(*A higher-order instance of a first-order constant? Example is the definition of +(*A higher-order instance of a first-order constant? Example is the definition of HOL.one, 1, at a function type in theory SetsAndFunctions.*) -fun higher_inst_const thy (c,T) = +fun higher_inst_const thy (c,T) = case binder_types T of [] => false (*not a function type, OK*) | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts; -(*Raises an exception if any Vars in the theorem mention type bool. +(*Raises an exception if any Vars in the theorem mention type bool. Also rejects functions whose arguments are Booleans or other functions.*) fun is_fol_term thy t = Term.is_first_order ["all","All","Ex"] t andalso not (exists (has_bool o fastype_of) (term_vars t) orelse - has_bool_arg_const t orelse - exists_Const (higher_inst_const thy) t orelse - has_meta_conn t); + has_bool_arg_const t orelse + exists_Const (higher_inst_const thy) t orelse + has_meta_conn t); fun rigid t = not (is_Var (head_of t)); @@ -405,8 +412,8 @@ | ok4horn _ = false; (*Create a meta-level Horn clause*) -fun make_horn crules th = - if ok4horn (concl_of th) +fun make_horn crules th = + if ok4horn (concl_of th) then make_horn crules (tryres(th,crules)) handle THM _ => th else th; @@ -414,17 +421,17 @@ is a HOL disjunction.*) fun add_contras crules (th,hcs) = let fun rots (0,th) = hcs - | rots (k,th) = zero_var_indexes (make_horn crules th) :: - rots(k-1, assoc_right (th RS disj_comm)) + | rots (k,th) = zero_var_indexes (make_horn crules th) :: + rots(k-1, assoc_right (th RS disj_comm)) in case nliterals(prop_of th) of - 1 => th::hcs + 1 => th::hcs | n => rots(n, assoc_right th) end; (*Use "theorem naming" to label the clauses*) fun name_thms label = let fun name1 (th, (k,ths)) = - (k-1, PureThy.put_name_hint (label ^ string_of_int k) th :: ths) + (k-1, PureThy.put_name_hint (label ^ string_of_int k) th :: ths) in fn ths => #2 (foldr name1 (length ths, []) ths) end; (*Is the given disjunction an all-negative support clause?*) @@ -436,7 +443,7 @@ (***** MESON PROOF PROCEDURE *****) fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi, - As) = rhyps(phi, A::As) + As) = rhyps(phi, A::As) | rhyps (_, As) = As; (** Detecting repeated assumptions in a subgoal **) @@ -449,7 +456,7 @@ | has_reps [_] = false | has_reps [t,u] = (t aconv u) | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false) - handle Net.INSERT => true; + handle Net.INSERT => true; (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) fun TRYING_eq_assume_tac 0 st = Seq.single st @@ -485,8 +492,8 @@ | ok4nnf (Const ("Trueprop",_) $ t) = rigid t | ok4nnf _ = false; -fun make_nnf1 th = - if ok4nnf (concl_of th) +fun make_nnf1 th = + if ok4nnf (concl_of th) then make_nnf1 (tryres(th, nnf_rls)) handle THM _ => forward_res make_nnf1 @@ -494,23 +501,23 @@ handle THM _ => th else th; -(*The simplification removes defined quantifiers and occurrences of True and False. +(*The simplification removes defined quantifiers and occurrences of True and False. nnf_ss also includes the one-point simprocs, which are needed to avoid the various one-point theorems from generating junk clauses.*) val nnf_simps = - [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True, + [simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True, if_False, if_cancel, if_eq_cancel, cases_simp]; val nnf_extra_simps = thms"split_ifs" @ ex_simps @ all_simps @ simp_thms; val nnf_ss = - HOL_basic_ss addsimps nnf_extra_simps + HOL_basic_ss addsimps nnf_extra_simps addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}]; fun make_nnf th = case prems_of th of [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps) - |> simplify nnf_ss - |> make_nnf1 + |> simplify nnf_ss + |> make_nnf1 | _ => raise THM ("make_nnf: premises in argument", 0, [th]); (*Pull existential quantifiers to front. This accomplishes Skolemization for @@ -553,20 +560,20 @@ (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions. Function mkcl converts theorems to clauses.*) -fun MESON mkcl cltac i st = +fun MESON mkcl cltac i st = SELECT_GOAL (EVERY [ObjectLogic.atomize_prems_tac 1, rtac ccontr 1, - METAHYPS (fn negs => - EVERY1 [skolemize_prems_tac negs, - METAHYPS (cltac o mkcl)]) 1]) i st - handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*) + METAHYPS (fn negs => + EVERY1 [skolemize_prems_tac negs, + METAHYPS (cltac o mkcl)]) 1]) i st + handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*) (** Best-first search versions **) (*ths is a list of additional clauses (HOL disjunctions) to use.*) fun best_meson_tac sizef = - MESON make_clauses + MESON make_clauses (fn cls => THEN_BEST_FIRST (resolve_tac (gocls cls) 1) (has_fewer_prems 1, sizef) @@ -600,19 +607,19 @@ fun iter_deepen_prolog_tac horns = ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns); -fun iter_deepen_meson_tac ths = MESON make_clauses +fun iter_deepen_meson_tac ths = MESON make_clauses (fn cls => case (gocls (cls@ths)) of - [] => no_tac (*no goal clauses*) - | goes => - let val horns = make_horns (cls@ths) - val _ = - Output.debug (fn () => ("meson method called:\n" ^ - space_implode "\n" (map string_of_thm (cls@ths)) ^ - "\nclauses:\n" ^ - space_implode "\n" (map string_of_thm horns))) - in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) - end + [] => no_tac (*no goal clauses*) + | goes => + let val horns = make_horns (cls@ths) + val _ = + Output.debug (fn () => ("meson method called:\n" ^ + space_implode "\n" (map string_of_thm (cls@ths)) ^ + "\nclauses:\n" ^ + space_implode "\n" (map string_of_thm horns))) + in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) + end ); fun meson_claset_tac ths cs = @@ -623,7 +630,7 @@ (**** Code to support ordinary resolution, rather than Model Elimination ****) -(*Convert a list of clauses (disjunctions) to meta-level clauses (==>), +(*Convert a list of clauses (disjunctions) to meta-level clauses (==>), with no contrapositives, for ordinary resolution.*) (*Rules to convert the head literal into a negated assumption. If the head @@ -632,21 +639,21 @@ val notEfalse = read_instantiate [("R","False")] notE; val notEfalse' = rotate_prems 1 notEfalse; -fun negated_asm_of_head th = +fun negated_asm_of_head th = th RS notEfalse handle THM _ => th RS notEfalse'; (*Converting one clause*) -val make_meta_clause = +val make_meta_clause = zero_var_indexes o negated_asm_of_head o make_horn resolution_clause_rules; - + fun make_meta_clauses ths = name_thms "MClause#" (distinct Thm.eq_thm_prop (map make_meta_clause ths)); (*Permute a rule's premises to move the i-th premise to the last position.*) fun make_last i th = - let val n = nprems_of th - in if 1 <= i andalso i <= n + let val n = nprems_of th + in if 1 <= i andalso i <= n then Thm.permute_prems (i-1) 1 th else raise THM("select_literal", i, [th]) end; @@ -660,17 +667,17 @@ (*Top-level Skolemization. Allows part of the conversion to clauses to be - expressed as a tactic (or Isar method). Each assumption of the selected + expressed as a tactic (or Isar method). Each assumption of the selected goal is converted to NNF and then its existential quantifiers are pulled - to the front. Finally, all existential quantifiers are eliminated, + to the front. Finally, all existential quantifiers are eliminated, leaving !!-quantified variables. Perhaps Safe_tac should follow, but it might generate many subgoals.*) -fun skolemize_tac i st = +fun skolemize_tac i st = let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1)) - in + in EVERY' [METAHYPS - (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1 + (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1 THEN REPEAT (etac exE 1))), REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st end @@ -678,5 +685,3 @@ end; -structure BasicMeson: BASIC_MESON = Meson; -open BasicMeson; diff -r 91d893799212 -r e170cee91c66 src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Thu Aug 16 21:52:08 2007 +0200 +++ b/src/HOL/Tools/metis_tools.ML Fri Aug 17 00:03:50 2007 +0200 @@ -338,7 +338,7 @@ val index_th2 = get_index i_atm prems_th2 handle Empty => error "Failed to find literal in th2" val _ = Output.debug (fn () => " index_th2: " ^ Int.toString index_th2) - in (select_literal index_th1 i_th1) RSN (index_th2, i_th2) end + in (Meson.select_literal index_th1 i_th1) RSN (index_th2, i_th2) end end; (* INFERENCE RULE: REFL *) @@ -560,7 +560,7 @@ "Metis called with theorems " ^ cat_lines (map string_of_thm ths)) val ths' = ResAxioms.cnf_rules_of_ths ths in - (MESON ResAxioms.neg_clausify (fn cls => rtac (FOL_SOLVE mode ctxt cls ths') 1) i + (Meson.MESON ResAxioms.neg_clausify (fn cls => rtac (FOL_SOLVE mode ctxt cls ths') 1) i THEN ResAxioms.expand_defs_tac st0) st0 end; diff -r 91d893799212 -r e170cee91c66 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Aug 16 21:52:08 2007 +0200 +++ b/src/HOL/Tools/res_atp.ML Fri Aug 17 00:03:50 2007 +0200 @@ -768,7 +768,7 @@ (*Called by the oracle-based methods declared in res_atp_methods.ML*) fun write_subgoal_file dfg mode ctxt conjectures user_thms n = - let val conj_cls = make_clauses conjectures + let val conj_cls = Meson.make_clauses conjectures |> ResAxioms.assume_abstract_list "subgoal" |> Meson.finish_cnf val hyp_cls = cnf_hyps_thms ctxt val goal_cls = conj_cls@hyp_cls diff -r 91d893799212 -r e170cee91c66 src/HOL/Tools/res_atp_methods.ML --- a/src/HOL/Tools/res_atp_methods.ML Thu Aug 16 21:52:08 2007 +0200 +++ b/src/HOL/Tools/res_atp_methods.ML Fri Aug 17 00:03:50 2007 +0200 @@ -9,7 +9,7 @@ (* convert the negated 1st subgoal into CNF, write to file and call an ATP oracle *) fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms n thm = - (EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, skolemize_tac, + (EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac, METAHYPS(fn negs => HEADGOAL(Tactic.rtac (res_atp_oracle (ProofContext.theory_of ctxt) diff -r 91d893799212 -r e170cee91c66 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Thu Aug 16 21:52:08 2007 +0200 +++ b/src/HOL/Tools/res_axioms.ML Fri Aug 17 00:03:50 2007 +0200 @@ -409,7 +409,7 @@ fun to_nnf th = th |> transfer_to_ATP_Linkup |> transform_elim |> zero_var_indexes |> freeze_thm - |> Conv.fconv_rule ObjectLogic.atomize |> make_nnf |> strip_lambdas ~1; + |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1; (*Generate Skolem functions for a theorem supplied in nnf*) fun skolem_of_nnf s th = @@ -636,13 +636,14 @@ (*** Converting a subgoal into negated conjecture clauses. ***) -val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, skolemize_tac]; +val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac]; (*finish_cnf removes tautologies and functional reflexivity axioms, but by calling Thm.varifyT it can introduce TVars, which are useless in conjecture clauses.*) val no_tvars = null o term_tvars o prop_of; -val neg_clausify = filter no_tvars o Meson.finish_cnf o assume_abstract_list "subgoal" o make_clauses; +val neg_clausify = + filter no_tvars o Meson.finish_cnf o assume_abstract_list "subgoal" o Meson.make_clauses; fun neg_conjecture_clauses st0 n = let val st = Seq.hd (neg_skolemize_tac n st0) diff -r 91d893799212 -r e170cee91c66 src/HOL/ex/Classical.thy --- a/src/HOL/ex/Classical.thy Thu Aug 16 21:52:08 2007 +0200 +++ b/src/HOL/ex/Classical.thy Fri Aug 17 00:03:50 2007 +0200 @@ -430,7 +430,7 @@ lemma "(\x y z. R(x,y) & R(y,z) --> R(x,z)) & (\x. \y. R(x,y)) --> ~ (\x. P x = (\y. R(x,y) --> ~ P y))" -by (tactic{*safe_best_meson_tac 1*}) +by (tactic{*Meson.safe_best_meson_tac 1*}) --{*In contrast, @{text meson} is SLOW: 7.6s on griffon*} @@ -724,7 +724,7 @@ (\x y. bird x & snail y \ ~eats x y) & (\x. (caterpillar x \ snail x) \ (\y. plant y & eats x y)) \ (\x y. animal x & animal y & (\z. grain z & eats y z & eats x y))" -by (tactic{*safe_best_meson_tac 1*}) +by (tactic{*Meson.safe_best_meson_tac 1*}) --{*Nearly twice as fast as @{text meson}, which performs iterative deepening rather than best-first search*} diff -r 91d893799212 -r e170cee91c66 src/HOL/ex/Meson_Test.thy --- a/src/HOL/ex/Meson_Test.thy Thu Aug 16 21:52:08 2007 +0200 +++ b/src/HOL/ex/Meson_Test.thy Fri Aug 17 00:03:50 2007 +0200 @@ -30,19 +30,19 @@ Goal "(\x. P x) & (\x. L x --> ~ (M x & R x)) & (\x. P x --> (M x & L x)) & ((\x. P x --> Q x) | (\x. P x & R x)) --> (\x. Q x & P x)"; by (rtac ccontr 1); val [prem25] = gethyps 1; -val nnf25 = make_nnf prem25; -val xsko25 = skolemize nnf25; +val nnf25 = Meson.make_nnf prem25; +val xsko25 = Meson.skolemize nnf25; by (cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1)); val [_,sko25] = gethyps 1; -val clauses25 = make_clauses [sko25]; (*7 clauses*) -val horns25 = make_horns clauses25; (*16 Horn clauses*) -val go25::_ = gocls clauses25; +val clauses25 = Meson.make_clauses [sko25]; (*7 clauses*) +val horns25 = Meson.make_horns clauses25; (*16 Horn clauses*) +val go25::_ = Meson.gocls clauses25; *} ML {* Goal "False"; by (rtac go25 1); -by (depth_prolog_tac horns25); +by (Meson.depth_prolog_tac horns25); *} ML {* @@ -50,19 +50,19 @@ Goal "((\x. p x) = (\x. q x)) & (\x. \y. p x & q y --> (r x = s y)) --> ((\x. p x --> r x) = (\x. q x --> s x))"; by (rtac ccontr 1); val [prem26] = gethyps 1; -val nnf26 = make_nnf prem26; -val xsko26 = skolemize nnf26; +val nnf26 = Meson.make_nnf prem26; +val xsko26 = Meson.skolemize nnf26; by (cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1)); val [_,sko26] = gethyps 1; -val clauses26 = make_clauses [sko26]; (*9 clauses*) -val horns26 = make_horns clauses26; (*24 Horn clauses*) -val go26::_ = gocls clauses26; +val clauses26 = Meson.make_clauses [sko26]; (*9 clauses*) +val horns26 = Meson.make_horns clauses26; (*24 Horn clauses*) +val go26::_ = Meson.gocls clauses26; *} ML {* Goal "False"; by (rtac go26 1); -by (depth_prolog_tac horns26); (*1.4 secs*) +by (Meson.depth_prolog_tac horns26); (*1.4 secs*) (*Proof is of length 107!!*) *} @@ -71,19 +71,19 @@ Goal "(\x. \y. q x y = (\z. p z x = (p z y::bool))) --> (\x. (\y. q x y = (q y x::bool)))"; by (rtac ccontr 1); val [prem43] = gethyps 1; -val nnf43 = make_nnf prem43; -val xsko43 = skolemize nnf43; +val nnf43 = Meson.make_nnf prem43; +val xsko43 = Meson.skolemize nnf43; by (cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1)); val [_,sko43] = gethyps 1; -val clauses43 = make_clauses [sko43]; (*6*) -val horns43 = make_horns clauses43; (*16*) -val go43::_ = gocls clauses43; +val clauses43 = Meson.make_clauses [sko43]; (*6*) +val horns43 = Meson.make_horns clauses43; (*16*) +val go43::_ = Meson.gocls clauses43; *} ML {* Goal "False"; by (rtac go43 1); -by (best_prolog_tac size_of_subgoals horns43); (*1.6 secs*) +by (Meson.best_prolog_tac Meson.size_of_subgoals horns43); (*1.6 secs*) *} ML {* Logic.auto_rename := false; *}