1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 06 11:33:58 2010 +0200
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Aug 06 11:35:10 2010 +0200
1.3 @@ -113,8 +113,8 @@
1.4 val dest_n_tuple : int -> term -> term list
1.5 val is_real_datatype : theory -> string -> bool
1.6 val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
1.7 + val is_codatatype : theory -> typ -> bool
1.8 val is_quot_type : theory -> typ -> bool
1.9 - val is_codatatype : theory -> typ -> bool
1.10 val is_pure_typedef : Proof.context -> typ -> bool
1.11 val is_univ_typedef : Proof.context -> typ -> bool
1.12 val is_datatype : Proof.context -> (typ option * bool) list -> typ -> bool
1.13 @@ -640,17 +640,19 @@
1.14 in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
1.15 fun unregister_codatatype co_T = register_codatatype co_T "" []
1.16
1.17 -fun is_quot_type thy (Type (s, _)) =
1.18 - is_some (Quotient_Info.quotdata_lookup_raw thy s)
1.19 - | is_quot_type _ _ = false
1.20 fun is_codatatype thy (Type (s, _)) =
1.21 not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
1.22 |> Option.map snd |> these))
1.23 | is_codatatype _ _ = false
1.24 +fun is_real_quot_type thy (Type (s, _)) =
1.25 + is_some (Quotient_Info.quotdata_lookup_raw thy s)
1.26 + | is_real_quot_type _ _ = false
1.27 +fun is_quot_type thy T =
1.28 + is_real_quot_type thy T andalso not (is_codatatype thy T)
1.29 fun is_pure_typedef ctxt (T as Type (s, _)) =
1.30 let val thy = ProofContext.theory_of ctxt in
1.31 is_typedef ctxt s andalso
1.32 - not (is_real_datatype thy s orelse is_quot_type thy T orelse
1.33 + not (is_real_datatype thy s orelse is_real_quot_type thy T orelse
1.34 is_codatatype thy T orelse is_record_type T orelse
1.35 is_integer_like_type T)
1.36 end
1.37 @@ -681,7 +683,7 @@
1.38 fun is_datatype ctxt stds (T as Type (s, _)) =
1.39 let val thy = ProofContext.theory_of ctxt in
1.40 (is_typedef ctxt s orelse is_codatatype thy T orelse T = @{typ ind} orelse
1.41 - is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
1.42 + is_real_quot_type thy T) andalso not (is_basic_datatype thy stds s)
1.43 end
1.44 | is_datatype _ _ _ = false
1.45
1.46 @@ -718,15 +720,19 @@
1.47 SOME {Rep_name, ...} => s = Rep_name
1.48 | NONE => false)
1.49 | is_rep_fun _ _ = false
1.50 -fun is_quot_abs_fun ctxt
1.51 - (x as (_, Type (@{type_name fun}, [_, Type (s', _)]))) =
1.52 - (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
1.53 - = SOME (Const x))
1.54 +fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun},
1.55 + [_, abs_T as Type (s', _)]))) =
1.56 + let val thy = ProofContext.theory_of ctxt in
1.57 + (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
1.58 + = SOME (Const x)) andalso not (is_codatatype thy abs_T)
1.59 + end
1.60 | is_quot_abs_fun _ _ = false
1.61 -fun is_quot_rep_fun ctxt
1.62 - (x as (_, Type (@{type_name fun}, [Type (s', _), _]))) =
1.63 - (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s'
1.64 - = SOME (Const x))
1.65 +fun is_quot_rep_fun ctxt (x as (_, Type (@{type_name fun},
1.66 + [abs_T as Type (s', _), _]))) =
1.67 + let val thy = ProofContext.theory_of ctxt in
1.68 + (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s'
1.69 + = SOME (Const x)) andalso not (is_codatatype thy abs_T)
1.70 + end
1.71 | is_quot_rep_fun _ _ = false
1.72
1.73 fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun},
1.74 @@ -913,7 +919,7 @@
1.75 val T' = (Record.get_extT_fields thy T
1.76 |> apsnd single |> uncurry append |> map snd) ---> T
1.77 in [(s', T')] end
1.78 - else if is_quot_type thy T then
1.79 + else if is_real_quot_type thy T then
1.80 [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
1.81 else case typedef_info ctxt s of
1.82 SOME {abs_type, rep_type, Abs_name, ...} =>
2.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 06 11:33:58 2010 +0200
2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Aug 06 11:35:10 2010 +0200
2.3 @@ -960,31 +960,25 @@
2.4 fold (add_nondef_axiom depth)
2.5 (nondef_props_for_const thy true choice_spec_table x) accum
2.6 else if is_abs_fun ctxt x then
2.7 - if is_quot_type thy (range_type T) then
2.8 - accum
2.9 - else
2.10 - accum |> fold (add_nondef_axiom depth)
2.11 - (nondef_props_for_const thy false nondef_table x)
2.12 - |> (is_funky_typedef thy (range_type T) orelse
2.13 - range_type T = nat_T)
2.14 - ? fold (add_maybe_def_axiom depth)
2.15 - (nondef_props_for_const thy true
2.16 + accum |> fold (add_nondef_axiom depth)
2.17 + (nondef_props_for_const thy false nondef_table x)
2.18 + |> (is_funky_typedef thy (range_type T) orelse
2.19 + range_type T = nat_T)
2.20 + ? fold (add_maybe_def_axiom depth)
2.21 + (nondef_props_for_const thy true
2.22 (extra_table def_table s) x)
2.23 else if is_rep_fun ctxt x then
2.24 - if is_quot_type thy (domain_type T) then
2.25 - accum
2.26 - else
2.27 - accum |> fold (add_nondef_axiom depth)
2.28 - (nondef_props_for_const thy false nondef_table x)
2.29 - |> (is_funky_typedef thy (range_type T) orelse
2.30 - range_type T = nat_T)
2.31 - ? fold (add_maybe_def_axiom depth)
2.32 - (nondef_props_for_const thy true
2.33 + accum |> fold (add_nondef_axiom depth)
2.34 + (nondef_props_for_const thy false nondef_table x)
2.35 + |> (is_funky_typedef thy (range_type T) orelse
2.36 + range_type T = nat_T)
2.37 + ? fold (add_maybe_def_axiom depth)
2.38 + (nondef_props_for_const thy true
2.39 (extra_table def_table s) x)
2.40 - |> add_axioms_for_term depth
2.41 - (Const (mate_of_rep_fun ctxt x))
2.42 - |> fold (add_def_axiom depth)
2.43 - (inverse_axioms_for_rep_fun ctxt x)
2.44 + |> add_axioms_for_term depth
2.45 + (Const (mate_of_rep_fun ctxt x))
2.46 + |> fold (add_def_axiom depth)
2.47 + (inverse_axioms_for_rep_fun ctxt x)
2.48 else if s = @{const_name TYPE} then
2.49 accum
2.50 else case def_of_const thy def_table x of