# HG changeset patch
# User blanchet
# Date 1406928589 -7200
# Node ID 5bc204ca27cecda408554582b06781eafe37494c
# Parent  77b48e7c0d89acae8031558696e8517bff77c593
centralized boolean simplification so that e.g. LEO-II benefits from it

diff -r 77b48e7c0d89 -r 5bc204ca27ce src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- 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)
diff -r 77b48e7c0d89 -r 5bc204ca27ce src/HOL/Tools/SMT2/smtlib2_isar.ML
--- 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
diff -r 77b48e7c0d89 -r 5bc204ca27ce src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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