# HG changeset patch # User paulson # Date 1157093513 -7200 # Node ID 85414caac94a1c653e6d7e2b15229c89f437c0d3 # Parent 42be3a46dcd8c45bbafbf7ec653a45bbf371a296 refinements to conversion into clause form, esp for the HO case diff -r 42be3a46dcd8 -r 85414caac94a src/HOL/Tools/ATP/reduce_axiomsN.ML --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML Fri Sep 01 08:36:55 2006 +0200 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML Fri Sep 01 08:51:53 2006 +0200 @@ -2,9 +2,16 @@ ID: $Id$ Filtering strategies *) +(*A surprising number of theorems contain only a few significant constants. + These include all induction rules, and other general theorems. Filtering + theorems in clause form reveals these complexities in the form of Skolem + functions. If we were instead to filter theorems in their natural form, + some other method of measuring theorem complexity would become necessary.*) + structure ReduceAxiomsN = struct +val run_relevance_filter = ref true; val pass_mark = ref 0.6; val convergence = ref 2.4; (*Higher numbers allow longer inference chains*) val follow_defs = ref false; (*Follow definitions. Makes problems bigger.*) @@ -19,8 +26,8 @@ (*Including equality in this list might be expected to stop rules like subset_antisym from being chosen, but for some reason filtering works better with them listed.*) val standard_consts = - ["Trueprop","==>","all","Ex","op &","op |","Not","All","op -->", - "op =","==","True","False"]; + ["Trueprop","==>","all","==","All","Ex","Ball","Bex","op &","op |","Not","op -->", + "op =","True","False"]; (*** constants with types ***) @@ -74,7 +81,7 @@ val null_const_tab : const_typ list list Symtab.table = foldl add_standard_const Symtab.empty standard_consts; -fun get_goal_consts_typs thy cs = foldl (add_term_consts_typs_rm thy) null_const_tab cs; +fun get_goal_consts_typs thy = foldl (add_term_consts_typs_rm thy) null_const_tab; (**** Constant / Type Frequencies ****) @@ -201,8 +208,8 @@ end; fun relevance_filter thy axioms goals = - if !pass_mark < 0.1 then axioms - else map #1 (relevance_filter_aux thy axioms goals); - + if !run_relevance_filter andalso !pass_mark >= 0.1 + then map #1 (relevance_filter_aux thy axioms goals) + else axioms end; diff -r 42be3a46dcd8 -r 85414caac94a src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Fri Sep 01 08:36:55 2006 +0200 +++ b/src/HOL/Tools/res_atp.ML Fri Sep 01 08:51:53 2006 +0200 @@ -5,6 +5,7 @@ ATPs with TPTP format input. *) +(*FIXME: Do we need this signature?*) signature RES_ATP = sig val prover: string ref @@ -52,7 +53,7 @@ val rm_clasimp : unit -> unit end; -structure ResAtp : RES_ATP = +structure ResAtp = struct (********************************************************************) @@ -159,7 +160,7 @@ (**** relevance filter ****) -val run_relevance_filter = ref true; +val run_relevance_filter = ReduceAxiomsN.run_relevance_filter; val run_blacklist_filter = ref true; (******************************************************************) @@ -173,11 +174,9 @@ | string_of_logic HOLC = "HOLC" | string_of_logic HOLCS = "HOLCS"; - fun is_fol_logic FOL = true | is_fol_logic _ = false - (*HOLCS will not occur here*) fun upgrade_lg HOLC _ = HOLC | upgrade_lg HOL HOLC = HOLC @@ -216,51 +215,47 @@ fun term_lg [] (lg,seen) = (lg,seen) | term_lg (tm::tms) (FOL,seen) = - let val (f,args) = strip_comb tm - val (lg',seen') = if f mem seen then (FOL,seen) - else fn_lg f (FOL,seen) - val _ = - if is_fol_logic lg' then () - else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f) - in - term_lg (args@tms) (lg',seen') - end + let val (f,args) = strip_comb tm + val (lg',seen') = if f mem seen then (FOL,seen) + else fn_lg f (FOL,seen) + in + if is_fol_logic lg' then () + else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f); + term_lg (args@tms) (lg',seen') + end | term_lg _ (lg,seen) = (lg,seen) exception PRED_LG of term; fun pred_lg (t as Const(P,tp)) (lg,seen)= - if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) + if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) | pred_lg (t as Free(P,tp)) (lg,seen) = - if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) + if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen) | pred_lg P _ = raise PRED_LG(P); fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen) | lit_lg P (lg,seen) = - let val (pred,args) = strip_comb P - val (lg',seen') = if pred mem seen then (lg,seen) - else pred_lg pred (lg,seen) - val _ = - if is_fol_logic lg' then () - else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred) - in + let val (pred,args) = strip_comb P + val (lg',seen') = if pred mem seen then (lg,seen) + else pred_lg pred (lg,seen) + in + if is_fol_logic lg' then () + else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred); term_lg args (lg',seen') - end; + end; fun lits_lg [] (lg,seen) = (lg,seen) | lits_lg (lit::lits) (FOL,seen) = - let val (lg,seen') = lit_lg lit (FOL,seen) - val _ = - if is_fol_logic lg then () - else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit) - in + let val (lg,seen') = lit_lg lit (FOL,seen) + in + if is_fol_logic lg then () + else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit); lits_lg lits (lg,seen') - end + end | lits_lg lits (lg,seen) = (lg,seen); - fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = dest_disj_aux t (dest_disj_aux t' disjs) | dest_disj_aux t disjs = t::disjs; @@ -314,11 +309,10 @@ "Datatype.unit.inducts", "Datatype.unit.split", "Datatype.unit.splits", - "Product_Type.unit_abs_eta_conv", - "Product_Type.unit_induct", + "Datatype.prod.size", - "Datatype.prod.size", "Divides.dvd_0_left_iff", + "Finite_Set.card_0_eq", "Finite_Set.card_infinite", "Finite_Set.Max_ge", @@ -335,15 +329,22 @@ "Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", "Finite_Set.min.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*) "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*) + + "HOL.split_if", (*splitting theorem*) + "HOL.split_if_asm", (*splitting theorem*) + "IntDef.Integ.Abs_Integ_inject", "IntDef.Integ.Abs_Integ_inverse", + "IntDef.abs_split", "IntDiv.zdvd_0_left", + "List.append_eq_append_conv", "List.hd_Cons_tl", (*Says everything is [] or Cons. Probably prolific.*) "List.in_listsD", "List.in_listsI", "List.lists.Cons", "List.listsE", + "Nat.less_one", (*not directional? obscure*) "Nat.not_gr0", "Nat.one_eq_mult_iff", (*duplicate by symmetry*) @@ -368,6 +369,7 @@ "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*) "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*) "NatSimprocs.zero_less_divide_iff_number_of", + "OrderedGroup.abs_0_eq", (*duplicate by symmetry*) "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*) "OrderedGroup.join_0_eq_0", @@ -375,6 +377,9 @@ "OrderedGroup.pprt_eq_0", (*obscure*) "OrderedGroup.pprt_eq_id", (*obscure*) "OrderedGroup.pprt_mono", (*obscure*) + "Orderings.split_min", (*splitting theorem*) + "Orderings.split_max", (*splitting theorem*) + "Parity.even_nat_power", (*obscure, somewhat prolilfic*) "Parity.power_eq_0_iff_number_of", "Parity.power_le_zero_eq_number_of", (*obscure and prolific*) @@ -382,6 +387,14 @@ "Parity.zero_le_power_eq_number_of", (*obscure and prolific*) "Parity.zero_less_power_eq_number_of", (*obscure and prolific*) "Power.zero_less_power_abs_iff", + "Product_Type.unit_abs_eta_conv", + "Product_Type.unit_induct", + + "Product_Type.split_paired_Ball_Sigma", (*splitting theorem*) + "Product_Type.split_paired_Bex_Sigma", (*splitting theorem*) + "Product_Type.split_split", (*splitting theorem*) + "Product_Type.split_split_asm", (*splitting theorem*) + "Relation.diagI", "Relation.ImageI", "Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*) @@ -446,18 +459,8 @@ (*** retrieve lemmas from clasimpset and atpset, may filter them ***) -(*The "name" of a theorem is its statement, if nothing else is available.*) -val plain_string_of_thm = - setmp show_question_marks false - (setmp print_mode [] - (Pretty.setmp_margin 999 string_of_thm)); - -(*Returns the first substring enclosed in quotation marks, typically omitting - the [.] of meta-level assumptions.*) -val firstquoted = hd o (String.tokens (fn c => c = #"\"")) - fun fake_thm_name th = - Context.theory_name (theory_of_thm th) ^ "." ^ firstquoted (plain_string_of_thm th); + Context.theory_name (theory_of_thm th) ^ "." ^ gensym""; fun put_name_pair ("",th) = (fake_thm_name th, th) | put_name_pair (a,th) = (a,th); @@ -484,11 +487,14 @@ else [s] | [] => [s]; +fun banned_thmlist s = + (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"]; + fun make_banned_test xs = let val ht = Polyhash.mkTable (Polyhash.hash_string, op =) (6000, HASH_STRING) - fun banned s = exists (fn s' => isSome (Polyhash.peek ht s')) - (delete_numeric_suffix s) + fun banned_aux s = isSome (Polyhash.peek ht s) orelse banned_thmlist s + fun banned s = exists banned_aux (delete_numeric_suffix s) in app (fn x => Polyhash.insert ht (x,())) (!blacklist); app (insert_suffixed_names ht) (!blacklist @ xs); banned @@ -519,28 +525,41 @@ | get_literals lit lits = (lit::lits); -fun hash_term term = Word.toIntX (xor_words (map hash_literal (get_literals term []))); - -fun hash_thm thm = hash_term (prop_of thm); +fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t []))); fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2); + (*Create a hash table for clauses, of the given size*) fun mk_clause_table n = - Polyhash.mkTable (hash_thm, equal_thm) + Polyhash.mkTable (hash_term o prop_of, equal_thm) (n, HASH_CLAUSE); -(*Use a hash table to eliminate duplicates from xs*) -fun make_unique ht xs = - (app (ignore o Polyhash.peekInsert ht) xs; Polyhash.listItems ht); +(*Use a hash table to eliminate duplicates from xs. Argument is a list of + (name, theorem) pairs, but the theorems are hashed into the table. *) +fun make_unique xs = + let val ht = mk_clause_table 2200 + in + (app (ignore o Polyhash.peekInsert ht) (map swap xs); + map swap (Polyhash.listItems ht)) + end; +(*FIXME: SLOW!!!*) fun mem_thm th [] = false | mem_thm th ((th',_)::thms_names) = equal_thm (th,th') orelse mem_thm th thms_names; +(*FIXME: SLOW!!! These two functions are called only by get_relevant_clauses. + It would be faster to compare names, rather than theorems, and to use + a symbol table or hash table.*) fun insert_thms [] thms_names = thms_names | insert_thms ((thm,name)::thms_names) thms_names' = if mem_thm thm thms_names' then insert_thms thms_names thms_names' else insert_thms thms_names ((thm,name)::thms_names'); +(* filter axiom clauses, but keep supplied clauses and clauses in whitelist *) +fun get_relevant_clauses thy cls_thms white_cls goals = + insert_thms white_cls (ReduceAxiomsN.relevance_filter thy cls_thms goals); + + fun display_thms [] = () | display_thms ((name,thm)::nthms) = let val nthm = name ^ ": " ^ (string_of_thm thm) @@ -555,8 +574,8 @@ fun get_clasimp_atp_lemmas ctxt user_thms = let val included_thms = if !include_all - then (tap (fn ths => Output.debug ("Including all " ^ Int.toString (length ths) ^ - " theorems")) + then (tap (fn ths => Output.debug + ("Including all " ^ Int.toString (length ths) ^ " theorems")) (all_facts_of ctxt @ PureThy.all_thms_of (ProofContext.theory_of ctxt))) else let val claset_thms = @@ -578,7 +597,7 @@ (map put_name_pair included_thms, user_rules) end; -(* remove lemmas that are banned from the backlist *) +(*Remove lemmas that are banned from the backlist. Also remove duplicates. *) fun blacklist_filter thms = if !run_blacklist_filter then let val banned = make_banned_test (map #1 thms) @@ -586,22 +605,10 @@ in filter ok thms end else thms; -(* filter axiom clauses, but keep supplied clauses and clauses in whitelist *) -fun get_relevant_clauses ctxt cls_thms white_cls goals = - let val cls_thms_list = make_unique (mk_clause_table 2200) (List.concat (white_cls@cls_thms)) - val relevant_cls_thms_list = - if !run_relevance_filter - then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals - else cls_thms_list - in - insert_thms (List.concat white_cls) relevant_cls_thms_list - end; - (***************************************************************) (* ATP invocation methods setup *) (***************************************************************) - (**** prover-specific format: TPTP ****) @@ -634,12 +641,12 @@ val goal_cls = conj_cls@hyp_cls val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms val user_lemmas_names = map #1 user_rules - val rm_black_cls = blacklist_filter included_thms - val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_black_cls + val cla_simp_atp_clauses = included_thms |> blacklist_filter + |> make_unique |> ResAxioms.cnf_rules_pairs val user_cls = ResAxioms.cnf_rules_pairs user_rules - val axclauses = get_relevant_clauses ctxt cla_simp_atp_clauses + val thy = ProofContext.theory_of ctxt + val axclauses = get_relevant_clauses thy cla_simp_atp_clauses user_cls (map prop_of goal_cls) - val thy = ProofContext.theory_of ctxt val prob_logic = case mode of Auto => problem_logic_goals [map prop_of goal_cls] | Fol => FOL @@ -730,6 +737,13 @@ let val path = File.tmp_path (Path.basic fname) in Array.app (File.append path o (fn s => s ^ "\n")) end; +(*Converting a subgoal into negated conjecture clauses*) +fun neg_clauses th n = + let val tacs = [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac] + val st = Seq.hd (EVERY' tacs n th) + val negs = Option.valOf (metahyps_thms n st) + in make_clauses negs |> ResAxioms.assume_abstract_list |> Meson.finish_cnf end; + (*We write out problem files for each subgoal. Argument probfile generates filenames, and allows the suppression of the suffix "_1" in problem-generation mode. FIXME: does not cope with &&, and it isn't easy because one could have multiple @@ -738,38 +752,39 @@ let val goals = Thm.prems_of th val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals)) val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt [] - val rm_blacklist_cls = blacklist_filter included_thms - val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_blacklist_cls - val axclauses = get_relevant_clauses ctxt cla_simp_atp_clauses (ResAxioms.cnf_rules_pairs white_thms) goals - val _ = Output.debug ("total clauses from thms = " ^ Int.toString (length axclauses)) + val cla_simp_atp_clauses = included_thms |> blacklist_filter + |> make_unique |> ResAxioms.cnf_rules_pairs + val white_cls = ResAxioms.cnf_rules_pairs white_thms + val _ = Output.debug ("clauses = " ^ Int.toString(length cla_simp_atp_clauses)) val thy = ProofContext.theory_of ctxt - fun get_neg_subgoals n = - if n=0 then [] - else - let val st = Seq.hd (EVERY' [rtac ccontr, ObjectLogic.atomize_tac, - skolemize_tac] n th) - val negs = Option.valOf (metahyps_thms n st) - val negs_clauses = make_clauses negs |> ResAxioms.assume_abstract_list - |> Meson.finish_cnf + fun get_neg_subgoals [] _ = [] + | get_neg_subgoals (gl::gls) n = + let val axclauses = get_relevant_clauses thy cla_simp_atp_clauses + white_cls [gl] (*relevant to goal*) in - negs_clauses :: get_neg_subgoals (n-1) + (neg_clauses th n, axclauses) :: get_neg_subgoals gls (n+1) end - val neg_subgoals = get_neg_subgoals (length goals) - val goals_logic = case !linkup_logic_mode of - Auto => problem_logic_goals (map (map prop_of) neg_subgoals) - | Fol => FOL - | Hol => HOL - val keep_types = if is_fol_logic goals_logic then !ResClause.keep_types else is_typed_hol () - val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else [] - val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses)) - val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else [] + val goal_pairs = get_neg_subgoals goals 1 + val logic = case !linkup_logic_mode of + Auto => problem_logic_goals (map ((map prop_of) o #1) goal_pairs) + | Fol => FOL + | Hol => HOL + val keep_types = if is_fol_logic logic then !ResClause.keep_types + else is_typed_hol () + val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy + else [] + val _ = Output.debug ("classrel clauses = " ^ + Int.toString (length classrel_clauses)) + val arity_clauses = if keep_types then ResClause.arity_clause_thy thy + else [] val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses)) val writer = if !prover = "spass" then dfg_writer else tptp_writer fun write_all [] _ = [] - | write_all (sub::subgoals) k = - (writer goals_logic sub (probfile k) (axclauses,classrel_clauses,arity_clauses) [], - probfile k) :: write_all subgoals (k-1) - val (clnames::_, filenames) = ListPair.unzip (write_all neg_subgoals (length goals)) + | write_all ((ccls,axcls)::subgoals) k = + (writer logic ccls (probfile k) (axcls,classrel_clauses,arity_clauses) [], + probfile k) + :: write_all subgoals (k+1) + val (clnames::_, filenames) = ListPair.unzip (write_all goal_pairs 1) val thm_names = Array.fromList clnames val _ = if !Output.show_debug_msgs then trace_array "thm_names" thm_names else () diff -r 42be3a46dcd8 -r 85414caac94a src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Fri Sep 01 08:36:55 2006 +0200 +++ b/src/HOL/Tools/res_axioms.ML Fri Sep 01 08:51:53 2006 +0200 @@ -229,15 +229,13 @@ fun crhs_of th = case Drule.strip_comb (cprop_of th) of (f, [_, rhs]) => - (case term_of f of - Const ("==", _) => rhs + (case term_of f of Const ("==", _) => rhs | _ => raise THM ("crhs_of", 0, [th])) | _ => raise THM ("crhs_of", 1, [th]); fun rhs_of th = - case #prop (rep_thm th) of - (Const("==",_) $ _ $ rhs) => rhs - | _ => raise THM ("rhs_of", 1, [th]); + case prop_of th of (Const("==",_) $ _ $ rhs) => rhs + | _ => raise THM ("rhs_of", 1, [th]); (*Apply a function definition to an argument, beta-reducing the result.*) fun beta_comb cf x = @@ -265,9 +263,7 @@ fun lambda_free (Abs _) = false | lambda_free (t $ u) = lambda_free t andalso lambda_free u | lambda_free _ = true; - -fun lambda_free_thm th = lambda_free (#prop (rep_thm th)); - + (*Traverse a theorem, declaring abstraction function definitions. String s is the suggested prefix for the constants. Resulting theory is returned in the first theorem. *) fun declare_absfuns th = @@ -424,10 +420,12 @@ fun skolem_of_nnf th = map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th); +fun assert_lambda_free ths = assert (forall (lambda_free o prop_of) ths); + fun assume_abstract th = - if lambda_free_thm th then [th] + if lambda_free (prop_of th) then [th] else th |> eta_conversion_rule |> assume_absfuns - |> tap (fn ths => assert ((forall lambda_free_thm) ths) "assume_abstract: lambdas") + |> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas") (*Replace lambdas by assumed function definitions in the theorems*) fun assume_abstract_list ths = @@ -438,11 +436,11 @@ fun declare_abstract' (thy, []) = (thy, []) | declare_abstract' (thy, th::ths) = let val (thy', th_defs) = - if lambda_free_thm th then (thy, [th]) + if lambda_free (prop_of th) then (thy, [th]) else th |> zero_var_indexes |> Drule.freeze_thaw |> #1 |> eta_conversion_rule |> transfer thy |> declare_absfuns - val _ = assert ((forall lambda_free_thm) th_defs) "declare_abstract: lambdas" + val _ = assert_lambda_free th_defs "declare_abstract: lambdas" val (thy'', ths') = declare_abstract' (thy', ths) in (thy'', th_defs @ ths') end; @@ -494,9 +492,6 @@ Output.debug (string_of_thm th'); ([th],thy)); -fun skolem_cache ((name,th), thy) = #2 (skolem_cache_thm ((name,th), thy)); - - (*Exported function to convert Isabelle theorems into axiom clauses*) fun cnf_axiom (name,th) = case name of @@ -565,7 +560,7 @@ fun cnf_rules_pairs_aux pairs [] = pairs | cnf_rules_pairs_aux pairs ((name,th)::ths) = - let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) :: pairs + let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) @ pairs handle THM _ => pairs | ResClause.CLAUSE _ => pairs | ResHolClause.LAM2COMB _ => pairs in cnf_rules_pairs_aux pairs' ths end; @@ -576,6 +571,15 @@ (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****) (*Setup function: takes a theory and installs ALL known theorems into the clause cache*) + +fun skolem_cache ((name,th), thy) = + let val prop = prop_of th + in + if lambda_free prop orelse null (term_tvars prop) + then thy (*monomorphic theorems can be Skolemized on demand*) + else #2 (skolem_cache_thm ((name,th), thy)) + end; + fun clause_cache_setup thy = List.foldl skolem_cache thy (PureThy.all_thms_of thy); @@ -598,8 +602,8 @@ fun conj2_rule (th1,th2) = conjI OF [th1,th2]; -(*Conjoin a list of theorems to recreate a single theorem*) -fun conj_rule [] = raise THM ("conj_rule", 0, []) +(*Conjoin a list of theorems to form a single theorem*) +fun conj_rule [] = TrueI | conj_rule ths = foldr1 conj2_rule ths; fun skolem_attr (Context.Theory thy, th) =