--- a/src/HOL/Nitpick.thy Thu May 10 22:00:24 2012 +0200
+++ b/src/HOL/Nitpick.thy Fri May 11 00:45:24 2012 +0200
@@ -72,6 +72,10 @@
"tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
by (simp add: trancl_def)
+lemma [nitpick_simp, no_atp]:
+"of_nat n = (if n = 0 then 0 else 1 + of_nat (n - 1))"
+by (case_tac n) auto
+
definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
"prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
@@ -93,7 +97,7 @@
text {*
The following lemmas are not strictly necessary but they help the
-\textit{special\_level} optimization.
+\textit{specialize} optimization.
*}
lemma The_psimp [nitpick_psimp, no_atp]:
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Thu May 10 22:00:24 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri May 11 00:45:24 2012 +0200
@@ -145,9 +145,7 @@
oops
lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
-(* FIXME: broken by conversion of RealDef.thy to lift_definition/transfer.
nitpick [show_datatypes, expect = genuine]
-*)
oops
subsection {* 2.8. Inductive and Coinductive Predicates *}
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu May 10 22:00:24 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri May 11 00:45:24 2012 +0200
@@ -396,13 +396,13 @@
(@{const_name unknown}, 0),
(@{const_name is_unknown}, 1),
(@{const_name safe_The}, 1),
- (@{const_name Frac}, 0),
- (@{const_name norm_frac}, 0)]
+ (@{const_name Nitpick.Frac}, 0),
+ (@{const_name Nitpick.norm_frac}, 0)]
val built_in_nat_consts =
[(@{const_name Suc}, 0),
(@{const_name nat}, 0),
- (@{const_name nat_gcd}, 0),
- (@{const_name nat_lcm}, 0)]
+ (@{const_name Nitpick.nat_gcd}, 0),
+ (@{const_name Nitpick.nat_lcm}, 0)]
val built_in_typed_consts =
[((@{const_name zero_class.zero}, int_T), 0),
((@{const_name one_class.one}, int_T), 0),
@@ -565,10 +565,13 @@
fun typedef_info ctxt s =
if is_frac_type ctxt (Type (s, [])) then
SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
- Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
- set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Collect Frac"}
- |> Logic.varify_global,
- set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
+ Abs_name = @{const_name Nitpick.Abs_Frac},
+ Rep_name = @{const_name Nitpick.Rep_Frac},
+ set_def = NONE,
+ prop_of_Rep = @{prop "Nitpick.Rep_Frac x \<in> Collect Nitpick.Frac"}
+ |> Logic.varify_global,
+ set_name = @{const_name Nitpick.Frac}, Abs_inverse = NONE,
+ Rep_inverse = NONE}
else case Typedef.get_info ctxt s of
(* When several entries are returned, it shouldn't matter much which one
we take (according to Florian Haftmann). *)
@@ -662,17 +665,19 @@
s |> AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
|> Option.map snd |> these |> null |> not
| is_codatatype _ _ = false
+fun is_registered_type ctxt T = is_frac_type ctxt T orelse is_codatatype ctxt T
fun is_real_quot_type ctxt (Type (s, _)) =
is_some (Quotient_Info.lookup_quotients ctxt s)
| is_real_quot_type _ _ = false
fun is_quot_type ctxt T =
- is_real_quot_type ctxt T andalso not (is_codatatype ctxt T)
+ is_real_quot_type ctxt T andalso not (is_registered_type ctxt T)
fun is_pure_typedef ctxt (T as Type (s, _)) =
let val thy = Proof_Context.theory_of ctxt in
- is_typedef ctxt s andalso
- not (is_real_datatype thy s orelse is_real_quot_type ctxt T orelse
- is_codatatype ctxt T orelse is_record_type T orelse
- is_integer_like_type T)
+ is_frac_type ctxt T orelse
+ (is_typedef ctxt s andalso
+ not (is_real_datatype thy s orelse is_real_quot_type ctxt T orelse
+ is_codatatype ctxt T orelse is_record_type T orelse
+ is_integer_like_type T))
end
| is_pure_typedef _ _ = false
fun is_univ_typedef ctxt (Type (s, _)) =
@@ -700,7 +705,7 @@
| is_univ_typedef _ _ = false
fun is_datatype ctxt stds (T as Type (s, _)) =
let val thy = Proof_Context.theory_of ctxt in
- (is_typedef ctxt s orelse is_codatatype ctxt T orelse
+ (is_typedef ctxt s orelse is_registered_type ctxt T orelse
T = @{typ ind} orelse is_real_quot_type ctxt T) andalso
not (is_basic_datatype thy stds s)
end
@@ -742,12 +747,13 @@
fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun},
[_, abs_T as Type (s', _)]))) =
try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.AbsF) s'
- = SOME (Const x) andalso not (is_codatatype ctxt abs_T)
+ = SOME (Const x) andalso not (is_registered_type ctxt abs_T)
| is_quot_abs_fun _ _ = false
fun is_quot_rep_fun ctxt (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)
+ SOME (Const (s', _)) =>
+ s = s' andalso not (is_registered_type ctxt abs_T)
| NONE => false)
| is_quot_rep_fun _ _ = false
@@ -801,9 +807,9 @@
(is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse
is_coconstr ctxt x
end
-fun is_stale_constr ctxt (x as (_, T)) =
- is_codatatype ctxt (body_type T) andalso is_constr_like ctxt x andalso
- not (is_coconstr ctxt x)
+fun is_stale_constr ctxt (x as (s, T)) =
+ is_registered_type ctxt (body_type T) andalso is_constr_like ctxt x andalso
+ not (s = @{const_name Nitpick.Abs_Frac} orelse is_coconstr ctxt x)
fun is_constr ctxt stds (x as (_, T)) =
let val thy = Proof_Context.theory_of ctxt in
is_constr_like ctxt x andalso
@@ -919,7 +925,13 @@
s of
SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type ctxt T)) xs'
| _ =>
- if is_datatype ctxt stds T then
+ if is_frac_type ctxt T then
+ case typedef_info ctxt s of
+ SOME {abs_type, rep_type, Abs_name, ...} =>
+ [(Abs_name,
+ varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
+ | NONE => [] (* impossible *)
+ else if is_datatype ctxt stds T then
case Datatype.get_info thy s of
SOME {index, descr, ...} =>
let
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu May 10 22:00:24 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri May 11 00:45:24 2012 +0200
@@ -574,7 +574,7 @@
|> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
|> dest_n_tuple (length uncur_arg_Ts)
val t =
- if constr_s = @{const_name Abs_Frac} then
+ if constr_s = @{const_name Nitpick.Abs_Frac} then
case ts of
[Const (@{const_name Pair}, _) $ t1 $ t2] =>
frac_from_term_pair (body_type T) t1 t2
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu May 10 22:00:24 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri May 11 00:45:24 2012 +0200
@@ -569,8 +569,8 @@
Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
else
do_apply t0 ts
- | (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any)
- | (Const (@{const_name nat_lcm}, T), []) => Cst (Lcm, T, Any)
+ | (Const (@{const_name Nitpick.nat_gcd}, T), []) => Cst (Gcd, T, Any)
+ | (Const (@{const_name Nitpick.nat_lcm}, T), []) => Cst (Lcm, T, Any)
| (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) =>
if is_built_in_const thy stds x then
let val num_T = domain_type T in
@@ -586,8 +586,9 @@
| (Const (@{const_name safe_The},
Type (@{type_name fun}, [_, T2])), [t1]) =>
Op1 (SafeThe, T2, Any, sub t1)
- | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
- | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any)
+ | (Const (@{const_name Nitpick.Frac}, T), []) => Cst (Fracs, T, Any)
+ | (Const (@{const_name Nitpick.norm_frac}, T), []) =>
+ Cst (NormFrac, T, Any)
| (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) =>
Cst (NatToInt, T, Any)
| (Const (@{const_name of_nat},
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu May 10 22:00:24 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri May 11 00:45:24 2012 +0200
@@ -45,9 +45,10 @@
| aux def (t1 $ t2) = aux def t1 andalso aux def t2
| aux def (t as Const (s, _)) =
(not def orelse t <> @{const Suc}) andalso
- not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
- @{const_name nat_gcd}, @{const_name nat_lcm},
- @{const_name Frac}, @{const_name norm_frac}] s)
+ not (member (op =)
+ [@{const_name Nitpick.Abs_Frac}, @{const_name Nitpick.Rep_Frac},
+ @{const_name Nitpick.nat_gcd}, @{const_name Nitpick.nat_lcm},
+ @{const_name Nitpick.Frac}, @{const_name Nitpick.norm_frac}] s)
| aux def (Abs (_, _, t')) = aux def t'
| aux _ _ = true
in aux end
@@ -1061,10 +1062,12 @@
(t = t' andalso is_sel_like_and_no_discr s andalso
sel_no_from_name s = n)
| is_nth_sel_on _ _ _ = false
- fun do_term (Const (@{const_name Rep_Frac}, _)
- $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
- | do_term (Const (@{const_name Abs_Frac}, _)
- $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
+ fun do_term (Const (@{const_name Nitpick.Rep_Frac}, _)
+ $ (Const (@{const_name Nitpick.Abs_Frac}, _) $ t1)) [] =
+ do_term t1 []
+ | do_term (Const (@{const_name Nitpick.Abs_Frac}, _)
+ $ (Const (@{const_name Nitpick.Rep_Frac}, _) $ t1)) [] =
+ do_term t1 []
| do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
| do_term (t as Const (x as (s, T))) (args as _ :: _) =
((if is_constr_like ctxt x then
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu May 10 22:00:24 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri May 11 00:45:24 2012 +0200
@@ -450,7 +450,7 @@
has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T
fun is_concrete facto =
is_word_type T orelse
- (* FIXME: looks wrong other types than just functions might be
+ (* FIXME: looks wrong; other types than just functions might be
abstract. "is_complete" is also suspicious. *)
xs |> maps (binder_types o snd) |> maps binder_types
|> forall (has_exact_card hol_ctxt facto finitizable_dataTs