--- a/src/CCL/Wfd.thy Thu Oct 29 14:06:49 2009 +0100
+++ b/src/CCL/Wfd.thy Thu Oct 29 18:17:26 2009 +0100
@@ -440,7 +440,7 @@
fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>
let val bvs = bvars Bi []
- val ihs = List.filter could_IH (Logic.strip_assums_hyp Bi)
+ val ihs = filter could_IH (Logic.strip_assums_hyp Bi)
val rnames = map (fn x=>
let val (a,b) = get_bno [] 0 x
in (List.nth(bvs,a),b) end) ihs
--- a/src/FOLP/simp.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/FOLP/simp.ML Thu Oct 29 18:17:26 2009 +0100
@@ -215,7 +215,7 @@
fun add_norm_tags congs =
let val ccs = map cong_const congs
- val new_asms = List.filter (exists not o #2)
+ val new_asms = filter (exists not o #2)
(ccs ~~ (map (map atomic o prems_of) congs));
in add_norms(congs,ccs,new_asms) end;
--- a/src/HOL/ATP_Linkup.thy Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/ATP_Linkup.thy Thu Oct 29 18:17:26 2009 +0100
@@ -91,9 +91,9 @@
subsection {* Setup of external ATPs *}
-use "Tools/res_axioms.ML" setup ResAxioms.setup
+use "Tools/res_axioms.ML" setup Res_Axioms.setup
use "Tools/res_hol_clause.ML"
-use "Tools/res_reconstruct.ML" setup ResReconstruct.setup
+use "Tools/res_reconstruct.ML" setup Res_Reconstruct.setup
use "Tools/res_atp.ML"
use "Tools/ATP_Manager/atp_wrapper.ML" setup ATP_Wrapper.setup
--- a/src/HOL/Auth/KerberosIV.thy Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Auth/KerberosIV.thy Thu Oct 29 18:17:26 2009 +0100
@@ -780,7 +780,7 @@
lemma u_NotexpiredSK_NotexpiredAK:
"\<lbrakk> \<not> expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \<rbrakk>
\<Longrightarrow> \<not> expiredAK Ta evs"
- by (metis nat_add_commute le_less_trans)
+ by (metis le_less_trans)
subsection{* Reliability: friendly agents send something if something else happened*}
--- a/src/HOL/HOL.thy Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/HOL.thy Thu Oct 29 18:17:26 2009 +0100
@@ -24,6 +24,7 @@
"~~/src/Tools/coherent.ML"
"~~/src/Tools/eqsubst.ML"
"~~/src/Provers/quantifier1.ML"
+ "Tools/res_blacklist.ML"
("Tools/simpdata.ML")
"~~/src/Tools/random_word.ML"
"~~/src/Tools/atomize_elim.ML"
@@ -35,6 +36,8 @@
setup {* Intuitionistic.method_setup @{binding iprover} *}
+setup Res_Blacklist.setup
+
subsection {* Primitive logic *}
@@ -833,19 +836,14 @@
val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
end);
-structure BasicClassical: BASIC_CLASSICAL = Classical;
-open BasicClassical;
+structure Basic_Classical: BASIC_CLASSICAL = Classical;
+open Basic_Classical;
ML_Antiquote.value "claset"
(Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())");
-
-structure ResBlacklist = Named_Thms
- (val name = "noatp" val description = "theorems blacklisted for ATP");
*}
-text {*ResBlacklist holds theorems blacklisted to sledgehammer.
- These theorems typically produce clauses that are prolific (match too many equality or
- membership literals) and relate to seldom-used facts. Some duplicate other rules.*}
+setup Classical.setup
setup {*
let
@@ -856,8 +854,6 @@
in
Hypsubst.hypsubst_setup
#> ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
- #> Classical.setup
- #> ResBlacklist.setup
end
*}
--- a/src/HOL/Import/import_syntax.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Import/import_syntax.ML Thu Oct 29 18:17:26 2009 +0100
@@ -61,7 +61,7 @@
val thyname = get_generating_thy thy
val segname = get_import_segment thy
val (int_thms,facts) = Replay.setup_int_thms thyname thy
- val thmnames = List.filter (not o should_ignore thyname thy) facts
+ val thmnames = filter_out (should_ignore thyname thy) facts
fun replay thy =
let
val _ = ImportRecorder.load_history thyname
--- a/src/HOL/Import/shuffler.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Import/shuffler.ML Thu Oct 29 18:17:26 2009 +0100
@@ -628,7 +628,7 @@
val all_thms =
map (`Thm.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy)))
in
- List.filter (match_consts ignored t) all_thms
+ filter (match_consts ignored t) all_thms
end
fun gen_shuffle_tac ctxt search thms i st =
--- a/src/HOL/IsaMakefile Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/IsaMakefile Thu Oct 29 18:17:26 2009 +0100
@@ -302,6 +302,7 @@
Tools/recdef.ML \
Tools/res_atp.ML \
Tools/res_axioms.ML \
+ Tools/res_blacklist.ML \
Tools/res_clause.ML \
Tools/res_hol_clause.ML \
Tools/res_reconstruct.ML \
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 29 18:17:26 2009 +0100
@@ -319,7 +319,7 @@
if success then (message, SH_OK (time_isa, time_atp, theorem_names))
else (message, SH_FAIL(time_isa, time_atp))
end
- handle ResHolClause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, []))
+ handle Res_HOL_Clause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, []))
| ERROR msg => ("error: " ^ msg, SH_ERROR)
| TimeLimit.TimeOut => ("timeout", SH_ERROR)
--- a/src/HOL/Nominal/nominal_datatype.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Oct 29 18:17:26 2009 +0100
@@ -66,7 +66,7 @@
fun mk_case_names_exhausts descr new =
map (RuleCases.case_names o exhaust_cases descr o #1)
- (List.filter (fn ((_, (name, _, _))) => name mem_string new) descr);
+ (filter (fn ((_, (name, _, _))) => name mem_string new) descr);
end;
@@ -1166,11 +1166,11 @@
fun make_ind_prem fsT f k T ((cname, cargs), idxs) =
let
- val recs = List.filter is_rec_type cargs;
+ val recs = filter is_rec_type cargs;
val Ts = map (typ_of_dtyp descr'' sorts) cargs;
val recTs' = map (typ_of_dtyp descr'' sorts) recs;
val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
- val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
+ val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
val frees = tnames ~~ Ts;
val frees' = partition_cargs idxs frees;
val z = (Name.variant tnames "z", fsT);
--- a/src/HOL/Nominal/nominal_primrec.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Thu Oct 29 18:17:26 2009 +0100
@@ -193,7 +193,7 @@
NONE =>
let
val dummy_fns = map (fn (_, cargs) => Const (@{const_name undefined},
- replicate ((length cargs) + (length (List.filter is_rec_type cargs)))
+ replicate (length cargs + length (filter is_rec_type cargs))
dummyT ---> HOLogic.unitT)) constrs;
val _ = warning ("No function definition for datatype " ^ quote tname)
in
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Oct 29 18:17:26 2009 +0100
@@ -86,7 +86,7 @@
(* unregister ATP thread *)
-fun unregister (success, message) thread = Synchronized.change global_state
+fun unregister message thread = Synchronized.change global_state
(fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
(case lookup_thread active thread of
SOME (birth_time, _, description) =>
@@ -149,7 +149,7 @@
do
(Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
|> these
- |> List.app (unregister (false, "Interrupted (reached timeout)"));
+ |> List.app (unregister "Interrupted (reached timeout)");
print_new_messages ();
(*give threads some time to respond to interrupt*)
OS.Process.sleep min_wait_time)
@@ -263,14 +263,11 @@
let
val _ = register birth_time death_time (Thread.self (), desc);
val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
- val result =
- let val {success, message, ...} = prover (! timeout) problem;
- in (success, message) end
- handle ResHolClause.TOO_TRIVIAL => (* FIXME !? *)
- (true, "Empty clause: Try this command: " ^
- Markup.markup Markup.sendback "apply metis")
- | ERROR msg => (false, "Error: " ^ msg);
- val _ = unregister result (Thread.self ());
+ val message = #message (prover (! timeout) problem)
+ handle Res_HOL_Clause.TOO_TRIVIAL => (* FIXME !? *)
+ "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
+ | ERROR msg => ("Error: " ^ msg);
+ val _ = unregister message (Thread.self ());
in () end)
in () end);
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Oct 29 18:17:26 2009 +0100
@@ -103,7 +103,7 @@
let
val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
- val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
+ val axclauses = Res_Axioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
val {context = ctxt, facts, goal} = Proof.raw_goal state (* FIXME ?? *)
val problem =
{with_full_types = ! ATP_Manager.full_types,
@@ -138,9 +138,9 @@
val to_use =
if length ordered_used < length name_thms_pairs then
filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
- else
- name_thms_pairs
- val (min_thms, n) = if null to_use then ([], 0)
+ else name_thms_pairs
+ val (min_thms, n) =
+ if null to_use then ([], 0)
else minimal (test_thms (SOME filtered)) to_use
val min_names = sort_distinct string_ord (map fst min_thms)
val _ = priority (cat_lines
@@ -157,7 +157,7 @@
(NONE, "Error in prover: " ^ msg)
| (Failure, _) =>
(NONE, "Failure: No proof with the theorems supplied"))
- handle ResHolClause.TOO_TRIVIAL =>
+ handle Res_HOL_Clause.TOO_TRIVIAL =>
(SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
| ERROR msg => (NONE, "Error: " ^ msg)
end
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Oct 29 18:17:26 2009 +0100
@@ -117,8 +117,8 @@
(* get clauses and prepare them for writing *)
val (ctxt, (chain_ths, th)) = goal;
val thy = ProofContext.theory_of ctxt;
- val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths;
- val goal_cls = #1 (ResAxioms.neg_conjecture_clauses ctxt th subgoalno);
+ val chain_ths = map (Thm.put_name_hint Res_Reconstruct.chained_hint) chain_ths;
+ val goal_cls = #1 (Res_Axioms.neg_conjecture_clauses ctxt th subgoalno);
val the_filtered_clauses =
(case filtered_clauses of
NONE => relevance_filter goal goal_cls
@@ -204,14 +204,14 @@
val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem;
in
external_prover
- (ResAtp.get_relevant max_new_clauses insert_theory_const)
- (ResAtp.prepare_clauses false)
- (ResHolClause.tptp_write_file with_full_types)
+ (Res_ATP.get_relevant max_new_clauses insert_theory_const)
+ (Res_ATP.prepare_clauses false)
+ (Res_HOL_Clause.tptp_write_file with_full_types)
command
(arguments timeout)
- ResReconstruct.find_failure
- (if emit_structured_proof then ResReconstruct.structured_proof
- else ResReconstruct.lemma_list false)
+ Res_Reconstruct.find_failure
+ (if emit_structured_proof then Res_Reconstruct.structured_proof
+ else Res_Reconstruct.lemma_list false)
axiom_clauses
filtered_clauses
name
@@ -280,13 +280,13 @@
val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem
in
external_prover
- (ResAtp.get_relevant max_new_clauses insert_theory_const)
- (ResAtp.prepare_clauses true)
- (ResHolClause.dfg_write_file with_full_types)
+ (Res_ATP.get_relevant max_new_clauses insert_theory_const)
+ (Res_ATP.prepare_clauses true)
+ (Res_HOL_Clause.dfg_write_file with_full_types)
command
(arguments timeout)
- ResReconstruct.find_failure
- (ResReconstruct.lemma_list true)
+ Res_Reconstruct.find_failure
+ (Res_Reconstruct.lemma_list true)
axiom_clauses
filtered_clauses
name
--- a/src/HOL/Tools/Datatype/datatype.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Thu Oct 29 18:17:26 2009 +0100
@@ -63,9 +63,11 @@
val get_all = #types o DatatypesData.get;
val get_info = Symtab.lookup o get_all;
-fun the_info thy name = (case get_info thy name of
- SOME info => info
- | NONE => error ("Unknown datatype " ^ quote name));
+
+fun the_info thy name =
+ (case get_info thy name of
+ SOME info => info
+ | NONE => error ("Unknown datatype " ^ quote name));
fun info_of_constr thy (c, T) =
let
@@ -94,6 +96,7 @@
cases = cases |> fold Symtab.update
(map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)});
+
(* complex queries *)
fun the_spec thy dtco =
@@ -155,6 +158,7 @@
| NONE => NONE;
+
(** various auxiliary **)
(* prepare datatype specifications *)
@@ -207,6 +211,7 @@
end;
+
(* translation rules for case *)
fun make_case ctxt = DatatypeCase.make_case
@@ -228,6 +233,7 @@
[], []);
+
(** document antiquotation **)
val _ = ThyOutput.antiquotation "datatype" Args.tyname
@@ -254,15 +260,17 @@
in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
+
(** abstract theory extensions relative to a datatype characterisation **)
-structure DatatypeInterpretation = InterpretationFun
+structure Datatype_Interpretation = Interpretation
(type T = config * string list val eq: T * T -> bool = eq_snd op =);
-fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
+fun interpretation f = Datatype_Interpretation.interpretation (uncurry f);
fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
(index, (((((((((((_, (tname, _, _))), inject), distinct),
- exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong), (split, split_asm))) =
+ exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong),
+ (split, split_asm))) =
(tname,
{index = index,
alt_names = alt_names,
@@ -309,7 +317,8 @@
config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
- val dt_infos = map_index (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
+ val dt_infos = map_index
+ (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
(hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
val dt_names = map fst dt_infos;
@@ -319,7 +328,7 @@
[((Binding.empty, [nth inducts index]), [Induct.induct_type tname]),
((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
val unnamed_rules = map (fn induct =>
- ((Binding.empty, [induct]), [Thm.kind_internal, Induct.induct_type ""]))
+ ((Binding.empty, [induct]), [RuleCases.inner_rule, Induct.induct_type ""]))
(Library.drop (length dt_names, inducts));
in
thy9
@@ -337,14 +346,16 @@
|> snd
|> add_case_tr' case_names
|> register dt_infos
- |> DatatypeInterpretation.data (config, dt_names)
+ |> Datatype_Interpretation.data (config, dt_names)
|> pair dt_names
end;
+
(** declare existing type as datatype **)
-fun prove_rep_datatype config dt_names alt_names descr sorts raw_inject half_distinct raw_induct thy1 =
+fun prove_rep_datatype config dt_names alt_names descr sorts
+ raw_inject half_distinct raw_induct thy1 =
let
val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
@@ -417,7 +428,8 @@
(*FIXME somehow dubious*)
in
ProofContext.theory_result
- (prove_rep_datatype config dt_names alt_names descr vs raw_inject half_distinct raw_induct)
+ (prove_rep_datatype config dt_names alt_names descr vs
+ raw_inject half_distinct raw_induct)
#-> after_qed
end;
in
@@ -430,6 +442,7 @@
val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);
+
(** definitional introduction of datatypes **)
fun gen_add_datatype prep_typ config new_type_names dts thy =
@@ -445,16 +458,20 @@
val (tyvars, _, _, _)::_ = dts;
val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
- in (case duplicates (op =) tvs of
- [] => if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
- else error ("Mutually recursive datatypes must have same type parameters")
- | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
- " : " ^ commas dups))
+ in
+ (case duplicates (op =) tvs of
+ [] =>
+ if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
+ else error ("Mutually recursive datatypes must have same type parameters")
+ | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
+ " : " ^ commas dups))
end) dts);
val dt_names = map fst new_dts;
- val _ = (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
- [] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
+ val _ =
+ (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
+ [] => ()
+ | dups => error ("Duplicate datatypes: " ^ commas dups));
fun prep_dt_spec ((tvs, tname, mx, constrs), tname') (dts', constr_syntax, sorts, i) =
let
@@ -508,13 +525,15 @@
val datatype_cmd = snd ooo gen_add_datatype read_typ default_config;
+
(** package setup **)
(* setup theory *)
val setup =
trfun_setup #>
- DatatypeInterpretation.init;
+ Datatype_Interpretation.init;
+
(* outer syntax *)
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Oct 29 18:17:26 2009 +0100
@@ -292,7 +292,7 @@
val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
let
val Ts = map (typ_of_dtyp descr' sorts) cargs;
- val Ts' = map mk_dummyT (List.filter is_rec_type cargs)
+ val Ts' = map mk_dummyT (filter is_rec_type cargs)
in Const (@{const_name undefined}, Ts @ Ts' ---> T')
end) constrs) descr';
@@ -305,7 +305,7 @@
val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
let
val Ts = map (typ_of_dtyp descr' sorts) cargs;
- val Ts' = Ts @ map mk_dummyT (List.filter is_rec_type cargs);
+ val Ts' = Ts @ map mk_dummyT (filter is_rec_type cargs);
val frees' = map (uncurry (mk_Free "x")) (Ts' ~~ (1 upto length Ts'));
val frees = Library.take (length cargs, frees');
val free = mk_Free "f" (Ts ---> T') j
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Thu Oct 29 18:17:26 2009 +0100
@@ -231,7 +231,7 @@
fun name_of_typ (Type (s, Ts)) =
let val s' = Long_Name.base_name s
- in space_implode "_" (List.filter (not o equal "") (map name_of_typ Ts) @
+ in space_implode "_" (filter_out (equal "") (map name_of_typ Ts) @
[if Syntax.is_identifier s' then s' else "x"])
end
| name_of_typ _ = "";
@@ -272,7 +272,7 @@
fun get_arities descr = fold (fn (_, (_, _, constrs)) =>
fold (fn (_, cargs) => fold (insert op =) (map (length o fst o strip_dtyp)
- (List.filter is_rec_type cargs))) constrs) descr [];
+ (filter is_rec_type cargs))) constrs) descr [];
(* interpret construction of datatype *)
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Oct 29 18:17:26 2009 +0100
@@ -42,8 +42,8 @@
fun add_dt_defs thy defs dep module (descr: Datatype.descr) sorts gr =
let
- val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
- val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) =>
+ val descr' = filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
+ val rtnames = map (#1 o snd) (filter (fn (_, (_, _, cs)) =>
exists (exists DatatypeAux.is_rec_type o snd) cs) descr');
val (_, (tname, _, _)) :: _ = descr';
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Thu Oct 29 18:17:26 2009 +0100
@@ -130,11 +130,11 @@
(make_pred (body_index dt) U $ app_bnds (Free (s, T)) (length Us)))
end;
- val recs = List.filter is_rec_type cargs;
+ val recs = filter is_rec_type cargs;
val Ts = map (typ_of_dtyp descr' sorts) cargs;
val recTs' = map (typ_of_dtyp descr' sorts) recs;
val tnames = Name.variant_list pnames (make_tnames Ts);
- val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
+ val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
val frees = tnames ~~ Ts;
val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
@@ -190,7 +190,7 @@
map (fn (_, cargs) =>
let
val Ts = map (typ_of_dtyp descr' sorts) cargs;
- val recs = List.filter (is_rec_type o fst) (cargs ~~ Ts);
+ val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
fun mk_argT (dt, T) =
binder_types T ---> List.nth (rec_result_Ts, body_index dt);
@@ -223,11 +223,11 @@
fun make_primrec T comb_t (cname, cargs) (ts, f::fs) =
let
- val recs = List.filter is_rec_type cargs;
+ val recs = filter is_rec_type cargs;
val Ts = map (typ_of_dtyp descr' sorts) cargs;
val recTs' = map (typ_of_dtyp descr' sorts) recs;
val tnames = make_tnames Ts;
- val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
+ val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
val frees = map Free (tnames ~~ Ts);
val frees' = map Free (rec_tnames ~~ recTs');
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Oct 29 18:17:26 2009 +0100
@@ -419,7 +419,7 @@
val rec_consts = fold add_term_consts_2 cs' [];
val intr_consts = fold add_term_consts_2 intr_ts' [];
fun unify (cname, cT) =
- let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
+ let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
val (env, _) = fold unify rec_consts (Vartab.empty, i');
val subst = map_types (Envir.norm_type env)
@@ -1036,7 +1036,7 @@
fun check_modes_pred options with_generator thy param_vs clauses modes gen_modes (p, ms) =
let
val rs = case AList.lookup (op =) clauses p of SOME rs => rs | NONE => []
- in (p, List.filter (fn m => case find_index
+ in (p, filter (fn m => case find_index
(is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
~1 => true
| i => (print_failed_mode options thy modes p m rs i; false)) ms)
--- a/src/HOL/Tools/TFL/post.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/TFL/post.ML Thu Oct 29 18:17:26 2009 +0100
@@ -71,7 +71,7 @@
| _ => r RS P_imp_P_eq_True
(*Is this the best way to invoke the simplifier??*)
-fun rewrite L = rewrite_rule (map mk_meta_eq (List.filter(not o id_thm) L))
+fun rewrite L = rewrite_rule (map mk_meta_eq (filter_out id_thm L))
fun join_assums th =
let val thy = Thm.theory_of_thm th
--- a/src/HOL/Tools/TFL/rules.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/TFL/rules.ML Thu Oct 29 18:17:26 2009 +0100
@@ -807,7 +807,7 @@
(prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
val th2 = equal_elim th1 th
in
- (th2, List.filter (not o restricted) (!tc_list))
+ (th2, filter_out restricted (!tc_list))
end;
--- a/src/HOL/Tools/TFL/tfl.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML Thu Oct 29 18:17:26 2009 +0100
@@ -423,13 +423,13 @@
end;
-fun givens pats = map pat_of (List.filter given pats);
+fun givens pats = map pat_of (filter given pats);
fun post_definition meta_tflCongs (theory, (def, pats)) =
let val tych = Thry.typecheck theory
val f = #lhs(S.dest_eq(concl def))
val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
- val pats' = List.filter given pats
+ val pats' = filter given pats
val given_pats = map pat_of pats'
val rows = map row_of_pat pats'
val WFR = #ant(S.dest_imp(concl corollary))
@@ -821,7 +821,7 @@
let val ex_tm = S.mk_exists{Bvar=v,Body=tm}
in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm)
end
- val [veq] = List.filter (can S.dest_eq) (#1 (R.dest_thm thm))
+ val [veq] = filter (can S.dest_eq) (#1 (R.dest_thm thm))
val {lhs,rhs} = S.dest_eq veq
val L = S.free_vars_lr rhs
in #2 (fold_rev CHOOSER L (veq,thm)) end;
--- a/src/HOL/Tools/choice_specification.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/choice_specification.ML Thu Oct 29 18:17:26 2009 +0100
@@ -143,7 +143,7 @@
val (_, c') = Type.varify [] c
val (cname,ctyp) = dest_Const c'
in
- case List.filter (fn t => let val (name,typ) = dest_Const t
+ case filter (fn t => let val (name,typ) = dest_Const t
in name = cname andalso Sign.typ_equiv thy (typ, ctyp)
end) thawed_prop_consts of
[] => error ("Specification: No suitable instances of constant \"" ^ Syntax.string_of_term_global thy c ^ "\" found")
--- a/src/HOL/Tools/inductive.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/inductive.ML Thu Oct 29 18:17:26 2009 +0100
@@ -392,7 +392,7 @@
list_all (params',
Logic.list_implies (map (HOLogic.mk_Trueprop o HOLogic.mk_eq)
(frees ~~ us) @ ts, P));
- val c_intrs = (List.filter (equal c o #1 o #1 o #1) intrs);
+ val c_intrs = filter (equal c o #1 o #1 o #1) intrs;
val prems = HOLogic.mk_Trueprop (list_comb (c, params @ frees)) ::
map mk_elim_prem (map #1 c_intrs)
in
--- a/src/HOL/Tools/inductive_codegen.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Thu Oct 29 18:17:26 2009 +0100
@@ -174,7 +174,7 @@
let val is' = map (fn i => i - k) (List.drop (is, k))
in map (fn x => Mode (m, is', x)) (cprods (map
(fn (NONE, _) => [NONE]
- | (SOME js, arg) => map SOME (List.filter
+ | (SOME js, arg) => map SOME (filter
(fn Mode (_, js', _) => js=js') (modes_of modes arg)))
(iss ~~ args1)))
end
@@ -237,7 +237,7 @@
fun check_modes_pred thy arg_vs preds modes (p, ms) =
let val SOME rs = AList.lookup (op =) preds p
- in (p, List.filter (fn m => case find_index
+ in (p, filter (fn m => case find_index
(not o check_mode_clause thy arg_vs modes m) rs of
~1 => true
| i => (message ("Clause " ^ string_of_int (i+1) ^ " of " ^
--- a/src/HOL/Tools/lin_arith.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML Thu Oct 29 18:17:26 2009 +0100
@@ -681,7 +681,7 @@
val beta_eta_norm = map (apsnd (map (Envir.eta_contract o Envir.beta_norm)))
split_goals
(* TRY (etac notE) THEN eq_assume_tac: *)
- val result = List.filter (not o negated_term_occurs_positively o snd)
+ val result = filter_out (negated_term_occurs_positively o snd)
beta_eta_norm
in
result
--- a/src/HOL/Tools/meson.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/meson.ML Thu Oct 29 18:17:26 2009 +0100
@@ -450,7 +450,7 @@
(*Is the given disjunction an all-negative support clause?*)
fun is_negative th = forall (not o #1) (literals (prop_of th));
-val neg_clauses = List.filter is_negative;
+val neg_clauses = filter is_negative;
(***** MESON PROOF PROCEDURE *****)
--- a/src/HOL/Tools/metis_tools.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/metis_tools.ML Thu Oct 29 18:17:26 2009 +0100
@@ -63,62 +63,62 @@
fun metis_lit b c args = (b, (c, args));
-fun hol_type_to_fol (ResClause.AtomV x) = Metis.Term.Var x
- | hol_type_to_fol (ResClause.AtomF x) = Metis.Term.Fn(x,[])
- | hol_type_to_fol (ResClause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
+fun hol_type_to_fol (Res_Clause.AtomV x) = Metis.Term.Var x
+ | hol_type_to_fol (Res_Clause.AtomF x) = Metis.Term.Fn(x,[])
+ | hol_type_to_fol (Res_Clause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
(*These two functions insert type literals before the real literals. That is the
opposite order from TPTP linkup, but maybe OK.*)
fun hol_term_to_fol_FO tm =
- case ResHolClause.strip_comb tm of
- (ResHolClause.CombConst(c,_,tys), tms) =>
+ case Res_HOL_Clause.strip_comb tm of
+ (Res_HOL_Clause.CombConst(c,_,tys), tms) =>
let val tyargs = map hol_type_to_fol tys
val args = map hol_term_to_fol_FO tms
in Metis.Term.Fn (c, tyargs @ args) end
- | (ResHolClause.CombVar(v,_), []) => Metis.Term.Var v
+ | (Res_HOL_Clause.CombVar(v,_), []) => Metis.Term.Var v
| _ => error "hol_term_to_fol_FO";
-fun hol_term_to_fol_HO (ResHolClause.CombVar (a, _)) = Metis.Term.Var a
- | hol_term_to_fol_HO (ResHolClause.CombConst (a, _, tylist)) =
+fun hol_term_to_fol_HO (Res_HOL_Clause.CombVar (a, _)) = Metis.Term.Var a
+ | hol_term_to_fol_HO (Res_HOL_Clause.CombConst (a, _, tylist)) =
Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
- | hol_term_to_fol_HO (ResHolClause.CombApp (tm1, tm2)) =
+ | hol_term_to_fol_HO (Res_HOL_Clause.CombApp (tm1, tm2)) =
Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
(*The fully-typed translation, to avoid type errors*)
fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
-fun hol_term_to_fol_FT (ResHolClause.CombVar(a, ty)) =
+fun hol_term_to_fol_FT (Res_HOL_Clause.CombVar(a, ty)) =
wrap_type (Metis.Term.Var a, ty)
- | hol_term_to_fol_FT (ResHolClause.CombConst(a, ty, _)) =
+ | hol_term_to_fol_FT (Res_HOL_Clause.CombConst(a, ty, _)) =
wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
- | hol_term_to_fol_FT (tm as ResHolClause.CombApp(tm1,tm2)) =
+ | hol_term_to_fol_FT (tm as Res_HOL_Clause.CombApp(tm1,tm2)) =
wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
- ResHolClause.type_of_combterm tm);
+ Res_HOL_Clause.type_of_combterm tm);
-fun hol_literal_to_fol FO (ResHolClause.Literal (pol, tm)) =
- let val (ResHolClause.CombConst(p,_,tys), tms) = ResHolClause.strip_comb tm
+fun hol_literal_to_fol FO (Res_HOL_Clause.Literal (pol, tm)) =
+ let val (Res_HOL_Clause.CombConst(p,_,tys), tms) = Res_HOL_Clause.strip_comb tm
val tylits = if p = "equal" then [] else map hol_type_to_fol tys
val lits = map hol_term_to_fol_FO tms
in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
- | hol_literal_to_fol HO (ResHolClause.Literal (pol, tm)) =
- (case ResHolClause.strip_comb tm of
- (ResHolClause.CombConst("equal",_,_), tms) =>
+ | hol_literal_to_fol HO (Res_HOL_Clause.Literal (pol, tm)) =
+ (case Res_HOL_Clause.strip_comb tm of
+ (Res_HOL_Clause.CombConst("equal",_,_), tms) =>
metis_lit pol "=" (map hol_term_to_fol_HO tms)
| _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]) (*hBOOL*)
- | hol_literal_to_fol FT (ResHolClause.Literal (pol, tm)) =
- (case ResHolClause.strip_comb tm of
- (ResHolClause.CombConst("equal",_,_), tms) =>
+ | hol_literal_to_fol FT (Res_HOL_Clause.Literal (pol, tm)) =
+ (case Res_HOL_Clause.strip_comb tm of
+ (Res_HOL_Clause.CombConst("equal",_,_), tms) =>
metis_lit pol "=" (map hol_term_to_fol_FT tms)
| _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
fun literals_of_hol_thm thy mode t =
- let val (lits, types_sorts) = ResHolClause.literals_of_term thy t
+ let val (lits, types_sorts) = Res_HOL_Clause.literals_of_term thy t
in (map (hol_literal_to_fol mode) lits, types_sorts) end;
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
-fun metis_of_typeLit pos (ResClause.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x]
- | metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
+fun metis_of_typeLit pos (Res_Clause.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x]
+ | metis_of_typeLit pos (Res_Clause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
fun default_sort _ (TVar _) = false
| default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
@@ -132,9 +132,9 @@
(literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
in
if is_conjecture then
- (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), ResClause.add_typs types_sorts)
+ (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), Res_Clause.add_typs types_sorts)
else
- let val tylits = ResClause.add_typs
+ let val tylits = Res_Clause.add_typs
(filter (not o default_sort ctxt) types_sorts)
val mtylits = if Config.get ctxt type_lits
then map (metis_of_typeLit false) tylits else []
@@ -145,13 +145,13 @@
(* ARITY CLAUSE *)
-fun m_arity_cls (ResClause.TConsLit (c,t,args)) =
- metis_lit true (ResClause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
- | m_arity_cls (ResClause.TVarLit (c,str)) =
- metis_lit false (ResClause.make_type_class c) [Metis.Term.Var str];
+fun m_arity_cls (Res_Clause.TConsLit (c,t,args)) =
+ metis_lit true (Res_Clause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
+ | m_arity_cls (Res_Clause.TVarLit (c,str)) =
+ metis_lit false (Res_Clause.make_type_class c) [Metis.Term.Var str];
(*TrueI is returned as the Isabelle counterpart because there isn't any.*)
-fun arity_cls (ResClause.ArityClause{conclLit,premLits,...}) =
+fun arity_cls (Res_Clause.ArityClause{conclLit,premLits,...}) =
(TrueI,
Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
@@ -160,7 +160,7 @@
fun m_classrel_cls subclass superclass =
[metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
-fun classrel_cls (ResClause.ClassrelClause {subclass, superclass, ...}) =
+fun classrel_cls (Res_Clause.ClassrelClause {subclass, superclass, ...}) =
(TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
(* ------------------------------------------------------------------------- *)
@@ -209,14 +209,14 @@
| strip_happ args x = (x, args);
fun fol_type_to_isa _ (Metis.Term.Var v) =
- (case ResReconstruct.strip_prefix ResClause.tvar_prefix v of
- SOME w => ResReconstruct.make_tvar w
- | NONE => ResReconstruct.make_tvar v)
+ (case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix v of
+ SOME w => Res_Reconstruct.make_tvar w
+ | NONE => Res_Reconstruct.make_tvar v)
| fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
- (case ResReconstruct.strip_prefix ResClause.tconst_prefix x of
- SOME tc => Term.Type (ResReconstruct.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
+ (case Res_Reconstruct.strip_prefix Res_Clause.tconst_prefix x of
+ SOME tc => Term.Type (Res_Reconstruct.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
| NONE =>
- case ResReconstruct.strip_prefix ResClause.tfree_prefix x of
+ case Res_Reconstruct.strip_prefix Res_Clause.tfree_prefix x of
SOME tf => mk_tfree ctxt tf
| NONE => error ("fol_type_to_isa: " ^ x));
@@ -225,10 +225,10 @@
let val thy = ProofContext.theory_of ctxt
val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
fun tm_to_tt (Metis.Term.Var v) =
- (case ResReconstruct.strip_prefix ResClause.tvar_prefix v of
- SOME w => Type (ResReconstruct.make_tvar w)
+ (case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix v of
+ SOME w => Type (Res_Reconstruct.make_tvar w)
| NONE =>
- case ResReconstruct.strip_prefix ResClause.schematic_var_prefix v of
+ case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix v of
SOME w => Term (mk_var (w, HOLogic.typeT))
| NONE => Term (mk_var (v, HOLogic.typeT)) )
(*Var from Metis with a name like _nnn; possibly a type variable*)
@@ -245,14 +245,14 @@
and applic_to_tt ("=",ts) =
Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts)))
| applic_to_tt (a,ts) =
- case ResReconstruct.strip_prefix ResClause.const_prefix a of
+ case Res_Reconstruct.strip_prefix Res_Clause.const_prefix a of
SOME b =>
- let val c = ResReconstruct.invert_const b
- val ntypes = ResReconstruct.num_typargs thy c
+ let val c = Res_Reconstruct.invert_const b
+ val ntypes = Res_Reconstruct.num_typargs thy c
val nterms = length ts - ntypes
val tts = map tm_to_tt ts
val tys = types_of (List.take(tts,ntypes))
- val ntyargs = ResReconstruct.num_typargs thy c
+ val ntyargs = Res_Reconstruct.num_typargs thy c
in if length tys = ntyargs then
apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
@@ -263,14 +263,14 @@
cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
end
| NONE => (*Not a constant. Is it a type constructor?*)
- case ResReconstruct.strip_prefix ResClause.tconst_prefix a of
+ case Res_Reconstruct.strip_prefix Res_Clause.tconst_prefix a of
SOME b =>
- Type (Term.Type (ResReconstruct.invert_type_const b, types_of (map tm_to_tt ts)))
+ Type (Term.Type (Res_Reconstruct.invert_type_const b, types_of (map tm_to_tt ts)))
| NONE => (*Maybe a TFree. Should then check that ts=[].*)
- case ResReconstruct.strip_prefix ResClause.tfree_prefix a of
+ case Res_Reconstruct.strip_prefix Res_Clause.tfree_prefix a of
SOME b => Type (mk_tfree ctxt b)
| NONE => (*a fixed variable? They are Skolem functions.*)
- case ResReconstruct.strip_prefix ResClause.fixed_var_prefix a of
+ case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix a of
SOME b =>
let val opr = Term.Free(b, HOLogic.typeT)
in apply_list opr (length ts) (map tm_to_tt ts) end
@@ -281,16 +281,16 @@
fun fol_term_to_hol_FT ctxt fol_tm =
let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
- (case ResReconstruct.strip_prefix ResClause.schematic_var_prefix v of
+ (case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix v of
SOME w => mk_var(w, dummyT)
| NONE => mk_var(v, dummyT))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
Const ("op =", HOLogic.typeT)
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
- (case ResReconstruct.strip_prefix ResClause.const_prefix x of
- SOME c => Const (ResReconstruct.invert_const c, dummyT)
+ (case Res_Reconstruct.strip_prefix Res_Clause.const_prefix x of
+ SOME c => Const (Res_Reconstruct.invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
- case ResReconstruct.strip_prefix ResClause.fixed_var_prefix x of
+ case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix x of
SOME v => Free (v, fol_type_to_isa ctxt ty)
| NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
@@ -301,10 +301,10 @@
| cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2])
| cvt (t as Metis.Term.Fn (x, [])) =
- (case ResReconstruct.strip_prefix ResClause.const_prefix x of
- SOME c => Const (ResReconstruct.invert_const c, dummyT)
+ (case Res_Reconstruct.strip_prefix Res_Clause.const_prefix x of
+ SOME c => Const (Res_Reconstruct.invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
- case ResReconstruct.strip_prefix ResClause.fixed_var_prefix x of
+ case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix x of
SOME v => Free (v, dummyT)
| NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x);
fol_term_to_hol_RAW ctxt t))
@@ -383,9 +383,9 @@
" in " ^ Display.string_of_thm ctxt i_th);
NONE)
fun remove_typeinst (a, t) =
- case ResReconstruct.strip_prefix ResClause.schematic_var_prefix a of
+ case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix a of
SOME b => SOME (b, t)
- | NONE => case ResReconstruct.strip_prefix ResClause.tvar_prefix a of
+ | NONE => case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix a of
SOME _ => NONE (*type instantiations are forbidden!*)
| NONE => SOME (a,t) (*internal Metis var?*)
val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
@@ -452,7 +452,7 @@
in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
fun get_ty_arg_size _ (Const ("op =", _)) = 0 (*equality has no type arguments*)
- | get_ty_arg_size thy (Const (c, _)) = (ResReconstruct.num_typargs thy c handle TYPE _ => 0)
+ | get_ty_arg_size thy (Const (c, _)) = (Res_Reconstruct.num_typargs thy c handle TYPE _ => 0)
| get_ty_arg_size _ _ = 0;
(* INFERENCE RULE: EQUALITY *)
@@ -538,7 +538,7 @@
| step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
equality_inf ctxt mode f_lit f_p f_r;
-fun real_literal (_, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
+fun real_literal (_, (c, _)) = not (String.isPrefix Res_Clause.class_prefix c);
fun translate _ _ thpairs [] = thpairs
| translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
@@ -564,23 +564,23 @@
(* Translation of HO Clauses *)
(* ------------------------------------------------------------------------- *)
-fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th);
+fun cnf_th thy th = hd (Res_Axioms.cnf_axiom thy th);
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 @{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;
+val comb_I = cnf_th @{theory} Res_HOL_Clause.comb_I;
+val comb_K = cnf_th @{theory} Res_HOL_Clause.comb_K;
+val comb_B = cnf_th @{theory} Res_HOL_Clause.comb_B;
+val comb_C = cnf_th @{theory} Res_HOL_Clause.comb_C;
+val comb_S = cnf_th @{theory} Res_HOL_Clause.comb_S;
fun type_ext thy tms =
- let val subs = ResAtp.tfree_classes_of_terms tms
- val supers = ResAtp.tvar_classes_of_terms tms
- and tycons = ResAtp.type_consts_of_terms thy tms
- val (supers', arity_clauses) = ResClause.make_arity_clauses thy tycons supers
- val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
+ let val subs = Res_ATP.tfree_classes_of_terms tms
+ val supers = Res_ATP.tvar_classes_of_terms tms
+ and tycons = Res_ATP.type_consts_of_terms thy tms
+ val (supers', arity_clauses) = Res_Clause.make_arity_clauses thy tycons supers
+ val classrel_clauses = Res_Clause.make_classrel_clauses thy subs supers'
in map classrel_cls classrel_clauses @ map arity_cls arity_clauses
end;
@@ -590,7 +590,7 @@
type logic_map =
{axioms : (Metis.Thm.thm * thm) list,
- tfrees : ResClause.type_literal list};
+ tfrees : Res_Clause.type_literal list};
fun const_in_metis c (pred, tm_list) =
let
@@ -602,7 +602,7 @@
(*Extract TFree constraints from context to include as conjecture clauses*)
fun init_tfrees ctxt =
let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
- in ResClause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
+ in Res_Clause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
(*transform isabelle type / arity clause to metis clause *)
fun add_type_thm [] lmap = lmap
@@ -664,7 +664,7 @@
(* Main function to start metis prove and reconstruction *)
fun FOL_SOLVE mode ctxt cls ths0 =
let val thy = ProofContext.theory_of ctxt
- val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
+ val th_cls_pairs = map (fn th => (Thm.get_name_hint th, Res_Axioms.cnf_axiom thy th)) ths0
val ths = maps #2 th_cls_pairs
val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
@@ -673,14 +673,14 @@
val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
val _ = if null tfrees then ()
else (trace_msg (fn () => "TFREE CLAUSES");
- app (fn tf => trace_msg (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)
+ app (fn tf => trace_msg (fn _ => Res_Clause.tptp_of_typeLit true tf)) tfrees)
val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
val thms = map #1 axioms
val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
in
- case List.filter (is_false o prop_of) cls of
+ case filter (is_false o prop_of) cls of
false_th::_ => [false_th RS @{thm FalseE}]
| [] =>
case refute thms of
@@ -694,10 +694,11 @@
and used = map_filter (used_axioms axioms) proof
val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
- val unused = filter (fn (_, cls) => not (common_thm used cls)) th_cls_pairs
+ val unused = th_cls_pairs |> map_filter (fn (name, cls) =>
+ if common_thm used cls then NONE else SOME name)
in
if null unused then ()
- else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
+ else warning ("Metis: unused theorems " ^ commas_quote unused);
case result of
(_,ith)::_ =>
(trace_msg (fn () => "success: " ^ Display.string_of_thm ctxt ith);
@@ -714,12 +715,12 @@
let val _ = trace_msg (fn () =>
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
- if exists_type ResAxioms.type_has_empty_sort (prop_of st0)
+ if exists_type Res_Axioms.type_has_empty_sort (prop_of st0)
then (warning "Proof state contains the empty sort"; Seq.empty)
else
- (Meson.MESON ResAxioms.neg_clausify
+ (Meson.MESON Res_Axioms.neg_clausify
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
- THEN ResAxioms.expand_defs_tac st0) st0
+ THEN Res_Axioms.expand_defs_tac st0) st0
end
handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
@@ -736,7 +737,7 @@
method @{binding metisF} FO "METIS for FOL problems" #>
method @{binding metisFT} FT "METIS With-fully typed translation" #>
Method.setup @{binding finish_clausify}
- (Scan.succeed (K (SIMPLE_METHOD (ResAxioms.expand_defs_tac refl))))
+ (Scan.succeed (K (SIMPLE_METHOD (Res_Axioms.expand_defs_tac refl))))
"cleanup after conversion to clauses";
end;
--- a/src/HOL/Tools/old_primrec.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/old_primrec.ML Thu Oct 29 18:17:26 2009 +0100
@@ -195,7 +195,7 @@
NONE =>
let
val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined",
- replicate ((length cargs) + (length (List.filter is_rec_type cargs)))
+ replicate (length cargs + length (filter is_rec_type cargs))
dummyT ---> HOLogic.unitT)) constrs;
val _ = warning ("No function definition for datatype " ^ quote tname)
in
--- a/src/HOL/Tools/primrec.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/primrec.ML Thu Oct 29 18:17:26 2009 +0100
@@ -178,7 +178,7 @@
NONE =>
let
val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined",
- replicate ((length cargs) + (length (List.filter is_rec_type cargs)))
+ replicate (length cargs + length (filter is_rec_type cargs))
dummyT ---> HOLogic.unitT)) constrs;
val _ = warning ("No function definition for datatype " ^ quote tname)
in
--- a/src/HOL/Tools/refute.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/refute.ML Thu Oct 29 18:17:26 2009 +0100
@@ -394,7 +394,7 @@
(* (string * int) list *)
val sizes = map_filter
(fn (name, value) => Option.map (pair name) (Int.fromString value))
- (List.filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
+ (filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
andalso name<>"maxvars" andalso name<>"maxtime"
andalso name<>"satsolver") allparams)
in
@@ -1070,8 +1070,7 @@
(* continue search *)
next max (len+1) (sum+x1) (x2::xs)
(* only consider those types for which the size is not fixed *)
- val mutables = List.filter
- (not o (AList.defined (op =) sizes) o string_of_typ o fst) xs
+ val mutables = filter_out (AList.defined (op =) sizes o string_of_typ o fst) xs
(* subtract 'minsize' from every size (will be added again at the end) *)
val diffs = map (fn (_, n) => n-minsize) mutables
in
@@ -2552,7 +2551,7 @@
(* arguments *)
val (_, _, constrs) = the (AList.lookup (op =) descr idx)
val (_, dtyps) = List.nth (constrs, c)
- val rec_dtyps_args = List.filter
+ val rec_dtyps_args = filter
(DatatypeAux.is_rec_type o fst) (dtyps ~~ args)
(* map those indices to interpretations *)
val rec_dtyps_intrs = map (fn (dtyp, arg) =>
--- a/src/HOL/Tools/res_atp.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/res_atp.ML Thu Oct 29 18:17:26 2009 +0100
@@ -1,4 +1,6 @@
-(* Author: Jia Meng, Cambridge University Computer Laboratory, NICTA *)
+(* Title: HOL/Tools/res_atp.ML
+ Author: Jia Meng, Cambridge University Computer Laboratory, NICTA
+*)
signature RES_ATP =
sig
@@ -9,14 +11,14 @@
val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
(thm * (string * int)) list
val prepare_clauses : bool -> thm list -> thm list ->
- (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list ->
- (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory ->
- ResHolClause.axiom_name vector *
- (ResHolClause.clause list * ResHolClause.clause list * ResHolClause.clause list *
- ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
+ (thm * (Res_HOL_Clause.axiom_name * Res_HOL_Clause.clause_id)) list ->
+ (thm * (Res_HOL_Clause.axiom_name * Res_HOL_Clause.clause_id)) list -> theory ->
+ Res_HOL_Clause.axiom_name vector *
+ (Res_HOL_Clause.clause list * Res_HOL_Clause.clause list * Res_HOL_Clause.clause list *
+ Res_HOL_Clause.clause list * Res_Clause.classrelClause list * Res_Clause.arityClause list)
end;
-structure ResAtp: RES_ATP =
+structure Res_ATP: RES_ATP =
struct
@@ -236,10 +238,10 @@
let val cls = sort compare_pairs newpairs
val accepted = List.take (cls, max_new)
in
- ResAxioms.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
+ Res_Axioms.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
", exceeds the limit of " ^ Int.toString (max_new)));
- ResAxioms.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
- ResAxioms.trace_msg (fn () => "Actually passed: " ^
+ Res_Axioms.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
+ Res_Axioms.trace_msg (fn () => "Actually passed: " ^
space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
(map #1 accepted, map #1 (List.drop (cls, max_new)))
@@ -254,7 +256,7 @@
val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
val newp = p + (1.0-p) / convergence
in
- ResAxioms.trace_msg (fn () => ("relevant this iteration: " ^ Int.toString (length newrels)));
+ Res_Axioms.trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
(map #1 newrels) @
(relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
end
@@ -262,12 +264,12 @@
let val weight = clause_weight ctab rel_consts consts_typs
in
if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts)
- then (ResAxioms.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^
+ then (Res_Axioms.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^
" passes: " ^ Real.toString weight));
relevant ((ax,weight)::newrels, rejects) axs)
else relevant (newrels, ax::rejects) axs
end
- in ResAxioms.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
+ in Res_Axioms.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
relevant ([],[])
end;
@@ -276,12 +278,12 @@
then
let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
val goal_const_tab = get_goal_consts_typs thy goals
- val _ = ResAxioms.trace_msg (fn () => ("Initial constants: " ^
+ val _ = Res_Axioms.trace_msg (fn () => ("Initial constants: " ^
space_implode ", " (Symtab.keys goal_const_tab)));
val rels = relevant_clauses max_new thy const_tab (pass_mark)
goal_const_tab (map (pair_consts_typs_axiom theory_const thy) axioms)
in
- ResAxioms.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
+ Res_Axioms.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
rels
end
else axioms;
@@ -335,7 +337,7 @@
fun make_unique xs =
let val ht = mk_clause_table 7000
in
- ResAxioms.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
+ Res_Axioms.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
app (ignore o Polyhash.peekInsert ht) xs;
Polyhash.listItems ht
end;
@@ -352,11 +354,12 @@
fun valid_facts facts =
Facts.fold_static (fn (name, ths) =>
- if run_blacklist_filter andalso is_package_def name then I
+ if Facts.is_concealed facts name orelse
+ (run_blacklist_filter andalso is_package_def name) then I
else
let val xname = Facts.extern facts name in
if Name_Space.is_hidden xname then I
- else cons (xname, filter_out ResAxioms.bad_for_atp ths)
+ else cons (xname, filter_out Res_Axioms.bad_for_atp ths)
end) facts [];
fun all_valid_thms ctxt =
@@ -365,29 +368,29 @@
val local_facts = ProofContext.facts_of ctxt;
in valid_facts global_facts @ valid_facts local_facts end;
-fun multi_name a (th, (n,pairs)) =
- (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
+fun multi_name a th (n, pairs) =
+ (n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs);
-fun add_single_names ((a, []), pairs) = pairs
- | add_single_names ((a, [th]), pairs) = (a,th)::pairs
- | add_single_names ((a, ths), pairs) = #2 (List.foldl (multi_name a) (1,pairs) ths);
+fun add_single_names (a, []) pairs = pairs
+ | add_single_names (a, [th]) pairs = (a, th) :: pairs
+ | add_single_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs));
(*Ignore blacklisted basenames*)
-fun add_multi_names ((a, ths), pairs) =
- if (Long_Name.base_name a) mem_string ResAxioms.multi_base_blacklist then pairs
- else add_single_names ((a, ths), pairs);
+fun add_multi_names (a, ths) pairs =
+ if (Long_Name.base_name a) mem_string Res_Axioms.multi_base_blacklist then pairs
+ else add_single_names (a, ths) pairs;
fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
(*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*)
fun name_thm_pairs ctxt =
- let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
- val ht = mk_clause_table 900 (*ht for blacklisted theorems*)
- fun blacklisted x = run_blacklist_filter andalso is_some (Polyhash.peek ht x)
+ let
+ val (mults, singles) = List.partition is_multi (all_valid_thms ctxt)
+ fun blacklisted (_, th) =
+ run_blacklist_filter andalso Res_Blacklist.blacklisted ctxt th
in
- app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt);
- filter (not o blacklisted o #2)
- (List.foldl add_single_names (List.foldl add_multi_names [] mults) singles)
+ filter_out blacklisted
+ (fold add_single_names singles (fold add_multi_names mults []))
end;
fun check_named ("", th) =
@@ -396,7 +399,7 @@
fun get_all_lemmas ctxt =
let val included_thms =
- tap (fn ths => ResAxioms.trace_msg
+ tap (fn ths => Res_Axioms.trace_msg
(fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
(name_thm_pairs ctxt)
in
@@ -499,17 +502,14 @@
| Fol => true
| Hol => false
-fun ths_to_cls thy ths =
- ResAxioms.cnf_rules_pairs thy (filter check_named (map ResAxioms.pairname ths))
-
fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
let
val thy = ProofContext.theory_of ctxt
val isFO = isFO thy goal_cls
- val included_thms = get_all_lemmas ctxt
- val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
- |> restrict_to_logic thy isFO
- |> remove_unwanted_clauses
+ val included_cls = get_all_lemmas ctxt
+ |> Res_Axioms.cnf_rules_pairs thy |> make_unique
+ |> restrict_to_logic thy isFO
+ |> remove_unwanted_clauses
in
relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
end;
@@ -519,24 +519,25 @@
fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
let
(* add chain thms *)
- val chain_cls = ths_to_cls thy chain_ths
+ val chain_cls =
+ Res_Axioms.cnf_rules_pairs thy (filter check_named (map Res_Axioms.pairname chain_ths))
val axcls = chain_cls @ axcls
val extra_cls = chain_cls @ extra_cls
val isFO = isFO thy goal_cls
val ccls = subtract_cls goal_cls extra_cls
- val _ = app (fn th => ResAxioms.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
+ val _ = app (fn th => Res_Axioms.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
val ccltms = map prop_of ccls
and axtms = map (prop_of o #1) extra_cls
val subs = tfree_classes_of_terms ccltms
and supers = tvar_classes_of_terms axtms
and tycons = type_consts_of_terms thy (ccltms@axtms)
(*TFrees in conjecture clauses; TVars in axiom clauses*)
- val conjectures = ResHolClause.make_conjecture_clauses dfg thy ccls
- val (_, extra_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy extra_cls)
- val (clnames,axiom_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy axcls)
- val helper_clauses = ResHolClause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
- val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
- val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
+ val conjectures = Res_HOL_Clause.make_conjecture_clauses dfg thy ccls
+ val (_, extra_clauses) = ListPair.unzip (Res_HOL_Clause.make_axiom_clauses dfg thy extra_cls)
+ val (clnames,axiom_clauses) = ListPair.unzip (Res_HOL_Clause.make_axiom_clauses dfg thy axcls)
+ val helper_clauses = Res_HOL_Clause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
+ val (supers',arity_clauses) = Res_Clause.make_arity_clauses_dfg dfg thy tycons supers
+ val classrel_clauses = Res_Clause.make_classrel_clauses thy subs supers'
in
(Vector.fromList clnames,
(conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
--- a/src/HOL/Tools/res_axioms.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML Thu Oct 29 18:17:26 2009 +0100
@@ -1,4 +1,5 @@
-(* Author: Jia Meng, Cambridge University Computer Laboratory
+(* Title: HOL/Tools/res_axioms.ML
+ Author: Jia Meng, Cambridge University Computer Laboratory
Transformation of axiom rules (elim/intro/etc) into CNF forms.
*)
@@ -22,7 +23,7 @@
val setup: theory -> theory
end;
-structure ResAxioms: RES_AXIOMS =
+structure Res_Axioms: RES_AXIOMS =
struct
val trace = Unsynchronized.ref false;
@@ -285,7 +286,7 @@
map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
-(*** Blacklisting (duplicated in ResAtp?) ***)
+(*** Blacklisting (duplicated in Res_ATP?) ***)
val max_lambda_nesting = 3;
@@ -316,18 +317,17 @@
fun is_strange_thm th =
case head_of (concl_of th) of
- Const (a,_) => (a <> "Trueprop" andalso a <> "==")
+ Const (a, _) => (a <> "Trueprop" andalso a <> "==")
| _ => false;
fun bad_for_atp th =
- Thm.is_internal th
- orelse too_complex (prop_of th)
+ too_complex (prop_of th)
orelse exists_type type_has_empty_sort (prop_of th)
orelse is_strange_thm th;
val multi_base_blacklist =
["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm",
- "cases","ext_cases"]; (*FIXME: put other record thms here, or use the "Internal" marker*)
+ "cases","ext_cases"]; (* FIXME put other record thms here, or declare as "noatp" *)
(*Keep the full complexity of the original name*)
fun flatten_name s = space_implode "_X" (Long_Name.explode s);
@@ -387,14 +387,14 @@
fun cnf_rules_pairs_aux _ pairs [] = pairs
| cnf_rules_pairs_aux thy pairs ((name,th)::ths) =
let val pairs' = (pair_name_cls 0 (name, cnf_axiom thy th)) @ pairs
- handle THM _ => pairs | ResClause.CLAUSE _ => pairs
+ handle THM _ => pairs | Res_Clause.CLAUSE _ => pairs
in cnf_rules_pairs_aux thy pairs' ths end;
(*The combination of rev and tail recursion preserves the original order*)
fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l);
-(**** Convert all facts of the theory into clauses (ResClause.clause, or ResHolClause.clause) ****)
+(**** Convert all facts of the theory into clauses (Res_Clause.clause, or Res_HOL_Clause.clause) ****)
local
@@ -421,8 +421,10 @@
fun saturate_skolem_cache thy =
let
- val new_facts = (PureThy.facts_of thy, []) |-> Facts.fold_static (fn (name, ths) =>
- if already_seen thy name then I else cons (name, ths));
+ val facts = PureThy.facts_of thy;
+ val new_facts = (facts, []) |-> Facts.fold_static (fn (name, ths) =>
+ if Facts.is_concealed facts name orelse already_seen thy name then I
+ else cons (name, ths));
val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
if member (op =) multi_base_blacklist (Long_Name.base_name name) then I
else fold_index (fn (i, th) =>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/res_blacklist.ML Thu Oct 29 18:17:26 2009 +0100
@@ -0,0 +1,43 @@
+(* Title: HOL/Tools/res_blacklist.ML
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Makarius
+
+Theorems blacklisted to sledgehammer. These theorems typically
+produce clauses that are prolific (match too many equality or
+membership literals) and relate to seldom-used facts. Some duplicate
+other rules.
+*)
+
+signature RES_BLACKLIST =
+sig
+ val setup: theory -> theory
+ val blacklisted: Proof.context -> thm -> bool
+ val add: attribute
+ val del: attribute
+end;
+
+structure Res_Blacklist: RES_BLACKLIST =
+struct
+
+structure Data = GenericDataFun
+(
+ type T = thm Termtab.table;
+ val empty = Termtab.empty;
+ val extend = I;
+ fun merge _ tabs = Termtab.merge (K true) tabs;
+);
+
+fun blacklisted ctxt th =
+ Termtab.defined (Data.get (Context.Proof ctxt)) (Thm.full_prop_of th);
+
+fun add_thm th = Data.map (Termtab.update (Thm.full_prop_of th, th));
+fun del_thm th = Data.map (Termtab.delete_safe (Thm.full_prop_of th));
+
+val add = Thm.declaration_attribute add_thm;
+val del = Thm.declaration_attribute del_thm;
+
+val setup =
+ Attrib.setup @{binding noatp} (Attrib.add_del add del) "sledgehammer blacklisting" #>
+ PureThy.add_thms_dynamic (@{binding noatp}, map #2 o Termtab.dest o Data.get);
+
+end;
--- a/src/HOL/Tools/res_clause.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/res_clause.ML Thu Oct 29 18:17:26 2009 +0100
@@ -1,11 +1,12 @@
-(* Author: Jia Meng, Cambridge University Computer Laboratory
- Copyright 2004 University of Cambridge
+(* Title: HOL/Tools/res_clause.ML
+ Author: Jia Meng, Cambridge University Computer Laboratory
-Storing/printing FOL clauses and arity clauses.
-Typed equality is treated differently.
+Storing/printing FOL clauses and arity clauses. Typed equality is
+treated differently.
+
+FIXME: combine with res_hol_clause!
*)
-(*FIXME: combine with res_hol_clause!*)
signature RES_CLAUSE =
sig
val schematic_var_prefix: string
@@ -76,7 +77,7 @@
val tptp_classrelClause : classrelClause -> string
end
-structure ResClause: RES_CLAUSE =
+structure Res_Clause: RES_CLAUSE =
struct
val schematic_var_prefix = "V_";
--- a/src/HOL/Tools/res_hol_clause.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/res_hol_clause.ML Thu Oct 29 18:17:26 2009 +0100
@@ -1,5 +1,5 @@
-(*
- Author: Jia Meng, NICTA
+(* Title: HOL/Tools/res_hol_clause.ML
+ Author: Jia Meng, NICTA
FOL clauses translated from HOL formulae.
*)
@@ -17,13 +17,13 @@
type polarity = bool
type clause_id = int
datatype combterm =
- CombConst of string * ResClause.fol_type * ResClause.fol_type list (*Const and Free*)
- | CombVar of string * ResClause.fol_type
+ CombConst of string * Res_Clause.fol_type * Res_Clause.fol_type list (*Const and Free*)
+ | CombVar of string * Res_Clause.fol_type
| CombApp of combterm * combterm
datatype literal = Literal of polarity * combterm
datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm,
- kind: ResClause.kind,literals: literal list, ctypes_sorts: typ list}
- val type_of_combterm: combterm -> ResClause.fol_type
+ kind: Res_Clause.kind,literals: literal list, ctypes_sorts: typ list}
+ val type_of_combterm: combterm -> Res_Clause.fol_type
val strip_comb: combterm -> combterm * combterm list
val literals_of_term: theory -> term -> literal list * typ list
exception TOO_TRIVIAL
@@ -38,18 +38,18 @@
clause list
val tptp_write_file: bool -> Path.T ->
clause list * clause list * clause list * clause list *
- ResClause.classrelClause list * ResClause.arityClause list ->
+ Res_Clause.classrelClause list * Res_Clause.arityClause list ->
int * int
val dfg_write_file: bool -> Path.T ->
clause list * clause list * clause list * clause list *
- ResClause.classrelClause list * ResClause.arityClause list ->
+ Res_Clause.classrelClause list * Res_Clause.arityClause list ->
int * int
end
-structure ResHolClause: RES_HOL_CLAUSE =
+structure Res_HOL_Clause: RES_HOL_CLAUSE =
struct
-structure RC = ResClause;
+structure RC = Res_Clause; (* FIXME avoid structure alias *)
(* theorems for combinators and function extensionality *)
val ext = thm "HOL.ext";
@@ -404,7 +404,7 @@
else ct;
fun cnf_helper_thms thy =
- ResAxioms.cnf_rules_pairs thy o map ResAxioms.pairname
+ Res_Axioms.cnf_rules_pairs thy o map Res_Axioms.pairname
fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
if isFO then [] (*first-order*)
@@ -454,7 +454,7 @@
fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
fun display_arity const_needs_hBOOL (c,n) =
- ResAxioms.trace_msg (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
+ Res_Axioms.trace_msg (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
(if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
@@ -527,4 +527,5 @@
length helper_clauses + 1, length tfree_clss + length dfg_clss)
end;
-end
+end;
+
--- a/src/HOL/Tools/res_reconstruct.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML Thu Oct 29 18:17:26 2009 +0100
@@ -1,8 +1,9 @@
-(* Author: L C Paulson and Claire Quigley, Cambridge University Computer Laboratory *)
+(* Title: HOL/Tools/res_reconstruct.ML
+ Author: Lawrence C Paulson and Claire Quigley, Cambridge University Computer Laboratory
-(***************************************************************************)
-(* Code to deal with the transfer of proofs from a prover process *)
-(***************************************************************************)
+Transfer of proofs from external provers.
+*)
+
signature RES_RECONSTRUCT =
sig
val chained_hint: string
@@ -23,13 +24,13 @@
string * string vector * (int * int) * Proof.context * thm * int -> string * string list
end;
-structure ResReconstruct : RES_RECONSTRUCT =
+structure Res_Reconstruct : RES_RECONSTRUCT =
struct
val trace_path = Path.basic "atp_trace";
fun trace s =
- if ! ResAxioms.trace then File.append (File.tmp_path trace_path) s
+ if ! Res_Axioms.trace then File.append (File.tmp_path trace_path) s
else ();
fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
@@ -106,12 +107,12 @@
(*If string s has the prefix s1, return the result of deleting it.*)
fun strip_prefix s1 s =
if String.isPrefix s1 s
- then SOME (ResClause.undo_ascii_of (String.extract (s, size s1, NONE)))
+ then SOME (Res_Clause.undo_ascii_of (String.extract (s, size s1, NONE)))
else NONE;
(*Invert the table of translations between Isabelle and ATPs*)
val type_const_trans_table_inv =
- Symtab.make (map swap (Symtab.dest ResClause.type_const_trans_table));
+ Symtab.make (map swap (Symtab.dest Res_Clause.type_const_trans_table));
fun invert_type_const c =
case Symtab.lookup type_const_trans_table_inv c of
@@ -129,15 +130,15 @@
| Br (a,ts) =>
let val Ts = map type_of_stree ts
in
- case strip_prefix ResClause.tconst_prefix a of
+ case strip_prefix Res_Clause.tconst_prefix a of
SOME b => Type(invert_type_const b, Ts)
| NONE =>
if not (null ts) then raise STREE t (*only tconsts have type arguments*)
else
- case strip_prefix ResClause.tfree_prefix a of
+ case strip_prefix Res_Clause.tfree_prefix a of
SOME b => TFree("'" ^ b, HOLogic.typeS)
| NONE =>
- case strip_prefix ResClause.tvar_prefix a of
+ case strip_prefix Res_Clause.tvar_prefix a of
SOME b => make_tvar b
| NONE => make_tvar a (*Variable from the ATP, say X1*)
end;
@@ -145,7 +146,7 @@
(*Invert the table of translations between Isabelle and ATPs*)
val const_trans_table_inv =
Symtab.update ("fequal", "op =")
- (Symtab.make (map swap (Symtab.dest ResClause.const_trans_table)));
+ (Symtab.make (map swap (Symtab.dest Res_Clause.const_trans_table)));
fun invert_const c =
case Symtab.lookup const_trans_table_inv c of
@@ -166,7 +167,7 @@
| Br ("hBOOL",[t]) => term_of_stree [] thy t (*ignore hBOOL*)
| Br ("hAPP",[t,u]) => term_of_stree (u::args) thy t
| Br (a,ts) =>
- case strip_prefix ResClause.const_prefix a of
+ case strip_prefix Res_Clause.const_prefix a of
SOME "equal" =>
list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree [] thy) ts)
| SOME b =>
@@ -180,10 +181,10 @@
| NONE => (*a variable, not a constant*)
let val T = HOLogic.typeT
val opr = (*a Free variable is typically a Skolem function*)
- case strip_prefix ResClause.fixed_var_prefix a of
+ case strip_prefix Res_Clause.fixed_var_prefix a of
SOME b => Free(b,T)
| NONE =>
- case strip_prefix ResClause.schematic_var_prefix a of
+ case strip_prefix Res_Clause.schematic_var_prefix a of
SOME b => make_var (b,T)
| NONE => make_var (a,T) (*Variable from the ATP, say X1*)
in list_comb (opr, List.map (term_of_stree [] thy) (ts@args)) end;
@@ -193,7 +194,7 @@
| constraint_of_stree pol t = case t of
Int _ => raise STREE t
| Br (a,ts) =>
- (case (strip_prefix ResClause.class_prefix a, map type_of_stree ts) of
+ (case (strip_prefix Res_Clause.class_prefix a, map type_of_stree ts) of
(SOME b, [T]) => (pol, b, T)
| _ => raise STREE t);
@@ -443,11 +444,11 @@
val _ = trace (Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
val (_,lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
val _ = trace (Int.toString (length lines) ^ " lines extracted\n")
- val (ccls,fixes) = ResAxioms.neg_conjecture_clauses ctxt th sgno
+ val (ccls,fixes) = Res_Axioms.neg_conjecture_clauses ctxt th sgno
val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
val ccls = map forall_intr_vars ccls
val _ =
- if ! ResAxioms.trace then app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
+ if ! Res_Axioms.trace then app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
else ()
val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
val _ = trace "\ndecode_tstp_file: finishing\n"
@@ -456,124 +457,128 @@
end;
- (*=== EXTRACTING PROOF-TEXT === *)
+(*=== EXTRACTING PROOF-TEXT === *)
- val begin_proof_strings = ["# SZS output start CNFRefutation.",
- "=========== Refutation ==========",
+val begin_proof_strings = ["# SZS output start CNFRefutation.",
+ "=========== Refutation ==========",
"Here is a proof"];
- val end_proof_strings = ["# SZS output end CNFRefutation",
- "======= End of refutation =======",
+
+val end_proof_strings = ["# SZS output end CNFRefutation",
+ "======= End of refutation =======",
"Formulae used in the proof"];
- fun get_proof_extract proof =
- let
+
+fun get_proof_extract proof =
+ let
(*splits to_split by the first possible of a list of splitters*)
val (begin_string, end_string) =
(find_first (fn s => String.isSubstring s proof) begin_proof_strings,
find_first (fn s => String.isSubstring s proof) end_proof_strings)
- in
- if is_none begin_string orelse is_none end_string
- then error "Could not extract proof (no substring indicating a proof)"
- else proof |> first_field (the begin_string) |> the |> snd
- |> first_field (the end_string) |> the |> fst end;
+ in
+ if is_none begin_string orelse is_none end_string
+ then error "Could not extract proof (no substring indicating a proof)"
+ else proof |> first_field (the begin_string) |> the |> snd
+ |> first_field (the end_string) |> the |> fst
+ end;
(* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
- val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable",
- "SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"];
- val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
- val failure_strings_SPASS = ["SPASS beiseite: Completion found.",
- "SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."];
- val failure_strings_remote = ["Remote-script could not extract proof"];
- fun find_failure proof =
- let val failures =
- map_filter (fn s => if String.isSubstring s proof then SOME s else NONE)
- (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote)
- val correct = null failures andalso
- exists (fn s => String.isSubstring s proof) begin_proof_strings andalso
- exists (fn s => String.isSubstring s proof) end_proof_strings
- in
- if correct then NONE
- else if null failures then SOME "Output of ATP not in proper format"
- else SOME (hd failures) end;
+val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable",
+ "SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"];
+val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
+val failure_strings_SPASS = ["SPASS beiseite: Completion found.",
+ "SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."];
+val failure_strings_remote = ["Remote-script could not extract proof"];
+fun find_failure proof =
+ let val failures =
+ map_filter (fn s => if String.isSubstring s proof then SOME s else NONE)
+ (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote)
+ val correct = null failures andalso
+ exists (fn s => String.isSubstring s proof) begin_proof_strings andalso
+ exists (fn s => String.isSubstring s proof) end_proof_strings
+ in
+ if correct then NONE
+ else if null failures then SOME "Output of ATP not in proper format"
+ else SOME (hd failures) end;
- (* === EXTRACTING LEMMAS === *)
- (* lines have the form "cnf(108, axiom, ...",
- the number (108) has to be extracted)*)
- fun get_step_nums false proofextract =
- let val toks = String.tokens (not o Char.isAlphaNum)
- fun inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok
- | inputno ("cnf"::ntok::"negated"::"conjecture"::_) = Int.fromString ntok
- | inputno _ = NONE
- val lines = split_lines proofextract
- in map_filter (inputno o toks) lines end
- (*String contains multiple lines. We want those of the form
- "253[0:Inp] et cetera..."
- A list consisting of the first number in each line is returned. *)
- | get_step_nums true proofextract =
- let val toks = String.tokens (not o Char.isAlphaNum)
- fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
- | inputno _ = NONE
- val lines = split_lines proofextract
- in map_filter (inputno o toks) lines end
-
- (*extracting lemmas from tstp-output between the lines from above*)
- fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) =
+(* === EXTRACTING LEMMAS === *)
+(* lines have the form "cnf(108, axiom, ...",
+the number (108) has to be extracted)*)
+fun get_step_nums false proofextract =
+ let val toks = String.tokens (not o Char.isAlphaNum)
+ fun inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok
+ | inputno ("cnf"::ntok::"negated"::"conjecture"::_) = Int.fromString ntok
+ | inputno _ = NONE
+ val lines = split_lines proofextract
+ in map_filter (inputno o toks) lines end
+(*String contains multiple lines. We want those of the form
+ "253[0:Inp] et cetera..."
+ A list consisting of the first number in each line is returned. *)
+| get_step_nums true proofextract =
+ let val toks = String.tokens (not o Char.isAlphaNum)
+ fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
+ | inputno _ = NONE
+ val lines = split_lines proofextract
+ in map_filter (inputno o toks) lines end
+
+(*extracting lemmas from tstp-output between the lines from above*)
+fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) =
+ let
+ (* get the names of axioms from their numbers*)
+ fun get_axiom_names thm_names step_nums =
let
- (* get the names of axioms from their numbers*)
- fun get_axiom_names thm_names step_nums =
- let
- val last_axiom = Vector.length thm_names
- fun is_axiom n = n <= last_axiom
- fun is_conj n = n >= fst conj_count andalso n < fst conj_count + snd conj_count
- fun getname i = Vector.sub(thm_names, i-1)
- in
- (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
- (map getname (filter is_axiom step_nums))),
- exists is_conj step_nums)
- end
- val proofextract = get_proof_extract proof
+ val last_axiom = Vector.length thm_names
+ fun is_axiom n = n <= last_axiom
+ fun is_conj n = n >= fst conj_count andalso n < fst conj_count + snd conj_count
+ fun getname i = Vector.sub(thm_names, i-1)
in
- get_axiom_names thm_names (get_step_nums proofextract)
- end;
+ (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
+ (map getname (filter is_axiom step_nums))),
+ exists is_conj step_nums)
+ end
+ val proofextract = get_proof_extract proof
+ in
+ get_axiom_names thm_names (get_step_nums proofextract)
+ end;
- (*Used to label theorems chained into the sledgehammer call*)
- val chained_hint = "CHAINED";
- val nochained = filter_out (fn y => y = chained_hint)
-
- (* metis-command *)
- fun metis_line [] = "apply metis"
- | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
+(*Used to label theorems chained into the sledgehammer call*)
+val chained_hint = "CHAINED";
+val nochained = filter_out (fn y => y = chained_hint)
+
+(* metis-command *)
+fun metis_line [] = "apply metis"
+ | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
- (* atp_minimize [atp=<prover>] <lemmas> *)
- fun minimize_line _ [] = ""
- | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^
- (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^
- space_implode " " (nochained lemmas))
+(* atp_minimize [atp=<prover>] <lemmas> *)
+fun minimize_line _ [] = ""
+ | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^
+ (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^
+ space_implode " " (nochained lemmas))
- fun sendback_metis_nochained lemmas =
- (Markup.markup Markup.sendback o metis_line) (nochained lemmas)
+fun sendback_metis_nochained lemmas =
+ (Markup.markup Markup.sendback o metis_line) (nochained lemmas)
- fun lemma_list dfg name result =
- let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
- in (sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^
- (if used_conj then ""
- else "\nWarning: Goal is provable because context is inconsistent."),
- nochained lemmas)
- end;
+fun lemma_list dfg name result =
+ let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
+ in (sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^
+ (if used_conj then ""
+ else "\nWarning: Goal is provable because context is inconsistent."),
+ nochained lemmas)
+ end;
- (* === Extracting structured Isar-proof === *)
- fun structured_proof name (result as (proof, thm_names, conj_count, ctxt, goal, subgoalno)) =
- let
- (*Could use split_lines, but it can return blank lines...*)
- val lines = String.tokens (equal #"\n");
- val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c)
- val proofextract = get_proof_extract proof
- val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
- val (one_line_proof, lemma_names) = lemma_list false name result
- val structured = if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
- else decode_tstp_file cnfs ctxt goal subgoalno thm_names
- in
- (one_line_proof ^ "\n\n" ^ (Markup.markup Markup.sendback) structured, lemma_names)
- end
+(* === Extracting structured Isar-proof === *)
+fun structured_proof name (result as (proof, thm_names, conj_count, ctxt, goal, subgoalno)) =
+ let
+ (*Could use split_lines, but it can return blank lines...*)
+ val lines = String.tokens (equal #"\n");
+ val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c)
+ val proofextract = get_proof_extract proof
+ val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
+ val (one_line_proof, lemma_names) = lemma_list false name result
+ val structured =
+ if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
+ else decode_tstp_file cnfs ctxt goal subgoalno thm_names
+ in
+ (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback structured, lemma_names)
+end
end;
--- a/src/HOL/Tools/sat_solver.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/sat_solver.ML Thu Oct 29 18:17:26 2009 +0100
@@ -272,7 +272,7 @@
else
parse_lines lines
in
- (parse_lines o (List.filter (fn l => l <> "")) o split_lines o File.read) path
+ (parse_lines o filter (fn l => l <> "") o split_lines o File.read) path
end;
(* ------------------------------------------------------------------------- *)
@@ -352,7 +352,7 @@
o (map int_from_string)
o (maps (String.fields (fn c => c mem [#" ", #"\t", #"\n"])))
o filter_preamble
- o (List.filter (fn l => l <> ""))
+ o filter (fn l => l <> "")
o split_lines
o File.read)
path
--- a/src/HOL/Tools/typecopy.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/typecopy.ML Thu Oct 29 18:17:26 2009 +0100
@@ -44,8 +44,8 @@
(* interpretation of type copies *)
-structure TypecopyInterpretation = InterpretationFun(type T = string val eq = op =);
-val interpretation = TypecopyInterpretation.interpretation;
+structure Typecopy_Interpretation = Interpretation(type T = string val eq = op =);
+val interpretation = Typecopy_Interpretation.interpretation;
(* introducing typecopies *)
@@ -76,7 +76,7 @@
in
thy
|> (TypecopyData.map o Symtab.update_new) (tyco, info)
- |> TypecopyInterpretation.data tyco
+ |> Typecopy_Interpretation.data tyco
|> pair (tyco, info)
end
in
@@ -126,7 +126,7 @@
end;
val setup =
- TypecopyInterpretation.init
+ Typecopy_Interpretation.init
#> interpretation add_default_code
end;
--- a/src/HOL/Tools/typedef.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOL/Tools/typedef.ML Thu Oct 29 18:17:26 2009 +0100
@@ -53,8 +53,8 @@
fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
-structure TypedefInterpretation = InterpretationFun(type T = string val eq = op =);
-val interpretation = TypedefInterpretation.interpretation;
+structure Typedef_Interpretation = Interpretation(type T = string val eq = op =);
+val interpretation = Typedef_Interpretation.interpretation;
fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy =
let
@@ -169,7 +169,7 @@
in
thy2
|> put_info full_tname info
- |> TypedefInterpretation.data full_tname
+ |> Typedef_Interpretation.data full_tname
|> pair (full_tname, info)
end);
@@ -264,6 +264,6 @@
end;
-val setup = TypedefInterpretation.init;
+val setup = Typedef_Interpretation.init;
end;
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Thu Oct 29 18:17:26 2009 +0100
@@ -184,7 +184,7 @@
fun one_con (con,args) = let
val nonrec_args = filter_out is_rec args;
- val rec_args = List.filter is_rec args;
+ val rec_args = filter is_rec args;
val recs_cnt = length rec_args;
val allargs = nonrec_args @ rec_args
@ map (upd_vname (fn s=> s^"'")) rec_args;
--- a/src/HOLCF/Tools/Domain/domain_library.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Thu Oct 29 18:17:26 2009 +0100
@@ -241,8 +241,8 @@
val upd_vname = upd_third;
fun is_rec arg = rec_of arg >=0;
fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
-fun nonlazy args = map vname (filter_out is_lazy args);
-fun nonlazy_rec args = map vname (List.filter is_nonlazy_rec args);
+fun nonlazy args = map vname (filter_out is_lazy args);
+fun nonlazy_rec args = map vname (filter is_nonlazy_rec args);
(* ----- combinators for making dtyps ----- *)
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Oct 29 18:17:26 2009 +0100
@@ -446,7 +446,7 @@
val nlas = nonlazy args;
val vns = map vname args;
val vnn = List.nth (vns, n);
- val nlas' = List.filter (fn v => v <> vnn) nlas;
+ val nlas' = filter (fn v => v <> vnn) nlas;
val lhs = (%%:sel)`(con_app con args);
val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn));
fun tacs1 ctxt =
@@ -555,7 +555,7 @@
val sargs = case largs of [_] => [] | _ => nonlazy args;
val prop = lift_defined %: (sargs, mk_trp (prem === concl));
in pg con_appls prop end;
- val cons' = List.filter (fn (_,args) => args<>[]) cons;
+ val cons' = filter (fn (_,args) => args<>[]) cons;
in
val _ = trace " Proving inverts...";
val inverts =
@@ -593,7 +593,7 @@
else (%# arg);
val rhs = con_app2 con one_rhs args;
val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
- val args' = List.filter (fn a => not (is_rec a orelse is_lazy a)) args;
+ val args' = filter_out (fn a => is_rec a orelse is_lazy a) args;
val stricts = abs_strict :: rep_strict :: @{thms domain_fun_stricts};
fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args';
val rules = [ax_abs_iso] @ @{thms domain_fun_simps};
@@ -616,7 +616,7 @@
fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args;
in
val _ = trace " Proving copy_stricts...";
- val copy_stricts = map one_strict (List.filter has_nonlazy_rec cons);
+ val copy_stricts = map one_strict (filter has_nonlazy_rec cons);
end;
val copy_rews = copy_strict :: copy_apps @ copy_stricts;
@@ -722,7 +722,7 @@
in Library.foldr mk_all (map vname args, lhs === rhs) end;
fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons;
val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs));
- val simps = List.filter (has_fewer_prems 1) copy_rews;
+ val simps = filter (has_fewer_prems 1) copy_rews;
fun con_tac ctxt (con, args) =
if nonlazy_rec args = []
then all_tac
@@ -747,7 +747,7 @@
let
fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
- val t2 = lift ind_hyp (List.filter is_rec args, t1);
+ val t2 = lift ind_hyp (filter is_rec args, t1);
val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2);
in Library.foldr mk_All (map vname args, t3) end;
@@ -767,7 +767,7 @@
maps (fn (_,args) =>
resolve_tac prems 1 ::
map (K(atac 1)) (nonlazy args) @
- map (K(atac 1)) (List.filter is_rec args))
+ map (K(atac 1)) (filter is_rec args))
cons))
conss);
local
@@ -812,10 +812,10 @@
(List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
fun con_tacs (con, args) =
asm_simp_tac take_ss 1 ::
- map arg_tac (List.filter is_nonlazy_rec args) @
+ map arg_tac (filter is_nonlazy_rec args) @
[resolve_tac prems 1] @
- map (K (atac 1)) (nonlazy args) @
- map (K (etac spec 1)) (List.filter is_rec args);
+ map (K (atac 1)) (nonlazy args) @
+ map (K (etac spec 1)) (filter is_rec args);
fun cases_tacs (cons, cases) =
res_inst_tac context [(("x", 0), "x")] cases 1 ::
asm_simp_tac (take_ss addsimps prems) 1 ::
--- a/src/Provers/Arith/fast_lin_arith.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Thu Oct 29 18:17:26 2009 +0100
@@ -340,7 +340,7 @@
case ty of Eq => k <> 0 | Le => k > 0 | Lt => k >= 0;
fun calc_blowup l =
- let val (p,n) = List.partition (curry (op <) 0) (List.filter (curry (op <>) 0) l)
+ let val (p,n) = List.partition (curry (op <) 0) (filter (curry (op <>) 0) l)
in length p * length n end;
(* ------------------------------------------------------------------------- *)
--- a/src/Provers/classical.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Provers/classical.ML Thu Oct 29 18:17:26 2009 +0100
@@ -670,7 +670,7 @@
(*version of bimatch_from_nets_tac that only applies rules that
create precisely n subgoals.*)
fun n_bimatch_from_nets_tac n =
- biresolution_from_nets_tac (order_list o List.filter (nsubgoalsP n)) true;
+ biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true;
fun eq_contr_tac i = ematch_tac [not_elim] i THEN eq_assume_tac i;
val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
--- a/src/Provers/splitter.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Provers/splitter.ML Thu Oct 29 18:17:26 2009 +0100
@@ -192,7 +192,7 @@
if n > length ts then []
else let val lev = length apsns
val lbnos = fold add_lbnos (Library.take (n, ts)) []
- val flbnos = List.filter (fn i => i < lev) lbnos
+ val flbnos = filter (fn i => i < lev) lbnos
val tt = incr_boundvars (~lev) t
in if null flbnos then
if T = T' then [(thm,[],pos,TB,tt)] else []
--- a/src/Pure/Isar/code.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Pure/Isar/code.ML Thu Oct 29 18:17:26 2009 +0100
@@ -639,7 +639,8 @@
(* datatypes *)
-structure Type_Interpretation = InterpretationFun(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
+structure Type_Interpretation =
+ Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
fun add_datatype raw_cs thy =
let
--- a/src/Pure/Isar/expression.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Pure/Isar/expression.ML Thu Oct 29 18:17:26 2009 +0100
@@ -641,8 +641,8 @@
|> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
|> Sign.declare_const ((bname, predT), NoSyn) |> snd
|> PureThy.add_defs false
- [((Binding.conceal (Binding.map_name Thm.def_name bname), Logic.mk_equals (head, body)),
- [Thm.kind_internal])];
+ [((Binding.conceal (Binding.map_name Thm.def_name bname),
+ Logic.mk_equals (head, body)), [])];
val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
val cert = Thm.cterm_of defs_thy;
--- a/src/Pure/Isar/rule_cases.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Pure/Isar/rule_cases.ML Thu Oct 29 18:17:26 2009 +0100
@@ -37,6 +37,8 @@
val name: string list -> thm -> thm
val case_names: string list -> attribute
val case_conclusion: string * string list -> attribute
+ val is_inner_rule: thm -> bool
+ val inner_rule: attribute
val save: thm -> thm -> thm
val get: thm -> (string * string list) list * int
val rename_params: string list list -> thm -> thm
@@ -90,7 +92,7 @@
fun extract_case is_open thy (case_outline, raw_prop) name concls =
let
- val rename = if is_open then I else (apfst (Name.internal o Name.clean));
+ val rename = if is_open then I else apfst (Name.internal o Name.clean);
val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
val len = length props;
@@ -212,7 +214,7 @@
val consumes_tagN = "consumes";
fun lookup_consumes th =
- (case AList.lookup (op =) (Thm.get_tags th) (consumes_tagN) of
+ (case AList.lookup (op =) (Thm.get_tags th) consumes_tagN of
NONE => NONE
| SOME s =>
(case Lexicon.read_nat s of SOME n => SOME n
@@ -223,14 +225,13 @@
fun put_consumes NONE th = th
| put_consumes (SOME n) th = th
|> Thm.untag_rule consumes_tagN
- |> Thm.tag_rule
- (consumes_tagN, Library.string_of_int (if n < 0 then Thm.nprems_of th + n else n));
+ |> Thm.tag_rule (consumes_tagN, string_of_int (if n < 0 then Thm.nprems_of th + n else n));
fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th;
val save_consumes = put_consumes o lookup_consumes;
-fun consumes n x = Thm.rule_attribute (K (put_consumes (SOME n))) x;
+fun consumes n = Thm.rule_attribute (K (put_consumes (SOME n)));
fun consumes_default n x =
if is_some (lookup_consumes (#2 x)) then x else consumes n x;
@@ -282,7 +283,24 @@
else NONE)
in fold add_case_concl concls end;
-fun case_conclusion concl = Thm.rule_attribute (fn _ => add_case_concl concl);
+fun case_conclusion concl = Thm.rule_attribute (K (add_case_concl concl));
+
+
+
+(** inner rule **)
+
+val inner_rule_tagN = "inner_rule";
+
+fun is_inner_rule th =
+ AList.defined (op =) (Thm.get_tags th) inner_rule_tagN;
+
+fun put_inner_rule inner =
+ Thm.untag_rule inner_rule_tagN
+ #> inner ? Thm.tag_rule (inner_rule_tagN, "");
+
+val save_inner_rule = put_inner_rule o is_inner_rule;
+
+val inner_rule = Thm.rule_attribute (K (put_inner_rule true));
@@ -290,7 +308,11 @@
(* access hints *)
-fun save th = save_consumes th #> save_case_names th #> save_case_concls th;
+fun save th =
+ save_consumes th #>
+ save_case_names th #>
+ save_case_concls th #>
+ save_inner_rule th;
fun get th =
let
@@ -357,5 +379,5 @@
end;
-structure BasicRuleCases: BASIC_RULE_CASES = RuleCases;
-open BasicRuleCases;
+structure Basic_Rule_Cases: BASIC_RULE_CASES = RuleCases;
+open Basic_Rule_Cases;
--- a/src/Pure/Isar/rule_insts.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML Thu Oct 29 18:17:26 2009 +0100
@@ -268,7 +268,7 @@
(* Separate type and term insts *)
fun has_type_var ((x, _), _) =
(case Symbol.explode x of "'" :: _ => true | _ => false);
- val Tinsts = List.filter has_type_var insts;
+ val Tinsts = filter has_type_var insts;
val tinsts = filter_out has_type_var insts;
(* Tactic *)
--- a/src/Pure/Proof/extraction.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Pure/Proof/extraction.ML Thu Oct 29 18:17:26 2009 +0100
@@ -651,7 +651,7 @@
val nt = Envir.beta_norm t;
val args = filter_out (fn v => member (op =) rtypes
(tname_of (body_type (fastype_of v)))) (vfs_of prop);
- val args' = List.filter (fn v => Logic.occs (v, nt)) args;
+ val args' = filter (fn v => Logic.occs (v, nt)) args;
val t' = mkabs nt args';
val T = fastype_of t';
val cname = extr_name s vs';
--- a/src/Pure/Syntax/parser.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Pure/Syntax/parser.ML Thu Oct 29 18:17:26 2009 +0100
@@ -615,11 +615,11 @@
(*Get all rhss with precedence >= minPrec*)
-fun getRHS minPrec = List.filter (fn (_, _, prec:int) => prec >= minPrec);
+fun getRHS minPrec = filter (fn (_, _, prec:int) => prec >= minPrec);
(*Get all rhss with precedence >= minPrec and < maxPrec*)
fun getRHS' minPrec maxPrec =
- List.filter (fn (_, _, prec:int) => prec >= minPrec andalso prec < maxPrec);
+ filter (fn (_, _, prec:int) => prec >= minPrec andalso prec < maxPrec);
(*Make states using a list of rhss*)
fun mkStates i minPrec lhsID rhss =
@@ -655,19 +655,19 @@
in update (used, []) end;
fun getS A maxPrec Si =
- List.filter
+ filter
(fn (_, _, _, Nonterminal (B, prec) :: _, _, _)
=> A = B andalso prec <= maxPrec
| _ => false) Si;
fun getS' A maxPrec minPrec Si =
- List.filter
+ filter
(fn (_, _, _, Nonterminal (B, prec) :: _, _, _)
=> A = B andalso prec > minPrec andalso prec <= maxPrec
| _ => false) Si;
fun getStates Estate i ii A maxPrec =
- List.filter
+ filter
(fn (_, _, _, Nonterminal (B, prec) :: _, _, _)
=> A = B andalso prec <= maxPrec
| _ => false)
--- a/src/Pure/Syntax/syn_ext.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Pure/Syntax/syn_ext.ML Thu Oct 29 18:17:26 2009 +0100
@@ -218,7 +218,7 @@
val read_symbs = map_filter I o the o Scan.read Symbol.stopper scan_symbs;
fun unique_index xsymbs =
- if length (List.filter is_index xsymbs) <= 1 then xsymbs
+ if length (filter is_index xsymbs) <= 1 then xsymbs
else error "Duplicate index arguments (\\<index>)";
in
@@ -226,7 +226,7 @@
val read_mfix = unique_index o read_symbs o Symbol.explode;
fun mfix_delims sy = fold_rev (fn Delim s => cons s | _ => I) (read_mfix sy) [];
-val mfix_args = length o List.filter is_argument o read_mfix;
+val mfix_args = length o filter is_argument o read_mfix;
val escape_mfix = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
@@ -276,7 +276,7 @@
val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix;
- val args = List.filter (fn Argument _ => true | _ => false) raw_symbs;
+ val args = filter (fn Argument _ => true | _ => false) raw_symbs;
val (const', typ', parse_rules) =
if not (exists is_index args) then (const, typ, [])
else
@@ -312,7 +312,7 @@
val xprod' =
if Lexicon.is_terminal lhs' then err_in_mfix ("Illegal lhs: " ^ lhs') mfix
else if const <> "" then xprod
- else if length (List.filter is_argument symbs') <> 1 then
+ else if length (filter is_argument symbs') <> 1 then
err_in_mfix "Copy production must have exactly one argument" mfix
else if exists is_terminal symbs' then xprod
else XProd (lhs', map rem_pri symbs', "", chain_pri);
--- a/src/Pure/Tools/find_consts.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Pure/Tools/find_consts.ML Thu Oct 29 18:17:26 2009 +0100
@@ -11,11 +11,10 @@
Strict of string
| Loose of string
| Name of string
-
val find_consts : Proof.context -> (bool * criterion) list -> unit
end;
-structure FindConsts : FIND_CONSTS =
+structure Find_Consts : FIND_CONSTS =
struct
(* search criteria *)
@@ -162,7 +161,7 @@
val _ =
OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag
- (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
+ (Scan.repeat ((Scan.option P.minus >> is_none) -- criterion)
>> (Toplevel.no_timing oo find_consts_cmd));
end;
--- a/src/Pure/Tools/find_theorems.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML Thu Oct 29 18:17:26 2009 +0100
@@ -18,7 +18,7 @@
(bool * string criterion) list -> unit
end;
-structure FindTheorems: FIND_THEOREMS =
+structure Find_Theorems: FIND_THEOREMS =
struct
(** search criteria **)
@@ -28,24 +28,22 @@
Pattern of 'term;
fun apply_dummies tm =
- strip_abs tm
- |> fst
- |> map (Term.dummy_pattern o snd)
- |> betapplys o pair tm
- |> (fn x => Term.replace_dummy_patterns x 1)
- |> fst;
+ let
+ val (xs, _) = Term.strip_abs tm;
+ val tm' = Term.betapplys (tm, map (Term.dummy_pattern o #2) xs);
+ in #1 (Term.replace_dummy_patterns tm' 1) end;
fun parse_pattern ctxt nm =
let
- val nm' = case Syntax.parse_term ctxt nm of Const (n, _) => n | _ => nm;
val consts = ProofContext.consts_of ctxt;
+ val nm' =
+ (case Syntax.parse_term ctxt nm of
+ Const (c, _) => c
+ | _ => Consts.intern consts nm);
in
- nm'
- |> Consts.intern consts
- |> Consts.the_abbreviation consts
- |> snd
- |> apply_dummies
- handle TYPE _ => ProofContext.read_term_pattern ctxt nm
+ (case try (Consts.the_abbreviation consts) nm' of
+ SOME (_, rhs) => apply_dummies rhs
+ | NONE => ProofContext.read_term_pattern ctxt nm)
end;
fun read_criterion _ (Name name) = Name name
--- a/src/Pure/Tools/named_thms.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Pure/Tools/named_thms.ML Thu Oct 29 18:17:26 2009 +0100
@@ -1,7 +1,8 @@
(* Title: Pure/Tools/named_thms.ML
Author: Makarius
-Named collections of theorems in canonical order.
+Named collections of theorems in canonical order. Based on naive data
+structures -- not scalable!
*)
signature NAMED_THMS =
--- a/src/Pure/axclass.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Pure/axclass.ML Thu Oct 29 18:17:26 2009 +0100
@@ -311,7 +311,7 @@
(Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
#>> Thm.varifyT
#-> (fn thm => add_inst_param (c, tyco) (c'', thm)
- #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [Thm.kind_internal])
+ #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
#> snd
#> Sign.restore_naming thy
#> pair (Const (c, T))))
--- a/src/Pure/codegen.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Pure/codegen.ML Thu Oct 29 18:17:26 2009 +0100
@@ -137,7 +137,7 @@
| args_of (Ignore :: ms) (_ :: xs) = args_of ms xs
| args_of (_ :: ms) xs = args_of ms xs;
-fun num_args_of x = length (List.filter is_arg x);
+fun num_args_of x = length (filter is_arg x);
(**** theory data ****)
--- a/src/Pure/interpretation.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Pure/interpretation.ML Thu Oct 29 18:17:26 2009 +0100
@@ -13,7 +13,7 @@
val init: theory -> theory
end;
-functor InterpretationFun(type T val eq: T * T -> bool): INTERPRETATION =
+functor Interpretation(type T val eq: T * T -> bool): INTERPRETATION =
struct
type T = T;
--- a/src/Pure/more_thm.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Pure/more_thm.ML Thu Oct 29 18:17:26 2009 +0100
@@ -91,13 +91,9 @@
val lemmaK: string
val corollaryK: string
val internalK: string
- val has_kind: thm -> bool
val get_kind: thm -> string
val kind_rule: string -> thm -> thm
val kind: string -> attribute
- val kind_internal: attribute
- val has_internal: Properties.property list -> bool
- val is_internal: thm -> bool
end;
structure Thm: THM =
@@ -425,16 +421,10 @@
val corollaryK = "corollary";
val internalK = Markup.internalK;
-fun the_kind thm = the (Properties.get (Thm.get_tags thm) Markup.kindN);
-
-val has_kind = can the_kind;
-val get_kind = the_default "" o try the_kind;
+fun get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);
fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN;
fun kind k x = if k = "" then x else rule_attribute (K (kind_rule k)) x;
-fun kind_internal x = kind internalK x;
-fun has_internal tags = exists (fn tg => tg = (Markup.kindN, internalK)) tags;
-val is_internal = has_internal o Thm.get_tags;
open Thm;
--- a/src/Pure/proofterm.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Pure/proofterm.ML Thu Oct 29 18:17:26 2009 +0100
@@ -1024,7 +1024,7 @@
(** see pattern.ML **)
-fun flt (i: int) = List.filter (fn n => n < i);
+fun flt (i: int) = filter (fn n => n < i);
fun fomatch Ts tymatch j =
let
--- a/src/Pure/unify.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Pure/unify.ML Thu Oct 29 18:17:26 2009 +0100
@@ -473,7 +473,7 @@
if i<lev then Bound i
else if member (op =) banned (i-lev)
then raise CHANGE_FAIL (**flexible occurrence: give up**)
- else Bound (i - length (List.filter (fn j => j < i-lev) banned))
+ else Bound (i - length (filter (fn j => j < i-lev) banned))
| change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
| change lev (t$u) = change lev t $ change lev u
| change lev t = t
--- a/src/Tools/IsaPlanner/rw_inst.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Tools/IsaPlanner/rw_inst.ML Thu Oct 29 18:17:26 2009 +0100
@@ -169,7 +169,7 @@
OldTerm.add_term_tfrees (t,tfrees)))
([],[]) ts;
val unfixed_tvars =
- List.filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
+ filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars
in (fixtyinsts, tfrees) end;
--- a/src/Tools/auto_solve.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Tools/auto_solve.ML Thu Oct 29 18:17:26 2009 +0100
@@ -5,7 +5,7 @@
existing theorem. Duplicate lemmas can be detected in this way.
The implementation is based in part on Berghofer and Haftmann's
-quickcheck.ML. It relies critically on the FindTheorems solves
+quickcheck.ML. It relies critically on the Find_Theorems solves
feature.
*)
@@ -45,8 +45,8 @@
let
val ctxt = Proof.context_of state;
- val crits = [(true, FindTheorems.Solves)];
- fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
+ val crits = [(true, Find_Theorems.Solves)];
+ fun find g = snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
fun prt_result (goal, results) =
let
@@ -57,7 +57,7 @@
in
Pretty.big_list
(msg ^ " could be solved directly with:")
- (map (FindTheorems.pretty_thm ctxt) results)
+ (map (Find_Theorems.pretty_thm ctxt) results)
end;
fun seek_against_goal () =
--- a/src/Tools/induct.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/Tools/induct.ML Thu Oct 29 18:17:26 2009 +0100
@@ -570,7 +570,7 @@
((fn [] => NONE | ts => List.last ts) #>
(fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
find_inductT ctxt)) [[]]
- |> filter_out (forall Thm.is_internal);
+ |> filter_out (forall RuleCases.is_inner_rule);
fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
| get_inductP _ _ = [];
--- a/src/ZF/arith_data.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/ZF/arith_data.ML Thu Oct 29 18:17:26 2009 +0100
@@ -68,7 +68,7 @@
fun prove_conv name tacs ctxt prems (t,u) =
if t aconv u then NONE
else
- let val prems' = List.filter (not o is_eq_thm) prems
+ let val prems' = filter_out is_eq_thm prems
val goal = Logic.list_implies (map (#prop o Thm.rep_thm) prems',
FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs)))
--- a/src/ZF/ind_syntax.ML Thu Oct 29 14:06:49 2009 +0100
+++ b/src/ZF/ind_syntax.ML Thu Oct 29 18:17:26 2009 +0100
@@ -96,8 +96,8 @@
fun union_params (rec_tm, cs) =
let val (_,args) = strip_comb rec_tm
fun is_ind arg = (type_of arg = iT)
- in case List.filter is_ind (args @ cs) of
- [] => @{const 0}
+ in case filter is_ind (args @ cs) of
+ [] => @{const 0}
| u_args => Balanced_Tree.make mk_Un u_args
end;