# HG changeset patch # User paulson # Date 1114703818 -7200 # Node ID 8336ff711d80fdb0d564b38b5ab1c93e2eed9576 # Parent e524119dbf1934dfa8ad609108b455645d231d15 fixed treatment of higher-order simprules diff -r e524119dbf19 -r 8336ff711d80 src/HOL/Main.thy --- a/src/HOL/Main.thy Thu Apr 28 17:08:08 2005 +0200 +++ b/src/HOL/Main.thy Thu Apr 28 17:56:58 2005 +0200 @@ -6,7 +6,7 @@ header {* Main HOL *} theory Main - imports Extraction Refute Reconstruction + imports Refute Reconstruction begin diff -r e524119dbf19 -r 8336ff711d80 src/HOL/Reconstruction.thy --- a/src/HOL/Reconstruction.thy Thu Apr 28 17:08:08 2005 +0200 +++ b/src/HOL/Reconstruction.thy Thu Apr 28 17:56:58 2005 +0200 @@ -7,7 +7,7 @@ header{*Attributes for Reconstructing External Resolution Proofs*} theory Reconstruction - imports Hilbert_Choice Map Infinite_Set + imports Hilbert_Choice Map Infinite_Set Extraction files "Tools/res_lib.ML" "Tools/res_clause.ML" "Tools/res_skolem_function.ML" diff -r e524119dbf19 -r 8336ff711d80 src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Thu Apr 28 17:08:08 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Thu Apr 28 17:56:58 2005 +0200 @@ -170,9 +170,6 @@ -fun thm_is_fol (x, thm) = rule_is_fol thm - - fun get_simp_metas [] = [[]] | get_simp_metas (x::xs) = let val metas = ResAxioms.meta_cnf_axiom x in @@ -208,7 +205,7 @@ val names_rules = ListPair.zip (good_names,name_fol_cs); - val new_clasrls = #1(ResAxioms.clausify_classical_rules name_fol_cs[]) + val new_clasrls = #1(ResAxioms.clausify_rules name_fol_cs[]) val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls; @@ -251,11 +248,10 @@ val simp_names = map #1 named_simps; val simp_rules = map #2 named_simps; - val (simpset_cls,badthms) = ResAxioms.clausify_simpset_rules simp_rules []; + val (simpset_cls,badthms) = ResAxioms.clausify_rules simp_rules []; (* 1137 clausif simps *) - val clausifiable_simps = remove_all_simps badthms named_simps; + val name_fol_simps = remove_all_simps badthms named_simps; - val name_fol_simps = List.filter thm_is_fol clausifiable_simps ; val simp_names = map #1 name_fol_simps; val simp_rules = map #2 name_fol_simps; @@ -263,7 +259,7 @@ (* need to get names of claset_cluases so we can make sure we've*) (* got the same ones (ie. the named ones ) as the claset rules *) (* length 1374*) - val new_simps = #1(ResAxioms.clausify_simpset_rules simp_rules []); + val new_simps = #1(ResAxioms.clausify_rules simp_rules []); val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps; val stick_strs = map stick simpset_tptp_strs; diff -r e524119dbf19 -r 8336ff711d80 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Thu Apr 28 17:08:08 2005 +0200 +++ b/src/HOL/Tools/meson.ML Thu Apr 28 17:56:58 2005 +0200 @@ -307,7 +307,11 @@ (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) handle THM _ => th; -fun make_nnf th = make_nnf1 (check_no_bool th); +(*The simplification removes occurrences of True and False.*) +val nnf_ss = HOL_basic_ss addsimps Ball_def::Bex_def::simp_thms; + +fun make_nnf th = th |> simplify nnf_ss + |> check_no_bool |> make_nnf1 (*Pull existential quantifiers (Skolemization)*) fun skolemize th = diff -r e524119dbf19 -r 8336ff711d80 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Thu Apr 28 17:08:08 2005 +0200 +++ b/src/HOL/Tools/res_axioms.ML Thu Apr 28 17:56:58 2005 +0200 @@ -141,75 +141,6 @@ end; -(* some lemmas *) - -Goal "(P==True) ==> P"; -by(Blast_tac 1); -qed "Eq_TrueD1"; - -Goal "(True==P) ==> P"; -by(Blast_tac 1); -qed "Eq_TrueD2"; - -Goal "(P=True) ==> P"; -by(Blast_tac 1); -qed "Eq_TrueD3"; - -Goal "(P==False) ==> ~P"; -by(Blast_tac 1); -qed "Eq_FalseD1"; - -Goal "(False==P) ==> ~P"; -by(Blast_tac 1); -qed "Eq_FalseD2"; - -Goal "(P=False) ==> ~P"; -by(Blast_tac 1); -qed "Eq_FalseD3"; - - -Goal "[|u == (if P then x else y); P|] ==> u==x"; -by Auto_tac; -qed "eq_if_elim1"; - - -Goal "[|u == (if P then x else y); ~P|] ==> u==y"; -by Auto_tac; -qed"eq_if_elim2"; - - - -fun resolve_or_id ths th = - case [th] RL ths of - [] => [th] - | ths2 => ths2; - - - -val remove_bool_ths = [eq_if_elim1,eq_if_elim2,Eq_TrueD1,Eq_TrueD2,Eq_FalseD1,Eq_FalseD2]; - - - -local - - fun prove s = prove_goal (the_context()) s (fn _ => [Simp_tac 1]); - -val small_simps = - map prove - ["(P | True) == True", "(True | P) == True", - "(P & True) == P", "(True & P) == P", - "(False | P) == P", "(P | False) == P", - "(False & P) == False", "(P & False) == False", - "~True == False", "~False == True"(*, - "(False = P) == ~P", "(P = False) == ~P", - "(True = P) == P", "(P = True) == P"*) - (*"(True ==> PROP P) == PROP P"*)]; -in - -val small_simpset = empty_ss addsimps small_simps - -end; - signature RES_AXIOMS = sig @@ -230,8 +161,7 @@ : (Term.term * Term.term) list -> Thm.thm list -> Term.term list val claset_rules_of_thy : Theory.theory -> Thm.thm list val simpset_rules_of_thy : Theory.theory -> (string * Thm.thm) list -val clausify_simpset_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list -val clausify_classical_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list +val clausify_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list end; @@ -258,25 +188,19 @@ end; - -(* added this function to remove True/False in a theorem that is in NNF form. *) -fun rm_TF_nnf thm = simplify small_simpset thm; - - (* convert a theorem into NNF and also skolemize it. *) fun skolem_axiom thm = - let val thm' = (skolemize o rm_TF_nnf o make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) thm + if Term.is_first_order (prop_of thm) then + let val thm' = (skolemize o make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) thm in repeat_RS thm' someI_ex - end; + end + else raise THM ("skolem_axiom: not first-order", 0, [thm]); -fun isa_cls thm = make_clauses [skolem_axiom thm] +fun cnf_rule thm = make_clauses [skolem_axiom thm] -fun cnf_elim thm = isa_cls (transform_elim thm); - -val cnf_rule = isa_cls; - +fun cnf_elim thm = cnf_rule (transform_elim thm); (*Transfer a theorem in to theory Reconstruction.thy if it is not already @@ -383,16 +307,11 @@ fun make_axiom_clauses _ [] = [] | make_axiom_clauses i (cls::clss) = (ResClause.make_axiom_clause cls (thm_name,i)) :: make_axiom_clauses (i+1) clss in - make_axiom_clauses 0 isa_clauses' - + make_axiom_clauses 0 isa_clauses' end; -(******** Extracting and CNF/Clausify theorems from a classical reasoner and simpset of a given theory ******) - - -fun retr_thms ([]:MetaSimplifier.rrule list) = [] - | retr_thms (r::rs) = (#name r, #thm r)::(retr_thms rs); +(**** Extract and Clausify theorems from a theory's claset and simpset ****) fun claset_rules_of_thy thy = let val clsset = rep_cs (claset_of thy) @@ -405,89 +324,48 @@ end; fun simpset_rules_of_thy thy = - let val simpset = simpset_of thy - val rules = #rules(fst (rep_ss simpset)) - val thms = retr_thms (map #2 (Net.dest rules)) + let val rules = #rules(fst (rep_ss (simpset_of thy))) in - thms + map (fn (_,r) => (#name r, #thm r)) (Net.dest rules) end; -(**** Translate a set of classical rules or simplifier rules into CNF (still as type "thm") from a given theory ****) +(**** Translate a set of classical/simplifier rules into CNF (still as type "thm") ****) (* classical rules *) -fun cnf_classical_rules [] err_list = ([],err_list) - | cnf_classical_rules (thm::thms) err_list = - let val (ts,es) = cnf_classical_rules thms err_list - in - ((cnf_axiom thm)::ts,es) handle _ => (ts,(thm::es)) - end; +fun cnf_rules [] err_list = ([],err_list) + | cnf_rules (thm::thms) err_list = + let val (ts,es) = cnf_rules thms err_list + in (cnf_axiom thm :: ts,es) handle _ => (ts,(thm::es)) end; (* CNF all rules from a given theory's classical reasoner *) fun cnf_classical_rules_thy thy = - let val rules = claset_rules_of_thy thy - in - cnf_classical_rules rules [] - end; - - -(* simplifier rules *) -fun cnf_simpset_rules [] err_list = ([],err_list) - | cnf_simpset_rules (thm::thms) err_list = - let val (ts,es) = cnf_simpset_rules thms err_list - val thm' = resolve_or_id remove_bool_ths thm - in - ((map cnf_axiom thm')@ts,es) handle _ => (ts,(thm::es)) - end; - + cnf_rules (claset_rules_of_thy thy) []; (* CNF all simplifier rules from a given theory's simpset *) fun cnf_simpset_rules_thy thy = - let val thms = map #2 (simpset_rules_of_thy thy) - in - cnf_simpset_rules thms [] - end; - + cnf_rules (map #2 (simpset_rules_of_thy thy)) []; -(**** Convert all theorems of a classical reason/simpset into clauses (ResClause.clause) ****) +(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****) (* classical rules *) -fun clausify_classical_rules [] err_list = ([],err_list) - | clausify_classical_rules (thm::thms) err_list = - let val (ts,es) = clausify_classical_rules thms err_list +fun clausify_rules [] err_list = ([],err_list) + | clausify_rules (thm::thms) err_list = + let val (ts,es) = clausify_rules thms err_list in ((clausify_axiom thm)::ts,es) handle _ => (ts,(thm::es)) end; - (* convert all classical rules from a given theory into Clause.clause format. *) fun clausify_classical_rules_thy thy = - let val rules = claset_rules_of_thy thy - in - clausify_classical_rules rules [] - end; - - -(* simplifier rules *) -fun clausify_simpset_rules [] err_list = ([],err_list) - | clausify_simpset_rules (thm::thms) err_list = - let val (ts,es) = clausify_simpset_rules thms err_list - in - ((clausify_axiom thm)::ts,es) handle _ => (ts,(thm::es)) - end; - + clausify_rules (claset_rules_of_thy thy) []; (* convert all simplifier rules from a given theory into Clause.clause format. *) fun clausify_simpset_rules_thy thy = - let val thms = map #2 (simpset_rules_of_thy thy) - in - clausify_simpset_rules thms [] - end; - - + clausify_rules (map #2 (simpset_rules_of_thy thy)) []; end;