--- a/src/HOL/Tools/Sledgehammer/meson_clausifier.ML Wed Sep 29 17:59:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_clausifier.ML Wed Sep 29 22:23:27 2010 +0200
@@ -7,11 +7,12 @@
signature MESON_CLAUSIFIER =
sig
+ val new_skolemizer : bool Config.T
val extensionalize_theorem : thm -> thm
val introduce_combinators_in_cterm : cterm -> thm
val introduce_combinators_in_theorem : thm -> thm
val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
- val meson_cnf_axiom : theory -> thm -> thm list
+ val cnf_axiom : theory -> thm -> thm list
val meson_general_tac : Proof.context -> thm list -> int -> tactic
val setup: theory -> theory
end;
@@ -19,6 +20,9 @@
structure Meson_Clausifier : MESON_CLAUSIFIER =
struct
+val (new_skolemizer, new_skolemizer_setup) =
+ Attrib.config_bool "meson_new_skolemizer" (K false)
+
(**** Transformation of Elimination Rules into First-Order Formulas****)
val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
@@ -39,7 +43,7 @@
(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
-fun mk_skolem t =
+fun mk_old_skolem_term_wrapper t =
let val T = fastype_of t in
Const (@{const_name skolem}, T --> T) $ t
end
@@ -49,7 +53,7 @@
| beta_eta_under_lambdas t = Envir.beta_eta_contract t
(*Traverse a theorem, accumulating Skolem function definitions.*)
-fun assume_skolem_funs th =
+fun old_skolem_defs th =
let
fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss =
(*Existential: declare a Skolem function, then insert into body and continue*)
@@ -59,7 +63,7 @@
val rhs =
list_abs_free (map dest_Free args,
HOLogic.choice_const T $ beta_eta_under_lambdas body)
- |> mk_skolem
+ |> mk_old_skolem_term_wrapper
val comb = list_comb (rhs, args)
in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
| dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
@@ -190,7 +194,7 @@
(* Given the definition of a Skolem function, return a theorem to replace
an existential formula by a use of that function.
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
-fun skolem_theorem_of_def thy rhs0 =
+fun old_skolem_theorem_from_def thy rhs0 =
let
val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
val rhs' = rhs |> Thm.dest_comb |> snd
@@ -199,7 +203,8 @@
val T =
case hilbert of
Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
- | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [hilbert])
+ | _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"",
+ [hilbert])
val cex = cterm_of thy (HOLogic.exists_const T)
val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
val conc =
@@ -217,7 +222,7 @@
(* Converts an Isabelle theorem (intro, elim or simp format, even higher-order)
into NNF. *)
-fun to_nnf th ctxt0 =
+fun nnf_axiom th ctxt0 =
let
val th1 = th |> transform_elim_theorem |> zero_var_indexes
val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
@@ -234,13 +239,13 @@
in Thm.equal_elim eqth th end
(* Convert a theorem to CNF, with Skolem functions as additional premises. *)
-fun meson_cnf_axiom thy th =
+fun cnf_axiom thy th =
let
val ctxt0 = Variable.global_thm_context th
- val (nnf_th, ctxt) = to_nnf th ctxt0
+ val (nnf_th, ctxt) = nnf_axiom th ctxt0
fun aux th =
- Meson.make_cnf (map (skolem_theorem_of_def thy) (assume_skolem_funs th))
- th ctxt
+ Meson.make_cnf (map (old_skolem_theorem_from_def thy)
+ (old_skolem_defs th)) th ctxt
val (cnf_ths, ctxt) =
aux nnf_th
|> (fn ([], _) => aux (to_definitional_cnf_with_quantifiers thy nnf_th)
@@ -257,7 +262,7 @@
let
val thy = ProofContext.theory_of ctxt
val ctxt0 = Classical.put_claset HOL_cs ctxt
- in Meson.meson_tac ctxt0 (maps (meson_cnf_axiom thy) ths) end
+ in Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) end
val setup =
Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
--- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Wed Sep 29 17:59:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Wed Sep 29 22:23:27 2010 +0200
@@ -114,13 +114,18 @@
| applic_to_tt (a,ts) =
case strip_prefix_and_unascii const_prefix a of
SOME b =>
- let val c = smart_invert_const b
- val ntypes = num_type_args thy c
- val nterms = length ts - ntypes
- val tts = map tm_to_tt ts
- val tys = types_of (List.take(tts,ntypes))
+ let
+ val c = smart_invert_const b
+ val ntypes = num_type_args thy c
+ val nterms = length ts - ntypes
+ val tts = map tm_to_tt ts
+ val tys = types_of (List.take(tts,ntypes))
+ val t = if String.isPrefix new_skolem_prefix c then
+ Var (new_skolem_var_from_const c, tl tys ---> hd tys)
+ else
+ Const (c, dummyT)
in if length tys = ntypes then
- apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
+ apply_list t nterms (List.drop(tts,ntypes))
else
raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
" but gets " ^ Int.toString (length tys) ^
@@ -187,11 +192,12 @@
fun hol_term_from_metis FT = hol_term_from_metis_FT
| hol_term_from_metis _ = hol_term_from_metis_PT
-fun hol_terms_from_fol ctxt mode skolems fol_tms =
+fun hol_terms_from_fol ctxt mode old_skolems fol_tms =
let val ts = map (hol_term_from_metis mode ctxt) fol_tms
val _ = trace_msg (fn () => " calling type inference:")
val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
- val ts' = ts |> map (reveal_skolem_terms skolems) |> infer_types ctxt
+ val ts' = ts |> map (reveal_old_skolem_terms old_skolems)
+ |> infer_types ctxt
val _ = app (fn t => trace_msg
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
" of type " ^ Syntax.string_of_typ ctxt (type_of t)))
@@ -232,24 +238,24 @@
val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
in cterm_instantiate substs th end;
-fun assume_inf ctxt mode skolems atm =
+fun assume_inf ctxt mode old_skolems atm =
inst_excluded_middle
(ProofContext.theory_of ctxt)
- (singleton (hol_terms_from_fol ctxt mode skolems) (Metis_Term.Fn atm))
+ (singleton (hol_terms_from_fol ctxt mode old_skolems) (Metis_Term.Fn atm))
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
to reconstruct them admits new possibilities of errors, e.g. concerning
sorts. Instead we try to arrange that new TVars are distinct and that types
can be inferred from terms. *)
-fun inst_inf ctxt mode skolems thpairs fsubst th =
+fun inst_inf ctxt mode old_skolems thpairs fsubst th =
let val thy = ProofContext.theory_of ctxt
val i_th = lookth thpairs th
val i_th_vars = Term.add_vars (prop_of i_th) []
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
fun subst_translation (x,y) =
let val v = find_var x
- (* We call "reveal_skolem_terms" and "infer_types" below. *)
+ (* We call "reveal_old_skolem_terms" and "infer_types" below. *)
val t = hol_term_from_metis mode ctxt y
in SOME (cterm_of thy (Var v), t) end
handle Option.Option =>
@@ -269,7 +275,8 @@
val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
- val tms = rawtms |> map (reveal_skolem_terms skolems) |> infer_types ctxt
+ val tms = rawtms |> map (reveal_old_skolem_terms old_skolems)
+ |> infer_types ctxt
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
val substs' = ListPair.zip (vars, map ctm_of tms)
val _ = trace_msg (fn () =>
@@ -344,7 +351,7 @@
get (n+1) xs
in get 1 end
-fun resolve_inf ctxt mode skolems thpairs atm th1 th2 =
+fun resolve_inf ctxt mode old_skolems thpairs atm th1 th2 =
let
val thy = ProofContext.theory_of ctxt
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
@@ -358,7 +365,7 @@
i_th1
else
let
- val i_atm = singleton (hol_terms_from_fol ctxt mode skolems)
+ val i_atm = singleton (hol_terms_from_fol ctxt mode old_skolems)
(Metis_Term.Fn atm)
val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
val prems_th1 = prems_of i_th1
@@ -382,9 +389,9 @@
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
-fun refl_inf ctxt mode skolems t =
+fun refl_inf ctxt mode old_skolems t =
let val thy = ProofContext.theory_of ctxt
- val i_t = singleton (hol_terms_from_fol ctxt mode skolems) t
+ val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t
val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
@@ -400,10 +407,10 @@
| get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
| get_ty_arg_size _ _ = 0;
-fun equality_inf ctxt mode skolems (pos, atm) fp fr =
+fun equality_inf ctxt mode old_skolems (pos, atm) fp fr =
let val thy = ProofContext.theory_of ctxt
val m_tm = Metis_Term.Fn atm
- val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolems [m_tm, fr]
+ val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr]
val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
fun replace_item_list lx 0 (_::ls) = lx::ls
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
@@ -482,33 +489,29 @@
val factor = Seq.hd o distinct_subgoals_tac;
-fun step ctxt mode skolems thpairs p =
+fun step ctxt mode old_skolems thpairs p =
case p of
(fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
- | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolems f_atm
+ | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode old_skolems f_atm
| (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
- factor (inst_inf ctxt mode skolems thpairs f_subst f_th1)
+ factor (inst_inf ctxt mode old_skolems thpairs f_subst f_th1)
| (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
- factor (resolve_inf ctxt mode skolems thpairs f_atm f_th1 f_th2)
- | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolems f_tm
+ factor (resolve_inf ctxt mode old_skolems thpairs f_atm f_th1 f_th2)
+ | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems f_tm
| (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
- equality_inf ctxt mode skolems f_lit f_p f_r
+ equality_inf ctxt mode old_skolems f_lit f_p f_r
fun is_real_literal (_, (c, _)) = not (String.isPrefix class_prefix c)
-fun replay_one_inference ctxt mode skolems (fol_th, inf) thpairs =
+fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs =
let
val _ = trace_msg (fn () => "=============================================")
val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
- val th = Meson.flexflex_first_order (step ctxt mode skolems
- thpairs (fol_th, inf))
+ val th = step ctxt mode old_skolems thpairs (fol_th, inf)
+ |> Meson.flexflex_first_order
val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
val _ = trace_msg (fn () => "=============================================")
- val n_metis_lits =
- length (filter is_real_literal (Metis_LiteralSet.toList (Metis_Thm.clause fol_th)))
- val _ = if nprems_of th = n_metis_lits then ()
- else error "Cannot replay Metis proof in Isabelle: Out of sync."
in (fol_th, th) :: thpairs end
end;
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Sep 29 17:59:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Sep 29 22:23:27 2010 +0200
@@ -56,15 +56,15 @@
let val thy = ProofContext.theory_of ctxt
val type_lits = Config.get ctxt type_lits
val th_cls_pairs =
- map (fn th => (Thm.get_name_hint th,
- Meson_Clausifier.meson_cnf_axiom thy th)) ths0
- val ths = maps #2 th_cls_pairs
+ map (fn th => (Thm.get_name_hint th, Meson_Clausifier.cnf_axiom thy th))
+ ths0
+ val thss = map #2 th_cls_pairs
val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
val _ = trace_msg (fn () => "THEOREM CLAUSES")
- val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
- val (mode, {axioms, tfrees, skolems}) =
- build_logic_map mode ctxt type_lits cls ths
+ val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss
+ val (mode, {axioms, tfrees, old_skolems}) =
+ build_logic_map mode ctxt type_lits cls thss
val _ = if null tfrees then ()
else (trace_msg (fn () => "TFREE CLAUSES");
app (fn TyLitFree ((s, _), (s', _)) =>
@@ -86,7 +86,8 @@
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
(*add constraints arising from converting goal to clause form*)
val proof = Metis_Proof.proof mth
- val result = fold (replay_one_inference ctxt' mode skolems) proof axioms
+ val result =
+ fold (replay_one_inference ctxt' mode old_skolems) proof axioms
and used = map_filter (used_axioms axioms) proof
val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
@@ -139,9 +140,6 @@
val type_has_top_sort =
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
-val preproc_ss =
- HOL_basic_ss addsimps @{thms all_simps[symmetric] ex_simps[symmetric]}
-
fun generic_metis_tac mode ctxt ths i st0 =
let
val _ = trace_msg (fn () =>
--- a/src/HOL/Tools/Sledgehammer/metis_translate.ML Wed Sep 29 17:59:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_translate.ML Wed Sep 29 22:23:27 2010 +0200
@@ -34,7 +34,7 @@
type logic_map =
{axioms: (Metis_Thm.thm * thm) list,
tfrees: type_literal list,
- skolems: (string * term) list}
+ old_skolems: (string * term) list}
val type_wrapper_name : string
val bound_var_prefix : string
@@ -45,6 +45,7 @@
val const_prefix: string
val type_const_prefix: string
val class_prefix: string
+ val new_skolem_prefix : string
val invert_const: string -> string
val ascii_of: string -> string
val unascii_of: string -> string
@@ -58,6 +59,7 @@
val make_fixed_type_const : string -> string
val make_type_class : string -> string
val num_type_args: theory -> string -> int
+ val new_skolem_var_from_const: string -> indexname
val type_literals_for_types : typ list -> type_literal list
val make_class_rel_clauses :
theory -> class list -> class list -> class_rel_clause list
@@ -66,14 +68,15 @@
val combtyp_of : combterm -> combtyp
val strip_combterm_comb : combterm -> combterm * combterm list
val combterm_from_term :
- theory -> (string * typ) list -> term -> combterm * typ list
- val reveal_skolem_terms : (string * term) list -> term -> term
+ theory -> int -> (string * typ) list -> term -> combterm * typ list
+ val reveal_old_skolem_terms : (string * term) list -> term -> term
val tfree_classes_of_terms : term list -> string list
val tvar_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
val string_of_mode : mode -> string
val build_logic_map :
- mode -> Proof.context -> bool -> thm list -> thm list -> mode * logic_map
+ mode -> Proof.context -> bool -> thm list -> thm list list
+ -> mode * logic_map
end
structure Metis_Translate : METIS_TRANSLATE =
@@ -92,6 +95,12 @@
val type_const_prefix = "tc_";
val class_prefix = "class_";
+val new_skolem_var_prefix = "SK?" (* purposedly won't parse *)
+
+val skolem_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
+val old_skolem_prefix = skolem_prefix ^ "o"
+val new_skolem_prefix = skolem_prefix ^ "n"
+
fun union_all xss = fold (union (op =)) xss []
(* Readable names for the more common symbolic functions. Do not mess with the
@@ -198,8 +207,6 @@
fun make_type_class clas = class_prefix ^ ascii_of clas;
-val skolem_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
-
(* The number of type arguments of a constant, zero if it's monomorphic. For
(instances of) Skolem pseudoconstants, this information is encoded in the
constant name. *)
@@ -209,6 +216,13 @@
else
(s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
+fun new_skolem_var_from_const s =
+ let
+ val ss = s |> space_explode Long_Name.separator
+ val n = length ss
+ in (nth ss (n - 2), nth ss (n - 3) |> Int.fromString |> the) end
+
+
(**** Definitions and functions for FOL clauses for TPTP format output ****)
type name = string * string
@@ -384,92 +398,107 @@
| simple_combtype_of (TVar (x, _)) =
CombTVar (make_schematic_type_var x, string_of_indexname x)
+fun new_skolem_name th_no s num_T_args =
+ [new_skolem_prefix, string_of_int th_no, s, string_of_int num_T_args]
+ |> space_implode Long_Name.separator
+
(* Converts a term (with combinators) into a combterm. Also accummulates sort
infomation. *)
-fun combterm_from_term thy bs (P $ Q) =
- let val (P', tsP) = combterm_from_term thy bs P
- val (Q', tsQ) = combterm_from_term thy bs Q
+fun combterm_from_term thy th_no bs (P $ Q) =
+ let val (P', tsP) = combterm_from_term thy th_no bs P
+ val (Q', tsQ) = combterm_from_term thy th_no bs Q
in (CombApp (P', Q'), union (op =) tsP tsQ) end
- | combterm_from_term thy _ (Const (c, T)) =
+ | combterm_from_term thy _ _ (Const (c, T)) =
let
val (tp, ts) = combtype_of T
val tvar_list =
- (if String.isPrefix skolem_prefix c then
+ (if String.isPrefix old_skolem_prefix c then
[] |> Term.add_tvarsT T |> map TVar
else
(c, T) |> Sign.const_typargs thy)
|> map simple_combtype_of
val c' = CombConst (`make_fixed_const c, tp, tvar_list)
in (c',ts) end
- | combterm_from_term _ _ (Free (v, T)) =
+ | combterm_from_term _ _ _ (Free (v, T)) =
let val (tp, ts) = combtype_of T
val v' = CombConst (`make_fixed_var v, tp, [])
in (v',ts) end
- | combterm_from_term _ _ (Var (v, T)) =
- let val (tp,ts) = combtype_of T
- val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
- in (v',ts) end
- | combterm_from_term _ bs (Bound j) =
+ | combterm_from_term _ th_no _ (Var (v as (s, _), T)) =
+ let
+ val (tp, ts) = combtype_of T
+ val v' =
+ if String.isPrefix new_skolem_var_prefix s then
+ let
+ val tys = T |> strip_type |> swap |> op ::
+ val s' = new_skolem_name th_no s (length tys)
+ in
+ CombConst (`make_fixed_const s', tp, map simple_combtype_of tys)
+ end
+ else
+ CombVar ((make_schematic_var v, string_of_indexname v), tp)
+ in (v', ts) end
+ | combterm_from_term _ _ bs (Bound j) =
let
val (s, T) = nth bs j
val (tp, ts) = combtype_of T
val v' = CombConst (`make_bound_var s, tp, [])
in (v', ts) end
- | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
+ | combterm_from_term _ _ _ (Abs _) = raise Fail "HOL clause: Abs"
-fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
- | predicate_of thy (t, pos) =
- (combterm_from_term thy [] (Envir.eta_contract t), pos)
+fun predicate_of thy th_no ((@{const Not} $ P), pos) =
+ predicate_of thy th_no (P, not pos)
+ | predicate_of thy th_no (t, pos) =
+ (combterm_from_term thy th_no [] (Envir.eta_contract t), pos)
-fun literals_of_term1 args thy (@{const Trueprop} $ P) =
- literals_of_term1 args thy P
- | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
- literals_of_term1 (literals_of_term1 args thy P) thy Q
- | literals_of_term1 (lits, ts) thy P =
- let val ((pred, ts'), pol) = predicate_of thy (P, true) in
+fun literals_of_term1 args thy th_no (@{const Trueprop} $ P) =
+ literals_of_term1 args thy th_no P
+ | literals_of_term1 args thy th_no (@{const HOL.disj} $ P $ Q) =
+ literals_of_term1 (literals_of_term1 args thy th_no P) thy th_no Q
+ | literals_of_term1 (lits, ts) thy th_no P =
+ let val ((pred, ts'), pol) = predicate_of thy th_no (P, true) in
(FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
end
val literals_of_term = literals_of_term1 ([], [])
-fun skolem_name i j num_T_args =
- skolem_prefix ^ Long_Name.separator ^
+fun old_skolem_name i j num_T_args =
+ old_skolem_prefix ^ Long_Name.separator ^
(space_implode Long_Name.separator (map Int.toString [i, j, num_T_args]))
-fun conceal_skolem_terms i skolems t =
+fun conceal_old_skolem_terms i old_skolems t =
if exists_Const (curry (op =) @{const_name skolem} o fst) t then
let
- fun aux skolems
+ fun aux old_skolems
(t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) =
let
- val (skolems, s) =
+ val (old_skolems, s) =
if i = ~1 then
- (skolems, @{const_name undefined})
- else case AList.find (op aconv) skolems t of
- s :: _ => (skolems, s)
+ (old_skolems, @{const_name undefined})
+ else case AList.find (op aconv) old_skolems t of
+ s :: _ => (old_skolems, s)
| [] =>
let
- val s = skolem_name i (length skolems)
- (length (Term.add_tvarsT T []))
- in ((s, t) :: skolems, s) end
- in (skolems, Const (s, T)) end
- | aux skolems (t1 $ t2) =
+ val s = old_skolem_name i (length old_skolems)
+ (length (Term.add_tvarsT T []))
+ in ((s, t) :: old_skolems, s) end
+ in (old_skolems, Const (s, T)) end
+ | aux old_skolems (t1 $ t2) =
let
- val (skolems, t1) = aux skolems t1
- val (skolems, t2) = aux skolems t2
- in (skolems, t1 $ t2) end
- | aux skolems (Abs (s, T, t')) =
- let val (skolems, t') = aux skolems t' in
- (skolems, Abs (s, T, t'))
+ val (old_skolems, t1) = aux old_skolems t1
+ val (old_skolems, t2) = aux old_skolems t2
+ in (old_skolems, t1 $ t2) end
+ | aux old_skolems (Abs (s, T, t')) =
+ let val (old_skolems, t') = aux old_skolems t' in
+ (old_skolems, Abs (s, T, t'))
end
- | aux skolems t = (skolems, t)
- in aux skolems t end
+ | aux old_skolems t = (old_skolems, t)
+ in aux old_skolems t end
else
- (skolems, t)
+ (old_skolems, t)
-fun reveal_skolem_terms skolems =
+fun reveal_old_skolem_terms old_skolems =
map_aterms (fn t as Const (s, _) =>
- if String.isPrefix skolem_prefix s then
- AList.lookup (op =) skolems s |> the
+ if String.isPrefix old_skolem_prefix s then
+ AList.lookup (op =) old_skolems s |> the
|> map_types Type_Infer.paramify_vars
else
t
@@ -580,8 +609,8 @@
metis_lit pos "=" (map hol_term_to_fol_FT tms)
| _ => metis_lit pos "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
-fun literals_of_hol_term thy mode t =
- let val (lits, types_sorts) = literals_of_term thy t
+fun literals_of_hol_term thy th_no mode t =
+ let val (lits, types_sorts) = literals_of_term thy th_no t
in (map (hol_literal_to_fol mode) lits, types_sorts) end;
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
@@ -596,16 +625,16 @@
fun metis_of_tfree tf =
Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
-fun hol_thm_to_fol is_conjecture ctxt type_lits mode j skolems th =
+fun hol_thm_to_fol is_conjecture th_no ctxt type_lits mode j old_skolems th =
let
val thy = ProofContext.theory_of ctxt
- val (skolems, (mlits, types_sorts)) =
- th |> prop_of |> conceal_skolem_terms j skolems
- ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
+ val (old_skolems, (mlits, types_sorts)) =
+ th |> prop_of |> conceal_old_skolem_terms j old_skolems
+ ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy th_no mode)
in
if is_conjecture then
(Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
- type_literals_for_types types_sorts, skolems)
+ type_literals_for_types types_sorts, old_skolems)
else
let
val tylits = filter_out (default_sort ctxt) types_sorts
@@ -614,7 +643,7 @@
if type_lits then map (metis_of_type_literals false) tylits else []
in
(Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [],
- skolems)
+ old_skolems)
end
end;
@@ -637,10 +666,10 @@
type logic_map =
{axioms: (Metis_Thm.thm * thm) list,
tfrees: type_literal list,
- skolems: (string * term) list}
+ old_skolems: (string * term) list}
fun is_quasi_fol_clause thy =
- Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of
+ Meson.is_fol_term thy o snd o conceal_old_skolem_terms ~1 [] o prop_of
(*Extract TFree constraints from context to include as conjecture clauses*)
fun init_tfrees ctxt =
@@ -650,16 +679,16 @@
end;
(*Insert non-logical axioms corresponding to all accumulated TFrees*)
-fun add_tfrees {axioms, tfrees, skolems} : logic_map =
+fun add_tfrees {axioms, tfrees, old_skolems} : logic_map =
{axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
axioms,
- tfrees = tfrees, skolems = skolems}
+ tfrees = tfrees, old_skolems = old_skolems}
(*transform isabelle type / arity clause to metis clause *)
fun add_type_thm [] lmap = lmap
- | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolems} =
+ | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, old_skolems} =
add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
- skolems = skolems}
+ old_skolems = old_skolems}
fun const_in_metis c (pred, tm_list) =
let
@@ -694,29 +723,31 @@
end;
(* Function to generate metis clauses, including comb and type clauses *)
-fun build_logic_map mode0 ctxt type_lits cls ths =
+fun build_logic_map mode0 ctxt type_lits cls thss =
let val thy = ProofContext.theory_of ctxt
(*The modes FO and FT are sticky. HO can be downgraded to FO.*)
fun set_mode FO = FO
| set_mode HO =
- if forall (is_quasi_fol_clause thy) (cls @ ths) then FO else HO
+ if forall (forall (is_quasi_fol_clause thy)) (cls :: thss) then FO
+ else HO
| set_mode FT = FT
val mode = set_mode mode0
(*transform isabelle clause to metis clause *)
- fun add_thm is_conjecture (metis_ith, isa_ith) {axioms, tfrees, skolems}
- : logic_map =
+ fun add_thm th_no is_conjecture (metis_ith, isa_ith)
+ {axioms, tfrees, old_skolems} : logic_map =
let
- val (mth, tfree_lits, skolems) =
- hol_thm_to_fol is_conjecture ctxt type_lits mode (length axioms)
- skolems metis_ith
+ val (mth, tfree_lits, old_skolems) =
+ hol_thm_to_fol is_conjecture th_no ctxt type_lits mode (length axioms)
+ old_skolems metis_ith
in
{axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
- tfrees = union (op =) tfree_lits tfrees, skolems = skolems}
+ tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
end;
- val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []}
- |> fold (add_thm true o `I) cls
+ val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}
+ |> fold (add_thm 0 true o `I) cls
|> add_tfrees
- |> fold (add_thm false o `I) ths
+ |> fold (fn (th_no, ths) => fold (add_thm th_no false o `I) ths)
+ (1 upto length thss ~~ thss)
val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap)
fun is_used c =
exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
@@ -733,7 +764,9 @@
[]
else
thms)
- in lmap |> fold (add_thm false) helper_ths end
- in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
+ in lmap |> fold (add_thm ~1 false) helper_ths end
+ in
+ (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap)
+ end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Sep 29 17:59:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Sep 29 22:23:27 2010 +0200
@@ -57,7 +57,7 @@
fun combformula_for_prop thy =
let
- val do_term = combterm_from_term thy
+ val do_term = combterm_from_term thy ~1
fun do_quant bs q s T t' =
let val s = Name.variant (map fst bs) s in
do_formula ((s, T) :: bs) t'
--- a/src/HOL/Tools/meson.ML Wed Sep 29 17:59:20 2010 +0200
+++ b/src/HOL/Tools/meson.ML Wed Sep 29 22:23:27 2010 +0200
@@ -330,7 +330,7 @@
(* Conjunctive normal form, adding clauses from th in front of ths (for foldr).
Strips universal quantifiers and breaks up conjunctions.
Eliminates existential quantifiers using Skolemization theorems. *)
-fun cnf skolem_ths ctxt (th, ths) =
+fun cnf old_skolem_ths ctxt (th, ths) =
let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *)
fun cnf_aux (th,ths) =
if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
@@ -344,7 +344,7 @@
in ctxtr := ctxt'; cnf_aux (th', ths) end
| Const (@{const_name Ex}, _) =>
(*existential quantifier: Insert Skolem functions*)
- cnf_aux (apply_skolem_theorem (th, skolem_ths), ths)
+ cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths)
| Const (@{const_name HOL.disj}, _) =>
(*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
all combinations of converting P, Q to CNF.*)
@@ -360,7 +360,7 @@
else cnf_aux (th,ths)
in (cls, !ctxtr) end;
-fun make_cnf skolem_ths th ctxt = cnf skolem_ths ctxt (th, []);
+fun make_cnf old_skolem_ths th ctxt = cnf old_skolem_ths ctxt (th, [])
(*Generalization, removal of redundant equalities, removal of tautologies.*)
fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);