renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
authorwenzelm
Thu Mar 04 21:10:25 2010 +0100 (2010-03-04 ago)
changeset 355688fbbfc39508f
parent 35567 309e75c58af2
child 35569 77dfdbf85fb8
renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
metis: type_has_topsort leads to tactic failure (with warning), like other metis failures;
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Tools/metis_tools.ML	Thu Mar 04 21:02:21 2010 +0100
     1.2 +++ b/src/HOL/Tools/metis_tools.ML	Thu Mar 04 21:10:25 2010 +0100
     1.3 @@ -714,12 +714,12 @@
     1.4    let val _ = trace_msg (fn () =>
     1.5          "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
     1.6    in
     1.7 -     if exists_type Res_Axioms.type_has_empty_sort (prop_of st0)
     1.8 -     then (error "metis: Proof state contains the empty sort"; Seq.empty)
     1.9 -     else
    1.10 -       (Meson.MESON Res_Axioms.neg_clausify
    1.11 -         (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
    1.12 -        THEN Res_Axioms.expand_defs_tac st0) st0
    1.13 +    if exists_type Res_Axioms.type_has_topsort (prop_of st0)
    1.14 +    then raise METIS "Metis: Proof state contains the universal sort {}"
    1.15 +    else
    1.16 +      (Meson.MESON Res_Axioms.neg_clausify
    1.17 +        (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
    1.18 +          THEN Res_Axioms.expand_defs_tac st0) st0
    1.19    end
    1.20    handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
    1.21  
    1.22 @@ -734,7 +734,7 @@
    1.23    type_lits_setup #>
    1.24    method @{binding metis} HO "METIS for FOL & HOL problems" #>
    1.25    method @{binding metisF} FO "METIS for FOL problems" #>
    1.26 -  method @{binding metisFT} FT "METIS With-fully typed translation" #>
    1.27 +  method @{binding metisFT} FT "METIS with fully-typed translation" #>
    1.28    Method.setup @{binding finish_clausify}
    1.29      (Scan.succeed (K (SIMPLE_METHOD (Res_Axioms.expand_defs_tac refl))))
    1.30      "cleanup after conversion to clauses";
     2.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Mar 04 21:02:21 2010 +0100
     2.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Mar 04 21:10:25 2010 +0100
     2.3 @@ -12,7 +12,7 @@
     2.4    val pairname: thm -> string * thm
     2.5    val multi_base_blacklist: string list
     2.6    val bad_for_atp: thm -> bool
     2.7 -  val type_has_empty_sort: typ -> bool
     2.8 +  val type_has_topsort: typ -> bool
     2.9    val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
    2.10    val neg_clausify: thm list -> thm list
    2.11    val expand_defs_tac: thm -> tactic
    2.12 @@ -31,10 +31,10 @@
    2.13  
    2.14  fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
    2.15  
    2.16 -fun type_has_empty_sort (TFree (_, [])) = true
    2.17 -  | type_has_empty_sort (TVar (_, [])) = true
    2.18 -  | type_has_empty_sort (Type (_, Ts)) = exists type_has_empty_sort Ts
    2.19 -  | type_has_empty_sort _ = false;
    2.20 +val type_has_topsort = Term.exists_subtype
    2.21 +  (fn TFree (_, []) => true
    2.22 +    | TVar (_, []) => true
    2.23 +    | _ => false);
    2.24  
    2.25  
    2.26  (**** Transformation of Elimination Rules into First-Order Formulas****)
    2.27 @@ -321,7 +321,7 @@
    2.28  
    2.29  fun bad_for_atp th =
    2.30    too_complex (prop_of th)
    2.31 -  orelse exists_type type_has_empty_sort (prop_of th)
    2.32 +  orelse exists_type type_has_topsort (prop_of th)
    2.33    orelse is_strange_thm th;
    2.34  
    2.35  val multi_base_blacklist =