src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 42418 508acf776ebf
parent 42415 10accf397ab6
child 42425 2aa907d5ee4f
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 19 14:04:58 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 19 14:38:38 2011 +0200
     1.3 @@ -1264,35 +1264,6 @@
     1.4      boring <> is_funky_typedef_name ctxt s andalso is_typedef ctxt s
     1.5    | is_typedef_axiom _ _ _ = false
     1.6  
     1.7 -(* Distinguishes between (1) constant definition axioms, (2) type arity and
     1.8 -   typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
     1.9 -   Typedef axioms are uninteresting to Nitpick, because it can retrieve them
    1.10 -   using "typedef_info". *)
    1.11 -fun filter_defs def_names =
    1.12 -  sort (fast_string_ord o pairself fst)
    1.13 -  #> Ord_List.inter (fast_string_ord o apsnd fst) def_names
    1.14 -  #> map snd
    1.15 -
    1.16 -(* Ideally we would check against "Complex_Main", not "Refute", but any theory
    1.17 -   will do as long as it contains all the "axioms" and "axiomatization"
    1.18 -   commands. *)
    1.19 -fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})
    1.20 -
    1.21 -val is_trivial_definition =
    1.22 -  the_default false o try (op aconv o Logic.dest_equals)
    1.23 -val is_plain_definition =
    1.24 -  let
    1.25 -    fun do_lhs t1 =
    1.26 -      case strip_comb t1 of
    1.27 -        (Const _, args) =>
    1.28 -        forall is_Var args andalso not (has_duplicates (op =) args)
    1.29 -      | _ => false
    1.30 -    fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
    1.31 -      | do_eq (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ _)) =
    1.32 -        do_lhs t1
    1.33 -      | do_eq _ = false
    1.34 -  in do_eq end
    1.35 -
    1.36  fun all_defs_of thy subst =
    1.37    let
    1.38      val def_names =
    1.39 @@ -1300,19 +1271,20 @@
    1.40            |> Defs.all_specifications_of
    1.41            |> maps snd |> map_filter #def
    1.42            |> Ord_List.make fast_string_ord
    1.43 -    val thys = thy :: Theory.ancestors_of thy
    1.44    in
    1.45 -    (* FIXME: avoid relying on "Thm.definitionK" *)
    1.46 -    (thy |> Global_Theory.all_thms_of
    1.47 -         |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
    1.48 -         |> map (subst_atomic subst o prop_of o snd)
    1.49 -         |> filter_out is_trivial_definition
    1.50 -         |> filter is_plain_definition) @
    1.51 -    (thys |> maps Thm.axioms_of
    1.52 -          |> map (apsnd (subst_atomic subst o prop_of))
    1.53 -          |> filter_defs def_names)
    1.54 +    thy :: Theory.ancestors_of thy
    1.55 +    |> maps Thm.axioms_of
    1.56 +    |> map (apsnd (subst_atomic subst o prop_of))
    1.57 +    |> sort (fast_string_ord o pairself fst)
    1.58 +    |> Ord_List.inter (fast_string_ord o apsnd fst) def_names
    1.59 +    |> map snd
    1.60    end
    1.61  
    1.62 +(* Ideally we would check against "Complex_Main", not "Refute", but any theory
    1.63 +   will do as long as it contains all the "axioms" and "axiomatization"
    1.64 +   commands. *)
    1.65 +fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})
    1.66 +
    1.67  fun all_nondefs_of ctxt subst =
    1.68    ctxt |> Spec_Rules.get
    1.69         |> filter (curry (op =) Spec_Rules.Unknown o fst)