--- a/doc-src/Nitpick/nitpick.tex Tue Feb 23 13:57:51 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Tue Feb 23 14:00:36 2010 +0100
@@ -154,7 +154,7 @@
15~seconds (instead of 30~seconds). This was done by adding the line
\prew
-\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1, \,\,\textit{timeout} = 15$\,s$]
+\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1, \,\textit{timeout} = 15$\,s$]
\postw
after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
--- a/src/HOL/NSA/Hyperreal.thy Tue Feb 23 13:57:51 2010 +0100
+++ b/src/HOL/NSA/Hyperreal.thy Tue Feb 23 14:00:36 2010 +0100
@@ -7,7 +7,7 @@
*)
theory Hyperreal
-imports Ln Deriv Taylor Integration HLog
+imports Ln Deriv Taylor HLog
begin
end
--- a/src/HOL/Nitpick.thy Tue Feb 23 13:57:51 2010 +0100
+++ b/src/HOL/Nitpick.thy Tue Feb 23 14:00:36 2010 +0100
@@ -36,7 +36,6 @@
and bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
and bisim_iterator_max :: bisim_iterator
and Quot :: "'a \<Rightarrow> 'b"
- and quot_normal :: "'a \<Rightarrow> 'a"
and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
datatype ('a, 'b) pair_box = PairBox 'a 'b
@@ -237,11 +236,10 @@
setup {* Nitpick_Isar.setup *}
hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim
- bisim_iterator_max Quot quot_normal Tha PairBox FunBox Word refl' wf'
- wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd
- int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac
- plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac
- of_frac
+ bisim_iterator_max Quot Tha PairBox FunBox Word refl' wf' wf_wfrec wf_wfrec'
+ wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac
+ Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac
+ times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac
hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Feb 23 13:57:51 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Feb 23 14:00:36 2010 +0100
@@ -149,7 +149,7 @@
"\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
-nitpick [card nat = 10, unary_ints, verbose, show_consts] (* FIXME: should be genuine *)
+nitpick [card nat = 10, unary_ints, verbose, show_consts]
oops
lemma "even' (n - 2) \<Longrightarrow> even' n"
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy Tue Feb 23 13:57:51 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Tue Feb 23 14:00:36 2010 +0100
@@ -110,12 +110,12 @@
lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.
f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
-nitpick [expect = potential] (* unfortunate *)
+nitpick [expect = genuine]
oops
lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.
f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
-nitpick [expect = potential] (* unfortunate *)
+nitpick [expect = genuine]
oops
lemma "\<forall>a. g a = a
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Feb 23 13:57:51 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Feb 23 14:00:36 2010 +0100
@@ -143,11 +143,11 @@
by (rule Rep_Sum_inverse)
lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
-(* nitpick [expect = none] FIXME *)
+nitpick [expect = none]
by (rule Zero_nat_def_raw)
lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Rep_Nat n))"
-(* nitpick [expect = none] FIXME *)
+nitpick [expect = none]
by (rule Suc_def)
lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))"
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Feb 23 13:57:51 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Feb 23 14:00:36 2010 +0100
@@ -54,6 +54,7 @@
val numeral_prefix : string
val ubfp_prefix : string
val lbfp_prefix : string
+ val quot_normal_prefix : string
val skolem_prefix : string
val special_prefix : string
val uncurry_prefix : string
@@ -173,7 +174,7 @@
val inverse_axioms_for_rep_fun : theory -> styp -> term list
val optimized_typedef_axioms : theory -> string * typ list -> term list
val optimized_quot_type_axioms :
- theory -> (typ option * bool) list -> string * typ list -> term list
+ Proof.context -> (typ option * bool) list -> string * typ list -> term list
val def_of_const : theory -> const_table -> styp -> term option
val fixpoint_kind_of_const :
theory -> const_table -> string * typ -> fixpoint_kind
@@ -268,6 +269,7 @@
val step_prefix = nitpick_prefix ^ "step" ^ name_sep
val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep
val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep
+val quot_normal_prefix = nitpick_prefix ^ "qn" ^ name_sep
val skolem_prefix = nitpick_prefix ^ "sk"
val special_prefix = nitpick_prefix ^ "sp"
val uncurry_prefix = nitpick_prefix ^ "unc"
@@ -277,6 +279,9 @@
(* int -> string *)
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
+(* Proof.context -> typ -> string *)
+fun quot_normal_name_for_type ctxt T =
+ quot_normal_prefix ^ unyxml (Syntax.string_of_typ ctxt T)
(* string -> string * string *)
val strip_first_name_sep =
@@ -559,14 +564,15 @@
(* theory -> typ -> typ -> typ -> typ *)
fun instantiate_type thy T1 T1' T2 =
Same.commit (Envir.subst_type_same
- (Sign.typ_match thy (Logic.varifyT T1, T1') Vartab.empty))
- (Logic.varifyT T2)
+ (Sign.typ_match thy (T1, T1') Vartab.empty)) T2
handle Type.TYPE_MATCH =>
raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
+fun varify_and_instantiate_type thy T1 T1' T2 =
+ instantiate_type thy (Logic.varifyT T1) T1' (Logic.varifyT T2)
(* theory -> typ -> typ -> styp *)
fun repair_constr_type thy body_T' T =
- instantiate_type thy (body_type T) body_T' T
+ varify_and_instantiate_type thy (body_type T) body_T' T
(* string -> (string * string) list -> theory -> theory *)
fun register_frac_type frac_s ersaetze thy =
@@ -889,7 +895,8 @@
[(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
else case typedef_info thy s of
SOME {abs_type, rep_type, Abs_name, ...} =>
- [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
+ [(Abs_name,
+ varify_and_instantiate_type thy abs_type T rep_type --> T)]
| NONE =>
if T = @{typ ind} then
[dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
@@ -1385,7 +1392,7 @@
else case typedef_info thy abs_s of
SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} =>
let
- val rep_T = instantiate_type thy abs_type abs_T rep_type
+ val rep_T = varify_and_instantiate_type thy abs_type abs_T rep_type
val rep_t = Const (Rep_name, abs_T --> rep_T)
val set_t = Const (set_name, rep_T --> bool_T)
val set_t' =
@@ -1400,8 +1407,10 @@
end
| NONE => []
end
-fun optimized_quot_type_axioms thy stds abs_z =
+(* Proof.context -> string * typ list -> term list *)
+fun optimized_quot_type_axioms ctxt stds abs_z =
let
+ val thy = ProofContext.theory_of ctxt
val abs_T = Type abs_z
val rep_T = rep_type_for_quot_type thy abs_T
val equiv_rel = equiv_relation_for_quot_type thy abs_T
@@ -1410,7 +1419,7 @@
val y_var = Var (("y", 0), rep_T)
val x = (@{const_name Quot}, rep_T --> abs_T)
val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T
- val normal_t = Const (@{const_name quot_normal}, rep_T --> rep_T)
+ val normal_t = Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T)
val normal_x = normal_t $ x_var
val normal_y = normal_t $ y_var
val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T)
@@ -1639,7 +1648,7 @@
in
(Abs (Name.uu, rep_T,
Const (@{const_name Quot}, rep_T --> abs_T)
- $ (Const (@{const_name quot_normal},
+ $ (Const (quot_normal_name_for_type ctxt abs_T,
rep_T --> rep_T) $ Bound 0)), ts)
end
else if is_quot_rep_fun ctxt x then
@@ -2230,6 +2239,10 @@
else if String.isPrefix step_prefix s then
(Const (step_name, T --> T) $ Const (unprefix step_prefix s, T),
format_type default_format default_format T)
+ else if String.isPrefix quot_normal_prefix s then
+ let val t = Const (nitpick_prefix ^ "normalize quotient type", T) in
+ (t, format_term_type thy def_table formats t)
+ end
else if String.isPrefix skolem_prefix s then
let
val ss = the (AList.lookup (op =) (!skolems) s)
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Feb 23 13:57:51 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Feb 23 14:00:36 2010 +0100
@@ -1595,12 +1595,7 @@
KK.Atom (offset_of_type ofs nat_T)
else
fold kk_join (map to_integer [u1, u2]) (KK.Rel nat_subtract_rel)
- | Op2 (Apply, _, R, u1, u2) =>
- if is_Cst Unrep u2 andalso is_set_type (type_of u1) andalso
- is_FreeName u1 then
- false_atom
- else
- to_apply R u1 u2
+ | Op2 (Apply, _, R, u1, u2) => to_apply R u1 u2
| Op2 (Lambda, _, R as Opt (Atom (1, j0)), u1, u2) =>
to_guard [u1, u2] R (KK.Atom j0)
| Op2 (Lambda, _, Func (_, Formula Neut), u1, u2) =>
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Feb 23 13:57:51 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Feb 23 14:00:36 2010 +0100
@@ -95,7 +95,6 @@
val nickname_of : nut -> string
val is_skolem_name : nut -> bool
val is_eval_name : nut -> bool
- val is_FreeName : nut -> bool
val is_Cst : cst -> nut -> bool
val fold_nut : (nut -> 'a -> 'a) -> nut -> 'a -> 'a
val map_nut : (nut -> nut) -> nut -> nut
@@ -369,8 +368,6 @@
fun is_eval_name u =
String.isPrefix eval_prefix (nickname_of u)
handle NUT ("Nitpick_Nut.nickname_of", _) => false
-fun is_FreeName (FreeName _) = true
- | is_FreeName _ = false
(* cst -> nut -> bool *)
fun is_Cst cst (Cst (cst', _, _)) = (cst = cst')
| is_Cst _ _ = false
@@ -794,9 +791,9 @@
end
(* A nut is said to be constructive if whenever it evaluates to unknown in our
- three-valued logic, it would evaluate to a unrepresentable value ("unrep")
+ three-valued logic, it would evaluate to a unrepresentable value ("Unrep")
according to the HOL semantics. For example, "Suc n" is constructive if "n"
- is representable or "Unrep", because unknown implies unrep. *)
+ is representable or "Unrep", because unknown implies "Unrep". *)
(* nut -> bool *)
fun is_constructive u =
is_Cst Unrep u orelse
@@ -819,6 +816,16 @@
fun unknown_boolean T R =
Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown,
T, R)
+(* nut -> bool *)
+fun is_fully_representable_set u =
+ not (is_opt_rep (rep_of u)) andalso
+ case u of
+ FreeName _ => true
+ | Op1 (SingletonSet, _, _, _) => true
+ | Op2 (oper, _, _, u1, u2) =>
+ member (op =) [Union, SetDifference, Intersect] oper andalso
+ forall is_fully_representable_set [u1, u2]
+ | _ => false
(* op1 -> typ -> rep -> nut -> nut *)
fun s_op1 oper T R u1 =
@@ -860,7 +867,7 @@
if is_constructive u1 then
Cst (Unrep, T, R)
else if is_boolean_type T then
- if is_FreeName u1 then Cst (False, T, Formula Neut)
+ if is_fully_representable_set u1 then Cst (False, T, Formula Neut)
else unknown_boolean T R
else case u1 of
Op2 (Apply, _, _, ConstName (@{const_name List.append}, _, _), _) =>
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Feb 23 13:57:51 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Feb 23 14:00:36 2010 +0100
@@ -293,15 +293,15 @@
$ do_term new_Ts old_Ts polar t2
| Const (s as @{const_name The}, T) => do_description_operator s T
| Const (s as @{const_name Eps}, T) => do_description_operator s T
- | Const (@{const_name quot_normal}, Type ("fun", [T, _])) =>
- let val T' = box_type hol_ctxt InFunLHS T in
- Const (@{const_name quot_normal}, T' --> T')
- end
| Const (s as @{const_name Tha}, T) => do_description_operator s T
| Const (x as (s, T)) =>
Const (s, if s = @{const_name converse} orelse
s = @{const_name trancl} then
box_relational_operator_type T
+ else if String.isPrefix quot_normal_prefix s then
+ let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
+ T' --> T'
+ end
else if is_built_in_const thy stds fast_descrs x orelse
s = @{const_name Sigma} then
T
@@ -1022,8 +1022,9 @@
(* hol_context -> term -> (term list * term list) * (bool * bool) *)
fun axioms_for_term
- (hol_ctxt as {thy, max_bisim_depth, stds, user_axioms, fast_descrs,
- evals, def_table, nondef_table, user_nondefs, ...}) t =
+ (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
+ fast_descrs, evals, def_table, nondef_table, user_nondefs,
+ ...}) t =
let
type accumulator = styp list * (term list * term list)
(* (term list * term list -> term list)
@@ -1090,7 +1091,8 @@
else
accum |> fold (add_nondef_axiom depth)
(nondef_props_for_const thy false nondef_table x)
- |> is_funky_typedef thy (range_type T)
+ |> (is_funky_typedef thy (range_type T) orelse
+ range_type T = nat_T)
? fold (add_maybe_def_axiom depth)
(nondef_props_for_const thy true
(extra_table def_table s) x)
@@ -1100,7 +1102,8 @@
else
accum |> fold (add_nondef_axiom depth)
(nondef_props_for_const thy false nondef_table x)
- |> is_funky_typedef thy (range_type T)
+ |> (is_funky_typedef thy (range_type T) orelse
+ range_type T = nat_T)
? fold (add_maybe_def_axiom depth)
(nondef_props_for_const thy true
(extra_table def_table s) x)
@@ -1134,7 +1137,8 @@
#> (if is_pure_typedef thy T then
fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
else if is_quot_type thy T then
- fold (add_def_axiom depth) (optimized_quot_type_axioms thy stds z)
+ fold (add_def_axiom depth)
+ (optimized_quot_type_axioms ctxt stds z)
else if max_bisim_depth >= 0 andalso is_codatatype thy T then
fold (add_maybe_def_axiom depth)
(codatatype_bisim_axioms hol_ctxt T)