simplify monotonicity code after killing "fin_fun" optimization
authorblanchet
Tue Dec 07 11:56:56 2010 +0100 (2010-12-07)
changeset 41054e58d1cdda832
parent 41053 8e2f2398aae7
child 41055 d6f45159ae84
simplify monotonicity code after killing "fin_fun" optimization
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/Tools/Nitpick/nitpick_mono.ML
     1.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Dec 07 11:56:56 2010 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Dec 07 11:56:56 2010 +0100
     1.3 @@ -67,7 +67,6 @@
     1.4  ML {* Nitpick_Mono.trace := false *}
     1.5  
     1.6  ML {* const @{term "A\<Colon>('a\<Rightarrow>'b)"} *}
     1.7 -(*
     1.8  ML {* const @{term "(A\<Colon>'a set) = A"} *}
     1.9  ML {* const @{term "(A\<Colon>'a set set) = A"} *}
    1.10  ML {* const @{term "(\<lambda>x\<Colon>'a set. x a)"} *}
    1.11 @@ -138,7 +137,6 @@
    1.12  
    1.13  ML {* nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"} *}
    1.14  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"} *}
    1.15 -*)
    1.16  
    1.17  ML {*
    1.18  val preproc_timeout = SOME (seconds 5.0)
    1.19 @@ -184,8 +182,6 @@
    1.20  
    1.21  fun check_theory thy =
    1.22    let
    1.23 -    val finitizes = [(NONE, SOME false)]
    1.24 -    val monos = [(NONE, SOME false)]
    1.25      val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode)
    1.26      val _ = File.write path ""
    1.27      fun check_theorem (name, th) =
    1.28 @@ -193,8 +189,7 @@
    1.29          val t = th |> prop_of |> Type.legacy_freeze |> close_form
    1.30          val neg_t = Logic.mk_implies (t, @{prop False})
    1.31          val (nondef_ts, def_ts, _, _, _) =
    1.32 -          time_limit preproc_timeout
    1.33 -              (preprocess_formulas hol_ctxt finitizes monos []) neg_t
    1.34 +          time_limit preproc_timeout (preprocess_formulas hol_ctxt []) neg_t
    1.35          val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
    1.36        in File.append path (res ^ "\n"); writeln res end
    1.37        handle TimeLimit.TimeOut => ()
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 11:56:56 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 11:56:56 2010 +0100
     2.3 @@ -38,23 +38,16 @@
     2.4    MType of string * mtyp list |
     2.5    MRec of string * typ list
     2.6  
     2.7 -datatype mterm =
     2.8 -  MRaw of term * mtyp |
     2.9 -  MAbs of string * typ * mtyp * annotation_atom * mterm |
    2.10 -  MApp of mterm * mterm
    2.11 -
    2.12  type mdata =
    2.13    {hol_ctxt: hol_context,
    2.14     binarize: bool,
    2.15     alpha_T: typ,
    2.16 -   no_harmless: bool,
    2.17     max_fresh: int Unsynchronized.ref,
    2.18     datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
    2.19     constr_mcache: (styp * mtyp) list Unsynchronized.ref}
    2.20  
    2.21  exception UNSOLVABLE of unit
    2.22  exception MTYPE of string * mtyp list * typ list
    2.23 -exception MTERM of string * mterm list
    2.24  
    2.25  val trace = Unsynchronized.ref false
    2.26  fun trace_msg msg = if !trace then tracing (msg ()) else ()
    2.27 @@ -126,43 +119,9 @@
    2.28    | flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms
    2.29    | flatten_mtype M = [M]
    2.30  
    2.31 -fun precedence_of_mterm (MRaw _) = no_prec
    2.32 -  | precedence_of_mterm (MAbs _) = 1
    2.33 -  | precedence_of_mterm (MApp _) = 2
    2.34 -
    2.35 -fun string_for_mterm ctxt =
    2.36 -  let
    2.37 -    fun mtype_annotation M = "\<^bsup>" ^ string_for_mtype M ^ "\<^esup>"
    2.38 -    fun aux outer_prec m =
    2.39 -      let
    2.40 -        val prec = precedence_of_mterm m
    2.41 -        val need_parens = (prec < outer_prec)
    2.42 -      in
    2.43 -        (if need_parens then "(" else "") ^
    2.44 -        (case m of
    2.45 -           MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
    2.46 -         | MAbs (s, _, M, aa, m) =>
    2.47 -           "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
    2.48 -           string_for_annotation_atom aa ^ "\<^esup> " ^ aux prec m
    2.49 -         | MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^
    2.50 -        (if need_parens then ")" else "")
    2.51 -      end
    2.52 -  in aux 0 end
    2.53 -
    2.54 -fun mtype_of_mterm (MRaw (_, M)) = M
    2.55 -  | mtype_of_mterm (MAbs (_, _, M, aa, m)) = MFun (M, aa, mtype_of_mterm m)
    2.56 -  | mtype_of_mterm (MApp (m1, _)) =
    2.57 -    case mtype_of_mterm m1 of
    2.58 -      MFun (_, _, M12) => M12
    2.59 -    | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1], [])
    2.60 -
    2.61 -fun strip_mcomb (MApp (m1, m2)) = strip_mcomb m1 ||> (fn ms => append ms [m2])
    2.62 -  | strip_mcomb m = (m, [])
    2.63 -
    2.64 -fun initial_mdata hol_ctxt binarize no_harmless alpha_T =
    2.65 +fun initial_mdata hol_ctxt binarize alpha_T =
    2.66    ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
    2.67 -    no_harmless = no_harmless, max_fresh = Unsynchronized.ref 0,
    2.68 -    datatype_mcache = Unsynchronized.ref [],
    2.69 +    max_fresh = Unsynchronized.ref 0, datatype_mcache = Unsynchronized.ref [],
    2.70      constr_mcache = Unsynchronized.ref []} : mdata)
    2.71  
    2.72  fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
    2.73 @@ -243,7 +202,7 @@
    2.74                  $ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
    2.75    | fin_fun_body _ _ _ = NONE
    2.76  
    2.77 -(* ### FIXME: make sure well-annotated! *)
    2.78 +(* FIXME: make sure well-annotated *)
    2.79  
    2.80  fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) all_minus
    2.81                              T1 T2 =
    2.82 @@ -306,7 +265,8 @@
    2.83        | _ => MType (simple_string_of_typ T, [])
    2.84    in do_type end
    2.85  
    2.86 -val ground_and_sole_base_constrs = [] (* FIXME: [@{const_name Nil}, @{const_name None}], cf. lists_empty *)
    2.87 +val ground_and_sole_base_constrs = []
    2.88 +(* FIXME: [@{const_name Nil}, @{const_name None}], cf. lists_empty *)
    2.89  
    2.90  fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
    2.91    | prodM_factors M = [M]
    2.92 @@ -644,8 +604,6 @@
    2.93    {bound_Ts = bound_Ts, bound_Ms = bound_Ms, frame = frame, frees = frees,
    2.94     consts = consts}
    2.95  
    2.96 -(* FIXME: make sure tracing messages are complete *)
    2.97 -
    2.98  fun add_comp_frame aa cmp = fold (add_annotation_atom_comp cmp [] aa o snd)
    2.99  
   2.100  fun add_bound_frame j frame =
   2.101 @@ -691,11 +649,11 @@
   2.102     [(aa1, (Eq, Fls)), (aa2, (Neq, Gen)), (res_aa, (Eq, Gen))],
   2.103     [(aa1, (Eq, Fls)), (aa2, (Neq, New)), (res_aa, (Eq, Gen))]]
   2.104  
   2.105 -val meta_conj_triple = ("\<and>", conj_clauses, @{const Pure.conjunction})
   2.106 -val meta_imp_triple = ("\<implies>", imp_clauses, @{const "==>"})
   2.107 -val conj_triple = ("\<and>", conj_clauses, @{const conj})
   2.108 -val disj_triple = ("\<or>", disj_clauses, @{const disj})
   2.109 -val imp_triple = ("\<implies>", imp_clauses, @{const implies})
   2.110 +val meta_conj_spec = ("\<and>", conj_clauses)
   2.111 +val meta_imp_spec = ("\<implies>", imp_clauses)
   2.112 +val conj_spec = ("\<and>", conj_clauses)
   2.113 +val disj_spec = ("\<or>", disj_clauses)
   2.114 +val imp_spec = ("\<implies>", imp_clauses)
   2.115  
   2.116  fun add_annotation_clause_from_quasi_clause _ NONE = NONE
   2.117    | add_annotation_clause_from_quasi_clause [] accum = accum
   2.118 @@ -761,19 +719,17 @@
   2.119      #> fold add_arg_order1 (tl arg_frame ~~ (fst (split_last arg_frame)))
   2.120      #> fold (add_app1 fun_aa) (res_frame ~~ arg_frame)
   2.121  
   2.122 -fun consider_connective mdata (conn, mk_quasi_clauses, t0) do_t1 do_t2
   2.123 +fun consider_connective mdata (conn, mk_quasi_clauses) do_t1 do_t2
   2.124                          (accum as ({frame, ...}, _)) =
   2.125    let
   2.126 -    val mtype_for = fresh_mtype_for_type mdata false
   2.127      val frame1 = fresh_frame mdata (SOME Tru) NONE frame
   2.128      val frame2 = fresh_frame mdata (SOME Fls) NONE frame
   2.129 -    val (m1, accum) = accum |>> set_frame frame1 |> do_t1
   2.130 -    val (m2, accum) = accum |>> set_frame frame2 |> do_t2
   2.131    in
   2.132 -    (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
   2.133 -     accum |>> set_frame frame
   2.134 -           ||> apsnd (add_connective_frames conn mk_quasi_clauses frame frame1
   2.135 -                                            frame2))
   2.136 +    accum |>> set_frame frame1 |> do_t1
   2.137 +          |>> set_frame frame2 |> do_t2
   2.138 +          |>> set_frame frame
   2.139 +          ||> apsnd (add_connective_frames conn mk_quasi_clauses frame frame1
   2.140 +                                           frame2)
   2.141    end
   2.142  
   2.143  fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
   2.144 @@ -834,8 +790,9 @@
   2.145          M as MPair (a_M, b_M) =>
   2.146          pair (MFun (M, A Gen, if n = 0 then a_M else b_M))
   2.147        | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
   2.148 -    and do_connect triple t1 t2 =
   2.149 -      consider_connective mdata triple (do_term t1) (do_term t2)
   2.150 +    and do_connect spec t1 t2 accum =
   2.151 +      (bool_M, consider_connective mdata spec (snd o do_term t1)
   2.152 +                                   (snd o do_term t2) accum)
   2.153      and do_term t
   2.154              (accum as (gamma as {bound_Ts, bound_Ms, frame, frees, consts},
   2.155                         cset)) =
   2.156 @@ -843,12 +800,10 @@
   2.157                             " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
   2.158                             " : _?");
   2.159         case t of
   2.160 -         @{const False} =>
   2.161 -         (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame)
   2.162 +         @{const False} => (bool_M, accum ||> add_comp_frame (A Fls) Leq frame)
   2.163         | Const (@{const_name None}, T) =>
   2.164 -         (MRaw (t, mtype_for T), accum ||> add_comp_frame (A Fls) Leq frame)
   2.165 -       | @{const True} =>
   2.166 -         (MRaw (t, bool_M), accum ||> add_comp_frame (A Tru) Leq frame)
   2.167 +         (mtype_for T, accum ||> add_comp_frame (A Fls) Leq frame)
   2.168 +       | @{const True} => (bool_M, accum ||> add_comp_frame (A Tru) Leq frame)
   2.169         | (t0 as Const (@{const_name HOL.eq}, _)) $ Bound 0 $ t2 =>
   2.170           (* hack to exploit symmetry of equality when typing "insert" *)
   2.171           (if t2 = Bound 0 then do_term @{term True}
   2.172 @@ -870,7 +825,6 @@
   2.173                                    (Abs (Name.uu, domain_type set_T,
   2.174                                          @{const False}),
   2.175                                     Bound 0)))) accum
   2.176 -                |>> mtype_of_mterm
   2.177                end
   2.178              | @{const_name HOL.eq} => do_equals T accum
   2.179              | @{const_name The} =>
   2.180 @@ -947,7 +901,6 @@
   2.181                    (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms, frame = frame,
   2.182                          frees = frees, consts = (x, M) :: consts}, cset))
   2.183                  end)
   2.184 -           |>> curry MRaw t
   2.185             ||> apsnd (add_comp_frame (A Gen) Eq frame)
   2.186           | Free (x as (_, T)) =>
   2.187             (case AList.lookup (op =) frees x of
   2.188 @@ -957,20 +910,20 @@
   2.189                  (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms, frame = frame,
   2.190                        frees = (x, M) :: frees, consts = consts}, cset))
   2.191                end)
   2.192 -           |>> curry MRaw t ||> apsnd (add_comp_frame (A Gen) Eq frame)
   2.193 +           ||> apsnd (add_comp_frame (A Gen) Eq frame)
   2.194           | Var _ => (trace_msg (K "*** Var"); raise UNSOLVABLE ())
   2.195           | Bound j =>
   2.196 -           (MRaw (t, nth bound_Ms j),
   2.197 +           (nth bound_Ms j,
   2.198              accum ||> add_bound_frame (length bound_Ts - j - 1) frame)
   2.199 -         | Abs (s, T, t') =>
   2.200 +         | Abs (_, T, t') =>
   2.201             (case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of
   2.202                SOME t' =>
   2.203                let
   2.204                  val M = mtype_for T
   2.205                  val x = Unsynchronized.inc max_fresh
   2.206 -                val (m', accum) = do_term t' (accum |>> push_bound (V x) T M)
   2.207 +                val (M', accum) = do_term t' (accum |>> push_bound (V x) T M)
   2.208                in
   2.209 -                (MAbs (s, T, M, V x, m'),
   2.210 +                (MFun (M, V x, M'),
   2.211                   accum |>> pop_bound
   2.212                         ||> add_annotation_atom_comp Leq [] (A Fls) (V x))
   2.213                end
   2.214 @@ -992,13 +945,13 @@
   2.215                        let
   2.216                          val M = mtype_for T
   2.217                          val x = Unsynchronized.inc max_fresh
   2.218 -                        val (m', accum) =
   2.219 +                        val (M', accum) =
   2.220                            do_term t' (accum |>> push_bound (V x) T M)
   2.221 -                      in (MAbs (s, T, M, V x, m'), accum |>> pop_bound) end))
   2.222 -         | @{const Not} $ t1 => do_connect imp_triple t1 @{const False} accum
   2.223 -         | @{const conj} $ t1 $ t2 => do_connect conj_triple t1 t2 accum
   2.224 -         | @{const disj} $ t1 $ t2 => do_connect disj_triple t1 t2 accum
   2.225 -         | @{const implies} $ t1 $ t2 => do_connect imp_triple t1 t2 accum
   2.226 +                      in (MFun (M, V x, M'), accum |>> pop_bound) end))
   2.227 +         | @{const Not} $ t1 => do_connect imp_spec t1 @{const False} accum
   2.228 +         | @{const conj} $ t1 $ t2 => do_connect conj_spec t1 t2 accum
   2.229 +         | @{const disj} $ t1 $ t2 => do_connect disj_spec t1 t2 accum
   2.230 +         | @{const implies} $ t1 $ t2 => do_connect imp_spec t1 t2 accum
   2.231           | Const (@{const_name Let}, _) $ t1 $ t2 =>
   2.232             do_term (betapply (t2, t1)) accum
   2.233           | t1 $ t2 =>
   2.234 @@ -1011,121 +964,106 @@
   2.235               val frame2b =
   2.236                 frame1b |> map (apsnd (fn _ => V (Unsynchronized.inc max_fresh)))
   2.237               val frame2 = frame2a @ frame2b
   2.238 -             val (m1, accum) = accum |>> set_frame frame1a |> do_term t1
   2.239 -             val (m2, accum) = accum |>> set_frame frame2 |> do_term t2
   2.240 +             val (M1, accum) = accum |>> set_frame frame1a |> do_term t1
   2.241 +             val (M2, accum) = accum |>> set_frame frame2 |> do_term t2
   2.242             in
   2.243               let
   2.244 -               val (M11, aa, _) = mtype_of_mterm m1 |> dest_MFun
   2.245 -               val M2 = mtype_of_mterm m2
   2.246 +               val (M11, aa, M12) = M1 |> dest_MFun
   2.247               in
   2.248 -               (MApp (m1, m2),
   2.249 -                accum |>> set_frame frame
   2.250 -                      ||> add_is_sub_mtype M2 M11
   2.251 -                      ||> add_app aa frame1b frame2b)
   2.252 +               (M12, accum |>> set_frame frame
   2.253 +                           ||> add_is_sub_mtype M2 M11
   2.254 +                           ||> add_app aa frame1b frame2b)
   2.255               end
   2.256             end)
   2.257 -        |> tap (fn (m, (gamma, _)) =>
   2.258 +        |> tap (fn (M, (gamma, _)) =>
   2.259                     trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
   2.260                                         " \<turnstile> " ^
   2.261 -                                       string_for_mterm ctxt m))
   2.262 +                                       Syntax.string_of_term ctxt t ^ " : " ^
   2.263 +                                       string_for_mtype M))
   2.264    in do_term end
   2.265  
   2.266  fun force_gen_funs 0 _ = I
   2.267    | force_gen_funs n (M as MFun (M1, _, M2)) =
   2.268      add_mtypes_equal M (MFun (M1, A Gen, M2)) #> force_gen_funs (n - 1) M2
   2.269    | force_gen_funs _ M = raise MTYPE ("Nitpick_Mono.force_gen_funs", [M], [])
   2.270 -fun consider_general_equals mdata def (x as (_, T)) t1 t2 accum =
   2.271 +fun consider_general_equals mdata def t1 t2 accum =
   2.272    let
   2.273 -    val (m1, accum) = consider_term mdata t1 accum
   2.274 -    val (m2, accum) = consider_term mdata t2 accum
   2.275 -    val M1 = mtype_of_mterm m1
   2.276 -    val M2 = mtype_of_mterm m2
   2.277 +    val (M1, accum) = consider_term mdata t1 accum
   2.278 +    val (M2, accum) = consider_term mdata t2 accum
   2.279      val accum = accum ||> add_mtypes_equal M1 M2
   2.280 -    val body_M = fresh_mtype_for_type mdata false (nth_range_type 2 T)
   2.281 -    val m = MApp (MApp (MRaw (Const x,
   2.282 -                           MFun (M1, A Gen, MFun (M2, A Gen, body_M))), m1), m2)
   2.283    in
   2.284 -    (m, (if def then
   2.285 -           let val (head_m, arg_ms) = strip_mcomb m1 in
   2.286 -             accum ||> force_gen_funs (length arg_ms) (mtype_of_mterm head_m)
   2.287 -           end
   2.288 -         else
   2.289 -           accum))
   2.290 +    if def then
   2.291 +      let
   2.292 +        val (head1, args1) = strip_comb t1
   2.293 +        val (head_M1, accum) = consider_term mdata head1 accum
   2.294 +      in accum ||> force_gen_funs (length args1) head_M1 end
   2.295 +    else
   2.296 +      accum
   2.297    end
   2.298  
   2.299  fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, max_fresh,
   2.300                                          ...}) =
   2.301    let
   2.302      val mtype_for = fresh_mtype_for_type mdata false
   2.303 -    val do_term = consider_term mdata
   2.304 +    val do_term = snd oo consider_term mdata
   2.305      fun do_formula sn t (accum as (gamma, _)) =
   2.306        let
   2.307 -        fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
   2.308 +        fun do_quantifier quant_s abs_T body_t =
   2.309            let
   2.310              val abs_M = mtype_for abs_T
   2.311              val x = Unsynchronized.inc max_fresh
   2.312              val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
   2.313              fun ann () = if quant_s = @{const_name Ex} then Fls else Tru
   2.314 -            val (body_m, accum) =
   2.315 -              accum ||> side_cond
   2.316 -                        ? add_mtype_is_complete [(x, (Plus, ann ()))] abs_M
   2.317 -                    |>> push_bound (V x) abs_T abs_M |> do_formula sn body_t
   2.318 -            val body_M = mtype_of_mterm body_m
   2.319            in
   2.320 -            (MApp (MRaw (Const quant_x,
   2.321 -                         MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M)),
   2.322 -                   MAbs (abs_s, abs_T, abs_M, A Gen, body_m)),
   2.323 -             accum |>> pop_bound)
   2.324 +            accum ||> side_cond
   2.325 +                      ? add_mtype_is_complete [(x, (Plus, ann ()))] abs_M
   2.326 +                  |>> push_bound (V x) abs_T abs_M
   2.327 +                  |> do_formula sn body_t
   2.328 +                  |>> pop_bound
   2.329            end
   2.330 -        fun do_connect triple neg1 t1 t2 =
   2.331 -          consider_connective mdata triple
   2.332 +        fun do_connect spec neg1 t1 t2 =
   2.333 +          consider_connective mdata spec
   2.334                (do_formula (sn |> neg1 ? negate_sign) t1) (do_formula sn t2)
   2.335 -        fun do_equals x t1 t2 =
   2.336 +        fun do_equals t1 t2 =
   2.337            case sn of
   2.338              Plus => do_term t accum
   2.339 -          | Minus => consider_general_equals mdata false x t1 t2 accum
   2.340 +          | Minus => consider_general_equals mdata false t1 t2 accum
   2.341        in
   2.342          trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
   2.343                              " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
   2.344                              " : o\<^sup>" ^ string_for_sign sn ^ "?");
   2.345          case t of
   2.346 -          Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
   2.347 -          do_quantifier x s1 T1 t1
   2.348 -        | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
   2.349 -        | @{const Trueprop} $ t1 =>
   2.350 -          let val (m1, accum) = do_formula sn t1 accum in
   2.351 -            (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)), m1),
   2.352 -             accum)
   2.353 -          end
   2.354 -        | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
   2.355 -          do_quantifier x s1 T1 t1
   2.356 -        | Const (x0 as (@{const_name Ex}, T0)) $ (t1 as Abs (s1, T1, t1')) =>
   2.357 +          Const (s as @{const_name all}, _) $ Abs (_, T1, t1) =>
   2.358 +          do_quantifier s T1 t1
   2.359 +        | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2
   2.360 +        | @{const Trueprop} $ t1 => do_formula sn t1 accum
   2.361 +        | Const (s as @{const_name All}, _) $ Abs (_, T1, t1) =>
   2.362 +          do_quantifier s T1 t1
   2.363 +        | Const (s as @{const_name Ex}, T0) $ (t1 as Abs (_, T1, t1')) =>
   2.364            (case sn of
   2.365 -             Plus => do_quantifier x0 s1 T1 t1'
   2.366 +             Plus => do_quantifier s T1 t1'
   2.367             | Minus =>
   2.368 -             (* FIXME: Move elsewhere *)
   2.369 +             (* FIXME: Needed? *)
   2.370               do_term (@{const Not}
   2.371                        $ (HOLogic.eq_const (domain_type T0) $ t1
   2.372                           $ Abs (Name.uu, T1, @{const False}))) accum)
   2.373 -        | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 => do_equals x t1 t2
   2.374 +        | Const (@{const_name HOL.eq}, _) $ t1 $ t2 => do_equals t1 t2
   2.375          | Const (@{const_name Let}, _) $ t1 $ t2 =>
   2.376            do_formula sn (betapply (t2, t1)) accum
   2.377          | @{const Pure.conjunction} $ t1 $ t2 =>
   2.378 -          do_connect meta_conj_triple false t1 t2 accum
   2.379 -        | @{const "==>"} $ t1 $ t2 =>
   2.380 -          do_connect meta_imp_triple true t1 t2 accum
   2.381 -        | @{const Not} $ t1 =>
   2.382 -          do_connect imp_triple true t1 @{const False} accum
   2.383 -        | @{const conj} $ t1 $ t2 => do_connect conj_triple false t1 t2 accum
   2.384 -        | @{const disj} $ t1 $ t2 => do_connect disj_triple false t1 t2 accum
   2.385 -        | @{const implies} $ t1 $ t2 => do_connect imp_triple true t1 t2 accum
   2.386 +          do_connect meta_conj_spec false t1 t2 accum
   2.387 +        | @{const "==>"} $ t1 $ t2 => do_connect meta_imp_spec true t1 t2 accum
   2.388 +        | @{const Not} $ t1 => do_connect imp_spec true t1 @{const False} accum
   2.389 +        | @{const conj} $ t1 $ t2 => do_connect conj_spec false t1 t2 accum
   2.390 +        | @{const disj} $ t1 $ t2 => do_connect disj_spec false t1 t2 accum
   2.391 +        | @{const implies} $ t1 $ t2 => do_connect imp_spec true t1 t2 accum
   2.392          | _ => do_term t accum
   2.393        end
   2.394 -      |> tap (fn (m, (gamma, _)) =>
   2.395 +      |> tap (fn (gamma, _) =>
   2.396                   trace_msg (fn () => string_for_mcontext ctxt t gamma ^
   2.397                                       " \<turnstile> " ^
   2.398 -                                     string_for_mterm ctxt m ^ " : o\<^sup>" ^
   2.399 -                                     string_for_sign sn))
   2.400 +                                     Syntax.string_of_term ctxt t ^
   2.401 +                                     " : o\<^sup>" ^ string_for_sign sn))
   2.402    in do_formula end
   2.403  
   2.404  (* The harmless axiom optimization below is somewhat too aggressive in the face
   2.405 @@ -1134,72 +1072,44 @@
   2.406    [@{const_name ord_class.less}, @{const_name ord_class.less_eq}]
   2.407  val bounteous_consts = [@{const_name bisim}]
   2.408  
   2.409 -fun is_harmless_axiom ({no_harmless = true, ...} : mdata) _ = false
   2.410 -  | is_harmless_axiom {hol_ctxt = {thy, stds, ...}, ...} t =
   2.411 +fun is_harmless_axiom {hol_ctxt = {thy, stds, ...}, ...} t =
   2.412      Term.add_consts t []
   2.413      |> filter_out (is_built_in_const thy stds)
   2.414      |> (forall (member (op =) harmless_consts o original_name o fst) orf
   2.415          exists (member (op =) bounteous_consts o fst))
   2.416  
   2.417  fun consider_nondefinitional_axiom mdata t =
   2.418 -  if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M))
   2.419 +  if is_harmless_axiom mdata t then I
   2.420    else consider_general_formula mdata Plus t
   2.421  
   2.422  fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...}) t =
   2.423    if not (is_constr_pattern_formula ctxt t) then
   2.424      consider_nondefinitional_axiom mdata t
   2.425    else if is_harmless_axiom mdata t then
   2.426 -    pair (MRaw (t, dummy_M))
   2.427 +    I
   2.428    else
   2.429      let
   2.430        val mtype_for = fresh_mtype_for_type mdata false
   2.431 -      val do_term = consider_term mdata
   2.432 -      fun do_all quant_t abs_s abs_T body_t accum =
   2.433 -        let
   2.434 -          val abs_M = mtype_for abs_T
   2.435 -          val (body_m, accum) =
   2.436 -            accum |>> push_bound (A Gen) abs_T abs_M |> do_formula body_t
   2.437 -          val body_M = mtype_of_mterm body_m
   2.438 -        in
   2.439 -          (MApp (MRaw (quant_t, MFun (MFun (abs_M, A Gen, body_M), A Gen,
   2.440 -                       body_M)),
   2.441 -                 MAbs (abs_s, abs_T, abs_M, A Gen, body_m)),
   2.442 -           accum |>> pop_bound)
   2.443 -        end
   2.444 -      and do_conjunction t0 t1 t2 accum =
   2.445 -        let
   2.446 -          val (m1, accum) = do_formula t1 accum
   2.447 -          val (m2, accum) = do_formula t2 accum
   2.448 -        in
   2.449 -          (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
   2.450 -        end
   2.451 -      and do_implies t0 t1 t2 accum =
   2.452 -        let
   2.453 -          val (m1, accum) = do_term t1 accum
   2.454 -          val (m2, accum) = do_formula t2 accum
   2.455 -        in
   2.456 -          (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
   2.457 -        end
   2.458 +      val do_term = snd oo consider_term mdata
   2.459 +      fun do_all abs_T body_t accum =
   2.460 +        accum |>> push_bound (A Gen) abs_T (mtype_for abs_T)
   2.461 +              |> do_formula body_t
   2.462 +              |>> pop_bound
   2.463 +      and do_implies t1 t2 = do_term t1 #> do_formula t2
   2.464        and do_formula t accum =
   2.465          case t of
   2.466 -          (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
   2.467 -          do_all t0 s1 T1 t1 accum
   2.468 -        | @{const Trueprop} $ t1 =>
   2.469 -          let val (m1, accum) = do_formula t1 accum in
   2.470 -            (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)), m1),
   2.471 -             accum)
   2.472 -          end
   2.473 -        | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
   2.474 -          consider_general_equals mdata true x t1 t2 accum
   2.475 -        | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
   2.476 -        | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
   2.477 -          do_conjunction t0 t1 t2 accum
   2.478 -        | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
   2.479 -          do_all t0 s0 T1 t1 accum
   2.480 -        | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
   2.481 -          consider_general_equals mdata true x t1 t2 accum
   2.482 -        | (t0 as @{const conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
   2.483 -        | (t0 as @{const implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
   2.484 +          Const (@{const_name all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
   2.485 +        | @{const Trueprop} $ t1 => do_formula t1 accum
   2.486 +        | Const (@{const_name "=="}, _) $ t1 $ t2 =>
   2.487 +          consider_general_equals mdata true t1 t2 accum
   2.488 +        | @{const "==>"} $ t1 $ t2 => do_implies t1 t2 accum
   2.489 +        | @{const Pure.conjunction} $ t1 $ t2 =>
   2.490 +          fold (do_formula) [t1, t2] accum
   2.491 +        | Const (@{const_name All}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
   2.492 +        | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
   2.493 +          consider_general_equals mdata true t1 t2 accum
   2.494 +        | @{const conj} $ t1 $ t2 => fold (do_formula) [t1, t2] accum
   2.495 +        | @{const implies} $ t1 $ t2 => do_implies t1 t2 accum
   2.496          | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
   2.497                             \do_formula", [t])
   2.498      in do_formula t end
   2.499 @@ -1213,37 +1123,26 @@
   2.500        map (fn (x, M) => string_for_mtype_of_term ctxt asgs (Const x) M) consts
   2.501        |> cat_lines)
   2.502  
   2.503 -fun amass f t (ms, accum) =
   2.504 -  let val (m, accum) = f t accum in (m :: ms, accum) end
   2.505 -
   2.506 -fun infer which no_harmless (hol_ctxt as {ctxt, tac_timeout, ...}) binarize
   2.507 -          alpha_T (nondef_ts, def_ts) =
   2.508 +fun formulas_monotonic (hol_ctxt as {ctxt, tac_timeout, ...}) binarize alpha_T
   2.509 +                       (nondef_ts, def_ts) =
   2.510    let
   2.511 -    val _ = trace_msg (fn () => "****** " ^ which ^ " analysis: " ^
   2.512 +    val _ = trace_msg (fn () => "****** Monotonicity analysis: " ^
   2.513                                  string_for_mtype MAlpha ^ " is " ^
   2.514                                  Syntax.string_of_typ ctxt alpha_T)
   2.515 -    val mdata as {max_fresh, constr_mcache, ...} =
   2.516 -      initial_mdata hol_ctxt binarize no_harmless alpha_T
   2.517 -    val accum = (initial_gamma, ([], []))
   2.518 -    val (nondef_ms, accum) =
   2.519 -      ([], accum) |> amass (consider_general_formula mdata Plus) (hd nondef_ts)
   2.520 -                  |> fold (amass (consider_nondefinitional_axiom mdata))
   2.521 -                          (tl nondef_ts)
   2.522 -    val (def_ms, (gamma, cset)) =
   2.523 -      ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
   2.524 +    val mdata as {max_fresh, ...} = initial_mdata hol_ctxt binarize alpha_T
   2.525 +    val (gamma, cset) =
   2.526 +      (initial_gamma, ([], []))
   2.527 +      |> consider_general_formula mdata Plus (hd nondef_ts)
   2.528 +      |> fold (consider_nondefinitional_axiom mdata) (tl nondef_ts)
   2.529 +      |> fold (consider_definitional_axiom mdata) def_ts
   2.530    in
   2.531      case solve tac_timeout (!max_fresh) cset of
   2.532 -      SOME asgs => (print_mcontext ctxt asgs gamma;
   2.533 -                    SOME (asgs, (nondef_ms, def_ms), !constr_mcache))
   2.534 -    | _ => NONE
   2.535 +      SOME asgs => (print_mcontext ctxt asgs gamma; true)
   2.536 +    | _ => false
   2.537    end
   2.538 -  handle UNSOLVABLE () => NONE
   2.539 +  handle UNSOLVABLE () => false
   2.540         | MTYPE (loc, Ms, Ts) =>
   2.541           raise BAD (loc, commas (map string_for_mtype Ms @
   2.542                                   map (Syntax.string_of_typ ctxt) Ts))
   2.543 -       | MTERM (loc, ms) =>
   2.544 -         raise BAD (loc, commas (map (string_for_mterm ctxt) ms))
   2.545 -
   2.546 -val formulas_monotonic = is_some oooo infer "Monotonicity" false
   2.547  
   2.548  end;