--- a/src/HOL/ATP.thy Tue Jul 05 17:09:59 2011 +0100
+++ b/src/HOL/ATP.thy Tue Jul 05 17:09:59 2011 +0100
@@ -39,6 +39,11 @@
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
"fequal x y \<longleftrightarrow> (x = y)"
+definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
+"fAll P \<longleftrightarrow> All P"
+
+definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
+"fEx P \<longleftrightarrow> Ex P"
subsection {* Setup *}
--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jul 05 17:09:59 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jul 05 17:09:59 2011 +0100
@@ -38,7 +38,9 @@
val tptp_fun_type : string
val tptp_product_type : string
val tptp_forall : string
+ val tptp_ho_forall : string
val tptp_exists : string
+ val tptp_ho_exists : string
val tptp_not : string
val tptp_and : string
val tptp_or : string
@@ -125,7 +127,9 @@
val tptp_fun_type = ">"
val tptp_product_type = "*"
val tptp_forall = "!"
+val tptp_ho_forall = "!!"
val tptp_exists = "?"
+val tptp_ho_exists = "??"
val tptp_not = "~"
val tptp_and = "&"
val tptp_or = "|"
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Jul 05 17:09:59 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Jul 05 17:09:59 2011 +0100
@@ -8,7 +8,7 @@
signature ATP_PROOF =
sig
- type 'a fo_term = 'a ATP_Problem.fo_term
+ type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
type 'a problem = 'a ATP_Problem.problem
@@ -41,7 +41,7 @@
Definition of step_name * 'a * 'a |
Inference of step_name * 'a * step_name list
- type 'a proof = ('a, 'a, 'a fo_term) formula step list
+ type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
val short_output : bool -> string -> string
val string_for_failure : failure -> string
@@ -54,7 +54,7 @@
val is_same_atp_step : step_name -> step_name -> bool
val scan_general_id : string list -> string * string list
val parse_formula :
- string list -> (string, 'a, string fo_term) formula * string list
+ string list -> (string, 'a, (string, 'a) ho_term) formula * string list
val atp_proof_from_tstplike_proof :
string problem -> string -> string -> string proof
val clean_up_atp_proof_dependencies : string proof -> string proof
@@ -228,7 +228,7 @@
Definition of step_name * 'a * 'a |
Inference of step_name * 'a * step_name list
-type 'a proof = ('a, 'a, 'a fo_term) formula step list
+type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
fun step_name (Definition (name, _, _)) = name
| step_name (Inference (name, _, _)) = name
@@ -293,7 +293,7 @@
| (u1, SOME (SOME _, u2)) =>
mk_anot (AAtom (ATerm ("equal", [u1, u2]))))) x
-fun fo_term_head (ATerm (s, _)) = s
+fun ho_term_head (ATerm (s, _)) = s
(* TPTP formulas are fully parenthesized, so we don't need to worry about
operator precedence. *)
@@ -325,7 +325,7 @@
--| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal
>> (fn ((q, ts), phi) =>
(* We ignore TFF and THF types for now. *)
- AQuant (q, map (rpair NONE o fo_term_head) ts, phi))) x
+ AQuant (q, map (rpair NONE o ho_term_head) ts, phi))) x
fun skip_formula ss =
let
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Jul 05 17:09:59 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Jul 05 17:09:59 2011 +0100
@@ -8,7 +8,7 @@
signature ATP_RECONSTRUCT =
sig
- type 'a fo_term = 'a ATP_Problem.fo_term
+ type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
type 'a proof = 'a ATP_Proof.proof
type locality = ATP_Translate.locality
@@ -41,11 +41,11 @@
val make_tvar : string -> typ
val make_tfree : Proof.context -> string -> typ
val term_from_atp :
- Proof.context -> bool -> int Symtab.table -> typ option -> string fo_term
+ Proof.context -> bool -> int Symtab.table -> typ option -> (string, string) ho_term
-> term
val prop_from_atp :
Proof.context -> bool -> int Symtab.table
- -> (string, string, string fo_term) formula -> term
+ -> (string, string, (string, string) ho_term) formula -> term
val isar_proof_text :
Proof.context -> bool -> isar_params -> one_line_params -> string
val proof_text :
@@ -304,8 +304,8 @@
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
-exception FO_TERM of string fo_term list
-exception FORMULA of (string, string, string fo_term) formula list
+exception HO_TERM of (string, string) ho_term list
+exception FORMULA of (string, string, (string, string) ho_term) formula list
exception SAME of unit
(* Type variables are given the basic sort "HOL.type". Some will later be
@@ -316,7 +316,7 @@
SOME b => Type (invert_const b, Ts)
| NONE =>
if not (null us) then
- raise FO_TERM [u] (* only "tconst"s have type arguments *)
+ raise HO_TERM [u] (* only "tconst"s have type arguments *)
else case strip_prefix_and_unascii tfree_prefix a of
SOME b => make_tfree ctxt b
| NONE =>
@@ -333,7 +333,7 @@
fun type_constraint_from_term ctxt (u as ATerm (a, us)) =
case (strip_prefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of
(SOME b, [T]) => (b, T)
- | _ => raise FO_TERM [u]
+ | _ => raise HO_TERM [u]
(** Accumulate type constraints in a formula: negative type literals **)
fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
@@ -393,7 +393,7 @@
case mangled_us @ us of
[typ_u, term_u] =>
do_term extra_ts (SOME (typ_from_atp ctxt typ_u)) term_u
- | _ => raise FO_TERM us
+ | _ => raise HO_TERM us
else if s' = predicator_name then
do_term [] (SOME @{typ bool}) (hd us)
else if s' = app_op_name then
--- a/src/HOL/Tools/ATP/atp_translate.ML Tue Jul 05 17:09:59 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Jul 05 17:09:59 2011 +0100
@@ -229,7 +229,11 @@
("c_implies", (@{const_name implies}, (@{thm fimplies_def},
("fimplies", @{const_name ATP.fimplies})))),
("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
- ("fequal", @{const_name ATP.fequal}))))]
+ ("fequal", @{const_name ATP.fequal})))),
+ ("c_All", (@{const_name All}, (@{thm fAll_def},
+ ("fAll", @{const_name ATP.fAll})))),
+ ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
+ ("fEx", @{const_name ATP.fEx}))))]
val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
@@ -245,6 +249,8 @@
(@{const_name disj}, "disj"),
(@{const_name implies}, "implies"),
(@{const_name HOL.eq}, "equal"),
+ (@{const_name All}, "All"),
+ (@{const_name Ex}, "Ex"),
(@{const_name If}, "If"),
(@{const_name Set.member}, "member"),
(@{const_name Meson.COMBI}, "COMBI"),
@@ -493,7 +499,11 @@
nth bs j
|> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
| combterm_from_term thy bs (Abs (s, T, t)) =
- let val (tm, atomic_Ts) = combterm_from_term thy ((s, T) :: bs) t in
+ let
+ fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
+ val s = vary s
+ val (tm, atomic_Ts) = combterm_from_term thy ((s, T) :: bs) t
+ in
(CombAbs ((`make_bound_var s, T), tm),
union (op =) atomic_Ts (atyps_of T))
end
@@ -817,6 +827,8 @@
| (false, "c_conj") => (`I tptp_and, [])
| (false, "c_disj") => (`I tptp_or, [])
| (false, "c_implies") => (`I tptp_implies, [])
+ | (false, "c_All") => (`I tptp_ho_forall, [])
+ | (false, "c_Ex") => (`I tptp_ho_exists, [])
| (false, s) =>
if is_tptp_equal s then (`I tptp_equal, [])
else (proxy_base |>> prefix const_prefix, T_args)
@@ -886,7 +898,7 @@
else
t
-fun introduce_combinators_in_term ctxt kind t =
+fun process_abstractions_in_term ctxt type_enc kind t =
let val thy = Proof_Context.theory_of ctxt in
if Meson.is_fol_term thy t then
t
@@ -911,6 +923,8 @@
t0 $ aux Ts t1 $ aux Ts t2
| _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
t
+ else if is_type_enc_higher_order type_enc then
+ t |> Envir.eta_contract
else
t |> conceal_bounds Ts
|> Envir.eta_contract
@@ -950,8 +964,7 @@
|> extensionalize_term ctxt
|> presimplify_term ctxt presimp_consts
|> perhaps (try (HOLogic.dest_Trueprop))
- |> not (is_type_enc_higher_order type_enc)
- ? introduce_combinators_in_term ctxt kind
+ |> process_abstractions_in_term ctxt type_enc kind
end
(* making fact and conjecture formulas *)
@@ -1140,6 +1153,8 @@
end)
end
| CombVar (_, T) => add_var_or_bound_var T accum
+ | CombAbs ((_, T), tm) =>
+ accum |> add_var_or_bound_var T |> add false tm
| _ => accum)
|> fold (add false) args
end
@@ -1291,12 +1306,6 @@
(("COMBB", false), @{thms Meson.COMBB_def}),
(("COMBC", false), @{thms Meson.COMBC_def}),
(("COMBS", false), @{thms Meson.COMBS_def}),
- (("fequal", true),
- (* This is a lie: Higher-order equality doesn't need a sound type encoding.
- However, this is done so for backward compatibility: Including the
- equality helpers by default in Metis breaks a few existing proofs. *)
- @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
- fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
(("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]),
(("fFalse", true), @{thms True_or_False}),
(("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]),
@@ -1313,6 +1322,14 @@
(("fimplies", false),
@{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
by (unfold fimplies_def) fast+}),
+ (("fequal", true),
+ (* This is a lie: Higher-order equality doesn't need a sound type encoding.
+ However, this is done so for backward compatibility: Including the
+ equality helpers by default in Metis breaks a few existing proofs. *)
+ @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
+ fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
+ (("fAll", false), []), (*TODO: add helpers*)
+ (("fEx", false), []), (*TODO: add helpers*)
(("If", true), @{thms if_True if_False True_or_False})]
|> map (apsnd (map zero_var_indexes))
@@ -1491,7 +1508,7 @@
in
mk_aterm format type_enc name T_args (map (aux arg_site) args)
end
- | CombVar (name, _) => mk_aterm format type_enc name [] []
+ | CombVar (name, _) => mk_aterm format type_enc name [] (map (aux Elsewhere) args)
| CombAbs ((name, T), tm) =>
AAbs ((name, ho_type_from_typ format type_enc true 0 T), aux Elsewhere tm)
| CombApp _ => raise Fail "impossible \"CombApp\""
@@ -1635,6 +1652,7 @@
else
I
end
+ | CombAbs (_, tm) => add_combterm in_conj tm
| _ => I)
#> fold (add_combterm in_conj) args
end