# HG changeset patch
# User blanchet
# Date 1305888478 -7200
# Node ID 85ac4c12a4b7b06cb37d217c11d03e583149b01e
# Parent  d7447b8c42657ffd23596999d9db9f4a8d7aa0ac
slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous

diff -r d7447b8c4265 -r 85ac4c12a4b7 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 20 12:47:58 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 20 12:47:58 2011 +0200
@@ -168,15 +168,24 @@
   | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
   | formula_map f (AAtom tm) = AAtom (f tm)
 
+fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi
+  | aconn_fold pos f (AImplies, [phi1, phi2]) =
+    f (Option.map not pos) phi1 #> f pos phi2
+  | aconn_fold pos f (AAnd, phis) = fold (f pos) phis
+  | aconn_fold pos f (AOr, phis) = fold (f pos) phis
+  | aconn_fold _ f (_, phis) = fold (f NONE) phis
+
+fun aconn_map pos f (ANot, [phi]) = AConn (ANot, [f (Option.map not pos) phi])
+  | aconn_map pos f (AImplies, [phi1, phi2]) =
+    AConn (AImplies, [f (Option.map not pos) phi1, f pos phi2])
+  | aconn_map pos f (AAnd, phis) = AConn (AAnd, map (f pos) phis)
+  | aconn_map pos f (AOr, phis) = AConn (AOr, map (f pos) phis)
+  | aconn_map _ f (c, phis) = AConn (c, map (f NONE) phis)
+
 fun formula_fold pos f =
   let
     fun aux pos (AQuant (_, _, phi)) = aux pos phi
-      | aux pos (AConn (ANot, [phi])) = aux (Option.map not pos) phi
-      | aux pos (AConn (AImplies, [phi1, phi2])) =
-        aux (Option.map not pos) phi1 #> aux pos phi2
-      | aux pos (AConn (AAnd, phis)) = fold (aux pos) phis
-      | aux pos (AConn (AOr, phis)) = fold (aux pos) phis
-      | aux _ (AConn (_, phis)) = fold (aux NONE) phis
+      | aux pos (AConn conn) = aconn_fold pos aux conn
       | aux pos (AAtom tm) = f pos tm
   in aux pos end
 
@@ -489,8 +498,8 @@
 
 fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
                              should_predicate_on_var T =
-     (heaviness = Heavy orelse should_predicate_on_var ()) andalso
-     should_encode_type ctxt nonmono_Ts level T
+    (heaviness = Heavy orelse should_predicate_on_var ()) andalso
+    should_encode_type ctxt nonmono_Ts level T
   | should_predicate_on_type _ _ _ _ _ = false
 
 fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
@@ -780,17 +789,17 @@
 
 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
 
-fun type_pred_combatom ctxt nonmono_Ts type_sys T tm =
+fun type_pred_combterm ctxt nonmono_Ts type_sys T tm =
   CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T])
            |> enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys,
            tm)
-  |> AAtom
 
-fun var_occurs_naked_in_term name (ATerm ((s, _), tms)) accum =
-  accum orelse
-  (s = "equal" andalso member (op =) tms (ATerm (name, [])))
-fun var_occurs_naked_in_formula phi name =
-  formula_fold NONE (K (var_occurs_naked_in_term name)) phi false
+fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum
+  | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
+    accum orelse (s = "equal" andalso member (op =) tms (ATerm (name, [])))
+fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false
+  | is_var_nonmonotonic_in_formula pos phi _ name =
+    formula_fold pos (var_occurs_positively_naked_in_term name) phi false
 
 fun tag_with_type ctxt nonmono_Ts type_sys T tm =
   CombConst (`make_fixed_const type_tag_name, T --> T, [T])
@@ -819,34 +828,38 @@
   end
 and formula_from_combformula ctxt nonmono_Ts type_sys should_predicate_on_var =
   let
+    val do_term = term_from_combterm ctxt nonmono_Ts type_sys Top_Level
     val do_bound_type =
       case type_sys of
         Simple_Types level =>
         SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level
       | _ => K NONE
-    fun do_out_of_bound_type phi (name, T) =
+    fun do_out_of_bound_type pos phi universal (name, T) =
       if should_predicate_on_type ctxt nonmono_Ts type_sys
-             (fn () => should_predicate_on_var phi name) T then
+             (fn () => should_predicate_on_var pos phi universal name) T then
         CombVar (name, T)
-        |> type_pred_combatom ctxt nonmono_Ts type_sys T
-        |> do_formula |> SOME
+        |> type_pred_combterm ctxt nonmono_Ts type_sys T
+        |> do_term |> AAtom |> SOME
       else
         NONE
-    and do_formula (AQuant (q, xs, phi)) =
-        let val phi = phi |> do_formula in
+    fun do_formula pos (AQuant (q, xs, phi)) =
+        let
+          val phi = phi |> do_formula pos
+          val universal = Option.map (q = AExists ? not) pos
+        in
           AQuant (q, xs |> map (apsnd (fn NONE => NONE
                                         | SOME T => do_bound_type T)),
                   (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
                       (map_filter
                            (fn (_, NONE) => NONE
                              | (s, SOME T) =>
-                               do_out_of_bound_type phi (s, T)) xs)
+                               do_out_of_bound_type pos phi universal (s, T))
+                           xs)
                       phi)
         end
-      | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
-      | do_formula (AAtom tm) =
-        AAtom (term_from_combterm ctxt nonmono_Ts type_sys Top_Level tm)
-  in do_formula end
+      | do_formula pos (AConn conn) = aconn_map pos do_formula conn
+      | do_formula _ (AAtom tm) = AAtom (do_term tm)
+  in do_formula o SOME end
 
 fun bound_atomic_types type_sys Ts =
   mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
@@ -857,7 +870,7 @@
   combformula
   |> close_combformula_universally
   |> formula_from_combformula ctxt nonmono_Ts type_sys
-                              var_occurs_naked_in_formula
+                              is_var_nonmonotonic_in_formula true
   |> bound_atomic_types type_sys atomic_types
   |> close_formula_universally
 
@@ -908,7 +921,7 @@
         ({name, kind, combformula, ...} : translated_formula) =
   Formula (conjecture_prefix ^ name, kind,
            formula_from_combformula ctxt nonmono_Ts type_sys
-                                    var_occurs_naked_in_formula
+                                    is_var_nonmonotonic_in_formula false
                                     (close_combformula_universally combformula)
            |> close_formula_universally, NONE, NONE)
 
@@ -1029,9 +1042,11 @@
              (if n > 1 then "_" ^ string_of_int j else ""), kind,
              CombConst ((s, s'), T, T_args)
              |> fold (curry (CombApp o swap)) bounds
-             |> type_pred_combatom ctxt nonmono_Ts type_sys res_T
+             |> type_pred_combterm ctxt nonmono_Ts type_sys res_T
+             |> AAtom
              |> mk_aquant AForall (bound_names ~~ bound_Ts)
-             |> formula_from_combformula ctxt nonmono_Ts type_sys (K (K true))
+             |> formula_from_combformula ctxt nonmono_Ts type_sys
+                                         (K (K (K (K true)))) true
              |> n > 1 ? bound_atomic_types type_sys (atyps_of T)
              |> close_formula_universally
              |> maybe_negate,