author blanchet Fri, 01 Aug 2014 23:29:49 +0200 changeset 57767 5bc204ca27ce parent 57766 77b48e7c0d89 child 57768 a63f14f1214c
centralized boolean simplification so that e.g. LEO-II benefits from it
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Fri Aug 01 20:44:51 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Fri Aug 01 23:29:49 2014 +0200
@@ -30,6 +30,7 @@

val forall_of : term -> term -> term
val exists_of : term -> term -> term
+  val simplify_bool : term -> term
val rename_bound_vars : term -> term
val type_enc_aliases : (string * string list) list
val unalias_type_enc : string -> string list
@@ -102,6 +103,21 @@
TFree (ww, the_default @{sort type} (Variable.def_sort ctxt (ww, ~1)))
end

+fun simplify_bool ((all as Const (@{const_name All}, _)) \$ Abs (s, T, t)) =
+    let val t' = simplify_bool t in
+      if loose_bvar1 (t', 0) then all \$ Abs (s, T, t') else t'
+    end
+  | simplify_bool (@{const Not} \$ t) = s_not (simplify_bool t)
+  | simplify_bool (@{const conj} \$ t \$ u) = s_conj (simplify_bool t, simplify_bool u)
+  | simplify_bool (@{const disj} \$ t \$ u) = s_disj (simplify_bool t, simplify_bool u)
+  | simplify_bool (@{const implies} \$ t \$ u) = s_imp (simplify_bool t, simplify_bool u)
+  | simplify_bool (@{const HOL.eq (bool)} \$ t \$ u) = s_iff (simplify_bool t, simplify_bool u)
+  | simplify_bool (t as Const (@{const_name HOL.eq}, _) \$ u \$ v) =
+    if u aconv v then @{const True} else t
+  | simplify_bool (t \$ u) = simplify_bool t \$ simplify_bool u
+  | simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t)
+  | simplify_bool t = t
+
fun single_letter upper s =
let val s' = if String.isPrefix "o" s orelse String.isPrefix "O" s then "z" else s in
String.extract (Name.desymbolize (SOME upper) (Long_Name.base_name s'), 0, SOME 1)
--- a/src/HOL/Tools/SMT2/smtlib2_isar.ML	Fri Aug 01 20:44:51 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_isar.ML	Fri Aug 01 23:29:49 2014 +0200
@@ -7,7 +7,6 @@

signature SMTLIB2_ISAR =
sig
-  val simplify_bool: term -> term
val unlift_term: term list -> term -> term
val postprocess_step_conclusion: theory -> thm list -> term list -> term -> term
val normalizing_prems : Proof.context -> term -> (string * string list) list
@@ -22,24 +21,6 @@
open ATP_Problem
open ATP_Util

-fun simplify_bool ((all as Const (@{const_name All}, _)) \$ Abs (s, T, t)) =
-    let val t' = simplify_bool t in
-      if loose_bvar1 (t', 0) then all \$ Abs (s, T, t') else t'
-    end
-  | simplify_bool (@{const Not} \$ t) = s_not (simplify_bool t)
-  | simplify_bool (@{const conj} \$ t \$ u) = s_conj (simplify_bool t, simplify_bool u)
-  | simplify_bool (@{const disj} \$ t \$ u) = s_disj (simplify_bool t, simplify_bool u)
-  | simplify_bool (@{const implies} \$ t \$ u) = s_imp (simplify_bool t, simplify_bool u)
-  | simplify_bool (@{const HOL.eq (bool)} \$ t \$ u) = s_iff (simplify_bool t, simplify_bool u)
-  | simplify_bool (t as Const (@{const_name HOL.eq}, _) \$ u \$ v) =
-    if u aconv v then @{const True} else t
-  | simplify_bool (t \$ u) = simplify_bool t \$ simplify_bool u
-  | simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t)
-  | simplify_bool t = t
-
-fun strip_alls (Const (@{const_name All}, _) \$ Abs (s, T, body)) = strip_alls body |>> cons (s, T)
-  | strip_alls t = ([], t)
-
fun unlift_term ll_defs =
let
val lifted = map (ATP_Util.extract_lambda_def dest_Free o ATP_Util.hol_open_form I) ll_defs
@@ -60,7 +41,6 @@
fun postprocess_step_conclusion thy rewrite_rules ll_defs =
Raw_Simplifier.rewrite_term thy rewrite_rules []
#> Object_Logic.atomize_term thy
-  #> simplify_bool
#> not (null ll_defs) ? unlift_term ll_defs
#> unskolemize_names
#> HOLogic.mk_Trueprop
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 20:44:51 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 23:29:49 2014 +0200
@@ -210,9 +210,9 @@

val rule_of_clause_id = fst o the o Symtab.lookup steps o fst

-        val close_form_etc = rename_bound_vars o close_form
+        val finish_off = simplify_bool #> close_form #> rename_bound_vars

-        fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form_etc
+        fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off
| prop_of_clause names =
let
val lits =
@@ -223,7 +223,7 @@
s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos)
| _ => fold (curry s_disj) lits @{term False})
end
-            |> HOLogic.mk_Trueprop |> close_form_etc
+            |> HOLogic.mk_Trueprop |> finish_off

fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show