--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jan 03 18:33:17 2012 +0100
@@ -87,7 +87,7 @@
val frac_from_term_pair : typ -> term -> term -> term
val is_TFree : typ -> bool
val is_fun_type : typ -> bool
- val is_set_type : typ -> bool
+ val is_set_like_type : typ -> bool
val is_pair_type : typ -> bool
val is_lfp_iterator_type : typ -> bool
val is_gfp_iterator_type : typ -> bool
@@ -101,6 +101,7 @@
val is_record_type : typ -> bool
val is_number_type : Proof.context -> typ -> bool
val is_higher_order_type : typ -> bool
+ val elem_type : typ -> typ
val const_for_iterator_type : typ -> styp
val strip_n_binders : int -> typ -> typ list * typ
val nth_range_type : int -> typ -> typ
@@ -416,7 +417,7 @@
((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
((@{const_name of_nat}, nat_T --> int_T), 0)]
-val built_in_set_consts =
+val built_in_set_like_consts =
[(@{const_name ord_class.less_eq}, 2)]
fun unarize_type @{typ "unsigned_bit word"} = nat_T
@@ -477,8 +478,9 @@
| is_TFree _ = false
fun is_fun_type (Type (@{type_name fun}, _)) = true
| is_fun_type _ = false
-fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
- | is_set_type _ = false
+fun is_set_like_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
+ | is_set_like_type (Type (@{type_name set}, _)) = true
+ | is_set_like_type _ = false
fun is_pair_type (Type (@{type_name prod}, _)) = true
| is_pair_type _ = false
fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
@@ -503,6 +505,9 @@
| is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
| is_higher_order_type _ = false
+fun elem_type (Type (@{type_name set}, [T])) = T
+ | elem_type T = raise TYPE ("Nitpick_HOL.elem_type", [T], [])
+
fun iterator_type_for_const gfp (s, T) =
Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
binder_types T)
@@ -1314,8 +1319,8 @@
if is_iterator_type T then SOME 0 else NONE
| @{const_name Suc} =>
if is_iterator_type (domain_type T) then SOME 0 else NONE
- | _ => if is_fun_type T andalso is_set_type (domain_type T) then
- AList.lookup (op =) built_in_set_consts s
+ | _ => if is_fun_type T andalso is_set_like_type (domain_type T) then
+ AList.lookup (op =) built_in_set_like_consts s
else
NONE
end
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Jan 03 18:33:17 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Jan 03 18:33:17 2012 +0100
@@ -224,6 +224,7 @@
Type (@{type_name fun}, [T1, T2]) =>
MFun (fresh_mfun_for_fun_type mdata all_minus T1 T2)
| Type (@{type_name prod}, [T1, T2]) => MPair (pairself do_type (T1, T2))
+ | Type (@{type_name set}, [T']) => do_type (T' --> bool_T)
| Type (z as (s, _)) =>
if could_exist_alpha_sub_mtype ctxt alpha_T T then
case AList.lookup (op =) (!datatype_mcache) z of
@@ -474,15 +475,18 @@
fun prop_for_bool b = if b then Prop_Logic.True else Prop_Logic.False
fun prop_for_bool_var_equality (v1, v2) =
- Prop_Logic.SAnd (Prop_Logic.SOr (Prop_Logic.BoolVar v1, Prop_Logic.SNot (Prop_Logic.BoolVar v2)),
- Prop_Logic.SOr (Prop_Logic.SNot (Prop_Logic.BoolVar v1), Prop_Logic.BoolVar v2))
+ Prop_Logic.SAnd (Prop_Logic.SOr (Prop_Logic.BoolVar v1,
+ Prop_Logic.SNot (Prop_Logic.BoolVar v2)),
+ Prop_Logic.SOr (Prop_Logic.SNot (Prop_Logic.BoolVar v1),
+ Prop_Logic.BoolVar v2))
fun prop_for_assign (x, a) =
let val (b1, b2) = bools_from_annotation a in
Prop_Logic.SAnd (Prop_Logic.BoolVar (fst_var x) |> not b1 ? Prop_Logic.SNot,
- Prop_Logic.BoolVar (snd_var x) |> not b2 ? Prop_Logic.SNot)
+ Prop_Logic.BoolVar (snd_var x) |> not b2 ? Prop_Logic.SNot)
end
fun prop_for_assign_literal (x, (Plus, a)) = prop_for_assign (x, a)
- | prop_for_assign_literal (x, (Minus, a)) = Prop_Logic.SNot (prop_for_assign (x, a))
+ | prop_for_assign_literal (x, (Minus, a)) =
+ Prop_Logic.SNot (prop_for_assign (x, a))
fun prop_for_atom_assign (A a', a) = prop_for_bool (a = a')
| prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, (Plus, a))
fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2)
@@ -499,7 +503,8 @@
| prop_for_comp (aa1, aa2, Neq, []) =
Prop_Logic.SNot (prop_for_comp (aa1, aa2, Eq, []))
| prop_for_comp (aa1, aa2, Leq, []) =
- Prop_Logic.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen))
+ Prop_Logic.SOr (prop_for_atom_equality (aa1, aa2),
+ prop_for_atom_assign (aa2, Gen))
| prop_for_comp (aa1, aa2, cmp, xs) =
Prop_Logic.SOr (prop_for_exists_var_assign_literal xs Gen,
prop_for_comp (aa1, aa2, cmp, []))
@@ -540,7 +545,8 @@
SOME (extract_assigns max_var assigns asgs |> tap print_solution)
val _ = print_problem comps clauses
val prop =
- Prop_Logic.all (map prop_for_comp comps @ map prop_for_assign_clause clauses)
+ Prop_Logic.all (map prop_for_comp comps @
+ map prop_for_assign_clause clauses)
in
if Prop_Logic.eval (K false) prop then
do_assigns (K (SOME false))
@@ -739,6 +745,7 @@
<= length ts
| _ => true
val mtype_for = fresh_mtype_for_type mdata false
+ fun mtype_for_set x T = MFun (mtype_for (elem_type T), V x, bool_M)
fun do_all T (gamma, cset) =
let
val abs_M = mtype_for (domain_type (domain_type T))
@@ -774,6 +781,8 @@
fun custom_mtype_for (T as Type (@{type_name fun}, [T1, T2])) =
if T = set_T then set_M
else MFun (custom_mtype_for T1, A Gen, custom_mtype_for T2)
+ | custom_mtype_for (Type (@{type_name set}, [T'])) =
+ custom_mtype_for (T' --> bool_T)
| custom_mtype_for T = mtype_for T
in
(custom_mtype_for T, (gamma, cset |> add_mtype_is_concrete [] set_M))
@@ -840,10 +849,8 @@
| @{const_name converse} =>
let
val x = Unsynchronized.inc max_fresh
- fun mtype_for_set T =
- MFun (mtype_for (domain_type T), V x, bool_M)
- val ab_set_M = domain_type T |> mtype_for_set
- val ba_set_M = range_type T |> mtype_for_set
+ val ab_set_M = domain_type T |> mtype_for_set x
+ val ba_set_M = range_type T |> mtype_for_set x
in
(MFun (ab_set_M, A Gen, ba_set_M),
accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
@@ -852,29 +859,25 @@
| @{const_name rel_comp} =>
let
val x = Unsynchronized.inc max_fresh
- fun mtype_for_set T =
- MFun (mtype_for (domain_type T), V x, bool_M)
- val bc_set_M = domain_type T |> mtype_for_set
- val ab_set_M = domain_type (range_type T) |> mtype_for_set
- val ac_set_M = nth_range_type 2 T |> mtype_for_set
+ val bc_set_M = domain_type T |> mtype_for_set x
+ val ab_set_M = domain_type (range_type T) |> mtype_for_set x
+ val ac_set_M = nth_range_type 2 T |> mtype_for_set x
in
(MFun (bc_set_M, A Gen, MFun (ab_set_M, A Gen, ac_set_M)),
accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
end
| @{const_name finite} =>
let
- val M1 = mtype_for (domain_type (domain_type T))
+ val M1 = mtype_for (elem_type (domain_type T))
val a = if exists_alpha_sub_mtype M1 then Fls else Gen
in (MFun (MFun (M1, A a, bool_M), A Gen, bool_M), accum) end
| @{const_name prod} =>
let
val x = Unsynchronized.inc max_fresh
- fun mtype_for_set T =
- MFun (mtype_for (domain_type T), V x, bool_M)
- val a_set_M = mtype_for_set (domain_type T)
+ val a_set_M = domain_type T |> mtype_for_set x
val b_set_M =
- mtype_for_set (range_type (domain_type (range_type T)))
- val ab_set_M = mtype_for_set (nth_range_type 2 T)
+ range_type (domain_type (range_type T)) |> mtype_for_set x
+ val ab_set_M = nth_range_type 2 T |> mtype_for_set x
in
(MFun (a_set_M, A Gen, MFun (b_set_M, A Gen, ab_set_M)),
accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
@@ -886,7 +889,7 @@
val a_M = dest_MFun a_set_M |> #1
in (MFun (a_set_M, A Gen, a_M), accum) end
else if s = @{const_name ord_class.less_eq} andalso
- is_set_type (domain_type T) then
+ is_set_like_type (domain_type T) then
do_fragile_set_operation T accum
else if is_sel s then
(mtype_for_sel mdata x, accum)