1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML Wed Jun 01 14:16:45 2005 +0200
1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Wed Jun 01 14:50:48 2005 +0200
1.3 @@ -7,7 +7,7 @@
1.4
1.5 signature RES_CLASIMP =
1.6 sig
1.7 - val write_out_clasimp :string -> (ResClause.clause * Thm.thm) Array.array * int
1.8 + val write_out_clasimp :string -> theory -> (ResClause.clause * thm) Array.array * int
1.9 end;
1.10
1.11 structure ResClasimp : RES_CLASIMP =
1.12 @@ -63,25 +63,22 @@
1.13 fun multi x 0 xlist = xlist
1.14 |multi x n xlist = multi x (n -1 ) (x::xlist);
1.15
1.16 +fun clause_numbering ((clause, theorem), cls) =
1.17 + let val num_of_cls = length cls
1.18 + val numbers = 0 upto (num_of_cls -1)
1.19 + val multi_name = multi (clause, theorem) num_of_cls []
1.20 + in
1.21 + (multi_name)
1.22 + end;
1.23
1.24 -fun clause_numbering ((clause, theorem), cls) = let val num_of_cls = length cls
1.25 - val numbers = 0 upto (num_of_cls -1)
1.26 - val multi_name = multi (clause, theorem) num_of_cls []
1.27 - in
1.28 - (multi_name)
1.29 - end;
1.30 -
1.31 -
1.32 -
1.33 -
1.34 -
1.35 -fun write_out_clasimp filename =
1.36 - let val claset_rules = ResAxioms.claset_rules_of_thy (the_context());
1.37 +(*Write out the claset and simpset rules of the supplied theory.*)
1.38 +fun write_out_clasimp filename thy =
1.39 + let val claset_rules = ResAxioms.claset_rules_of_thy thy;
1.40 val named_claset = List.filter has_name_pair claset_rules;
1.41 val claset_names = map remove_spaces_pair (named_claset)
1.42 val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
1.43
1.44 - val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context());
1.45 + val simpset_rules = ResAxioms.simpset_rules_of_thy thy;
1.46 val named_simpset =
1.47 map remove_spaces_pair (List.filter has_name_pair simpset_rules)
1.48 val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
2.1 --- a/src/HOL/Tools/res_atp.ML Wed Jun 01 14:16:45 2005 +0200
2.2 +++ b/src/HOL/Tools/res_atp.ML Wed Jun 01 14:50:48 2005 +0200
2.3 @@ -31,11 +31,9 @@
2.4 val subgoals = [];
2.5
2.6 val traceflag = ref true;
2.7 -(* used for debug *)
2.8 +
2.9 val debug = ref false;
2.10 -
2.11 fun debug_tac tac = (warning "testing";tac);
2.12 -(* default value is false *)
2.13
2.14 val trace_res = ref false;
2.15 val full_spass = ref false;
2.16 @@ -71,13 +69,10 @@
2.17
2.18 (**** for Isabelle/ML interface ****)
2.19
2.20 -fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ")
2.21 +fun is_proof_char ch = (ch = " ") orelse
2.22 + ((ord"!" <= ord ch) andalso (ord ch <= ord"~") andalso (ch <> "?"))
2.23
2.24 -fun proofstring x = let val exp = explode x
2.25 - in
2.26 - List.filter (is_proof_char ) exp
2.27 - end
2.28 -
2.29 +fun proofstring x = List.filter (is_proof_char) (explode x);
2.30
2.31
2.32 (*
2.33 @@ -135,11 +130,11 @@
2.34 val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
2.35 val out = TextIO.openOut(probfile)
2.36 in
2.37 - (ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
2.38 + (ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out;
2.39 + if !trace_res then (warning probfile) else ())
2.40 end;
2.41
2.42
2.43 -
2.44 (*********************************************************************)
2.45 (* call SPASS with settings and problem file for the current subgoal *)
2.46 (* should be modified to allow other provers to be called *)
2.47 @@ -221,28 +216,27 @@
2.48
2.49
2.50 fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) =
2.51 - (
2.52 - warning("in call_atp_tac_tfrees");
2.53 -
2.54 - tptp_inputs_tfrees (make_clauses thms) n tfrees;
2.55 - call_resolve_tac sign thms sg_term (childin, childout, pid) n;
2.56 - dummy_tac);
2.57 + (
2.58 + warning("in call_atp_tac_tfrees");
2.59 + tptp_inputs_tfrees (make_clauses thms) n tfrees;
2.60 + call_resolve_tac sign thms sg_term (childin, childout, pid) n;
2.61 + dummy_tac);
2.62
2.63 fun atp_tac_tfrees tfrees sg_term (childin, childout,pid) n st =
2.64 -let val sign = sign_of_thm st
2.65 - val _ = warning ("in atp_tac_tfrees ")
2.66 - val _ = warning ("sg_term :" ^ (Sign.string_of_term sign sg_term))
2.67 -
2.68 - in
2.69 -
2.70 -SELECT_GOAL
2.71 - (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac,
2.72 - METAHYPS(fn negs => ( call_atp_tac_tfrees sign negs n tfrees sg_term (childin, childout,pid) ))]) n st
2.73 -end;
2.74 + let val sign = sign_of_thm st
2.75 + val _ = warning ("in atp_tac_tfrees ")
2.76 + val _ = warning ("sg_term :" ^ (Sign.string_of_term sign sg_term))
2.77 + in
2.78 + SELECT_GOAL
2.79 + (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac,
2.80 + METAHYPS(fn negs => (call_atp_tac_tfrees sign negs n tfrees sg_term
2.81 + (childin, childout,pid) ))]) n st
2.82 + end;
2.83
2.84
2.85 fun isar_atp_g tfrees sg_term (childin, childout, pid) n =
2.86 -((warning("in isar_atp_g"));atp_tac_tfrees tfrees sg_term (childin, childout, pid) n);
2.87 + ((warning("in isar_atp_g"));
2.88 + atp_tac_tfrees tfrees sg_term (childin, childout, pid) n);
2.89
2.90
2.91
2.92 @@ -256,7 +250,7 @@
2.93 if (k > n)
2.94 then ()
2.95 else
2.96 - let val prems = prems_of thm
2.97 + let val prems = prems_of thm
2.98 val sg_term = ReconOrderClauses.get_nth n prems
2.99 val thmstring = string_of_thm thm
2.100 in
2.101 @@ -282,9 +276,8 @@
2.102
2.103 fun isar_atp_aux thms thm n_subgoals (childin, childout, pid) =
2.104 let val tfree_lits = isar_atp_h thms
2.105 - in
2.106 - (warning("in isar_atp_aux"));
2.107 - isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid)
2.108 + in warning("in isar_atp_aux");
2.109 + isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid)
2.110 end;
2.111
2.112 (******************************************************************)
2.113 @@ -294,9 +287,8 @@
2.114 (* turns off xsymbol at start of function, restoring it at end *)
2.115 (******************************************************************)
2.116 (*FIX changed to clasimp_file *)
2.117 -fun isar_atp' (thms, thm) =
2.118 - let
2.119 - val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
2.120 +fun isar_atp' (ctxt, thms, thm) =
2.121 + let val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
2.122 val _= (warning ("in isar_atp'"))
2.123 val prems = prems_of thm
2.124 val sign = sign_of_thm thm
2.125 @@ -305,8 +297,10 @@
2.126 val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
2.127
2.128 (* set up variables for writing out the clasimps to a tptp file *)
2.129 - val (clause_arr, num_of_clauses) = ResClasimp.write_out_clasimp (File.sysify_path clasimp_file)
2.130 - val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )
2.131 + val (clause_arr, num_of_clauses) =
2.132 + ResClasimp.write_out_clasimp (File.sysify_path clasimp_file)
2.133 + (ProofContext.theory_of ctxt)
2.134 + val _ = warning ("clasimp_file is " ^ File.sysify_path clasimp_file)
2.135
2.136 (* cq: add write out clasimps to file *)
2.137
2.138 @@ -349,8 +343,6 @@
2.139 safeEs @ safeIs @ hazEs @ hazIs
2.140 end;
2.141
2.142 -
2.143 -
2.144 fun append_name name [] _ = []
2.145 | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1));
2.146
2.147 @@ -360,7 +352,6 @@
2.148 thms'::(append_names names thmss)
2.149 end;
2.150
2.151 -
2.152 fun get_thms_ss [] = []
2.153 | get_thms_ss thms =
2.154 let val names = map Thm.name_of_thm thms
2.155 @@ -370,9 +361,6 @@
2.156 ResLib.flat_noDup thms''
2.157 end;
2.158
2.159 -
2.160 -
2.161 -
2.162 in
2.163
2.164
2.165 @@ -395,8 +383,6 @@
2.166 *)
2.167
2.168
2.169 -
2.170 -
2.171 (* called in Isar automatically *)
2.172
2.173 fun isar_atp (ctxt,thm) =
2.174 @@ -413,14 +399,12 @@
2.175 (warning ("subgoals in isar_atp: "^prems_string));
2.176 (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
2.177 ((*isar_local_thms (d_cs,d_ss_thms); *)(warning("about to call isar_atp'"));
2.178 - isar_atp' (prems, thm))
2.179 + isar_atp' (ctxt, prems, thm))
2.180 end;
2.181
2.182 end
2.183
2.184
2.185 -
2.186 -
2.187 end;
2.188
2.189 Proof.atp_hook := ResAtp.isar_atp;