# HG changeset patch # User blanchet # Date 1336689924 -7200 # Node ID 5f1afeebafbc372ffb8f0cf6c4bc87deb802fd28 # Parent 25686e1e00241da6fd882f58fa503c917ae6a459 fixed "real" after they were redefined as a 'quotient_type' diff -r 25686e1e0024 -r 5f1afeebafbc src/HOL/Nitpick.thy --- 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 \ (a, b) \ 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 \ 'b set \ ('a \ 'b) set" where "prod A B = {(a, b). a \ A \ b \ 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]: diff -r 25686e1e0024 -r 5f1afeebafbc src/HOL/Nitpick_Examples/Manual_Nits.thy --- 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\real) \ 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 *} diff -r 25686e1e0024 -r 5f1afeebafbc src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 \ 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 \ 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 diff -r 25686e1e0024 -r 5f1afeebafbc src/HOL/Tools/Nitpick/nitpick_model.ML --- 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 diff -r 25686e1e0024 -r 5f1afeebafbc src/HOL/Tools/Nitpick/nitpick_nut.ML --- 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}, diff -r 25686e1e0024 -r 5f1afeebafbc src/HOL/Tools/Nitpick/nitpick_preproc.ML --- 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 diff -r 25686e1e0024 -r 5f1afeebafbc src/HOL/Tools/Nitpick/nitpick_scope.ML --- 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