# HG changeset patch # User blanchet # Date 1314018165 -7200 # Node ID cd1e32b8d4c4754bfdb7fa196a0df503ebe0f078 # Parent d21f7e330ec8673eb9ebabf18b9b9eb593d08f66 added caching for (in)finiteness checks diff -r d21f7e330ec8 -r cd1e32b8d4c4 src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Aug 22 15:02:45 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Aug 22 15:02:45 2011 +0200 @@ -165,6 +165,12 @@ exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name | _ => false) +(* (quasi-)underapproximation of the truth *) +fun is_locality_global Local = false + | is_locality_global Assum = false + | is_locality_global Chained = false + | is_locality_global _ = true + fun used_facts_in_unsound_atp_proof _ _ _ _ [] = NONE | used_facts_in_unsound_atp_proof ctxt conjecture_shape facts_offset fact_names atp_proof = diff -r d21f7e330ec8 -r cd1e32b8d4c4 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Mon Aug 22 15:02:45 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Aug 22 15:02:45 2011 +0200 @@ -85,7 +85,6 @@ val new_skolem_var_name_from_const : string -> string val atp_irrelevant_consts : string list val atp_schematic_consts_of : term -> typ list Symtab.table - val is_locality_global : locality -> bool val type_enc_from_string : soundness -> string -> type_enc val is_type_enc_higher_order : type_enc -> bool val polymorphism_of_type_enc : type_enc -> polymorphism @@ -521,12 +520,6 @@ General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum | Chained -(* (quasi-)underapproximation of the truth *) -fun is_locality_global Local = false - | is_locality_global Assum = false - | is_locality_global Chained = false - | is_locality_global _ = true - datatype order = First_Order | Higher_Order datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound @@ -673,12 +666,10 @@ fun fact_lift f ({iformula, ...} : translated_formula) = f iformula -val type_instance = Sign.typ_instance o Proof_Context.theory_of - fun insert_type ctxt get_T x xs = let val T = get_T x in - if exists (curry (type_instance ctxt) T o get_T) xs then xs - else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs + if exists (type_instance ctxt T o get_T) xs then xs + else x :: filter_out (type_generalization ctxt T o get_T) xs end (* The Booleans indicate whether all type arguments should be kept. *) @@ -1081,41 +1072,52 @@ (** Finite and infinite type inference **) +type monotonicity_info = + {maybe_finite_Ts : typ list, + surely_finite_Ts : typ list, + maybe_infinite_Ts : typ list, + surely_infinite_Ts : typ list, + maybe_nonmono_Ts : typ list} + (* These types witness that the type classes they belong to allow infinite models and hence that any types with these type classes is monotonic. *) val known_infinite_types = [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}] -fun is_type_infinite ctxt soundness locality T = +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. *) soundness <> Sound andalso - is_type_surely_infinite ctxt - (if soundness = Unsound andalso locality <> Extensionality then - known_infinite_types - else - []) 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 proofs. On the other hand, all HOL infinite types can be given the same models in first-order logic (via Löwenheim-Skolem). *) -fun should_encode_type _ _ All_Types _ = true - | should_encode_type ctxt nonmono_Ts (Noninf_Nonmono_Types soundness) T = - exists (curry (type_instance ctxt) T) nonmono_Ts andalso - not (is_type_infinite ctxt soundness General T) - | should_encode_type ctxt nonmono_Ts Fin_Nonmono_Types T = - exists (curry (type_instance ctxt) T) nonmono_Ts andalso - is_type_surely_finite ctxt T +fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true + | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts, + maybe_nonmono_Ts, ...} + (Noninf_Nonmono_Types soundness) T = + exists (type_instance 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)) + | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts, + maybe_nonmono_Ts, ...} + Fin_Nonmono_Types T = + exists (type_instance ctxt T) maybe_nonmono_Ts andalso + (exists (type_instance ctxt T) surely_finite_Ts orelse + (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso + is_type_surely_finite ctxt T)) | should_encode_type _ _ _ _ = false -fun should_predicate_on_type ctxt nonmono_Ts - (Guards (_, level, heaviness)) should_predicate_on_var T = - (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso - should_encode_type ctxt nonmono_Ts level T - | should_predicate_on_type _ _ _ _ _ = false +fun should_guard_type ctxt mono (Guards (_, level, heaviness)) should_guard_var + T = + (heaviness = Heavyweight orelse should_guard_var ()) andalso + should_encode_type ctxt mono level T + | should_guard_type _ _ _ _ _ = false fun is_var_or_bound_var (IConst ((s, _), _, _)) = String.isPrefix bound_var_prefix s @@ -1128,19 +1130,18 @@ Elsewhere fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false - | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site - u T = + | should_tag_with_type ctxt mono (Tags (_, level, heaviness)) site u T = (case heaviness of - Heavyweight => should_encode_type ctxt nonmono_Ts level T + Heavyweight => should_encode_type ctxt mono level T | Lightweight => case (site, is_var_or_bound_var u) of - (Eq_Arg _, true) => should_encode_type ctxt nonmono_Ts level T + (Eq_Arg _, true) => should_encode_type ctxt mono level T | _ => false) | should_tag_with_type _ _ _ _ _ _ = false -fun homogenized_type ctxt nonmono_Ts level = +fun homogenized_type ctxt mono level = let - val should_encode = should_encode_type ctxt nonmono_Ts level + val should_encode = should_encode_type ctxt mono level fun homo 0 T = if should_encode T then T else homo_infinite_type | homo ary (Type (@{type_name fun}, [T1, T2])) = homo 0 T1 --> homo (ary - 1) T2 @@ -1157,8 +1158,8 @@ fun consider_var_arity const_T var_T max_ary = let fun iter ary T = - if ary = max_ary orelse type_instance ctxt (var_T, T) orelse - type_instance ctxt (T, var_T) then + if ary = max_ary orelse type_instance ctxt var_T T orelse + type_instance ctxt T var_T then ary else iter (ary + 1) (range_type T) @@ -1574,20 +1575,20 @@ | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum = accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, []))) | is_var_positively_naked_in_term _ _ _ _ = true -fun should_predicate_on_var_in_formula pos phi (SOME true) name = +fun should_guard_var_in_formula pos phi (SOME true) name = formula_fold pos (is_var_positively_naked_in_term name) phi false - | should_predicate_on_var_in_formula _ _ _ _ = true + | should_guard_var_in_formula _ _ _ _ = true fun mk_aterm format type_enc name T_args args = ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args) -fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm = +fun tag_with_type ctxt format mono type_enc pos T tm = IConst (type_tag, T --> T, [T]) |> enforce_type_arg_policy_in_iterm ctxt format type_enc - |> ho_term_from_iterm ctxt format nonmono_Ts type_enc (Top_Level pos) + |> ho_term_from_iterm ctxt format mono type_enc (Top_Level pos) |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]) | _ => raise Fail "unexpected lambda-abstraction") -and ho_term_from_iterm ctxt format nonmono_Ts type_enc = +and ho_term_from_iterm ctxt format mono type_enc = let fun aux site u = let @@ -1613,25 +1614,24 @@ | IApp _ => raise Fail "impossible \"IApp\"" val T = ityp_of u in - t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then - tag_with_type ctxt format nonmono_Ts type_enc pos T + t |> (if should_tag_with_type ctxt mono type_enc site u T then + tag_with_type ctxt format mono type_enc pos T else I) end in aux end -and formula_from_iformula ctxt format nonmono_Ts type_enc - should_predicate_on_var = +and formula_from_iformula ctxt format mono type_enc should_guard_var = let - val do_term = ho_term_from_iterm ctxt format nonmono_Ts type_enc o Top_Level + val do_term = ho_term_from_iterm ctxt format mono type_enc o Top_Level val do_bound_type = case type_enc of Simple_Types (_, level) => - homogenized_type ctxt nonmono_Ts level 0 + homogenized_type ctxt mono level 0 #> ho_type_from_typ format type_enc false 0 #> SOME | _ => K NONE fun do_out_of_bound_type pos phi universal (name, T) = - if should_predicate_on_type ctxt nonmono_Ts type_enc - (fn () => should_predicate_on_var pos phi universal name) T then + if should_guard_type ctxt mono type_enc + (fn () => should_guard_var pos phi universal name) T then IVar (name, T) |> type_guard_iterm ctxt format type_enc T |> do_term pos |> AAtom |> SOME @@ -1663,13 +1663,13 @@ (* 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 formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts - type_enc (j, {name, locality, kind, iformula, atomic_types}) = +fun formula_line_for_fact ctxt format prefix encode freshen pos mono type_enc + (j, {name, locality, kind, iformula, atomic_types}) = (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind, iformula |> close_iformula_universally - |> formula_from_iformula ctxt format nonmono_Ts type_enc - should_predicate_on_var_in_formula + |> formula_from_iformula ctxt format mono type_enc + should_guard_var_in_formula (if pos then SOME true else NONE) |> bound_tvars type_enc atomic_types |> close_formula_universally, @@ -1704,11 +1704,11 @@ (fo_literal_from_arity_literal concl_lits)) |> close_formula_universally, isabelle_info introN, NONE) -fun formula_line_for_conjecture ctxt format nonmono_Ts type_enc +fun formula_line_for_conjecture ctxt format mono type_enc ({name, kind, iformula, atomic_types, ...} : translated_formula) = Formula (conjecture_prefix ^ name, kind, - formula_from_iformula ctxt format nonmono_Ts type_enc - should_predicate_on_var_in_formula (SOME false) + formula_from_iformula ctxt format mono type_enc + should_guard_var_in_formula (SOME false) (close_iformula_universally iformula) |> bound_tvars type_enc atomic_types |> close_formula_universally, NONE, NONE) @@ -1785,48 +1785,80 @@ | _ => fold add_undefined_const (var_types ()))) end +(* We add "bool" in case the helper "True_or_False" is included later. *) +val default_mono = + {maybe_finite_Ts = [@{typ bool}], + surely_finite_Ts = [@{typ bool}], + maybe_infinite_Ts = known_infinite_types, + surely_infinite_Ts = known_infinite_types, + maybe_nonmono_Ts = [@{typ bool}]} + (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it out with monotonicity" paper presented at CADE 2011. *) -fun add_iterm_nonmonotonic_types _ _ _ (SOME false) _ = I - | add_iterm_nonmonotonic_types ctxt level locality _ - (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) = - (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso - (case level of +fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono + | add_iterm_mononotonicity_info ctxt level _ + (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) + (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts, + surely_infinite_Ts, maybe_nonmono_Ts}) = + if is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] then + case level of Noninf_Nonmono_Types soundness => - (* The second conjunct about globality is not strictly necessary, but it - helps prevent finding proofs that are only sound "modulo - infiniteness". For example, if the conjecture is - "EX x y::nat. x ~= y", its untyped negation "ALL x y. x = y" would - lead to a nonsensical proof that we can't replay. *) - not (is_type_infinite ctxt soundness locality T - (* andalso is_locality_global locality *)) - | Fin_Nonmono_Types => is_type_surely_finite ctxt T - | _ => true)) ? insert_type ctxt I T - | add_iterm_nonmonotonic_types _ _ _ _ _ = I -fun add_fact_nonmonotonic_types ctxt level - ({kind, locality, iformula, ...} : translated_formula) = + 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 + {maybe_finite_Ts = maybe_finite_Ts, + surely_finite_Ts = surely_finite_Ts, + maybe_infinite_Ts = maybe_infinite_Ts, + surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T, + maybe_nonmono_Ts = maybe_nonmono_Ts} + else + {maybe_finite_Ts = maybe_finite_Ts |> insert (type_aconv ctxt) T, + surely_finite_Ts = surely_finite_Ts, + maybe_infinite_Ts = maybe_infinite_Ts, + surely_infinite_Ts = surely_infinite_Ts, + maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T} + | Fin_Nonmono_Types => + if exists (type_instance ctxt T) surely_finite_Ts orelse + member (type_aconv ctxt) maybe_infinite_Ts T then + mono + else if is_type_surely_finite ctxt T then + {maybe_finite_Ts = maybe_finite_Ts, + surely_finite_Ts = surely_finite_Ts |> insert_type ctxt I T, + maybe_infinite_Ts = maybe_infinite_Ts, + surely_infinite_Ts = surely_infinite_Ts, + maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T} + else + {maybe_finite_Ts = maybe_finite_Ts, + surely_finite_Ts = surely_finite_Ts, + maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_aconv ctxt) T, + surely_infinite_Ts = surely_infinite_Ts, + maybe_nonmono_Ts = maybe_nonmono_Ts} + | _ => mono + else + mono + | add_iterm_mononotonicity_info _ _ _ _ mono = mono +fun add_fact_mononotonicity_info ctxt level + ({kind, iformula, ...} : translated_formula) = formula_fold (SOME (kind <> Conjecture)) - (add_iterm_nonmonotonic_types ctxt level locality) iformula -fun nonmonotonic_types_for_facts ctxt type_enc facts = + (add_iterm_mononotonicity_info ctxt level) iformula +fun mononotonicity_info_for_facts ctxt type_enc facts = let val level = level_of_type_enc type_enc in - if is_type_level_monotonicity_based level then - [] |> fold (add_fact_nonmonotonic_types ctxt level) facts - (* We must add "bool" in case the helper "True_or_False" is added - later. *) - |> insert_type ctxt I @{typ bool} - else - [] + default_mono + |> is_type_level_monotonicity_based level + ? fold (add_fact_mononotonicity_info ctxt level) facts end (* FIXME: do the right thing for existentials! *) -fun formula_line_for_guards_mono_type ctxt format nonmono_Ts type_enc T = +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), Axiom, IConst (`make_bound_var "X", T, []) |> type_guard_iterm ctxt format type_enc T |> AAtom - |> formula_from_iformula ctxt format nonmono_Ts type_enc + |> formula_from_iformula ctxt format mono type_enc (K (K (K (K true)))) (SOME true) |> bound_tvars type_enc (atyps_of T) |> close_formula_universally, @@ -1838,27 +1870,25 @@ |> bound_tvars type_enc atomic_Ts |> close_formula_universally -fun formula_line_for_tags_mono_type ctxt format nonmono_Ts type_enc T = +fun formula_line_for_tags_mono_type ctxt format mono type_enc T = let val x_var = ATerm (`make_bound_var "X", []) in Formula (tags_sym_formula_prefix ^ ascii_of (mangled_type format type_enc T), Axiom, eq_formula type_enc (atyps_of T) false - (tag_with_type ctxt format nonmono_Ts type_enc NONE T - x_var) + (tag_with_type ctxt format mono type_enc NONE T x_var) x_var, isabelle_info simpN, NONE) end -fun problem_lines_for_mono_types ctxt format nonmono_Ts type_enc Ts = +fun problem_lines_for_mono_types ctxt format mono type_enc Ts = case type_enc of Simple_Types _ => [] | Guards _ => - map (formula_line_for_guards_mono_type ctxt format nonmono_Ts type_enc) Ts - | Tags _ => - map (formula_line_for_tags_mono_type ctxt format nonmono_Ts type_enc) Ts + map (formula_line_for_guards_mono_type ctxt format mono type_enc) Ts + | Tags _ => map (formula_line_for_tags_mono_type ctxt format mono type_enc) Ts -fun decl_line_for_sym ctxt format nonmono_Ts type_enc s +fun decl_line_for_sym ctxt format mono type_enc s (s', T_args, T, pred_sym, ary, _) = let val (T_arg_Ts, level) = @@ -1867,12 +1897,12 @@ | _ => (replicate (length T_args) homo_infinite_type, No_Types) in Decl (sym_decl_prefix ^ s, (s, s'), - (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary)) + (T_arg_Ts ---> (T |> homogenized_type ctxt mono level ary)) |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary)) end -fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind nonmono_Ts - type_enc n s j (s', T_args, T, _, ary, in_conj) = +fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s + j (s', T_args, T, _, ary, in_conj) = let val (kind, maybe_negate) = if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot) @@ -1886,7 +1916,7 @@ val sym_needs_arg_types = exists (curry (op =) dummyT) T_args fun should_keep_arg_type T = sym_needs_arg_types andalso - should_predicate_on_type ctxt nonmono_Ts type_enc (K true) T + should_guard_type ctxt mono type_enc (K true) T val bound_Ts = arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE) in @@ -1896,7 +1926,7 @@ |> fold (curry (IApp o swap)) bounds |> type_guard_iterm ctxt format type_enc res_T |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts) - |> formula_from_iformula ctxt format nonmono_Ts type_enc + |> formula_from_iformula ctxt format mono type_enc (K (K (K (K true)))) (SOME true) |> n > 1 ? bound_tvars type_enc (atyps_of T) |> close_formula_universally @@ -1904,8 +1934,8 @@ isabelle_info introN, NONE) end -fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind - nonmono_Ts type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) = +fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind mono + type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) = let val ident_base = tags_sym_formula_prefix ^ s ^ @@ -1920,8 +1950,8 @@ val cst = mk_aterm format type_enc (s, s') T_args val eq = maybe_negate oo eq_formula type_enc (atyps_of T) pred_sym val should_encode = - should_encode_type ctxt nonmono_Ts (level_of_type_enc type_enc) - val tag_with = tag_with_type ctxt format nonmono_Ts type_enc NONE + should_encode_type ctxt mono (level_of_type_enc type_enc) + val tag_with = tag_with_type ctxt format mono type_enc NONE val add_formula_for_res = if should_encode res_T then cons (Formula (ident_base ^ "_res", kind, @@ -1949,19 +1979,19 @@ fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd -fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_enc +fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc (s, decls) = case type_enc of Simple_Types _ => - decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s) + decls |> map (decl_line_for_sym ctxt format mono type_enc s) | Guards (_, level, _) => let val decls = case decls of decl :: (decls' as _ :: _) => let val T = result_type_of_decl decl in - if forall (curry (type_instance ctxt o swap) T - o result_type_of_decl) decls' then + if forall (type_generalization ctxt T o result_type_of_decl) + decls' then [decl] else decls @@ -1969,12 +1999,12 @@ | _ => decls val n = length decls val decls = - decls |> filter (should_encode_type ctxt nonmono_Ts level + decls |> filter (should_encode_type ctxt mono level o result_type_of_decl) in (0 upto length decls - 1, decls) - |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind - nonmono_Ts type_enc n s) + |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono + type_enc n s) end | Tags (_, _, heaviness) => (case heaviness of @@ -1983,26 +2013,26 @@ let val n = length decls in (0 upto n - 1 ~~ decls) |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format - conj_sym_kind nonmono_Ts type_enc n s) + conj_sym_kind mono type_enc n s) end) -fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts - type_enc sym_decl_tab = +fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc + 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 nonmono_Ts + |> 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 nonmono_Ts type_enc mono_Ts + problem_lines_for_mono_types ctxt format mono type_enc mono_Ts val decl_lines = fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind - nonmono_Ts type_enc) + mono type_enc) syms [] in mono_lines @ decl_lines end @@ -2063,7 +2093,7 @@ translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc hyp_ts concl_t facts val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply - val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc + val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc val repair = repair_fact ctxt format type_enc sym_tab val (conjs, facts) = (conjs, facts) |> pairself (map repair) val repaired_sym_tab = @@ -2074,12 +2104,12 @@ 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 nonmono_Ts + |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc val helper_lines = 0 upto length helpers - 1 ~~ helpers - |> map (formula_line_for_fact ctxt format helper_prefix I false true - nonmono_Ts type_enc) + |> map (formula_line_for_fact ctxt format helper_prefix I false true mono + type_enc) |> (if needs_type_tag_idempotence type_enc then cons (type_tag_idempotence_fact ()) else @@ -2090,15 +2120,14 @@ [(explicit_declsN, sym_decl_lines), (factsN, map (formula_line_for_fact ctxt format fact_prefix ascii_of - (not exporter) (not exporter) nonmono_Ts + (not exporter) (not exporter) mono type_enc) (0 upto length facts - 1 ~~ facts)), (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses), (aritiesN, map formula_line_for_arity_clause arity_clauses), (helpersN, helper_lines), (conjsN, - map (formula_line_for_conjecture ctxt format nonmono_Ts type_enc) - conjs), + map (formula_line_for_conjecture ctxt format mono type_enc) conjs), (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))] val problem = problem diff -r d21f7e330ec8 -r cd1e32b8d4c4 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Mon Aug 22 15:02:45 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Mon Aug 22 15:02:45 2011 +0200 @@ -15,6 +15,9 @@ val maybe_quote : string -> string val string_from_ext_time : bool * Time.time -> string val string_from_time : Time.time -> string + val type_instance : Proof.context -> typ -> typ -> bool + val type_generalization : Proof.context -> typ -> typ -> bool + val type_aconv : Proof.context -> typ * typ -> bool val varify_type : Proof.context -> typ -> typ val instantiate_type : theory -> typ -> typ -> typ -> typ val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ @@ -22,7 +25,7 @@ Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp -> typ val is_type_surely_finite : Proof.context -> typ -> bool - val is_type_surely_infinite : Proof.context -> typ list -> typ -> bool + val is_type_surely_infinite : Proof.context -> bool -> typ list -> typ -> bool val s_not : term -> term val s_conj : term * term -> term val s_disj : term * term -> term @@ -111,6 +114,12 @@ val string_from_time = string_from_ext_time o pair false +fun type_instance ctxt T T' = + Sign.typ_instance (Proof_Context.theory_of ctxt) (T, T') +fun type_generalization ctxt T T' = type_instance ctxt T' T +fun type_aconv ctxt (T, T') = + type_instance ctxt T T' andalso type_instance ctxt T' T + fun varify_type ctxt T = Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)] |> snd |> the_single |> dest_Const |> snd @@ -149,14 +158,16 @@ 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 assigns default_card T = +fun tiny_card_of_type ctxt inst_tvars 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 (Sign.typ_instance thy o swap) assigns T of + else case AList.lookup type_cmp assigns T of SOME k => k | NONE => case T of @@ -208,9 +219,9 @@ | TVar _ => default_card in Int.min (max, aux false [] T) end -fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt [] 0 T <> 0 -fun is_type_surely_infinite ctxt infinite_Ts T = - tiny_card_of_type ctxt (map (rpair 0) infinite_Ts) 1 T = 0 +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 (* Simple simplifications to ensure that sort annotations don't leave a trail of spurious "True"s. *)