src/HOL/Tools/Nitpick/nitpick_mono.ML
author blanchet
Sat Apr 24 16:33:01 2010 +0200 (2010-04-24)
changeset 36385 ff5f88702590
parent 35832 1dac16f00cd2
child 37256 0dca1ec52999
permissions -rw-r--r--
remove type annotations as comments;
Nitpick is now 1136 lines shorter
     1 (*  Title:      HOL/Tools/Nitpick/nitpick_mono.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009, 2010
     4 
     5 Monotonicity inference for higher-order logic.
     6 *)
     7 
     8 signature NITPICK_MONO =
     9 sig
    10   type hol_context = Nitpick_HOL.hol_context
    11 
    12   val formulas_monotonic :
    13     hol_context -> bool -> typ -> term list * term list -> bool
    14   val finitize_funs :
    15     hol_context -> bool -> (typ option * bool option) list -> typ
    16     -> term list * term list -> term list * term list
    17 end;
    18 
    19 structure Nitpick_Mono : NITPICK_MONO =
    20 struct
    21 
    22 open Nitpick_Util
    23 open Nitpick_HOL
    24 
    25 type var = int
    26 
    27 datatype sign = Plus | Minus
    28 datatype sign_atom = S of sign | V of var
    29 
    30 type literal = var * sign
    31 
    32 datatype mtyp =
    33   MAlpha |
    34   MFun of mtyp * sign_atom * mtyp |
    35   MPair of mtyp * mtyp |
    36   MType of string * mtyp list |
    37   MRec of string * typ list
    38 
    39 datatype mterm =
    40   MRaw of term * mtyp |
    41   MAbs of string * typ * mtyp * sign_atom * mterm |
    42   MApp of mterm * mterm
    43 
    44 type mdata =
    45   {hol_ctxt: hol_context,
    46    binarize: bool,
    47    alpha_T: typ,
    48    no_harmless: bool,
    49    max_fresh: int Unsynchronized.ref,
    50    datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
    51    constr_mcache: (styp * mtyp) list Unsynchronized.ref}
    52 
    53 exception UNSOLVABLE of unit
    54 exception MTYPE of string * mtyp list * typ list
    55 exception MTERM of string * mterm list
    56 
    57 fun print_g (_ : string) = ()
    58 (* val print_g = tracing *)
    59 
    60 val string_for_var = signed_string_of_int
    61 fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>"
    62   | string_for_vars sep xs = space_implode sep (map string_for_var xs)
    63 fun subscript_string_for_vars sep xs =
    64   if null xs then "" else "\<^bsub>" ^ string_for_vars sep xs ^ "\<^esub>"
    65 
    66 fun string_for_sign Plus = "+"
    67   | string_for_sign Minus = "-"
    68 
    69 fun xor sn1 sn2 = if sn1 = sn2 then Plus else Minus
    70 val negate = xor Minus
    71 
    72 fun string_for_sign_atom (S sn) = string_for_sign sn
    73   | string_for_sign_atom (V x) = string_for_var x
    74 
    75 fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn
    76 
    77 val bool_M = MType (@{type_name bool}, [])
    78 val dummy_M = MType (nitpick_prefix ^ "dummy", [])
    79 
    80 fun is_MRec (MRec _) = true
    81   | is_MRec _ = false
    82 fun dest_MFun (MFun z) = z
    83   | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M], [])
    84 
    85 val no_prec = 100
    86 
    87 fun precedence_of_mtype (MFun _) = 1
    88   | precedence_of_mtype (MPair _) = 2
    89   | precedence_of_mtype _ = no_prec
    90 
    91 val string_for_mtype =
    92   let
    93     fun aux outer_prec M =
    94       let
    95         val prec = precedence_of_mtype M
    96         val need_parens = (prec < outer_prec)
    97       in
    98         (if need_parens then "(" else "") ^
    99         (if M = dummy_M then
   100            "_"
   101          else case M of
   102              MAlpha => "\<alpha>"
   103            | MFun (M1, a, M2) =>
   104              aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^
   105              string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2
   106            | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2
   107            | MType (s, []) =>
   108              if s = @{type_name prop} orelse s = @{type_name bool} then "o"
   109              else s
   110            | MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s
   111            | MRec (s, _) => "[" ^ s ^ "]") ^
   112         (if need_parens then ")" else "")
   113       end
   114   in aux 0 end
   115 
   116 fun flatten_mtype (MPair (M1, M2)) = maps flatten_mtype [M1, M2]
   117   | flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms
   118   | flatten_mtype M = [M]
   119 
   120 fun precedence_of_mterm (MRaw _) = no_prec
   121   | precedence_of_mterm (MAbs _) = 1
   122   | precedence_of_mterm (MApp _) = 2
   123 
   124 fun string_for_mterm ctxt =
   125   let
   126     fun mtype_annotation M = "\<^bsup>" ^ string_for_mtype M ^ "\<^esup>"
   127     fun aux outer_prec m =
   128       let
   129         val prec = precedence_of_mterm m
   130         val need_parens = (prec < outer_prec)
   131       in
   132         (if need_parens then "(" else "") ^
   133         (case m of
   134            MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
   135          | MAbs (s, _, M, a, m) =>
   136            "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
   137            string_for_sign_atom a ^ "\<^esup> " ^ aux prec m
   138          | MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^
   139         (if need_parens then ")" else "")
   140       end
   141   in aux 0 end
   142 
   143 fun mtype_of_mterm (MRaw (_, M)) = M
   144   | mtype_of_mterm (MAbs (_, _, M, a, m)) = MFun (M, a, mtype_of_mterm m)
   145   | mtype_of_mterm (MApp (m1, _)) =
   146     case mtype_of_mterm m1 of
   147       MFun (_, _, M12) => M12
   148     | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1], [])
   149 
   150 fun strip_mcomb (MApp (m1, m2)) = strip_mcomb m1 ||> (fn ms => append ms [m2])
   151   | strip_mcomb m = (m, [])
   152 
   153 fun initial_mdata hol_ctxt binarize no_harmless alpha_T =
   154   ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
   155     no_harmless = no_harmless, max_fresh = Unsynchronized.ref 0,
   156     datatype_mcache = Unsynchronized.ref [],
   157     constr_mcache = Unsynchronized.ref []} : mdata)
   158 
   159 fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
   160     T = alpha_T orelse (not (is_fp_iterator_type T) andalso
   161                         exists (could_exist_alpha_subtype alpha_T) Ts)
   162   | could_exist_alpha_subtype alpha_T T = (T = alpha_T)
   163 fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
   164     could_exist_alpha_subtype alpha_T T
   165   | could_exist_alpha_sub_mtype thy alpha_T T =
   166     (T = alpha_T orelse is_datatype thy [(NONE, true)] T)
   167 
   168 fun exists_alpha_sub_mtype MAlpha = true
   169   | exists_alpha_sub_mtype (MFun (M1, _, M2)) =
   170     exists exists_alpha_sub_mtype [M1, M2]
   171   | exists_alpha_sub_mtype (MPair (M1, M2)) =
   172     exists exists_alpha_sub_mtype [M1, M2]
   173   | exists_alpha_sub_mtype (MType (_, Ms)) = exists exists_alpha_sub_mtype Ms
   174   | exists_alpha_sub_mtype (MRec _) = true
   175 
   176 fun exists_alpha_sub_mtype_fresh MAlpha = true
   177   | exists_alpha_sub_mtype_fresh (MFun (_, V _, _)) = true
   178   | exists_alpha_sub_mtype_fresh (MFun (_, _, M2)) =
   179     exists_alpha_sub_mtype_fresh M2
   180   | exists_alpha_sub_mtype_fresh (MPair (M1, M2)) =
   181     exists exists_alpha_sub_mtype_fresh [M1, M2]
   182   | exists_alpha_sub_mtype_fresh (MType (_, Ms)) =
   183     exists exists_alpha_sub_mtype_fresh Ms
   184   | exists_alpha_sub_mtype_fresh (MRec _) = true
   185 
   186 fun constr_mtype_for_binders z Ms =
   187   fold_rev (fn M => curry3 MFun M (S Minus)) Ms (MRec z)
   188 
   189 fun repair_mtype _ _ MAlpha = MAlpha
   190   | repair_mtype cache seen (MFun (M1, a, M2)) =
   191     MFun (repair_mtype cache seen M1, a, repair_mtype cache seen M2)
   192   | repair_mtype cache seen (MPair Mp) =
   193     MPair (pairself (repair_mtype cache seen) Mp)
   194   | repair_mtype cache seen (MType (s, Ms)) =
   195     MType (s, maps (flatten_mtype o repair_mtype cache seen) Ms)
   196   | repair_mtype cache seen (MRec (z as (s, _))) =
   197     case AList.lookup (op =) cache z |> the of
   198       MRec _ => MType (s, [])
   199     | M => if member (op =) seen M then MType (s, [])
   200            else repair_mtype cache (M :: seen) M
   201 
   202 fun repair_datatype_mcache cache =
   203   let
   204     fun repair_one (z, M) =
   205       Unsynchronized.change cache
   206           (AList.update (op =) (z, repair_mtype (!cache) [] M))
   207   in List.app repair_one (rev (!cache)) end
   208 
   209 fun repair_constr_mcache dtype_cache constr_mcache =
   210   let
   211     fun repair_one (x, M) =
   212       Unsynchronized.change constr_mcache
   213           (AList.update (op =) (x, repair_mtype dtype_cache [] M))
   214   in List.app repair_one (!constr_mcache) end
   215 
   216 fun is_fin_fun_supported_type @{typ prop} = true
   217   | is_fin_fun_supported_type @{typ bool} = true
   218   | is_fin_fun_supported_type (Type (@{type_name option}, _)) = true
   219   | is_fin_fun_supported_type _ = false
   220 fun fin_fun_body _ _ (t as @{term False}) = SOME t
   221   | fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t
   222   | fin_fun_body dom_T ran_T
   223                  ((t0 as Const (@{const_name If}, _))
   224                   $ (t1 as Const (@{const_name "op ="}, _) $ Bound 0 $ t1')
   225                   $ t2 $ t3) =
   226     (if loose_bvar1 (t1', 0) then
   227        NONE
   228      else case fin_fun_body dom_T ran_T t3 of
   229        NONE => NONE
   230      | SOME t3 =>
   231        SOME (t0 $ (Const (@{const_name is_unknown}, dom_T --> bool_T) $ t1')
   232                 $ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
   233   | fin_fun_body _ _ _ = NONE
   234 
   235 fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) all_minus
   236                             T1 T2 =
   237   let
   238     val M1 = fresh_mtype_for_type mdata all_minus T1
   239     val M2 = fresh_mtype_for_type mdata all_minus T2
   240     val a = if not all_minus andalso exists_alpha_sub_mtype_fresh M1 andalso
   241                is_fin_fun_supported_type (body_type T2) then
   242               V (Unsynchronized.inc max_fresh)
   243             else
   244               S Minus
   245   in (M1, a, M2) end
   246 and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
   247                                     datatype_mcache, constr_mcache, ...})
   248                          all_minus =
   249   let
   250     fun do_type T =
   251       if T = alpha_T then
   252         MAlpha
   253       else case T of
   254         Type (@{type_name fun}, [T1, T2]) =>
   255         MFun (fresh_mfun_for_fun_type mdata false T1 T2)
   256       | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
   257       | Type (z as (s, _)) =>
   258         if could_exist_alpha_sub_mtype thy alpha_T T then
   259           case AList.lookup (op =) (!datatype_mcache) z of
   260             SOME M => M
   261           | NONE =>
   262             let
   263               val _ = Unsynchronized.change datatype_mcache (cons (z, MRec z))
   264               val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
   265               val (all_Ms, constr_Ms) =
   266                 fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) =>
   267                              let
   268                                val binder_Ms = map do_type (binder_types T')
   269                                val new_Ms = filter exists_alpha_sub_mtype_fresh
   270                                                    binder_Ms
   271                                val constr_M = constr_mtype_for_binders z
   272                                                                        binder_Ms
   273                              in
   274                                (union (op =) new_Ms all_Ms,
   275                                 constr_M :: constr_Ms)
   276                              end)
   277                          xs ([], [])
   278               val M = MType (s, all_Ms)
   279               val _ = Unsynchronized.change datatype_mcache
   280                           (AList.update (op =) (z, M))
   281               val _ = Unsynchronized.change constr_mcache
   282                           (append (xs ~~ constr_Ms))
   283             in
   284               if forall (not o is_MRec o snd) (!datatype_mcache) then
   285                 (repair_datatype_mcache datatype_mcache;
   286                  repair_constr_mcache (!datatype_mcache) constr_mcache;
   287                  AList.lookup (op =) (!datatype_mcache) z |> the)
   288               else
   289                 M
   290             end
   291         else
   292           MType (s, [])
   293       | _ => MType (Refute.string_of_typ T, [])
   294   in do_type end
   295 
   296 fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
   297   | prodM_factors M = [M]
   298 fun curried_strip_mtype (MFun (M1, _, M2)) =
   299     curried_strip_mtype M2 |>> append (prodM_factors M1)
   300   | curried_strip_mtype M = ([], M)
   301 fun sel_mtype_from_constr_mtype s M =
   302   let val (arg_Ms, dataM) = curried_strip_mtype M in
   303     MFun (dataM, S Minus,
   304           case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n)
   305   end
   306 
   307 fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_mcache,
   308                                 ...}) (x as (_, T)) =
   309   if could_exist_alpha_sub_mtype thy alpha_T T then
   310     case AList.lookup (op =) (!constr_mcache) x of
   311       SOME M => M
   312     | NONE => if T = alpha_T then
   313                 let val M = fresh_mtype_for_type mdata false T in
   314                   (Unsynchronized.change constr_mcache (cons (x, M)); M)
   315                 end
   316               else
   317                 (fresh_mtype_for_type mdata false (body_type T);
   318                  AList.lookup (op =) (!constr_mcache) x |> the)
   319   else
   320     fresh_mtype_for_type mdata false T
   321 fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
   322   x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
   323     |> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
   324 
   325 fun resolve_sign_atom lits (V x) =
   326     x |> AList.lookup (op =) lits |> Option.map S |> the_default (V x)
   327   | resolve_sign_atom _ a = a
   328 fun resolve_mtype lits =
   329   let
   330     fun aux MAlpha = MAlpha
   331       | aux (MFun (M1, a, M2)) = MFun (aux M1, resolve_sign_atom lits a, aux M2)
   332       | aux (MPair Mp) = MPair (pairself aux Mp)
   333       | aux (MType (s, Ms)) = MType (s, map aux Ms)
   334       | aux (MRec z) = MRec z
   335   in aux end
   336 
   337 datatype comp_op = Eq | Leq
   338 
   339 type comp = sign_atom * sign_atom * comp_op * var list
   340 type sign_expr = literal list
   341 
   342 type constraint_set = literal list * comp list * sign_expr list
   343 
   344 fun string_for_comp_op Eq = "="
   345   | string_for_comp_op Leq = "\<le>"
   346 
   347 fun string_for_sign_expr [] = "\<bot>"
   348   | string_for_sign_expr lits =
   349     space_implode " \<or> " (map string_for_literal lits)
   350 
   351 fun do_literal _ NONE = NONE
   352   | do_literal (x, sn) (SOME lits) =
   353     case AList.lookup (op =) lits x of
   354       SOME sn' => if sn = sn' then SOME lits else NONE
   355     | NONE => SOME ((x, sn) :: lits)
   356 
   357 fun do_sign_atom_comp Eq [] a1 a2 (accum as (lits, comps)) =
   358     (case (a1, a2) of
   359        (S sn1, S sn2) => if sn1 = sn2 then SOME accum else NONE
   360      | (V x1, S sn2) =>
   361        Option.map (rpair comps) (do_literal (x1, sn2) (SOME lits))
   362      | (V _, V _) => SOME (lits, insert (op =) (a1, a2, Eq, []) comps)
   363      | _ => do_sign_atom_comp Eq [] a2 a1 accum)
   364   | do_sign_atom_comp Leq [] a1 a2 (accum as (lits, comps)) =
   365     (case (a1, a2) of
   366        (_, S Minus) => SOME accum
   367      | (S Plus, _) => SOME accum
   368      | (S Minus, S Plus) => NONE
   369      | (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps)
   370      | _ => do_sign_atom_comp Eq [] a1 a2 accum)
   371   | do_sign_atom_comp cmp xs a1 a2 (lits, comps) =
   372     SOME (lits, insert (op =) (a1, a2, cmp, xs) comps)
   373 
   374 fun do_mtype_comp _ _ _ _ NONE = NONE
   375   | do_mtype_comp _ _ MAlpha MAlpha accum = accum
   376   | do_mtype_comp Eq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
   377                   (SOME accum) =
   378      accum |> do_sign_atom_comp Eq xs a1 a2 |> do_mtype_comp Eq xs M11 M21
   379            |> do_mtype_comp Eq xs M12 M22
   380   | do_mtype_comp Leq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
   381                   (SOME accum) =
   382     (if exists_alpha_sub_mtype M11 then
   383        accum |> do_sign_atom_comp Leq xs a1 a2
   384              |> do_mtype_comp Leq xs M21 M11
   385              |> (case a2 of
   386                    S Minus => I
   387                  | S Plus => do_mtype_comp Leq xs M11 M21
   388                  | V x => do_mtype_comp Leq (x :: xs) M11 M21)
   389      else
   390        SOME accum)
   391     |> do_mtype_comp Leq xs M12 M22
   392   | do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22))
   393                   accum =
   394     (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
   395      handle Library.UnequalLengths =>
   396             raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2], []))
   397   | do_mtype_comp _ _ (MType _) (MType _) accum =
   398     accum (* no need to compare them thanks to the cache *)
   399   | do_mtype_comp cmp _ M1 M2 _ =
   400     raise MTYPE ("Nitpick_Mono.do_mtype_comp (" ^ string_for_comp_op cmp ^ ")",
   401                  [M1, M2], [])
   402 
   403 fun add_mtype_comp cmp M1 M2 ((lits, comps, sexps) : constraint_set) =
   404     (print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^
   405               " " ^ string_for_mtype M2);
   406      case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of
   407        NONE => (print_g "**** Unsolvable"; raise UNSOLVABLE ())
   408      | SOME (lits, comps) => (lits, comps, sexps))
   409 
   410 val add_mtypes_equal = add_mtype_comp Eq
   411 val add_is_sub_mtype = add_mtype_comp Leq
   412 
   413 fun do_notin_mtype_fv _ _ _ NONE = NONE
   414   | do_notin_mtype_fv Minus _ MAlpha accum = accum
   415   | do_notin_mtype_fv Plus [] MAlpha _ = NONE
   416   | do_notin_mtype_fv Plus [(x, sn)] MAlpha (SOME (lits, sexps)) =
   417     SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps)
   418   | do_notin_mtype_fv Plus sexp MAlpha (SOME (lits, sexps)) =
   419     SOME (lits, insert (op =) sexp sexps)
   420   | do_notin_mtype_fv sn sexp (MFun (M1, S sn', M2)) accum =
   421     accum |> (if sn' = Plus andalso sn = Plus then
   422                 do_notin_mtype_fv Plus sexp M1
   423               else
   424                 I)
   425           |> (if sn' = Minus orelse sn = Plus then
   426                 do_notin_mtype_fv Minus sexp M1
   427               else
   428                 I)
   429           |> do_notin_mtype_fv sn sexp M2
   430   | do_notin_mtype_fv Plus sexp (MFun (M1, V x, M2)) accum =
   431     accum |> (case do_literal (x, Minus) (SOME sexp) of
   432                 NONE => I
   433               | SOME sexp' => do_notin_mtype_fv Plus sexp' M1)
   434           |> do_notin_mtype_fv Minus sexp M1
   435           |> do_notin_mtype_fv Plus sexp M2
   436   | do_notin_mtype_fv Minus sexp (MFun (M1, V x, M2)) accum =
   437     accum |> (case do_literal (x, Plus) (SOME sexp) of
   438                 NONE => I
   439               | SOME sexp' => do_notin_mtype_fv Plus sexp' M1)
   440           |> do_notin_mtype_fv Minus sexp M2
   441   | do_notin_mtype_fv sn sexp (MPair (M1, M2)) accum =
   442     accum |> fold (do_notin_mtype_fv sn sexp) [M1, M2]
   443   | do_notin_mtype_fv sn sexp (MType (_, Ms)) accum =
   444     accum |> fold (do_notin_mtype_fv sn sexp) Ms
   445   | do_notin_mtype_fv _ _ M _ =
   446     raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
   447 
   448 fun add_notin_mtype_fv sn M ((lits, comps, sexps) : constraint_set) =
   449     (print_g ("*** Add " ^ string_for_mtype M ^ " is " ^
   450               (case sn of Minus => "concrete" | Plus => "complete") ^ ".");
   451      case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
   452        NONE => (print_g "**** Unsolvable"; raise UNSOLVABLE ())
   453      | SOME (lits, sexps) => (lits, comps, sexps))
   454 
   455 val add_mtype_is_concrete = add_notin_mtype_fv Minus
   456 val add_mtype_is_complete = add_notin_mtype_fv Plus
   457 
   458 val bool_from_minus = true
   459 
   460 fun bool_from_sign Plus = not bool_from_minus
   461   | bool_from_sign Minus = bool_from_minus
   462 fun sign_from_bool b = if b = bool_from_minus then Minus else Plus
   463 
   464 fun prop_for_literal (x, sn) =
   465   (not (bool_from_sign sn) ? PropLogic.Not) (PropLogic.BoolVar x)
   466 fun prop_for_sign_atom_eq (S sn', sn) =
   467     if sn = sn' then PropLogic.True else PropLogic.False
   468   | prop_for_sign_atom_eq (V x, sn) = prop_for_literal (x, sn)
   469 fun prop_for_sign_expr xs = PropLogic.exists (map prop_for_literal xs)
   470 fun prop_for_exists_eq xs sn =
   471   PropLogic.exists (map (fn x => prop_for_literal (x, sn)) xs)
   472 fun prop_for_comp (a1, a2, Eq, []) =
   473     PropLogic.SAnd (prop_for_comp (a1, a2, Leq, []),
   474                     prop_for_comp (a2, a1, Leq, []))
   475   | prop_for_comp (a1, a2, Leq, []) =
   476     PropLogic.SOr (prop_for_sign_atom_eq (a1, Plus),
   477                    prop_for_sign_atom_eq (a2, Minus))
   478   | prop_for_comp (a1, a2, cmp, xs) =
   479     PropLogic.SOr (prop_for_exists_eq xs Minus, prop_for_comp (a1, a2, cmp, []))
   480 
   481 fun literals_from_assignments max_var assigns lits =
   482   fold (fn x => fn accum =>
   483            if AList.defined (op =) lits x then
   484              accum
   485            else case assigns x of
   486              SOME b => (x, sign_from_bool b) :: accum
   487            | NONE => accum) (max_var downto 1) lits
   488 
   489 fun string_for_comp (a1, a2, cmp, xs) =
   490   string_for_sign_atom a1 ^ " " ^ string_for_comp_op cmp ^
   491   subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_sign_atom a2
   492 
   493 fun print_problem lits comps sexps =
   494   print_g ("*** Problem:\n" ^ cat_lines (map string_for_literal lits @
   495                                          map string_for_comp comps @
   496                                          map string_for_sign_expr sexps))
   497 
   498 fun print_solution lits =
   499   let val (pos, neg) = List.partition (curry (op =) Plus o snd) lits in
   500     print_g ("*** Solution:\n" ^
   501              "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
   502              "-: " ^ commas (map (string_for_var o fst) neg))
   503   end
   504 
   505 fun solve max_var (lits, comps, sexps) =
   506     let
   507       fun do_assigns assigns =
   508         SOME (literals_from_assignments max_var assigns lits
   509               |> tap print_solution)
   510       val _ = print_problem lits comps sexps
   511       val prop = PropLogic.all (map prop_for_literal lits @
   512                                 map prop_for_comp comps @
   513                                 map prop_for_sign_expr sexps)
   514       val default_val = bool_from_sign Minus
   515     in
   516       if PropLogic.eval (K default_val) prop then
   517         do_assigns (K (SOME default_val))
   518       else
   519         let
   520           (* use the first ML solver (to avoid startup overhead) *)
   521           val solvers = !SatSolver.solvers
   522                         |> filter (member (op =) ["dptsat", "dpll"] o fst)
   523         in
   524           case snd (hd solvers) prop of
   525             SatSolver.SATISFIABLE assigns => do_assigns assigns
   526           | _ => NONE
   527         end
   528     end
   529 
   530 type mtype_schema = mtyp * constraint_set
   531 type mtype_context =
   532   {bound_Ts: typ list,
   533    bound_Ms: mtyp list,
   534    frees: (styp * mtyp) list,
   535    consts: (styp * mtyp) list}
   536 
   537 type accumulator = mtype_context * constraint_set
   538 
   539 val initial_gamma = {bound_Ts = [], bound_Ms = [], frees = [], consts = []}
   540 
   541 fun push_bound T M {bound_Ts, bound_Ms, frees, consts} =
   542   {bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms, frees = frees,
   543    consts = consts}
   544 fun pop_bound {bound_Ts, bound_Ms, frees, consts} =
   545   {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms, frees = frees,
   546    consts = consts}
   547   handle List.Empty => initial_gamma (* FIXME: needed? *)
   548 
   549 fun consider_term (mdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
   550                                           def_table, ...},
   551                              alpha_T, max_fresh, ...}) =
   552   let
   553     val mtype_for = fresh_mtype_for_type mdata false
   554     fun plus_set_mtype_for_dom M =
   555       MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
   556     fun do_all T (gamma, cset) =
   557       let
   558         val abs_M = mtype_for (domain_type (domain_type T))
   559         val body_M = mtype_for (body_type T)
   560       in
   561         (MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M),
   562          (gamma, cset |> add_mtype_is_complete abs_M))
   563       end
   564     fun do_equals T (gamma, cset) =
   565       let val M = mtype_for (domain_type T) in
   566         (MFun (M, S Minus, MFun (M, V (Unsynchronized.inc max_fresh),
   567                                  mtype_for (nth_range_type 2 T))),
   568          (gamma, cset |> add_mtype_is_concrete M))
   569       end
   570     fun do_robust_set_operation T (gamma, cset) =
   571       let
   572         val set_T = domain_type T
   573         val M1 = mtype_for set_T
   574         val M2 = mtype_for set_T
   575         val M3 = mtype_for set_T
   576       in
   577         (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
   578          (gamma, cset |> add_is_sub_mtype M1 M3 |> add_is_sub_mtype M2 M3))
   579       end
   580     fun do_fragile_set_operation T (gamma, cset) =
   581       let
   582         val set_T = domain_type T
   583         val set_M = mtype_for set_T
   584         fun custom_mtype_for (T as Type (@{type_name fun}, [T1, T2])) =
   585             if T = set_T then set_M
   586             else MFun (custom_mtype_for T1, S Minus, custom_mtype_for T2)
   587           | custom_mtype_for T = mtype_for T
   588       in
   589         (custom_mtype_for T, (gamma, cset |> add_mtype_is_concrete set_M))
   590       end
   591     fun do_pair_constr T accum =
   592       case mtype_for (nth_range_type 2 T) of
   593         M as MPair (a_M, b_M) =>
   594         (MFun (a_M, S Minus, MFun (b_M, S Minus, M)), accum)
   595       | M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M], [])
   596     fun do_nth_pair_sel n T =
   597       case mtype_for (domain_type T) of
   598         M as MPair (a_M, b_M) =>
   599         pair (MFun (M, S Minus, if n = 0 then a_M else b_M))
   600       | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
   601     fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
   602       let
   603         val abs_M = mtype_for abs_T
   604         val (bound_m, accum) =
   605           accum |>> push_bound abs_T abs_M |> do_term bound_t
   606         val expected_bound_M = plus_set_mtype_for_dom abs_M
   607         val (body_m, accum) =
   608           accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
   609                 |> do_term body_t ||> apfst pop_bound
   610         val bound_M = mtype_of_mterm bound_m
   611         val (M1, a, M2) = dest_MFun bound_M
   612       in
   613         (MApp (MRaw (t0, MFun (bound_M, S Minus, bool_M)),
   614                MAbs (abs_s, abs_T, M1, a,
   615                      MApp (MApp (MRaw (connective_t,
   616                                        mtype_for (fastype_of connective_t)),
   617                                  MApp (bound_m, MRaw (Bound 0, M1))),
   618                            body_m))), accum)
   619       end
   620     and do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts},
   621                              cset)) =
   622         (case t of
   623            Const (x as (s, T)) =>
   624            (case AList.lookup (op =) consts x of
   625               SOME M => (M, accum)
   626             | NONE =>
   627               if not (could_exist_alpha_subtype alpha_T T) then
   628                 (mtype_for T, accum)
   629               else case s of
   630                 @{const_name all} => do_all T accum
   631               | @{const_name "=="} => do_equals T accum
   632               | @{const_name All} => do_all T accum
   633               | @{const_name Ex} =>
   634                 let val set_T = domain_type T in
   635                   do_term (Abs (Name.uu, set_T,
   636                                 @{const Not} $ (HOLogic.mk_eq
   637                                     (Abs (Name.uu, domain_type set_T,
   638                                           @{const False}),
   639                                      Bound 0)))) accum
   640                   |>> mtype_of_mterm
   641                 end
   642               | @{const_name "op ="} => do_equals T accum
   643               | @{const_name The} => (print_g "*** The"; raise UNSOLVABLE ())
   644               | @{const_name Eps} => (print_g "*** Eps"; raise UNSOLVABLE ())
   645               | @{const_name If} =>
   646                 do_robust_set_operation (range_type T) accum
   647                 |>> curry3 MFun bool_M (S Minus)
   648               | @{const_name Pair} => do_pair_constr T accum
   649               | @{const_name fst} => do_nth_pair_sel 0 T accum
   650               | @{const_name snd} => do_nth_pair_sel 1 T accum 
   651               | @{const_name Id} =>
   652                 (MFun (mtype_for (domain_type T), S Minus, bool_M), accum)
   653               | @{const_name insert} =>
   654                 let
   655                   val set_T = domain_type (range_type T)
   656                   val M1 = mtype_for (domain_type set_T)
   657                   val M1' = plus_set_mtype_for_dom M1
   658                   val M2 = mtype_for set_T
   659                   val M3 = mtype_for set_T
   660                 in
   661                   (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
   662                    (gamma, cset |> add_mtype_is_concrete M1
   663                                 |> add_is_sub_mtype M1' M3
   664                                 |> add_is_sub_mtype M2 M3))
   665                 end
   666               | @{const_name converse} =>
   667                 let
   668                   val x = Unsynchronized.inc max_fresh
   669                   fun mtype_for_set T =
   670                     MFun (mtype_for (domain_type T), V x, bool_M)
   671                   val ab_set_M = domain_type T |> mtype_for_set
   672                   val ba_set_M = range_type T |> mtype_for_set
   673                 in (MFun (ab_set_M, S Minus, ba_set_M), accum) end
   674               | @{const_name trancl} => do_fragile_set_operation T accum
   675               | @{const_name rel_comp} =>
   676                 let
   677                   val x = Unsynchronized.inc max_fresh
   678                   fun mtype_for_set T =
   679                     MFun (mtype_for (domain_type T), V x, bool_M)
   680                   val bc_set_M = domain_type T |> mtype_for_set
   681                   val ab_set_M = domain_type (range_type T) |> mtype_for_set
   682                   val ac_set_M = nth_range_type 2 T |> mtype_for_set
   683                 in
   684                   (MFun (bc_set_M, S Minus, MFun (ab_set_M, S Minus, ac_set_M)),
   685                    accum)
   686                 end
   687               | @{const_name image} =>
   688                 let
   689                   val a_M = mtype_for (domain_type (domain_type T))
   690                   val b_M = mtype_for (range_type (domain_type T))
   691                 in
   692                   (MFun (MFun (a_M, S Minus, b_M), S Minus,
   693                          MFun (plus_set_mtype_for_dom a_M, S Minus,
   694                                plus_set_mtype_for_dom b_M)), accum)
   695                 end
   696               | @{const_name finite} =>
   697                 let val M1 = mtype_for (domain_type (domain_type T)) in
   698                   (MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum)
   699                 end
   700               | @{const_name Sigma} =>
   701                 let
   702                   val x = Unsynchronized.inc max_fresh
   703                   fun mtype_for_set T =
   704                     MFun (mtype_for (domain_type T), V x, bool_M)
   705                   val a_set_T = domain_type T
   706                   val a_M = mtype_for (domain_type a_set_T)
   707                   val b_set_M = mtype_for_set (range_type (domain_type
   708                                                                (range_type T)))
   709                   val a_set_M = mtype_for_set a_set_T
   710                   val a_to_b_set_M = MFun (a_M, S Minus, b_set_M)
   711                   val ab_set_M = mtype_for_set (nth_range_type 2 T)
   712                 in
   713                   (MFun (a_set_M, S Minus,
   714                          MFun (a_to_b_set_M, S Minus, ab_set_M)), accum)
   715                 end
   716               | _ =>
   717                 if s = @{const_name safe_The} orelse
   718                    s = @{const_name safe_Eps} then
   719                   let
   720                     val a_set_M = mtype_for (domain_type T)
   721                     val a_M = dest_MFun a_set_M |> #1
   722                   in (MFun (a_set_M, S Minus, a_M), accum) end
   723                 else if s = @{const_name minus_class.minus} andalso
   724                         is_set_type (domain_type T) then
   725                   let
   726                     val set_T = domain_type T
   727                     val left_set_M = mtype_for set_T
   728                     val right_set_M = mtype_for set_T
   729                   in
   730                     (MFun (left_set_M, S Minus,
   731                            MFun (right_set_M, S Minus, left_set_M)),
   732                      (gamma, cset |> add_mtype_is_concrete right_set_M
   733                                   |> add_is_sub_mtype right_set_M left_set_M))
   734                   end
   735                 else if s = @{const_name ord_class.less_eq} andalso
   736                         is_set_type (domain_type T) then
   737                   do_fragile_set_operation T accum
   738                 else if (s = @{const_name semilattice_inf_class.inf} orelse
   739                          s = @{const_name semilattice_sup_class.sup}) andalso
   740                         is_set_type (domain_type T) then
   741                   do_robust_set_operation T accum
   742                 else if is_sel s then
   743                   (mtype_for_sel mdata x, accum)
   744                 else if is_constr thy stds x then
   745                   (mtype_for_constr mdata x, accum)
   746                 else if is_built_in_const thy stds fast_descrs x then
   747                   (fresh_mtype_for_type mdata true T, accum)
   748                 else
   749                   let val M = mtype_for T in
   750                     (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
   751                           frees = frees, consts = (x, M) :: consts}, cset))
   752                   end) |>> curry MRaw t
   753          | Free (x as (_, T)) =>
   754            (case AList.lookup (op =) frees x of
   755               SOME M => (M, accum)
   756             | NONE =>
   757               let val M = mtype_for T in
   758                 (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
   759                       frees = (x, M) :: frees, consts = consts}, cset))
   760               end) |>> curry MRaw t
   761          | Var _ => (print_g "*** Var"; raise UNSOLVABLE ())
   762          | Bound j => (MRaw (t, nth bound_Ms j), accum)
   763          | Abs (s, T, t') =>
   764            (case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of
   765               SOME t' =>
   766               let
   767                 val M = mtype_for T
   768                 val a = V (Unsynchronized.inc max_fresh)
   769                 val (m', accum) = do_term t' (accum |>> push_bound T M)
   770               in (MAbs (s, T, M, a, m'), accum |>> pop_bound) end
   771             | NONE =>
   772               ((case t' of
   773                   t1' $ Bound 0 =>
   774                   if not (loose_bvar1 (t1', 0)) then
   775                     do_term (incr_boundvars ~1 t1') accum
   776                   else
   777                     raise SAME ()
   778                 | _ => raise SAME ())
   779                handle SAME () =>
   780                       let
   781                         val M = mtype_for T
   782                         val (m', accum) = do_term t' (accum |>> push_bound T M)
   783                       in
   784                         (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound)
   785                       end))
   786          | (t0 as Const (@{const_name All}, _))
   787            $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) =>
   788            do_bounded_quantifier t0 s' T' t10 t11 t12 accum
   789          | (t0 as Const (@{const_name Ex}, _))
   790            $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) =>
   791            do_bounded_quantifier t0 s' T' t10 t11 t12 accum
   792          | Const (@{const_name Let}, _) $ t1 $ t2 =>
   793            do_term (betapply (t2, t1)) accum
   794          | t1 $ t2 =>
   795            let
   796              val (m1, accum) = do_term t1 accum
   797              val (m2, accum) = do_term t2 accum
   798            in
   799              let
   800                val T11 = domain_type (fastype_of1 (bound_Ts, t1))
   801                val T2 = fastype_of1 (bound_Ts, t2)
   802                val M11 = mtype_of_mterm m1 |> dest_MFun |> #1
   803                val M2 = mtype_of_mterm m2
   804              in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
   805            end)
   806         |> tap (fn (m, _) => print_g ("  \<Gamma> \<turnstile> " ^
   807                                       string_for_mterm ctxt m))
   808   in do_term end
   809 
   810 fun force_minus_funs 0 _ = I
   811   | force_minus_funs n (M as MFun (M1, _, M2)) =
   812     add_mtypes_equal M (MFun (M1, S Minus, M2))
   813     #> force_minus_funs (n - 1) M2
   814   | force_minus_funs _ M =
   815     raise MTYPE ("Nitpick_Mono.force_minus_funs", [M], [])
   816 fun consider_general_equals mdata def (x as (_, T)) t1 t2 accum =
   817   let
   818     val (m1, accum) = consider_term mdata t1 accum
   819     val (m2, accum) = consider_term mdata t2 accum
   820     val M1 = mtype_of_mterm m1
   821     val M2 = mtype_of_mterm m2
   822     val accum = accum ||> add_mtypes_equal M1 M2
   823     val body_M = fresh_mtype_for_type mdata false (nth_range_type 2 T)
   824     val m = MApp (MApp (MRaw (Const x,
   825                 MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2)
   826   in
   827     (m, if def then
   828           let val (head_m, arg_ms) = strip_mcomb m1 in
   829             accum ||> force_minus_funs (length arg_ms) (mtype_of_mterm head_m)
   830           end
   831         else
   832           accum)
   833   end
   834 
   835 fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) =
   836   let
   837     val mtype_for = fresh_mtype_for_type mdata false
   838     val do_term = consider_term mdata
   839     fun do_formula sn t accum =
   840         let
   841           fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
   842             let
   843               val abs_M = mtype_for abs_T
   844               val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
   845               val (body_m, accum) =
   846                 accum ||> side_cond ? add_mtype_is_complete abs_M
   847                       |>> push_bound abs_T abs_M |> do_formula sn body_t
   848               val body_M = mtype_of_mterm body_m
   849             in
   850               (MApp (MRaw (Const quant_x,
   851                            MFun (MFun (abs_M, S Minus, body_M), S Minus,
   852                                  body_M)),
   853                      MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
   854                accum |>> pop_bound)
   855             end
   856           fun do_equals x t1 t2 =
   857             case sn of
   858               Plus => do_term t accum
   859             | Minus => consider_general_equals mdata false x t1 t2 accum
   860         in
   861           case t of
   862             Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
   863             do_quantifier x s1 T1 t1
   864           | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
   865           | @{const Trueprop} $ t1 =>
   866             let val (m1, accum) = do_formula sn t1 accum in
   867               (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
   868                      m1), accum)
   869             end
   870           | @{const Not} $ t1 =>
   871             let val (m1, accum) = do_formula (negate sn) t1 accum in
   872               (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
   873                accum)
   874             end
   875           | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
   876             do_quantifier x s1 T1 t1
   877           | Const (x0 as (s0 as @{const_name Ex}, T0))
   878             $ (t1 as Abs (s1, T1, t1')) =>
   879             (case sn of
   880                Plus => do_quantifier x0 s1 T1 t1'
   881              | Minus =>
   882                (* FIXME: Move elsewhere *)
   883                do_term (@{const Not}
   884                         $ (HOLogic.eq_const (domain_type T0) $ t1
   885                            $ Abs (Name.uu, T1, @{const False}))) accum)
   886           | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
   887             do_equals x t1 t2
   888           | (t0 as Const (s0, _)) $ t1 $ t2 =>
   889             if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
   890                s0 = @{const_name "op |"} orelse s0 = @{const_name "op -->"} then
   891               let
   892                 val impl = (s0 = @{const_name "==>"} orelse
   893                            s0 = @{const_name "op -->"})
   894                 val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
   895                 val (m2, accum) = do_formula sn t2 accum
   896               in
   897                 (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
   898                  accum)
   899               end 
   900             else
   901               do_term t accum
   902           | _ => do_term t accum
   903         end
   904         |> tap (fn (m, _) =>
   905                    print_g ("\<Gamma> \<turnstile> " ^
   906                             string_for_mterm ctxt m ^ " : o\<^sup>" ^
   907                             string_for_sign sn))
   908   in do_formula end
   909 
   910 (* The harmless axiom optimization below is somewhat too aggressive in the face
   911    of (rather peculiar) user-defined axioms. *)
   912 val harmless_consts =
   913   [@{const_name ord_class.less}, @{const_name ord_class.less_eq}]
   914 val bounteous_consts = [@{const_name bisim}]
   915 
   916 fun is_harmless_axiom ({no_harmless = true, ...} : mdata) _ = false
   917   | is_harmless_axiom {hol_ctxt = {thy, stds, fast_descrs, ...}, ...} t =
   918     Term.add_consts t []
   919     |> filter_out (is_built_in_const thy stds fast_descrs)
   920     |> (forall (member (op =) harmless_consts o original_name o fst) orf
   921         exists (member (op =) bounteous_consts o fst))
   922 
   923 fun consider_nondefinitional_axiom mdata t =
   924   if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M))
   925   else consider_general_formula mdata Plus t
   926 
   927 fun consider_definitional_axiom (mdata as {hol_ctxt = {thy, ...}, ...}) t =
   928   if not (is_constr_pattern_formula thy t) then
   929     consider_nondefinitional_axiom mdata t
   930   else if is_harmless_axiom mdata t then
   931     pair (MRaw (t, dummy_M))
   932   else
   933     let
   934       val mtype_for = fresh_mtype_for_type mdata false
   935       val do_term = consider_term mdata
   936       fun do_all quant_t abs_s abs_T body_t accum =
   937         let
   938           val abs_M = mtype_for abs_T
   939           val (body_m, accum) =
   940             accum |>> push_bound abs_T abs_M |> do_formula body_t
   941           val body_M = mtype_of_mterm body_m
   942         in
   943           (MApp (MRaw (quant_t,
   944                        MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M)),
   945                  MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
   946            accum |>> pop_bound)
   947         end
   948       and do_conjunction t0 t1 t2 accum =
   949         let
   950           val (m1, accum) = do_formula t1 accum
   951           val (m2, accum) = do_formula t2 accum
   952         in
   953           (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
   954         end
   955       and do_implies t0 t1 t2 accum =
   956         let
   957           val (m1, accum) = do_term t1 accum
   958           val (m2, accum) = do_formula t2 accum
   959         in
   960           (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
   961         end
   962       and do_formula t accum =
   963           case t of
   964             (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
   965             do_all t0 s1 T1 t1 accum
   966           | @{const Trueprop} $ t1 =>
   967             let val (m1, accum) = do_formula t1 accum in
   968               (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
   969                      m1), accum)
   970             end
   971           | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
   972             consider_general_equals mdata true x t1 t2 accum
   973           | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
   974           | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
   975             do_conjunction t0 t1 t2 accum
   976           | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
   977             do_all t0 s0 T1 t1 accum
   978           | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
   979             consider_general_equals mdata true x t1 t2 accum
   980           | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
   981           | (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
   982           | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
   983                              \do_formula", [t])
   984     in do_formula t end
   985 
   986 fun string_for_mtype_of_term ctxt lits t M =
   987   Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype lits M)
   988 
   989 fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) =
   990   map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @
   991   map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
   992   |> cat_lines |> print_g
   993 
   994 fun amass f t (ms, accum) =
   995   let val (m, accum) = f t accum in (m :: ms, accum) end
   996 
   997 fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
   998           (nondef_ts, def_ts) =
   999   let
  1000     val _ = print_g ("****** " ^ which ^ " analysis: " ^
  1001                      string_for_mtype MAlpha ^ " is " ^
  1002                      Syntax.string_of_typ ctxt alpha_T)
  1003     val mdata as {max_fresh, constr_mcache, ...} =
  1004       initial_mdata hol_ctxt binarize no_harmless alpha_T
  1005     val accum = (initial_gamma, ([], [], []))
  1006     val (nondef_ms, accum) =
  1007       ([], accum) |> amass (consider_general_formula mdata Plus) (hd nondef_ts)
  1008                   |> fold (amass (consider_nondefinitional_axiom mdata))
  1009                           (tl nondef_ts)
  1010     val (def_ms, (gamma, cset)) =
  1011       ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
  1012   in
  1013     case solve (!max_fresh) cset of
  1014       SOME lits => (print_mtype_context ctxt lits gamma;
  1015                     SOME (lits, (nondef_ms, def_ms), !constr_mcache))
  1016     | _ => NONE
  1017   end
  1018   handle UNSOLVABLE () => NONE
  1019        | MTYPE (loc, Ms, Ts) =>
  1020          raise BAD (loc, commas (map string_for_mtype Ms @
  1021                                  map (Syntax.string_of_typ ctxt) Ts))
  1022        | MTERM (loc, ms) =>
  1023          raise BAD (loc, commas (map (string_for_mterm ctxt) ms))
  1024 
  1025 val formulas_monotonic = is_some oooo infer "Monotonicity" false
  1026 
  1027 fun fin_fun_constr T1 T2 =
  1028   (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
  1029 
  1030 fun finitize_funs (hol_ctxt as {thy, stds, fast_descrs, constr_cache, ...})
  1031                   binarize finitizes alpha_T tsp =
  1032   case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
  1033     SOME (lits, msp, constr_mtypes) =>
  1034     if forall (curry (op =) Minus o snd) lits then
  1035       tsp
  1036     else
  1037       let
  1038         fun should_finitize T a =
  1039           case triple_lookup (type_match thy) finitizes T of
  1040             SOME (SOME false) => false
  1041           | _ => resolve_sign_atom lits a = S Plus
  1042         fun type_from_mtype T M =
  1043           case (M, T) of
  1044             (MAlpha, _) => T
  1045           | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) =>
  1046             Type (if should_finitize T a then @{type_name fin_fun}
  1047                   else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
  1048           | (MPair (M1, M2), Type (@{type_name "*"}, Ts)) =>
  1049             Type (@{type_name "*"}, map2 type_from_mtype Ts [M1, M2])
  1050           | (MType _, _) => T
  1051           | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
  1052                               [M], [T])
  1053         fun finitize_constr (x as (s, T)) =
  1054           (s, case AList.lookup (op =) constr_mtypes x of
  1055                 SOME M => type_from_mtype T M
  1056               | NONE => T)
  1057         fun term_from_mterm Ts m =
  1058           case m of
  1059             MRaw (t, M) =>
  1060             let
  1061               val T = fastype_of1 (Ts, t)
  1062               val T' = type_from_mtype T M
  1063             in
  1064               case t of
  1065                 Const (x as (s, _)) =>
  1066                 if s = @{const_name insert} then
  1067                   case nth_range_type 2 T' of
  1068                     set_T' as Type (@{type_name fin_fun}, [elem_T', _]) =>
  1069                       Abs (Name.uu, elem_T', Abs (Name.uu, set_T',
  1070                           Const (@{const_name If},
  1071                                  bool_T --> set_T' --> set_T' --> set_T')
  1072                           $ (Const (@{const_name is_unknown},
  1073                                     elem_T' --> bool_T) $ Bound 1)
  1074                           $ (Const (@{const_name unknown}, set_T'))
  1075                           $ (coerce_term hol_ctxt Ts T' T (Const x)
  1076                              $ Bound 1 $ Bound 0)))
  1077                   | _ => Const (s, T')
  1078                 else if s = @{const_name finite} then
  1079                   case domain_type T' of
  1080                     set_T' as Type (@{type_name fin_fun}, _) =>
  1081                     Abs (Name.uu, set_T', @{const True})
  1082                   | _ => Const (s, T')
  1083                 else if s = @{const_name "=="} orelse
  1084                         s = @{const_name "op ="} then
  1085                   Const (s, T')
  1086                 else if is_built_in_const thy stds fast_descrs x then
  1087                   coerce_term hol_ctxt Ts T' T t
  1088                 else if is_constr thy stds x then
  1089                   Const (finitize_constr x)
  1090                 else if is_sel s then
  1091                   let
  1092                     val n = sel_no_from_name s
  1093                     val x' =
  1094                       x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
  1095                         |> finitize_constr
  1096                     val x'' =
  1097                       binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize
  1098                                                              x' n
  1099                   in Const x'' end
  1100                 else
  1101                   Const (s, T')
  1102               | Free (s, T) => Free (s, type_from_mtype T M)
  1103               | Bound _ => t
  1104               | _ => raise MTERM ("Nitpick_Mono.finitize_funs.term_from_mterm",
  1105                                   [m])
  1106             end
  1107           | MApp (m1, m2) =>
  1108             let
  1109               val (t1, t2) = pairself (term_from_mterm Ts) (m1, m2)
  1110               val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2)
  1111               val (t1', T2') =
  1112                 case T1 of
  1113                   Type (s, [T11, T12]) => 
  1114                   (if s = @{type_name fin_fun} then
  1115                      select_nth_constr_arg thy stds (fin_fun_constr T11 T12) t1
  1116                                            0 (T11 --> T12)
  1117                    else
  1118                      t1, T11)
  1119                 | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm",
  1120                                    [T1], [])
  1121             in betapply (t1', coerce_term hol_ctxt Ts T2' T2 t2) end
  1122           | MAbs (s, T, M, a, m') =>
  1123             let
  1124               val T = type_from_mtype T M
  1125               val t' = term_from_mterm (T :: Ts) m'
  1126               val T' = fastype_of1 (T :: Ts, t')
  1127             in
  1128               Abs (s, T, t')
  1129               |> should_finitize (T --> T') a
  1130                  ? construct_value thy stds (fin_fun_constr T T') o single
  1131             end
  1132       in
  1133         Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
  1134         pairself (map (term_from_mterm [])) msp
  1135       end
  1136   | NONE => tsp
  1137 
  1138 end;