extended simple types with polymorphism -- the implementation still needs some work though

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 30 16:07:45 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 30 16:07:45 2011 +0200
@@ -576,7 +576,7 @@
             relevance_override
       in
         if !reconstructor = "sledgehammer_tac" then
-          sledge_tac 0.25 ATP_Systems.z3_tptpN "simple"
+          sledge_tac 0.25 ATP_Systems.z3_tptpN "mono_simple"
           ORELSE' sledge_tac 0.25 ATP_Systems.eN "mono_guards?"
           ORELSE' sledge_tac 0.25 ATP_Systems.spassN "poly_tags_uniform"
           ORELSE' Metis_Tactics.metis_tac [] ctxt thms

--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 30 16:07:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 30 16:07:45 2011 +0200
@@ -243,8 +243,10 @@
    prem_kind = Hypothesis,
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.667, (false, (150, THF0 THF_Without_Choice, "simple_higher", sosN))),
-      (0.333, (true, (50, THF0 THF_Without_Choice, "simple_higher", no_sosN)))]
+     [(0.667, (false, (150, THF0 THF_Without_Choice,
+                       "mono_simple_higher", sosN))),
+      (0.333, (true, (50, THF0 THF_Without_Choice,
+                      "mono_simple_higher", no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -264,7 +266,7 @@
    conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
    best_slices =
-     K [(1.0, (true, (100, THF0 THF_With_Choice, "simple_higher", "")))]
+     K [(1.0, (true, (100, THF0 THF_With_Choice, "mono_simple_higher", "")))]
      (* FUDGE *)}
 
 val satallax = (satallaxN, satallax_config)
@@ -346,8 +348,8 @@
          (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))]
       else
         [(0.333, (false, (150, vampire_tff, "poly_guards", sosN))),
-         (0.333, (false, (500, vampire_tff, "simple", sosN))),
-         (0.334, (true, (50, vampire_tff, "simple", no_sosN)))])
+         (0.333, (false, (500, vampire_tff, "mono_simple", sosN))),
+         (0.334, (true, (50, vampire_tff, "mono_simple", no_sosN)))])
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -375,10 +377,10 @@
    prem_kind = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(0.5, (false, (250, z3_tff, "simple", ""))),
-        (0.25, (false, (125, z3_tff, "simple", ""))),
-        (0.125, (false, (62, z3_tff, "simple", ""))),
-        (0.125, (false, (31, z3_tff, "simple", "")))]}
+     K [(0.5, (false, (250, z3_tff, "mono_simple", ""))),
+        (0.25, (false, (125, z3_tff, "mono_simple", ""))),
+        (0.125, (false, (62, z3_tff, "mono_simple", ""))),
+        (0.125, (false, (31, z3_tff, "mono_simple", "")))]}
 
 val z3_tptp = (z3_tptpN, z3_tptp_config)
 
@@ -480,25 +482,27 @@
                (K (750, FOF, "mono_tags?") (* FUDGE *))
 val remote_leo2 =
   remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
-               (K (100, THF0 THF_Without_Choice, "simple_higher") (* FUDGE *))
+               (K (100, THF0 THF_Without_Choice,
+                   "mono_simple_higher") (* FUDGE *))
 val remote_satallax =
   remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
-               (K (100, THF0 THF_With_Choice, "simple_higher") (* FUDGE *))
+               (K (100, THF0 THF_With_Choice,
+                   "mono_simple_higher") (* FUDGE *))
 val remote_vampire =
   remotify_atp vampire "Vampire" ["1.8"]
                (K (250, FOF, "mono_guards?") (* FUDGE *))
 val remote_z3_tptp =
-  remotify_atp z3_tptp "Z3" ["3.0"] (K (250, z3_tff, "simple") (* FUDGE *))
+  remotify_atp z3_tptp "Z3" ["3.0"] (K (250, z3_tff, "mono_simple") (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
              Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
-             (K (100, dumb_tff, "simple") (* FUDGE *))
+             (K (100, dumb_tff, "mono_simple") (* FUDGE *))
 val remote_e_tofof =
   remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
-             Hypothesis (K (150, dumb_tff, "simple") (* FUDGE *))
+             Hypothesis (K (150, dumb_tff, "mono_simple") (* FUDGE *))
 val remote_waldmeister =
   remote_atp waldmeisterN "Waldmeister" ["710"]
              [("#START OF PROOF", "Proved Goals:")]

--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:07:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 30 16:07:45 2011 +0200
@@ -31,7 +31,7 @@
   datatype type_uniformity = Uniform | Nonuniform
 
   datatype type_enc =
-    Simple_Types of order * type_level |
+    Simple_Types of order * polymorphism * type_level |
     Guards of polymorphism * type_level * type_uniformity |
     Tags of polymorphism * type_level * type_uniformity
 
@@ -547,7 +547,7 @@
 datatype type_uniformity = Uniform | Nonuniform
 
 datatype type_enc =
-  Simple_Types of order * type_level |
+  Simple_Types of order * polymorphism * type_level |
   Guards of polymorphism * type_level * type_uniformity |
   Tags of polymorphism * type_level * type_uniformity
 
@@ -579,12 +579,15 @@
                 | NONE => (Nonuniform, s))
   |> (fn (poly, (level, (uniformity, core))) =>
          case (core, (poly, level, uniformity)) of
-           ("simple", (NONE, _, Nonuniform)) =>
-           Simple_Types (First_Order, level)
-         | ("simple_higher", (NONE, _, Nonuniform)) =>
-           (case level of
-              Noninf_Nonmono_Types _ => raise Same.SAME
-            | _ => Simple_Types (Higher_Order, level))
+           ("simple", (SOME poly, _, Nonuniform)) =>
+           (case poly of
+              Raw_Monomorphic => raise Same.SAME
+            | _ => Simple_Types (First_Order, poly, level))
+         | ("simple_higher", (SOME poly, _, Nonuniform)) =>
+           (case (poly, level) of
+              (Raw_Monomorphic, _) => raise Same.SAME
+            | (_, Noninf_Nonmono_Types _) => raise Same.SAME
+            | _ => Simple_Types (Higher_Order, poly, level))
          | ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity)
          | ("tags", (SOME Polymorphic, _, _)) =>
            Tags (Polymorphic, level, uniformity)
@@ -596,14 +599,14 @@
          | _ => raise Same.SAME)
   handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
 
-fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true
+fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true
   | is_type_enc_higher_order _ = false
 
-fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic
+fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly
   | polymorphism_of_type_enc (Guards (poly, _, _)) = poly
   | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
 
-fun level_of_type_enc (Simple_Types (_, level)) = level
+fun level_of_type_enc (Simple_Types (_, _, level)) = level
   | level_of_type_enc (Guards (_, level, _)) = level
   | level_of_type_enc (Tags (_, level, _)) = level
 
@@ -625,11 +628,15 @@
   | is_type_level_monotonicity_based Fin_Nonmono_Types = true
   | is_type_level_monotonicity_based _ = false
 
-fun adjust_type_enc (THF0 _) type_enc = type_enc
-  | adjust_type_enc (TFF _) (Simple_Types (_, level)) =
-    Simple_Types (First_Order, level)
-  | adjust_type_enc format (Simple_Types (_, level)) =
-    adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform))
+fun adjust_type_enc (THF0 _) (Simple_Types (order, Polymorphic, level)) =
+    Simple_Types (order, Mangled_Monomorphic, level)
+  | adjust_type_enc (THF0 _) type_enc = type_enc
+  | adjust_type_enc (TFF (TFF_Monomorphic, _)) (Simple_Types (_, _, level)) =
+    Simple_Types (First_Order, Mangled_Monomorphic, level)
+  | adjust_type_enc (TFF (_, _)) (Simple_Types (_, poly, level)) =
+    Simple_Types (First_Order, poly, level)
+  | adjust_type_enc format (Simple_Types (_, poly, level)) =
+    adjust_type_enc format (Guards (poly, level, Uniform))
   | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
     (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
   | adjust_type_enc _ type_enc = type_enc
@@ -1662,7 +1669,7 @@
     val do_term = ho_term_from_iterm ctxt format mono type_enc o Top_Level
     val do_bound_type =
       case type_enc of
-        Simple_Types (_, level) =>
+        Simple_Types (_, _, level) =>
         homogenized_type ctxt mono level 0
         #> ho_type_from_typ format type_enc false 0 #> SOME
       | _ => K NONE
@@ -1940,7 +1947,7 @@
   let
     val (T_arg_Ts, level) =
       case type_enc of
-        Simple_Types (_, level) => ([], level)
+        Simple_Types (_, _, level) => ([], level)
       | _ => (replicate (length T_args) homo_infinite_type, No_Types)
   in
     Decl (sym_decl_prefix ^ s, (s, s'),

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 30 16:07:45 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 30 16:07:45 2011 +0200
@@ -148,8 +148,8 @@
                             | _ => value)
     | NONE => (name, value)
 
-(* Ensure that type systems such as "simple!" and "mono_guards?" are handled
-   correctly. *)
+(* Ensure that type systems such as "mono_simple!" and "mono_guards?" are
+   handled correctly. *)
 fun implode_param [s, "?"] = s ^ "?"
   | implode_param [s, "!"] = s ^ "!"
   | implode_param ss = space_implode " " ss