1.1 --- a/src/HOL/Tools/res_atp.ML Sun Apr 16 08:22:29 2006 +0200
1.2 +++ b/src/HOL/Tools/res_atp.ML Tue Apr 18 05:36:38 2006 +0200
1.3 @@ -313,18 +313,6 @@
1.4 end
1.5 | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
1.6
1.7 -fun logic_of_nclauses [] (lg,seen) = (lg,seen)
1.8 - | logic_of_nclauses (cls::clss) (FOL,seen) =
1.9 - logic_of_nclauses clss (logic_of_clauses (snd cls) (FOL,seen))
1.10 - | logic_of_nclauses clss (lg,seen) = (lg,seen);
1.11 -
1.12 -fun problem_logic (goal_cls,rules_cls) =
1.13 - let val (lg1,seen1) = logic_of_clauses goal_cls (FOL,[])
1.14 - val (lg2,seen2) = logic_of_nclauses rules_cls (lg1,seen1)
1.15 - in
1.16 - lg2
1.17 - end;
1.18 -
1.19 fun problem_logic_goals_aux [] (lg,seen) = lg
1.20 | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) =
1.21 problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
1.22 @@ -360,13 +348,13 @@
1.23
1.24
1.25 fun write_subgoal_file mode ctxt conjectures user_thms n =
1.26 - let val conj_cls = map prop_of (make_clauses conjectures)
1.27 - val hyp_cls = map prop_of (cnf_hyps_thms ctxt)
1.28 + let val conj_cls = make_clauses conjectures
1.29 + val hyp_cls = cnf_hyps_thms ctxt
1.30 val goal_cls = conj_cls@hyp_cls
1.31 val user_rules = map ResAxioms.pairname user_thms
1.32 - val (names_arr,axclauses_as_thms) = ResClasimp.get_clasimp_atp_lemmas ctxt (goal_cls) user_rules (!include_claset,!include_simpset,!include_atpset) (!run_relevance_filter)
1.33 + val (names_arr,axclauses_as_thms) = ResClasimp.get_clasimp_atp_lemmas ctxt (map prop_of goal_cls) user_rules (!include_claset,!include_simpset,!include_atpset) (!run_relevance_filter)
1.34 val thy = ProofContext.theory_of ctxt
1.35 - val prob_logic = case mode of Auto => problem_logic_goals [goal_cls]
1.36 + val prob_logic = case mode of Auto => problem_logic_goals [map prop_of goal_cls]
1.37 | Fol => FOL
1.38 | Hol => HOL
1.39 val keep_types = if is_fol_logic prob_logic then !fol_keep_types else is_typed_hol ()
1.40 @@ -465,7 +453,7 @@
1.41 fun write_problem_files pf (ctxt,th) =
1.42 let val goals = Thm.prems_of th
1.43 val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
1.44 - val (names_arr, axclauses_as_terms) = ResClasimp.get_clasimp_atp_lemmas ctxt goals [] (true,true,true) (!run_relevance_filter) (* no user supplied rules here, because no user invocation *)
1.45 + val (names_arr, axclauses) = ResClasimp.get_clasimp_atp_lemmas ctxt goals [] (true,true,true) (!run_relevance_filter) (* no user supplied rules here, because no user invocation *)
1.46 val _ = Output.debug ("claset, simprules and atprules total clauses = " ^
1.47 Int.toString (Array.length names_arr))
1.48 val thy = ProofContext.theory_of ctxt
1.49 @@ -475,12 +463,12 @@
1.50 let val st = Seq.hd (EVERY'
1.51 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac] n th)
1.52 val negs = Option.valOf (metahyps_thms n st)
1.53 - val negs_clauses = map prop_of (make_clauses negs)
1.54 + val negs_clauses = make_clauses negs
1.55 in
1.56 negs_clauses::(get_neg_subgoals (n - 1))
1.57 end
1.58 val neg_subgoals = get_neg_subgoals (length goals)
1.59 - val goals_logic = case !linkup_logic_mode of Auto => problem_logic_goals neg_subgoals
1.60 + val goals_logic = case !linkup_logic_mode of Auto => problem_logic_goals (map (map prop_of) neg_subgoals)
1.61 | Fol => FOL
1.62 | Hol => HOL
1.63 val keep_types = if is_fol_logic goals_logic then !ResClause.keep_types else is_typed_hol ()
1.64 @@ -491,7 +479,7 @@
1.65 val writer = (*if !prover ~= "spass" then *)tptp_writer
1.66 fun write_all [] _ = []
1.67 | write_all (subgoal::subgoals) k =
1.68 - (writer goals_logic subgoal (pf k) (axclauses_as_terms,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1))
1.69 + (writer goals_logic subgoal (pf k) (axclauses,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1))
1.70 in
1.71 (write_all neg_subgoals (length goals), names_arr)
1.72 end;
2.1 --- a/src/HOL/Tools/res_axioms.ML Sun Apr 16 08:22:29 2006 +0200
2.2 +++ b/src/HOL/Tools/res_axioms.ML Tue Apr 18 05:36:38 2006 +0200
2.3 @@ -12,22 +12,15 @@
2.4 val elimRule_tac : thm -> Tactical.tactic
2.5 val elimR2Fol : thm -> term
2.6 val transform_elim : thm -> thm
2.7 - val clausify_axiom_pairs : (string*thm) -> (ResClause.clause*thm) list
2.8 - val clausify_axiom_pairsH : (string*thm) -> (ResHolClause.clause*thm) list
2.9 val cnf_axiom : (string * thm) -> thm list
2.10 val meta_cnf_axiom : thm -> thm list
2.11 val claset_rules_of_thy : theory -> (string * thm) list
2.12 val simpset_rules_of_thy : theory -> (string * thm) list
2.13 val claset_rules_of_ctxt: Proof.context -> (string * thm) list
2.14 val simpset_rules_of_ctxt : Proof.context -> (string * thm) list
2.15 - val clausify_rules_pairs : (string*thm) list -> (ResClause.clause*thm) list list
2.16 - val clausify_rules_pairsH : (string*thm) list -> (ResHolClause.clause*thm) list list
2.17 val pairname : thm -> (string * thm)
2.18 val skolem_thm : thm -> thm list
2.19 - val cnf_rules1 : (string * thm) list -> string list -> (string * thm list) list * string list
2.20 - val cnf_rules2 : (string * thm) list -> string list -> (string * term list) list * string list
2.21 val cnf_rules_pairs : (string * Thm.thm) list -> (Thm.thm * (string * int)) list list;
2.22 - val clausify_rules_pairs_abs : (string * thm) list -> (Term.term * (string * int)) list list
2.23 val meson_method_setup : theory -> theory
2.24 val setup : theory -> theory
2.25
2.26 @@ -391,19 +384,6 @@
2.27 (*works for both FOL and HOL*)
2.28 val cnf_rules = cnf_rules_g cnf_axiom;
2.29
2.30 -fun cnf_rules1 [] err_list = ([],err_list)
2.31 - | cnf_rules1 ((name,th) :: ths) err_list =
2.32 - let val (ts,es) = cnf_rules1 ths err_list
2.33 - in ((name,cnf_axiom (name,th)) :: ts,es) handle _ => (ts,(name::es)) end;
2.34 -
2.35 -fun cnf_rules2 [] err_list = ([],err_list)
2.36 - | cnf_rules2 ((name,th) :: ths) err_list =
2.37 - let val (ts,es) = cnf_rules2 ths err_list
2.38 - in
2.39 - ((name,map prop_of (cnf_axiom (name,th))) :: ts,es) handle _ => (ts,(name::es))
2.40 - end;
2.41 -
2.42 -
2.43 fun cnf_rules_pairs_aux [] = []
2.44 | cnf_rules_pairs_aux ((name,th)::ths) =
2.45 let val ts = cnf_rules_pairs_aux ths
2.46 @@ -418,70 +398,9 @@
2.47
2.48 fun cnf_rules_pairs thms = rev (cnf_rules_pairs_aux thms);
2.49
2.50 -fun clausify_rules_pairs_abs_aux [] = []
2.51 - | clausify_rules_pairs_abs_aux ((name,th)::ths) =
2.52 - let val ts = clausify_rules_pairs_abs_aux ths
2.53 - fun pair_name_cls k (n, []) = []
2.54 - | pair_name_cls k (n, cls::clss) =
2.55 - (prop_of cls, (n,k)) :: (pair_name_cls (k+1) (n, clss))
2.56 - in
2.57 - pair_name_cls 0 (name, (cnf_axiom(name,th))) :: ts
2.58 - handle THM _ => ts | ResClause.CLAUSE _ => ts | ResHolClause.LAM2COMB _ => ts
2.59 - end;
2.60 -
2.61 -fun clausify_rules_pairs_abs thms = rev (clausify_rules_pairs_abs_aux thms);
2.62 -
2.63
2.64 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
2.65
2.66 -fun make_axiom_clauses _ _ [] = []
2.67 - | make_axiom_clauses name i (th::ths) =
2.68 - case ResClause.make_axiom_clause (prop_of th) (name,i) of
2.69 - SOME cls => (cls, th) :: make_axiom_clauses name (i+1) ths
2.70 - | NONE => make_axiom_clauses name i ths;
2.71 -
2.72 -(* outputs a list of (clause,theorem) pairs *)
2.73 -fun clausify_axiom_pairs (name,th) =
2.74 - filter (fn (c,th) => not (ResClause.isTaut c))
2.75 - (make_axiom_clauses name 0 (cnf_axiom (name,th)));
2.76 -
2.77 -fun make_axiom_clausesH _ _ [] = []
2.78 - | make_axiom_clausesH name i (th::ths) =
2.79 - (ResHolClause.make_axiom_clause (prop_of th) (name,i), th) ::
2.80 - (make_axiom_clausesH name (i+1) ths)
2.81 -
2.82 -fun clausify_axiom_pairsH (name,th) =
2.83 - filter (fn (c,th) => not (ResHolClause.isTaut c))
2.84 - (make_axiom_clausesH name 0 (cnf_axiom (name,th)));
2.85 -
2.86 -
2.87 -fun clausify_rules_pairs_aux result [] = result
2.88 - | clausify_rules_pairs_aux result ((name,th)::ths) =
2.89 - clausify_rules_pairs_aux (clausify_axiom_pairs (name,th) :: result) ths
2.90 - handle THM (msg,_,_) =>
2.91 - (Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg);
2.92 - clausify_rules_pairs_aux result ths)
2.93 - | ResClause.CLAUSE (msg,t) =>
2.94 - (Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg ^
2.95 - ": " ^ TermLib.string_of_term t);
2.96 - clausify_rules_pairs_aux result ths)
2.97 -
2.98 -
2.99 -fun clausify_rules_pairs_auxH result [] = result
2.100 - | clausify_rules_pairs_auxH result ((name,th)::ths) =
2.101 - clausify_rules_pairs_auxH (clausify_axiom_pairsH (name,th) :: result) ths
2.102 - handle THM (msg,_,_) =>
2.103 - (Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg);
2.104 - clausify_rules_pairs_auxH result ths)
2.105 - | ResHolClause.LAM2COMB (t) =>
2.106 - (Output.debug ("Cannot clausify " ^ TermLib.string_of_term t);
2.107 - clausify_rules_pairs_auxH result ths)
2.108 -
2.109 -
2.110 -
2.111 -val clausify_rules_pairs = clausify_rules_pairs_aux [];
2.112 -
2.113 -val clausify_rules_pairsH = clausify_rules_pairs_auxH [];
2.114
2.115 (*These should include any plausibly-useful theorems, especially if they need
2.116 Skolem functions. FIXME: this list is VERY INCOMPLETE*)