author blanchet Tue, 07 Dec 2010 11:56:56 +0100 changeset 41054 e58d1cdda832 parent 41053 8e2f2398aae7 child 41055 d6f45159ae84
simplify monotonicity code after killing "fin_fun" optimization
```--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Dec 07 11:56:56 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Dec 07 11:56:56 2010 +0100
@@ -67,7 +67,6 @@
ML {* Nitpick_Mono.trace := false *}

ML {* const @{term "A\<Colon>('a\<Rightarrow>'b)"} *}
-(*
ML {* const @{term "(A\<Colon>'a set) = A"} *}
ML {* const @{term "(A\<Colon>'a set set) = A"} *}
ML {* const @{term "(\<lambda>x\<Colon>'a set. x a)"} *}
@@ -138,7 +137,6 @@

ML {* nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"} *}
ML {* nonmono @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h"} *}
-*)

ML {*
val preproc_timeout = SOME (seconds 5.0)
@@ -184,8 +182,6 @@

fun check_theory thy =
let
-    val finitizes = [(NONE, SOME false)]
-    val monos = [(NONE, SOME false)]
val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode)
val _ = File.write path ""
fun check_theorem (name, th) =
@@ -193,8 +189,7 @@
val t = th |> prop_of |> Type.legacy_freeze |> close_form
val neg_t = Logic.mk_implies (t, @{prop False})
val (nondef_ts, def_ts, _, _, _) =
-          time_limit preproc_timeout
-              (preprocess_formulas hol_ctxt finitizes monos []) neg_t
+          time_limit preproc_timeout (preprocess_formulas hol_ctxt []) neg_t
val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
in File.append path (res ^ "\n"); writeln res end
handle TimeLimit.TimeOut => ()```
```--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 11:56:56 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 11:56:56 2010 +0100
@@ -38,23 +38,16 @@
MType of string * mtyp list |
MRec of string * typ list

-datatype mterm =
-  MRaw of term * mtyp |
-  MAbs of string * typ * mtyp * annotation_atom * mterm |
-  MApp of mterm * mterm
-
type mdata =
{hol_ctxt: hol_context,
binarize: bool,
alpha_T: typ,
-   no_harmless: bool,
max_fresh: int Unsynchronized.ref,
datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
constr_mcache: (styp * mtyp) list Unsynchronized.ref}

exception UNSOLVABLE of unit
exception MTYPE of string * mtyp list * typ list
-exception MTERM of string * mterm list

val trace = Unsynchronized.ref false
fun trace_msg msg = if !trace then tracing (msg ()) else ()
@@ -126,43 +119,9 @@
| flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms
| flatten_mtype M = [M]

-fun precedence_of_mterm (MRaw _) = no_prec
-  | precedence_of_mterm (MAbs _) = 1
-  | precedence_of_mterm (MApp _) = 2
-
-fun string_for_mterm ctxt =
-  let
-    fun mtype_annotation M = "\<^bsup>" ^ string_for_mtype M ^ "\<^esup>"
-    fun aux outer_prec m =
-      let
-        val prec = precedence_of_mterm m
-        val need_parens = (prec < outer_prec)
-      in
-        (if need_parens then "(" else "") ^
-        (case m of
-           MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
-         | MAbs (s, _, M, aa, m) =>
-           "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
-           string_for_annotation_atom aa ^ "\<^esup> " ^ aux prec m
-         | MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^
-        (if need_parens then ")" else "")
-      end
-  in aux 0 end
-
-fun mtype_of_mterm (MRaw (_, M)) = M
-  | mtype_of_mterm (MAbs (_, _, M, aa, m)) = MFun (M, aa, mtype_of_mterm m)
-  | mtype_of_mterm (MApp (m1, _)) =
-    case mtype_of_mterm m1 of
-      MFun (_, _, M12) => M12
-    | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1], [])
-
-fun strip_mcomb (MApp (m1, m2)) = strip_mcomb m1 ||> (fn ms => append ms [m2])
-  | strip_mcomb m = (m, [])
-
-fun initial_mdata hol_ctxt binarize no_harmless alpha_T =
+fun initial_mdata hol_ctxt binarize alpha_T =
({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
-    no_harmless = no_harmless, max_fresh = Unsynchronized.ref 0,
-    datatype_mcache = Unsynchronized.ref [],
+    max_fresh = Unsynchronized.ref 0, datatype_mcache = Unsynchronized.ref [],
constr_mcache = Unsynchronized.ref []} : mdata)

fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
@@ -243,7 +202,7 @@
\$ (Const (@{const_name unknown}, ran_T)) \$ (t0 \$ t1 \$ t2 \$ t3)))
| fin_fun_body _ _ _ = NONE

-(* ### FIXME: make sure well-annotated! *)
+(* FIXME: make sure well-annotated *)

fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) all_minus
T1 T2 =
@@ -306,7 +265,8 @@
| _ => MType (simple_string_of_typ T, [])
in do_type end

-val ground_and_sole_base_constrs = [] (* FIXME: [@{const_name Nil}, @{const_name None}], cf. lists_empty *)
+val ground_and_sole_base_constrs = []
+(* FIXME: [@{const_name Nil}, @{const_name None}], cf. lists_empty *)

fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
| prodM_factors M = [M]
@@ -644,8 +604,6 @@
{bound_Ts = bound_Ts, bound_Ms = bound_Ms, frame = frame, frees = frees,
consts = consts}

-(* FIXME: make sure tracing messages are complete *)
-
fun add_comp_frame aa cmp = fold (add_annotation_atom_comp cmp [] aa o snd)

@@ -691,11 +649,11 @@
[(aa1, (Eq, Fls)), (aa2, (Neq, Gen)), (res_aa, (Eq, Gen))],
[(aa1, (Eq, Fls)), (aa2, (Neq, New)), (res_aa, (Eq, Gen))]]

-val meta_conj_triple = ("\<and>", conj_clauses, @{const Pure.conjunction})
-val meta_imp_triple = ("\<implies>", imp_clauses, @{const "==>"})
-val conj_triple = ("\<and>", conj_clauses, @{const conj})
-val disj_triple = ("\<or>", disj_clauses, @{const disj})
-val imp_triple = ("\<implies>", imp_clauses, @{const implies})
+val meta_conj_spec = ("\<and>", conj_clauses)
+val meta_imp_spec = ("\<implies>", imp_clauses)
+val conj_spec = ("\<and>", conj_clauses)
+val disj_spec = ("\<or>", disj_clauses)
+val imp_spec = ("\<implies>", imp_clauses)

fun add_annotation_clause_from_quasi_clause _ NONE = NONE
| add_annotation_clause_from_quasi_clause [] accum = accum
@@ -761,19 +719,17 @@
#> fold add_arg_order1 (tl arg_frame ~~ (fst (split_last arg_frame)))
#> fold (add_app1 fun_aa) (res_frame ~~ arg_frame)

-fun consider_connective mdata (conn, mk_quasi_clauses, t0) do_t1 do_t2
+fun consider_connective mdata (conn, mk_quasi_clauses) do_t1 do_t2
(accum as ({frame, ...}, _)) =
let
-    val mtype_for = fresh_mtype_for_type mdata false
val frame1 = fresh_frame mdata (SOME Tru) NONE frame
val frame2 = fresh_frame mdata (SOME Fls) NONE frame
-    val (m1, accum) = accum |>> set_frame frame1 |> do_t1
-    val (m2, accum) = accum |>> set_frame frame2 |> do_t2
in
-    (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
-     accum |>> set_frame frame
-           ||> apsnd (add_connective_frames conn mk_quasi_clauses frame frame1
-                                            frame2))
+    accum |>> set_frame frame1 |> do_t1
+          |>> set_frame frame2 |> do_t2
+          |>> set_frame frame
+          ||> apsnd (add_connective_frames conn mk_quasi_clauses frame frame1
+                                           frame2)
end

fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
@@ -834,8 +790,9 @@
M as MPair (a_M, b_M) =>
pair (MFun (M, A Gen, if n = 0 then a_M else b_M))
| M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
-    and do_connect triple t1 t2 =
-      consider_connective mdata triple (do_term t1) (do_term t2)
+    and do_connect spec t1 t2 accum =
+      (bool_M, consider_connective mdata spec (snd o do_term t1)
+                                   (snd o do_term t2) accum)
and do_term t
(accum as (gamma as {bound_Ts, bound_Ms, frame, frees, consts},
cset)) =
@@ -843,12 +800,10 @@
" \<turnstile> " ^ Syntax.string_of_term ctxt t ^
" : _?");
case t of
-         @{const False} =>
-         (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame)
+         @{const False} => (bool_M, accum ||> add_comp_frame (A Fls) Leq frame)
| Const (@{const_name None}, T) =>
-         (MRaw (t, mtype_for T), accum ||> add_comp_frame (A Fls) Leq frame)
-       | @{const True} =>
-         (MRaw (t, bool_M), accum ||> add_comp_frame (A Tru) Leq frame)
+         (mtype_for T, accum ||> add_comp_frame (A Fls) Leq frame)
+       | @{const True} => (bool_M, accum ||> add_comp_frame (A Tru) Leq frame)
| (t0 as Const (@{const_name HOL.eq}, _)) \$ Bound 0 \$ t2 =>
(* hack to exploit symmetry of equality when typing "insert" *)
(if t2 = Bound 0 then do_term @{term True}
@@ -870,7 +825,6 @@
(Abs (Name.uu, domain_type set_T,
@{const False}),
Bound 0)))) accum
-                |>> mtype_of_mterm
end
| @{const_name HOL.eq} => do_equals T accum
| @{const_name The} =>
@@ -947,7 +901,6 @@
(M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms, frame = frame,
frees = frees, consts = (x, M) :: consts}, cset))
end)
-           |>> curry MRaw t
||> apsnd (add_comp_frame (A Gen) Eq frame)
| Free (x as (_, T)) =>
(case AList.lookup (op =) frees x of
@@ -957,20 +910,20 @@
(M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms, frame = frame,
frees = (x, M) :: frees, consts = consts}, cset))
end)
-           |>> curry MRaw t ||> apsnd (add_comp_frame (A Gen) Eq frame)
+           ||> apsnd (add_comp_frame (A Gen) Eq frame)
| Var _ => (trace_msg (K "*** Var"); raise UNSOLVABLE ())
| Bound j =>
-           (MRaw (t, nth bound_Ms j),
+           (nth bound_Ms j,
accum ||> add_bound_frame (length bound_Ts - j - 1) frame)
-         | Abs (s, T, t') =>
+         | Abs (_, T, t') =>
(case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of
SOME t' =>
let
val M = mtype_for T
val x = Unsynchronized.inc max_fresh
-                val (m', accum) = do_term t' (accum |>> push_bound (V x) T M)
+                val (M', accum) = do_term t' (accum |>> push_bound (V x) T M)
in
-                (MAbs (s, T, M, V x, m'),
+                (MFun (M, V x, M'),
accum |>> pop_bound
||> add_annotation_atom_comp Leq [] (A Fls) (V x))
end
@@ -992,13 +945,13 @@
let
val M = mtype_for T
val x = Unsynchronized.inc max_fresh
-                        val (m', accum) =
+                        val (M', accum) =
do_term t' (accum |>> push_bound (V x) T M)
-                      in (MAbs (s, T, M, V x, m'), accum |>> pop_bound) end))
-         | @{const Not} \$ t1 => do_connect imp_triple t1 @{const False} accum
-         | @{const conj} \$ t1 \$ t2 => do_connect conj_triple t1 t2 accum
-         | @{const disj} \$ t1 \$ t2 => do_connect disj_triple t1 t2 accum
-         | @{const implies} \$ t1 \$ t2 => do_connect imp_triple t1 t2 accum
+                      in (MFun (M, V x, M'), accum |>> pop_bound) end))
+         | @{const Not} \$ t1 => do_connect imp_spec t1 @{const False} accum
+         | @{const conj} \$ t1 \$ t2 => do_connect conj_spec t1 t2 accum
+         | @{const disj} \$ t1 \$ t2 => do_connect disj_spec t1 t2 accum
+         | @{const implies} \$ t1 \$ t2 => do_connect imp_spec t1 t2 accum
| Const (@{const_name Let}, _) \$ t1 \$ t2 =>
do_term (betapply (t2, t1)) accum
| t1 \$ t2 =>
@@ -1011,121 +964,106 @@
val frame2b =
frame1b |> map (apsnd (fn _ => V (Unsynchronized.inc max_fresh)))
val frame2 = frame2a @ frame2b
-             val (m1, accum) = accum |>> set_frame frame1a |> do_term t1
-             val (m2, accum) = accum |>> set_frame frame2 |> do_term t2
+             val (M1, accum) = accum |>> set_frame frame1a |> do_term t1
+             val (M2, accum) = accum |>> set_frame frame2 |> do_term t2
in
let
-               val (M11, aa, _) = mtype_of_mterm m1 |> dest_MFun
-               val M2 = mtype_of_mterm m2
+               val (M11, aa, M12) = M1 |> dest_MFun
in
-               (MApp (m1, m2),
-                accum |>> set_frame frame
-                      ||> add_app aa frame1b frame2b)
+               (M12, accum |>> set_frame frame
+                           ||> add_app aa frame1b frame2b)
end
end)
-        |> tap (fn (m, (gamma, _)) =>
+        |> tap (fn (M, (gamma, _)) =>
trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
" \<turnstile> " ^
-                                       string_for_mterm ctxt m))
+                                       Syntax.string_of_term ctxt t ^ " : " ^
+                                       string_for_mtype M))
in do_term end

fun force_gen_funs 0 _ = I
| force_gen_funs n (M as MFun (M1, _, M2)) =
add_mtypes_equal M (MFun (M1, A Gen, M2)) #> force_gen_funs (n - 1) M2
| force_gen_funs _ M = raise MTYPE ("Nitpick_Mono.force_gen_funs", [M], [])
-fun consider_general_equals mdata def (x as (_, T)) t1 t2 accum =
+fun consider_general_equals mdata def t1 t2 accum =
let
-    val (m1, accum) = consider_term mdata t1 accum
-    val (m2, accum) = consider_term mdata t2 accum
-    val M1 = mtype_of_mterm m1
-    val M2 = mtype_of_mterm m2
+    val (M1, accum) = consider_term mdata t1 accum
+    val (M2, accum) = consider_term mdata t2 accum
val accum = accum ||> add_mtypes_equal M1 M2
-    val body_M = fresh_mtype_for_type mdata false (nth_range_type 2 T)
-    val m = MApp (MApp (MRaw (Const x,
-                           MFun (M1, A Gen, MFun (M2, A Gen, body_M))), m1), m2)
in
-    (m, (if def then
-           let val (head_m, arg_ms) = strip_mcomb m1 in
-             accum ||> force_gen_funs (length arg_ms) (mtype_of_mterm head_m)
-           end
-         else
-           accum))
+    if def then
+      let
+        val (head1, args1) = strip_comb t1
+      in accum ||> force_gen_funs (length args1) head_M1 end
+    else
+      accum
end

fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, max_fresh,
...}) =
let
val mtype_for = fresh_mtype_for_type mdata false
-    val do_term = consider_term mdata
+    val do_term = snd oo consider_term mdata
fun do_formula sn t (accum as (gamma, _)) =
let
-        fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
+        fun do_quantifier quant_s abs_T body_t =
let
val abs_M = mtype_for abs_T
val x = Unsynchronized.inc max_fresh
val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
fun ann () = if quant_s = @{const_name Ex} then Fls else Tru
-            val (body_m, accum) =
-              accum ||> side_cond
-                        ? add_mtype_is_complete [(x, (Plus, ann ()))] abs_M
-                    |>> push_bound (V x) abs_T abs_M |> do_formula sn body_t
-            val body_M = mtype_of_mterm body_m
in
-            (MApp (MRaw (Const quant_x,
-                         MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M)),
-                   MAbs (abs_s, abs_T, abs_M, A Gen, body_m)),
-             accum |>> pop_bound)
+            accum ||> side_cond
+                      ? add_mtype_is_complete [(x, (Plus, ann ()))] abs_M
+                  |>> push_bound (V x) abs_T abs_M
+                  |> do_formula sn body_t
+                  |>> pop_bound
end
-        fun do_connect triple neg1 t1 t2 =
-          consider_connective mdata triple
+        fun do_connect spec neg1 t1 t2 =
+          consider_connective mdata spec
(do_formula (sn |> neg1 ? negate_sign) t1) (do_formula sn t2)
-        fun do_equals x t1 t2 =
+        fun do_equals t1 t2 =
case sn of
Plus => do_term t accum
-          | Minus => consider_general_equals mdata false x t1 t2 accum
+          | Minus => consider_general_equals mdata false t1 t2 accum
in
trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
" \<turnstile> " ^ Syntax.string_of_term ctxt t ^
" : o\<^sup>" ^ string_for_sign sn ^ "?");
case t of
-          Const (x as (@{const_name all}, _)) \$ Abs (s1, T1, t1) =>
-          do_quantifier x s1 T1 t1
-        | Const (x as (@{const_name "=="}, _)) \$ t1 \$ t2 => do_equals x t1 t2
-        | @{const Trueprop} \$ t1 =>
-          let val (m1, accum) = do_formula sn t1 accum in
-            (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)), m1),
-             accum)
-          end
-        | Const (x as (@{const_name All}, _)) \$ Abs (s1, T1, t1) =>
-          do_quantifier x s1 T1 t1
-        | Const (x0 as (@{const_name Ex}, T0)) \$ (t1 as Abs (s1, T1, t1')) =>
+          Const (s as @{const_name all}, _) \$ Abs (_, T1, t1) =>
+          do_quantifier s T1 t1
+        | Const (@{const_name "=="}, _) \$ t1 \$ t2 => do_equals t1 t2
+        | @{const Trueprop} \$ t1 => do_formula sn t1 accum
+        | Const (s as @{const_name All}, _) \$ Abs (_, T1, t1) =>
+          do_quantifier s T1 t1
+        | Const (s as @{const_name Ex}, T0) \$ (t1 as Abs (_, T1, t1')) =>
(case sn of
-             Plus => do_quantifier x0 s1 T1 t1'
+             Plus => do_quantifier s T1 t1'
| Minus =>
-             (* FIXME: Move elsewhere *)
+             (* FIXME: Needed? *)
do_term (@{const Not}
\$ (HOLogic.eq_const (domain_type T0) \$ t1
\$ Abs (Name.uu, T1, @{const False}))) accum)
-        | Const (x as (@{const_name HOL.eq}, _)) \$ t1 \$ t2 => do_equals x t1 t2
+        | Const (@{const_name HOL.eq}, _) \$ t1 \$ t2 => do_equals t1 t2
| Const (@{const_name Let}, _) \$ t1 \$ t2 =>
do_formula sn (betapply (t2, t1)) accum
| @{const Pure.conjunction} \$ t1 \$ t2 =>
-          do_connect meta_conj_triple false t1 t2 accum
-        | @{const "==>"} \$ t1 \$ t2 =>
-          do_connect meta_imp_triple true t1 t2 accum
-        | @{const Not} \$ t1 =>
-          do_connect imp_triple true t1 @{const False} accum
-        | @{const conj} \$ t1 \$ t2 => do_connect conj_triple false t1 t2 accum
-        | @{const disj} \$ t1 \$ t2 => do_connect disj_triple false t1 t2 accum
-        | @{const implies} \$ t1 \$ t2 => do_connect imp_triple true t1 t2 accum
+          do_connect meta_conj_spec false t1 t2 accum
+        | @{const "==>"} \$ t1 \$ t2 => do_connect meta_imp_spec true t1 t2 accum
+        | @{const Not} \$ t1 => do_connect imp_spec true t1 @{const False} accum
+        | @{const conj} \$ t1 \$ t2 => do_connect conj_spec false t1 t2 accum
+        | @{const disj} \$ t1 \$ t2 => do_connect disj_spec false t1 t2 accum
+        | @{const implies} \$ t1 \$ t2 => do_connect imp_spec true t1 t2 accum
| _ => do_term t accum
end
-      |> tap (fn (m, (gamma, _)) =>
+      |> tap (fn (gamma, _) =>
trace_msg (fn () => string_for_mcontext ctxt t gamma ^
" \<turnstile> " ^
-                                     string_for_mterm ctxt m ^ " : o\<^sup>" ^
-                                     string_for_sign sn))
+                                     Syntax.string_of_term ctxt t ^
+                                     " : o\<^sup>" ^ string_for_sign sn))
in do_formula end

(* The harmless axiom optimization below is somewhat too aggressive in the face
@@ -1134,72 +1072,44 @@
[@{const_name ord_class.less}, @{const_name ord_class.less_eq}]
val bounteous_consts = [@{const_name bisim}]

-fun is_harmless_axiom ({no_harmless = true, ...} : mdata) _ = false
-  | is_harmless_axiom {hol_ctxt = {thy, stds, ...}, ...} t =
+fun is_harmless_axiom {hol_ctxt = {thy, stds, ...}, ...} t =
|> filter_out (is_built_in_const thy stds)
|> (forall (member (op =) harmless_consts o original_name o fst) orf
exists (member (op =) bounteous_consts o fst))

fun consider_nondefinitional_axiom mdata t =
-  if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M))
+  if is_harmless_axiom mdata t then I
else consider_general_formula mdata Plus t

fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...}) t =
if not (is_constr_pattern_formula ctxt t) then
consider_nondefinitional_axiom mdata t
else if is_harmless_axiom mdata t then
-    pair (MRaw (t, dummy_M))
+    I
else
let
val mtype_for = fresh_mtype_for_type mdata false
-      val do_term = consider_term mdata
-      fun do_all quant_t abs_s abs_T body_t accum =
-        let
-          val abs_M = mtype_for abs_T
-          val (body_m, accum) =
-            accum |>> push_bound (A Gen) abs_T abs_M |> do_formula body_t
-          val body_M = mtype_of_mterm body_m
-        in
-          (MApp (MRaw (quant_t, MFun (MFun (abs_M, A Gen, body_M), A Gen,
-                       body_M)),
-                 MAbs (abs_s, abs_T, abs_M, A Gen, body_m)),
-           accum |>> pop_bound)
-        end
-      and do_conjunction t0 t1 t2 accum =
-        let
-          val (m1, accum) = do_formula t1 accum
-          val (m2, accum) = do_formula t2 accum
-        in
-          (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
-        end
-      and do_implies t0 t1 t2 accum =
-        let
-          val (m1, accum) = do_term t1 accum
-          val (m2, accum) = do_formula t2 accum
-        in
-          (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
-        end
+      val do_term = snd oo consider_term mdata
+      fun do_all abs_T body_t accum =
+        accum |>> push_bound (A Gen) abs_T (mtype_for abs_T)
+              |> do_formula body_t
+              |>> pop_bound
+      and do_implies t1 t2 = do_term t1 #> do_formula t2
and do_formula t accum =
case t of
-          (t0 as Const (@{const_name all}, _)) \$ Abs (s1, T1, t1) =>
-          do_all t0 s1 T1 t1 accum
-        | @{const Trueprop} \$ t1 =>
-          let val (m1, accum) = do_formula t1 accum in
-            (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)), m1),
-             accum)
-          end
-        | Const (x as (@{const_name "=="}, _)) \$ t1 \$ t2 =>
-          consider_general_equals mdata true x t1 t2 accum
-        | (t0 as @{const "==>"}) \$ t1 \$ t2 => do_implies t0 t1 t2 accum
-        | (t0 as @{const Pure.conjunction}) \$ t1 \$ t2 =>
-          do_conjunction t0 t1 t2 accum
-        | (t0 as Const (@{const_name All}, _)) \$ Abs (s0, T1, t1) =>
-          do_all t0 s0 T1 t1 accum
-        | Const (x as (@{const_name HOL.eq}, _)) \$ t1 \$ t2 =>
-          consider_general_equals mdata true x t1 t2 accum
-        | (t0 as @{const conj}) \$ t1 \$ t2 => do_conjunction t0 t1 t2 accum
-        | (t0 as @{const implies}) \$ t1 \$ t2 => do_implies t0 t1 t2 accum
+          Const (@{const_name all}, _) \$ Abs (_, T1, t1) => do_all T1 t1 accum
+        | @{const Trueprop} \$ t1 => do_formula t1 accum
+        | Const (@{const_name "=="}, _) \$ t1 \$ t2 =>
+          consider_general_equals mdata true t1 t2 accum
+        | @{const "==>"} \$ t1 \$ t2 => do_implies t1 t2 accum
+        | @{const Pure.conjunction} \$ t1 \$ t2 =>
+          fold (do_formula) [t1, t2] accum
+        | Const (@{const_name All}, _) \$ Abs (_, T1, t1) => do_all T1 t1 accum
+        | Const (@{const_name HOL.eq}, _) \$ t1 \$ t2 =>
+          consider_general_equals mdata true t1 t2 accum
+        | @{const conj} \$ t1 \$ t2 => fold (do_formula) [t1, t2] accum
+        | @{const implies} \$ t1 \$ t2 => do_implies t1 t2 accum
| _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
\do_formula", [t])
in do_formula t end
@@ -1213,37 +1123,26 @@
map (fn (x, M) => string_for_mtype_of_term ctxt asgs (Const x) M) consts
|> cat_lines)

-fun amass f t (ms, accum) =
-  let val (m, accum) = f t accum in (m :: ms, accum) end
-
-fun infer which no_harmless (hol_ctxt as {ctxt, tac_timeout, ...}) binarize
-          alpha_T (nondef_ts, def_ts) =
+fun formulas_monotonic (hol_ctxt as {ctxt, tac_timeout, ...}) binarize alpha_T
+                       (nondef_ts, def_ts) =
let
-    val _ = trace_msg (fn () => "****** " ^ which ^ " analysis: " ^
+    val _ = trace_msg (fn () => "****** Monotonicity analysis: " ^
string_for_mtype MAlpha ^ " is " ^
Syntax.string_of_typ ctxt alpha_T)
-    val mdata as {max_fresh, constr_mcache, ...} =
-      initial_mdata hol_ctxt binarize no_harmless alpha_T
-    val accum = (initial_gamma, ([], []))
-    val (nondef_ms, accum) =
-      ([], accum) |> amass (consider_general_formula mdata Plus) (hd nondef_ts)
-                  |> fold (amass (consider_nondefinitional_axiom mdata))
-                          (tl nondef_ts)
-    val (def_ms, (gamma, cset)) =
-      ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
+    val mdata as {max_fresh, ...} = initial_mdata hol_ctxt binarize alpha_T
+    val (gamma, cset) =
+      (initial_gamma, ([], []))
+      |> consider_general_formula mdata Plus (hd nondef_ts)
+      |> fold (consider_nondefinitional_axiom mdata) (tl nondef_ts)
+      |> fold (consider_definitional_axiom mdata) def_ts
in
case solve tac_timeout (!max_fresh) cset of
-      SOME asgs => (print_mcontext ctxt asgs gamma;
-                    SOME (asgs, (nondef_ms, def_ms), !constr_mcache))
-    | _ => NONE
+      SOME asgs => (print_mcontext ctxt asgs gamma; true)
+    | _ => false
end
-  handle UNSOLVABLE () => NONE
+  handle UNSOLVABLE () => false
| MTYPE (loc, Ms, Ts) =>
raise BAD (loc, commas (map string_for_mtype Ms @
map (Syntax.string_of_typ ctxt) Ts))
-       | MTERM (loc, ms) =>
-         raise BAD (loc, commas (map (string_for_mterm ctxt) ms))
-
-val formulas_monotonic = is_some oooo infer "Monotonicity" false

end;```