ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
authorwenzelm
Thu Jun 12 18:54:29 2008 +0200 (2008-06-12)
changeset 27178c8ddb3000743
parent 27177 adefd3454174
child 27179 8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/metis_tools.ML	Thu Jun 12 16:42:00 2008 +0200
     1.2 +++ b/src/HOL/Tools/metis_tools.ML	Thu Jun 12 18:54:29 2008 +0200
     1.3 @@ -470,16 +470,16 @@
     1.4    (* Translation of HO Clauses                                                 *)
     1.5    (* ------------------------------------------------------------------------- *)
     1.6  
     1.7 -  fun cnf_th th = hd (ResAxioms.cnf_axiom th);
     1.8 +  fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th);
     1.9  
    1.10 -  val equal_imp_fequal' = cnf_th (thm"equal_imp_fequal");
    1.11 -  val fequal_imp_equal' = cnf_th (thm"fequal_imp_equal");
    1.12 +  val equal_imp_fequal' = cnf_th @{theory} (thm"equal_imp_fequal");
    1.13 +  val fequal_imp_equal' = cnf_th @{theory} (thm"fequal_imp_equal");
    1.14  
    1.15 -  val comb_I = cnf_th ResHolClause.comb_I;
    1.16 -  val comb_K = cnf_th ResHolClause.comb_K;
    1.17 -  val comb_B = cnf_th ResHolClause.comb_B;
    1.18 -  val comb_C = cnf_th ResHolClause.comb_C;
    1.19 -  val comb_S = cnf_th ResHolClause.comb_S;
    1.20 +  val comb_I = cnf_th @{theory} ResHolClause.comb_I;
    1.21 +  val comb_K = cnf_th @{theory} ResHolClause.comb_K;
    1.22 +  val comb_B = cnf_th @{theory} ResHolClause.comb_B;
    1.23 +  val comb_C = cnf_th @{theory} ResHolClause.comb_C;
    1.24 +  val comb_S = cnf_th @{theory} ResHolClause.comb_S;
    1.25  
    1.26    fun type_ext thy tms =
    1.27      let val subs = ResAtp.tfree_classes_of_terms tms
    1.28 @@ -567,7 +567,8 @@
    1.29  
    1.30    (* Main function to start metis prove and reconstruction *)
    1.31    fun FOL_SOLVE mode ctxt cls ths0 =
    1.32 -    let val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom th)) ths0
    1.33 +    let val thy = ProofContext.theory_of ctxt
    1.34 +        val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
    1.35          val ths = List.concat (map #2 th_cls_pairs)
    1.36          val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause"
    1.37                  else ();
     2.1 --- a/src/HOL/Tools/res_atp.ML	Thu Jun 12 16:42:00 2008 +0200
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Jun 12 18:54:29 2008 +0200
     2.3 @@ -570,8 +570,10 @@
     2.4  (***************************************************************)
     2.5  
     2.6  fun cnf_hyps_thms ctxt =
     2.7 -    let val ths = Assumption.prems_of ctxt
     2.8 -    in fold (fold (insert Thm.eq_thm) o ResAxioms.cnf_axiom) ths [] end;
     2.9 +  let
    2.10 +    val thy = ProofContext.theory_of ctxt
    2.11 +    val hyps = Assumption.prems_of ctxt
    2.12 +  in fold (fold (insert Thm.eq_thm) o ResAxioms.cnf_axiom thy) hyps [] end;
    2.13  
    2.14  (*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
    2.15  datatype mode = Auto | Fol | Hol;
    2.16 @@ -646,10 +648,10 @@
    2.17                            | Hol => false
    2.18          val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
    2.19          val cla_simp_atp_clauses = included_thms
    2.20 -                                     |> ResAxioms.cnf_rules_pairs |> make_unique
    2.21 +                                     |> ResAxioms.cnf_rules_pairs thy |> make_unique
    2.22                                       |> restrict_to_logic thy isFO
    2.23                                       |> remove_unwanted_clauses
    2.24 -        val user_cls = ResAxioms.cnf_rules_pairs user_rules
    2.25 +        val user_cls = ResAxioms.cnf_rules_pairs thy user_rules
    2.26          val axclauses = make_unique (user_cls @ relevance_filter thy cla_simp_atp_clauses goal_tms)
    2.27          val subs = tfree_classes_of_terms goal_tms
    2.28          and axtms = map (prop_of o #1) axclauses
    2.29 @@ -729,11 +731,11 @@
    2.30  			| Fol => true
    2.31  			| Hol => false
    2.32        val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
    2.33 -      val included_cls = included_thms |> ResAxioms.cnf_rules_pairs |> make_unique
    2.34 +      val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
    2.35                                         |> restrict_to_logic thy isFO
    2.36                                         |> remove_unwanted_clauses
    2.37        val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
    2.38 -      val white_cls = ResAxioms.cnf_rules_pairs white_thms
    2.39 +      val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
    2.40        (*clauses relevant to goal gl*)
    2.41        val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls
    2.42        val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))
     3.1 --- a/src/HOL/Tools/res_hol_clause.ML	Thu Jun 12 16:42:00 2008 +0200
     3.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Thu Jun 12 18:54:29 2008 +0200
     3.3 @@ -395,7 +395,8 @@
     3.4    if axiom_name mem_string user_lemmas then foldl count_literal ct literals
     3.5    else ct;
     3.6  
     3.7 -val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname)
     3.8 +fun cnf_helper_thms thy =
     3.9 +  ResAxioms.cnf_rules_pairs thy o map ResAxioms.pairname
    3.10  
    3.11  fun get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas) =
    3.12    if isFO then []  (*first-order*)
    3.13 @@ -404,15 +405,15 @@
    3.14          val ct = foldl (count_user_clause user_lemmas) ct0 axclauses
    3.15          fun needed c = valOf (Symtab.lookup ct c) > 0
    3.16          val IK = if needed "c_COMBI" orelse needed "c_COMBK"
    3.17 -                 then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms [comb_I,comb_K])
    3.18 +                 then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms thy [comb_I,comb_K])
    3.19                   else []
    3.20          val BC = if needed "c_COMBB" orelse needed "c_COMBC"
    3.21 -                 then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms [comb_B,comb_C])
    3.22 +                 then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms thy [comb_B,comb_C])
    3.23                   else []
    3.24          val S = if needed "c_COMBS"
    3.25 -                then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S])
    3.26 +                then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms thy [comb_S])
    3.27                  else []
    3.28 -        val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
    3.29 +        val other = cnf_helper_thms thy [ext,fequal_imp_equal,equal_imp_fequal]
    3.30      in
    3.31          map #2 (make_axiom_clauses thy (other @ IK @ BC @ S))
    3.32      end;