1.1 --- a/src/HOL/ATP.thy	Tue Jul 05 17:09:59 2011 +0100
     1.2 +++ b/src/HOL/ATP.thy	Tue Jul 05 17:09:59 2011 +0100
     1.3 @@ -39,6 +39,11 @@
     1.4  definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
     1.5  "fequal x y \<longleftrightarrow> (x = y)"
     1.6  
     1.7 +definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
     1.8 +"fAll P \<longleftrightarrow> All P"
     1.9 +
    1.10 +definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
    1.11 +"fEx P \<longleftrightarrow> Ex P"
    1.12  
    1.13  subsection {* Setup *}
    1.14  

     2.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Jul 05 17:09:59 2011 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Jul 05 17:09:59 2011 +0100
     2.3 @@ -38,7 +38,9 @@
     2.4    val tptp_fun_type : string
     2.5    val tptp_product_type : string
     2.6    val tptp_forall : string
     2.7 +  val tptp_ho_forall : string
     2.8    val tptp_exists : string
     2.9 +  val tptp_ho_exists : string
    2.10    val tptp_not : string
    2.11    val tptp_and : string
    2.12    val tptp_or : string
    2.13 @@ -125,7 +127,9 @@
    2.14  val tptp_fun_type = ">"
    2.15  val tptp_product_type = "*"
    2.16  val tptp_forall = "!"
    2.17 +val tptp_ho_forall = "!!"
    2.18  val tptp_exists = "?"
    2.19 +val tptp_ho_exists = "??"
    2.20  val tptp_not = "~"
    2.21  val tptp_and = "&"
    2.22  val tptp_or = "|"

     3.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Jul 05 17:09:59 2011 +0100
     3.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Jul 05 17:09:59 2011 +0100
     3.3 @@ -8,7 +8,7 @@
     3.4  
     3.5  signature ATP_PROOF =
     3.6  sig
     3.7 -  type 'a fo_term = 'a ATP_Problem.fo_term
     3.8 +  type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
     3.9    type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
    3.10    type 'a problem = 'a ATP_Problem.problem
    3.11  
    3.12 @@ -41,7 +41,7 @@
    3.13      Definition of step_name * 'a * 'a |
    3.14      Inference of step_name * 'a * step_name list
    3.15  
    3.16 -  type 'a proof = ('a, 'a, 'a fo_term) formula step list
    3.17 +  type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
    3.18  
    3.19    val short_output : bool -> string -> string
    3.20    val string_for_failure : failure -> string
    3.21 @@ -54,7 +54,7 @@
    3.22    val is_same_atp_step : step_name -> step_name -> bool
    3.23    val scan_general_id : string list -> string * string list
    3.24    val parse_formula :
    3.25 -    string list -> (string, 'a, string fo_term) formula * string list
    3.26 +    string list -> (string, 'a, (string, 'a) ho_term) formula * string list
    3.27    val atp_proof_from_tstplike_proof :
    3.28      string problem -> string -> string -> string proof
    3.29    val clean_up_atp_proof_dependencies : string proof -> string proof
    3.30 @@ -228,7 +228,7 @@
    3.31    Definition of step_name * 'a * 'a |
    3.32    Inference of step_name * 'a * step_name list
    3.33  
    3.34 -type 'a proof = ('a, 'a, 'a fo_term) formula step list
    3.35 +type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
    3.36  
    3.37  fun step_name (Definition (name, _, _)) = name
    3.38    | step_name (Inference (name, _, _)) = name
    3.39 @@ -293,7 +293,7 @@
    3.40          | (u1, SOME (SOME _, u2)) =>
    3.41            mk_anot (AAtom (ATerm ("equal", [u1, u2]))))) x
    3.42  
    3.43 -fun fo_term_head (ATerm (s, _)) = s
    3.44 +fun ho_term_head (ATerm (s, _)) = s
    3.45  
    3.46  (* TPTP formulas are fully parenthesized, so we don't need to worry about
    3.47     operator precedence. *)
    3.48 @@ -325,7 +325,7 @@
    3.49     --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal
    3.50     >> (fn ((q, ts), phi) =>
    3.51            (* We ignore TFF and THF types for now. *)
    3.52 -          AQuant (q, map (rpair NONE o fo_term_head) ts, phi))) x
    3.53 +          AQuant (q, map (rpair NONE o ho_term_head) ts, phi))) x
    3.54  
    3.55  fun skip_formula ss =
    3.56    let

     4.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue Jul 05 17:09:59 2011 +0100
     4.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue Jul 05 17:09:59 2011 +0100
     4.3 @@ -8,7 +8,7 @@
     4.4  
     4.5  signature ATP_RECONSTRUCT =
     4.6  sig
     4.7 -  type 'a fo_term = 'a ATP_Problem.fo_term
     4.8 +  type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
     4.9    type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
    4.10    type 'a proof = 'a ATP_Proof.proof
    4.11    type locality = ATP_Translate.locality
    4.12 @@ -41,11 +41,11 @@
    4.13    val make_tvar : string -> typ
    4.14    val make_tfree : Proof.context -> string -> typ
    4.15    val term_from_atp :
    4.16 -    Proof.context -> bool -> int Symtab.table -> typ option -> string fo_term
    4.17 +    Proof.context -> bool -> int Symtab.table -> typ option -> (string, string) ho_term
    4.18      -> term
    4.19    val prop_from_atp :
    4.20      Proof.context -> bool -> int Symtab.table
    4.21 -    -> (string, string, string fo_term) formula -> term
    4.22 +    -> (string, string, (string, string) ho_term) formula -> term
    4.23    val isar_proof_text :
    4.24      Proof.context -> bool -> isar_params -> one_line_params -> string
    4.25    val proof_text :
    4.26 @@ -304,8 +304,8 @@
    4.27  
    4.28  (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
    4.29  
    4.30 -exception FO_TERM of string fo_term list
    4.31 -exception FORMULA of (string, string, string fo_term) formula list
    4.32 +exception HO_TERM of (string, string) ho_term list
    4.33 +exception FORMULA of (string, string, (string, string) ho_term) formula list
    4.34  exception SAME of unit
    4.35  
    4.36  (* Type variables are given the basic sort "HOL.type". Some will later be
    4.37 @@ -316,7 +316,7 @@
    4.38        SOME b => Type (invert_const b, Ts)
    4.39      | NONE =>
    4.40        if not (null us) then
    4.41 -        raise FO_TERM [u]  (* only "tconst"s have type arguments *)
    4.42 +        raise HO_TERM [u]  (* only "tconst"s have type arguments *)
    4.43        else case strip_prefix_and_unascii tfree_prefix a of
    4.44          SOME b => make_tfree ctxt b
    4.45        | NONE =>
    4.46 @@ -333,7 +333,7 @@
    4.47  fun type_constraint_from_term ctxt (u as ATerm (a, us)) =
    4.48    case (strip_prefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of
    4.49      (SOME b, [T]) => (b, T)
    4.50 -  | _ => raise FO_TERM [u]
    4.51 +  | _ => raise HO_TERM [u]
    4.52  
    4.53  (** Accumulate type constraints in a formula: negative type literals **)
    4.54  fun add_var (key, z)  = Vartab.map_default (key, []) (cons z)
    4.55 @@ -393,7 +393,7 @@
    4.56                case mangled_us @ us of
    4.57                  [typ_u, term_u] =>
    4.58                  do_term extra_ts (SOME (typ_from_atp ctxt typ_u)) term_u
    4.59 -              | _ => raise FO_TERM us
    4.60 +              | _ => raise HO_TERM us
    4.61              else if s' = predicator_name then
    4.62                do_term [] (SOME @{typ bool}) (hd us)
    4.63              else if s' = app_op_name then

     5.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 05 17:09:59 2011 +0100
     5.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 05 17:09:59 2011 +0100
     5.3 @@ -229,7 +229,11 @@
     5.4     ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
     5.5         ("fimplies", @{const_name ATP.fimplies})))),
     5.6     ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
     5.7 -       ("fequal", @{const_name ATP.fequal}))))]
     5.8 +       ("fequal", @{const_name ATP.fequal})))),
     5.9 +   ("c_All", (@{const_name All}, (@{thm fAll_def},
    5.10 +       ("fAll", @{const_name ATP.fAll})))),
    5.11 +   ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
    5.12 +       ("fEx", @{const_name ATP.fEx}))))]
    5.13  
    5.14  val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
    5.15  
    5.16 @@ -245,6 +249,8 @@
    5.17     (@{const_name disj}, "disj"),
    5.18     (@{const_name implies}, "implies"),
    5.19     (@{const_name HOL.eq}, "equal"),
    5.20 +   (@{const_name All}, "All"),
    5.21 +   (@{const_name Ex}, "Ex"),
    5.22     (@{const_name If}, "If"),
    5.23     (@{const_name Set.member}, "member"),
    5.24     (@{const_name Meson.COMBI}, "COMBI"),
    5.25 @@ -493,7 +499,11 @@
    5.26      nth bs j
    5.27      |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
    5.28    | combterm_from_term thy bs (Abs (s, T, t)) =
    5.29 -    let val (tm, atomic_Ts) = combterm_from_term thy ((s, T) :: bs) t in
    5.30 +    let
    5.31 +      fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
    5.32 +      val s = vary s
    5.33 +      val (tm, atomic_Ts) = combterm_from_term thy ((s, T) :: bs) t
    5.34 +    in
    5.35        (CombAbs ((`make_bound_var s, T), tm),
    5.36         union (op =) atomic_Ts (atyps_of T))
    5.37      end
    5.38 @@ -817,6 +827,8 @@
    5.39               | (false, "c_conj") => (`I tptp_and, [])
    5.40               | (false, "c_disj") => (`I tptp_or, [])
    5.41               | (false, "c_implies") => (`I tptp_implies, [])
    5.42 +             | (false, "c_All") => (`I tptp_ho_forall, [])
    5.43 +             | (false, "c_Ex") => (`I tptp_ho_exists, [])
    5.44               | (false, s) =>
    5.45                 if is_tptp_equal s then (`I tptp_equal, [])
    5.46                 else (proxy_base |>> prefix const_prefix, T_args)
    5.47 @@ -886,7 +898,7 @@
    5.48    else
    5.49      t
    5.50  
    5.51 -fun introduce_combinators_in_term ctxt kind t =
    5.52 +fun process_abstractions_in_term ctxt type_enc kind t =
    5.53    let val thy = Proof_Context.theory_of ctxt in
    5.54      if Meson.is_fol_term thy t then
    5.55        t
    5.56 @@ -911,6 +923,8 @@
    5.57              t0 $ aux Ts t1 $ aux Ts t2
    5.58            | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
    5.59                     t
    5.60 +                 else if is_type_enc_higher_order type_enc then
    5.61 +                   t |> Envir.eta_contract
    5.62                   else
    5.63                     t |> conceal_bounds Ts
    5.64                       |> Envir.eta_contract
    5.65 @@ -950,8 +964,7 @@
    5.66        |> extensionalize_term ctxt
    5.67        |> presimplify_term ctxt presimp_consts
    5.68        |> perhaps (try (HOLogic.dest_Trueprop))
    5.69 -      |> not (is_type_enc_higher_order type_enc)
    5.70 -         ? introduce_combinators_in_term ctxt kind
    5.71 +      |> process_abstractions_in_term ctxt type_enc kind
    5.72    end
    5.73  
    5.74  (* making fact and conjecture formulas *)
    5.75 @@ -1140,6 +1153,8 @@
    5.76                    end)
    5.77               end
    5.78           | CombVar (_, T) => add_var_or_bound_var T accum
    5.79 +         | CombAbs ((_, T), tm) =>
    5.80 +           accum |> add_var_or_bound_var T |> add false tm
    5.81           | _ => accum)
    5.82          |> fold (add false) args
    5.83        end
    5.84 @@ -1291,12 +1306,6 @@
    5.85     (("COMBB", false), @{thms Meson.COMBB_def}),
    5.86     (("COMBC", false), @{thms Meson.COMBC_def}),
    5.87     (("COMBS", false), @{thms Meson.COMBS_def}),
    5.88 -   (("fequal", true),
    5.89 -    (* This is a lie: Higher-order equality doesn't need a sound type encoding.
    5.90 -       However, this is done so for backward compatibility: Including the
    5.91 -       equality helpers by default in Metis breaks a few existing proofs. *)
    5.92 -    @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
    5.93 -           fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
    5.94     (("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]),
    5.95     (("fFalse", true), @{thms True_or_False}),
    5.96     (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]),
    5.97 @@ -1313,6 +1322,14 @@
    5.98     (("fimplies", false),
    5.99      @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
   5.100          by (unfold fimplies_def) fast+}),
   5.101 +   (("fequal", true),
   5.102 +    (* This is a lie: Higher-order equality doesn't need a sound type encoding.
   5.103 +       However, this is done so for backward compatibility: Including the
   5.104 +       equality helpers by default in Metis breaks a few existing proofs. *)
   5.105 +    @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
   5.106 +           fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
   5.107 +   (("fAll", false), []), (*TODO: add helpers*)
   5.108 +   (("fEx", false), []), (*TODO: add helpers*)
   5.109     (("If", true), @{thms if_True if_False True_or_False})]
   5.110    |> map (apsnd (map zero_var_indexes))
   5.111  
   5.112 @@ -1491,7 +1508,7 @@
   5.113              in
   5.114                mk_aterm format type_enc name T_args (map (aux arg_site) args)
   5.115              end
   5.116 -          | CombVar (name, _) => mk_aterm format type_enc name [] []
   5.117 +          | CombVar (name, _) => mk_aterm format type_enc name [] (map (aux Elsewhere) args)
   5.118            | CombAbs ((name, T), tm) =>
   5.119              AAbs ((name, ho_type_from_typ format type_enc true 0 T), aux Elsewhere tm)
   5.120            | CombApp _ => raise Fail "impossible \"CombApp\""
   5.121 @@ -1635,6 +1652,7 @@
   5.122               else
   5.123                 I
   5.124             end
   5.125 +         | CombAbs (_, tm) => add_combterm in_conj tm
   5.126           | _ => I)
   5.127          #> fold (add_combterm in_conj) args
   5.128        end