src/HOL/Tools/res_atp.ML
changeset 21397 2134b81a0b37
parent 21373 18f519614978
child 21431 ef9080e7dbbc
equal deleted inserted replaced
21396:afd8ba74313c 21397:2134b81a0b37
   664 fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   664 fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   665   | fold_type_consts f T x = x;
   665   | fold_type_consts f T x = x;
   666 
   666 
   667 val add_type_consts_in_type = fold_type_consts setinsert;
   667 val add_type_consts_in_type = fold_type_consts setinsert;
   668 
   668 
   669 val add_type_consts_in_term = fold_types add_type_consts_in_type;
   669 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
   670 
   670 fun add_type_consts_in_term thy =
   671 fun type_consts_of_terms ts =
   671   let val const_typargs = Sign.const_typargs thy
   672   Symtab.keys (fold add_type_consts_in_term ts Symtab.empty);
   672       fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x
       
   673         | add_tcs (Abs (_, T, u)) x = add_tcs u x
       
   674         | add_tcs (t $ u) x = add_tcs t (add_tcs u x)
       
   675         | add_tcs _ x = x
       
   676   in  add_tcs  end
       
   677 
       
   678 fun type_consts_of_terms thy ts =
       
   679   Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
   673 
   680 
   674 
   681 
   675 (***************************************************************)
   682 (***************************************************************)
   676 (* ATP invocation methods setup                                *)
   683 (* ATP invocation methods setup                                *)
   677 (***************************************************************)
   684 (***************************************************************)
   720 	                            user_cls (map prop_of goal_cls) |> make_unique
   727 	                            user_cls (map prop_of goal_cls) |> make_unique
   721 	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
   728 	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
   722         val subs = tfree_classes_of_terms (map prop_of goal_cls)
   729         val subs = tfree_classes_of_terms (map prop_of goal_cls)
   723         and axtms = map (prop_of o #1) axclauses
   730         and axtms = map (prop_of o #1) axclauses
   724         val supers = tvar_classes_of_terms axtms
   731         val supers = tvar_classes_of_terms axtms
   725         and tycons = type_consts_of_terms axtms
   732         and tycons = type_consts_of_terms thy axtms
   726         (*TFrees in conjecture clauses; TVars in axiom clauses*)
   733         (*TFrees in conjecture clauses; TVars in axiom clauses*)
   727         val classrel_clauses = 
   734         val classrel_clauses = 
   728               if keep_types then ResClause.make_classrel_clauses thy subs supers
   735               if keep_types then ResClause.make_classrel_clauses thy subs supers
   729               else []
   736               else []
   730 	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy tycons supers else []
   737 	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy tycons supers else []
   852                 val axcls = make_unique axcls
   859                 val axcls = make_unique axcls
   853                 val ccls = subtract_cls ccls axcls
   860                 val ccls = subtract_cls ccls axcls
   854                 val subs = tfree_classes_of_terms (map prop_of ccls)
   861                 val subs = tfree_classes_of_terms (map prop_of ccls)
   855                 and axtms = map (prop_of o #1) axcls
   862                 and axtms = map (prop_of o #1) axcls
   856                 val supers = tvar_classes_of_terms axtms
   863                 val supers = tvar_classes_of_terms axtms
   857                 and tycons = type_consts_of_terms axtms
   864                 and tycons = type_consts_of_terms thy axtms
   858                 (*TFrees in conjecture clauses; TVars in axiom clauses*)
   865                 (*TFrees in conjecture clauses; TVars in axiom clauses*)
   859                 val classrel_clauses = 
   866                 val classrel_clauses = 
   860                       if keep_types then ResClause.make_classrel_clauses thy subs supers
   867                       if keep_types then ResClause.make_classrel_clauses thy subs supers
   861                       else []
   868                       else []
   862                 val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
   869                 val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))