# HG changeset patch # User Cezary Kaliszyk # Date 1314366784 -32400 # Node ID f7259c9064ea546215dfd3ef1eb43d88ea042921 # Parent 5e0f9e0e32fbc7afdbbbc137cafeb8876a058320# Parent 9ec0dcd351a442f9135e55c0fc8369c1c1aa1631 merge diff -r 5e0f9e0e32fb -r f7259c9064ea src/HOL/List.thy --- a/src/HOL/List.thy Fri Aug 26 09:31:56 2011 +0900 +++ b/src/HOL/List.thy Fri Aug 26 22:53:04 2011 +0900 @@ -4703,7 +4703,7 @@ qed -text{* Accessible part of @{term listrel1} relations: *} +text{* Accessible part and wellfoundedness: *} lemma Cons_acc_listrel1I [intro!]: "x \ acc r \ xs \ acc (listrel1 r) \ (x # xs) \ acc (listrel1 r)" @@ -4729,6 +4729,9 @@ apply (fastsimp dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def) done +lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r" +by(metis wf_acc_iff in_lists_conv_set lists_accI lists_accD Cons_in_lists_iff) + subsubsection {* Lifting Relations to Lists: all elements *} diff -r 5e0f9e0e32fb -r f7259c9064ea src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Fri Aug 26 09:31:56 2011 +0900 +++ b/src/HOL/Tools/ATP/atp_problem.ML Fri Aug 26 22:53:04 2011 +0900 @@ -19,12 +19,13 @@ datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type + datatype tff_flavor = Implicit | Explicit datatype thf_flavor = Without_Choice | With_Choice datatype format = CNF | CNF_UEQ | FOF | - TFF | + TFF of tff_flavor | THF of thf_flavor datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture @@ -118,12 +119,14 @@ datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type +datatype tff_flavor = Implicit | Explicit datatype thf_flavor = Without_Choice | With_Choice + datatype format = CNF | CNF_UEQ | FOF | - TFF | + TFF of tff_flavor | THF of thf_flavor datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture @@ -199,10 +202,10 @@ fun formula_fold pos f = let - fun aux pos (AQuant (_, _, phi)) = aux pos phi - | aux pos (AConn conn) = aconn_fold pos aux conn - | aux pos (AAtom tm) = f pos tm - in aux pos end + fun fld pos (AQuant (_, _, phi)) = fld pos phi + | fld pos (AConn conn) = aconn_fold pos fld conn + | fld pos (AAtom tm) = f pos tm + in fld pos end fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi) | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis) @@ -210,7 +213,7 @@ fun is_format_thf (THF _) = true | is_format_thf _ = false -fun is_format_typed TFF = true +fun is_format_typed (TFF _) = true | is_format_typed (THF _) = true | is_format_typed _ = false @@ -232,7 +235,7 @@ aux false ty1 ^ " " ^ tptp_fun_type ^ " " ^ aux true ty2 |> not rhs ? enclose "(" ")" in aux true ty end - | string_for_type TFF ty = + | string_for_type (TFF _) ty = (case strip_tff_type ty of ([], s) => s | ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s @@ -320,7 +323,7 @@ fun string_for_format CNF = tptp_cnf | string_for_format CNF_UEQ = tptp_cnf | string_for_format FOF = tptp_fof - | string_for_format TFF = tptp_tff + | string_for_format (TFF _) = tptp_tff | string_for_format (THF _) = tptp_thf fun string_for_problem_line format (Decl (ident, sym, ty)) = diff -r 5e0f9e0e32fb -r f7259c9064ea src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Aug 26 09:31:56 2011 +0900 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Aug 26 22:53:04 2011 +0900 @@ -304,8 +304,10 @@ (* Vampire *) +(* Vampire 1.8 has TFF support, but it's buggy and therefore disabled on + SystemOnTPTP. *) fun is_old_vampire_version () = - string_ord (getenv "VAMPIRE_VERSION", "1.8") = LESS + string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER val vampire_config : atp_config = {exec = ("VAMPIRE_HOME", "vampire"), @@ -335,12 +337,12 @@ (* FUDGE *) (if is_old_vampire_version () then [(0.333, (false, (150, FOF, "poly_guards", sosN))), - (0.334, (true, (50, FOF, "mono_guards?", no_sosN))), - (0.333, (false, (500, FOF, "mono_tags?", sosN)))] + (0.333, (false, (500, FOF, "mono_tags?", sosN))), + (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))] else - [(0.333, (false, (150, TFF, "poly_guards", sosN))), - (0.334, (true, (50, TFF, "simple", no_sosN))), - (0.333, (false, (500, TFF, "simple", sosN)))]) + [(0.333, (false, (150, TFF Implicit, "poly_guards", sosN))), + (0.333, (false, (500, TFF Implicit, "simple", sosN))), + (0.334, (true, (50, TFF Implicit, "simple", no_sosN)))]) |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -368,8 +370,8 @@ (* FUDGE *) K [(0.5, (false, (250, FOF, "mono_guards?", ""))), (0.25, (false, (125, FOF, "mono_guards?", ""))), - (0.125, (false, (62, TFF, "simple", ""))), - (0.125, (false, (31, TFF, "simple", "")))]} + (0.125, (false, (62, TFF Implicit, "simple", ""))), + (0.125, (false, (31, TFF Implicit, "simple", "")))]} val z3_tptp = (z3_tptpN, z3_tptp_config) @@ -457,19 +459,21 @@ remotify_atp satallax "Satallax" ["2.1", "2.0", "2"] (K (100, THF With_Choice, "simple_higher") (* FUDGE *)) val remote_vampire = - remotify_atp vampire "Vampire" ["1.8"] (K (250, TFF, "simple") (* FUDGE *)) + remotify_atp vampire "Vampire" ["1.8"] + (K (250, TFF Implicit, "simple") (* FUDGE *)) val remote_z3_tptp = - remotify_atp z3_tptp "Z3" ["3.0"] (K (250, TFF, "simple") (* FUDGE *)) + remotify_atp z3_tptp "Z3" ["3.0"] + (K (250, TFF Implicit, "simple") (* FUDGE *)) val remote_e_sine = remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *)) val remote_snark = remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"] [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis - (K (100, TFF, "simple") (* FUDGE *)) + (K (100, TFF Explicit, "simple") (* FUDGE *)) val remote_e_tofof = remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) - Axiom Hypothesis (K (150, TFF, "simple") (* FUDGE *)) + Axiom Hypothesis (K (150, TFF Explicit, "simple") (* FUDGE *)) val remote_waldmeister = remote_atp waldmeisterN "Waldmeister" ["710"] [("#START OF PROOF", "Proved Goals:")] diff -r 5e0f9e0e32fb -r f7259c9064ea src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Fri Aug 26 09:31:56 2011 +0900 +++ b/src/HOL/Tools/ATP/atp_translate.ML Fri Aug 26 22:53:04 2011 +0900 @@ -621,7 +621,7 @@ | is_type_level_monotonicity_based _ = false fun adjust_type_enc (THF _) type_enc = type_enc - | adjust_type_enc TFF (Simple_Types (_, level)) = + | adjust_type_enc (TFF _) (Simple_Types (_, level)) = Simple_Types (First_Order, level) | adjust_type_enc format (Simple_Types (_, level)) = adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform)) @@ -1020,7 +1020,7 @@ fun preprocess_abstractions_in_terms trans_lambdas facts = let val (facts, lambda_ts) = - facts |> map (snd o snd) |> trans_lambdas + facts |> map (snd o snd) |> trans_lambdas |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts val lambda_facts = map2 (fn t => fn j => @@ -1095,12 +1095,9 @@ val known_infinite_types = [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}] -fun is_type_surely_infinite' ctxt soundness cached_Ts T = - (* Unlike virtually any other polymorphic fact whose type variables can be - instantiated by a known infinite type, extensionality actually encodes a - cardinality constraints. *) +fun is_type_kind_of_surely_infinite ctxt soundness cached_Ts T = soundness <> Sound andalso - is_type_surely_infinite ctxt (soundness = Unsound) cached_Ts T + is_type_surely_infinite ctxt (soundness <> Unsound) cached_Ts T (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are dangerous because their "exhaust" properties can easily lead to unsound ATP @@ -1114,7 +1111,7 @@ exists (type_intersect ctxt T) maybe_nonmono_Ts andalso not (exists (type_instance ctxt T) surely_infinite_Ts orelse (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso - is_type_surely_infinite' ctxt soundness surely_infinite_Ts T)) + is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts T)) | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts, maybe_nonmono_Ts, ...} Fin_Nonmono_Types T = @@ -1249,14 +1246,15 @@ end in add true end fun add_fact_syms_to_table ctxt explicit_apply = - formula_fold NONE (K (add_iterm_syms_to_table ctxt explicit_apply)) - |> fact_lift + K (add_iterm_syms_to_table ctxt explicit_apply) + |> formula_fold NONE |> fact_lift val tvar_a = TVar (("'a", 0), HOLogic.typeS) val default_sym_tab_entries : (string * sym_info) list = (prefixed_predicator_name, - {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) :: + {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) + (* FIXME: needed? *) :: (make_fixed_const NONE @{const_name undefined}, {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) :: ([tptp_false, tptp_true] @@ -1674,8 +1672,7 @@ else if should_generate_tag_bound_decl ctxt mono type_enc universal T then let val var = ATerm (name, []) - val tagged_var = - ATerm (type_tag, [ho_term_from_typ format type_enc T, var]) + val tagged_var = var |> tag_with_type ctxt format mono type_enc pos T in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end else NONE @@ -1792,7 +1789,7 @@ #> fold (add_iterm_syms in_conj) args end fun add_fact_syms in_conj = - fact_lift (formula_fold NONE (K (add_iterm_syms in_conj))) + K (add_iterm_syms in_conj) |> formula_fold NONE |> fact_lift fun add_formula_var_types (AQuant (_, xs, phi)) = fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs #> add_formula_var_types phi @@ -1844,8 +1841,8 @@ if exists (type_instance ctxt T) surely_infinite_Ts orelse member (type_aconv ctxt) maybe_finite_Ts T then mono - else if is_type_surely_infinite' ctxt soundness surely_infinite_Ts - T then + else if is_type_kind_of_surely_infinite ctxt soundness + surely_infinite_Ts T then {maybe_finite_Ts = maybe_finite_Ts, surely_finite_Ts = surely_finite_Ts, maybe_infinite_Ts = maybe_infinite_Ts, @@ -1888,6 +1885,22 @@ ? fold (add_fact_mononotonicity_info ctxt level) facts end +fun add_iformula_monotonic_types ctxt mono type_enc = + let + val level = level_of_type_enc type_enc + val should_encode = should_encode_type ctxt mono level + fun add_type T = not (should_encode T) ? insert_type ctxt I T + fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2 + | add_args _ = I + and add_term tm = add_type (ityp_of tm) #> add_args tm + in formula_fold NONE (K add_term) end +fun add_fact_monotonic_types ctxt mono type_enc = + add_iformula_monotonic_types ctxt mono type_enc |> fact_lift +fun monotonic_types_for_facts ctxt mono type_enc facts = + [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso + is_type_level_monotonicity_based (level_of_type_enc type_enc)) + ? fold (add_fact_monotonic_types ctxt mono type_enc) facts + fun formula_line_for_guards_mono_type ctxt format mono type_enc T = Formula (guards_sym_formula_prefix ^ ascii_of (mangled_type format type_enc T), @@ -2049,17 +2062,9 @@ end) fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc - sym_decl_tab = + mono_Ts sym_decl_tab = let val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst - val mono_Ts = - if polymorphism_of_type_enc type_enc = Polymorphic then - syms |> maps (map result_type_of_decl o snd) - |> filter_out (should_encode_type ctxt mono - (level_of_type_enc type_enc)) - |> rpair [] |-> fold (insert_type ctxt I) - else - [] val mono_lines = problem_lines_for_mono_types ctxt format mono type_enc mono_Ts val decl_lines = @@ -2134,11 +2139,14 @@ val helpers = repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc |> map repair + val mono_Ts = + helpers @ conjs @ facts + |> monotonic_types_for_facts ctxt mono type_enc val sym_decl_lines = (conjs, helpers @ facts) |> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono - type_enc + type_enc mono_Ts val helper_lines = 0 upto length helpers - 1 ~~ helpers |> map (formula_line_for_fact ctxt format helper_prefix I false true mono @@ -2168,7 +2176,7 @@ CNF => ensure_cnf_problem | CNF_UEQ => filter_cnf_ueq_problem | _ => I) - |> (if is_format_typed format then + |> (if is_format_typed format andalso format <> TFF Implicit then declare_undeclared_syms_in_atp_problem type_decl_prefix implicit_declsN else diff -r 5e0f9e0e32fb -r f7259c9064ea src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Fri Aug 26 09:31:56 2011 +0900 +++ b/src/HOL/Tools/ATP/atp_util.ML Fri Aug 26 22:53:04 2011 +0900 @@ -161,16 +161,14 @@ 0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means cardinality 2 or more. The specified default cardinality is returned if the cardinality of the type can't be determined. *) -fun tiny_card_of_type ctxt inst_tvars assigns default_card T = +fun tiny_card_of_type ctxt sound assigns default_card T = let val thy = Proof_Context.theory_of ctxt val max = 2 (* 1 would be too small for the "fun" case *) - val type_cmp = - if inst_tvars then uncurry (type_generalization ctxt) else type_aconv ctxt fun aux slack avoid T = if member (op =) avoid T then 0 - else case AList.lookup type_cmp assigns T of + else case AList.lookup (type_aconv ctxt) assigns T of SOME k => k | NONE => case T of @@ -218,13 +216,14 @@ (* Very slightly unsound: Type variables are assumed not to be constrained to cardinality 1. (In practice, the user would most likely have used "unit" directly anyway.) *) - | TFree _ => if default_card = 1 then 2 else default_card + | TFree _ => + if not sound andalso default_card = 1 then 2 else default_card | TVar _ => default_card in Int.min (max, aux false [] T) end -fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt false [] 0 T <> 0 -fun is_type_surely_infinite ctxt inst_tvars infinite_Ts T = - tiny_card_of_type ctxt inst_tvars (map (rpair 0) infinite_Ts) 1 T = 0 +fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt true [] 0 T <> 0 +fun is_type_surely_infinite ctxt sound infinite_Ts T = + tiny_card_of_type ctxt sound (map (rpair 0) infinite_Ts) 1 T = 0 (* Simple simplifications to ensure that sort annotations don't leave a trail of spurious "True"s. *) diff -r 5e0f9e0e32fb -r f7259c9064ea src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Aug 26 09:31:56 2011 +0900 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Aug 26 22:53:04 2011 +0900 @@ -536,6 +536,11 @@ #> Config.put Monomorph.max_new_instances max_new_instances #> Config.put Monomorph.keep_partial_instances false +fun suffix_for_mode Auto_Try = "_auto_try" + | suffix_for_mode Try = "_try" + | suffix_for_mode Normal = "" + | suffix_for_mode Minimize = "_min" + (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on Linux appears to be the only ATP that does not honor its time limit. *) val atp_timeout_slack = seconds 1.0 @@ -557,7 +562,7 @@ else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix) val problem_file_name = Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ - "_" ^ string_of_int subgoal) + suffix_for_mode mode ^ "_" ^ string_of_int subgoal) val problem_path_name = if dest_dir = "" then File.tmp_path problem_file_name