# HG changeset patch # User blanchet # Date 1305888479 -7200 # Node ID 208ec29cc013c20510646d2b29a99ebceeafb4f0 # Parent 91adf04946d1c05002b20cf20da9cec51bd6b363 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything diff -r 91adf04946d1 -r 208ec29cc013 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 12:47:59 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 12:47:59 2011 +0200 @@ -140,15 +140,12 @@ |> (fn (poly, (level, (heaviness, core))) => case (core, (poly, level, heaviness)) of ("simple", (NONE, _, Light)) => Simple_Types level - | ("preds", (SOME Polymorphic, _, _)) => - Preds (Polymorphic, level, heaviness) | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness) | ("tags", (SOME Polymorphic, All_Types, _)) => Tags (Polymorphic, All_Types, heaviness) - | ("tags", (SOME Polymorphic, Finite_Types, _)) => - (* The actual light encoding yields too many unsound proofs. *) - Tags (Polymorphic, Finite_Types, Heavy) - | ("tags", (SOME Polymorphic, _, _)) => raise Same.SAME + | ("tags", (SOME Polymorphic, _, _)) => + (* The actual light encoding is very unsound. *) + Tags (Polymorphic, level, Heavy) | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness) | ("args", (SOME poly, All_Types (* naja *), Light)) => Preds (poly, Const_Arg_Types, Light) @@ -499,13 +496,19 @@ (** Finite and infinite type inference **) +fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S) + | deep_freeze_atyp T = T +val deep_freeze_type = map_atyps deep_freeze_atyp + +val type_instance = Sign.typ_instance o Proof_Context.theory_of + (* 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 _ (nonmono_Ts as _ :: _) _ T = - exists (curry Type.raw_instance T) nonmono_Ts +fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T = + exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts | should_encode_type _ _ All_Types _ = true | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T | should_encode_type _ _ _ _ = false @@ -951,10 +954,10 @@ (** Symbol declarations **) -fun insert_type get_T x xs = +fun insert_type ctxt get_T x xs = let val T = get_T x in - if exists (curry Type.raw_instance T o get_T) xs then xs - else x :: filter_out ((fn T' => Type.raw_instance (T', T)) o get_T) xs + 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 end fun should_declare_sym type_sys pred_sym s = @@ -965,7 +968,7 @@ | Tags (_, _, Light) => true | _ => false) orelse not pred_sym) -fun sym_decl_table_for_facts type_sys repaired_sym_tab (conjs, facts) = +fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) = let fun add_combterm in_conj tm = let val (head, args) = strip_combterm_comb tm in @@ -974,8 +977,8 @@ let val pred_sym = is_pred_sym repaired_sym_tab s in if should_declare_sym type_sys pred_sym s then Symtab.map_default (s, []) - (insert_type #3 (s', T_args, T, pred_sym, length args, - in_conj)) + (insert_type ctxt #3 (s', T_args, T, pred_sym, length args, + in_conj)) else I end @@ -990,35 +993,37 @@ ? (fold (add_fact true) conjs #> fold (add_fact false) facts) end +(* 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}, @{typ int}, @{typ "nat => 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_combterm_nonmonotonic_types _ _ (SOME false) _ = I +fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I | add_combterm_nonmonotonic_types ctxt level _ (CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1), tm2)) = (exists is_var_or_bound_var [tm1, tm2] andalso (case level of - Nonmonotonic_Types => not (is_type_surely_infinite ctxt T) + Nonmonotonic_Types => + not (is_type_surely_infinite ctxt known_infinite_types T) | Finite_Types => is_type_surely_finite ctxt T - | _ => true)) ? insert_type I T + | _ => true)) ? insert_type ctxt I (deep_freeze_type T) | add_combterm_nonmonotonic_types _ _ _ _ = I fun add_fact_nonmonotonic_types ctxt level ({kind, combformula, ...} : translated_formula) = formula_fold (SOME (kind <> Conjecture)) (add_combterm_nonmonotonic_types ctxt level) combformula -fun add_nonmonotonic_types_for_facts ctxt type_sys facts = +fun nonmonotonic_types_for_facts ctxt type_sys facts = let val level = level_of_type_sys type_sys in - (case level of - Nonmonotonic_Types => true - | Finite_Types => - heaviness_of_type_sys type_sys = Light andalso - polymorphism_of_type_sys type_sys <> Polymorphic - | _ => false) - ? (fold (add_fact_nonmonotonic_types ctxt level) facts - (* We must add bool in case the helper "True_or_False" is added later. - In addition, several places in the code rely on the list of - nonmonotonic types not being empty. *) - #> insert_type I @{typ bool}) + if level = Nonmonotonic_Types orelse level = Finite_Types then + [] |> fold (add_fact_nonmonotonic_types ctxt level) facts + (* We must add "bool" in case the helper "True_or_False" is added + later. In addition, several places in the code rely on the list of + nonmonotonic types not being empty. *) + |> insert_type ctxt I @{typ bool} + else + [] end fun decl_line_for_sym ctxt nonmono_Ts level s (s', _, T, pred_sym, ary, _) = @@ -1124,7 +1129,7 @@ case decls of decl :: (decls' as _ :: _) => let val T = result_type_of_decl decl in - if forall ((fn T' => Type.raw_instance (T', T)) + if forall (curry (type_instance ctxt o swap) T o result_type_of_decl) decls' then [decl] else @@ -1198,8 +1203,7 @@ val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = translate_formulas ctxt prem_kind type_sys hyp_ts concl_t facts val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply - val nonmono_Ts = - [] |> fold (add_nonmonotonic_types_for_facts ctxt type_sys) [facts, conjs] + val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys val repair = repair_fact ctxt nonmono_Ts type_sys sym_tab val (conjs, facts) = (conjs, facts) |> pairself (map repair) val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false @@ -1207,7 +1211,7 @@ repaired_sym_tab |> helper_facts_for_sym_table ctxt type_sys |> map repair val sym_decl_lines = (conjs, helpers @ facts) - |> sym_decl_table_for_facts type_sys repaired_sym_tab + |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab |> problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys val helper_lines = map (formula_line_for_fact ctxt helper_prefix nonmono_Ts type_sys) diff -r 91adf04946d1 -r 208ec29cc013 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 20 12:47:59 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 20 12:47:59 2011 +0200 @@ -22,7 +22,7 @@ val instantiate_type : theory -> typ -> typ -> typ -> typ val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ val is_type_surely_finite : Proof.context -> typ -> bool - val is_type_surely_infinite : Proof.context -> typ -> bool + val is_type_surely_infinite : Proof.context -> typ list -> typ -> bool val monomorphic_term : Type.tyenv -> term -> term val eta_expand : typ list -> term -> int -> term val transform_elim_term : term -> term @@ -122,79 +122,74 @@ | NONE => []) | datatype_constrs _ _ = [] -(* Feel free to extend this list with any sorts that don't have finiteness - axioms. *) -val safe_sorts = - @{sort type} @ @{sort "{default,zero,one,plus,minus,uminus,times,inverse}"} @ - @{sort "{abs,sgn,ord,equal,number}"} - (* Similar to "Nitpick_HOL.bounded_exact_card_of_type". 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 default_card T = +fun tiny_card_of_type ctxt default_card assigns T = let + val thy = Proof_Context.theory_of ctxt val max = 2 (* 1 would be too small for the "fun" case *) fun aux slack avoid T = if member (op =) avoid T then 0 - else case T of - Type (@{type_name fun}, [T1, T2]) => - (case (aux slack avoid T1, aux slack avoid T2) of - (k, 1) => if slack andalso k = 0 then 0 else 1 - | (0, _) => 0 - | (_, 0) => 0 - | (k1, k2) => - if k1 >= max orelse k2 >= max then max - else Int.min (max, Integer.pow k2 k1)) - | @{typ prop} => 2 - | @{typ bool} => 2 (* optimization *) - | @{typ nat} => 0 (* optimization *) - | @{typ int} => 0 (* optimization *) - | Type (s, _) => - let val thy = Proof_Context.theory_of ctxt in - case datatype_constrs thy T of - constrs as _ :: _ => - let - val constr_cards = - map (Integer.prod o map (aux slack (T :: avoid)) o binder_types - o snd) constrs - in - if exists (curry (op =) 0) constr_cards then 0 - else Int.min (max, Integer.sum constr_cards) - end - | [] => - case Typedef.get_info ctxt s of - ({abs_type, rep_type, ...}, _) :: _ => - (* We cheat here by assuming that typedef types are infinite if - their underlying type is infinite. This is unsound in general - but it's hard to think of a realistic example where this would - not be the case. We are also slack with representation types: - If a representation type has the form "sigma => tau", we - consider it enough to check "sigma" for infiniteness. (Look for - "slack" in this function.) *) - (case varify_and_instantiate_type ctxt - (Logic.varifyT_global abs_type) T - (Logic.varifyT_global rep_type) - |> aux true avoid of - 0 => 0 - | 1 => 1 - | _ => default_card) - | [] => default_card - end - (* 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 - (* Schematic type variables that contain only unproblematic sorts - (with no finiteness axiom) can safely be considered infinite. *) - | TVar (_, S) => - if default_card = 0 orelse subset (op =) (S, safe_sorts) then 0 - else default_card + else case AList.lookup (Sign.typ_instance thy o swap) assigns T of + SOME k => k + | NONE => + case T of + Type (@{type_name fun}, [T1, T2]) => + (case (aux slack avoid T1, aux slack avoid T2) of + (k, 1) => if slack andalso k = 0 then 0 else 1 + | (0, _) => 0 + | (_, 0) => 0 + | (k1, k2) => + if k1 >= max orelse k2 >= max then max + else Int.min (max, Integer.pow k2 k1)) + | @{typ prop} => 2 + | @{typ bool} => 2 (* optimization *) + | @{typ nat} => 0 (* optimization *) + | @{typ int} => 0 (* optimization *) + | Type (s, _) => + (case datatype_constrs thy T of + constrs as _ :: _ => + let + val constr_cards = + map (Integer.prod o map (aux slack (T :: avoid)) o binder_types + o snd) constrs + in + if exists (curry (op =) 0) constr_cards then 0 + else Int.min (max, Integer.sum constr_cards) + end + | [] => + case Typedef.get_info ctxt s of + ({abs_type, rep_type, ...}, _) :: _ => + (* We cheat here by assuming that typedef types are infinite if + their underlying type is infinite. This is unsound in general + but it's hard to think of a realistic example where this would + not be the case. We are also slack with representation types: + If a representation type has the form "sigma => tau", we + consider it enough to check "sigma" for infiniteness. (Look + for "slack" in this function.) *) + (case varify_and_instantiate_type ctxt + (Logic.varifyT_global abs_type) T + (Logic.varifyT_global rep_type) + |> aux true avoid of + 0 => 0 + | 1 => 1 + | _ => default_card) + | [] => default_card) + (* 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 + (* Schematic type variables that contain only unproblematic sorts + (with no finiteness axiom) can safely be considered infinite. *) + | 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 T = tiny_card_of_type ctxt 1 T = 0 +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 1 (map (rpair 0) infinite_Ts) T = 0 fun monomorphic_term subst t = map_types (map_type_tvar (fn v =>