--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 06 11:33:58 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 06 11:35:10 2010 +0200
@@ -113,8 +113,8 @@
val dest_n_tuple : int -> term -> term list
val is_real_datatype : theory -> string -> bool
val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
+ val is_codatatype : theory -> typ -> bool
val is_quot_type : theory -> typ -> bool
- val is_codatatype : theory -> typ -> bool
val is_pure_typedef : Proof.context -> typ -> bool
val is_univ_typedef : Proof.context -> typ -> bool
val is_datatype : Proof.context -> (typ option * bool) list -> typ -> bool
@@ -640,17 +640,19 @@
in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
fun unregister_codatatype co_T = register_codatatype co_T "" []
-fun is_quot_type thy (Type (s, _)) =
- is_some (Quotient_Info.quotdata_lookup_raw thy s)
- | is_quot_type _ _ = false
fun is_codatatype thy (Type (s, _)) =
not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
|> Option.map snd |> these))
| is_codatatype _ _ = false
+fun is_real_quot_type thy (Type (s, _)) =
+ is_some (Quotient_Info.quotdata_lookup_raw thy s)
+ | is_real_quot_type _ _ = false
+fun is_quot_type thy T =
+ is_real_quot_type thy T andalso not (is_codatatype thy T)
fun is_pure_typedef ctxt (T as Type (s, _)) =
let val thy = ProofContext.theory_of ctxt in
is_typedef ctxt s andalso
- not (is_real_datatype thy s orelse is_quot_type thy T orelse
+ not (is_real_datatype thy s orelse is_real_quot_type thy T orelse
is_codatatype thy T orelse is_record_type T orelse
is_integer_like_type T)
end
@@ -681,7 +683,7 @@
fun is_datatype ctxt stds (T as Type (s, _)) =
let val thy = ProofContext.theory_of ctxt in
(is_typedef ctxt s orelse is_codatatype thy T orelse T = @{typ ind} orelse
- is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
+ is_real_quot_type thy T) andalso not (is_basic_datatype thy stds s)
end
| is_datatype _ _ _ = false
@@ -718,15 +720,19 @@
SOME {Rep_name, ...} => s = Rep_name
| NONE => false)
| is_rep_fun _ _ = false
-fun is_quot_abs_fun ctxt
- (x as (_, Type (@{type_name fun}, [_, Type (s', _)]))) =
- (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
- = SOME (Const x))
+fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun},
+ [_, abs_T as Type (s', _)]))) =
+ let val thy = ProofContext.theory_of ctxt in
+ (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
+ = SOME (Const x)) andalso not (is_codatatype thy abs_T)
+ end
| is_quot_abs_fun _ _ = false
-fun is_quot_rep_fun ctxt
- (x as (_, Type (@{type_name fun}, [Type (s', _), _]))) =
- (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s'
- = SOME (Const x))
+fun is_quot_rep_fun ctxt (x as (_, Type (@{type_name fun},
+ [abs_T as Type (s', _), _]))) =
+ let val thy = ProofContext.theory_of ctxt in
+ (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s'
+ = SOME (Const x)) andalso not (is_codatatype thy abs_T)
+ end
| is_quot_rep_fun _ _ = false
fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun},
@@ -913,7 +919,7 @@
val T' = (Record.get_extT_fields thy T
|> apsnd single |> uncurry append |> map snd) ---> T
in [(s', T')] end
- else if is_quot_type thy T then
+ else if is_real_quot_type thy T then
[(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
else case typedef_info ctxt s of
SOME {abs_type, rep_type, Abs_name, ...} =>
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 06 11:33:58 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 06 11:35:10 2010 +0200
@@ -960,31 +960,25 @@
fold (add_nondef_axiom depth)
(nondef_props_for_const thy true choice_spec_table x) accum
else if is_abs_fun ctxt x then
- if is_quot_type thy (range_type T) then
- accum
- else
- accum |> fold (add_nondef_axiom depth)
- (nondef_props_for_const thy false nondef_table x)
- |> (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
+ accum |> fold (add_nondef_axiom depth)
+ (nondef_props_for_const thy false nondef_table x)
+ |> (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)
else if is_rep_fun ctxt x then
- if is_quot_type thy (domain_type T) then
- accum
- else
- accum |> fold (add_nondef_axiom depth)
- (nondef_props_for_const thy false nondef_table x)
- |> (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
+ accum |> fold (add_nondef_axiom depth)
+ (nondef_props_for_const thy false nondef_table x)
+ |> (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)
- |> add_axioms_for_term depth
- (Const (mate_of_rep_fun ctxt x))
- |> fold (add_def_axiom depth)
- (inverse_axioms_for_rep_fun ctxt x)
+ |> add_axioms_for_term depth
+ (Const (mate_of_rep_fun ctxt x))
+ |> fold (add_def_axiom depth)
+ (inverse_axioms_for_rep_fun ctxt x)
else if s = @{const_name TYPE} then
accum
else case def_of_const thy def_table x of