src/HOL/Tools/res_atp.ML
changeset 21470 7c1b59ddcd56
parent 21431 ef9080e7dbbc
child 21506 b2a673894ce5
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Nov 22 19:55:22 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Nov 22 20:08:07 2006 +0100
     1.3 @@ -247,9 +247,11 @@
     1.4  exception PRED_LG of term;
     1.5  
     1.6  fun pred_lg (t as Const(P,tp)) (lg,seen)= 
     1.7 -      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen) 
     1.8 +      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) 
     1.9 +      else (lg,insert (op =) t seen) 
    1.10    | pred_lg (t as Free(P,tp)) (lg,seen) =
    1.11 -      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen)
    1.12 +      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) 
    1.13 +      else (lg,insert (op =) t seen)
    1.14    | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen)
    1.15    | pred_lg P _ = raise PRED_LG(P);
    1.16  
    1.17 @@ -275,18 +277,13 @@
    1.18        end
    1.19    | lits_lg lits (lg,seen) = (lg,seen);
    1.20  
    1.21 -fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = 
    1.22 -    dest_disj_aux t (dest_disj_aux t' disjs)
    1.23 +fun dest_disj_aux (Const("Trueprop",_) $ t) disjs = dest_disj_aux t disjs
    1.24 +  | dest_disj_aux (Const ("op |", _) $ t $ t') disjs = dest_disj_aux t (dest_disj_aux t' disjs)
    1.25    | dest_disj_aux t disjs = t::disjs;
    1.26  
    1.27  fun dest_disj t = dest_disj_aux t [];
    1.28  
    1.29 -fun logic_of_clause tm (lg,seen) =
    1.30 -    let val tm' = HOLogic.dest_Trueprop tm
    1.31 -	val disjs = dest_disj tm'
    1.32 -    in
    1.33 -	lits_lg disjs (lg,seen)
    1.34 -    end;
    1.35 +fun logic_of_clause tm = lits_lg (dest_disj tm);
    1.36  
    1.37  fun logic_of_clauses [] (lg,seen) = (lg,seen)
    1.38    | logic_of_clauses (cls::clss) (FOL,seen) =
    1.39 @@ -316,7 +313,7 @@
    1.40  (*The rule subsetI is frequently omitted by the relevance filter.*)
    1.41  val whitelist = ref [subsetI]; 
    1.42    
    1.43 -(*Names of theorems (not theorem lists! See multi_blacklist above) to be banned. 
    1.44 +(*Names of theorems (not theorem lists! See multi_blacklist below) to be banned. 
    1.45  
    1.46    These theorems typically produce clauses that are prolific (match too many equality or
    1.47    membership literals) and relate to seldom-used facts. Some duplicate other rules.
    1.48 @@ -471,10 +468,6 @@
    1.49        Polyhash.insert ht (x^"_iff2", ()); 
    1.50        Polyhash.insert ht (x^"_dest", ())); 
    1.51  
    1.52 -(*FIXME: probably redundant now that ALL boolean-valued variables are banned*)
    1.53 -fun banned_thmlist s =
    1.54 -  (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"];
    1.55 -
    1.56  (*Reject theorems with names like "List.filter.filter_list_def" or
    1.57    "Accessible_Part.acc.defs", as these are definitions arising from packages.
    1.58    FIXME: this will also block definitions within locales*)
    1.59 @@ -486,7 +479,7 @@
    1.60    let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
    1.61                                  (6000, HASH_STRING)
    1.62        fun banned s = 
    1.63 -            isSome (Polyhash.peek ht s) orelse banned_thmlist s orelse is_package_def s
    1.64 +            isSome (Polyhash.peek ht s) orelse is_package_def s
    1.65    in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
    1.66        app (insert_suffixed_names ht) (!blacklist @ xs); 
    1.67        banned
    1.68 @@ -505,12 +498,7 @@
    1.69  fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0))
    1.70    | hash_literal P = hashw_term(P,0w0);
    1.71  
    1.72 -
    1.73 -fun get_literals (Const("Trueprop",_)$P) lits = get_literals P lits
    1.74 -  | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits)
    1.75 -  | get_literals lit lits = (lit::lits);
    1.76 -
    1.77 -fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t [])));
    1.78 +fun hash_term t = Word.toIntX (xor_words (map hash_literal (dest_disj t)));
    1.79  
    1.80  fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
    1.81  
    1.82 @@ -565,9 +553,13 @@
    1.83    ["Set.ball_simps", "Set.bex_simps",  (*quantifier rewriting: useless*)
    1.84     "Set.disjoint_insert", "Set.insert_disjoint", "Set.Inter_UNIV_conv"];
    1.85  
    1.86 +val multi_base_blacklist =
    1.87 +  ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"];
    1.88 +
    1.89  (*Ignore blacklisted theorem lists*)
    1.90  fun add_multi_names ((a, ths), pairs) = 
    1.91 -  if a mem_string multi_blacklist then pairs
    1.92 +  if a mem_string multi_blacklist orelse (Sign.base_name a) mem_string multi_base_blacklist
    1.93 +  then pairs
    1.94    else add_multi_names_aux ((a, ths), pairs);
    1.95  
    1.96  fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
    1.97 @@ -675,16 +667,50 @@
    1.98    if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls 
    1.99  	                else cls;
   1.100  
   1.101 +(**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
   1.102 +
   1.103 +(** Too general means, positive equality literal with a variable X as one operand,
   1.104 +  when X does not occur properly in the other operand. This rules out clearly
   1.105 +  inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
   1.106 + 
   1.107 +fun occurs ix =
   1.108 +    let fun occ(Var (jx,_)) = (ix=jx)
   1.109 +          | occ(t1$t2)      = occ t1 orelse occ t2
   1.110 +          | occ(Abs(_,_,t)) = occ t
   1.111 +          | occ _           = false
   1.112 +    in occ end;
   1.113 +
   1.114 +fun is_recordtype T = not (null (RecordPackage.dest_recTs T));
   1.115 +
   1.116 +(*Unwanted equalities include
   1.117 +  (1) those between a variable that does not properly occur in the second operand,
   1.118 +  (2) those between a variable and a record, since these seem to be prolific "cases" thms
   1.119 +*)  
   1.120 +fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T
   1.121 +  | too_general_eqterms _ = false;
   1.122 +
   1.123 +fun too_general_equality (Const ("op =", _) $ x $ y) =
   1.124 +      too_general_eqterms (x,y) orelse too_general_eqterms(y,x)
   1.125 +  | too_general_equality _ = false;
   1.126 +
   1.127 +(* tautologous? *)
   1.128 +fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true
   1.129 +  | is_taut _ = false;
   1.130 +
   1.131  (*True if the term contains a variable whose (atomic) type is in the given list.*)
   1.132  fun has_typed_var tycons = 
   1.133    let fun var_tycon (Var (_, Type(a,_))) = a mem_string tycons
   1.134          | var_tycon _ = false
   1.135    in  exists var_tycon o term_vars  end;
   1.136  
   1.137 +fun unwanted t =
   1.138 +    is_taut t orelse has_typed_var ["Product_Type.unit","bool"] t orelse
   1.139 +    forall too_general_equality (dest_disj t);
   1.140 +
   1.141  (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
   1.142    likely to lead to unsound proofs.*)
   1.143 -fun remove_finite_types cls =
   1.144 -  filter (not o has_typed_var ["Product_Type.unit","bool"] o prop_of o fst) cls;
   1.145 +fun remove_unwanted_clauses cls =
   1.146 +  filter (not o unwanted o prop_of o fst) cls;
   1.147  
   1.148  fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   1.149      if is_fol_logic logic 
   1.150 @@ -711,7 +737,7 @@
   1.151  	val cla_simp_atp_clauses = included_thms |> blacklist_filter
   1.152  	                             |> ResAxioms.cnf_rules_pairs |> make_unique 
   1.153                                       |> restrict_to_logic logic 
   1.154 -                                     |> remove_finite_types
   1.155 +                                     |> remove_unwanted_clauses
   1.156  	val user_cls = ResAxioms.cnf_rules_pairs user_rules
   1.157  	val thy = ProofContext.theory_of ctxt
   1.158  	val axclauses = make_unique (get_relevant_clauses thy cla_simp_atp_clauses user_cls goal_tms)
   1.159 @@ -833,7 +859,7 @@
   1.160        val included_cls = included_thms |> blacklist_filter
   1.161                                         |> ResAxioms.cnf_rules_pairs |> make_unique 
   1.162                                         |> restrict_to_logic logic
   1.163 -                                       |> remove_finite_types
   1.164 +                                       |> remove_unwanted_clauses
   1.165        val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
   1.166        val white_cls = ResAxioms.cnf_rules_pairs white_thms
   1.167        (*clauses relevant to goal gl*)