# HG changeset patch # User blanchet # Date 1343050350 -7200 # Node ID 3e45c98fe127464cee94bdcc4cfd7d983450c713 # Parent 82b9feeab1efff7113cc12348f91b60b54f06486 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh diff -r 82b9feeab1ef -r 3e45c98fe127 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Mon Jul 23 15:32:30 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Mon Jul 23 15:32:30 2012 +0200 @@ -113,10 +113,6 @@ handle TYPE _ => @{prop True} end -fun all_non_tautological_facts_of thy css_table = - Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table - |> filter_out (Sledgehammer_Fact.is_likely_tautology_or_too_meta o snd) - fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name = let val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt @@ -126,7 +122,8 @@ val mono = not (is_type_enc_polymorphic type_enc) val path = file_name |> Path.explode val _ = File.write path "" - val facts = all_non_tautological_facts_of thy css_table + val facts = + Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table val atp_problem = facts |> map (fn ((_, loc), th) => diff -r 82b9feeab1ef -r 3e45c98fe127 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Mon Jul 23 15:32:30 2012 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Mon Jul 23 15:32:30 2012 +0200 @@ -26,9 +26,7 @@ val max_facts_slack = 2 -val all_names = - filter_out is_likely_tautology_or_too_meta - #> map (rpair () o nickname_of) #> Symtab.make +val all_names = map (rpair () o nickname_of) #> Symtab.make fun evaluate_mash_suggestions ctxt params thy file_name = let diff -r 82b9feeab1ef -r 3e45c98fe127 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Mon Jul 23 15:32:30 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Mon Jul 23 15:32:30 2012 +0200 @@ -49,9 +49,7 @@ val thy_name_of_fact = hd o Long_Name.explode fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact -val all_names = - filter_out is_likely_tautology_or_too_meta - #> map (rpair () o nickname_of) #> Symtab.make +val all_names = map (rpair () o nickname_of) #> Symtab.make fun generate_accessibility thy include_thy file_name = let diff -r 82b9feeab1ef -r 3e45c98fe127 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Mon Jul 23 15:32:30 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Mon Jul 23 15:32:30 2012 +0200 @@ -88,11 +88,13 @@ val isabelle_info : string -> int -> (string, 'a) ho_term list val extract_isabelle_status : (string, 'a) ho_term list -> string option val extract_isabelle_rank : (string, 'a) ho_term list -> int + val inductionN : string val introN : string val inductiveN : string val elimN : string val simpN : string - val defN : string + val non_rec_defN : string + val rec_defN : string val rankN : string val minimum_rank : int val default_rank : int @@ -222,11 +224,14 @@ val isabelle_info_prefix = "isabelle_" +val inductionN = "induction" val introN = "intro" val inductiveN = "inductive" val elimN = "elim" val simpN = "simp" -val defN = "def" +val non_rec_defN = "non_rec_def" +val rec_defN = "rec_def" + val rankN = "rank" val minimum_rank = 0 @@ -503,9 +508,13 @@ fun suffix_tag top_level s = if top_level then case extract_isabelle_status info of - SOME s' => if s' = defN then s ^ ":lt" - else if s' = simpN andalso gen_simp then s ^ ":lr" - else s + SOME s' => + if s' = non_rec_defN then + s ^ ":lt" + else if (s' = simpN orelse s' = rec_defN) andalso gen_simp then + s ^ ":lr" + else + s | NONE => s else s diff -r 82b9feeab1ef -r 3e45c98fe127 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jul 23 15:32:30 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jul 23 15:32:30 2012 +0200 @@ -18,7 +18,9 @@ datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter datatype scope = Global | Local | Assum | Chained - datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def + datatype status = + General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | + Rec_Def type stature = scope * status datatype strictness = Strict | Non_Strict @@ -103,6 +105,7 @@ val helper_table : ((string * bool) * (status * thm) list) list val trans_lams_from_string : Proof.context -> type_enc -> string -> term list -> term list * term list + val string_of_status : status -> string val factsN : string val prepare_atp_problem : Proof.context -> atp_format -> formula_role -> type_enc -> mode -> string @@ -123,7 +126,8 @@ datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter datatype scope = Global | Local | Assum | Chained -datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def +datatype status = + General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def type stature = scope * status datatype order = @@ -1236,7 +1240,8 @@ |>> map2 (fn (name, (role, _)) => fn t => (name, (role, t))) facts val lam_facts = map2 (fn t => fn j => - ((lam_fact_prefix ^ Int.toString j, (Global, Def)), (Axiom, t))) + ((lam_fact_prefix ^ Int.toString j, + (Global, Non_Rec_Def)), (Axiom, t))) lambda_ts (1 upto length lambda_ts) in (facts, lam_facts) end @@ -1293,7 +1298,7 @@ ((name, stature as (_, status)), t) = let val role = - if is_format_with_defs format andalso status = Def andalso + if is_format_with_defs format andalso status = Non_Rec_Def andalso is_legitimate_tptp_def t then Definition else @@ -1664,18 +1669,18 @@ (* The Boolean indicates that a fairly sound type encoding is needed. *) val base_helper_table = - [(("COMBI", false), [(Def, @{thm Meson.COMBI_def})]), - (("COMBK", false), [(Def, @{thm Meson.COMBK_def})]), - (("COMBB", false), [(Def, @{thm Meson.COMBB_def})]), - (("COMBC", false), [(Def, @{thm Meson.COMBC_def})]), - (("COMBS", false), [(Def, @{thm Meson.COMBS_def})]), + [(("COMBI", false), [(Non_Rec_Def, @{thm Meson.COMBI_def})]), + (("COMBK", false), [(Non_Rec_Def, @{thm Meson.COMBK_def})]), + (("COMBB", false), [(Non_Rec_Def, @{thm Meson.COMBB_def})]), + (("COMBC", false), [(Non_Rec_Def, @{thm Meson.COMBC_def})]), + (("COMBS", false), [(Non_Rec_Def, @{thm Meson.COMBS_def})]), ((predicator_name, false), [(General, not_ffalse), (General, ftrue)]), (("fFalse", false), [(General, not_ffalse)]), (("fFalse", true), [(General, @{thm True_or_False})]), (("fTrue", false), [(General, ftrue)]), (("fTrue", true), [(General, @{thm True_or_False})]), (("If", true), - [(Def, @{thm if_True}), (Def, @{thm if_False}), + [(Non_Rec_Def, @{thm if_True}), (Non_Rec_Def, @{thm if_False}), (General, @{thm True_or_False})])] val helper_table = @@ -1683,7 +1688,7 @@ [(("fNot", false), @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1] fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]} - |> map (pair Def)), + |> map (pair Non_Rec_Def)), (("fconj", false), @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q" by (unfold fconj_def) fast+} @@ -1718,19 +1723,19 @@ ((app_op_name, true), [(General, @{lemma "EX x. ~ f x = g x | f = g" by blast})]), (("fconj", false), - @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Def)), + @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)), (("fdisj", false), - @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Def)), + @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)), (("fimplies", false), @{thms fimplies_table fconj_laws fdisj_laws fimplies_laws} - |> map (pair Def)), + |> map (pair Non_Rec_Def)), (("fequal", false), - (@{thms fequal_table} |> map (pair Def)) @ + (@{thms fequal_table} |> map (pair Non_Rec_Def)) @ (@{thms fequal_laws} |> map (pair General))), (("fAll", false), - @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Def)), + @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def)), (("fEx", false), - @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))] + @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def))] |> map (apsnd (map (apsnd zero_var_indexes))) fun bound_tvars type_enc sorts Ts = @@ -2104,28 +2109,29 @@ | do_formula pos (AAtom tm) = AAtom (do_term pos tm) in do_formula end +fun string_of_status General = "" + | string_of_status Induction = inductionN + | string_of_status Intro = introN + | string_of_status Inductive = inductiveN + | string_of_status Elim = elimN + | string_of_status Simp = simpN + | string_of_status Non_Rec_Def = non_rec_defN + | string_of_status Rec_Def = rec_defN + (* Each fact is given a unique fact number to avoid name clashes (e.g., because of monomorphization). The TPTP explicitly forbids name clashes, and some of the remote provers might care. *) fun line_for_fact ctxt prefix encode freshen pos mono type_enc rank - (j, {name, stature, role, iformula, atomic_types}) = - (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, role, - iformula - |> formula_from_iformula ctxt mono type_enc should_guard_var_in_formula - (if pos then SOME true else NONE) - |> close_formula_universally - |> bound_tvars type_enc true atomic_types, - NONE, - let val rank = rank j in - case snd stature of - Intro => isabelle_info introN rank - | Inductive => isabelle_info inductiveN rank - | Elim => isabelle_info elimN rank - | Simp => isabelle_info simpN rank - | Def => isabelle_info defN rank - | _ => isabelle_info "" rank - end) - |> Formula + (j, {name, stature = (_, status), role, iformula, atomic_types}) = + Formula (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ + encode name, + role, + iformula + |> formula_from_iformula ctxt mono type_enc + should_guard_var_in_formula (if pos then SOME true else NONE) + |> close_formula_universally + |> bound_tvars type_enc true atomic_types, + NONE, isabelle_info (string_of_status status) (rank j)) fun lines_for_subclass type_enc sub super = Formula (subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, Axiom, @@ -2355,7 +2361,7 @@ Axiom, eq_formula type_enc (atomic_types_of T) [] false (tag_with_type ctxt mono type_enc NONE T x_var) x_var, - NONE, isabelle_info defN helper_rank) + NONE, isabelle_info non_rec_defN helper_rank) end fun lines_for_mono_types ctxt mono type_enc Ts = @@ -2438,7 +2444,7 @@ val tag_with = tag_with_type ctxt mono type_enc NONE fun formula c = [Formula (ident, role, eq (tag_with res_T c) c, NONE, isabelle_info - defN helper_rank)] + non_rec_defN helper_rank)] in if pred_sym orelse not (should_encode_type ctxt mono level res_T) then [] @@ -2538,7 +2544,7 @@ in ([tm1, tm2], [Formula (uncurried_alias_eq_prefix ^ s2, role, eq |> maybe_negate, - NONE, isabelle_info defN helper_rank)]) + NONE, isabelle_info non_rec_defN helper_rank)]) |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I else pair_append (do_alias (ary - 1))) end @@ -2878,8 +2884,9 @@ fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis) val graph = Graph.empty - |> fold (fold (add_eq_deps (has_status defN)) o snd) problem - |> fold (fold (add_eq_deps (has_status simpN orf is_conj)) o snd) problem + |> fold (fold (add_eq_deps (has_status non_rec_defN)) o snd) problem + |> fold (fold (add_eq_deps (has_status rec_defN orf has_status simpN + orf is_conj)) o snd) problem |> fold (fold (add_intro_deps (has_status inductiveN)) o snd) problem |> fold (fold (add_intro_deps (has_status introN)) o snd) problem fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1 diff -r 82b9feeab1ef -r 3e45c98fe127 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jul 23 15:32:30 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jul 23 15:32:30 2012 +0200 @@ -200,10 +200,11 @@ else isa_ext -fun add_all_defs fact_names accum = +fun add_non_rec_defs fact_names accum = Vector.foldl (fn (facts, facts') => - union (op =) (filter (fn (_, (_, status)) => status = Def) facts) + union (op =) + (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts) facts') accum fact_names @@ -214,12 +215,12 @@ (* LEO 1.3.3 does not record definitions properly, leading to missing dependencies in the TSTP proof. Remove the next line once this is fixed. *) - add_all_defs fact_names + add_non_rec_defs fact_names else if rule = satallax_unsat_coreN then (fn [] => (* Satallax doesn't include definitions in its unsatisfiable cores, so we assume the worst and include them all here. *) - [(ext_name ctxt, (Global, General))] |> add_all_defs fact_names + [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names | facts => facts) else I) diff -r 82b9feeab1ef -r 3e45c98fe127 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Jul 23 15:32:30 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Jul 23 15:32:30 2012 +0200 @@ -23,7 +23,6 @@ val fact_from_ref : Proof.context -> unit Symtab.table -> thm list -> status Termtab.table -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list - val is_likely_tautology_or_too_meta : thm -> bool val backquote_thm : thm -> string val clasimpset_rule_table_of : Proof.context -> status Termtab.table val maybe_instantiate_inducts : @@ -50,7 +49,8 @@ del : (Facts.ref * Attrib.src list) list, only : bool} -val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator +val sledgehammer_prefixes = + ["ATP", "Meson", "Metis", "Sledgehammer"] |> map (suffix Long_Name.separator) (* experimental features *) val ignore_no_atp = @@ -182,9 +182,9 @@ apply_depth t > max_apply_depth orelse (not ho_atp andalso formula_has_too_many_lambdas [] t) -(* FIXME: Extend to "Meson" and "Metis" *) val exists_sledgehammer_const = - exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) + exists_Const (fn (s, _) => + exists (fn pref => String.isPrefix pref s) sledgehammer_prefixes) (* FIXME: make more reliable *) val exists_low_level_class_const = @@ -192,25 +192,11 @@ s = @{const_name equal_class.equal} orelse String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s) -fun is_metastrange_theorem th = - case head_of (concl_of th) of - Const (s, _) => (s <> @{const_name Trueprop} andalso - s <> @{const_name "=="}) - | _ => false - fun is_that_fact th = String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th) andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN | _ => false) (prop_of th) -fun is_theorem_bad_for_atps ho_atp thm = - is_metastrange_theorem thm orelse - let val t = prop_of thm in - is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse - exists_sledgehammer_const t orelse exists_low_level_class_const t orelse - is_that_fact thm - end - fun is_likely_tautology_or_too_meta th = let val is_boring_const = member (op =) atp_widely_irrelevant_consts @@ -229,6 +215,15 @@ is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th)) end +fun is_theorem_bad_for_atps ho_atp th = + is_likely_tautology_or_too_meta th orelse + let val t = prop_of th in + is_formula_too_complex ho_atp t orelse + exists_type type_has_top_sort t orelse + exists_sledgehammer_const t orelse exists_low_level_class_const t orelse + is_that_fact th + end + fun hackish_string_for_term thy t = Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) (Syntax.string_of_term_global thy) t @@ -299,8 +294,8 @@ |> maps (snd o snd) in Termtab.empty |> add Simp [atomize] snd simps - |> add Simp [] I rec_defs - |> add Def [] I nonrec_defs + |> add Rec_Def [] I rec_defs + |> add Non_Rec_Def [] I nonrec_defs (* Add once it is used: |> add Elim [] I elims *) @@ -458,7 +453,6 @@ else let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in all_facts ctxt ho_atp reserved add chained css - |> filter_out (is_likely_tautology_or_too_meta o snd) |> filter_out (member Thm.eq_thm_prop del o snd) |> maybe_filter_no_atps ctxt |> uniquify diff -r 82b9feeab1ef -r 3e45c98fe127 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jul 23 15:32:30 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jul 23 15:32:30 2012 +0200 @@ -312,22 +312,32 @@ |> forall is_lambda_free ts ? cons "no_lams" |> forall (not o exists_Const is_exists) ts ? cons "no_skos" |> scope <> Global ? cons "local" - |> (case status of - General => I - | Induction => cons "induction" - | Intro => cons "intro" - | Inductive => cons "inductive" - | Elim => cons "elim" - | Simp => cons "simp" - | Def => cons "def") + |> (case string_of_status status of "" => I | s => cons s) (* Too many dependencies is a sign that a decision procedure is at work. There isn't much too learn from such proofs. *) -val max_dependencies = 10 +val max_dependencies = 15 val atp_dependency_default_max_fact = 50 +(* "type_definition_xxx" facts are characterized by their use of "CollectI". *) +val typedef_sig = [@{thm CollectI} |> nickname_of] + +(* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *) +val typedef_ths = + @{thms type_definition.Abs_inverse type_definition.Rep_inverse + type_definition.Rep type_definition.Rep_inject + type_definition.Abs_inject type_definition.Rep_cases + type_definition.Abs_cases type_definition.Rep_induct + type_definition.Abs_induct type_definition.Rep_range + type_definition.Abs_image} + |> map nickname_of + fun trim_dependencies deps = - if length deps <= max_dependencies then SOME deps else NONE + if length deps > max_dependencies orelse deps = typedef_sig orelse + exists (member (op =) typedef_ths) deps then + NONE + else + SOME deps fun isar_dependencies_of all_names = thms_in_proof (SOME all_names) #> trim_dependencies @@ -708,10 +718,7 @@ else let val all_names = - facts |> map snd - |> filter_out is_likely_tautology_or_too_meta - |> map (rpair () o nickname_of) - |> Symtab.make + facts |> map snd |> map (rpair () o nickname_of) |> Symtab.make val deps_of = if atp then atp_dependencies_of ctxt params prover auto_level facts all_names