fixed "real" after they were redefined as a 'quotient_type'
authorblanchet
Fri May 11 00:45:24 2012 +0200 (2012-05-11)
changeset 479095f1afeebafbc
parent 47908 25686e1e0024
child 47910 ca5b629a5995
fixed "real" after they were redefined as a 'quotient_type'
src/HOL/Nitpick.thy
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
     1.1 --- a/src/HOL/Nitpick.thy	Thu May 10 22:00:24 2012 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Fri May 11 00:45:24 2012 +0200
     1.3 @@ -72,6 +72,10 @@
     1.4  "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
     1.5  by (simp add: trancl_def)
     1.6  
     1.7 +lemma [nitpick_simp, no_atp]:
     1.8 +"of_nat n = (if n = 0 then 0 else 1 + of_nat (n - 1))"
     1.9 +by (case_tac n) auto
    1.10 +
    1.11  definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
    1.12  "prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
    1.13  
    1.14 @@ -93,7 +97,7 @@
    1.15  
    1.16  text {*
    1.17  The following lemmas are not strictly necessary but they help the
    1.18 -\textit{special\_level} optimization.
    1.19 +\textit{specialize} optimization.
    1.20  *}
    1.21  
    1.22  lemma The_psimp [nitpick_psimp, no_atp]:
     2.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu May 10 22:00:24 2012 +0200
     2.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri May 11 00:45:24 2012 +0200
     2.3 @@ -145,9 +145,7 @@
     2.4  oops
     2.5  
     2.6  lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
     2.7 -(* FIXME: broken by conversion of RealDef.thy to lift_definition/transfer.
     2.8  nitpick [show_datatypes, expect = genuine]
     2.9 -*)
    2.10  oops
    2.11  
    2.12  subsection {* 2.8. Inductive and Coinductive Predicates *}
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu May 10 22:00:24 2012 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri May 11 00:45:24 2012 +0200
     3.3 @@ -396,13 +396,13 @@
     3.4     (@{const_name unknown}, 0),
     3.5     (@{const_name is_unknown}, 1),
     3.6     (@{const_name safe_The}, 1),
     3.7 -   (@{const_name Frac}, 0),
     3.8 -   (@{const_name norm_frac}, 0)]
     3.9 +   (@{const_name Nitpick.Frac}, 0),
    3.10 +   (@{const_name Nitpick.norm_frac}, 0)]
    3.11  val built_in_nat_consts =
    3.12    [(@{const_name Suc}, 0),
    3.13     (@{const_name nat}, 0),
    3.14 -   (@{const_name nat_gcd}, 0),
    3.15 -   (@{const_name nat_lcm}, 0)]
    3.16 +   (@{const_name Nitpick.nat_gcd}, 0),
    3.17 +   (@{const_name Nitpick.nat_lcm}, 0)]
    3.18  val built_in_typed_consts =
    3.19    [((@{const_name zero_class.zero}, int_T), 0),
    3.20     ((@{const_name one_class.one}, int_T), 0),
    3.21 @@ -565,10 +565,13 @@
    3.22  fun typedef_info ctxt s =
    3.23    if is_frac_type ctxt (Type (s, [])) then
    3.24      SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
    3.25 -          Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
    3.26 -          set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Collect Frac"}
    3.27 -                          |> Logic.varify_global,
    3.28 -          set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
    3.29 +          Abs_name = @{const_name Nitpick.Abs_Frac},
    3.30 +          Rep_name = @{const_name Nitpick.Rep_Frac},
    3.31 +          set_def = NONE,
    3.32 +          prop_of_Rep = @{prop "Nitpick.Rep_Frac x \<in> Collect Nitpick.Frac"}
    3.33 +                        |> Logic.varify_global,
    3.34 +          set_name = @{const_name Nitpick.Frac}, Abs_inverse = NONE,
    3.35 +          Rep_inverse = NONE}
    3.36    else case Typedef.get_info ctxt s of
    3.37      (* When several entries are returned, it shouldn't matter much which one
    3.38         we take (according to Florian Haftmann). *)
    3.39 @@ -662,17 +665,19 @@
    3.40      s |> AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
    3.41        |> Option.map snd |> these |> null |> not
    3.42    | is_codatatype _ _ = false
    3.43 +fun is_registered_type ctxt T = is_frac_type ctxt T orelse is_codatatype ctxt T
    3.44  fun is_real_quot_type ctxt (Type (s, _)) =
    3.45      is_some (Quotient_Info.lookup_quotients ctxt s)
    3.46    | is_real_quot_type _ _ = false
    3.47  fun is_quot_type ctxt T =
    3.48 -    is_real_quot_type ctxt T andalso not (is_codatatype ctxt T)
    3.49 +  is_real_quot_type ctxt T andalso not (is_registered_type ctxt T)
    3.50  fun is_pure_typedef ctxt (T as Type (s, _)) =
    3.51      let val thy = Proof_Context.theory_of ctxt in
    3.52 -      is_typedef ctxt s andalso
    3.53 -      not (is_real_datatype thy s orelse is_real_quot_type ctxt T orelse
    3.54 -           is_codatatype ctxt T orelse is_record_type T orelse
    3.55 -           is_integer_like_type T)
    3.56 +      is_frac_type ctxt T orelse
    3.57 +      (is_typedef ctxt s andalso
    3.58 +       not (is_real_datatype thy s orelse is_real_quot_type ctxt T orelse
    3.59 +            is_codatatype ctxt T orelse is_record_type T orelse
    3.60 +            is_integer_like_type T))
    3.61      end
    3.62    | is_pure_typedef _ _ = false
    3.63  fun is_univ_typedef ctxt (Type (s, _)) =
    3.64 @@ -700,7 +705,7 @@
    3.65    | is_univ_typedef _ _ = false
    3.66  fun is_datatype ctxt stds (T as Type (s, _)) =
    3.67      let val thy = Proof_Context.theory_of ctxt in
    3.68 -      (is_typedef ctxt s orelse is_codatatype ctxt T orelse
    3.69 +      (is_typedef ctxt s orelse is_registered_type ctxt T orelse
    3.70         T = @{typ ind} orelse is_real_quot_type ctxt T) andalso
    3.71        not (is_basic_datatype thy stds s)
    3.72      end
    3.73 @@ -742,12 +747,13 @@
    3.74  fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun},
    3.75                                           [_, abs_T as Type (s', _)]))) =
    3.76      try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.AbsF) s'
    3.77 -    = SOME (Const x) andalso not (is_codatatype ctxt abs_T)
    3.78 +    = SOME (Const x) andalso not (is_registered_type ctxt abs_T)
    3.79    | is_quot_abs_fun _ _ = false
    3.80  fun is_quot_rep_fun ctxt (s, Type (@{type_name fun},
    3.81                                     [abs_T as Type (abs_s, _), _])) =
    3.82      (case try (Quotient_Term.absrep_const_chk ctxt Quotient_Term.RepF) abs_s of
    3.83 -       SOME (Const (s', _)) => s = s' andalso not (is_codatatype ctxt abs_T)
    3.84 +       SOME (Const (s', _)) =>
    3.85 +       s = s' andalso not (is_registered_type ctxt abs_T)
    3.86       | NONE => false)
    3.87    | is_quot_rep_fun _ _ = false
    3.88  
    3.89 @@ -801,9 +807,9 @@
    3.90      (is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse
    3.91      is_coconstr ctxt x
    3.92    end
    3.93 -fun is_stale_constr ctxt (x as (_, T)) =
    3.94 -  is_codatatype ctxt (body_type T) andalso is_constr_like ctxt x andalso
    3.95 -  not (is_coconstr ctxt x)
    3.96 +fun is_stale_constr ctxt (x as (s, T)) =
    3.97 +  is_registered_type ctxt (body_type T) andalso is_constr_like ctxt x andalso
    3.98 +  not (s = @{const_name Nitpick.Abs_Frac} orelse is_coconstr ctxt x)
    3.99  fun is_constr ctxt stds (x as (_, T)) =
   3.100    let val thy = Proof_Context.theory_of ctxt in
   3.101      is_constr_like ctxt x andalso
   3.102 @@ -919,7 +925,13 @@
   3.103                         s of
   3.104         SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type ctxt T)) xs'
   3.105       | _ =>
   3.106 -       if is_datatype ctxt stds T then
   3.107 +       if is_frac_type ctxt T then
   3.108 +         case typedef_info ctxt s of
   3.109 +           SOME {abs_type, rep_type, Abs_name, ...} =>
   3.110 +           [(Abs_name,
   3.111 +             varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
   3.112 +         | NONE => [] (* impossible *)
   3.113 +       else if is_datatype ctxt stds T then
   3.114           case Datatype.get_info thy s of
   3.115             SOME {index, descr, ...} =>
   3.116             let
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu May 10 22:00:24 2012 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri May 11 00:45:24 2012 +0200
     4.3 @@ -574,7 +574,7 @@
     4.4                      |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
     4.5                      |> dest_n_tuple (length uncur_arg_Ts)
     4.6                  val t =
     4.7 -                  if constr_s = @{const_name Abs_Frac} then
     4.8 +                  if constr_s = @{const_name Nitpick.Abs_Frac} then
     4.9                      case ts of
    4.10                        [Const (@{const_name Pair}, _) $ t1 $ t2] =>
    4.11                        frac_from_term_pair (body_type T) t1 t2
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu May 10 22:00:24 2012 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Fri May 11 00:45:24 2012 +0200
     5.3 @@ -569,8 +569,8 @@
     5.4              Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
     5.5            else
     5.6              do_apply t0 ts
     5.7 -        | (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any)
     5.8 -        | (Const (@{const_name nat_lcm}, T), []) => Cst (Lcm, T, Any)
     5.9 +        | (Const (@{const_name Nitpick.nat_gcd}, T), []) => Cst (Gcd, T, Any)
    5.10 +        | (Const (@{const_name Nitpick.nat_lcm}, T), []) => Cst (Lcm, T, Any)
    5.11          | (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) =>
    5.12            if is_built_in_const thy stds x then
    5.13              let val num_T = domain_type T in
    5.14 @@ -586,8 +586,9 @@
    5.15          | (Const (@{const_name safe_The},
    5.16                    Type (@{type_name fun}, [_, T2])), [t1]) =>
    5.17            Op1 (SafeThe, T2, Any, sub t1)
    5.18 -        | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
    5.19 -        | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any)
    5.20 +        | (Const (@{const_name Nitpick.Frac}, T), []) => Cst (Fracs, T, Any)
    5.21 +        | (Const (@{const_name Nitpick.norm_frac}, T), []) =>
    5.22 +          Cst (NormFrac, T, Any)
    5.23          | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) =>
    5.24            Cst (NatToInt, T, Any)
    5.25          | (Const (@{const_name of_nat},
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu May 10 22:00:24 2012 +0200
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri May 11 00:45:24 2012 +0200
     6.3 @@ -45,9 +45,10 @@
     6.4        | aux def (t1 $ t2) = aux def t1 andalso aux def t2
     6.5        | aux def (t as Const (s, _)) =
     6.6          (not def orelse t <> @{const Suc}) andalso
     6.7 -        not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
     6.8 -                            @{const_name nat_gcd}, @{const_name nat_lcm},
     6.9 -                            @{const_name Frac}, @{const_name norm_frac}] s)
    6.10 +        not (member (op =)
    6.11 +               [@{const_name Nitpick.Abs_Frac}, @{const_name Nitpick.Rep_Frac},
    6.12 +                @{const_name Nitpick.nat_gcd}, @{const_name Nitpick.nat_lcm},
    6.13 +                @{const_name Nitpick.Frac}, @{const_name Nitpick.norm_frac}] s)
    6.14        | aux def (Abs (_, _, t')) = aux def t'
    6.15        | aux _ _ = true
    6.16    in aux end
    6.17 @@ -1061,10 +1062,12 @@
    6.18          (t = t' andalso is_sel_like_and_no_discr s andalso
    6.19           sel_no_from_name s = n)
    6.20        | is_nth_sel_on _ _ _ = false
    6.21 -    fun do_term (Const (@{const_name Rep_Frac}, _)
    6.22 -                 $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
    6.23 -      | do_term (Const (@{const_name Abs_Frac}, _)
    6.24 -                 $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
    6.25 +    fun do_term (Const (@{const_name Nitpick.Rep_Frac}, _)
    6.26 +                 $ (Const (@{const_name Nitpick.Abs_Frac}, _) $ t1)) [] =
    6.27 +        do_term t1 []
    6.28 +      | do_term (Const (@{const_name Nitpick.Abs_Frac}, _)
    6.29 +                 $ (Const (@{const_name Nitpick.Rep_Frac}, _) $ t1)) [] =
    6.30 +        do_term t1 []
    6.31        | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
    6.32        | do_term (t as Const (x as (s, T))) (args as _ :: _) =
    6.33          ((if is_constr_like ctxt x then
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu May 10 22:00:24 2012 +0200
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri May 11 00:45:24 2012 +0200
     7.3 @@ -450,7 +450,7 @@
     7.4        has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T
     7.5      fun is_concrete facto =
     7.6        is_word_type T orelse
     7.7 -      (* FIXME: looks wrong other types than just functions might be
     7.8 +      (* FIXME: looks wrong; other types than just functions might be
     7.9           abstract. "is_complete" is also suspicious. *)
    7.10        xs |> maps (binder_types o snd) |> maps binder_types
    7.11           |> forall (has_exact_card hol_ctxt facto finitizable_dataTs