--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Mar 01 14:48:28 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Mar 01 14:48:32 2012 +0100
@@ -744,10 +744,11 @@
try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.AbsF) s'
= SOME (Const x) andalso not (is_codatatype ctxt abs_T)
| is_quot_abs_fun _ _ = false
-fun is_quot_rep_fun ctxt (x as (_, Type (@{type_name fun},
- [abs_T as Type (s', _), _]))) =
- try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) s'
- = SOME (Const x) andalso not (is_codatatype ctxt abs_T)
+fun is_quot_rep_fun ctxt (x as (s, Type (@{type_name fun},
+ [abs_T as Type (abs_s, _), _]))) =
+ (case try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) abs_s of
+ SOME (Const (s', _)) => s = s' andalso not (is_codatatype ctxt abs_T)
+ | NONE => false)
| is_quot_rep_fun _ _ = false
fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun},
@@ -767,7 +768,8 @@
raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
let
- val {qtyp, equiv_rel, equiv_thm, ...} = the (Quotient_Info.lookup_quotients thy s)
+ val {qtyp, equiv_rel, equiv_thm, ...} =
+ the (Quotient_Info.lookup_quotients thy s)
val partial =
case prop_of equiv_thm of
@{const Trueprop} $ (Const (@{const_name equivp}, _) $ _) => false
@@ -1785,12 +1787,14 @@
else if is_quot_type ctxt (domain_type T) then
let
val abs_T = domain_type T
- val rep_T = domain_type (range_type T)
+ val rep_T = elem_type (range_type T)
val (rep_fun, _) = quot_rep_of depth Ts abs_T rep_T []
val (equiv_rel, _) =
equiv_relation_for_quot_type ctxt abs_T
in
- (Abs (Name.uu, abs_T, equiv_rel $ (rep_fun $ Bound 0)),
+ (Abs (Name.uu, abs_T,
+ HOLogic.Collect_const rep_T
+ $ (equiv_rel $ (rep_fun $ Bound 0))),
ts)
end
else
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Mar 01 14:48:28 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Mar 01 14:48:32 2012 +0100
@@ -1060,7 +1060,7 @@
| Op1 (Finite, _, Opt (Atom _), _) => KK.None
| Op1 (Converse, T, R, u1) =>
let
- val (b_T, a_T) = HOLogic.dest_prodT (elem_type T)
+ val (b_T, a_T) = HOLogic.dest_prodT (pseudo_domain_type T)
val (b_R, a_R) =
case R of
Func (Struct [R1, R2], _) => (R1, R2)
@@ -1191,8 +1191,8 @@
end
| Op2 (Composition, _, R, u1, u2) =>
let
- val (a_T, b_T) = HOLogic.dest_prodT (elem_type (type_of u1))
- val (_, c_T) = HOLogic.dest_prodT (elem_type (type_of u2))
+ val (a_T, b_T) = HOLogic.dest_prodT (pseudo_domain_type (type_of u1))
+ val (_, c_T) = HOLogic.dest_prodT (pseudo_domain_type (type_of u2))
val ab_k = card_of_domain_from_rep 2 (rep_of u1)
val bc_k = card_of_domain_from_rep 2 (rep_of u2)
val ac_k = card_of_domain_from_rep 2 R
--- a/src/HOL/Tools/SMT/smt_solver.ML Thu Mar 01 14:48:28 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Thu Mar 01 14:48:32 2012 +0100
@@ -65,7 +65,9 @@
fun run ctxt name mk_cmd input =
(case SMT_Config.certificates_of ctxt of
NONE =>
- if Config.get ctxt SMT_Config.debug_files = "" then
+ if not (SMT_Config.is_available ctxt name) then
+ error ("The SMT solver " ^ quote name ^ " is not installed.")
+ else if Config.get ctxt SMT_Config.debug_files = "" then
trace_and ctxt ("Invoking SMT solver " ^ quote name ^ " ...")
(Cache_IO.run mk_cmd) input
else
@@ -237,13 +239,10 @@
fun gen_apply (ithms, ctxt) =
let val (name, {command, reconstruct, ...}) = name_and_info_of ctxt
in
- if not (SMT_Config.is_available ctxt name) then
- error ("The SMT solver " ^ quote name ^ " is not installed.")
- else
- (ithms, ctxt)
- |-> invoke name command
- |> reconstruct ctxt
- |>> distinct (op =)
+ (ithms, ctxt)
+ |-> invoke name command
+ |> reconstruct ctxt
+ |>> distinct (op =)
end
fun apply_solver ctxt = gen_apply o gen_preprocess ctxt