# HG changeset patch # User wenzelm # Date 1256836646 -3600 # Node ID 78faaec3209f60affd866e218a8f2b980b9fa5af # Parent 9b5286c0fb14fee7491f755e2f29aaf4c9474d8e# Parent b4534348b8fd3176d92cf087c18b4ca54704cc27 merged diff -r 9b5286c0fb14 -r 78faaec3209f src/CCL/Wfd.thy --- 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 diff -r 9b5286c0fb14 -r 78faaec3209f src/FOLP/simp.ML --- 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; diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/ATP_Linkup.thy --- 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 diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Auth/KerberosIV.thy --- 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: "\ \ expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \ \ \ 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*} diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/HOL.thy --- 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 *} diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Import/import_syntax.ML --- 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 diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Import/shuffler.ML --- 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 = diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/IsaMakefile --- 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 \ diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.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) diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Nominal/nominal_datatype.ML --- 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); diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Nominal/nominal_primrec.ML --- 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 diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/ATP_Manager/atp_manager.ML --- 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); diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/ATP_Manager/atp_minimal.ML --- 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 diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- 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 diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/Datatype/datatype.ML --- 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 *) diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- 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 diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/Datatype/datatype_aux.ML --- 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 *) diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/Datatype/datatype_codegen.ML --- 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'; diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/Datatype/datatype_prop.ML --- 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'); diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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) diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/TFL/post.ML --- 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 diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/TFL/rules.ML --- 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; diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/TFL/tfl.ML --- 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; diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/choice_specification.ML --- 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") diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/inductive.ML --- 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 diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/inductive_codegen.ML --- 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 " ^ diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/lin_arith.ML --- 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 diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/meson.ML --- 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 *****) diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/metis_tools.ML --- 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; diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/old_primrec.ML --- 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 diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/primrec.ML --- 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 diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/refute.ML --- 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) => diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/res_atp.ML --- 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)) diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/res_axioms.ML --- 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) => diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/res_blacklist.ML --- /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; diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/res_clause.ML --- 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_"; diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/res_hol_clause.ML --- 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; + diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/res_reconstruct.ML --- 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=] *) - 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=] *) +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; diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/sat_solver.ML --- 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 diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/typecopy.ML --- 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; diff -r 9b5286c0fb14 -r 78faaec3209f src/HOL/Tools/typedef.ML --- 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; diff -r 9b5286c0fb14 -r 78faaec3209f src/HOLCF/Tools/Domain/domain_axioms.ML --- 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; diff -r 9b5286c0fb14 -r 78faaec3209f src/HOLCF/Tools/Domain/domain_library.ML --- 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 ----- *) diff -r 9b5286c0fb14 -r 78faaec3209f src/HOLCF/Tools/Domain/domain_theorems.ML --- 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 :: diff -r 9b5286c0fb14 -r 78faaec3209f src/Provers/Arith/fast_lin_arith.ML --- 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; (* ------------------------------------------------------------------------- *) diff -r 9b5286c0fb14 -r 78faaec3209f src/Provers/classical.ML --- 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; diff -r 9b5286c0fb14 -r 78faaec3209f src/Provers/splitter.ML --- 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 [] diff -r 9b5286c0fb14 -r 78faaec3209f src/Pure/Isar/code.ML --- 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 diff -r 9b5286c0fb14 -r 78faaec3209f src/Pure/Isar/expression.ML --- 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; diff -r 9b5286c0fb14 -r 78faaec3209f src/Pure/Isar/rule_cases.ML --- 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; diff -r 9b5286c0fb14 -r 78faaec3209f src/Pure/Isar/rule_insts.ML --- 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 *) diff -r 9b5286c0fb14 -r 78faaec3209f src/Pure/Proof/extraction.ML --- 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'; diff -r 9b5286c0fb14 -r 78faaec3209f src/Pure/Syntax/parser.ML --- 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) diff -r 9b5286c0fb14 -r 78faaec3209f src/Pure/Syntax/syn_ext.ML --- 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 (\\)"; 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); diff -r 9b5286c0fb14 -r 78faaec3209f src/Pure/Tools/find_consts.ML --- 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; diff -r 9b5286c0fb14 -r 78faaec3209f src/Pure/Tools/find_theorems.ML --- 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 diff -r 9b5286c0fb14 -r 78faaec3209f src/Pure/Tools/named_thms.ML --- 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 = diff -r 9b5286c0fb14 -r 78faaec3209f src/Pure/axclass.ML --- 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)))) diff -r 9b5286c0fb14 -r 78faaec3209f src/Pure/codegen.ML --- 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 ****) diff -r 9b5286c0fb14 -r 78faaec3209f src/Pure/interpretation.ML --- 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; diff -r 9b5286c0fb14 -r 78faaec3209f src/Pure/more_thm.ML --- 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; diff -r 9b5286c0fb14 -r 78faaec3209f src/Pure/proofterm.ML --- 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 diff -r 9b5286c0fb14 -r 78faaec3209f src/Pure/unify.ML --- 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 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 diff -r 9b5286c0fb14 -r 78faaec3209f src/Tools/IsaPlanner/rw_inst.ML --- 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; diff -r 9b5286c0fb14 -r 78faaec3209f src/Tools/auto_solve.ML --- 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 () = diff -r 9b5286c0fb14 -r 78faaec3209f src/Tools/induct.ML --- 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 _ _ = []; diff -r 9b5286c0fb14 -r 78faaec3209f src/ZF/arith_data.ML --- 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))) diff -r 9b5286c0fb14 -r 78faaec3209f src/ZF/ind_syntax.ML --- 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;