1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Nov 23 14:34:05 2009 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Nov 23 17:26:32 2009 +0100
1.3 @@ -514,10 +514,12 @@
1.4 set_name = set_prefix ^ s, Rep_inverse = SOME Rep_inverse}
1.5 | NONE => NONE
1.6
1.7 +(* FIXME: use antiquotation for "code_numeral" below or detect "rep_datatype",
1.8 + e.g., by adding a field to "DatatypeAux.info". *)
1.9 (* string -> bool *)
1.10 fun is_basic_datatype s =
1.11 s mem [@{type_name "*"}, @{type_name bool}, @{type_name unit},
1.12 - @{type_name nat}, @{type_name int}]
1.13 + @{type_name nat}, @{type_name int}, "Code_Numeral.code_numeral"]
1.14 (* theory -> string -> bool *)
1.15 val is_typedef = is_some oo typedef_info
1.16 val is_real_datatype = is_some oo Datatype.get_info
1.17 @@ -539,7 +541,7 @@
1.18 try (fst o dest_Const o snd o Logic.dest_equals o prop_of) thm
1.19 | NONE =>
1.20 try (fst o dest_Const o snd o HOLogic.dest_mem
1.21 - o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name UNIV}
1.22 + o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top}
1.23 | NONE => false)
1.24 | is_univ_typedef _ _ = false
1.25 fun is_datatype thy (T as Type (s, _)) =
1.26 @@ -1288,8 +1290,10 @@
1.27 end
1.28 (* theory -> styp -> term *)
1.29 fun inverse_axiom_for_rep_fun thy (x as (_, T)) =
1.30 - typedef_info thy (fst (dest_Type (domain_type T)))
1.31 - |> the |> #Rep_inverse |> the |> prop_of |> Refute.specialize_type thy x
1.32 + let val abs_T = domain_type T in
1.33 + typedef_info thy (fst (dest_Type abs_T)) |> the |> #Rep_inverse |> the
1.34 + |> prop_of |> Refute.specialize_type thy x
1.35 + end
1.36
1.37 (* theory -> int * styp -> term *)
1.38 fun constr_case_body thy (j, (x as (_, T))) =
1.39 @@ -1404,6 +1408,7 @@
1.40 | _ => NONE
1.41 (* theory -> term -> bool *)
1.42 fun is_constr_pattern _ (Bound _) = true
1.43 + | is_constr_pattern _ (Var _) = true
1.44 | is_constr_pattern thy t =
1.45 case strip_comb t of
1.46 (Const (x as (s, _)), args) =>
1.47 @@ -1445,7 +1450,7 @@
1.48 else
1.49 raise SAME ())
1.50 handle SAME () => betapply (do_term depth Ts t0, do_term depth Ts t1))
1.51 - | Const (@{const_name refl_on}, T) $ Const (@{const_name UNIV}, _) $ t2 =>
1.52 + | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
1.53 do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
1.54 | (t0 as Const (x as (@{const_name Sigma}, T))) $ t1
1.55 $ (t2 as Abs (_, _, t2')) =>
1.56 @@ -1492,7 +1497,7 @@
1.57 if is_finite_type ext_ctxt (domain_type T) then
1.58 (Abs ("A", domain_type T, @{const True}), ts)
1.59 else case ts of
1.60 - [Const (@{const_name UNIV}, _)] => (@{const False}, [])
1.61 + [Const (@{const_name top}, _)] => (@{const False}, [])
1.62 | _ => (Const x, ts)
1.63 else
1.64 (Const x, ts)
1.65 @@ -3004,10 +3009,14 @@
1.66 end
1.67 end
1.68 (* int -> term -> accumulator -> accumulator *)
1.69 + and add_def_axiom depth = add_axiom fst apfst depth
1.70 and add_nondef_axiom depth = add_axiom snd apsnd depth
1.71 - and add_def_axiom depth t =
1.72 - (if head_of t = @{const "==>"} then add_nondef_axiom
1.73 - else add_axiom fst apfst) depth t
1.74 + and add_maybe_def_axiom depth t =
1.75 + (if head_of t <> @{const "==>"} then add_def_axiom
1.76 + else add_nondef_axiom) depth t
1.77 + and add_eq_axiom depth t =
1.78 + (if is_constr_pattern_formula thy t then add_def_axiom
1.79 + else add_nondef_axiom) depth t
1.80 (* int -> term -> accumulator -> accumulator *)
1.81 and add_axioms_for_term depth t (accum as (xs, axs)) =
1.82 case t of
1.83 @@ -3029,29 +3038,33 @@
1.84 val ax1 = try (Refute.specialize_type thy x) of_class
1.85 val ax2 = Option.map (Refute.specialize_type thy x o snd)
1.86 (Refute.get_classdef thy class)
1.87 - in fold (add_def_axiom depth) (map_filter I [ax1, ax2]) accum end
1.88 + in
1.89 + fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
1.90 + accum
1.91 + end
1.92 else if is_constr thy x then
1.93 accum
1.94 else if is_equational_fun ext_ctxt x then
1.95 - fold (add_def_axiom depth) (equational_fun_axioms ext_ctxt x)
1.96 + fold (add_eq_axiom depth) (equational_fun_axioms ext_ctxt x)
1.97 accum
1.98 else if is_abs_fun thy x then
1.99 accum |> fold (add_nondef_axiom depth)
1.100 (nondef_props_for_const thy false nondef_table x)
1.101 |> is_funky_typedef thy (range_type T)
1.102 - ? fold (add_def_axiom depth)
1.103 + ? fold (add_maybe_def_axiom depth)
1.104 (nondef_props_for_const thy true
1.105 (extra_table def_table s) x)
1.106 else if is_rep_fun thy x then
1.107 accum |> fold (add_nondef_axiom depth)
1.108 (nondef_props_for_const thy false nondef_table x)
1.109 |> is_funky_typedef thy (range_type T)
1.110 - ? fold (add_def_axiom depth)
1.111 + ? fold (add_maybe_def_axiom depth)
1.112 (nondef_props_for_const thy true
1.113 (extra_table def_table s) x)
1.114 |> add_axioms_for_term depth
1.115 (Const (mate_of_rep_fun thy x))
1.116 - |> add_def_axiom depth (inverse_axiom_for_rep_fun thy x)
1.117 + |> add_maybe_def_axiom depth
1.118 + (inverse_axiom_for_rep_fun thy x)
1.119 else
1.120 accum |> user_axioms <> SOME false
1.121 ? fold (add_nondef_axiom depth)
1.122 @@ -3076,9 +3089,10 @@
1.123 | Type (z as (_, Ts)) =>
1.124 fold (add_axioms_for_type depth) Ts
1.125 #> (if is_pure_typedef thy T then
1.126 - fold (add_def_axiom depth) (optimized_typedef_axioms thy z)
1.127 + fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
1.128 else if max_bisim_depth >= 0 andalso is_codatatype thy T then
1.129 - fold (add_def_axiom depth) (codatatype_bisim_axioms ext_ctxt T)
1.130 + fold (add_maybe_def_axiom depth)
1.131 + (codatatype_bisim_axioms ext_ctxt T)
1.132 else
1.133 I)
1.134 (* int -> typ -> sort -> accumulator -> accumulator *)