--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Fri Sep 08 00:02:21 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Fri Sep 08 00:02:22 2017 +0200
@@ -263,13 +263,13 @@
|> @{apply 3(2)} (map ((fn Type (s, _) => Type (s, Ts))))
|> @{apply 3(3)} (map (map (Ctr_Sugar.mk_ctr Ts)));
-fun typedef_of ctxt whacks T_name =
+fun typedef_of ctxt T_name =
if T_name = @{type_name set} then
let
val A = Logic.varifyT_global @{typ 'a};
val absT = Type (@{type_name set}, [A]);
val repT = A --> HOLogic.boolT;
- val pred = K (Abs (Name.uu, repT, @{const True}));
+ val pred = Abs (Name.uu, repT, @{const True});
val abs = Const (@{const_name Collect}, repT --> absT);
val rep = Const (@{const_name rmember}, absT --> repT);
in
@@ -284,25 +284,21 @@
let
val absT = Logic.varifyT_global abs_type;
val repT = Logic.varifyT_global rep_type;
- val set0 = Thm.prop_of Rep
+ val set = Thm.prop_of Rep
|> HOLogic.dest_Trueprop
|> HOLogic.dest_mem
|> snd;
- val pred0 = Abs (Name.uu, repT, HOLogic.mk_mem (Bound 0, set0));
- fun pred () = preprocess_prop false ctxt whacks pred0;
+ val pred = Abs (Name.uu, repT, HOLogic.mk_mem (Bound 0, set));
val abs = Const (Abs_name, repT --> absT);
val rep = Const (Rep_name, absT --> repT);
in
(absT, repT, pred, abs, rep)
end);
-fun quotient_of ctxt whacks T_name =
+fun quotient_of ctxt T_name =
(case Quotient_Info.lookup_quotients ctxt T_name of
- SOME {equiv_rel = equiv_rel0, qtyp, rtyp, quot_thm, ...} =>
- let
- val _ $ (_ $ _ $ abs $ rep) = Thm.prop_of quot_thm;
- fun equiv_rel () = preprocess_prop false ctxt whacks equiv_rel0;
- in
+ SOME {equiv_rel, qtyp, rtyp, quot_thm, ...} =>
+ let val _ $ (_ $ _ $ abs $ rep) = Thm.prop_of quot_thm in
(qtyp, rtyp, equiv_rel, abs, rep)
end);
@@ -354,64 +350,60 @@
val is_co_datatype_case = can o dest_co_datatype_case;
-fun is_quotient_abs ctxt whacks (s, T) =
+fun is_quotient_abs ctxt (s, T) =
(case T of
Type (@{type_name fun}, [_, Type (absT_name, _)]) =>
classify_type_name ctxt absT_name = Quotient andalso
- (case quotient_of ctxt whacks absT_name of
+ (case quotient_of ctxt absT_name of
(_, _, _, Const (s', _), _) => s' = s)
| _ => false);
-fun is_quotient_rep ctxt whacks (s, T) =
+fun is_quotient_rep ctxt (s, T) =
(case T of
Type (@{type_name fun}, [Type (absT_name, _), _]) =>
classify_type_name ctxt absT_name = Quotient andalso
- (case quotient_of ctxt whacks absT_name of
+ (case quotient_of ctxt absT_name of
(_, _, _, _, Const (s', _)) => s' = s)
| _ => false);
-fun is_maybe_typedef_abs ctxt whacks absT_name s =
+fun is_maybe_typedef_abs ctxt absT_name s =
if absT_name = @{type_name set} then
s = @{const_name Collect}
else
- (case try (typedef_of ctxt whacks) absT_name of
+ (case try (typedef_of ctxt) absT_name of
SOME (_, _, _, Const (s', _), _) => s' = s
| NONE => false);
-fun is_maybe_typedef_rep ctxt whacks absT_name s =
+fun is_maybe_typedef_rep ctxt absT_name s =
if absT_name = @{type_name set} then
s = @{const_name rmember}
else
- (case try (typedef_of ctxt whacks) absT_name of
+ (case try (typedef_of ctxt) absT_name of
SOME (_, _, _, _, Const (s', _)) => s' = s
| NONE => false);
-fun is_typedef_abs ctxt whacks (s, T) =
+fun is_typedef_abs ctxt (s, T) =
(case T of
Type (@{type_name fun}, [_, Type (absT_name, _)]) =>
- classify_type_name ctxt absT_name = Typedef andalso
- is_maybe_typedef_abs ctxt whacks absT_name s
+ classify_type_name ctxt absT_name = Typedef andalso is_maybe_typedef_abs ctxt absT_name s
| _ => false);
-fun is_typedef_rep ctxt whacks (s, T) =
+fun is_typedef_rep ctxt (s, T) =
(case T of
Type (@{type_name fun}, [Type (absT_name, _), _]) =>
- classify_type_name ctxt absT_name = Typedef andalso
- is_maybe_typedef_rep ctxt whacks absT_name s
+ classify_type_name ctxt absT_name = Typedef andalso is_maybe_typedef_rep ctxt absT_name s
| _ => false);
-fun is_stale_typedef_abs ctxt whacks (s, T) =
+fun is_stale_typedef_abs ctxt (s, T) =
(case T of
Type (@{type_name fun}, [_, Type (absT_name, _)]) =>
- classify_type_name ctxt absT_name <> Typedef andalso
- is_maybe_typedef_abs ctxt whacks absT_name s
+ classify_type_name ctxt absT_name <> Typedef andalso is_maybe_typedef_abs ctxt absT_name s
| _ => false);
-fun is_stale_typedef_rep ctxt whacks (s, T) =
+fun is_stale_typedef_rep ctxt (s, T) =
(case T of
Type (@{type_name fun}, [Type (absT_name, _), _]) =>
- classify_type_name ctxt absT_name <> Typedef andalso
- is_maybe_typedef_rep ctxt whacks absT_name s
+ classify_type_name ctxt absT_name <> Typedef andalso is_maybe_typedef_rep ctxt absT_name s
| _ => false);
fun instantiate_constant_types_in_term ctxt csts target =
@@ -887,12 +879,12 @@
fun consider_typedef_or_quotient itypedef_or_quotient tuple_of s =
let
- val (T0, repT0, wrt0, abs0, rep0) = tuple_of ctxt whacks s;
+ val (T0, repT0, wrt0, abs0, rep0) = tuple_of ctxt s;
val tyenv = Sign.typ_match thy (T0, T) Vartab.empty;
val substT = Envir.subst_type tyenv;
val subst = Envir.subst_term_types tyenv;
val repT = substT repT0;
- val wrt = subst (wrt0 ());
+ val wrt = preprocess_prop false ctxt whacks (subst wrt0);
val abs = subst abs0;
val rep = subst rep0;
in
@@ -944,12 +936,11 @@
(case t of
Const (x as (s, T)) =>
(if is_const_builtin s orelse is_co_datatype_ctr ctxt x orelse
- is_co_datatype_case ctxt x orelse is_quotient_abs ctxt whacks x orelse
- is_quotient_rep ctxt whacks x orelse is_typedef_abs ctxt whacks x orelse
- is_typedef_rep ctxt whacks x then
+ is_co_datatype_case ctxt x orelse is_quotient_abs ctxt x orelse
+ is_quotient_rep ctxt x orelse is_typedef_abs ctxt x orelse
+ is_typedef_rep ctxt x then
(seens, problem)
- else if is_stale_typedef_abs ctxt whacks x orelse
- is_stale_typedef_rep ctxt whacks x then
+ else if is_stale_typedef_abs ctxt x orelse is_stale_typedef_rep ctxt x then
raise UNSUPPORTED_FUNC t
else
(case spec_rules_of ctxt x of