# HG changeset patch
# User nik
# Date 1309882199 -3600
# Node ID 56d352659500ab0d04e32ebc9f90ec8a263ca924
# Parent  2cd0b478d1b683c1be3aab71714ef57c11ff9277
improved translation of lambdas in THF

diff -r 2cd0b478d1b6 -r 56d352659500 src/HOL/ATP.thy
--- 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 *}
 
diff -r 2cd0b478d1b6 -r 56d352659500 src/HOL/Tools/ATP/atp_problem.ML
--- 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 = "|"
diff -r 2cd0b478d1b6 -r 56d352659500 src/HOL/Tools/ATP/atp_proof.ML
--- 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
diff -r 2cd0b478d1b6 -r 56d352659500 src/HOL/Tools/ATP/atp_reconstruct.ML
--- 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
diff -r 2cd0b478d1b6 -r 56d352659500 src/HOL/Tools/ATP/atp_translate.ML
--- 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