868 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => |
868 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => |
869 if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t |
869 if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t |
870 | _ => do_term bs t |
870 | _ => do_term bs t |
871 in do_formula [] end |
871 in do_formula [] end |
872 |
872 |
873 fun presimplify_term ctxt = |
873 fun presimplify_term _ [] t = t |
874 Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |
874 | presimplify_term ctxt presimp_consts t = |
875 #> Meson.presimplify ctxt |
875 t |> exists_Const (member (op =) presimp_consts o fst) t |
876 #> prop_of |
876 ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |
|
877 #> Meson.presimplify ctxt |
|
878 #> prop_of) |
877 |
879 |
878 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j |
880 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j |
879 fun conceal_bounds Ts t = |
881 fun conceal_bounds Ts t = |
880 subst_bounds (map (Free o apfst concealed_bound_name) |
882 subst_bounds (map (Free o apfst concealed_bound_name) |
881 (0 upto length Ts - 1 ~~ Ts), t) |
883 (0 upto length Ts - 1 ~~ Ts), t) |
938 | aux (Var ((s, i), T)) = |
940 | aux (Var ((s, i), T)) = |
939 Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T) |
941 Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T) |
940 | aux t = t |
942 | aux t = t |
941 in t |> exists_subterm is_Var t ? aux end |
943 in t |> exists_subterm is_Var t ? aux end |
942 |
944 |
943 fun preprocess_prop ctxt presimp kind t = |
945 fun preprocess_prop ctxt presimp_consts kind t = |
944 let |
946 let |
945 val thy = Proof_Context.theory_of ctxt |
947 val thy = Proof_Context.theory_of ctxt |
946 val t = t |> Envir.beta_eta_contract |
948 val t = t |> Envir.beta_eta_contract |
947 |> transform_elim_prop |
949 |> transform_elim_prop |
948 |> Object_Logic.atomize_term thy |
950 |> Object_Logic.atomize_term thy |
949 val need_trueprop = (fastype_of t = @{typ bool}) |
951 val need_trueprop = (fastype_of t = @{typ bool}) |
950 in |
952 in |
951 t |> need_trueprop ? HOLogic.mk_Trueprop |
953 t |> need_trueprop ? HOLogic.mk_Trueprop |
952 |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) [] |
954 |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) [] |
953 |> extensionalize_term ctxt |
955 |> extensionalize_term ctxt |
954 |> presimp ? presimplify_term ctxt |
956 |> presimplify_term ctxt presimp_consts |
955 |> perhaps (try (HOLogic.dest_Trueprop)) |
957 |> perhaps (try (HOLogic.dest_Trueprop)) |
956 |> introduce_combinators_in_term ctxt kind |
958 |> introduce_combinators_in_term ctxt kind |
957 end |
959 end |
958 |
960 |
959 (* making fact and conjecture formulas *) |
961 (* making fact and conjecture formulas *) |
964 in |
966 in |
965 {name = name, locality = loc, kind = kind, combformula = combformula, |
967 {name = name, locality = loc, kind = kind, combformula = combformula, |
966 atomic_types = atomic_types} |
968 atomic_types = atomic_types} |
967 end |
969 end |
968 |
970 |
969 fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp |
971 fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp_consts |
970 ((name, loc), t) = |
972 ((name, loc), t) = |
971 let val thy = Proof_Context.theory_of ctxt in |
973 let val thy = Proof_Context.theory_of ctxt in |
972 case (keep_trivial, |
974 case (keep_trivial, |
973 t |> preproc ? preprocess_prop ctxt presimp Axiom |
975 t |> preproc ? preprocess_prop ctxt presimp_consts Axiom |
974 |> make_formula thy format type_sys eq_as_iff name loc Axiom) of |
976 |> make_formula thy format type_sys eq_as_iff name loc Axiom) of |
975 (false, |
977 (false, |
976 formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) => |
978 formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) => |
977 if s = tptp_true then NONE else SOME formula |
979 if s = tptp_true then NONE else SOME formula |
978 | (_, formula) => SOME formula |
980 | (_, formula) => SOME formula |
979 end |
981 end |
980 |
982 |
981 fun make_conjecture ctxt format prem_kind type_sys preproc ts = |
983 fun make_conjecture ctxt format prem_kind type_sys preproc presimp_consts ts = |
982 let |
984 let |
983 val thy = Proof_Context.theory_of ctxt |
985 val thy = Proof_Context.theory_of ctxt |
984 val last = length ts - 1 |
986 val last = length ts - 1 |
985 in |
987 in |
986 map2 (fn j => fn t => |
988 map2 (fn j => fn t => |
1342 ? (case types of |
1345 ? (case types of |
1343 [T] => specialize_type thy (invert_const unmangled_s, T) |
1346 [T] => specialize_type thy (invert_const unmangled_s, T) |
1344 | _ => I) |
1347 | _ => I) |
1345 end) |
1348 end) |
1346 val make_facts = |
1349 val make_facts = |
1347 map_filter (make_fact ctxt format type_sys false false false false) |
1350 map_filter (make_fact ctxt format type_sys false false false []) |
1348 val fairly_sound = is_type_sys_fairly_sound type_sys |
1351 val fairly_sound = is_type_sys_fairly_sound type_sys |
1349 in |
1352 in |
1350 helper_table |
1353 helper_table |
1351 |> maps (fn ((helper_s, needs_fairly_sound), ths) => |
1354 |> maps (fn ((helper_s, needs_fairly_sound), ths) => |
1352 if helper_s <> unmangled_s orelse |
1355 if helper_s <> unmangled_s orelse |
1404 fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t |
1407 fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t |
1405 facts = |
1408 facts = |
1406 let |
1409 let |
1407 val thy = Proof_Context.theory_of ctxt |
1410 val thy = Proof_Context.theory_of ctxt |
1408 val fact_ts = facts |> map snd |
1411 val fact_ts = facts |> map snd |
|
1412 val presimp_consts = Meson.presimplified_consts ctxt |
|
1413 val make_fact = |
|
1414 make_fact ctxt format type_sys false true true presimp_consts |
1409 val (facts, fact_names) = |
1415 val (facts, fact_names) = |
1410 facts |> map (fn (name, t) => |
1416 facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name) |
1411 (name, t) |
|
1412 |> make_fact ctxt format type_sys false true true true |
|
1413 |> rpair name) |
|
1414 |> map_filter (try (apfst the)) |
1417 |> map_filter (try (apfst the)) |
1415 |> ListPair.unzip |
1418 |> ListPair.unzip |
1416 (* Remove existing facts from the conjecture, as this can dramatically |
1419 (* Remove existing facts from the conjecture, as this can dramatically |
1417 boost an ATP's performance (for some reason). *) |
1420 boost an ATP's performance (for some reason). *) |
1418 val hyp_ts = |
1421 val hyp_ts = |
1423 val subs = tfree_classes_of_terms all_ts |
1426 val subs = tfree_classes_of_terms all_ts |
1424 val supers = tvar_classes_of_terms all_ts |
1427 val supers = tvar_classes_of_terms all_ts |
1425 val tycons = type_constrs_of_terms thy all_ts |
1428 val tycons = type_constrs_of_terms thy all_ts |
1426 val conjs = |
1429 val conjs = |
1427 hyp_ts @ [concl_t] |
1430 hyp_ts @ [concl_t] |
1428 |> make_conjecture ctxt format prem_kind type_sys preproc |
1431 |> make_conjecture ctxt format prem_kind type_sys preproc presimp_consts |
1429 val (supers', arity_clauses) = |
1432 val (supers', arity_clauses) = |
1430 if level_of_type_sys type_sys = No_Types then ([], []) |
1433 if level_of_type_sys type_sys = No_Types then ([], []) |
1431 else make_arity_clauses thy tycons supers |
1434 else make_arity_clauses thy tycons supers |
1432 val class_rel_clauses = make_class_rel_clauses thy subs supers' |
1435 val class_rel_clauses = make_class_rel_clauses thy subs supers' |
1433 in |
1436 in |