src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 35335 f715cfde056a
parent 35332 22442ab3e7a3
child 35384 88dbcfe75c45
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Feb 23 16:53:13 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Feb 23 19:10:25 2010 +0100
     1.3 @@ -155,7 +155,8 @@
     1.4    val is_finite_type : hol_context -> typ -> bool
     1.5    val special_bounds : term list -> (indexname * typ) list
     1.6    val is_funky_typedef : theory -> typ -> bool
     1.7 -  val all_axioms_of : theory -> term list * term list * term list
     1.8 +  val all_axioms_of :
     1.9 +    theory -> (term * term) list -> term list * term list * term list
    1.10    val arity_of_built_in_const :
    1.11      theory -> (typ option * bool) list -> bool -> styp -> int option
    1.12    val is_built_in_const :
    1.13 @@ -163,11 +164,13 @@
    1.14    val term_under_def : term -> term
    1.15    val case_const_names :
    1.16      theory -> (typ option * bool) list -> (string * int) list
    1.17 -  val const_def_table : Proof.context -> term list -> const_table
    1.18 +  val const_def_table :
    1.19 +    Proof.context -> (term * term) list -> term list -> const_table
    1.20    val const_nondef_table : term list -> const_table
    1.21 -  val const_simp_table : Proof.context -> const_table
    1.22 -  val const_psimp_table : Proof.context -> const_table
    1.23 -  val inductive_intro_table : Proof.context -> const_table -> const_table
    1.24 +  val const_simp_table : Proof.context -> (term * term) list -> const_table
    1.25 +  val const_psimp_table : Proof.context -> (term * term) list -> const_table
    1.26 +  val inductive_intro_table :
    1.27 +    Proof.context -> (term * term) list -> const_table -> const_table
    1.28    val ground_theorem_table : theory -> term list Inttab.table
    1.29    val ersatz_table : theory -> (string * string) list
    1.30    val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
    1.31 @@ -1173,11 +1176,12 @@
    1.32        | do_eq _ = false
    1.33    in do_eq end
    1.34  
    1.35 -(* theory -> term list * term list * term list *)
    1.36 -fun all_axioms_of thy =
    1.37 +(* theory -> (term * term) list -> term list * term list * term list *)
    1.38 +fun all_axioms_of thy subst =
    1.39    let
    1.40      (* theory list -> term list *)
    1.41 -    val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of)
    1.42 +    val axioms_of_thys =
    1.43 +      maps Thm.axioms_of #> map (apsnd (subst_atomic subst o prop_of))
    1.44      val specs = Defs.all_specifications_of (Theory.defs_of thy)
    1.45      val def_names = specs |> maps snd |> map_filter #def
    1.46                      |> OrdList.make fast_string_ord
    1.47 @@ -1324,12 +1328,13 @@
    1.48  fun pair_for_prop t =
    1.49    case term_under_def t of
    1.50      Const (s, _) => (s, t)
    1.51 -  | Free _ => raise NOT_SUPPORTED "local definitions"
    1.52    | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
    1.53  
    1.54 -(* (Proof.context -> term list) -> Proof.context -> const_table *)
    1.55 -fun table_for get ctxt =
    1.56 -  get ctxt |> map pair_for_prop |> AList.group (op =) |> Symtab.make
    1.57 +(* (Proof.context -> term list) -> Proof.context -> (term * term) list
    1.58 +   -> const_table *)
    1.59 +fun table_for get ctxt subst =
    1.60 +  ctxt |> get |> map (pair_for_prop o subst_atomic subst)
    1.61 +       |> AList.group (op =) |> Symtab.make
    1.62  
    1.63  (* theory -> (typ option * bool) list -> (string * int) list *)
    1.64  fun case_const_names thy stds =
    1.65 @@ -1342,23 +1347,23 @@
    1.66                (Datatype.get_all thy) [] @
    1.67    map (apsnd length o snd) (#codatatypes (Data.get thy))
    1.68  
    1.69 -(* Proof.context -> term list -> const_table *)
    1.70 -fun const_def_table ctxt ts =
    1.71 -  table_for (map prop_of o Nitpick_Defs.get) ctxt
    1.72 +(* Proof.context -> (term * term) list -> term list -> const_table *)
    1.73 +fun const_def_table ctxt subst ts =
    1.74 +  table_for (map prop_of o Nitpick_Defs.get) ctxt subst
    1.75    |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
    1.76            (map pair_for_prop ts)
    1.77  (* term list -> const_table *)
    1.78  fun const_nondef_table ts =
    1.79    fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts []
    1.80    |> AList.group (op =) |> Symtab.make
    1.81 -(* Proof.context -> const_table *)
    1.82 +(* Proof.context -> (term * term) list -> const_table *)
    1.83  val const_simp_table = table_for (map prop_of o Nitpick_Simps.get)
    1.84  val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get)
    1.85 -(* Proof.context -> const_table -> const_table *)
    1.86 -fun inductive_intro_table ctxt def_table =
    1.87 +(* Proof.context -> (term * term) list -> const_table -> const_table *)
    1.88 +fun inductive_intro_table ctxt subst def_table =
    1.89    table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
    1.90                                                    def_table o prop_of)
    1.91 -             o Nitpick_Intros.get) ctxt
    1.92 +             o Nitpick_Intros.get) ctxt subst
    1.93  (* theory -> term list Inttab.table *)
    1.94  fun ground_theorem_table thy =
    1.95    fold ((fn @{const Trueprop} $ t1 =>