testing for empty sort
authorpaulson
Wed Jan 02 12:22:38 2008 +0100 (2008-01-02)
changeset 25761466e714de2fc
parent 25760 6d947d7a5ae8
child 25762 c03e9d04b3e4
testing for empty sort
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Tools/metis_tools.ML	Wed Jan 02 12:22:05 2008 +0100
     1.2 +++ b/src/HOL/Tools/metis_tools.ML	Wed Jan 02 12:22:38 2008 +0100
     1.3 @@ -612,6 +612,8 @@
     1.4      let val _ = Output.debug (fn () =>
     1.5            "Metis called with theorems " ^ cat_lines (map string_of_thm ths))
     1.6      in
     1.7 +       if exists_type ResAxioms.type_has_empty_sort (prop_of st0)  
     1.8 +       then error "Proof state contains the empty sort" else ();
     1.9         (Meson.MESON ResAxioms.neg_clausify (fn cls => rtac (FOL_SOLVE mode ctxt cls ths) 1) i
    1.10          THEN ResAxioms.expand_defs_tac st0) st0
    1.11      end;
     2.1 --- a/src/HOL/Tools/res_atp.ML	Wed Jan 02 12:22:05 2008 +0100
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Jan 02 12:22:38 2008 +0100
     2.3 @@ -829,6 +829,8 @@
     2.4                        their original "name hints" may be bad anyway.*)
     2.5      val thy = ProofContext.theory_of ctxt
     2.6    in
     2.7 +    if exists_type ResAxioms.type_has_empty_sort (prop_of goal)  
     2.8 +    then error "Proof state contains the empty sort" else ();
     2.9      Output.debug (fn () => "subgoals in isar_atp:\n" ^
    2.10                    Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)));
    2.11      Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
     3.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Jan 02 12:22:05 2008 +0100
     3.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Jan 02 12:22:38 2008 +0100
     3.3 @@ -11,6 +11,7 @@
     3.4    val pairname: thm -> string * thm
     3.5    val multi_base_blacklist: string list 
     3.6    val bad_for_atp: thm -> bool
     3.7 +  val type_has_empty_sort: typ -> bool
     3.8    val cnf_rules_pairs: (string * thm) list -> (thm * (string * int)) list
     3.9    val cnf_rules_of_ths: thm list -> thm list
    3.10    val neg_clausify: thm list -> thm list
    3.11 @@ -32,7 +33,11 @@
    3.12  (* FIXME legacy *)
    3.13  fun freeze_thm th = #1 (Drule.freeze_thaw th);
    3.14  
    3.15 -
    3.16 +fun type_has_empty_sort (TFree (_, [])) = true
    3.17 +  | type_has_empty_sort (TVar (_, [])) = true
    3.18 +  | type_has_empty_sort (Type (_, Ts)) = exists type_has_empty_sort Ts
    3.19 +  | type_has_empty_sort _ = false;
    3.20 +  
    3.21  (**** Transformation of Elimination Rules into First-Order Formulas****)
    3.22  
    3.23  val cfalse = cterm_of HOL.thy HOLogic.false_const;
    3.24 @@ -343,7 +348,10 @@
    3.25      | _ => false;
    3.26  
    3.27  fun bad_for_atp th = 
    3.28 -  PureThy.is_internal th orelse too_complex (prop_of th) orelse is_strange_thm th;
    3.29 +  PureThy.is_internal th     
    3.30 +  orelse too_complex (prop_of th)   
    3.31 +  orelse exists_type type_has_empty_sort (prop_of th)  
    3.32 +  orelse is_strange_thm th;
    3.33  
    3.34  val multi_base_blacklist =
    3.35    ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm",