--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 29 09:19:16 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 29 09:26:56 2010 +0200
@@ -142,24 +142,23 @@
fun is_tautology (HOLClause {literals,...}) = exists is_true_literal literals
(* making axiom and conjecture clauses *)
-fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes =
+fun make_clause thy (clause_id, axiom_name, kind, th) skolems =
let
- val (skolem_somes, t) =
- th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
+ val (skolems, t) = th |> prop_of |> conceal_skolem_terms clause_id skolems
val (lits, ctypes_sorts) = literals_of_term thy t
in
if forall is_false_literal lits then
raise TRIVIAL ()
else
- (skolem_somes,
+ (skolems,
HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
end
-fun add_axiom_clause thy ((name, k), th) (skolem_somes, clss) =
+fun add_axiom_clause thy ((name, k), th) (skolems, clss) =
let
- val (skolem_somes, cls) = make_clause thy (k, name, Axiom, th) skolem_somes
- in (skolem_somes, clss |> not (is_tautology cls) ? cons (name, cls)) end
+ val (skolems, cls) = make_clause thy (k, name, Axiom, th) skolems
+ in (skolems, clss |> not (is_tautology cls) ? cons (name, cls)) end
fun make_axiom_clauses thy clauses =
([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
@@ -167,11 +166,11 @@
fun make_conjecture_clauses thy =
let
fun aux _ _ [] = []
- | aux n skolem_somes (th :: ths) =
+ | aux n skolems (th :: ths) =
let
- val (skolem_somes, cls) =
- make_clause thy (n, "conjecture", Conjecture, th) skolem_somes
- in cls :: aux (n + 1) skolem_somes ths end
+ val (skolems, cls) =
+ make_clause thy (n, "conjecture", Conjecture, th) skolems
+ in cls :: aux (n + 1) skolems ths end
in aux 0 [] end
(** Helper clauses **)
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jun 29 09:19:16 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jun 29 09:26:56 2010 +0200
@@ -64,7 +64,7 @@
val type_of_combterm : combterm -> combtyp
val strip_combterm_comb : combterm -> combterm * combterm list
val literals_of_term : theory -> term -> literal list * typ list
- val conceal_skolem_somes :
+ val conceal_skolem_terms :
int -> (string * term) list -> term -> (string * term) list * term
val tfree_classes_of_terms : term list -> string list
val tvar_classes_of_terms : term list -> string list
@@ -441,37 +441,37 @@
skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
skolem_infix ^ "g"
-fun conceal_skolem_somes i skolem_somes t =
+fun conceal_skolem_terms i skolems t =
if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
let
- fun aux skolem_somes
+ fun aux skolems
(t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
let
- val (skolem_somes, s) =
+ val (skolems, s) =
if i = ~1 then
- (skolem_somes, @{const_name undefined})
- else case AList.find (op aconv) skolem_somes t of
- s :: _ => (skolem_somes, s)
+ (skolems, @{const_name undefined})
+ else case AList.find (op aconv) skolems t of
+ s :: _ => (skolems, s)
| [] =>
let
val s = skolem_theory_name ^ "." ^
- skolem_name i (length skolem_somes)
+ skolem_name i (length skolems)
(length (Term.add_tvarsT T []))
- in ((s, t) :: skolem_somes, s) end
- in (skolem_somes, Const (s, T)) end
- | aux skolem_somes (t1 $ t2) =
+ in ((s, t) :: skolems, s) end
+ in (skolems, Const (s, T)) end
+ | aux skolems (t1 $ t2) =
let
- val (skolem_somes, t1) = aux skolem_somes t1
- val (skolem_somes, t2) = aux skolem_somes t2
- in (skolem_somes, t1 $ t2) end
- | aux skolem_somes (Abs (s, T, t')) =
- let val (skolem_somes, t') = aux skolem_somes t' in
- (skolem_somes, Abs (s, T, t'))
+ 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'))
end
- | aux skolem_somes t = (skolem_somes, t)
- in aux skolem_somes t end
+ | aux skolems t = (skolems, t)
+ in aux skolems t end
else
- (skolem_somes, t)
+ (skolems, t)
(***************************************************************)
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 29 09:19:16 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 29 09:26:56 2010 +0200
@@ -135,16 +135,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 mode j skolem_somes th =
+fun hol_thm_to_fol is_conjecture ctxt mode j skolems th =
let
val thy = ProofContext.theory_of ctxt
- val (skolem_somes, (mlits, types_sorts)) =
- th |> prop_of |> conceal_skolem_somes j skolem_somes
+ val (skolems, (mlits, types_sorts)) =
+ th |> prop_of |> conceal_skolem_terms j skolems
||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
in
if is_conjecture then
(Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
- type_literals_for_types types_sorts, skolem_somes)
+ type_literals_for_types types_sorts, skolems)
else
let val tylits = filter_out (default_sort ctxt) types_sorts
|> type_literals_for_types
@@ -152,7 +152,7 @@
then map (metis_of_type_literals false) tylits else []
in
(Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [],
- skolem_somes)
+ skolems)
end
end;
@@ -235,11 +235,11 @@
SOME tf => mk_tfree ctxt tf
| NONE => raise Fail ("fol_type_to_isa: " ^ x));
-fun reveal_skolem_somes skolem_somes =
+fun reveal_skolem_terms skolems =
map_aterms (fn t as Const (s, _) =>
if String.isPrefix skolem_theory_name s then
- AList.lookup (op =) skolem_somes s
- |> the |> map_types Type_Infer.paramify_vars
+ AList.lookup (op =) skolems s |> the
+ |> map_types Type_Infer.paramify_vars
else
t
| t => t)
@@ -345,11 +345,11 @@
fun hol_term_from_fol FT = hol_term_from_fol_FT
| hol_term_from_fol _ = hol_term_from_fol_PT
-fun hol_terms_from_fol ctxt mode skolem_somes fol_tms =
+fun hol_terms_from_fol ctxt mode skolems fol_tms =
let val ts = map (hol_term_from_fol 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_somes skolem_somes) |> infer_types ctxt
+ val ts' = ts |> map (reveal_skolem_terms 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)))
@@ -391,22 +391,22 @@
(*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
(* INFERENCE RULE: ASSUME *)
-fun assume_inf ctxt mode skolem_somes atm =
+fun assume_inf ctxt mode skolems atm =
inst_excluded_middle
- (ProofContext.theory_of ctxt)
- (singleton (hol_terms_from_fol ctxt mode skolem_somes) (Metis.Term.Fn atm))
+ (ProofContext.theory_of ctxt)
+ (singleton (hol_terms_from_fol ctxt mode 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 skolem_somes thpairs fsubst th =
+fun inst_inf ctxt mode 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_somes" and "infer_types" below. *)
+ (* We call "reveal_skolem_terms" and "infer_types" below. *)
val t = hol_term_from_fol mode ctxt y
in SOME (cterm_of thy (Var v), t) end
handle Option =>
@@ -422,8 +422,7 @@
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_somes skolem_somes)
- |> infer_types ctxt
+ val tms = rawtms |> map (reveal_skolem_terms 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 () =>
@@ -451,7 +450,7 @@
end
handle TERM (msg, _) => raise METIS ("resolve_inc_tyvars", msg)
-fun resolve_inf ctxt mode skolem_somes thpairs atm th1 th2 =
+fun resolve_inf ctxt mode skolems thpairs atm th1 th2 =
let
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
@@ -461,7 +460,7 @@
else if is_TrueI i_th2 then i_th1
else
let
- val i_atm = singleton (hol_terms_from_fol ctxt mode skolem_somes)
+ val i_atm = singleton (hol_terms_from_fol ctxt mode skolems)
(Metis.Term.Fn atm)
val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
val prems_th1 = prems_of i_th1
@@ -479,9 +478,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 skolem_somes t =
+fun refl_inf ctxt mode skolems t =
let val thy = ProofContext.theory_of ctxt
- val i_t = singleton (hol_terms_from_fol ctxt mode skolem_somes) t
+ val i_t = singleton (hol_terms_from_fol ctxt mode 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;
@@ -491,10 +490,10 @@
| get_ty_arg_size _ _ = 0;
(* INFERENCE RULE: EQUALITY *)
-fun equality_inf ctxt mode skolem_somes (pos, atm) fp fr =
+fun equality_inf ctxt mode 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 skolem_somes [m_tm, fr]
+ val [i_atm,i_tm] = hol_terms_from_fol ctxt mode 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
@@ -568,27 +567,27 @@
val factor = Seq.hd o distinct_subgoals_tac;
-fun step ctxt mode skolem_somes thpairs p =
+fun step ctxt mode 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 skolem_somes f_atm
+ | (_, Metis.Proof.Assume f_atm) => assume_inf ctxt mode skolems f_atm
| (_, Metis.Proof.Subst (f_subst, f_th1)) =>
- factor (inst_inf ctxt mode skolem_somes thpairs f_subst f_th1)
+ factor (inst_inf ctxt mode skolems thpairs f_subst f_th1)
| (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =>
- factor (resolve_inf ctxt mode skolem_somes thpairs f_atm f_th1 f_th2)
- | (_, Metis.Proof.Refl f_tm) => refl_inf ctxt mode skolem_somes f_tm
+ 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
| (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =>
- equality_inf ctxt mode skolem_somes f_lit f_p f_r
+ equality_inf ctxt mode skolems f_lit f_p f_r
fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
(* FIXME: use "fold" instead *)
fun translate _ _ _ thpairs [] = thpairs
- | translate ctxt mode skolem_somes thpairs ((fol_th, inf) :: infpairs) =
+ | translate ctxt mode skolems thpairs ((fol_th, inf) :: infpairs) =
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 skolem_somes
+ val th = Meson.flexflex_first_order (step ctxt mode skolems
thpairs (fol_th, inf))
val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
val _ = trace_msg (fn () => "=============================================")
@@ -597,7 +596,7 @@
in
if nprems_of th = n_metis_lits then ()
else raise METIS ("translate", "Proof reconstruction has gone wrong.");
- translate ctxt mode skolem_somes ((fol_th, th) :: thpairs) infpairs
+ translate ctxt mode skolems ((fol_th, th) :: thpairs) infpairs
end;
(*Determining which axiom clauses are actually used*)
@@ -627,7 +626,7 @@
type logic_map =
{axioms: (Metis.Thm.thm * thm) list,
tfrees: type_literal list,
- skolem_somes: (string * term) list}
+ skolems: (string * term) list}
fun const_in_metis c (pred, tm_list) =
let
@@ -645,15 +644,15 @@
(*transform isabelle type / arity clause to metis clause *)
fun add_type_thm [] lmap = lmap
- | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolem_somes} =
+ | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolems} =
add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
- skolem_somes = skolem_somes}
+ skolems = skolems}
(*Insert non-logical axioms corresponding to all accumulated TFrees*)
-fun add_tfrees {axioms, tfrees, skolem_somes} : logic_map =
+fun add_tfrees {axioms, tfrees, skolems} : logic_map =
{axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
axioms,
- tfrees = tfrees, skolem_somes = skolem_somes}
+ tfrees = tfrees, skolems = skolems}
fun string_of_mode FO = "FO"
| string_of_mode HO = "HO"
@@ -671,7 +670,7 @@
("c_If", (true, @{thms if_True if_False True_or_False}))]
fun is_quasi_fol_clause thy =
- Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 [] o prop_of
+ Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of
(* Function to generate metis clauses, including comb and type clauses *)
fun build_map mode0 ctxt cls ths =
@@ -683,17 +682,15 @@
| set_mode FT = FT
val mode = set_mode mode0
(*transform isabelle clause to metis clause *)
- fun add_thm is_conjecture ith {axioms, tfrees, skolem_somes} : logic_map =
+ fun add_thm is_conjecture ith {axioms, tfrees, skolems} : logic_map =
let
- val (mth, tfree_lits, skolem_somes) =
- hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolem_somes
- ith
+ val (mth, tfree_lits, skolems) =
+ hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems ith
in
{axioms = (mth, Meson.make_meta_clause ith) :: axioms,
- tfrees = union (op =) tfree_lits tfrees,
- skolem_somes = skolem_somes}
+ tfrees = union (op =) tfree_lits tfrees, skolems = skolems}
end;
- val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []}
+ val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []}
|> fold (add_thm true) cls
|> add_tfrees
|> fold (add_thm false) ths
@@ -733,7 +730,7 @@
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, skolem_somes}) = build_map mode ctxt cls ths
+ val (mode, {axioms, tfrees, skolems}) = build_map mode ctxt cls ths
val _ = if null tfrees then ()
else (trace_msg (fn () => "TFREE CLAUSES");
app (fn TyLitFree (s, (s', _)) =>
@@ -754,7 +751,7 @@
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 = translate ctxt' mode skolem_somes axioms proof
+ val result = translate ctxt' mode skolems axioms proof
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