wneuper/isa: comparison src/HOL/Tools/ATP/atp

equal deleted inserted replaced

-:69251cad0da0
+:e88e974c4846
 No_Type_Args
 else
 general_type_arg_policy type_sys
 (*Make literals for sorted type variables*)
-fun sorts_on_typs_aux (_, []) = []
+fun generic_sorts_on_type (_, []) = []
-| sorts_on_typs_aux ((x, i), s :: ss) =
+| generic_sorts_on_type ((x, i), s :: ss) =
-sorts_on_typs_aux ((x, i), ss)
+generic_sorts_on_type ((x, i), ss)
 |> (if s = the_single @{sort HOL.type} then
 I
 else if i = ~1 then
 cons (TyLitFree (`make_type_class s, `make_fixed_type_var x))
 else
 cons (TyLitVar (`make_type_class s,
 (make_schematic_type_var (x, i), x))))
+fun sorts_on_tfree (TFree (s, S)) = generic_sorts_on_type ((s, ~1), S)
-fun sorts_on_typs (TFree (a, s)) = sorts_on_typs_aux ((a, ~1), s)
+| sorts_on_tfree _ = []
-| sorts_on_typs (TVar (v, s)) = sorts_on_typs_aux (v, s)
+fun sorts_on_tvar (TVar z) = generic_sorts_on_type z
-| sorts_on_typs _ = raise Fail "expected \"TVar\" or \"TFree\""
+| sorts_on_tvar _ = []
-(*Given a list of sorted type variables, return a list of type literals.*)
+(* Given a list of sorted type variables, return a list of type literals. *)
-val raw_type_literals_for_types = union_all o map sorts_on_typs
+fun raw_type_literals_for_types Ts =
+union_all (map sorts_on_tfree Ts @ map sorts_on_tvar Ts)
-fun type_literals_for_types format type_sys kind Ts =
-if level_of_type_sys type_sys = No_Types orelse format = CNF_UEQ then
+fun type_literals_for_types type_sys sorts_on_typ Ts =
-[]
+if level_of_type_sys type_sys = No_Types then []
-else
+else union_all (map sorts_on_typ Ts)
-Ts |> raw_type_literals_for_types
-|> filter (fn TyLitVar _ => kind <> Conjecture
-| TyLitFree _ => kind = Conjecture)
 fun mk_aconns c phis =
 let val (phis', phi') = split_last phis in
 fold_rev (mk_aconn c) phis' phi'
 end
 t |> need_trueprop ? HOLogic.mk_Trueprop
 |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
 |> extensionalize_term ctxt
 |> presimp ? presimplify_term ctxt
 |> introduce_combinators_in_term ctxt kind
-|> kind <> Axiom ? freeze_term
 end
 (* making fact and conjecture formulas *)
 fun make_formula thy format type_sys eq_as_iff name loc kind t =
 let
 else
 (prem_kind,
 if prem_kind = Conjecture then update_combformula mk_anot
 else I)
 in
-t |> preproc ? preprocess_prop ctxt true kind
+t |> preproc ? (preprocess_prop ctxt true kind #> freeze_term)
 |> make_formula thy format type_sys true (string_of_int j)
 General kind
 |> maybe_negate
 end)
 (0 upto last) ts
 end
 | do_formula pos (AConn conn) = aconn_map pos do_formula conn
 | do_formula _ (AAtom tm) = AAtom (do_term tm)
 in do_formula o SOME end
-fun bound_atomic_types format type_sys Ts =
+fun bound_tvars type_sys Ts =
 mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
-(type_literals_for_types format type_sys Axiom Ts))
+(type_literals_for_types type_sys sorts_on_tvar Ts))
 fun formula_for_fact ctxt format nonmono_Ts type_sys
 ({combformula, atomic_types, ...} : translated_formula) =
 combformula
 |> close_combformula_universally
 |> formula_from_combformula ctxt format nonmono_Ts type_sys
 is_var_nonmonotonic_in_formula true
-|> bound_atomic_types format type_sys atomic_types
+|> bound_tvars type_sys atomic_types
 |> close_formula_universally
 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
 of monomorphization). The TPTP explicitly forbids name clashes, and some of
 the remote provers might care. *)
 (formula_from_fo_literal
 (fo_literal_from_arity_literal concl_lits))
 |> close_formula_universally, intro_info, NONE)
 fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
-({name, kind, combformula, ...} : translated_formula) =
+({name, kind, combformula, atomic_types, ...} : translated_formula) =
 Formula (conjecture_prefix ^ name, kind,
 formula_from_combformula ctxt format nonmono_Ts type_sys
 is_var_nonmonotonic_in_formula false
 (close_combformula_universally combformula)
+|> bound_tvars type_sys atomic_types
 |> close_formula_universally, NONE, NONE)
-fun free_type_literals format type_sys
+fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
-({atomic_types, ...} : translated_formula) =
+atomic_types |> type_literals_for_types type_sys sorts_on_tfree
-atomic_types |> type_literals_for_types format type_sys Conjecture
 |> map fo_literal_from_type_literal
 fun formula_line_for_free_type j lit =
 Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
 formula_from_fo_literal lit, NONE, NONE)
-fun formula_lines_for_free_types format type_sys facts =
+fun formula_lines_for_free_types type_sys facts =
 let
-val litss = map (free_type_literals format type_sys) facts
+val litss = map (free_type_literals type_sys) facts
 val lits = fold (union (op =)) litss []
 in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
 (** Symbol declarations **)
 |> fold (curry (CombApp o swap)) bounds
 |> type_pred_combterm ctxt nonmono_Ts type_sys res_T
 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
 |> formula_from_combformula ctxt format nonmono_Ts type_sys
 (K (K (K (K true)))) true
-|> n > 1 ? bound_atomic_types format type_sys (atyps_of T)
+|> n > 1 ? bound_tvars type_sys (atyps_of T)
 |> close_formula_universally
 |> maybe_negate,
 intro_info, NONE)
 end
 val cst = mk_const_aterm (s, s') T_args
 val atomic_Ts = atyps_of T
 fun eq tms =
 (if pred_sym then AConn (AIff, map AAtom tms)
 else AAtom (ATerm (`I tptp_equal, tms)))
-|> bound_atomic_types format type_sys atomic_Ts
+|> bound_tvars type_sys atomic_Ts
 |> close_formula_universally
 |> maybe_negate
 val should_encode = should_encode_type ctxt nonmono_Ts All_Types
 val tag_with = tag_with_type ctxt format nonmono_Ts type_sys
 val add_formula_for_res =
 (aritiesN, map formula_line_for_arity_clause arity_clauses),
 (helpersN, helper_lines),
 (conjsN,
 map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)
 conjs),
-(free_typesN,
+(free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
-formula_lines_for_free_types format type_sys (facts @ conjs))]
 val problem =
 problem
 |> (case format of
 CNF => ensure_cnf_problem
 | CNF_UEQ => filter_cnf_ueq_problem

changeset 43939	e88e974c4846
parent 43937	f181d66046d4
child 43942	1d46d85cd78b