added support for "specification" and "ax_specification" constructs to Nitpick
authorblanchet
Wed Mar 17 09:14:43 2010 +0100 (2010-03-17)
changeset 35807e4d1b5cbd429
parent 35806 a814cccce0b8
child 35808 df56c1b1680f
child 35816 2449e026483d
added support for "specification" and "ax_specification" constructs to Nitpick
src/HOL/HOL.thy
src/HOL/Nitpick.thy
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/Tools/Nitpick/HISTORY
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
src/HOL/Tools/choice_specification.ML
     1.1 --- a/src/HOL/HOL.thy	Tue Mar 16 08:45:08 2010 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Mar 17 09:14:43 2010 +0100
     1.3 @@ -1999,8 +1999,6 @@
     1.4  
     1.5  subsubsection {* Nitpick setup *}
     1.6  
     1.7 -text {* This will be relocated once Nitpick is moved to HOL. *}
     1.8 -
     1.9  ML {*
    1.10  structure Nitpick_Defs = Named_Thms
    1.11  (
    1.12 @@ -2022,6 +2020,11 @@
    1.13    val name = "nitpick_intro"
    1.14    val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
    1.15  )
    1.16 +structure Nitpick_Choice_Specs = Named_Thms
    1.17 +(
    1.18 +  val name = "nitpick_choice_specs"
    1.19 +  val description = "choice specification of constants as needed by Nitpick"
    1.20 +)
    1.21  *}
    1.22  
    1.23  setup {*
    1.24 @@ -2029,6 +2032,7 @@
    1.25    #> Nitpick_Simps.setup
    1.26    #> Nitpick_Psimps.setup
    1.27    #> Nitpick_Intros.setup
    1.28 +  #> Nitpick_Choice_Specs.setup
    1.29  *}
    1.30  
    1.31  
     2.1 --- a/src/HOL/Nitpick.thy	Tue Mar 16 08:45:08 2010 +0100
     2.2 +++ b/src/HOL/Nitpick.thy	Wed Mar 17 09:14:43 2010 +0100
     2.3 @@ -1,6 +1,6 @@
     2.4  (*  Title:      HOL/Nitpick.thy
     2.5      Author:     Jasmin Blanchette, TU Muenchen
     2.6 -    Copyright   2008, 2009
     2.7 +    Copyright   2008, 2009, 2010
     2.8  
     2.9  Nitpick: Yet another counterexample generator for Isabelle/HOL.
    2.10  *)
     3.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Mar 16 08:45:08 2010 +0100
     3.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Mar 17 09:14:43 2010 +0100
     3.3 @@ -25,10 +25,11 @@
     3.4     fast_descrs = false, tac_timeout = NONE, evals = [], case_names = [],
     3.5     def_table = def_table, nondef_table = Symtab.empty, user_nondefs = [],
     3.6     simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty,
     3.7 -   intro_table = Symtab.empty, ground_thm_table = Inttab.empty,
     3.8 -   ersatz_table = [], skolems = Unsynchronized.ref [],
     3.9 -   special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
    3.10 -   wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
    3.11 +   choice_spec_table = Symtab.empty, intro_table = Symtab.empty,
    3.12 +   ground_thm_table = Inttab.empty, ersatz_table = [],
    3.13 +   skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
    3.14 +   unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
    3.15 +   constr_cache = Unsynchronized.ref []}
    3.16  (* term -> bool *)
    3.17  fun is_mono t = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} ([t], [])
    3.18  fun is_const t =
     4.1 --- a/src/HOL/Tools/Nitpick/HISTORY	Tue Mar 16 08:45:08 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Wed Mar 17 09:14:43 2010 +0100
     4.3 @@ -5,6 +5,7 @@
     4.4    * Added and implemented "finitize" option to improve the precision of infinite
     4.5      datatypes based on a monotonicity analysis
     4.6    * Added support for quotient types
     4.7 +  * Added support for "specification" and "ax_specification" constructs
     4.8    * Added support for local definitions (for "function" and "termination"
     4.9      proofs)
    4.10    * Added support for term postprocessors
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Mar 16 08:45:08 2010 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 17 09:14:43 2010 +0100
     5.3 @@ -276,6 +276,9 @@
     5.4      val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
     5.5      val simp_table = Unsynchronized.ref (const_simp_table ctxt subst)
     5.6      val psimp_table = const_psimp_table ctxt subst
     5.7 +    val choice_spec_table = const_choice_spec_table ctxt subst
     5.8 +    val user_nondefs =
     5.9 +      user_nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
    5.10      val intro_table = inductive_intro_table ctxt subst def_table
    5.11      val ground_thm_table = ground_theorem_table thy
    5.12      val ersatz_table = ersatz_table thy
    5.13 @@ -289,9 +292,9 @@
    5.14         case_names = case_names, def_table = def_table,
    5.15         nondef_table = nondef_table, user_nondefs = user_nondefs,
    5.16         simp_table = simp_table, psimp_table = psimp_table,
    5.17 -       intro_table = intro_table, ground_thm_table = ground_thm_table,
    5.18 -       ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
    5.19 -       special_funs = Unsynchronized.ref [],
    5.20 +       choice_spec_table = choice_spec_table, intro_table = intro_table,
    5.21 +       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
    5.22 +       skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
    5.23         unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
    5.24         constr_cache = Unsynchronized.ref []}
    5.25      val frees = Term.add_frees assms_t []
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Mar 16 08:45:08 2010 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Mar 17 09:14:43 2010 +0100
     6.3 @@ -37,6 +37,7 @@
     6.4      user_nondefs: term list,
     6.5      simp_table: const_table Unsynchronized.ref,
     6.6      psimp_table: const_table,
     6.7 +    choice_spec_table: const_table,
     6.8      intro_table: const_table,
     6.9      ground_thm_table: term list Inttab.table,
    6.10      ersatz_table: (string * string) list,
    6.11 @@ -180,6 +181,8 @@
    6.12    val const_nondef_table : term list -> const_table
    6.13    val const_simp_table : Proof.context -> (term * term) list -> const_table
    6.14    val const_psimp_table : Proof.context -> (term * term) list -> const_table
    6.15 +  val const_choice_spec_table :
    6.16 +    Proof.context -> (term * term) list -> const_table
    6.17    val inductive_intro_table :
    6.18      Proof.context -> (term * term) list -> const_table -> const_table
    6.19    val ground_theorem_table : theory -> term list Inttab.table
    6.20 @@ -197,6 +200,10 @@
    6.21    val is_equational_fun : hol_context -> styp -> bool
    6.22    val is_constr_pattern_lhs : theory -> term -> bool
    6.23    val is_constr_pattern_formula : theory -> term -> bool
    6.24 +  val nondef_props_for_const :
    6.25 +    theory -> bool -> const_table -> styp -> term list
    6.26 +  val is_choice_spec_fun : hol_context -> styp -> bool
    6.27 +  val is_choice_spec_axiom : theory -> const_table -> term -> bool
    6.28    val codatatype_bisim_axioms : hol_context -> typ -> term list
    6.29    val is_well_founded_inductive_pred : hol_context -> styp -> bool
    6.30    val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
    6.31 @@ -241,6 +248,7 @@
    6.32    user_nondefs: term list,
    6.33    simp_table: const_table Unsynchronized.ref,
    6.34    psimp_table: const_table,
    6.35 +  choice_spec_table: const_table,
    6.36    intro_table: const_table,
    6.37    ground_thm_table: term list Inttab.table,
    6.38    ersatz_table: (string * string) list,
    6.39 @@ -1441,18 +1449,6 @@
    6.40                   | NONE => t)
    6.41                 | t => t)
    6.42  
    6.43 -(* term -> string * term *)
    6.44 -fun pair_for_prop t =
    6.45 -  case term_under_def t of
    6.46 -    Const (s, _) => (s, t)
    6.47 -  | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
    6.48 -
    6.49 -(* (Proof.context -> term list) -> Proof.context -> (term * term) list
    6.50 -   -> const_table *)
    6.51 -fun table_for get ctxt subst =
    6.52 -  ctxt |> get |> map (pair_for_prop o subst_atomic subst)
    6.53 -       |> AList.group (op =) |> Symtab.make
    6.54 -
    6.55  (* theory -> (typ option * bool) list -> (string * int) list *)
    6.56  fun case_const_names thy stds =
    6.57    Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
    6.58 @@ -1514,6 +1510,67 @@
    6.59      SOME t' => is_constr_pattern_lhs thy t'
    6.60    | NONE => false
    6.61  
    6.62 +(* Similar to "Refute.specialize_type" but returns all matches rather than only
    6.63 +   the first (preorder) match. *)
    6.64 +(* theory -> styp -> term -> term list *)
    6.65 +fun multi_specialize_type thy slack (s, T) t =
    6.66 +  let
    6.67 +    (* term -> (typ * term) list -> (typ * term) list *)
    6.68 +    fun aux (Const (s', T')) ys =
    6.69 +        if s = s' then
    6.70 +          ys |> (if AList.defined (op =) ys T' then
    6.71 +                   I
    6.72 +                 else
    6.73 +                   cons (T', Refute.monomorphic_term
    6.74 +                                 (Sign.typ_match thy (T', T) Vartab.empty) t)
    6.75 +                   handle Type.TYPE_MATCH => I
    6.76 +                        | Refute.REFUTE _ =>
    6.77 +                          if slack then
    6.78 +                            I
    6.79 +                          else
    6.80 +                            raise NOT_SUPPORTED ("too much polymorphism in \
    6.81 +                                                 \axiom involving " ^ quote s))
    6.82 +        else
    6.83 +          ys
    6.84 +      | aux _ ys = ys
    6.85 +  in map snd (fold_aterms aux t []) end
    6.86 +(* theory -> bool -> const_table -> styp -> term list *)
    6.87 +fun nondef_props_for_const thy slack table (x as (s, _)) =
    6.88 +  these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
    6.89 +
    6.90 +(* term -> term *)
    6.91 +fun unvarify_term (t1 $ t2) = unvarify_term t1 $ unvarify_term t2
    6.92 +  | unvarify_term (Var ((s, 0), T)) = Free (s, T)
    6.93 +  | unvarify_term (Abs (s, T, t')) = Abs (s, T, unvarify_term t')
    6.94 +  | unvarify_term t = t
    6.95 +(* theory -> term -> term *)
    6.96 +fun axiom_for_choice_spec thy =
    6.97 +  unvarify_term
    6.98 +  #> Object_Logic.atomize_term thy
    6.99 +  #> Choice_Specification.close_form
   6.100 +  #> HOLogic.mk_Trueprop
   6.101 +(* hol_context -> styp -> bool *)
   6.102 +fun is_choice_spec_fun ({thy, def_table, nondef_table, choice_spec_table, ...}
   6.103 +                        : hol_context) x =
   6.104 +  case nondef_props_for_const thy true choice_spec_table x of
   6.105 +    [] => false
   6.106 +  | ts => case def_of_const thy def_table x of
   6.107 +            SOME (Const (@{const_name Eps}, _) $ _) => true
   6.108 +          | SOME _ => false
   6.109 +          | NONE =>
   6.110 +            let val ts' = nondef_props_for_const thy true nondef_table x in
   6.111 +              length ts' = length ts andalso
   6.112 +              forall (fn t =>
   6.113 +                         exists (curry (op aconv) (axiom_for_choice_spec thy t))
   6.114 +                                ts') ts
   6.115 +            end
   6.116 +
   6.117 +(* theory -> const_table -> term -> bool *)
   6.118 +fun is_choice_spec_axiom thy choice_spec_table t =
   6.119 +  Symtab.exists (fn (_, ts) =>
   6.120 +                    exists (curry (op aconv) t o axiom_for_choice_spec thy) ts)
   6.121 +                choice_spec_table
   6.122 +
   6.123  (** Constant unfolding **)
   6.124  
   6.125  (* theory -> (typ option * bool) list -> int * styp -> term *)
   6.126 @@ -1700,7 +1757,8 @@
   6.127                    else
   6.128                      (Const x, ts)
   6.129                  end
   6.130 -              else if is_equational_fun hol_ctxt x then
   6.131 +              else if is_equational_fun hol_ctxt x orelse
   6.132 +                      is_choice_spec_fun hol_ctxt x then
   6.133                  (Const x, ts)
   6.134                else case def_of_const thy def_table x of
   6.135                  SOME def =>
   6.136 @@ -1719,29 +1777,45 @@
   6.137  
   6.138  (** Axiom extraction/generation **)
   6.139  
   6.140 +(* term -> string * term *)
   6.141 +fun pair_for_prop t =
   6.142 +  case term_under_def t of
   6.143 +    Const (s, _) => (s, t)
   6.144 +  | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
   6.145 +(* (Proof.context -> term list) -> Proof.context -> (term * term) list
   6.146 +   -> const_table *)
   6.147 +fun def_table_for get ctxt subst =
   6.148 +  ctxt |> get |> map (pair_for_prop o subst_atomic subst)
   6.149 +       |> AList.group (op =) |> Symtab.make
   6.150 +(* term -> string * term *)
   6.151 +fun paired_with_consts t = map (rpair t) (Term.add_const_names t [])
   6.152  (* Proof.context -> (term * term) list -> term list -> const_table *)
   6.153  fun const_def_table ctxt subst ts =
   6.154 -  table_for (map prop_of o Nitpick_Defs.get) ctxt subst
   6.155 +  def_table_for (map prop_of o Nitpick_Defs.get) ctxt subst
   6.156    |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
   6.157            (map pair_for_prop ts)
   6.158  (* term list -> const_table *)
   6.159  fun const_nondef_table ts =
   6.160 -  fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts []
   6.161 -  |> AList.group (op =) |> Symtab.make
   6.162 +  fold (append o paired_with_consts) ts [] |> AList.group (op =) |> Symtab.make
   6.163  (* Proof.context -> (term * term) list -> const_table *)
   6.164 -val const_simp_table = table_for (map prop_of o Nitpick_Simps.get)
   6.165 -val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get)
   6.166 +val const_simp_table = def_table_for (map prop_of o Nitpick_Simps.get)
   6.167 +val const_psimp_table = def_table_for (map prop_of o Nitpick_Psimps.get)
   6.168 +fun const_choice_spec_table ctxt subst =
   6.169 +  map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
   6.170 +  |> const_nondef_table
   6.171  (* Proof.context -> (term * term) list -> const_table -> const_table *)
   6.172  fun inductive_intro_table ctxt subst def_table =
   6.173 -  table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
   6.174 -                                                  def_table o prop_of)
   6.175 -             o Nitpick_Intros.get) ctxt subst
   6.176 +  def_table_for
   6.177 +      (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
   6.178 +                                            def_table o prop_of)
   6.179 +           o Nitpick_Intros.get) ctxt subst
   6.180  (* theory -> term list Inttab.table *)
   6.181  fun ground_theorem_table thy =
   6.182    fold ((fn @{const Trueprop} $ t1 =>
   6.183              is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
   6.184            | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty
   6.185  
   6.186 +(* TODO: Move to "Nitpick.thy" *)
   6.187  val basic_ersatz_table =
   6.188    [(@{const_name prod_case}, @{const_name split}),
   6.189     (@{const_name card}, @{const_name card'}),
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Mar 16 08:45:08 2010 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Mar 17 09:14:43 2010 +0100
     7.3 @@ -917,9 +917,9 @@
     7.4                        debug, binary_ints, destroy_constrs, specialize,
     7.5                        skolemize, star_linear_preds, uncurry, fast_descrs,
     7.6                        tac_timeout, evals, case_names, def_table, nondef_table,
     7.7 -                      user_nondefs, simp_table, psimp_table, intro_table,
     7.8 -                      ground_thm_table, ersatz_table, skolems, special_funs,
     7.9 -                      unrolled_preds, wf_cache, constr_cache},
    7.10 +                      user_nondefs, simp_table, psimp_table, choice_spec_table,
    7.11 +                      intro_table, ground_thm_table, ersatz_table, skolems,
    7.12 +                      special_funs, unrolled_preds, wf_cache, constr_cache},
    7.13           binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
    7.14          formats all_frees free_names sel_names nonsel_names rel_table bounds =
    7.15    let
    7.16 @@ -936,10 +936,11 @@
    7.17         case_names = case_names, def_table = def_table,
    7.18         nondef_table = nondef_table, user_nondefs = user_nondefs,
    7.19         simp_table = simp_table, psimp_table = psimp_table,
    7.20 -       intro_table = intro_table, ground_thm_table = ground_thm_table,
    7.21 -       ersatz_table = ersatz_table, skolems = skolems,
    7.22 -       special_funs = special_funs, unrolled_preds = unrolled_preds,
    7.23 -       wf_cache = wf_cache, constr_cache = constr_cache}
    7.24 +       choice_spec_table = choice_spec_table, intro_table = intro_table,
    7.25 +       ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
    7.26 +       skolems = skolems, special_funs = special_funs,
    7.27 +       unrolled_preds = unrolled_preds, wf_cache = wf_cache,
    7.28 +       constr_cache = constr_cache}
    7.29      val scope = {hol_ctxt = hol_ctxt, binarize = binarize,
    7.30                   card_assigns = card_assigns, bits = bits,
    7.31                   bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Mar 16 08:45:08 2010 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Mar 17 09:14:43 2010 +0100
     8.3 @@ -938,35 +938,6 @@
     8.4  
     8.5  (** Axiom selection **)
     8.6  
     8.7 -(* Similar to "Refute.specialize_type" but returns all matches rather than only
     8.8 -   the first (preorder) match. *)
     8.9 -(* theory -> styp -> term -> term list *)
    8.10 -fun multi_specialize_type thy slack (s, T) t =
    8.11 -  let
    8.12 -    (* term -> (typ * term) list -> (typ * term) list *)
    8.13 -    fun aux (Const (s', T')) ys =
    8.14 -        if s = s' then
    8.15 -          ys |> (if AList.defined (op =) ys T' then
    8.16 -                   I
    8.17 -                 else
    8.18 -                  cons (T', Refute.monomorphic_term
    8.19 -                                (Sign.typ_match thy (T', T) Vartab.empty) t)
    8.20 -                  handle Type.TYPE_MATCH => I
    8.21 -                       | Refute.REFUTE _ =>
    8.22 -                         if slack then
    8.23 -                           I
    8.24 -                         else
    8.25 -                           raise NOT_SUPPORTED ("too much polymorphism in \
    8.26 -                                                \axiom involving " ^ quote s))
    8.27 -        else
    8.28 -          ys
    8.29 -      | aux _ ys = ys
    8.30 -  in map snd (fold_aterms aux t []) end
    8.31 -
    8.32 -(* theory -> bool -> const_table -> styp -> term list *)
    8.33 -fun nondef_props_for_const thy slack table (x as (s, _)) =
    8.34 -  these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
    8.35 -
    8.36  (* 'a Symtab.table -> 'a list *)
    8.37  fun all_table_entries table = Symtab.fold (append o snd) table []
    8.38  (* const_table -> string -> const_table *)
    8.39 @@ -985,8 +956,8 @@
    8.40  (* hol_context -> term -> term list * term list * bool * bool *)
    8.41  fun axioms_for_term
    8.42          (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
    8.43 -                      fast_descrs, evals, def_table, nondef_table, user_nondefs,
    8.44 -                      ...}) t =
    8.45 +                      fast_descrs, evals, def_table, nondef_table,
    8.46 +                      choice_spec_table, user_nondefs, ...}) t =
    8.47    let
    8.48      type accumulator = styp list * (term list * term list)
    8.49      (* (term list * term list -> term list)
    8.50 @@ -1047,6 +1018,9 @@
    8.51               else if is_equational_fun hol_ctxt x then
    8.52                 fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
    8.53                      accum
    8.54 +             else if is_choice_spec_fun hol_ctxt x then
    8.55 +               fold (add_nondef_axiom depth)
    8.56 +                    (nondef_props_for_const thy true choice_spec_table x) accum
    8.57               else if is_abs_fun thy x then
    8.58                 if is_quot_type thy (range_type T) then
    8.59                   raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Mar 16 08:45:08 2010 +0100
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed Mar 17 09:14:43 2010 +0100
     9.3 @@ -293,8 +293,9 @@
     9.4  (* string -> string *)
     9.5  fun maybe_quote y =
     9.6    let val s = unyxml y in
     9.7 -    y |> (not (is_long_identifier (perhaps (try (unprefix "'")) s)) orelse
     9.8 -          OuterKeyword.is_keyword s) ? quote
     9.9 +    y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
    9.10 +           not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
    9.11 +           OuterKeyword.is_keyword s) ? quote
    9.12    end
    9.13  
    9.14  end;
    10.1 --- a/src/HOL/Tools/choice_specification.ML	Tue Mar 16 08:45:08 2010 +0100
    10.2 +++ b/src/HOL/Tools/choice_specification.ML	Wed Mar 17 09:14:43 2010 +0100
    10.3 @@ -6,6 +6,7 @@
    10.4  
    10.5  signature CHOICE_SPECIFICATION =
    10.6  sig
    10.7 +  val close_form : term -> term
    10.8    val add_specification: string option -> (bstring * xstring * bool) list ->
    10.9      theory * thm -> theory * thm
   10.10  end
   10.11 @@ -15,6 +16,10 @@
   10.12  
   10.13  (* actual code *)
   10.14  
   10.15 +fun close_form t =
   10.16 +    fold_rev (fn (s, T) => fn t => HOLogic.mk_all (s, T, t))
   10.17 +             (map dest_Free (OldTerm.term_frees t)) t
   10.18 +
   10.19  local
   10.20      fun mk_definitional [] arg = arg
   10.21        | mk_definitional ((thname,cname,covld)::cos) (thy,thm) =
   10.22 @@ -120,8 +125,7 @@
   10.23                  val frees = OldTerm.term_frees prop
   10.24                  val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
   10.25                    orelse error "Specificaton: Only free variables of sort 'type' allowed"
   10.26 -                val prop_closed = fold_rev (fn (vname, T) => fn prop =>
   10.27 -                  HOLogic.mk_all (vname, T, prop)) (map dest_Free frees) prop
   10.28 +                val prop_closed = close_form prop
   10.29              in
   10.30                  (prop_closed,frees)
   10.31              end
   10.32 @@ -190,7 +194,8 @@
   10.33                          args |> apsnd (remove_alls frees)
   10.34                               |> apsnd undo_imps
   10.35                               |> apsnd Drule.export_without_context
   10.36 -                             |> Thm.theory_attributes (map (Attrib.attribute thy) atts)
   10.37 +                             |> Thm.theory_attributes (map (Attrib.attribute thy)
   10.38 +                                                           (Attrib.internal (K Nitpick_Choice_Specs.add) :: atts))
   10.39                               |> add_final
   10.40                               |> Library.swap
   10.41                      end