# HG changeset patch # User paulson # Date 1110210936 -3600 # Node ID 32bee18c675f6f012f85a37f58bab4d524d15242 # Parent d364491ba718ed8ba38059f206e3f4aeca0d656e Tools/meson.ML: signature, structure and "open" rather than "local" diff -r d364491ba718 -r 32bee18c675f src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Fri Mar 04 23:25:06 2005 +0100 +++ b/src/HOL/Tools/meson.ML Mon Mar 07 16:55:36 2005 +0100 @@ -11,236 +11,264 @@ FUNCTION nodups -- if done to goal clauses too! *) -local - - val not_conjD = thm "meson_not_conjD"; - val not_disjD = thm "meson_not_disjD"; - val not_notD = thm "meson_not_notD"; - val not_allD = thm "meson_not_allD"; - val not_exD = thm "meson_not_exD"; - val imp_to_disjD = thm "meson_imp_to_disjD"; - val not_impD = thm "meson_not_impD"; - val iff_to_disjD = thm "meson_iff_to_disjD"; - val not_iffD = thm "meson_not_iffD"; - val conj_exD1 = thm "meson_conj_exD1"; - val conj_exD2 = thm "meson_conj_exD2"; - val disj_exD = thm "meson_disj_exD"; - val disj_exD1 = thm "meson_disj_exD1"; - val disj_exD2 = thm "meson_disj_exD2"; - val disj_assoc = thm "meson_disj_assoc"; - val disj_comm = thm "meson_disj_comm"; - val disj_FalseD1 = thm "meson_disj_FalseD1"; - val disj_FalseD2 = thm "meson_disj_FalseD2"; +signature BASIC_MESON = +sig + val size_of_subgoals : thm -> int + val make_nnf : 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 -> 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 : int -> tactic + val meson_tac : int -> tactic + val negate_head : thm -> thm + val select_literal : int -> thm -> thm + val skolemize_tac : int -> tactic + val make_clauses_tac : int -> tactic + val meson_setup : (theory -> theory) list +end - (**** Operators for forward proof ****) - - (*raises exception if no rules apply -- unlike RL*) - fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls)) - | tryres (th, []) = raise THM("tryres", 0, [th]); +structure Meson = +struct - val prop_of = #prop o rep_thm; - - (*Permits forward proof from rules that discharge assumptions*) - fun forward_res nf st = - case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st) - of SOME(th,_) => th - | NONE => raise THM("forward_res", 0, [st]); +val not_conjD = thm "meson_not_conjD"; +val not_disjD = thm "meson_not_disjD"; +val not_notD = thm "meson_not_notD"; +val not_allD = thm "meson_not_allD"; +val not_exD = thm "meson_not_exD"; +val imp_to_disjD = thm "meson_imp_to_disjD"; +val not_impD = thm "meson_not_impD"; +val iff_to_disjD = thm "meson_iff_to_disjD"; +val not_iffD = thm "meson_not_iffD"; +val conj_exD1 = thm "meson_conj_exD1"; +val conj_exD2 = thm "meson_conj_exD2"; +val disj_exD = thm "meson_disj_exD"; +val disj_exD1 = thm "meson_disj_exD1"; +val disj_exD2 = thm "meson_disj_exD2"; +val disj_assoc = thm "meson_disj_assoc"; +val disj_comm = thm "meson_disj_comm"; +val disj_FalseD1 = thm "meson_disj_FalseD1"; +val disj_FalseD2 = thm "meson_disj_FalseD2"; - (*Are any of the constants in "bs" present in the term?*) - fun has_consts bs = - let fun has (Const(a,_)) = a mem bs - | has (Const ("Hilbert_Choice.Eps",_) $ _) = false - (*ignore constants within @-terms*) - | has (f$u) = has f orelse has u - | has (Abs(_,_,t)) = has t - | has _ = false - in has end; +(**** Operators for forward proof ****) + +(*raises exception if no rules apply -- unlike RL*) +fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls)) + | tryres (th, []) = raise THM("tryres", 0, [th]); + +val prop_of = #prop o rep_thm; + +(*Permits forward proof from rules that discharge assumptions*) +fun forward_res nf st = + case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st) + of SOME(th,_) => th + | NONE => raise THM("forward_res", 0, [st]); + + +(*Are any of the constants in "bs" present in the term?*) +fun has_consts bs = + let fun has (Const(a,_)) = a mem bs + | has (Const ("Hilbert_Choice.Eps",_) $ _) = false + (*ignore constants within @-terms*) + | has (f$u) = has f orelse has u + | has (Abs(_,_,t)) = has t + | has _ = false + in has end; - (**** Clause handling ****) +(**** Clause handling ****) - fun literals (Const("Trueprop",_) $ P) = literals P - | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q - | literals (Const("Not",_) $ P) = [(false,P)] - | literals P = [(true,P)]; +fun literals (Const("Trueprop",_) $ P) = literals P + | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q + | literals (Const("Not",_) $ P) = [(false,P)] + | literals P = [(true,P)]; - (*number of literals in a term*) - val nliterals = length o literals; +(*number of literals in a term*) +val nliterals = length o literals; - (*to detect, and remove, tautologous clauses*) - fun taut_lits [] = false - | taut_lits ((flg,t)::ts) = (not flg,t) mem ts orelse taut_lits ts; +(*to detect, and remove, tautologous clauses*) +fun taut_lits [] = false + | taut_lits ((flg,t)::ts) = (not flg,t) mem ts orelse taut_lits ts; - (*Include False as a literal: an occurrence of ~False is a tautology*) - fun is_taut th = taut_lits ((true, HOLogic.false_const) :: - literals (prop_of th)); +(*Include False as a literal: an occurrence of ~False is a tautology*) +fun is_taut th = taut_lits ((true, HOLogic.false_const) :: + literals (prop_of th)); - (*Generation of unique names -- maxidx cannot be relied upon to increase! - Cannot rely on "variant", since variables might coincide when literals - are joined to make a clause... - 19 chooses "U" as the first variable name*) - val name_ref = ref 19; +(*Generation of unique names -- maxidx cannot be relied upon to increase! + Cannot rely on "variant", since variables might coincide when literals + are joined to make a clause... + 19 chooses "U" as the first variable name*) +val name_ref = ref 19; - (*Replaces universally quantified variables by FREE variables -- because - assumptions may not contain scheme variables. Later, call "generalize". *) - fun freeze_spec th = - let val sth = th RS spec - val newname = (name_ref := !name_ref + 1; - radixstring(26, "A", !name_ref)) - in read_instantiate [("x", newname)] sth end; +(*Replaces universally quantified variables by FREE variables -- because + assumptions may not contain scheme variables. Later, call "generalize". *) +fun freeze_spec th = + let val sth = th RS spec + val newname = (name_ref := !name_ref + 1; + radixstring(26, "A", !name_ref)) + in read_instantiate [("x", newname)] sth end; - fun resop nf [prem] = resolve_tac (nf prem) 1; +fun resop nf [prem] = resolve_tac (nf prem) 1; - (*Conjunctive normal form, detecting tautologies early. - Strips universal quantifiers and breaks up conjunctions. *) - fun cnf_aux seen (th,ths) = - if taut_lits (literals(prop_of th) @ seen) - then ths (*tautology ignored*) - else if not (has_consts ["All","op &"] (prop_of th)) - then th::ths (*no work to do, terminate*) - else (*conjunction?*) - cnf_aux seen (th RS conjunct1, - cnf_aux seen (th RS conjunct2, ths)) - handle THM _ => (*universal quant?*) - cnf_aux seen (freeze_spec th, ths) - handle THM _ => (*disjunction?*) - let val tac = - (METAHYPS (resop (cnf_nil seen)) 1) THEN - (fn st' => st' |> - METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1) - in Seq.list_of (tac (th RS disj_forward)) @ ths end - and cnf_nil seen th = cnf_aux seen (th,[]); +(*Conjunctive normal form, detecting tautologies early. + Strips universal quantifiers and breaks up conjunctions. *) +fun cnf_aux seen (th,ths) = + if taut_lits (literals(prop_of th) @ seen) + then ths (*tautology ignored*) + else if not (has_consts ["All","op &"] (prop_of th)) + then th::ths (*no work to do, terminate*) + else (*conjunction?*) + cnf_aux seen (th RS conjunct1, + cnf_aux seen (th RS conjunct2, ths)) + handle THM _ => (*universal quant?*) + cnf_aux seen (freeze_spec th, ths) + handle THM _ => (*disjunction?*) + let val tac = + (METAHYPS (resop (cnf_nil seen)) 1) THEN + (fn st' => st' |> + METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1) + in Seq.list_of (tac (th RS disj_forward)) @ ths end +and cnf_nil seen th = cnf_aux seen (th,[]); - (*Top-level call to cnf -- it's safe to reset name_ref*) - fun cnf (th,ths) = - (name_ref := 19; cnf (th RS conjunct1, cnf (th RS conjunct2, ths)) - handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths)); +(*Top-level call to cnf -- it's safe to reset name_ref*) +fun cnf (th,ths) = + (name_ref := 19; cnf (th RS conjunct1, cnf (th RS conjunct2, ths)) + handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths)); - (**** Removal of duplicate literals ****) +(**** Removal of duplicate literals ****) - (*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) - of SOME(th,_) => th - | NONE => raise THM("forward_res2", 0, [st]); +(*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) + of SOME(th,_) => th + | NONE => raise THM("forward_res2", 0, [st]); - (*Remove duplicates in P|Q by assuming ~P in Q - rls (initially []) accumulates assumptions of the form P==>False*) - 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]) - handle THM _ => th; +(*Remove duplicates in P|Q by assuming ~P in Q + rls (initially []) accumulates assumptions of the form P==>False*) +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]) + handle THM _ => th; - (*Remove duplicate literals, if there are any*) - fun nodups th = - if null(findrep(literals(prop_of th))) then th - else nodups_aux [] th; +(*Remove duplicate literals, if there are any*) +fun nodups th = + if null(findrep(literals(prop_of th))) then th + else nodups_aux [] th; - (**** Generation of contrapositives ****) +(**** Generation of contrapositives ****) - (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*) - fun assoc_right th = assoc_right (th RS disj_assoc) - handle THM _ => th; +(*Associate disjuctions to right -- make leftmost disjunct a LITERAL*) +fun assoc_right th = assoc_right (th RS disj_assoc) + handle THM _ => th; - (*Must check for negative literal first!*) - val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule]; +(*Must check for negative literal first!*) +val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule]; - (*For ordinary resolution. *) - val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule']; +(*For ordinary resolution. *) +val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule']; - (*Create a goal or support clause, conclusing False*) - fun make_goal th = (*Must check for negative literal first!*) - make_goal (tryres(th, clause_rules)) - handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]); +(*Create a goal or support clause, conclusing False*) +fun make_goal th = (*Must check for negative literal first!*) + make_goal (tryres(th, clause_rules)) + handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]); - (*Sort clauses by number of literals*) - fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2); +(*Sort clauses by number of literals*) +fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2); - (*TAUTOLOGY CHECK SHOULD NOT BE NECESSARY!*) - fun sort_clauses ths = sort (make_ord fewerlits) (List.filter (not o is_taut) ths); +(*TAUTOLOGY CHECK SHOULD NOT BE NECESSARY!*) +fun sort_clauses ths = sort (make_ord fewerlits) (List.filter (not o is_taut) ths); - (*Convert all suitable free variables to schematic variables*) - fun generalize th = forall_elim_vars 0 (forall_intr_frees th); +(*Convert all suitable free variables to schematic variables*) +fun generalize th = forall_elim_vars 0 (forall_intr_frees th); - (*Create a meta-level Horn clause*) - fun make_horn crules th = make_horn crules (tryres(th,crules)) - handle THM _ => th; +(*Create a meta-level Horn clause*) +fun make_horn crules th = make_horn crules (tryres(th,crules)) + handle THM _ => th; - (*Generate Horn clauses for all contrapositives of a clause*) - 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)) - in case nliterals(prop_of th) of - 1 => th::hcs - | n => rots(n, assoc_right th) - end; +(*Generate Horn clauses for all contrapositives of a clause*) +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)) + in case nliterals(prop_of th) of + 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, Thm.name_thm (label ^ string_of_int k, th) :: ths) +(*Use "theorem naming" to label the clauses*) +fun name_thms label = + let fun name1 (th, (k,ths)) = + (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths) - in fn ths => #2 (foldr name1 (length ths, []) ths) end; + in fn ths => #2 (foldr name1 (length ths, []) ths) end; - (*Find an all-negative support clause*) - fun is_negative th = forall (not o #1) (literals (prop_of th)); +(*Find an all-negative support clause*) +fun is_negative th = forall (not o #1) (literals (prop_of th)); - val neg_clauses = List.filter is_negative; +val neg_clauses = List.filter is_negative; - (***** MESON PROOF PROCEDURE *****) +(***** MESON PROOF PROCEDURE *****) - fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi, - As) = rhyps(phi, A::As) - | rhyps (_, As) = As; +fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi, + As) = rhyps(phi, A::As) + | rhyps (_, As) = As; - (** Detecting repeated assumptions in a subgoal **) +(** Detecting repeated assumptions in a subgoal **) - (*The stringtree detects repeated assumptions.*) - fun ins_term (net,t) = Net.insert_term((t,t), net, op aconv); +(*The stringtree detects repeated assumptions.*) +fun ins_term (net,t) = Net.insert_term((t,t), net, op aconv); - (*detects repetitions in a list of terms*) - fun has_reps [] = false - | has_reps [_] = false - | has_reps [t,u] = (t aconv u) - | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false) - handle INSERT => true; +(*detects repetitions in a list of terms*) +fun has_reps [] = false + | has_reps [_] = false + | has_reps [t,u] = (t aconv u) + | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false) + handle INSERT => true; - (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) - fun TRYALL_eq_assume_tac 0 st = Seq.single st - | TRYALL_eq_assume_tac i st = - TRYALL_eq_assume_tac (i-1) (eq_assumption i st) - handle THM _ => TRYALL_eq_assume_tac (i-1) st; +(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) +fun TRYALL_eq_assume_tac 0 st = Seq.single st + | TRYALL_eq_assume_tac i st = + TRYALL_eq_assume_tac (i-1) (eq_assumption i st) + handle THM _ => TRYALL_eq_assume_tac (i-1) st; - (*Loop checking: FAIL if trying to prove the same thing twice - -- if *ANY* subgoal has repeated literals*) - fun check_tac st = - if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st) - then Seq.empty else Seq.single st; +(*Loop checking: FAIL if trying to prove the same thing twice + -- if *ANY* subgoal has repeated literals*) +fun check_tac st = + if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st) + then Seq.empty else Seq.single st; - (* net_resolve_tac actually made it slower... *) - fun prolog_step_tac horns i = - (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN - TRYALL eq_assume_tac; +(* net_resolve_tac actually made it slower... *) +fun prolog_step_tac horns i = + (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN + TRYALL eq_assume_tac; -in + (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*) -local fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz -in -fun size_of_subgoals st = foldr addconcl 0 (prems_of st) -end; +fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz + +fun size_of_subgoals st = foldr addconcl 0 (prems_of st); + (*Negation Normal Form*) val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, @@ -415,9 +443,7 @@ end); -(** proof method setup **) - -local +(*** proof method setup ***) fun meson_meth ctxt = Method.SIMPLE_METHOD' HEADGOAL @@ -431,7 +457,6 @@ Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o make_clauses_tac); -in val meson_setup = [Method.add_methods @@ -444,4 +469,5 @@ end; -end; +structure BasicMeson: BASIC_MESON = Meson; +open BasicMeson; diff -r d364491ba718 -r 32bee18c675f src/HOL/Tools/reconstruction.ML --- a/src/HOL/Tools/reconstruction.ML Fri Mar 04 23:25:06 2005 +0100 +++ b/src/HOL/Tools/reconstruction.ML Mon Mar 07 16:55:36 2005 +0100 @@ -107,7 +107,7 @@ val eqsubst = eq_lit_th RSN (2,rev_subst) val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) val newth' = Seq.hd (flexflex_rule newth) - in negated_asm_of_head newth' end; + in Meson.negated_asm_of_head newth' end; fun paramod_syntax ((i, B), j) (x, A) = (x, paramod_rule ((A,i), (B,j))); @@ -128,7 +128,7 @@ val newth = Seq.hd(biresolution false [(false, fmod_th)] 1 eqsubst) val offset = #maxidx(rep_thm newth) + 1 (*ensures "renaming apart" even when Vars are frozen*) - in negated_asm_of_head (thaw offset newth) end; + in Meson.negated_asm_of_head (thaw offset newth) end; fun demod_syntax ((i, B), j) (x, A) = (x, demod_rule ((A,i), (B,j))); diff -r d364491ba718 -r 32bee18c675f src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Fri Mar 04 23:25:06 2005 +0100 +++ b/src/HOL/Tools/res_axioms.ML Mon Mar 07 16:55:36 2005 +0100 @@ -265,7 +265,8 @@ rm_redundant_cls thm'' end; -fun meta_cnf_axiom thm = map (zero_var_indexes o make_meta_clause) (cnf_axiom thm); +fun meta_cnf_axiom thm = + map (zero_var_indexes o Meson.make_meta_clause) (cnf_axiom thm); (* changed: with one extra case added *)