# HG changeset patch # User wenzelm # Date 1213289669 -7200 # Node ID c8ddb3000743d0a46ee2b8f113eadd04cdb9d175 # Parent adefd34541741914804aa148893be971f7ebadc9 ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context; diff -r adefd3454174 -r c8ddb3000743 src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Thu Jun 12 16:42:00 2008 +0200 +++ b/src/HOL/Tools/metis_tools.ML Thu Jun 12 18:54:29 2008 +0200 @@ -470,16 +470,16 @@ (* Translation of HO Clauses *) (* ------------------------------------------------------------------------- *) - fun cnf_th th = hd (ResAxioms.cnf_axiom th); + fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th); - val equal_imp_fequal' = cnf_th (thm"equal_imp_fequal"); - val fequal_imp_equal' = cnf_th (thm"fequal_imp_equal"); + val equal_imp_fequal' = cnf_th @{theory} (thm"equal_imp_fequal"); + val fequal_imp_equal' = cnf_th @{theory} (thm"fequal_imp_equal"); - val comb_I = cnf_th ResHolClause.comb_I; - val comb_K = cnf_th ResHolClause.comb_K; - val comb_B = cnf_th ResHolClause.comb_B; - val comb_C = cnf_th ResHolClause.comb_C; - val comb_S = cnf_th ResHolClause.comb_S; + val comb_I = cnf_th @{theory} ResHolClause.comb_I; + val comb_K = cnf_th @{theory} ResHolClause.comb_K; + val comb_B = cnf_th @{theory} ResHolClause.comb_B; + val comb_C = cnf_th @{theory} ResHolClause.comb_C; + val comb_S = cnf_th @{theory} ResHolClause.comb_S; fun type_ext thy tms = let val subs = ResAtp.tfree_classes_of_terms tms @@ -567,7 +567,8 @@ (* Main function to start metis prove and reconstruction *) fun FOL_SOLVE mode ctxt cls ths0 = - let val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom th)) ths0 + let val thy = ProofContext.theory_of ctxt + val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0 val ths = List.concat (map #2 th_cls_pairs) val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause" else (); diff -r adefd3454174 -r c8ddb3000743 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Jun 12 16:42:00 2008 +0200 +++ b/src/HOL/Tools/res_atp.ML Thu Jun 12 18:54:29 2008 +0200 @@ -570,8 +570,10 @@ (***************************************************************) fun cnf_hyps_thms ctxt = - let val ths = Assumption.prems_of ctxt - in fold (fold (insert Thm.eq_thm) o ResAxioms.cnf_axiom) ths [] end; + let + val thy = ProofContext.theory_of ctxt + val hyps = Assumption.prems_of ctxt + in fold (fold (insert Thm.eq_thm) o ResAxioms.cnf_axiom thy) hyps [] end; (*Translation mode can be auto-detected, or forced to be first-order or higher-order*) datatype mode = Auto | Fol | Hol; @@ -646,10 +648,10 @@ | Hol => false val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms val cla_simp_atp_clauses = included_thms - |> ResAxioms.cnf_rules_pairs |> make_unique + |> ResAxioms.cnf_rules_pairs thy |> make_unique |> restrict_to_logic thy isFO |> remove_unwanted_clauses - val user_cls = ResAxioms.cnf_rules_pairs user_rules + val user_cls = ResAxioms.cnf_rules_pairs thy user_rules val axclauses = make_unique (user_cls @ relevance_filter thy cla_simp_atp_clauses goal_tms) val subs = tfree_classes_of_terms goal_tms and axtms = map (prop_of o #1) axclauses @@ -729,11 +731,11 @@ | Fol => true | Hol => false val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths - val included_cls = included_thms |> ResAxioms.cnf_rules_pairs |> make_unique + val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique |> restrict_to_logic thy isFO |> remove_unwanted_clauses val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls)) - val white_cls = ResAxioms.cnf_rules_pairs white_thms + val white_cls = ResAxioms.cnf_rules_pairs thy white_thms (*clauses relevant to goal gl*) val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls))) diff -r adefd3454174 -r c8ddb3000743 src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Thu Jun 12 16:42:00 2008 +0200 +++ b/src/HOL/Tools/res_hol_clause.ML Thu Jun 12 18:54:29 2008 +0200 @@ -395,7 +395,8 @@ if axiom_name mem_string user_lemmas then foldl count_literal ct literals else ct; -val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname) +fun cnf_helper_thms thy = + ResAxioms.cnf_rules_pairs thy o map ResAxioms.pairname fun get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas) = if isFO then [] (*first-order*) @@ -404,15 +405,15 @@ val ct = foldl (count_user_clause user_lemmas) ct0 axclauses fun needed c = valOf (Symtab.lookup ct c) > 0 val IK = if needed "c_COMBI" orelse needed "c_COMBK" - then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms [comb_I,comb_K]) + then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms thy [comb_I,comb_K]) else [] val BC = if needed "c_COMBB" orelse needed "c_COMBC" - then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms [comb_B,comb_C]) + then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms thy [comb_B,comb_C]) else [] val S = if needed "c_COMBS" - then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S]) + then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms thy [comb_S]) else [] - val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal] + val other = cnf_helper_thms thy [ext,fequal_imp_equal,equal_imp_fequal] in map #2 (make_axiom_clauses thy (other @ IK @ BC @ S)) end;