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;