more work on the new monotonicity stuff in Nitpick
authorblanchet
Fri Feb 26 16:49:46 2010 +0100 (2010-02-26)
changeset 3538645a4e19d3ebd
parent 35385 29f81babefd7
child 35387 4356263e0bdd
more work on the new monotonicity stuff in Nitpick
doc-src/Nitpick/nitpick.tex
src/HOL/Nitpick_Examples/Core_Nits.thy
src/HOL/Nitpick_Examples/Datatype_Nits.thy
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/Nitpick_Examples/Typedef_Nits.thy
src/HOL/Tools/Nitpick/HISTORY
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Feb 25 16:33:39 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Fri Feb 26 16:49:46 2010 +0100
     1.3 @@ -2743,8 +2743,8 @@
     1.4  \item[$\bullet$] Although this has never been observed, arbitrary theorem
     1.5  morphisms could possibly confuse Nitpick, resulting in spurious counterexamples.
     1.6  
     1.7 -%\item[$\bullet$] All constants and types whose names start with
     1.8 -%\textit{Nitpick}{.} are reserved for internal use.
     1.9 +\item[$\bullet$] All constants, types, free variables, and schematic variables
    1.10 +whose names start with \textit{Nitpick}{.} are reserved for internal use.
    1.11  \end{enum}
    1.12  
    1.13  \let\em=\sl
     2.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Thu Feb 25 16:33:39 2010 +0100
     2.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Feb 26 16:49:46 2010 +0100
     2.3 @@ -1000,7 +1000,7 @@
     2.4  oops
     2.5  
     2.6  lemma "(Q\<Colon>nat set) (Eps Q)"
     2.7 -nitpick [expect = none]
     2.8 +nitpick [expect = none] (* unfortunate *)
     2.9  oops
    2.10  
    2.11  lemma "\<not> Q (Eps Q)"
    2.12 @@ -1053,11 +1053,11 @@
    2.13  
    2.14  lemma "Q = {x\<Colon>'a} \<Longrightarrow> (Q\<Colon>'a set) (The Q)"
    2.15  nitpick [expect = none]
    2.16 -oops
    2.17 +sorry
    2.18  
    2.19  lemma "Q = {x\<Colon>nat} \<Longrightarrow> (Q\<Colon>nat set) (The Q)"
    2.20  nitpick [expect = none]
    2.21 -oops
    2.22 +sorry
    2.23  
    2.24  subsection {* Destructors and Recursors *}
    2.25  
     3.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Thu Feb 25 16:33:39 2010 +0100
     3.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Fri Feb 26 16:49:46 2010 +0100
     3.3 @@ -69,7 +69,7 @@
     3.4  oops
     3.5  
     3.6  lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
     3.7 -nitpick [card = 1\<midarrow>10, expect = none]
     3.8 +nitpick [card = 1\<midarrow>9, expect = none]
     3.9  sorry
    3.10  
    3.11  lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
     4.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Feb 25 16:33:39 2010 +0100
     4.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Fri Feb 26 16:49:46 2010 +0100
     4.3 @@ -30,7 +30,7 @@
     4.4     special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
     4.5     wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
     4.6  (* term -> bool *)
     4.7 -val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} [] []
     4.8 +fun is_mono t = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} ([t], [])
     4.9  fun is_const t =
    4.10    let val T = fastype_of t in
    4.11      is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
    4.12 @@ -46,26 +46,26 @@
    4.13  ML {* const @{term "(A::'a set) = A"} *}
    4.14  ML {* const @{term "(A::'a set set) = A"} *}
    4.15  ML {* const @{term "(\<lambda>x::'a set. x a)"} *}
    4.16 -ML {* const @{term "{{a}} = C"} *}
    4.17 +ML {* const @{term "{{a::'a}} = C"} *}
    4.18  ML {* const @{term "{f::'a\<Rightarrow>nat} = {g::'a\<Rightarrow>nat}"} *}
    4.19 -ML {* const @{term "A \<union> B"} *}
    4.20 +ML {* const @{term "A \<union> (B::'a set)"} *}
    4.21  ML {* const @{term "P (a::'a)"} *}
    4.22  ML {* const @{term "\<lambda>a::'a. b (c (d::'a)) (e::'a) (f::'a)"} *}
    4.23  ML {* const @{term "\<forall>A::'a set. A a"} *}
    4.24  ML {* const @{term "\<forall>A::'a set. P A"} *}
    4.25  ML {* const @{term "P \<or> Q"} *}
    4.26 -ML {* const @{term "A \<union> B = C"} *}
    4.27 +ML {* const @{term "A \<union> B = (C::'a set)"} *}
    4.28  ML {* const @{term "(if P then (A::'a set) else B) = C"} *}
    4.29 -ML {* const @{term "let A = C in A \<union> B"} *}
    4.30 +ML {* const @{term "let A = (C::'a set) in A \<union> B"} *}
    4.31  ML {* const @{term "THE x::'b. P x"} *}
    4.32 -ML {* const @{term "{}::'a set"} *}
    4.33 +ML {* const @{term "(\<lambda>x::'a. False)"} *}
    4.34  ML {* const @{term "(\<lambda>x::'a. True)"} *}
    4.35 -ML {* const @{term "Let a A"} *}
    4.36 +ML {* const @{term "Let (a::'a) A"} *}
    4.37  ML {* const @{term "A (a::'a)"} *}
    4.38 -ML {* const @{term "insert a A = B"} *}
    4.39 +ML {* const @{term "insert (a::'a) A = B"} *}
    4.40  ML {* const @{term "- (A::'a set)"} *}
    4.41 -ML {* const @{term "finite A"} *}
    4.42 -ML {* const @{term "\<not> finite A"} *}
    4.43 +ML {* const @{term "finite (A::'a set)"} *}
    4.44 +ML {* const @{term "\<not> finite (A::'a set)"} *}
    4.45  ML {* const @{term "finite (A::'a set set)"} *}
    4.46  ML {* const @{term "\<lambda>a::'a. A a \<and> \<not> B a"} *}
    4.47  ML {* const @{term "A < (B::'a set)"} *}
    4.48 @@ -74,27 +74,25 @@
    4.49  ML {* const @{term "[a::'a set]"} *}
    4.50  ML {* const @{term "[A \<union> (B::'a set)]"} *}
    4.51  ML {* const @{term "[A \<union> (B::'a set)] = [C]"} *}
    4.52 -ML {* const @{term "\<forall>P. P a"} *}
    4.53  
    4.54 -ML {* nonconst @{term "{%x. True}"} *}
    4.55 -ML {* nonconst @{term "{(%x. x = a)} = C"} *}
    4.56 +ML {* nonconst @{term "{(\<lambda>x::'a. x = a)} = C"} *}
    4.57  ML {* nonconst @{term "\<forall>P (a::'a). P a"} *}
    4.58  ML {* nonconst @{term "\<forall>a::'a. P a"} *}
    4.59  ML {* nonconst @{term "(\<lambda>a::'a. \<not> A a) = B"} *}
    4.60 -ML {* nonconst @{term "THE x. P x"} *}
    4.61 -ML {* nonconst @{term "SOME x. P x"} *}
    4.62 +ML {* nonconst @{term "THE x::'a. P x"} *}
    4.63 +ML {* nonconst @{term "SOME x::'a. P x"} *}
    4.64  
    4.65  ML {* mono @{prop "Q (\<forall>x::'a set. P x)"} *}
    4.66  ML {* mono @{prop "P (a::'a)"} *}
    4.67 -ML {* mono @{prop "{a} = {b}"} *}
    4.68 +ML {* mono @{prop "{a} = {b::'a}"} *}
    4.69  ML {* mono @{prop "P (a::'a) \<and> P \<union> P = P"} *}
    4.70  ML {* mono @{prop "\<forall>F::'a set set. P"} *}
    4.71  ML {* mono @{prop "\<not> (\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h)"} *}
    4.72  ML {* mono @{prop "\<not> Q (\<forall>x::'a set. P x)"} *}
    4.73 -ML {* mono @{prop "\<not> (\<forall>x. P x)"} *}
    4.74 +ML {* mono @{prop "\<not> (\<forall>x::'a. P x)"} *}
    4.75  
    4.76 -ML {* nonmono @{prop "\<forall>x. P x"} *}
    4.77 +ML {* nonmono @{prop "\<forall>x::'a. P x"} *}
    4.78 +ML {* nonmono @{prop "myall P = (P = (\<lambda>x::'a. True))"} *}
    4.79  ML {* nonmono @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h"} *}
    4.80 -ML {* nonmono @{prop "myall P = (P = (\<lambda>x. True))"} *}
    4.81  
    4.82  end
     5.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Thu Feb 25 16:33:39 2010 +0100
     5.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Feb 26 16:49:46 2010 +0100
     5.3 @@ -64,7 +64,7 @@
     5.4  oops
     5.5  
     5.6  lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y"
     5.7 -nitpick [expect = none]
     5.8 +nitpick [fast_descrs (* ### FIXME *), expect = none]
     5.9  sorry
    5.10  
    5.11  lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
     6.1 --- a/src/HOL/Tools/Nitpick/HISTORY	Thu Feb 25 16:33:39 2010 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Fri Feb 26 16:49:46 2010 +0100
     6.3 @@ -4,7 +4,9 @@
     6.4    * Added "std" option and implemented support for nonstandard models
     6.5    * Added support for quotient types
     6.6    * Added support for local definitions
     6.7 -  * Optimized "Multiset.multiset"
     6.8 +  * Disabled "fast_descrs" option by default
     6.9 +  * Optimized "Multiset.multiset" and "FinFun.finfun"
    6.10 +  * Improved efficiency of "destroy_constrs" optimization
    6.11    * Improved precision of infinite datatypes whose constructors don't appear
    6.12      in the formula to falsify based on a monotonicity analysis
    6.13    * Fixed soundness bugs related to "destroy_constrs" optimization and record
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Feb 25 16:33:39 2010 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Feb 26 16:49:46 2010 +0100
     7.3 @@ -131,9 +131,7 @@
     7.4    nonsel_names: nut list,
     7.5    rel_table: nut NameTable.table,
     7.6    unsound: bool,
     7.7 -  scope: scope,
     7.8 -  core: KK.formula,
     7.9 -  defs: KK.formula list}
    7.10 +  scope: scope}
    7.11  
    7.12  type rich_problem = KK.problem * problem_extension
    7.13  
    7.14 @@ -195,7 +193,8 @@
    7.15      val timer = Timer.startRealTimer ()
    7.16      val thy = Proof.theory_of state
    7.17      val ctxt = Proof.context_of state
    7.18 -(* FIXME: reintroduce code before new release
    7.19 +(* FIXME: reintroduce code before new release:
    7.20 +
    7.21      val nitpick_thy = ThyInfo.get_theory "Nitpick"
    7.22      val _ = Theory.subthy (nitpick_thy, thy) orelse
    7.23              error "You must import the theory \"Nitpick\" to use Nitpick"
    7.24 @@ -289,8 +288,8 @@
    7.25      val frees = Term.add_frees assms_t []
    7.26      val _ = null (Term.add_tvars assms_t []) orelse
    7.27              raise NOT_SUPPORTED "schematic type variables"
    7.28 -    val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
    7.29 -         core_t, binarize) = preprocess_term hol_ctxt assms_t
    7.30 +    val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
    7.31 +         binarize) = preprocess_term hol_ctxt assms_t
    7.32      val got_all_user_axioms =
    7.33        got_all_mono_user_axioms andalso no_poly_user_axioms
    7.34  
    7.35 @@ -307,28 +306,25 @@
    7.36                     \unroll it.")))
    7.37      val _ = if verbose then List.app print_wf (!wf_cache) else ()
    7.38      val _ =
    7.39 -      pprint_d (fn () =>
    7.40 -          Pretty.chunks
    7.41 -              (pretties_for_formulas ctxt "Preprocessed formula" [core_t] @
    7.42 -               pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @
    7.43 -               pretties_for_formulas ctxt "Relevant nondefinitional axiom"
    7.44 -                                     nondef_ts))
    7.45 -    val _ = List.app (ignore o Term.type_of) (core_t :: def_ts @ nondef_ts)
    7.46 +      pprint_d (fn () => Pretty.chunks
    7.47 +          (pretties_for_formulas ctxt "Preprocessed formula" [hd nondef_ts] @
    7.48 +           pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @
    7.49 +           pretties_for_formulas ctxt "Relevant nondefinitional axiom"
    7.50 +                                 (tl nondef_ts)))
    7.51 +    val _ = List.app (ignore o Term.type_of) (nondef_ts @ def_ts)
    7.52              handle TYPE (_, Ts, ts) =>
    7.53                     raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
    7.54  
    7.55 -    val core_u = nut_from_term hol_ctxt Eq core_t
    7.56 +    val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
    7.57      val def_us = map (nut_from_term hol_ctxt DefEq) def_ts
    7.58 -    val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
    7.59      val (free_names, const_names) =
    7.60 -      fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
    7.61 +      fold add_free_and_const_names (nondef_us @ def_us) ([], [])
    7.62      val (sel_names, nonsel_names) =
    7.63        List.partition (is_sel o nickname_of) const_names
    7.64      val genuine_means_genuine = got_all_user_axioms andalso none_true wfs
    7.65      val standard = forall snd stds
    7.66  (*
    7.67 -    val _ = List.app (priority o string_for_nut ctxt)
    7.68 -                     (core_u :: def_us @ nondef_us)
    7.69 +    val _ = List.app (priority o string_for_nut ctxt) (nondef_us @ def_us)
    7.70  *)
    7.71  
    7.72      val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
    7.73 @@ -349,7 +345,7 @@
    7.74         (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
    7.75        is_number_type thy T orelse is_bit_type T
    7.76      fun is_type_actually_monotonic T =
    7.77 -      formulas_monotonic hol_ctxt binarize T (def_ts, nondef_ts, core_t)
    7.78 +      formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
    7.79      fun is_type_monotonic T =
    7.80        unique_scope orelse
    7.81        case triple_lookup (type_match thy) monos T of
    7.82 @@ -362,14 +358,14 @@
    7.83      fun is_datatype_deep T =
    7.84        not standard orelse T = nat_T orelse is_word_type T orelse
    7.85        exists (curry (op =) T o domain_type o type_of) sel_names
    7.86 -    val all_Ts = ground_types_in_terms hol_ctxt binarize
    7.87 -                                       (core_t :: def_ts @ nondef_ts)
    7.88 +    val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
    7.89                   |> sort TermOrd.typ_ord
    7.90      val _ = if verbose andalso binary_ints = SOME true andalso
    7.91                 exists (member (op =) [nat_T, int_T]) all_Ts then
    7.92                print_v (K "The option \"binary_ints\" will be ignored because \
    7.93                           \of the presence of rationals, reals, \"Suc\", \
    7.94 -                         \\"gcd\", or \"lcm\" in the problem.")
    7.95 +                         \\"gcd\", or \"lcm\" in the problem or because of the \
    7.96 +                         \\"non_std\" option.")
    7.97              else
    7.98                ()
    7.99      val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
   7.100 @@ -480,7 +476,6 @@
   7.101                           (univ_card nat_card int_card main_j0 [] KK.True)
   7.102          val _ = check_arity min_univ_card min_highest_arity
   7.103  
   7.104 -        val core_u = choose_reps_in_nut scope unsound rep_table false core_u
   7.105          val def_us = map (choose_reps_in_nut scope unsound rep_table true)
   7.106                           def_us
   7.107          val nondef_us = map (choose_reps_in_nut scope unsound rep_table false)
   7.108 @@ -488,7 +483,7 @@
   7.109  (*
   7.110          val _ = List.app (priority o string_for_nut ctxt)
   7.111                           (free_names @ sel_names @ nonsel_names @
   7.112 -                          core_u :: def_us @ nondef_us)
   7.113 +                          nondef_us @ def_us)
   7.114  *)
   7.115          val (free_rels, pool, rel_table) =
   7.116            rename_free_vars free_names initial_pool NameTable.empty
   7.117 @@ -496,13 +491,11 @@
   7.118            rename_free_vars sel_names pool rel_table
   7.119          val (other_rels, pool, rel_table) =
   7.120            rename_free_vars nonsel_names pool rel_table
   7.121 -        val core_u = rename_vars_in_nut pool rel_table core_u
   7.122 +        val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
   7.123          val def_us = map (rename_vars_in_nut pool rel_table) def_us
   7.124 -        val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
   7.125 -        val core_f = kodkod_formula_from_nut ofs kk core_u
   7.126 +        val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
   7.127          val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
   7.128 -        val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
   7.129 -        val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
   7.130 +        val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
   7.131          val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
   7.132                        PrintMode.setmp [] multiline_string_for_scope scope
   7.133          val kodkod_sat_solver =
   7.134 @@ -550,8 +543,7 @@
   7.135                 expr_assigns = [], formula = formula},
   7.136                {free_names = free_names, sel_names = sel_names,
   7.137                 nonsel_names = nonsel_names, rel_table = rel_table,
   7.138 -               unsound = unsound, scope = scope, core = core_f,
   7.139 -               defs = nondef_fs @ def_fs @ declarative_axioms})
   7.140 +               unsound = unsound, scope = scope})
   7.141        end
   7.142        handle TOO_LARGE (loc, msg) =>
   7.143               if loc = "Nitpick_Kodkod.check_arity" andalso
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Feb 25 16:33:39 2010 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Feb 26 16:49:46 2010 +0100
     8.3 @@ -154,6 +154,7 @@
     8.4      hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
     8.5    val is_finite_type : hol_context -> typ -> bool
     8.6    val special_bounds : term list -> (indexname * typ) list
     8.7 +  val abs_var : indexname * typ -> term -> term
     8.8    val is_funky_typedef : theory -> typ -> bool
     8.9    val all_axioms_of :
    8.10      theory -> (term * term) list -> term list * term list * term list
    8.11 @@ -631,8 +632,13 @@
    8.12         in
    8.13           case t_opt of
    8.14             SOME (Const (@{const_name top}, _)) => true
    8.15 +           (* "Multiset.multiset" *)
    8.16           | SOME (Const (@{const_name Collect}, _)
    8.17                   $ Abs (_, _, Const (@{const_name finite}, _) $ _)) => true
    8.18 +           (* "FinFun.finfun" *)
    8.19 +         | SOME (Const (@{const_name Collect}, _) $ Abs (_, _,
    8.20 +                     Const (@{const_name Ex}, _) $ Abs (_, _,
    8.21 +                         Const (@{const_name finite}, _) $ _))) => true
    8.22           | _ => false
    8.23         end
    8.24       | NONE => false)
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Feb 25 16:33:39 2010 +0100
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Feb 26 16:49:46 2010 +0100
     9.3 @@ -444,7 +444,7 @@
     9.4    single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1
     9.5  (* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr)
     9.6     -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr *)
     9.7 -fun tripl_rel_rel_let kk f r1 r2 r3 =
     9.8 +fun triple_rel_rel_let kk f r1 r2 r3 =
     9.9    double_rel_rel_let kk
    9.10        (fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2
    9.11  
    9.12 @@ -1615,7 +1615,7 @@
    9.13          kk_rel_let [to_expr_assign u1 u2] (to_rep R u3)
    9.14        | Op3 (If, _, R, u1, u2, u3) =>
    9.15          if is_opt_rep (rep_of u1) then
    9.16 -          tripl_rel_rel_let kk
    9.17 +          triple_rel_rel_let kk
    9.18                (fn r1 => fn r2 => fn r3 =>
    9.19                    let val empty_r = empty_rel_for_rep R in
    9.20                      fold1 kk_union
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 25 16:33:39 2010 +0100
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Feb 26 16:49:46 2010 +0100
    10.3 @@ -10,7 +10,7 @@
    10.4    type hol_context = Nitpick_HOL.hol_context
    10.5  
    10.6    val formulas_monotonic :
    10.7 -    hol_context -> bool -> typ -> term list * term list * term -> bool
    10.8 +    hol_context -> bool -> typ -> term list * term list -> bool
    10.9  end;
   10.10  
   10.11  structure Nitpick_Mono : NITPICK_MONO =
   10.12 @@ -34,7 +34,7 @@
   10.13    MRec of string * typ list
   10.14  
   10.15  datatype mterm =
   10.16 -  MAtom of term * mtyp |
   10.17 +  MRaw of term * mtyp |
   10.18    MAbs of string * typ * mtyp * sign_atom * mterm |
   10.19    MApp of mterm * mterm
   10.20  
   10.21 @@ -76,7 +76,7 @@
   10.22  fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn
   10.23  
   10.24  val bool_M = MType (@{type_name bool}, [])
   10.25 -val irrelevant_M = MType (nitpick_prefix ^ "irrelevant", [])
   10.26 +val dummy_M = MType (nitpick_prefix ^ "dummy", [])
   10.27  
   10.28  (* mtyp -> bool *)
   10.29  fun is_MRec (MRec _) = true
   10.30 @@ -102,16 +102,19 @@
   10.31          val need_parens = (prec < outer_prec)
   10.32        in
   10.33          (if need_parens then "(" else "") ^
   10.34 -        (case M of
   10.35 -           MAlpha => "\<alpha>"
   10.36 -         | MFun (M1, a, M2) =>
   10.37 -           aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^
   10.38 -           string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2
   10.39 -         | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2
   10.40 -         | MType (s, []) =>
   10.41 -           if s = @{type_name prop} orelse s = @{type_name bool} then "o" else s
   10.42 -         | MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s
   10.43 -         | MRec (s, _) => "[" ^ s ^ "]") ^
   10.44 +        (if M = dummy_M then
   10.45 +           "_"
   10.46 +         else case M of
   10.47 +             MAlpha => "\<alpha>"
   10.48 +           | MFun (M1, a, M2) =>
   10.49 +             aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^
   10.50 +             string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2
   10.51 +           | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2
   10.52 +           | MType (s, []) =>
   10.53 +             if s = @{type_name prop} orelse s = @{type_name bool} then "o"
   10.54 +             else s
   10.55 +           | MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s
   10.56 +           | MRec (s, _) => "[" ^ s ^ "]") ^
   10.57          (if need_parens then ")" else "")
   10.58        end
   10.59    in aux 0 end
   10.60 @@ -122,7 +125,7 @@
   10.61    | flatten_mtype M = [M]
   10.62  
   10.63  (* mterm -> bool *)
   10.64 -fun precedence_of_mterm (MAtom _) = no_prec
   10.65 +fun precedence_of_mterm (MRaw _) = no_prec
   10.66    | precedence_of_mterm (MAbs _) = 1
   10.67    | precedence_of_mterm (MApp _) = 2
   10.68  
   10.69 @@ -139,7 +142,7 @@
   10.70        in
   10.71          (if need_parens then "(" else "") ^
   10.72          (case m of
   10.73 -           MAtom (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
   10.74 +           MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
   10.75           | MAbs (s, _, M, a, m) =>
   10.76             "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
   10.77             string_for_sign_atom a ^ "\<^esup> " ^ aux prec m
   10.78 @@ -149,7 +152,7 @@
   10.79    in aux 0 end
   10.80  
   10.81  (* mterm -> mtyp *)
   10.82 -fun mtype_of_mterm (MAtom (_, M)) = M
   10.83 +fun mtype_of_mterm (MRaw (_, M)) = M
   10.84    | mtype_of_mterm (MAbs (_, _, M, a, m)) = MFun (M, a, mtype_of_mterm m)
   10.85    | mtype_of_mterm (MApp (m1, _)) =
   10.86      case mtype_of_mterm m1 of
   10.87 @@ -545,19 +548,28 @@
   10.88  fun solve _ UnsolvableCSet = (print_g "*** Problem: Unsolvable"; NONE)
   10.89    | solve max_var (CSet (lits, comps, sexps)) =
   10.90      let
   10.91 +      (* (int -> bool option) -> literal list option *)
   10.92 +      fun do_assigns assigns =
   10.93 +        SOME (literals_from_assignments max_var assigns lits
   10.94 +              |> tap print_solution)
   10.95        val _ = print_problem lits comps sexps
   10.96        val prop = PropLogic.all (map prop_for_literal lits @
   10.97                                  map prop_for_comp comps @
   10.98                                  map prop_for_sign_expr sexps)
   10.99 -      (* use the first ML solver (to avoid startup overhead) *)
  10.100 -      val solvers = !SatSolver.solvers
  10.101 -                    |> filter (member (op =) ["dptsat", "dpll"] o fst)
  10.102 +      val default_val = bool_from_sign Minus
  10.103      in
  10.104 -      case snd (hd solvers) prop of
  10.105 -        SatSolver.SATISFIABLE assigns =>
  10.106 -        SOME (literals_from_assignments max_var assigns lits
  10.107 -              |> tap print_solution)
  10.108 -      | _ => NONE
  10.109 +      if PropLogic.eval (K default_val) prop then
  10.110 +        do_assigns (K (SOME default_val))
  10.111 +      else
  10.112 +        let
  10.113 +          (* use the first ML solver (to avoid startup overhead) *)
  10.114 +          val solvers = !SatSolver.solvers
  10.115 +                        |> filter (member (op =) ["dptsat", "dpll"] o fst)
  10.116 +        in
  10.117 +          case snd (hd solvers) prop of
  10.118 +            SatSolver.SATISFIABLE assigns => do_assigns assigns
  10.119 +          | _ => NONE
  10.120 +        end
  10.121      end
  10.122  
  10.123  type mtype_schema = mtyp * constraint_set
  10.124 @@ -580,7 +592,7 @@
  10.125    handle List.Empty => initial_gamma
  10.126  
  10.127  (* mdata -> term -> accumulator -> mterm * accumulator *)
  10.128 -fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs,
  10.129 +fun consider_term (mdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
  10.130                                           def_table, ...},
  10.131                               alpha_T, max_fresh, ...}) =
  10.132    let
  10.133 @@ -595,7 +607,7 @@
  10.134      fun do_all T (gamma, cset) =
  10.135        let
  10.136          val abs_M = mtype_for (domain_type (domain_type T))
  10.137 -        val body_M = mtype_for (range_type T)
  10.138 +        val body_M = mtype_for (body_type T)
  10.139        in
  10.140          (MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M),
  10.141           (gamma, cset |> add_mtype_is_right_total abs_M))
  10.142 @@ -641,9 +653,9 @@
  10.143          pair (MFun (M, S Minus, if n = 0 then a_M else b_M))
  10.144        | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M])
  10.145      (* mtyp * accumulator *)
  10.146 -    val mtype_unsolvable = (irrelevant_M, unsolvable_accum)
  10.147 +    val mtype_unsolvable = (dummy_M, unsolvable_accum)
  10.148      (* term -> mterm * accumulator *)
  10.149 -    fun mterm_unsolvable t = (MAtom (t, irrelevant_M), unsolvable_accum)
  10.150 +    fun mterm_unsolvable t = (MRaw (t, dummy_M), unsolvable_accum)
  10.151      (* term -> string -> typ -> term -> term -> term -> accumulator
  10.152         -> mterm * accumulator *)
  10.153      fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
  10.154 @@ -657,10 +669,11 @@
  10.155          val bound_M = mtype_of_mterm bound_m
  10.156          val (M1, a, M2) = dest_MFun bound_M
  10.157        in
  10.158 -        (MApp (MAtom (t0, MFun (bound_M, S Minus, bool_M)),
  10.159 +        (MApp (MRaw (t0, MFun (bound_M, S Minus, bool_M)),
  10.160                 MAbs (abs_s, abs_T, M1, a,
  10.161 -                     MApp (MApp (MAtom (connective_t, irrelevant_M),
  10.162 -                                 MApp (bound_m, MAtom (Bound 0, M1))),
  10.163 +                     MApp (MApp (MRaw (connective_t,
  10.164 +                                       mtype_for (fastype_of connective_t)),
  10.165 +                                 MApp (bound_m, MRaw (Bound 0, M1))),
  10.166                             body_m))), accum)
  10.167        end
  10.168      (* term -> accumulator -> mterm * accumulator *)
  10.169 @@ -678,10 +691,14 @@
  10.170                | @{const_name "=="} => do_equals T accum
  10.171                | @{const_name All} => do_all T accum
  10.172                | @{const_name Ex} =>
  10.173 -                do_term (@{const Not}
  10.174 -                         $ (HOLogic.eq_const (domain_type T)
  10.175 -                            $ Abs (Name.uu, T, @{const False}))) accum
  10.176 -                |>> mtype_of_mterm
  10.177 +                let val set_T = domain_type T in
  10.178 +                  do_term (Abs (Name.uu, set_T,
  10.179 +                                @{const Not} $ (HOLogic.mk_eq
  10.180 +                                    (Abs (Name.uu, domain_type set_T,
  10.181 +                                          @{const False}),
  10.182 +                                     Bound 0)))) accum
  10.183 +                  |>> mtype_of_mterm
  10.184 +                end
  10.185                | @{const_name "op ="} => do_equals T accum
  10.186                | @{const_name The} => (print_g "*** The"; mtype_unsolvable)
  10.187                | @{const_name Eps} => (print_g "*** Eps"; mtype_unsolvable)
  10.188 @@ -719,9 +736,12 @@
  10.189                | @{const_name rtrancl} =>
  10.190                  (print_g "*** rtrancl"; mtype_unsolvable)
  10.191                | @{const_name finite} =>
  10.192 -                let val M1 = mtype_for (domain_type (domain_type T)) in
  10.193 -                  (MFun (pos_set_mtype_for_dom M1, S Minus, bool_M), accum)
  10.194 -                end
  10.195 +                if is_finite_type hol_ctxt T then
  10.196 +                  let val M1 = mtype_for (domain_type (domain_type T)) in
  10.197 +                    (MFun (pos_set_mtype_for_dom M1, S Minus, bool_M), accum)
  10.198 +                  end
  10.199 +                else
  10.200 +                  (print_g "*** finite"; mtype_unsolvable)
  10.201                | @{const_name rel_comp} =>
  10.202                  let
  10.203                    val x = Unsynchronized.inc max_fresh
  10.204 @@ -807,7 +827,7 @@
  10.205                    let val M = mtype_for T in
  10.206                      (M, ({bounds = bounds, frees = frees,
  10.207                            consts = (x, M) :: consts}, cset))
  10.208 -                  end) |>> curry MAtom t
  10.209 +                  end) |>> curry MRaw t
  10.210           | Free (x as (_, T)) =>
  10.211             (case AList.lookup (op =) frees x of
  10.212                SOME M => (M, accum)
  10.213 @@ -815,12 +835,12 @@
  10.214                let val M = mtype_for T in
  10.215                  (M, ({bounds = bounds, frees = (x, M) :: frees,
  10.216                        consts = consts}, cset))
  10.217 -              end) |>> curry MAtom t
  10.218 +              end) |>> curry MRaw t
  10.219           | Var _ => (print_g "*** Var"; mterm_unsolvable t)
  10.220 -         | Bound j => (MAtom (t, nth bounds j), accum)
  10.221 +         | Bound j => (MRaw (t, nth bounds j), accum)
  10.222           | Abs (s, T, t' as @{const False}) =>
  10.223             let val (M1, a, M2) = mfun_for T bool_T in
  10.224 -             (MAbs (s, T, M1, a, MAtom (t', M2)), accum)
  10.225 +             (MAbs (s, T, M1, a, MRaw (t', M2)), accum)
  10.226             end
  10.227           | Abs (s, T, t') =>
  10.228             ((case t' of
  10.229 @@ -850,88 +870,109 @@
  10.230             in
  10.231               case accum of
  10.232                 (_, UnsolvableCSet) => mterm_unsolvable t
  10.233 -             | _ => (MApp (m1, m2), accum)
  10.234 +             | _ =>
  10.235 +               let
  10.236 +                 val M11 = mtype_of_mterm m1 |> dest_MFun |> #1
  10.237 +                 val M2 = mtype_of_mterm m2
  10.238 +               in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
  10.239             end)
  10.240          |> tap (fn (m, _) => print_g ("  \<Gamma> \<turnstile> " ^
  10.241                                        string_for_mterm ctxt m))
  10.242    in do_term end
  10.243  
  10.244 -(* mdata -> sign -> term -> accumulator -> accumulator *)
  10.245 +(* mdata -> styp -> term -> term -> mterm * accumulator *)
  10.246 +fun consider_general_equals mdata (x as (_, T)) t1 t2 accum =
  10.247 +  let
  10.248 +    val (m1, accum) = consider_term mdata t1 accum
  10.249 +    val (m2, accum) = consider_term mdata t2 accum
  10.250 +    val M1 = mtype_of_mterm m1
  10.251 +    val M2 = mtype_of_mterm m2
  10.252 +    val body_M = fresh_mtype_for_type mdata (nth_range_type 2 T)
  10.253 +  in
  10.254 +    (MApp (MApp (MRaw (Const x,
  10.255 +         MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2),
  10.256 +     accum ||> add_mtypes_equal M1 M2)
  10.257 +  end
  10.258 +
  10.259 +(* mdata -> sign -> term -> accumulator -> mterm * accumulator *)
  10.260  fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) =
  10.261    let
  10.262      (* typ -> mtyp *)
  10.263      val mtype_for = fresh_mtype_for_type mdata
  10.264 -    (* term -> accumulator -> mtyp * accumulator *)
  10.265 -    val do_term = apfst mtype_of_mterm oo consider_term mdata
  10.266 -    (* sign -> term -> accumulator -> accumulator *)
  10.267 -    fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
  10.268 -      | do_formula sn t (accum as (gamma, cset)) =
  10.269 +    (* term -> accumulator -> mterm * accumulator *)
  10.270 +    val do_term = consider_term mdata
  10.271 +    (* sign -> term -> accumulator -> mterm * accumulator *)
  10.272 +    fun do_formula _ t (_, UnsolvableCSet) =
  10.273 +        (MRaw (t, dummy_M), unsolvable_accum)
  10.274 +      | do_formula sn t accum =
  10.275          let
  10.276 -          (* term -> accumulator -> accumulator *)
  10.277 -          val do_co_formula = do_formula sn
  10.278 -          val do_contra_formula = do_formula (negate sn)
  10.279 -          (* string -> typ -> term -> accumulator *)
  10.280 -          fun do_quantifier quant_s abs_T body_t =
  10.281 +          (* styp -> string -> typ -> term -> mterm * accumulator *)
  10.282 +          fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
  10.283              let
  10.284                val abs_M = mtype_for abs_T
  10.285                val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
  10.286 -              val cset = cset |> side_cond ? add_mtype_is_right_total abs_M
  10.287 +              val (body_m, accum) =
  10.288 +                accum ||> side_cond ? add_mtype_is_right_total abs_M
  10.289 +                      |>> push_bound abs_M |> do_formula sn body_t
  10.290 +              val body_M = mtype_of_mterm body_m
  10.291              in
  10.292 -              (gamma |> push_bound abs_M, cset)
  10.293 -              |> do_co_formula body_t |>> pop_bound
  10.294 +              (MApp (MRaw (Const quant_x, MFun (abs_M, S Minus, body_M)),
  10.295 +                     MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
  10.296 +               accum |>> pop_bound)
  10.297              end
  10.298 -          (* typ -> term -> accumulator *)
  10.299 -          fun do_bounded_quantifier abs_T body_t =
  10.300 -            accum |>> push_bound (mtype_for abs_T) |> do_co_formula body_t
  10.301 -                  |>> pop_bound
  10.302 -          (* term -> term -> accumulator *)
  10.303 -          fun do_equals t1 t2 =
  10.304 +          (* styp -> term -> term -> mterm * accumulator *)
  10.305 +          fun do_equals x t1 t2 =
  10.306              case sn of
  10.307 -              Plus => do_term t accum |> snd
  10.308 -            | Minus => let
  10.309 -                         val (M1, accum) = do_term t1 accum
  10.310 -                         val (M2, accum) = do_term t2 accum
  10.311 -                       in accum ||> add_mtypes_equal M1 M2 end
  10.312 +              Plus => do_term t accum
  10.313 +            | Minus => consider_general_equals mdata x t1 t2 accum
  10.314          in
  10.315            case t of
  10.316 -            Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>
  10.317 -            do_quantifier s0 T1 t1
  10.318 -          | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2
  10.319 -          | @{const "==>"} $ t1 $ t2 =>
  10.320 -            accum |> do_contra_formula t1 |> do_co_formula t2
  10.321 -          | @{const Trueprop} $ t1 => do_co_formula t1 accum
  10.322 -          | @{const Not} $ t1 => do_contra_formula t1 accum
  10.323 -          | Const (@{const_name All}, _)
  10.324 -            $ Abs (_, T1, t1 as @{const "op -->"} $ (_ $ Bound 0) $ _) =>
  10.325 -            do_bounded_quantifier T1 t1
  10.326 -          | Const (s0 as @{const_name All}, _) $ Abs (_, T1, t1) =>
  10.327 -            do_quantifier s0 T1 t1
  10.328 -          | Const (@{const_name Ex}, _)
  10.329 -            $ Abs (_, T1, t1 as @{const "op &"} $ (_ $ Bound 0) $ _) =>
  10.330 -            do_bounded_quantifier T1 t1
  10.331 -          | Const (s0 as @{const_name Ex}, T0) $ (t1 as Abs (_, T1, t1')) =>
  10.332 +            Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
  10.333 +            do_quantifier x s1 T1 t1
  10.334 +          | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
  10.335 +          | @{const Trueprop} $ t1 =>
  10.336 +            let val (m1, accum) = do_formula sn t1 accum in
  10.337 +              (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
  10.338 +                     m1), accum)
  10.339 +            end
  10.340 +          | @{const Not} $ t1 =>
  10.341 +            let val (m1, accum) = do_formula (negate sn) t1 accum in
  10.342 +              (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
  10.343 +               accum)
  10.344 +            end
  10.345 +          | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
  10.346 +            do_quantifier x s1 T1 t1
  10.347 +          | Const (x0 as (s0 as @{const_name Ex}, T0))
  10.348 +            $ (t1 as Abs (s1, T1, t1')) =>
  10.349              (case sn of
  10.350 -               Plus => do_quantifier s0 T1 t1'
  10.351 +               Plus => do_quantifier x0 s1 T1 t1'
  10.352               | Minus =>
  10.353 +               (* ### do elsewhere *)
  10.354                 do_term (@{const Not}
  10.355                          $ (HOLogic.eq_const (domain_type T0) $ t1
  10.356 -                           $ Abs (Name.uu, T1, @{const False}))) accum |> snd)
  10.357 -          | Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2
  10.358 -          | @{const "op &"} $ t1 $ t2 =>
  10.359 -            accum |> do_co_formula t1 |> do_co_formula t2
  10.360 -          | @{const "op |"} $ t1 $ t2 =>
  10.361 -            accum |> do_co_formula t1 |> do_co_formula t2
  10.362 -          | @{const "op -->"} $ t1 $ t2 =>
  10.363 -            accum |> do_contra_formula t1 |> do_co_formula t2
  10.364 -          | Const (@{const_name If}, _) $ t1 $ t2 $ t3 =>
  10.365 -            accum |> do_term t1 |> snd |> fold do_co_formula [t2, t3]
  10.366 -          | Const (@{const_name Let}, _) $ t1 $ t2 =>
  10.367 -            do_co_formula (betapply (t2, t1)) accum
  10.368 -          | _ => do_term t accum |> snd
  10.369 +                           $ Abs (Name.uu, T1, @{const False}))) accum)
  10.370 +          | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
  10.371 +            do_equals x t1 t2
  10.372 +          | (t0 as Const (s0, _)) $ t1 $ t2 =>
  10.373 +            if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
  10.374 +               s0 = @{const_name "op |"} orelse s0 = @{const_name "op -->"} then
  10.375 +              let
  10.376 +                val impl = (s0 = @{const_name "==>"} orelse
  10.377 +                           s0 = @{const_name "op -->"})
  10.378 +                val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
  10.379 +                val (m2, accum) = do_formula sn t2 accum
  10.380 +              in
  10.381 +                (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
  10.382 +                 accum)
  10.383 +              end 
  10.384 +            else
  10.385 +              do_term t accum
  10.386 +          | _ => do_term t accum
  10.387          end
  10.388 -        |> tap (fn _ => print_g ("\<Gamma> \<turnstile> " ^
  10.389 -                                 Syntax.string_of_term ctxt t ^
  10.390 -                                 " : o\<^sup>" ^ string_for_sign sn))
  10.391 +        |> tap (fn (m, _) =>
  10.392 +                   print_g ("\<Gamma> \<turnstile> " ^
  10.393 +                            string_for_mterm ctxt m ^ " : o\<^sup>" ^
  10.394 +                            string_for_sign sn))
  10.395    in do_formula end
  10.396  
  10.397  (* The harmless axiom optimization below is somewhat too aggressive in the face
  10.398 @@ -947,46 +988,69 @@
  10.399    |> (forall (member (op =) harmless_consts o original_name o fst)
  10.400        orf exists (member (op =) bounteous_consts o fst))
  10.401  
  10.402 -(* mdata -> sign -> term -> accumulator -> accumulator *)
  10.403 -fun consider_nondefinitional_axiom (mdata as {hol_ctxt, ...}) sn t =
  10.404 -  not (is_harmless_axiom hol_ctxt t) ? consider_general_formula mdata sn t
  10.405 +(* mdata -> term -> accumulator -> mterm * accumulator *)
  10.406 +fun consider_nondefinitional_axiom (mdata as {hol_ctxt, ...}) t =
  10.407 +  if is_harmless_axiom hol_ctxt t then pair (MRaw (t, dummy_M))
  10.408 +  else consider_general_formula mdata Plus t
  10.409  
  10.410 -(* mdata -> term -> accumulator -> accumulator *)
  10.411 +(* mdata -> term -> accumulator -> mterm * accumulator *)
  10.412  fun consider_definitional_axiom (mdata as {hol_ctxt as {thy, ...}, ...}) t =
  10.413    if not (is_constr_pattern_formula thy t) then
  10.414 -    consider_nondefinitional_axiom mdata Plus t
  10.415 +    consider_nondefinitional_axiom mdata t
  10.416    else if is_harmless_axiom hol_ctxt t then
  10.417 -    I
  10.418 +    pair (MRaw (t, dummy_M))
  10.419    else
  10.420      let
  10.421 -      (* term -> accumulator -> mtyp * accumulator *)
  10.422 -      val do_term = apfst mtype_of_mterm oo consider_term mdata
  10.423 -      (* typ -> term -> accumulator -> accumulator *)
  10.424 -      fun do_all abs_T body_t accum =
  10.425 -        let val abs_M = fresh_mtype_for_type mdata abs_T in
  10.426 -          accum |>> push_bound abs_M |> do_formula body_t |>> pop_bound
  10.427 +      (* typ -> mtyp *)
  10.428 +      val mtype_for = fresh_mtype_for_type mdata
  10.429 +      (* term -> accumulator -> mterm * accumulator *)
  10.430 +      val do_term = consider_term mdata
  10.431 +      (* term -> string -> typ -> term -> accumulator -> mterm * accumulator *)
  10.432 +      fun do_all quant_t abs_s abs_T body_t accum =
  10.433 +        let
  10.434 +          val abs_M = mtype_for abs_T
  10.435 +          val (body_m, accum) =
  10.436 +            accum |>> push_bound abs_M |> do_formula body_t
  10.437 +          val body_M = mtype_of_mterm body_m
  10.438 +        in
  10.439 +          (MApp (MRaw (quant_t, MFun (abs_M, S Minus, body_M)),
  10.440 +                 MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
  10.441 +           accum |>> pop_bound)
  10.442          end
  10.443 -      (* term -> term -> accumulator -> accumulator *)
  10.444 -      and do_implies t1 t2 = do_term t1 #> snd #> do_formula t2
  10.445 -      and do_equals t1 t2 accum =
  10.446 +      (* term -> term -> term -> accumulator -> mterm * accumulator *)
  10.447 +      and do_conjunction t0 t1 t2 accum =
  10.448          let
  10.449 -          val (M1, accum) = do_term t1 accum
  10.450 -          val (M2, accum) = do_term t2 accum
  10.451 -        in accum ||> add_mtypes_equal M1 M2 end
  10.452 +          val (m1, accum) = do_formula t1 accum
  10.453 +          val (m2, accum) = do_formula t2 accum
  10.454 +        in
  10.455 +          (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
  10.456 +        end
  10.457 +      and do_implies t0 t1 t2 accum =
  10.458 +        let
  10.459 +          val (m1, accum) = do_term t1 accum
  10.460 +          val (m2, accum) = do_formula t2 accum
  10.461 +        in
  10.462 +          (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
  10.463 +        end
  10.464        (* term -> accumulator -> accumulator *)
  10.465 -      and do_formula _ (_, UnsolvableCSet) = unsolvable_accum
  10.466 +      and do_formula t (_, UnsolvableCSet) =
  10.467 +          (MRaw (t, dummy_M), unsolvable_accum)
  10.468          | do_formula t accum =
  10.469            case t of
  10.470 -            Const (@{const_name all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
  10.471 +            (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
  10.472 +            do_all t0 s1 T1 t1 accum
  10.473            | @{const Trueprop} $ t1 => do_formula t1 accum
  10.474 -          | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2 accum
  10.475 -          | @{const "==>"} $ t1 $ t2 => do_implies t1 t2 accum
  10.476 -          | @{const Pure.conjunction} $ t1 $ t2 =>
  10.477 -            accum |> do_formula t1 |> do_formula t2
  10.478 -          | Const (@{const_name All}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
  10.479 -          | Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2 accum
  10.480 -          | @{const "op &"} $ t1 $ t2 => accum |> do_formula t1 |> do_formula t2
  10.481 -          | @{const "op -->"} $ t1 $ t2 => do_implies t1 t2 accum
  10.482 +          | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
  10.483 +            consider_general_equals mdata x t1 t2 accum
  10.484 +          | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
  10.485 +          | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
  10.486 +            do_conjunction t0 t1 t2 accum
  10.487 +          | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
  10.488 +            do_all t0 s0 T1 t1 accum
  10.489 +          | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
  10.490 +            consider_general_equals mdata x t1 t2 accum
  10.491 +          | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
  10.492 +          | (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
  10.493            | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
  10.494                               \do_formula", [t])
  10.495      in do_formula t end
  10.496 @@ -1002,20 +1066,27 @@
  10.497    map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
  10.498    |> cat_lines |> print_g
  10.499  
  10.500 -(* hol_context -> bool -> typ -> term list * term list * term -> bool *)
  10.501 +(* ('a -> 'b -> 'c * 'd) -> 'a -> 'c list * 'b -> 'c list * 'd *)
  10.502 +fun gather f t (ms, accum) =
  10.503 +  let val (m, accum) = f t accum in (m :: ms, accum) end
  10.504 +
  10.505 +(* hol_context -> bool -> typ -> term list * term list -> bool *)
  10.506  fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T
  10.507 -                       (def_ts, nondef_ts, core_t) =
  10.508 +                       (nondef_ts, def_ts) =
  10.509    let
  10.510      val _ = print_g ("****** Monotonicity analysis: " ^
  10.511                       string_for_mtype MAlpha ^ " is " ^
  10.512                       Syntax.string_of_typ ctxt alpha_T)
  10.513      val mdata as {max_fresh, constr_cache, ...} =
  10.514        initial_mdata hol_ctxt binarize alpha_T
  10.515 -    val (gamma as {frees, consts, ...}, cset) =
  10.516 -      (initial_gamma, slack)
  10.517 -      |> fold (consider_definitional_axiom mdata) def_ts
  10.518 -      |> fold (consider_nondefinitional_axiom mdata Plus) nondef_ts
  10.519 -      |> consider_general_formula mdata Plus core_t
  10.520 +
  10.521 +    val accum = (initial_gamma, slack)
  10.522 +    val (nondef_ms, accum) =
  10.523 +      ([], accum) |> gather (consider_general_formula mdata Plus) (hd nondef_ts)
  10.524 +                  |> fold (gather (consider_nondefinitional_axiom mdata))
  10.525 +                          (tl nondef_ts)
  10.526 +    val (def_ms, (gamma, cset)) =
  10.527 +      ([], accum) |> fold (gather (consider_definitional_axiom mdata)) def_ts
  10.528    in
  10.529      case solve (!max_fresh) cset of
  10.530        SOME lits => (print_mtype_context ctxt lits gamma; true)
    11.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Feb 25 16:33:39 2010 +0100
    11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Feb 26 16:49:46 2010 +0100
    11.3 @@ -9,8 +9,7 @@
    11.4  sig
    11.5    type hol_context = Nitpick_HOL.hol_context
    11.6    val preprocess_term :
    11.7 -    hol_context -> term
    11.8 -    -> ((term list * term list) * (bool * bool)) * term * bool
    11.9 +    hol_context -> term -> term list * term list * bool * bool * bool
   11.10  end
   11.11  
   11.12  structure Nitpick_Preproc : NITPICK_PREPROC =
   11.13 @@ -473,6 +472,19 @@
   11.14            (list_comb (t, args), seen)
   11.15    in aux [] 0 t [] [] |> fst end
   11.16  
   11.17 +val let_var_prefix = nitpick_prefix ^ "l"
   11.18 +val let_inline_threshold = 32
   11.19 +
   11.20 +(* int -> typ -> term -> (term -> term) -> term *)
   11.21 +fun hol_let n abs_T body_T f t =
   11.22 +  if n * size_of_term t <= let_inline_threshold then
   11.23 +    f t
   11.24 +  else
   11.25 +    let val z = ((let_var_prefix, 0), abs_T) in
   11.26 +      Const (@{const_name Let}, abs_T --> (abs_T --> body_T) --> body_T)
   11.27 +      $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
   11.28 +    end
   11.29 +
   11.30  (* hol_context -> bool -> term -> term *)
   11.31  fun destroy_pulled_out_constrs (hol_ctxt as {thy, stds, ...}) axiom t =
   11.32    let
   11.33 @@ -507,14 +519,19 @@
   11.34            if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
   11.35            else raise SAME ()
   11.36          | (Const (x as (s, T)), args) =>
   11.37 -          let val arg_Ts = binder_types T in
   11.38 -            if length arg_Ts = length args andalso
   11.39 -               (is_constr thy stds x orelse s = @{const_name Pair}) andalso
   11.40 +          let
   11.41 +            val (arg_Ts, dataT) = strip_type T
   11.42 +            val n = length arg_Ts
   11.43 +          in
   11.44 +            if length args = n andalso
   11.45 +               (is_constr thy stds x orelse s = @{const_name Pair} orelse
   11.46 +                x = (@{const_name Suc}, nat_T --> nat_T)) andalso
   11.47                 (not careful orelse not (is_Var t1) orelse
   11.48                  String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
   11.49 -              discriminate_value hol_ctxt x t1 ::
   11.50 -              map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
   11.51 -              |> foldr1 s_conj
   11.52 +                hol_let (n + 1) dataT bool_T
   11.53 +                    (fn t1 => discriminate_value hol_ctxt x t1 ::
   11.54 +                              map3 (sel_eq x t1) (index_seq 0 n) arg_Ts args
   11.55 +                              |> foldr1 s_conj) t1
   11.56              else
   11.57                raise SAME ()
   11.58            end
   11.59 @@ -1019,7 +1036,7 @@
   11.60  (* Prevents divergence in case of cyclic or infinite axiom dependencies. *)
   11.61  val axioms_max_depth = 255
   11.62  
   11.63 -(* hol_context -> term -> (term list * term list) * (bool * bool) *)
   11.64 +(* hol_context -> term -> term list * term list * bool * bool *)
   11.65  fun axioms_for_term
   11.66          (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
   11.67                        fast_descrs, evals, def_table, nondef_table, user_nondefs,
   11.68 @@ -1169,10 +1186,9 @@
   11.69                       |> user_axioms = SOME true
   11.70                          ? fold (add_nondef_axiom 1) mono_user_nondefs
   11.71      val defs = defs @ special_congruence_axioms hol_ctxt xs
   11.72 -  in
   11.73 -    ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
   11.74 -                       null poly_user_nondefs))
   11.75 -  end
   11.76 +    val got_all_mono_user_axioms =
   11.77 +      (user_axioms = SOME true orelse null mono_user_nondefs)
   11.78 +  in (t :: nondefs, defs, got_all_mono_user_axioms, null poly_user_nondefs) end
   11.79  
   11.80  (** Simplification of constructor/selector terms **)
   11.81  
   11.82 @@ -1274,7 +1290,7 @@
   11.83  
   11.84  (* Maximum number of quantifiers in a cluster for which the exponential
   11.85     algorithm is used. Larger clusters use a heuristic inspired by Claessen &
   11.86 -   Sörensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
   11.87 +   Soerensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
   11.88     paper). *)
   11.89  val quantifier_cluster_threshold = 7
   11.90  
   11.91 @@ -1385,29 +1401,29 @@
   11.92  
   11.93  (** Preprocessor entry point **)
   11.94  
   11.95 -(* hol_context -> term
   11.96 -   -> ((term list * term list) * (bool * bool)) * term * bool *)
   11.97 +(* hol_context -> term -> term list * term list * bool * bool * bool *)
   11.98  fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
   11.99                                    boxes, skolemize, uncurry, ...}) t =
  11.100    let
  11.101      val skolem_depth = if skolemize then 4 else ~1
  11.102 -    val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
  11.103 -         core_t) = t |> unfold_defs_in_term hol_ctxt
  11.104 -                     |> close_form
  11.105 -                     |> skolemize_term_and_more hol_ctxt skolem_depth
  11.106 -                     |> specialize_consts_in_term hol_ctxt 0
  11.107 -                     |> `(axioms_for_term hol_ctxt)
  11.108 +    val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
  11.109 +      t |> unfold_defs_in_term hol_ctxt
  11.110 +        |> close_form
  11.111 +        |> skolemize_term_and_more hol_ctxt skolem_depth
  11.112 +        |> specialize_consts_in_term hol_ctxt 0
  11.113 +        |> axioms_for_term hol_ctxt
  11.114      val binarize =
  11.115        is_standard_datatype thy stds nat_T andalso
  11.116        case binary_ints of
  11.117          SOME false => false
  11.118 -      | _ => forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
  11.119 +      | _ => forall may_use_binary_ints (nondef_ts @ def_ts) andalso
  11.120               (binary_ints = SOME true orelse
  11.121 -              exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
  11.122 +              exists should_use_binary_ints (nondef_ts @ def_ts))
  11.123      val box = exists (not_equal (SOME false) o snd) boxes
  11.124 +    val uncurry = uncurry andalso box
  11.125      val table =
  11.126 -      Termtab.empty |> uncurry
  11.127 -        ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
  11.128 +      Termtab.empty
  11.129 +      |> uncurry ? fold (add_to_uncurry_table thy) (nondef_ts @ def_ts)
  11.130      (* bool -> term -> term *)
  11.131      fun do_rest def =
  11.132        binarize ? binarize_nat_and_int_in_term
  11.133 @@ -1424,12 +1440,10 @@
  11.134        #> push_quantifiers_inward
  11.135        #> close_form
  11.136        #> Term.map_abs_vars shortest_name
  11.137 +    val nondef_ts = map (do_rest false) nondef_ts
  11.138      val def_ts = map (do_rest true) def_ts
  11.139 -    val nondef_ts = map (do_rest false) nondef_ts
  11.140 -    val core_t = do_rest false core_t
  11.141    in
  11.142 -    (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
  11.143 -     core_t, binarize)
  11.144 +    (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize)
  11.145    end
  11.146  
  11.147  end;