1.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Aug 02 19:15:15 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Aug 03 01:16:08 2010 +0200
     1.3 @@ -8,9 +8,9 @@
     1.4  signature NITPICK_PREPROC =
     1.5  sig
     1.6    type hol_context = Nitpick_HOL.hol_context
     1.7 -  val preprocess_term :
     1.8 +  val preprocess_formulas :
     1.9      hol_context -> (typ option * bool option) list
    1.10 -    -> (typ option * bool option) list -> term
    1.11 +    -> (typ option * bool option) list -> term list -> term
    1.12      -> term list * term list * bool * bool * bool
    1.13  end;
    1.14  
    1.15 @@ -854,6 +854,26 @@
    1.16  
    1.17  (** Axiom selection **)
    1.18  
    1.19 +fun defined_free_by_assumption t =
    1.20 +  let
    1.21 +    fun do_equals t1 t2 =
    1.22 +      if exists_subterm (curry (op aconv) t1) t2 then NONE else SOME t1
    1.23 +  in
    1.24 +    case t of
    1.25 +      Const (@{const_name "=="}, _) $ (t1 as Free _) $ t2 => do_equals t1 t2
    1.26 +    | @{const Trueprop} $ (Const (@{const_name "=="}, _)
    1.27 +                           $ (t1 as Free _) $ t2) =>
    1.28 +      do_equals t1 t2
    1.29 +    | _ => NONE
    1.30 +  end
    1.31 +
    1.32 +fun assumption_exclusively_defines_free assm_ts t =
    1.33 +  case defined_free_by_assumption t of
    1.34 +    SOME t1 =>
    1.35 +    length (filter ((fn SOME t1' => t1 aconv t1' | NONE => false)
    1.36 +                     o defined_free_by_assumption) assm_ts) = 1
    1.37 +  | NONE => false
    1.38 +
    1.39  fun all_table_entries table = Symtab.fold (append o snd) table []
    1.40  fun extra_table table s = Symtab.make [(s, all_table_entries table)]
    1.41  
    1.42 @@ -868,13 +888,13 @@
    1.43  fun axioms_for_term
    1.44          (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
    1.45                        fast_descrs, evals, def_table, nondef_table,
    1.46 -                      choice_spec_table, user_nondefs, ...}) t =
    1.47 +                      choice_spec_table, user_nondefs, ...}) assm_ts neg_t =
    1.48    let
    1.49      type accumulator = styp list * (term list * term list)
    1.50      fun add_axiom get app depth t (accum as (xs, axs)) =
    1.51        let
    1.52          val t = t |> unfold_defs_in_term hol_ctxt
    1.53 -                  |> skolemize_term_and_more hol_ctxt ~1
    1.54 +                  |> skolemize_term_and_more hol_ctxt ~1 (*### why ~1? *)
    1.55        in
    1.56          if is_trivial_equation t then
    1.57            accum
    1.58 @@ -1008,15 +1028,21 @@
    1.59        List.partition (null o Term.hidden_polymorphism) user_nondefs
    1.60      val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
    1.61                             evals
    1.62 +    val (def_assm_ts, nondef_assm_ts) =
    1.63 +      List.partition (assumption_exclusively_defines_free assm_ts) assm_ts
    1.64      val (xs, (defs, nondefs)) =
    1.65 -      ([], ([], [])) |> add_axioms_for_term 1 t 
    1.66 -                     |> fold_rev (add_def_axiom 1) eval_axioms
    1.67 -                     |> user_axioms = SOME true
    1.68 -                        ? fold (add_nondef_axiom 1) mono_user_nondefs
    1.69 +      ([], ([], []))
    1.70 +      |> add_axioms_for_term 1 neg_t
    1.71 +      |> fold_rev (add_def_axiom 1) def_assm_ts
    1.72 +      |> fold_rev (add_nondef_axiom 1) nondef_assm_ts
    1.73 +      |> fold_rev (add_def_axiom 1) eval_axioms
    1.74 +      |> user_axioms = SOME true ? fold (add_nondef_axiom 1) mono_user_nondefs
    1.75      val defs = defs @ special_congruence_axioms hol_ctxt xs
    1.76      val got_all_mono_user_axioms =
    1.77        (user_axioms = SOME true orelse null mono_user_nondefs)
    1.78 -  in (t :: nondefs, defs, got_all_mono_user_axioms, null poly_user_nondefs) end
    1.79 +  in
    1.80 +    (neg_t :: nondefs, defs, got_all_mono_user_axioms, null poly_user_nondefs)
    1.81 +  end
    1.82  
    1.83  (** Simplification of constructor/selector terms **)
    1.84  
    1.85 @@ -1235,15 +1261,16 @@
    1.86  
    1.87  val max_skolem_depth = 3
    1.88  
    1.89 -fun preprocess_term (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs,
    1.90 -                                  boxes, ...}) finitizes monos t =
    1.91 +fun preprocess_formulas
    1.92 +        (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,
    1.93 +                      ...}) finitizes monos assm_ts neg_t =
    1.94    let
    1.95      val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
    1.96 -      t |> unfold_defs_in_term hol_ctxt
    1.97 -        |> close_form
    1.98 -        |> skolemize_term_and_more hol_ctxt max_skolem_depth
    1.99 -        |> specialize_consts_in_term hol_ctxt 0
   1.100 -        |> axioms_for_term hol_ctxt
   1.101 +      neg_t |> unfold_defs_in_term hol_ctxt
   1.102 +            |> close_form
   1.103 +            |> skolemize_term_and_more hol_ctxt max_skolem_depth
   1.104 +            |> specialize_consts_in_term hol_ctxt 0
   1.105 +            |> axioms_for_term hol_ctxt assm_ts
   1.106      val binarize =
   1.107        is_standard_datatype thy stds nat_T andalso
   1.108        case binary_ints of