src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 42415 10accf397ab6
parent 42414 9465651c0db7
child 42418 508acf776ebf
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 19 12:22:59 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 19 14:04:58 2011 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4       case_names: (string * int) list,
     1.5       def_tables: const_table * const_table,
     1.6       nondef_table: const_table,
     1.7 -     user_nondefs: term list,
     1.8 +     nondefs: term list,
     1.9       simp_table: const_table Unsynchronized.ref,
    1.10       psimp_table: const_table,
    1.11       choice_spec_table: const_table,
    1.12 @@ -181,8 +181,8 @@
    1.13    val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
    1.14    val special_bounds : term list -> (indexname * typ) list
    1.15    val is_funky_typedef : Proof.context -> typ -> bool
    1.16 -  val all_axioms_of :
    1.17 -    Proof.context -> (term * term) list -> term list * term list * term list
    1.18 +  val all_defs_of : theory -> (term * term) list -> term list
    1.19 +  val all_nondefs_of : Proof.context -> (term * term) list -> term list
    1.20    val arity_of_built_in_const :
    1.21      theory -> (typ option * bool) list -> styp -> int option
    1.22    val is_built_in_const :
    1.23 @@ -267,7 +267,7 @@
    1.24     case_names: (string * int) list,
    1.25     def_tables: const_table * const_table,
    1.26     nondef_table: const_table,
    1.27 -   user_nondefs: term list,
    1.28 +   nondefs: term list,
    1.29     simp_table: const_table Unsynchronized.ref,
    1.30     psimp_table: const_table,
    1.31     choice_spec_table: const_table,
    1.32 @@ -1255,9 +1255,6 @@
    1.33    is_frac_type ctxt (Type (s, []))
    1.34  fun is_funky_typedef ctxt (Type (s, _)) = is_funky_typedef_name ctxt s
    1.35    | is_funky_typedef _ _ = false
    1.36 -fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
    1.37 -                         $ Const (@{const_name TYPE}, _)) = true
    1.38 -  | is_arity_type_axiom _ = false
    1.39  fun is_typedef_axiom ctxt boring (@{const "==>"} $ _ $ t2) =
    1.40      is_typedef_axiom ctxt boring t2
    1.41    | is_typedef_axiom ctxt boring
    1.42 @@ -1266,21 +1263,15 @@
    1.43           $ Const _ $ _)) =
    1.44      boring <> is_funky_typedef_name ctxt s andalso is_typedef ctxt s
    1.45    | is_typedef_axiom _ _ _ = false
    1.46 -val is_class_axiom =
    1.47 -  Logic.strip_horn #> swap #> op :: #> forall (can Logic.dest_of_class)
    1.48  
    1.49  (* Distinguishes between (1) constant definition axioms, (2) type arity and
    1.50     typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
    1.51     Typedef axioms are uninteresting to Nitpick, because it can retrieve them
    1.52     using "typedef_info". *)
    1.53 -fun partition_axioms_by_definitionality ctxt axioms def_names =
    1.54 -  let
    1.55 -    val axioms = sort (fast_string_ord o pairself fst) axioms
    1.56 -    val defs = Ord_List.inter (fast_string_ord o apsnd fst) def_names axioms
    1.57 -    val nondefs =
    1.58 -      Ord_List.subtract (fast_string_ord o apsnd fst) def_names axioms
    1.59 -      |> filter_out ((is_arity_type_axiom orf is_typedef_axiom ctxt true) o snd)
    1.60 -  in pairself (map snd) (defs, nondefs) end
    1.61 +fun filter_defs def_names =
    1.62 +  sort (fast_string_ord o pairself fst)
    1.63 +  #> Ord_List.inter (fast_string_ord o apsnd fst) def_names
    1.64 +  #> map snd
    1.65  
    1.66  (* Ideally we would check against "Complex_Main", not "Refute", but any theory
    1.67     will do as long as it contains all the "axioms" and "axiomatization"
    1.68 @@ -1302,36 +1293,32 @@
    1.69        | do_eq _ = false
    1.70    in do_eq end
    1.71  
    1.72 -fun all_axioms_of ctxt subst =
    1.73 +fun all_defs_of thy subst =
    1.74    let
    1.75 -    val thy = Proof_Context.theory_of ctxt
    1.76 -    val axioms_of_thys =
    1.77 -      maps Thm.axioms_of
    1.78 -      #> map (apsnd (subst_atomic subst o prop_of))
    1.79 -      #> filter_out (is_class_axiom o snd)
    1.80 -    val specs = Defs.all_specifications_of (Theory.defs_of thy)
    1.81 -    val def_names = specs |> maps snd |> map_filter #def
    1.82 -                    |> Ord_List.make fast_string_ord
    1.83 +    val def_names =
    1.84 +      thy |> Theory.defs_of
    1.85 +          |> Defs.all_specifications_of
    1.86 +          |> maps snd |> map_filter #def
    1.87 +          |> Ord_List.make fast_string_ord
    1.88      val thys = thy :: Theory.ancestors_of thy
    1.89 -    val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
    1.90 -    val built_in_axioms = axioms_of_thys built_in_thys
    1.91 -    val user_axioms = axioms_of_thys user_thys
    1.92 -    val (built_in_defs, built_in_nondefs) =
    1.93 -      partition_axioms_by_definitionality ctxt built_in_axioms def_names
    1.94 -      ||> filter (is_typedef_axiom ctxt false)
    1.95 -    val (user_defs, user_nondefs) =
    1.96 -      partition_axioms_by_definitionality ctxt user_axioms def_names
    1.97 -    val (built_in_nondefs, user_nondefs) =
    1.98 -      List.partition (is_typedef_axiom ctxt false) user_nondefs
    1.99 -      |>> append built_in_nondefs
   1.100 -    val defs =
   1.101 -      (thy |> Global_Theory.all_thms_of
   1.102 -           |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
   1.103 -           |> map (prop_of o snd)
   1.104 -           |> filter_out is_trivial_definition
   1.105 -           |> filter is_plain_definition) @
   1.106 -      user_defs @ built_in_defs
   1.107 -  in (defs, built_in_nondefs, user_nondefs) end
   1.108 +  in
   1.109 +    (* FIXME: avoid relying on "Thm.definitionK" *)
   1.110 +    (thy |> Global_Theory.all_thms_of
   1.111 +         |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
   1.112 +         |> map (subst_atomic subst o prop_of o snd)
   1.113 +         |> filter_out is_trivial_definition
   1.114 +         |> filter is_plain_definition) @
   1.115 +    (thys |> maps Thm.axioms_of
   1.116 +          |> map (apsnd (subst_atomic subst o prop_of))
   1.117 +          |> filter_defs def_names)
   1.118 +  end
   1.119 +
   1.120 +fun all_nondefs_of ctxt subst =
   1.121 +  ctxt |> Spec_Rules.get
   1.122 +       |> filter (curry (op =) Spec_Rules.Unknown o fst)
   1.123 +       |> maps (snd o snd)
   1.124 +       |> filter_out (is_built_in_theory o theory_of_thm)
   1.125 +       |> map (subst_atomic subst o prop_of)
   1.126  
   1.127  fun arity_of_built_in_const thy stds (s, T) =
   1.128    if s = @{const_name If} then