| author | haftmann |
| Thu, 18 Mar 2010 13:57:00 +0100 | |
| changeset 35824 | b766aad9136d |
| parent 35815 | 10e723e54076 (diff) |
| parent 35823 | bd26885af9f4 (current diff) |
| child 35831 | e31ec41a551b |
--- a/NEWS Thu Mar 18 13:56:34 2010 +0100 +++ b/NEWS Thu Mar 18 13:57:00 2010 +0100 @@ -221,6 +221,40 @@ * Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL. +* Library/Nat_Bijection.thy is a collection of bijective functions +between nat and other types, which supersedes the older libraries +Library/Nat_Int_Bij.thy and HOLCF/NatIso.thy. INCOMPATIBILITY. + + Constants: + Nat_Int_Bij.nat2_to_nat ~> prod_encode + Nat_Int_Bij.nat_to_nat2 ~> prod_decode + Nat_Int_Bij.int_to_nat_bij ~> int_encode + Nat_Int_Bij.nat_to_int_bij ~> int_decode + Countable.pair_encode ~> prod_encode + NatIso.prod2nat ~> prod_encode + NatIso.nat2prod ~> prod_decode + NatIso.sum2nat ~> sum_encode + NatIso.nat2sum ~> sum_decode + NatIso.list2nat ~> list_encode + NatIso.nat2list ~> list_decode + NatIso.set2nat ~> set_encode + NatIso.nat2set ~> set_decode + + Lemmas: + Nat_Int_Bij.bij_nat_to_int_bij ~> bij_int_decode + Nat_Int_Bij.nat2_to_nat_inj ~> inj_prod_encode + Nat_Int_Bij.nat2_to_nat_surj ~> surj_prod_encode + Nat_Int_Bij.nat_to_nat2_inj ~> inj_prod_decode + Nat_Int_Bij.nat_to_nat2_surj ~> surj_prod_decode + Nat_Int_Bij.i2n_n2i_id ~> int_encode_inverse + Nat_Int_Bij.n2i_i2n_id ~> int_decode_inverse + Nat_Int_Bij.surj_nat_to_int_bij ~> surj_int_encode + Nat_Int_Bij.surj_int_to_nat_bij ~> surj_int_decode + Nat_Int_Bij.inj_nat_to_int_bij ~> inj_int_encode + Nat_Int_Bij.inj_int_to_nat_bij ~> inj_int_decode + Nat_Int_Bij.bij_nat_to_int_bij ~> bij_int_encode + Nat_Int_Bij.bij_int_to_nat_bij ~> bij_int_decode + *** ML ***
--- a/doc-src/Nitpick/nitpick.tex Thu Mar 18 13:56:34 2010 +0100 +++ b/doc-src/Nitpick/nitpick.tex Thu Mar 18 13:57:00 2010 +0100 @@ -2617,6 +2617,12 @@ where the $P_i$'s are side conditions that do not involve $c$ and $M$ is an optional monotonic operator. The order of the assumptions is irrelevant. +\flushitem{\textit{nitpick\_choice\_spec}} + +\nopagebreak +This attribute specifies the (free-form) specification of a constant defined +using the \hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command. + \end{itemize} When faced with a constant, Nitpick proceeds as follows: @@ -2629,7 +2635,12 @@ the constant is not empty, it uses these rules as the specification of the constant. -\item[3.] Otherwise, it looks up the definition of the constant: +\item[3.] Otherwise, if the constant was defined using the +\hbox{(\textbf{ax\_})}\allowbreak\textbf{specification} command and the +\textit{nitpick\_choice\_spec} set associated with the constant is not empty, it +uses these theorems as the specification of the constant. + +\item[4.] Otherwise, it looks up the definition of the constant: \begin{enum} \item[1.] If the \textit{nitpick\_def} set associated with the constant @@ -2815,6 +2826,9 @@ representation of functions synthesized by Isabelle, which is an implementation detail. +\item[$\bullet$] Axioms that restrict the possible values of the +\textit{undefined} constant are in general ignored. + \item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions, which can become invalid if you change the definition of an inductive predicate that is registered in the cache. To clear the cache,
--- a/src/HOL/Divides.thy Thu Mar 18 13:56:34 2010 +0100 +++ b/src/HOL/Divides.thy Thu Mar 18 13:57:00 2010 +0100 @@ -588,8 +588,16 @@ from divmod_nat_rel have divmod_nat_m_n: "divmod_nat_rel m n (m div n, m mod n)" . with assms have m_div_n: "m div n \<ge> 1" by (cases "m div n") (auto simp add: divmod_nat_rel_def) - from assms divmod_nat_m_n have "divmod_nat_rel (m - n) n (m div n - Suc 0, m mod n)" - by (cases "m div n") (auto simp add: divmod_nat_rel_def) + have "divmod_nat_rel (m - n) n (m div n - Suc 0, m mod n)" + proof - + from assms have + "n \<noteq> 0" + "\<And>k. m = Suc k * n + m mod n ==> m - n = (Suc k - Suc 0) * n + m mod n" + by simp_all + then show ?thesis using assms divmod_nat_m_n + by (cases "m div n") + (simp_all only: divmod_nat_rel_def fst_conv snd_conv, simp_all) + qed with divmod_nat_eq have "divmod_nat (m - n) n = (m div n - Suc 0, m mod n)" by simp moreover from divmod_nat_div_mod have "divmod_nat (m - n) n = ((m - n) div n, (m - n) mod n)" . ultimately have "m div n = Suc ((m - n) div n)" @@ -1122,7 +1130,7 @@ lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1" proof - - { fix n :: nat have "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (induct n) simp_all } + { fix n :: nat have "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all } moreover have "m mod 2 < 2" by simp ultimately have "m mod 2 = 0 \<or> m mod 2 = 1" . then show ?thesis by auto @@ -1166,8 +1174,11 @@ lemma Suc_n_div_2_gt_zero [simp]: "(0::nat) < n ==> 0 < (n + 1) div 2" by (cases n) simp_all -lemma div_2_gt_zero [simp]: "(1::nat) < n ==> 0 < n div 2" -using Suc_n_div_2_gt_zero [of "n - 1"] by simp +lemma div_2_gt_zero [simp]: assumes A: "(1::nat) < n" shows "0 < n div 2" +proof - + from A have B: "0 < n - 1" and C: "n - 1 + 1 = n" by simp_all + from Suc_n_div_2_gt_zero [OF B] C show ?thesis by simp +qed (* Potential use of algebra : Equality modulo n*) lemma mod_mult_self3 [simp]: "(k*n + m) mod n = m mod (n::nat)" @@ -2092,15 +2103,16 @@ div_pos_pos_trivial) qed -lemma neg_zdiv_mult_2: "a \<le> (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a" -apply (subgoal_tac " (1 + 2* (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a) ") -apply (rule_tac [2] pos_zdiv_mult_2) -apply (auto simp add: right_diff_distrib) -apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))") -apply (simp only: zdiv_zminus_zminus diff_minus minus_add_distrib [symmetric]) -apply (simp_all add: algebra_simps) -apply (simp only: ab_diff_minus minus_add_distrib [symmetric] number_of_Min zdiv_zminus_zminus) -done +lemma neg_zdiv_mult_2: + assumes A: "a \<le> (0::int)" shows "(1 + 2*b) div (2*a) = (b+1) div a" +proof - + have R: "1 + - (2 * (b + 1)) = - (1 + 2 * b)" by simp + have "(1 + 2 * (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a)" + by (rule pos_zdiv_mult_2, simp add: A) + thus ?thesis + by (simp only: R zdiv_zminus_zminus diff_minus + minus_add_distrib [symmetric] mult_minus_right) +qed lemma zdiv_number_of_Bit0 [simp]: "number_of (Int.Bit0 v) div number_of (Int.Bit0 w) =
--- a/src/HOL/HOL.thy Thu Mar 18 13:56:34 2010 +0100 +++ b/src/HOL/HOL.thy Thu Mar 18 13:57:00 2010 +0100 @@ -2022,7 +2022,7 @@ ) structure Nitpick_Choice_Specs = Named_Thms ( - val name = "nitpick_choice_specs" + val name = "nitpick_choice_spec" val description = "choice specification of constants as needed by Nitpick" ) *}
--- a/src/HOL/Int.thy Thu Mar 18 13:56:34 2010 +0100 +++ b/src/HOL/Int.thy Thu Mar 18 13:57:00 2010 +0100 @@ -1829,11 +1829,12 @@ lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1" by (insert abs_zmult_eq_1 [of m n], arith) -lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)" -apply (auto dest: pos_zmult_eq_1_iff_lemma) -apply (simp add: mult_commute [of m]) -apply (frule pos_zmult_eq_1_iff_lemma, auto) -done +lemma pos_zmult_eq_1_iff: + assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)" +proof - + from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma) + thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma) +qed lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))" apply (rule iffI)
--- a/src/HOL/Nat_Numeral.thy Thu Mar 18 13:56:34 2010 +0100 +++ b/src/HOL/Nat_Numeral.thy Thu Mar 18 13:57:00 2010 +0100 @@ -643,8 +643,9 @@ fixes z :: "'a::number_ring" shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w then (let w = z ^ (number_of w) in z * w * w) else 1)" -apply (auto simp add: Let_def Bit1_def nat_number_of_def number_of_is_id - mult_assoc nat_add_distrib power_add not_le simp del: nat_number_of) +unfolding Let_def Bit1_def nat_number_of_def number_of_is_id +apply (cases "0 <= w") +apply (simp only: mult_assoc nat_add_distrib power_add, simp) apply (simp add: not_le mult_2 [symmetric] add_assoc) done @@ -673,9 +674,10 @@ "number_of (Int.Bit1 w) = (if neg (number_of w :: int) then 0 else let n = number_of w in Suc (n + n))" -apply (auto simp add: Let_def Bit1_def nat_number_of_def number_of_is_id neg_def - nat_add_distrib simp del: nat_number_of) +unfolding Let_def Bit1_def nat_number_of_def number_of_is_id neg_def +apply (cases "w < 0") apply (simp add: mult_2 [symmetric] add_assoc) +apply (simp only: nat_add_distrib, simp) done lemmas nat_number =
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Mar 18 13:56:34 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Mar 18 13:57:00 2010 +0100 @@ -31,7 +31,8 @@ unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []} (* term -> bool *) -fun is_mono t = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} ([t], []) +fun is_mono t = + Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} ([t], []) fun is_const t = let val T = fastype_of t in is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
--- a/src/HOL/Tools/Nitpick/HISTORY Thu Mar 18 13:56:34 2010 +0100 +++ b/src/HOL/Tools/Nitpick/HISTORY Thu Mar 18 13:57:00 2010 +0100 @@ -14,6 +14,7 @@ * Fixed soundness bugs related to "destroy_constrs" optimization and record getters * Fixed soundness bug related to higher-order constructors + * Added cache to speed up repeated Kodkod invocations on the same problems * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
--- a/src/HOL/Tools/Nitpick/kodkod.ML Thu Mar 18 13:56:34 2010 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Mar 18 13:57:00 2010 +0100 @@ -169,7 +169,7 @@ val max_arity : int -> int val arity_of_rel_expr : rel_expr -> int val is_problem_trivially_false : problem -> bool - val problems_equivalent : problem -> problem -> bool + val problems_equivalent : problem * problem -> bool val solve_any_problem : bool -> Time.time option -> int -> int -> problem list -> outcome end; @@ -500,19 +500,28 @@ fun is_problem_trivially_false ({formula = False, ...} : problem) = true | is_problem_trivially_false _ = false -(* string -> bool *) -val is_relevant_setting = not o member (op =) ["solver", "delay"] +(* string -> string list *) +val chop_solver = take 2 o space_explode "," -(* problem -> problem -> bool *) -fun problems_equivalent (p1 : problem) (p2 : problem) = +(* setting list * setting list -> bool *) +fun settings_equivalent ([], []) = true + | settings_equivalent ((key1, value1) :: settings1, + (key2, value2) :: settings2) = + key1 = key2 andalso + (value1 = value2 orelse key1 = "delay" orelse + (key1 = "solver" andalso chop_solver value1 = chop_solver value2)) andalso + settings_equivalent (settings1, settings2) + | settings_equivalent _ = false + +(* problem * problem -> bool *) +fun problems_equivalent (p1 : problem, p2 : problem) = #univ_card p1 = #univ_card p2 andalso #formula p1 = #formula p2 andalso #bounds p1 = #bounds p2 andalso #expr_assigns p1 = #expr_assigns p2 andalso #tuple_assigns p1 = #tuple_assigns p2 andalso #int_bounds p1 = #int_bounds p2 andalso - filter (is_relevant_setting o fst) (#settings p1) - = filter (is_relevant_setting o fst) (#settings p2) + settings_equivalent (#settings p1, #settings p2) (** Serialization of problem **) @@ -1005,10 +1014,6 @@ |>> rev ||> rev) handle IO.Io _ => (true, ([], [])) | OS.SysErr _ => (true, ([], [])) -(* The fudge term below is to account for Kodkodi's slow start-up time, which - is partly due to the JVM and partly due to the ML "bash" function. *) -val fudge_ms = 250 - (** Main Kodkod entry point **) val created_temp_dir = Unsynchronized.ref false @@ -1024,8 +1029,20 @@ else (created_temp_dir := true; File.mkdir (Path.explode dir)) in (serial_string (), dir) end +(* The fudge term below is to account for Kodkodi's slow start-up time, which + is partly due to the JVM and partly due to the ML "bash" function. *) +val fudge_ms = 250 + +(* Time.time option -> int *) +fun milliseconds_until_deadline deadline = + case deadline of + NONE => ~1 + | SOME time => + Int.max (0, Time.toMilliseconds (Time.- (time, Time.now ())) - fudge_ms) + (* bool -> Time.time option -> int -> int -> problem list -> outcome *) -fun solve_any_problem overlord deadline max_threads max_solutions problems = +fun uncached_solve_any_problem overlord deadline max_threads max_solutions + problems = let val j = find_index (curry (op =) True o #formula) problems val indexed_problems = if j >= 0 then @@ -1061,12 +1078,7 @@ else List.app (K () o try File.rm) [in_path, out_path, err_path] in let - val ms = - case deadline of - NONE => ~1 - | SOME time => - Int.max (0, Time.toMilliseconds (Time.- (time, Time.now ())) - - fudge_ms) + val ms = milliseconds_until_deadline deadline val outcome = let val code = @@ -1135,4 +1147,35 @@ end end +val cached_outcome = + Synchronized.var "Kodkod.cached_outcome" + (NONE : ((int * problem list) * outcome) option) + +(* bool -> Time.time option -> int -> int -> problem list -> outcome *) +fun solve_any_problem overlord deadline max_threads max_solutions problems = + let + (* unit -> outcome *) + fun do_solve () = uncached_solve_any_problem overlord deadline max_threads + max_solutions problems + in + if overlord then + do_solve () + else + case AList.lookup (fn ((max1, ps1), (max2, ps2)) => + max1 = max2 andalso length ps1 = length ps2 andalso + forall problems_equivalent (ps1 ~~ ps2)) + (the_list (Synchronized.value cached_outcome)) + (max_solutions, problems) of + SOME outcome => outcome + | NONE => + let val outcome = do_solve () in + (case outcome of + Normal (ps, js, "") => + Synchronized.change cached_outcome + (K (SOME ((max_solutions, problems), outcome))) + | _ => ()); + outcome + end + end + end;
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 18 13:56:34 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 18 13:57:00 2010 +0100 @@ -777,8 +777,8 @@ |> filter (fn j => j >= 0 andalso scopes_equivalent - (#scope (snd (nth problems j))) - (#scope (snd (nth problems (j + 1))))) + (#scope (snd (nth problems j)), + #scope (snd (nth problems (j + 1))))) val bye_js = sort_distinct int_ord (map fst sat_ps @ unsat_js @ co_js) val problems = @@ -862,8 +862,7 @@ SOME problem => (problems |> (null problems orelse - not (KK.problems_equivalent (fst problem) - (fst (hd problems)))) + not (KK.problems_equivalent (fst problem, fst (hd problems)))) ? cons problem, donno) | NONE => (problems, donno + 1)) val (problems, donno) = @@ -904,7 +903,7 @@ (* rich_problem list -> scope -> int *) fun scope_count (problems : rich_problem list) scope = - length (filter (scopes_equivalent scope o #scope o snd) problems) + length (filter (curry scopes_equivalent scope o #scope o snd) problems) (* string -> string *) fun excipit did_so_and_so = let
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Mar 18 13:56:34 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Mar 18 13:57:00 2010 +0100 @@ -50,6 +50,7 @@ datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref, constr_mcache: (styp * mtyp) list Unsynchronized.ref} +exception UNSOLVABLE of unit exception MTYPE of string * mtyp list * typ list exception MTERM of string * mterm list @@ -381,9 +382,7 @@ type comp = sign_atom * sign_atom * comp_op * var list type sign_expr = literal list -datatype constraint_set = - UnsolvableCSet | - CSet of literal list * comp list * sign_expr list +type constraint_set = literal list * comp list * sign_expr list (* comp_op -> string *) fun string_for_comp_op Eq = "=" @@ -394,9 +393,6 @@ | string_for_sign_expr lits = space_implode " \<or> " (map string_for_literal lits) -(* constraint_set *) -val slack = CSet ([], [], []) - (* literal -> literal list option -> literal list option *) fun do_literal _ NONE = NONE | do_literal (x, sn) (SOME lits) = @@ -455,13 +451,12 @@ [M1, M2], []) (* comp_op -> mtyp -> mtyp -> constraint_set -> constraint_set *) -fun add_mtype_comp _ _ _ UnsolvableCSet = UnsolvableCSet - | add_mtype_comp cmp M1 M2 (CSet (lits, comps, sexps)) = +fun add_mtype_comp cmp M1 M2 (lits, comps, sexps) = (print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^ " " ^ string_for_mtype M2); case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of - NONE => (print_g "**** Unsolvable"; UnsolvableCSet) - | SOME (lits, comps) => CSet (lits, comps, sexps)) + NONE => (print_g "**** Unsolvable"; raise UNSOLVABLE ()) + | SOME (lits, comps) => (lits, comps, sexps)) (* mtyp -> mtyp -> constraint_set -> constraint_set *) val add_mtypes_equal = add_mtype_comp Eq @@ -505,13 +500,12 @@ raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], []) (* sign -> mtyp -> constraint_set -> constraint_set *) -fun add_notin_mtype_fv _ _ UnsolvableCSet = UnsolvableCSet - | add_notin_mtype_fv sn M (CSet (lits, comps, sexps)) = +fun add_notin_mtype_fv sn M (lits, comps, sexps) = (print_g ("*** Add " ^ string_for_mtype M ^ " is " ^ (case sn of Minus => "concrete" | Plus => "complete") ^ "."); case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of - NONE => (print_g "**** Unsolvable"; UnsolvableCSet) - | SOME (lits, sexps) => CSet (lits, comps, sexps)) + NONE => (print_g "**** Unsolvable"; raise UNSOLVABLE ()) + | SOME (lits, sexps) => (lits, comps, sexps)) (* mtyp -> constraint_set -> constraint_set *) val add_mtype_is_concrete = add_notin_mtype_fv Minus @@ -576,8 +570,7 @@ end (* var -> constraint_set -> literal list option *) -fun solve _ UnsolvableCSet = (print_g "*** Problem: Unsolvable"; NONE) - | solve max_var (CSet (lits, comps, sexps)) = +fun solve max_var (lits, comps, sexps) = let (* (int -> bool option) -> literal list option *) fun do_assigns assigns = @@ -613,7 +606,6 @@ type accumulator = mtype_context * constraint_set val initial_gamma = {bound_Ts = [], bound_Ms = [], frees = [], consts = []} -val unsolvable_accum = (initial_gamma, UnsolvableCSet) (* typ -> mtyp -> mtype_context -> mtype_context *) fun push_bound T M {bound_Ts, bound_Ms, frees, consts} = @@ -684,10 +676,6 @@ M as MPair (a_M, b_M) => pair (MFun (M, S Minus, if n = 0 then a_M else b_M)) | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], []) - (* mtyp * accumulator *) - val mtype_unsolvable = (dummy_M, unsolvable_accum) - (* term -> mterm * accumulator *) - fun mterm_unsolvable t = (MRaw (t, dummy_M), unsolvable_accum) (* term -> string -> typ -> term -> term -> term -> accumulator -> mterm * accumulator *) fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum = @@ -710,8 +698,7 @@ body_m))), accum) end (* term -> accumulator -> mterm * accumulator *) - and do_term t (_, UnsolvableCSet) = mterm_unsolvable t - | do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts}, + and do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts}, cset)) = (case t of Const (x as (s, T)) => @@ -734,8 +721,8 @@ |>> mtype_of_mterm end | @{const_name "op ="} => do_equals T accum - | @{const_name The} => (print_g "*** The"; mtype_unsolvable) - | @{const_name Eps} => (print_g "*** Eps"; mtype_unsolvable) + | @{const_name The} => (print_g "*** The"; raise UNSOLVABLE ()) + | @{const_name Eps} => (print_g "*** Eps"; raise UNSOLVABLE ()) | @{const_name If} => do_robust_set_operation (range_type T) accum |>> curry3 MFun bool_M (S Minus) @@ -855,7 +842,7 @@ (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms, frees = (x, M) :: frees, consts = consts}, cset)) end) |>> curry MRaw t - | Var _ => (print_g "*** Var"; mterm_unsolvable t) + | Var _ => (print_g "*** Var"; raise UNSOLVABLE ()) | Bound j => (MRaw (t, nth bound_Ms j), accum) | Abs (s, T, t') => (case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of @@ -893,27 +880,17 @@ val (m1, accum) = do_term t1 accum val (m2, accum) = do_term t2 accum in - case accum of - (_, UnsolvableCSet) => mterm_unsolvable t - | _ => - let - val T11 = domain_type (fastype_of1 (bound_Ts, t1)) - val T2 = fastype_of1 (bound_Ts, t2) - val M11 = mtype_of_mterm m1 |> dest_MFun |> #1 - val M2 = mtype_of_mterm m2 - in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end + let + val T11 = domain_type (fastype_of1 (bound_Ts, t1)) + val T2 = fastype_of1 (bound_Ts, t2) + val M11 = mtype_of_mterm m1 |> dest_MFun |> #1 + val M2 = mtype_of_mterm m2 + in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end end) |> tap (fn (m, _) => print_g (" \<Gamma> \<turnstile> " ^ string_for_mterm ctxt m)) in do_term end -(* - accum |> (case a of - S Minus => accum - | S Plus => unsolvable_accum - | V x => do_literal (x, Minus) lits) -*) - (* int -> mtyp -> accumulator -> accumulator *) fun force_minus_funs 0 _ = I | force_minus_funs n (M as MFun (M1, _, M2)) = @@ -949,9 +926,7 @@ (* term -> accumulator -> mterm * accumulator *) val do_term = consider_term mdata (* sign -> term -> accumulator -> mterm * accumulator *) - fun do_formula _ t (_, UnsolvableCSet) = - (MRaw (t, dummy_M), unsolvable_accum) - | do_formula sn t accum = + fun do_formula sn t accum = let (* styp -> string -> typ -> term -> mterm * accumulator *) fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t = @@ -1084,9 +1059,7 @@ (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum) end (* term -> accumulator -> accumulator *) - and do_formula t (_, UnsolvableCSet) = - (MRaw (t, dummy_M), unsolvable_accum) - | do_formula t accum = + and do_formula t accum = case t of (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) => do_all t0 s1 T1 t1 accum @@ -1134,7 +1107,7 @@ Syntax.string_of_typ ctxt alpha_T) val mdata as {max_fresh, constr_mcache, ...} = initial_mdata hol_ctxt binarize no_harmless alpha_T - val accum = (initial_gamma, slack) + val accum = (initial_gamma, ([], [], [])) val (nondef_ms, accum) = ([], accum) |> amass (consider_general_formula mdata Plus) (hd nondef_ts) |> fold (amass (consider_nondefinitional_axiom mdata)) @@ -1147,7 +1120,8 @@ SOME (lits, (nondef_ms, def_ms), !constr_mcache)) | _ => NONE end - handle MTYPE (loc, Ms, Ts) => + handle UNSOLVABLE () => NONE + | MTYPE (loc, Ms, Ts) => raise BAD (loc, commas (map string_for_mtype Ms @ map (Syntax.string_of_typ ctxt) Ts)) | MTERM (loc, ms) => @@ -1166,108 +1140,112 @@ binarize finitizes alpha_T tsp = case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of SOME (lits, msp, constr_mtypes) => - let - (* typ -> sign_atom -> bool *) - fun should_finitize T a = - case triple_lookup (type_match thy) finitizes T of - SOME (SOME false) => false - | _ => resolve_sign_atom lits a = S Plus - (* typ -> mtyp -> typ *) - fun type_from_mtype T M = - case (M, T) of - (MAlpha, _) => T - | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) => - Type (if should_finitize T a then @{type_name fin_fun} - else @{type_name fun}, map2 type_from_mtype Ts [M1, M2]) - | (MPair (M1, M2), Type (@{type_name "*"}, Ts)) => - Type (@{type_name "*"}, map2 type_from_mtype Ts [M1, M2]) - | (MType _, _) => T - | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype", - [M], [T]) - (* styp -> styp *) - fun finitize_constr (x as (s, T)) = - (s, case AList.lookup (op =) constr_mtypes x of - SOME M => type_from_mtype T M - | NONE => T) - (* typ list -> mterm -> term *) - fun term_from_mterm Ts m = - case m of - MRaw (t, M) => - let - val T = fastype_of1 (Ts, t) - val T' = type_from_mtype T M - in - case t of - Const (x as (s, _)) => - if s = @{const_name insert} then - case nth_range_type 2 T' of - set_T' as Type (@{type_name fin_fun}, [elem_T', _]) => - Abs (Name.uu, elem_T', Abs (Name.uu, set_T', - Const (@{const_name If}, - bool_T --> set_T' --> set_T' --> set_T') - $ (Const (@{const_name is_unknown}, elem_T' --> bool_T) - $ Bound 1) - $ (Const (@{const_name unknown}, set_T')) - $ (coerce_term hol_ctxt Ts T' T (Const x) - $ Bound 1 $ Bound 0))) - | _ => Const (s, T') - else if s = @{const_name finite} then - case domain_type T' of - set_T' as Type (@{type_name fin_fun}, _) => - Abs (Name.uu, set_T', @{const True}) - | _ => Const (s, T') - else if s = @{const_name "=="} orelse - s = @{const_name "op ="} then - Const (s, T') - else if is_built_in_const thy stds fast_descrs x then - coerce_term hol_ctxt Ts T' T t - else if is_constr thy stds x then - Const (finitize_constr x) - else if is_sel s then - let - val n = sel_no_from_name s - val x' = x |> binarized_and_boxed_constr_for_sel hol_ctxt - binarize - |> finitize_constr - val x'' = binarized_and_boxed_nth_sel_for_constr hol_ctxt - binarize x' n - in Const x'' end - else - Const (s, T') - | Free (s, T) => Free (s, type_from_mtype T M) - | Bound _ => t - | _ => raise MTERM ("Nitpick_Mono.finitize_funs.term_from_mterm", - [m]) - end - | MApp (m1, m2) => - let - val (t1, t2) = pairself (term_from_mterm Ts) (m1, m2) - val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2) - val (t1', T2') = - case T1 of - Type (s, [T11, T12]) => - (if s = @{type_name fin_fun} then - select_nth_constr_arg thy stds (fin_fun_constr T11 T12) t1 0 - (T11 --> T12) - else - t1, T11) - | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm", - [T1], []) - in betapply (t1', coerce_term hol_ctxt Ts T2' T2 t2) end - | MAbs (s, T, M, a, m') => - let - val T = type_from_mtype T M - val t' = term_from_mterm (T :: Ts) m' - val T' = fastype_of1 (T :: Ts, t') - in - Abs (s, T, t') - |> should_finitize (T --> T') a - ? construct_value thy stds (fin_fun_constr T T') o single - end - in - Unsynchronized.change constr_cache (map (apsnd (map finitize_constr))); - pairself (map (term_from_mterm [])) msp - end + if forall (curry (op =) Minus o snd) lits then + tsp + else + let + (* typ -> sign_atom -> bool *) + fun should_finitize T a = + case triple_lookup (type_match thy) finitizes T of + SOME (SOME false) => false + | _ => resolve_sign_atom lits a = S Plus + (* typ -> mtyp -> typ *) + fun type_from_mtype T M = + case (M, T) of + (MAlpha, _) => T + | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) => + Type (if should_finitize T a then @{type_name fin_fun} + else @{type_name fun}, map2 type_from_mtype Ts [M1, M2]) + | (MPair (M1, M2), Type (@{type_name "*"}, Ts)) => + Type (@{type_name "*"}, map2 type_from_mtype Ts [M1, M2]) + | (MType _, _) => T + | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype", + [M], [T]) + (* styp -> styp *) + fun finitize_constr (x as (s, T)) = + (s, case AList.lookup (op =) constr_mtypes x of + SOME M => type_from_mtype T M + | NONE => T) + (* typ list -> mterm -> term *) + fun term_from_mterm Ts m = + case m of + MRaw (t, M) => + let + val T = fastype_of1 (Ts, t) + val T' = type_from_mtype T M + in + case t of + Const (x as (s, _)) => + if s = @{const_name insert} then + case nth_range_type 2 T' of + set_T' as Type (@{type_name fin_fun}, [elem_T', _]) => + Abs (Name.uu, elem_T', Abs (Name.uu, set_T', + Const (@{const_name If}, + bool_T --> set_T' --> set_T' --> set_T') + $ (Const (@{const_name is_unknown}, + elem_T' --> bool_T) $ Bound 1) + $ (Const (@{const_name unknown}, set_T')) + $ (coerce_term hol_ctxt Ts T' T (Const x) + $ Bound 1 $ Bound 0))) + | _ => Const (s, T') + else if s = @{const_name finite} then + case domain_type T' of + set_T' as Type (@{type_name fin_fun}, _) => + Abs (Name.uu, set_T', @{const True}) + | _ => Const (s, T') + else if s = @{const_name "=="} orelse + s = @{const_name "op ="} then + Const (s, T') + else if is_built_in_const thy stds fast_descrs x then + coerce_term hol_ctxt Ts T' T t + else if is_constr thy stds x then + Const (finitize_constr x) + else if is_sel s then + let + val n = sel_no_from_name s + val x' = + x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize + |> finitize_constr + val x'' = + binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize + x' n + in Const x'' end + else + Const (s, T') + | Free (s, T) => Free (s, type_from_mtype T M) + | Bound _ => t + | _ => raise MTERM ("Nitpick_Mono.finitize_funs.term_from_mterm", + [m]) + end + | MApp (m1, m2) => + let + val (t1, t2) = pairself (term_from_mterm Ts) (m1, m2) + val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2) + val (t1', T2') = + case T1 of + Type (s, [T11, T12]) => + (if s = @{type_name fin_fun} then + select_nth_constr_arg thy stds (fin_fun_constr T11 T12) t1 + 0 (T11 --> T12) + else + t1, T11) + | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm", + [T1], []) + in betapply (t1', coerce_term hol_ctxt Ts T2' T2 t2) end + | MAbs (s, T, M, a, m') => + let + val T = type_from_mtype T M + val t' = term_from_mterm (T :: Ts) m' + val T' = fastype_of1 (T :: Ts, t') + in + Abs (s, T, t') + |> should_finitize (T --> T') a + ? construct_value thy stds (fin_fun_constr T T') o single + end + in + Unsynchronized.change constr_cache (map (apsnd (map finitize_constr))); + pairself (map (term_from_mterm [])) msp + end | NONE => tsp end;
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Mar 18 13:56:34 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Mar 18 13:57:00 2010 +0100 @@ -46,7 +46,7 @@ val spec_of_type : scope -> typ -> int * int val pretties_for_scope : scope -> bool -> Pretty.T list val multiline_string_for_scope : scope -> string - val scopes_equivalent : scope -> scope -> bool + val scopes_equivalent : scope * scope -> bool val scope_less_eq : scope -> scope -> bool val all_scopes : hol_context -> bool -> int -> (typ option * int list) list @@ -213,8 +213,8 @@ | lines => space_implode "\n" lines end -(* scope -> scope -> bool *) -fun scopes_equivalent (s1 : scope) (s2 : scope) = +(* scope * scope -> bool *) +fun scopes_equivalent (s1 : scope, s2 : scope) = #datatypes s1 = #datatypes s2 andalso #card_assigns s1 = #card_assigns s2 fun scope_less_eq (s1 : scope) (s2 : scope) = (s1, s2) |> pairself (map snd o #card_assigns) |> op ~~ |> forall (op <=)