--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Sep 14 13:24:18 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Sep 14 13:44:43 2010 +0200
@@ -424,7 +424,6 @@
(@{const_name unknown}, 0),
(@{const_name is_unknown}, 1),
(@{const_name safe_The}, 1),
- (@{const_name safe_Eps}, 1),
(@{const_name Frac}, 0),
(@{const_name norm_frac}, 0)]
val built_in_nat_consts =
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Sep 14 13:24:18 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Sep 14 13:44:43 2010 +0200
@@ -1039,10 +1039,6 @@
fun kk_vect_set_bool_op connective k r1 r2 =
fold1 kk_and (map2 connective (unpack_formulas k r1)
(unpack_formulas k r2))
- fun is_surely_singleton R r =
- kk_and (kk_subset (full_rel_for_rep R)
- (kk_join r (full_rel_for_rep bool_atom_R)))
- (kk_one (kk_join r true_atom))
fun to_f u =
case rep_of u of
Formula polar =>
@@ -1185,12 +1181,6 @@
else
kk_rel_eq r1 r2
end)
- | Op2 (The, T, _, u1, u2) =>
- to_f_with_polarity polar
- (Op2 (The, T, Opt (Atom (2, bool_j0)), u1, u2))
- | Op2 (Eps, T, _, u1, u2) =>
- to_f_with_polarity polar
- (Op2 (Eps, T, Opt (Atom (2, bool_j0)), u1, u2))
| Op2 (Apply, T, _, u1, u2) =>
(case (polar, rep_of u1) of
(Neg, Func (R, Formula Neut)) => kk_subset (to_opt R u2) (to_r u1)
@@ -1473,41 +1463,6 @@
KK.None)
(to_rep R1 u1) (to_rep R1 u2)
end)
- | Op2 (The, _, R, u1, u2) =>
- if is_opt_rep R then
- let val r1 = to_opt (Func (unopt_rep R, bool_atom_R)) u1 in
- kk_rel_if (is_surely_singleton R r1) (kk_join r1 true_atom)
- (kk_rel_if (kk_or (kk_some (kk_join r1 true_atom))
- (kk_subset (full_rel_for_rep R)
- (kk_join r1 false_atom)))
- (to_rep R u2) (empty_rel_for_rep R))
- end
- else
- let val r1 = to_rep (Func (R, Formula Neut)) u1 in
- kk_rel_if (kk_one r1) r1 (to_rep R u2)
- end
- | Op2 (Eps, _, R, u1, u2) =>
- if is_opt_rep (rep_of u1) then
- let
- val r1 = to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1
- val r2 = to_rep R u2
- in
- kk_union (kk_rel_if (is_surely_singleton R r1)
- (kk_join r1 true_atom) (empty_rel_for_rep R))
- (kk_rel_if (kk_or (kk_subset r2 (kk_join r1 true_atom))
- (kk_subset (full_rel_for_rep R)
- (kk_join r1 false_atom)))
- r2 (empty_rel_for_rep R))
- end
- else
- let
- val r1 = to_rep (Func (unopt_rep R, Formula Neut)) u1
- val r2 = to_rep R u2
- in
- kk_union (kk_rel_if (kk_one r1) r1 (empty_rel_for_rep R))
- (kk_rel_if (kk_or (kk_no r1) (kk_subset r2 r1))
- r2 (empty_rel_for_rep R))
- end
| Op2 (Triad, _, Opt (Atom (2, j0)), u1, u2) =>
let
val f1 = to_f u1
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Sep 14 13:24:18 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Sep 14 13:44:43 2010 +0200
@@ -816,16 +816,6 @@
let
val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
in (t, format_term_type thy def_table formats t) end
- else if s = @{const_name undefined_fast_The} then
- (Const (nitpick_prefix ^ "The fallback", T),
- format_type default_format
- (lookup_format thy def_table formats
- (Const (@{const_name The}, (T --> bool_T) --> T))) T)
- else if s = @{const_name undefined_fast_Eps} then
- (Const (nitpick_prefix ^ "Eps fallback", T),
- format_type default_format
- (lookup_format thy def_table formats
- (Const (@{const_name Eps}, (T --> bool_T) --> T))) T)
else
let val t = Const (original_name s, T) in
(t, format_term_type thy def_table formats t)
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Sep 14 13:24:18 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Sep 14 13:44:43 2010 +0200
@@ -711,8 +711,7 @@
MFun (a_to_b_set_M, S Minus, ab_set_M)), accum)
end
| _ =>
- if s = @{const_name safe_The} orelse
- s = @{const_name safe_Eps} then
+ if s = @{const_name safe_The} then
let
val a_set_M = mtype_for (domain_type T)
val a_M = dest_MFun a_set_M |> #1
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Sep 14 13:24:18 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Sep 14 13:44:43 2010 +0200
@@ -53,8 +53,6 @@
Subset |
DefEq |
Eq |
- The |
- Eps |
Triad |
Composition |
Product |
@@ -170,8 +168,6 @@
Subset |
DefEq |
Eq |
- The |
- Eps |
Triad |
Composition |
Product |
@@ -237,8 +233,6 @@
| string_for_op2 Subset = "Subset"
| string_for_op2 DefEq = "DefEq"
| string_for_op2 Eq = "Eq"
- | string_for_op2 The = "The"
- | string_for_op2 Eps = "Eps"
| string_for_op2 Triad = "Triad"
| string_for_op2 Composition = "Composition"
| string_for_op2 Product = "Product"
@@ -674,16 +668,14 @@
else if is_rep_fun ctxt x then
Func oo best_non_opt_symmetric_reps_for_fun_type
else if all_exact orelse is_skolem_name v orelse
- member (op =) [@{const_name undefined_fast_The},
- @{const_name undefined_fast_Eps},
- @{const_name bisim},
- @{const_name bisim_iterator_max}]
- (original_name s) then
+ member (op =) [@{const_name bisim},
+ @{const_name bisim_iterator_max}]
+ (original_name s) then
best_non_opt_set_rep_for_type
else if member (op =) [@{const_name set}, @{const_name distinct},
@{const_name ord_class.less},
@{const_name ord_class.less_eq}]
- (original_name s) then
+ (original_name s) then
best_set_rep_for_type
else
best_opt_set_rep_for_type) scope T
@@ -1072,29 +1064,6 @@
raise SAME ())
handle SAME () => s_op2 oper T (Formula polar) u1' u2'
end
- else if oper = The orelse oper = Eps then
- let
- val u1' = sub u1
- val opt1 = is_opt_rep (rep_of u1')
- val opt = (oper = Eps orelse opt1)
- val unopt_R = best_one_rep_for_type scope T |> optable_rep ofs T
- val R = if is_boolean_type T then bool_rep polar opt
- else unopt_R |> opt ? opt_rep ofs T
- val u = Op2 (oper, T, R, u1', sub u2)
- in
- if is_complete_type datatypes true T orelse not opt1 then
- u
- else
- let
- val x_u = BoundName (~1, T, unopt_R, "descr.x")
- val R = R |> opt_rep ofs T
- in
- Op3 (If, T, R,
- Op2 (Exist, bool_T, Formula Pos, x_u,
- s_op2 Apply bool_T (Formula Pos) (gsub false Pos u1)
- x_u), u, Cst (Unknown, T, R))
- end
- end
else
let
val u1 = sub u1
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Sep 14 13:24:18 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Sep 14 13:44:43 2010 +0200
@@ -26,8 +26,7 @@
(polar = Neg andalso quant_s <> @{const_name Ex})
val is_descr =
- member (op =) [@{const_name The}, @{const_name Eps}, @{const_name safe_The},
- @{const_name safe_Eps}]
+ member (op =) [@{const_name The}, @{const_name Eps}, @{const_name safe_The}]
(** Binary coding of integers **)