# HG changeset patch # User paulson # Date 1161852515 -7200 # Node ID 7f2ebe5c5b722ca5d7631e321f9cc4ceda7d8c4f # Parent 286d68ce3f5bb7b5a6b090dfb9dce7b0206424e2 Conversion to clause form now tolerates Boolean variables without looping. Attribute "clausify" moved to res_axioms; rest of reconstruction.ML deleted diff -r 286d68ce3f5b -r 7f2ebe5c5b72 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Oct 24 12:02:53 2006 +0200 +++ b/src/HOL/IsaMakefile Thu Oct 26 10:48:35 2006 +0200 @@ -110,7 +110,7 @@ Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/prop_logic.ML \ Tools/polyhash.ML \ Tools/recdef_package.ML Tools/recfun_codegen.ML \ - Tools/reconstruction.ML Tools/record_package.ML Tools/refute.ML \ + Tools/record_package.ML Tools/refute.ML \ Tools/refute_isar.ML Tools/res_atp.ML Tools/res_axioms.ML \ Tools/res_clause.ML Tools/rewrite_hol_proof.ML \ Tools/sat_funcs.ML \ diff -r 286d68ce3f5b -r 7f2ebe5c5b72 src/HOL/Reconstruction.thy --- a/src/HOL/Reconstruction.thy Tue Oct 24 12:02:53 2006 +0200 +++ b/src/HOL/Reconstruction.thy Thu Oct 26 10:48:35 2006 +0200 @@ -16,7 +16,6 @@ ("Tools/res_hol_clause.ML") ("Tools/res_axioms.ML") ("Tools/res_atp.ML") - ("Tools/reconstruction.ML") begin @@ -72,13 +71,10 @@ apply (simp add: COMBB_def) done - use "Tools/res_axioms.ML" use "Tools/res_hol_clause.ML" use "Tools/res_atp.ML" -use "Tools/reconstruction.ML" setup ResAxioms.meson_method_setup -setup Reconstruction.setup end diff -r 286d68ce3f5b -r 7f2ebe5c5b72 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Tue Oct 24 12:02:53 2006 +0200 +++ b/src/HOL/Tools/meson.ML Thu Oct 26 10:48:35 2006 +0200 @@ -312,9 +312,14 @@ (**** Generation of contrapositives ****) +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 = assoc_right (th RS disj_assoc) - handle THM _ => th; +fun assoc_right th = + if is_left (prop_of th) then assoc_right (th RS disj_assoc) + else th; (*Must check for negative literal first!*) val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule]; @@ -349,18 +354,25 @@ exists_Const (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T)); -(*Raises an exception if any Vars in the theorem mention type bool; they - could cause make_horn to loop! Also rejects functions whose arguments are - Booleans or other functions.*) +(*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 t = not (exists (has_bool o fastype_of) (term_vars t) orelse not (Term.is_first_order ["all","All","Ex"] t) orelse has_bool_arg_const t orelse has_meta_conn t); +fun rigid t = not (is_Var (head_of t)); + +fun ok4horn (Const ("Trueprop",_) $ (Const ("op |", _) $ t $ _)) = rigid t + | ok4horn (Const ("Trueprop",_) $ t) = rigid t + | ok4horn _ = false; + (*Create a meta-level Horn clause*) -fun make_horn crules th = make_horn crules (tryres(th,crules)) - handle THM _ => th; +fun make_horn crules th = + if ok4horn (concl_of th) + then make_horn crules (tryres(th,crules)) handle THM _ => th + else th; (*Generate Horn clauses for all contrapositives of a clause. The input, th, is a HOL disjunction.*) @@ -434,11 +446,18 @@ val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, not_impD, not_iffD, not_allD, not_exD, not_notD]; -fun make_nnf1 th = make_nnf1 (tryres(th, nnf_rls)) +fun ok4nnf (Const ("Trueprop",_) $ (Const ("Not", _) $ t)) = rigid t + | ok4nnf (Const ("Trueprop",_) $ t) = rigid t + | ok4nnf _ = false; + +fun make_nnf1 th = + if ok4nnf (concl_of th) + then make_nnf1 (tryres(th, nnf_rls)) handle THM _ => forward_res make_nnf1 (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) - handle THM _ => th; + handle THM _ => th + else th; (*The simplification removes defined quantifiers and occurrences of True and False. nnf_ss also includes the one-point simprocs, @@ -455,7 +474,7 @@ fun make_nnf th = case prems_of th of [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps) - |> simplify nnf_ss (*But this doesn't simplify premises...*) + |> simplify nnf_ss |> make_nnf1 | _ => raise THM ("make_nnf: premises in argument", 0, [th]); @@ -587,10 +606,8 @@ (*Converting one clause*) fun make_meta_clause th = - if is_fol_term (prop_of th) - then negated_asm_of_head (make_horn resolution_clause_rules th) - else raise THM("make_meta_clause", 0, [th]); - + negated_asm_of_head (make_horn resolution_clause_rules th); + fun make_meta_clauses ths = name_thms "MClause#" (distinct Drule.eq_thm_prop (map make_meta_clause ths)); diff -r 286d68ce3f5b -r 7f2ebe5c5b72 src/HOL/Tools/reconstruction.ML --- a/src/HOL/Tools/reconstruction.ML Tue Oct 24 12:02:53 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,120 +0,0 @@ -(* Title: HOL/Reconstruction.thy - ID: $Id$ - Author: Lawrence C Paulson and Claire Quigley - Copyright 2004 University of Cambridge -*) - -(*Attributes for reconstructing external resolution proofs*) - -structure Reconstruction = -struct - -(**** attributes ****) - -(** Binary resolution **) - -fun binary_rule ((cl1, lit1), (cl2 , lit2)) = - select_literal (lit1 + 1) cl1 - RSN ((lit2 + 1), cl2); - -val binary = Attrib.syntax - (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat - >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => binary_rule ((A, i), (B, j))))); - - -(** Factoring **) - -(*NB this code did not work at all before 29/6/2006. Even now its behaviour may - not be as expected. It unifies the designated literals - and then deletes ALL duplicates of literals (not just those designated)*) - -fun mksubstlist [] sublist = sublist - | mksubstlist ((a, (T, b)) :: rest) sublist = - mksubstlist rest ((Var(a,T), b)::sublist); - -fun reorient (x,y) = - if is_Var x then (x,y) - else if is_Var y then (y,x) - else error "Reconstruction.reorient: neither term is a Var"; - -fun inst_subst sign subst cl = - let val subst' = map (pairself (cterm_of sign) o reorient) subst - in - Seq.hd(distinct_subgoals_tac (cterm_instantiate subst' cl)) - end; - -fun getnewenv seq = fst (fst (the (Seq.pull seq))); - -fun factor_rule (cl, lit1, lit2) = - let - val prems = prems_of cl - val fac1 = List.nth (prems,lit1) - val fac2 = List.nth (prems,lit2) - val sign = sign_of_thm cl - val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)]) - val newenv = getnewenv unif_env - val envlist = Envir.alist_of newenv - in - inst_subst sign (mksubstlist envlist []) cl - end; - -val factor = Attrib.syntax (Scan.lift (Args.nat -- Args.nat) - >> (fn (i, j) => Thm.rule_attribute (fn _ => fn A => factor_rule (A, i, j)))); - - -(** Paramodulation **) - -(*subst with premises exchanged: that way, side literals of the equality will appear - as the second to last premises of the result.*) -val rev_subst = rotate_prems 1 subst; - -fun paramod_rule ((cl1, lit1), (cl2, lit2)) = - let val eq_lit_th = select_literal (lit1+1) cl1 - val mod_lit_th = select_literal (lit2+1) cl2 - 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 Meson.negated_asm_of_head newth' end; - - -val paramod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat - >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => paramod_rule ((A, i), (B, j))))); - - -(** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **) - -fun demod_rule ctxt ((cl1, lit1), (cl2 , lit2)) = - let val eq_lit_th = select_literal (lit1+1) cl1 - val mod_lit_th = select_literal (lit2+1) cl2 - val ((_, [fmod_th]), ctxt') = Variable.import true [mod_lit_th] ctxt - val eqsubst = eq_lit_th RSN (2,rev_subst) - val newth = - Seq.hd (biresolution false [(false, fmod_th)] 1 eqsubst) - |> singleton (Variable.export ctxt' ctxt) - in Meson.negated_asm_of_head newth end; - -val demod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat - >> (fn ((i, B), j) => Thm.rule_attribute (fn context => fn A => - demod_rule (Context.proof_of context) ((A, i), (B, j))))); - - -(** Conversion of a theorem into clauses **) - -(*For efficiency, we rely upon memo-izing in ResAxioms.*) -fun clausify_rule (th,i) = List.nth (ResAxioms.meta_cnf_axiom th, i) - -val clausify = Attrib.syntax (Scan.lift Args.nat - >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i)))); - - -(** theory setup **) - -val setup = - Attrib.add_attributes - [("binary", binary, "binary resolution"), - ("paramod", paramod, "paramodulation"), - ("demod", demod, "demodulation"), - ("factor", factor, "factoring"), - ("clausify", clausify, "conversion to clauses")]; - -end diff -r 286d68ce3f5b -r 7f2ebe5c5b72 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Tue Oct 24 12:02:53 2006 +0200 +++ b/src/HOL/Tools/res_axioms.ML Thu Oct 26 10:48:35 2006 +0200 @@ -590,9 +590,6 @@ fun pairname th = (Thm.name_of_thm th, th); -fun meta_cnf_axiom th = - map Meson.make_meta_clause (cnf_axiom (pairname th)); - (*Principally for debugging*) fun cnf_name s = let val th = thm s @@ -695,9 +692,16 @@ [("meson", Method.thms_ctxt_args meson_meth, "MESON resolution proof procedure")]; +(** Attribute for converting a theorem into clauses **) +fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom (pairname th)); -(*** The Skolemization attribute ***) +fun clausify_rule (th,i) = List.nth (meta_cnf_axiom th, i) + +val clausify = Attrib.syntax (Scan.lift Args.nat + >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i)))); + +(** The Skolemization attribute **) fun conj2_rule (th1,th2) = conjI OF [th1,th2]; @@ -712,8 +716,9 @@ | skolem_attr (context, th) = (context, conj_rule (skolem_use_cache_thm th)); val setup_attrs = Attrib.add_attributes - [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem")]; - + [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"), + ("clausify", clausify, "conversion to clauses")]; + val setup = clause_cache_setup #> setup_attrs; end;