1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:35 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:12:45 2011 +0200
1.3 @@ -3,7 +3,7 @@
1.4 Author: Makarius
1.5 Author: Jasmin Blanchette, TU Muenchen
1.6
1.7 -Translation of HOL to FOL for Sledgehammer.
1.8 +Translation of HOL to FOL for Metis and Sledgehammer.
1.9 *)
1.10
1.11 signature ATP_TRANSLATE =
1.12 @@ -92,8 +92,8 @@
1.13 val introduce_combinators : Proof.context -> term -> term
1.14 val prepare_atp_problem :
1.15 Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
1.16 - -> bool -> ((formula_kind * term) list -> term list) -> bool -> bool
1.17 - -> term list -> term -> ((string * locality) * term) list
1.18 + -> bool -> (term list -> term list * term list) -> bool -> bool -> term list
1.19 + -> term -> ((string * locality) * term) list
1.20 -> string problem * string Symtab.table * int * int
1.21 * (string * locality) list vector * int list * int Symtab.table
1.22 val atp_problem_weights : string problem -> (string * real) list
1.23 @@ -120,15 +120,13 @@
1.24 val bound_var_prefix = "B_"
1.25 val schematic_var_prefix = "V_"
1.26 val fixed_var_prefix = "v_"
1.27 -
1.28 val tvar_prefix = "T_"
1.29 val tfree_prefix = "t_"
1.30 -
1.31 val const_prefix = "c_"
1.32 val type_const_prefix = "tc_"
1.33 val class_prefix = "cl_"
1.34
1.35 -val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
1.36 +val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
1.37 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
1.38 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
1.39
1.40 @@ -143,6 +141,7 @@
1.41 val arity_clause_prefix = "arity_"
1.42 val tfree_clause_prefix = "tfree_"
1.43
1.44 +val lambda_fact_prefix = "ATP.lambda_"
1.45 val typed_helper_suffix = "_T"
1.46 val untyped_helper_suffix = "_U"
1.47 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
1.48 @@ -158,9 +157,9 @@
1.49 val prefixed_type_tag_name = const_prefix ^ type_tag_name
1.50
1.51 (* Freshness almost guaranteed! *)
1.52 -val sledgehammer_weak_prefix = "Sledgehammer:"
1.53 +val atp_weak_prefix = "ATP:"
1.54
1.55 -val concealed_lambda_prefix = sledgehammer_weak_prefix ^ "lambda_"
1.56 +val concealed_lambda_prefix = atp_weak_prefix ^ "lambda_"
1.57
1.58 (*Escaping of special characters.
1.59 Alphanumeric characters are left unchanged.
1.60 @@ -879,7 +878,7 @@
1.61 #> Meson.presimplify ctxt
1.62 #> prop_of)
1.63
1.64 -fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
1.65 +fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
1.66 fun conceal_bounds Ts t =
1.67 subst_bounds (map (Free o apfst concealed_bound_name)
1.68 (0 upto length Ts - 1 ~~ Ts), t)
1.69 @@ -901,29 +900,34 @@
1.70 t
1.71
1.72 fun simple_translate_lambdas do_lambdas ctxt t =
1.73 - let
1.74 - fun aux Ts t =
1.75 - case t of
1.76 - @{const Not} $ t1 => @{const Not} $ aux Ts t1
1.77 - | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
1.78 - t0 $ Abs (s, T, aux (T :: Ts) t')
1.79 - | (t0 as Const (@{const_name All}, _)) $ t1 =>
1.80 - aux Ts (t0 $ eta_expand Ts t1 1)
1.81 - | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
1.82 - t0 $ Abs (s, T, aux (T :: Ts) t')
1.83 - | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
1.84 - aux Ts (t0 $ eta_expand Ts t1 1)
1.85 - | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
1.86 - | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
1.87 - | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
1.88 - | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
1.89 - $ t1 $ t2 =>
1.90 - t0 $ aux Ts t1 $ aux Ts t2
1.91 - | _ =>
1.92 - if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
1.93 - else t |> Envir.eta_contract |> do_lambdas ctxt Ts
1.94 - val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
1.95 - in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
1.96 + let val thy = Proof_Context.theory_of ctxt in
1.97 + if Meson.is_fol_term thy t then
1.98 + t
1.99 + else
1.100 + let
1.101 + fun aux Ts t =
1.102 + case t of
1.103 + @{const Not} $ t1 => @{const Not} $ aux Ts t1
1.104 + | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
1.105 + t0 $ Abs (s, T, aux (T :: Ts) t')
1.106 + | (t0 as Const (@{const_name All}, _)) $ t1 =>
1.107 + aux Ts (t0 $ eta_expand Ts t1 1)
1.108 + | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
1.109 + t0 $ Abs (s, T, aux (T :: Ts) t')
1.110 + | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
1.111 + aux Ts (t0 $ eta_expand Ts t1 1)
1.112 + | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
1.113 + | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
1.114 + | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
1.115 + | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
1.116 + $ t1 $ t2 =>
1.117 + t0 $ aux Ts t1 $ aux Ts t2
1.118 + | _ =>
1.119 + if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
1.120 + else t |> Envir.eta_contract |> do_lambdas ctxt Ts
1.121 + val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
1.122 + in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
1.123 + end
1.124
1.125 fun do_conceal_lambdas Ts (t1 $ t2) =
1.126 do_conceal_lambdas Ts t1 $ do_conceal_lambdas Ts t2
1.127 @@ -946,11 +950,16 @@
1.128 handle THM _ => do_conceal_lambdas Ts t
1.129 val introduce_combinators = simple_translate_lambdas do_introduce_combinators
1.130
1.131 -fun process_abstractions_in_terms ctxt trans_lambdas ps =
1.132 +fun preprocess_abstractions_in_terms ctxt trans_lambdas facts =
1.133 let
1.134 - val thy = Proof_Context.theory_of ctxt
1.135 - val (fo_ps, ho_ps) = ps |> List.partition (Meson.is_fol_term thy o snd)
1.136 - in map snd fo_ps @ trans_lambdas ho_ps end
1.137 + val (facts, lambda_ts) =
1.138 + facts |> map (snd o snd) |> trans_lambdas
1.139 + |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
1.140 + val lambda_facts =
1.141 + map2 (fn t => fn j =>
1.142 + ((lambda_fact_prefix ^ Int.toString j, Helper), (Axiom, t)))
1.143 + lambda_ts (1 upto length lambda_ts)
1.144 + in (facts, lambda_facts) end
1.145
1.146 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
1.147 same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
1.148 @@ -959,11 +968,11 @@
1.149 fun aux (t $ u) = aux t $ aux u
1.150 | aux (Abs (s, T, t)) = Abs (s, T, aux t)
1.151 | aux (Var ((s, i), T)) =
1.152 - Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
1.153 + Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
1.154 | aux t = t
1.155 in t |> exists_subterm is_Var t ? aux end
1.156
1.157 -fun preprocess_prop ctxt presimp_consts t =
1.158 +fun presimp_prop ctxt presimp_consts t =
1.159 let
1.160 val thy = Proof_Context.theory_of ctxt
1.161 val t = t |> Envir.beta_eta_contract
1.162 @@ -1002,9 +1011,8 @@
1.163 val thy = Proof_Context.theory_of ctxt
1.164 val last = length ps - 1
1.165 in
1.166 - map2 (fn j => fn (kind, t) =>
1.167 - t |> make_formula thy type_enc (format <> CNF) (string_of_int j)
1.168 - Local kind
1.169 + map2 (fn j => fn ((name, loc), (kind, t)) =>
1.170 + t |> make_formula thy type_enc (format <> CNF) name loc kind
1.171 |> (j <> last) = (kind = Conjecture) ? update_iformula mk_anot)
1.172 (0 upto last) ps
1.173 end
1.174 @@ -1426,29 +1434,32 @@
1.175 let
1.176 val thy = Proof_Context.theory_of ctxt
1.177 val presimp_consts = Meson.presimplified_consts ctxt
1.178 - fun preprocess kind =
1.179 - preprocess_prop ctxt presimp_consts
1.180 - #> pair kind #> single
1.181 - #> process_abstractions_in_terms ctxt trans_lambdas
1.182 - #> the_single
1.183 val fact_ts = facts |> map snd
1.184 (* Remove existing facts from the conjecture, as this can dramatically
1.185 boost an ATP's performance (for some reason). *)
1.186 val hyp_ts =
1.187 hyp_ts
1.188 |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
1.189 - val fact_ts = facts |> map snd |> preproc ? map (preprocess Axiom)
1.190 + val fact_ps = facts |> map (apsnd (pair Axiom))
1.191 val conj_ps =
1.192 map (pair prem_kind) hyp_ts @ [(Conjecture, concl_t)]
1.193 - |> preproc
1.194 - ? map (fn (kind, t) => (kind, t |> preprocess kind |> freeze_term))
1.195 - val (facts, fact_names) =
1.196 - map2 (fn (name, _) => fn t =>
1.197 - (make_fact ctxt format type_enc true (name, t), name))
1.198 - facts fact_ts
1.199 - |> map_filter (try (apfst the))
1.200 + |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
1.201 + val ((conj_ps, fact_ps), lambda_ps) =
1.202 + conj_ps @ fact_ps
1.203 + |> map (apsnd (apsnd (presimp_prop ctxt presimp_consts)))
1.204 + |> (if preproc then preprocess_abstractions_in_terms ctxt trans_lambdas
1.205 + else rpair [])
1.206 + |>> chop (length conj_ps)
1.207 + |>> preproc ? apfst (map (apsnd (apsnd freeze_term)))
1.208 + val conjs = make_conjecture ctxt format type_enc conj_ps
1.209 + val (fact_names, facts) =
1.210 + fact_ps
1.211 + |> map_filter (fn (name, (_, t)) =>
1.212 + make_fact ctxt format type_enc true (name, t)
1.213 + |> Option.map (pair name))
1.214 |> ListPair.unzip
1.215 - val conjs = make_conjecture ctxt format type_enc conj_ps
1.216 + val lambdas =
1.217 + lambda_ps |> map_filter (make_fact ctxt format type_enc false o apsnd snd)
1.218 val all_ts = concl_t :: hyp_ts @ fact_ts
1.219 val subs = tfree_classes_of_terms all_ts
1.220 val supers = tvar_classes_of_terms all_ts
1.221 @@ -1458,7 +1469,8 @@
1.222 else make_arity_clauses thy tycons supers
1.223 val class_rel_clauses = make_class_rel_clauses thy subs supers
1.224 in
1.225 - (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
1.226 + (fact_names |> map single,
1.227 + (conjs, facts @ lambdas, class_rel_clauses, arity_clauses))
1.228 end
1.229
1.230 fun fo_literal_from_type_literal (TyLitVar (class, name)) =