1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Jul 05 17:09:59 2011 +0100
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Jul 05 17:09:59 2011 +0100
1.3 @@ -229,7 +229,11 @@
1.4 ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
1.5 ("fimplies", @{const_name ATP.fimplies})))),
1.6 ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
1.7 - ("fequal", @{const_name ATP.fequal}))))]
1.8 + ("fequal", @{const_name ATP.fequal})))),
1.9 + ("c_All", (@{const_name All}, (@{thm fAll_def},
1.10 + ("fAll", @{const_name ATP.fAll})))),
1.11 + ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
1.12 + ("fEx", @{const_name ATP.fEx}))))]
1.13
1.14 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
1.15
1.16 @@ -245,6 +249,8 @@
1.17 (@{const_name disj}, "disj"),
1.18 (@{const_name implies}, "implies"),
1.19 (@{const_name HOL.eq}, "equal"),
1.20 + (@{const_name All}, "All"),
1.21 + (@{const_name Ex}, "Ex"),
1.22 (@{const_name If}, "If"),
1.23 (@{const_name Set.member}, "member"),
1.24 (@{const_name Meson.COMBI}, "COMBI"),
1.25 @@ -493,7 +499,11 @@
1.26 nth bs j
1.27 |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
1.28 | combterm_from_term thy bs (Abs (s, T, t)) =
1.29 - let val (tm, atomic_Ts) = combterm_from_term thy ((s, T) :: bs) t in
1.30 + let
1.31 + fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
1.32 + val s = vary s
1.33 + val (tm, atomic_Ts) = combterm_from_term thy ((s, T) :: bs) t
1.34 + in
1.35 (CombAbs ((`make_bound_var s, T), tm),
1.36 union (op =) atomic_Ts (atyps_of T))
1.37 end
1.38 @@ -817,6 +827,8 @@
1.39 | (false, "c_conj") => (`I tptp_and, [])
1.40 | (false, "c_disj") => (`I tptp_or, [])
1.41 | (false, "c_implies") => (`I tptp_implies, [])
1.42 + | (false, "c_All") => (`I tptp_ho_forall, [])
1.43 + | (false, "c_Ex") => (`I tptp_ho_exists, [])
1.44 | (false, s) =>
1.45 if is_tptp_equal s then (`I tptp_equal, [])
1.46 else (proxy_base |>> prefix const_prefix, T_args)
1.47 @@ -886,7 +898,7 @@
1.48 else
1.49 t
1.50
1.51 -fun introduce_combinators_in_term ctxt kind t =
1.52 +fun process_abstractions_in_term ctxt type_enc kind t =
1.53 let val thy = Proof_Context.theory_of ctxt in
1.54 if Meson.is_fol_term thy t then
1.55 t
1.56 @@ -911,6 +923,8 @@
1.57 t0 $ aux Ts t1 $ aux Ts t2
1.58 | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
1.59 t
1.60 + else if is_type_enc_higher_order type_enc then
1.61 + t |> Envir.eta_contract
1.62 else
1.63 t |> conceal_bounds Ts
1.64 |> Envir.eta_contract
1.65 @@ -950,8 +964,7 @@
1.66 |> extensionalize_term ctxt
1.67 |> presimplify_term ctxt presimp_consts
1.68 |> perhaps (try (HOLogic.dest_Trueprop))
1.69 - |> not (is_type_enc_higher_order type_enc)
1.70 - ? introduce_combinators_in_term ctxt kind
1.71 + |> process_abstractions_in_term ctxt type_enc kind
1.72 end
1.73
1.74 (* making fact and conjecture formulas *)
1.75 @@ -1140,6 +1153,8 @@
1.76 end)
1.77 end
1.78 | CombVar (_, T) => add_var_or_bound_var T accum
1.79 + | CombAbs ((_, T), tm) =>
1.80 + accum |> add_var_or_bound_var T |> add false tm
1.81 | _ => accum)
1.82 |> fold (add false) args
1.83 end
1.84 @@ -1291,12 +1306,6 @@
1.85 (("COMBB", false), @{thms Meson.COMBB_def}),
1.86 (("COMBC", false), @{thms Meson.COMBC_def}),
1.87 (("COMBS", false), @{thms Meson.COMBS_def}),
1.88 - (("fequal", true),
1.89 - (* This is a lie: Higher-order equality doesn't need a sound type encoding.
1.90 - However, this is done so for backward compatibility: Including the
1.91 - equality helpers by default in Metis breaks a few existing proofs. *)
1.92 - @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1.93 - fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1.94 (("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]),
1.95 (("fFalse", true), @{thms True_or_False}),
1.96 (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]),
1.97 @@ -1313,6 +1322,14 @@
1.98 (("fimplies", false),
1.99 @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
1.100 by (unfold fimplies_def) fast+}),
1.101 + (("fequal", true),
1.102 + (* This is a lie: Higher-order equality doesn't need a sound type encoding.
1.103 + However, this is done so for backward compatibility: Including the
1.104 + equality helpers by default in Metis breaks a few existing proofs. *)
1.105 + @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1.106 + fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1.107 + (("fAll", false), []), (*TODO: add helpers*)
1.108 + (("fEx", false), []), (*TODO: add helpers*)
1.109 (("If", true), @{thms if_True if_False True_or_False})]
1.110 |> map (apsnd (map zero_var_indexes))
1.111
1.112 @@ -1491,7 +1508,7 @@
1.113 in
1.114 mk_aterm format type_enc name T_args (map (aux arg_site) args)
1.115 end
1.116 - | CombVar (name, _) => mk_aterm format type_enc name [] []
1.117 + | CombVar (name, _) => mk_aterm format type_enc name [] (map (aux Elsewhere) args)
1.118 | CombAbs ((name, T), tm) =>
1.119 AAbs ((name, ho_type_from_typ format type_enc true 0 T), aux Elsewhere tm)
1.120 | CombApp _ => raise Fail "impossible \"CombApp\""
1.121 @@ -1635,6 +1652,7 @@
1.122 else
1.123 I
1.124 end
1.125 + | CombAbs (_, tm) => add_combterm in_conj tm
1.126 | _ => I)
1.127 #> fold (add_combterm in_conj) args
1.128 end