# HG changeset patch # User bulwahn # Date 1266930036 -3600 # Node ID fc132ff3dfa2b223bf4689adbe4d9fdff8e84f3e # Parent 956d08ec5d6569df3c30260a4c1f8b18cb92e11e# Parent 4123977b469d1e95bb7b5c986384f58211c39471 merged diff -r 4123977b469d -r fc132ff3dfa2 doc-src/Nitpick/nitpick.tex --- 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 diff -r 4123977b469d -r fc132ff3dfa2 src/HOL/NSA/Hyperreal.thy --- 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 diff -r 4123977b469d -r fc132ff3dfa2 src/HOL/Nitpick.thy --- 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 \ 'a \ 'a \ bool" and bisim_iterator_max :: bisim_iterator and Quot :: "'a \ 'b" - and quot_normal :: "'a \ 'a" and Tha :: "('a \ bool) \ '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 diff -r 4123977b469d -r fc132ff3dfa2 src/HOL/Nitpick_Examples/Manual_Nits.thy --- 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 @@ "\even' m; even' n\ \ even' (m + n)" lemma "\n \ {0, 2, 4, 6, 8}. \ 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) \ even' n" diff -r 4123977b469d -r fc132ff3dfa2 src/HOL/Nitpick_Examples/Special_Nits.thy --- 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 "\one \ {1}. \two \ {2}. f5 (\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 "\two \ {2}. \one \ {1}. f5 (\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 "\a. g a = a diff -r 4123977b469d -r fc132ff3dfa2 src/HOL/Nitpick_Examples/Typedef_Nits.thy --- 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 \ Abs_Nat Zero_Rep" -(* nitpick [expect = none] FIXME *) +nitpick [expect = none] by (rule Zero_nat_def_raw) lemma "Suc \ \n. Abs_Nat (Suc_Rep (Rep_Nat n))" -(* nitpick [expect = none] FIXME *) +nitpick [expect = none] by (rule Suc_def) lemma "Suc \ \n. Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))" diff -r 4123977b469d -r fc132ff3dfa2 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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) diff -r 4123977b469d -r fc132ff3dfa2 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- 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) => diff -r 4123977b469d -r fc132ff3dfa2 src/HOL/Tools/Nitpick/nitpick_nut.ML --- 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}, _, _), _) => diff -r 4123977b469d -r fc132ff3dfa2 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- 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)