1.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Aug 22 15:02:45 2011 +0200
     1.3 @@ -386,7 +386,7 @@
     1.4                           | NONE => NONE)
     1.5                          (nth us (length us - 2))
     1.6                end
     1.7 -            else if s' = type_pred_name then
     1.8 +            else if s' = type_guard_name then
     1.9                @{const True} (* ignore type predicates *)
    1.10              else
    1.11                let

     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     2.3 @@ -55,7 +55,7 @@
     2.4    val type_decl_prefix : string
     2.5    val sym_decl_prefix : string
     2.6    val guards_sym_formula_prefix : string
     2.7 -  val lightweight_tags_sym_formula_prefix : string
     2.8 +  val tags_sym_formula_prefix : string
     2.9    val fact_prefix : string
    2.10    val conjecture_prefix : string
    2.11    val helper_prefix : string
    2.12 @@ -67,8 +67,8 @@
    2.13    val type_tag_idempotence_helper_name : string
    2.14    val predicator_name : string
    2.15    val app_op_name : string
    2.16 +  val type_guard_name : string
    2.17    val type_tag_name : string
    2.18 -  val type_pred_name : string
    2.19    val simple_type_prefix : string
    2.20    val prefixed_predicator_name : string
    2.21    val prefixed_app_op_name : string
    2.22 @@ -150,7 +150,7 @@
    2.23  val type_decl_prefix = "ty_"
    2.24  val sym_decl_prefix = "sy_"
    2.25  val guards_sym_formula_prefix = "gsy_"
    2.26 -val lightweight_tags_sym_formula_prefix = "tsy_"
    2.27 +val tags_sym_formula_prefix = "tsy_"
    2.28  val fact_prefix = "fact_"
    2.29  val conjecture_prefix = "conj_"
    2.30  val helper_prefix = "help_"
    2.31 @@ -165,8 +165,8 @@
    2.32  
    2.33  val predicator_name = "hBOOL"
    2.34  val app_op_name = "hAPP"
    2.35 -val type_tag_name = "ti"
    2.36 -val type_pred_name = "is"
    2.37 +val type_guard_name = "g"
    2.38 +val type_tag_name = "t"
    2.39  val simple_type_prefix = "ty_"
    2.40  
    2.41  val prefixed_predicator_name = const_prefix ^ predicator_name
    2.42 @@ -789,6 +789,9 @@
    2.43      ^ ")"
    2.44    | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
    2.45  
    2.46 +fun mangled_type format type_enc =
    2.47 +  generic_mangled_type_name fst o ho_term_from_typ format type_enc
    2.48 +
    2.49  val bool_atype = AType (`I tptp_bool_type)
    2.50  
    2.51  fun make_simple_type s =
    2.52 @@ -1069,7 +1072,7 @@
    2.53  
    2.54  (** Finite and infinite type inference **)
    2.55  
    2.56 -fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)
    2.57 +fun deep_freeze_atyp (TVar (_, S)) = TFree ("'frozen", S)
    2.58    | deep_freeze_atyp T = T
    2.59  val deep_freeze_type = map_atyps deep_freeze_atyp
    2.60  
    2.61 @@ -1110,8 +1113,7 @@
    2.62         case (site, is_var_or_bound_var u) of
    2.63           (Eq_Arg pos, true) =>
    2.64           (* The first disjunct prevents a subtle soundness issue explained in
    2.65 -            Blanchette's Ph.D. thesis. See also
    2.66 -            "formula_lines_for_lightweight_tags_sym_decl". *)
    2.67 +            Blanchette's Ph.D. thesis. (FIXME?) *)
    2.68           (pos <> SOME false andalso poly = Polymorphic andalso
    2.69            level <> All_Types andalso heaviness = Lightweight andalso
    2.70            exists (fn T' => type_instance ctxt (T', T)) nonmono_Ts) orelse
    2.71 @@ -1243,7 +1245,7 @@
    2.72        let val s = s |> unmangled_const_name |> invert_const in
    2.73          if s = predicator_name then 1
    2.74          else if s = app_op_name then 2
    2.75 -        else if s = type_pred_name then 1
    2.76 +        else if s = type_guard_name then 1
    2.77          else 0
    2.78        end
    2.79      | NONE => 0
    2.80 @@ -1545,10 +1547,10 @@
    2.81  
    2.82  fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
    2.83  
    2.84 -val type_pred = `make_fixed_const type_pred_name
    2.85 +val type_guard = `make_fixed_const type_guard_name
    2.86  
    2.87 -fun type_pred_iterm ctxt format type_enc T tm =
    2.88 -  IApp (IConst (type_pred, T --> @{typ bool}, [T])
    2.89 +fun type_guard_iterm ctxt format type_enc T tm =
    2.90 +  IApp (IConst (type_guard, T --> @{typ bool}, [T])
    2.91          |> enforce_type_arg_policy_in_iterm ctxt format type_enc, tm)
    2.92  
    2.93  fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
    2.94 @@ -1614,7 +1616,7 @@
    2.95        if should_predicate_on_type ctxt nonmono_Ts type_enc
    2.96               (fn () => should_predicate_on_var pos phi universal name) T then
    2.97          IVar (name, T)
    2.98 -        |> type_pred_iterm ctxt format type_enc T
    2.99 +        |> type_guard_iterm ctxt format type_enc T
   2.100          |> do_term pos |> AAtom |> SOME
   2.101        else
   2.102          NONE
   2.103 @@ -1712,9 +1714,8 @@
   2.104  fun should_declare_sym type_enc pred_sym s =
   2.105    is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
   2.106    (case type_enc of
   2.107 -     Simple_Types _ => true
   2.108 -   | Tags (_, _, Lightweight) => true
   2.109 -   | _ => not pred_sym)
   2.110 +     Guards _ => not pred_sym
   2.111 +   | _ => true)
   2.112  
   2.113  fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
   2.114                               (conjs, facts) =
   2.115 @@ -1811,6 +1812,46 @@
   2.116        []
   2.117    end
   2.118  
   2.119 +(* FIXME: do the right thing for existentials! *)
   2.120 +fun formula_line_for_guards_mono_type ctxt format nonmono_Ts type_enc T =
   2.121 +  Formula (guards_sym_formula_prefix ^
   2.122 +           ascii_of (mangled_type format type_enc T),
   2.123 +           Axiom,
   2.124 +           IConst (`make_bound_var "X", T, [])
   2.125 +           |> type_guard_iterm ctxt format type_enc T
   2.126 +           |> AAtom
   2.127 +           |> formula_from_iformula ctxt format nonmono_Ts type_enc
   2.128 +                                    (K (K (K (K true)))) (SOME true)
   2.129 +           |> bound_tvars type_enc (atyps_of T)
   2.130 +           |> close_formula_universally,
   2.131 +           isabelle_info introN, NONE)
   2.132 +
   2.133 +fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
   2.134 +  (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
   2.135 +   else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
   2.136 +  |> bound_tvars type_enc atomic_Ts
   2.137 +  |> close_formula_universally
   2.138 +
   2.139 +fun formula_line_for_tags_mono_type ctxt format nonmono_Ts type_enc T =
   2.140 +  let val x_var = ATerm (`make_bound_var "X", []) in
   2.141 +    Formula (tags_sym_formula_prefix ^
   2.142 +             ascii_of (mangled_type format type_enc T),
   2.143 +             Axiom,
   2.144 +             eq_formula type_enc (atyps_of T) false
   2.145 +                        (tag_with_type ctxt format nonmono_Ts type_enc NONE T
   2.146 +                                       x_var)
   2.147 +                        x_var,
   2.148 +             isabelle_info simpN, NONE)
   2.149 +  end
   2.150 +
   2.151 +fun problem_lines_for_mono_types ctxt format nonmono_Ts type_enc Ts =
   2.152 +  case type_enc of
   2.153 +    Simple_Types _ => []
   2.154 +  | Guards _ =>
   2.155 +    map (formula_line_for_guards_mono_type ctxt format nonmono_Ts type_enc) Ts
   2.156 +  | Tags _ =>
   2.157 +    map (formula_line_for_tags_mono_type ctxt format nonmono_Ts type_enc) Ts
   2.158 +
   2.159  fun decl_line_for_sym ctxt format nonmono_Ts type_enc s
   2.160                        (s', T_args, T, pred_sym, ary, _) =
   2.161    let
   2.162 @@ -1825,7 +1866,7 @@
   2.163    end
   2.164  
   2.165  fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind nonmono_Ts
   2.166 -        poly_nonmono_Ts type_enc n s j (s', T_args, T, _, ary, in_conj) =
   2.167 +        type_enc n s j (s', T_args, T, _, ary, in_conj) =
   2.168    let
   2.169      val (kind, maybe_negate) =
   2.170        if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
   2.171 @@ -1847,9 +1888,9 @@
   2.172               (if n > 1 then "_" ^ string_of_int j else ""), kind,
   2.173               IConst ((s, s'), T, T_args)
   2.174               |> fold (curry (IApp o swap)) bounds
   2.175 -             |> type_pred_iterm ctxt format type_enc res_T
   2.176 +             |> type_guard_iterm ctxt format type_enc res_T
   2.177               |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
   2.178 -             |> formula_from_iformula ctxt format poly_nonmono_Ts type_enc
   2.179 +             |> formula_from_iformula ctxt format nonmono_Ts type_enc
   2.180                                        (K (K (K (K true)))) (SOME true)
   2.181               |> n > 1 ? bound_tvars type_enc (atyps_of T)
   2.182               |> close_formula_universally
   2.183 @@ -1858,11 +1899,10 @@
   2.184    end
   2.185  
   2.186  fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
   2.187 -        poly_nonmono_Ts type_enc n s
   2.188 -        (j, (s', T_args, T, pred_sym, ary, in_conj)) =
   2.189 +        nonmono_Ts type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
   2.190    let
   2.191      val ident_base =
   2.192 -      lightweight_tags_sym_formula_prefix ^ s ^
   2.193 +      tags_sym_formula_prefix ^ s ^
   2.194        (if n > 1 then "_" ^ string_of_int j else "")
   2.195      val (kind, maybe_negate) =
   2.196        if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
   2.197 @@ -1872,25 +1912,13 @@
   2.198        1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
   2.199      val bounds = bound_names |> map (fn name => ATerm (name, []))
   2.200      val cst = mk_aterm format type_enc (s, s') T_args
   2.201 -    val atomic_Ts = atyps_of T
   2.202 -    fun eq tms =
   2.203 -      (if pred_sym then AConn (AIff, map AAtom tms)
   2.204 -       else AAtom (ATerm (`I tptp_equal, tms)))
   2.205 -      |> bound_tvars type_enc atomic_Ts
   2.206 -      |> close_formula_universally
   2.207 -      |> maybe_negate
   2.208 -    (* See also "should_tag_with_type". *)
   2.209 -    fun should_encode T =
   2.210 -      should_encode_type ctxt poly_nonmono_Ts All_Types T orelse
   2.211 -      (case type_enc of
   2.212 -         Tags (Polymorphic, level, Lightweight) =>
   2.213 -         level <> All_Types andalso Monomorph.typ_has_tvars T
   2.214 -       | _ => false)
   2.215 -    val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_enc NONE
   2.216 +    val eq = maybe_negate oo eq_formula type_enc (atyps_of T) pred_sym
   2.217 +    val should_encode = should_encode_type ctxt nonmono_Ts All_Types
   2.218 +    val tag_with = tag_with_type ctxt format nonmono_Ts type_enc NONE
   2.219      val add_formula_for_res =
   2.220        if should_encode res_T then
   2.221          cons (Formula (ident_base ^ "_res", kind,
   2.222 -                       eq [tag_with res_T (cst bounds), cst bounds],
   2.223 +                       eq (tag_with res_T (cst bounds)) (cst bounds),
   2.224                         isabelle_info simpN, NONE))
   2.225        else
   2.226          I
   2.227 @@ -1900,8 +1928,8 @@
   2.228            case chop k bounds of
   2.229              (bounds1, bound :: bounds2) =>
   2.230              cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
   2.231 -                           eq [cst (bounds1 @ tag_with arg_T bound :: bounds2),
   2.232 -                               cst bounds],
   2.233 +                           eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
   2.234 +                              (cst bounds),
   2.235                             isabelle_info simpN, NONE))
   2.236            | _ => raise Fail "expected nonempty tail"
   2.237          else
   2.238 @@ -1914,8 +1942,8 @@
   2.239  
   2.240  fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
   2.241  
   2.242 -fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts
   2.243 -                                poly_nonmono_Ts type_enc (s, decls) =
   2.244 +fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_enc
   2.245 +                                (s, decls) =
   2.246    case type_enc of
   2.247      Simple_Types _ =>
   2.248      decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s)
   2.249 @@ -1934,13 +1962,13 @@
   2.250          | _ => decls
   2.251        val n = length decls
   2.252        val decls =
   2.253 -        decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_enc
   2.254 -                                                  (K true)
   2.255 +        decls |> filter (should_encode_type ctxt nonmono_Ts
   2.256 +                             (level_of_type_enc type_enc)
   2.257                           o result_type_of_decl)
   2.258      in
   2.259        (0 upto length decls - 1, decls)
   2.260        |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind
   2.261 -                   nonmono_Ts poly_nonmono_Ts type_enc n s)
   2.262 +                                                 nonmono_Ts type_enc n s)
   2.263      end
   2.264    | Tags (_, _, heaviness) =>
   2.265      (case heaviness of
   2.266 @@ -1949,14 +1977,28 @@
   2.267         let val n = length decls in
   2.268           (0 upto n - 1 ~~ decls)
   2.269           |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
   2.270 -                      conj_sym_kind poly_nonmono_Ts type_enc n s)
   2.271 +                      conj_sym_kind nonmono_Ts type_enc n s)
   2.272         end)
   2.273  
   2.274  fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
   2.275 -                                     poly_nonmono_Ts type_enc sym_decl_tab =
   2.276 -  sym_decl_tab |> Symtab.dest |> sort_wrt fst |> rpair []
   2.277 -  |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
   2.278 -                             nonmono_Ts poly_nonmono_Ts type_enc)
   2.279 +                                     type_enc sym_decl_tab =
   2.280 +  let
   2.281 +    val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
   2.282 +    val mono_Ts =
   2.283 +      if polymorphism_of_type_enc type_enc = Polymorphic then
   2.284 +        syms |> maps (map result_type_of_decl o snd)
   2.285 +             |> filter_out (should_encode_type ctxt nonmono_Ts
   2.286 +                                (level_of_type_enc type_enc))
   2.287 +             |> rpair [] |-> fold (insert_type ctxt I)
   2.288 +      else
   2.289 +        []
   2.290 +    val mono_lines =
   2.291 +      problem_lines_for_mono_types ctxt format nonmono_Ts type_enc mono_Ts
   2.292 +    val decl_lines =
   2.293 +      fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
   2.294 +                                                     nonmono_Ts type_enc)
   2.295 +               syms []
   2.296 +  in mono_lines @ decl_lines end
   2.297  
   2.298  fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
   2.299      poly <> Mangled_Monomorphic andalso
   2.300 @@ -2024,21 +2066,15 @@
   2.301      val helpers =
   2.302        repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
   2.303                         |> map repair
   2.304 -    val poly_nonmono_Ts =
   2.305 -      if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] (* FIXME? *) orelse
   2.306 -         polymorphism_of_type_enc type_enc <> Polymorphic then
   2.307 -        nonmono_Ts
   2.308 -      else
   2.309 -        [tvar_a]
   2.310      val sym_decl_lines =
   2.311        (conjs, helpers @ facts)
   2.312        |> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
   2.313        |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
   2.314 -                                               poly_nonmono_Ts type_enc
   2.315 +                                               type_enc
   2.316      val helper_lines =
   2.317        0 upto length helpers - 1 ~~ helpers
   2.318        |> map (formula_line_for_fact ctxt format helper_prefix I false true
   2.319 -                                    poly_nonmono_Ts type_enc)
   2.320 +                                    nonmono_Ts type_enc)
   2.321        |> (if needs_type_tag_idempotence type_enc then
   2.322              cons (type_tag_idempotence_fact ())
   2.323            else

     3.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     3.3 @@ -141,7 +141,7 @@
     3.4                    |> Metis_Thm.axiom, isa)
     3.5      in
     3.6        if ident = type_tag_idempotence_helper_name orelse
     3.7 -         String.isPrefix lightweight_tags_sym_formula_prefix ident then
     3.8 +         String.isPrefix tags_sym_formula_prefix ident then
     3.9          Isa_Reflexive_or_Trivial |> some
    3.10        else if String.isPrefix conjecture_prefix ident then
    3.11          NONE