--- a/src/HOL/Library/refute.ML Sun Dec 15 18:54:26 2013 +0100
+++ b/src/HOL/Library/refute.ML Sun Dec 15 19:01:06 2013 +0100
@@ -393,21 +393,7 @@
(* ------------------------------------------------------------------------- *)
val typ_of_dtyp = Nitpick_Util.typ_of_dtyp
-
-(* ------------------------------------------------------------------------- *)
-(* close_form: universal closure over schematic variables in 't' *)
-(* ------------------------------------------------------------------------- *)
-
-(* Term.term -> Term.term *)
-
-fun close_form t =
- let
- val vars = sort_wrt (fst o fst) (Term.add_vars t [])
- in
- fold (fn ((x, i), T) => fn t' =>
- Logic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
- end;
-
+val close_form = ATP_Util.close_form
val monomorphic_term = ATP_Util.monomorphic_term
val specialize_type = ATP_Util.specialize_type
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Dec 15 18:54:26 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Dec 15 19:01:06 2013 +0100
@@ -1332,10 +1332,6 @@
| formula => SOME formula
end
-fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
- | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t
- | s_not_prop t = @{const "==>"} $ t $ @{prop False}
-
fun make_conjecture ctxt format type_enc =
map (fn ((name, stature), (role, t)) =>
let
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Dec 15 18:54:26 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Dec 15 19:01:06 2013 +0100
@@ -504,6 +504,7 @@
|> uncombine_term thy
|> unlift_term lifted
|> infer_formula_types ctxt
+ |> HOLogic.mk_Trueprop
in
(name, role, t, rule, deps)
end
--- a/src/HOL/Tools/ATP/atp_util.ML Sun Dec 15 18:54:26 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML Sun Dec 15 19:01:06 2013 +0100
@@ -36,6 +36,7 @@
val s_disj : term * term -> term
val s_imp : term * term -> term
val s_iff : term * term -> term
+ val s_not_prop : term -> term
val close_form : term -> term
val hol_close_form_prefix : string
val hol_close_form : term -> term
@@ -292,22 +293,27 @@
| s_disj (@{const True}, _) = @{const True}
| s_disj (_, @{const True}) = @{const True}
| s_disj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_disj (t1, t2)
+
fun s_imp (@{const True}, t2) = t2
| s_imp (t1, @{const False}) = s_not t1
| s_imp (@{const False}, _) = @{const True}
| s_imp (_, @{const True}) = @{const True}
| s_imp p = HOLogic.mk_imp p
+
fun s_iff (@{const True}, t2) = t2
| s_iff (t1, @{const True}) = t1
| s_iff (@{const False}, t2) = s_not t2
| s_iff (t1, @{const False}) = s_not t1
| s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
-(* cf. "close_form" in "refute.ML" *)
+fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
+ | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t
+ | s_not_prop t = @{const "==>"} $ t $ @{prop False}
+
fun close_form t =
fold (fn ((s, i), T) => fn t' =>
- Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
- (Term.add_vars t []) t
+ Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
+ (Term.add_vars t []) t
val hol_close_form_prefix = "ATP.close_form."
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Dec 15 18:54:26 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Dec 15 19:01:06 2013 +0100
@@ -47,9 +47,6 @@
open String_Redirect
-fun maybe_mk_Trueprop t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
-val maybe_dest_Trueprop = perhaps (try HOLogic.dest_Trueprop)
-
val e_skolemize_rule = "skolemize"
val vampire_skolemisation_rule = "skolemisation"
(* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
@@ -81,7 +78,7 @@
fun inline_z3_defs _ [] = []
| inline_z3_defs defs ((line as (name, role, t, rule, deps)) :: lines) =
if rule = z3_intro_def_rule then
- let val def = t |> maybe_dest_Trueprop |> HOLogic.dest_eq |> swap in
+ let val def = t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> swap in
inline_z3_defs (insert (op =) def defs)
(map (replace_dependencies_in_line (name, [])) lines)
end
@@ -286,7 +283,7 @@
else if is_arith_rule rule then ([], ArithM)
else ([], AutoM)
in
- Prove ([], skos, l, maybe_mk_Trueprop t, [], (([], []), meth))
+ Prove ([], skos, l, t, [], (([], []), meth))
end)
val bot = atp_proof |> List.last |> #1
@@ -306,7 +303,7 @@
|> fold (fn (name as (s, _), role, t, rule, _) =>
Symtab.update_new (s, (rule,
t |> (if is_clause_tainted [name] then
- role <> Conjecture ? (maybe_dest_Trueprop #> s_not)
+ role <> Conjecture ? s_not_prop
#> fold exists_of (map Var (Term.add_vars t []))
else
I))))
@@ -314,14 +311,11 @@
val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
- (* The assumptions and conjecture are "prop"s; the other formulas are "bool"s (for ATPs) or
- "prop"s (for Z3). TODO: Always use "prop". *)
- fun prop_of_clause [(num, _)] =
- Symtab.lookup steps num |> the |> snd |> maybe_mk_Trueprop |> close_form
+ fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form
| prop_of_clause names =
let
val lits =
- map (maybe_dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names)
+ map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names)
in
(case List.partition (can HOLogic.dest_not) lits of
(negs as _ :: _, pos as _ :: _) =>