# HG changeset patch
# User blanchet
# Date 1340034606 -7200
# Node ID a0e4618d6fed61743f13b84d2faaea1feebf6a52
# Parent  d2173ff80c5748c288177f4e5c922d2b2518622b
sound monotonicity inference in the presence of "aggressive" helpers

diff -r d2173ff80c57 -r a0e4618d6fed src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jun 18 17:50:06 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jun 18 17:50:06 2012 +0200
@@ -2224,13 +2224,13 @@
   end
 
 (* We add "bool" in case the helper "True_or_False" is included later. *)
-fun default_mono level =
+fun default_mono level aggressive =
   {maybe_finite_Ts = [@{typ bool}],
    surely_infinite_Ts =
      case level of
        Nonmono_Types (Strict, _) => []
      | _ => known_infinite_types,
-   maybe_nonmono_Ts = [@{typ bool}]}
+   maybe_nonmono_Ts = [if aggressive then tvar_a else @{typ bool}]}
 
 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
    out with monotonicity" paper presented at CADE 2011. *)
@@ -2262,9 +2262,9 @@
 fun add_fact_mononotonicity_info ctxt level ({role, iformula, ...} : ifact) =
   formula_fold (SOME (role <> Conjecture))
                (add_iterm_mononotonicity_info ctxt level) iformula
-fun mononotonicity_info_for_facts ctxt type_enc facts =
+fun mononotonicity_info_for_facts ctxt type_enc aggressive facts =
   let val level = level_of_type_enc type_enc in
-    default_mono level
+    default_mono level aggressive
     |> is_type_level_monotonicity_based level
        ? fold (add_fact_mononotonicity_info ctxt level) facts
   end
@@ -2648,7 +2648,8 @@
                          concl_t facts
     val (_, sym_tab0) =
       sym_table_for_facts ctxt type_enc app_op_level conjs facts
-    val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
+    val mono =
+      conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc aggressive
     val constrs = all_constrs_of_polymorphic_datatypes thy
     fun firstorderize in_helper =
       firstorderize_fact thy constrs type_enc sym_tab0