conceal internal bindings;
authorwenzelm
Wed Oct 28 16:25:27 2009 +0100 (2009-10-28 ago)
changeset 33278ba9f52f56356
parent 33277 1bdc3c732fdd
child 33279 6b086276bbf7
conceal internal bindings;
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/inductive_wrap.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/recdef.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/locale.ML
src/Pure/axclass.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Oct 28 16:25:26 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Oct 28 16:25:27 2009 +0100
     1.3 @@ -567,13 +567,16 @@
     1.4      val rep_set_names'' = map (Sign.full_bname thy3) rep_set_names';
     1.5  
     1.6      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
     1.7 -        Inductive.add_inductive_global (serial ())
     1.8 +      thy3
     1.9 +      |> Sign.map_naming Name_Space.conceal
    1.10 +      |> Inductive.add_inductive_global (serial ())
    1.11            {quiet_mode = false, verbose = false, kind = Thm.internalK,
    1.12             alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
    1.13             skip_mono = true, fork_mono = false}
    1.14            (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
    1.15               (rep_set_names' ~~ recTs'))
    1.16 -          [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy3;
    1.17 +          [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
    1.18 +      ||> Sign.restore_naming thy3;
    1.19  
    1.20      (**** Prove that representing set is closed under permutation ****)
    1.21  
    1.22 @@ -1508,15 +1511,17 @@
    1.23            ([], [], [], [], 0);
    1.24  
    1.25      val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
    1.26 -      thy10 |>
    1.27 -        Inductive.add_inductive_global (serial ())
    1.28 +      thy10
    1.29 +      |> Sign.map_naming Name_Space.conceal
    1.30 +      |> Inductive.add_inductive_global (serial ())
    1.31            {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
    1.32             alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
    1.33             skip_mono = true, fork_mono = false}
    1.34            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    1.35            (map dest_Free rec_fns)
    1.36 -          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||>
    1.37 -      PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct");
    1.38 +          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
    1.39 +      ||> PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct")
    1.40 +      ||> Sign.restore_naming thy10;
    1.41  
    1.42      (** equivariance **)
    1.43  
     2.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Oct 28 16:25:26 2009 +0100
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Wed Oct 28 16:25:27 2009 +0100
     2.3 @@ -153,13 +153,17 @@
     2.4          (descr' ~~ recTs ~~ rec_sets') ([], 0);
     2.5  
     2.6      val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
     2.7 -        Inductive.add_inductive_global (serial ())
     2.8 +      thy0
     2.9 +      |> Sign.map_naming Name_Space.conceal
    2.10 +      |> Inductive.add_inductive_global (serial ())
    2.11            {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
    2.12              alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
    2.13              skip_mono = true, fork_mono = false}
    2.14            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    2.15            (map dest_Free rec_fns)
    2.16 -          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] thy0;
    2.17 +          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
    2.18 +      ||> Sign.restore_naming thy0
    2.19 +      ||> Theory.checkpoint;
    2.20  
    2.21      (* prove uniqueness and termination of primrec combinators *)
    2.22  
     3.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Wed Oct 28 16:25:26 2009 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Wed Oct 28 16:25:27 2009 +0100
     3.3 @@ -170,12 +170,16 @@
     3.4          ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names');
     3.5  
     3.6      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
     3.7 -        Inductive.add_inductive_global (serial ())
     3.8 +      thy1
     3.9 +      |> Sign.map_naming Name_Space.conceal
    3.10 +      |> Inductive.add_inductive_global (serial ())
    3.11            {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
    3.12             alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
    3.13             skip_mono = true, fork_mono = false}
    3.14            (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
    3.15 -          (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy1;
    3.16 +          (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
    3.17 +      ||> Sign.restore_naming thy1
    3.18 +      ||> Theory.checkpoint;
    3.19  
    3.20      (********************************* typedef ********************************)
    3.21  
     4.1 --- a/src/HOL/Tools/Function/function_core.ML	Wed Oct 28 16:25:26 2009 +0100
     4.2 +++ b/src/HOL/Tools/Function/function_core.ML	Wed Oct 28 16:25:27 2009 +0100
     4.3 @@ -488,7 +488,9 @@
     4.4                |> Syntax.check_term lthy
     4.5  
     4.6        val ((f, (_, f_defthm)), lthy) =
     4.7 -        LocalTheory.define Thm.internalK ((Binding.name (function_name fname), mixfix), ((Binding.name fdefname, []), f_def)) lthy
     4.8 +        LocalTheory.define Thm.internalK
     4.9 +          ((Binding.name (function_name fname), mixfix),
    4.10 +            ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
    4.11      in
    4.12        ((f, f_defthm), lthy)
    4.13      end
     5.1 --- a/src/HOL/Tools/Function/inductive_wrap.ML	Wed Oct 28 16:25:26 2009 +0100
     5.2 +++ b/src/HOL/Tools/Function/inductive_wrap.ML	Wed Oct 28 16:25:27 2009 +0100
     5.3 @@ -39,7 +39,9 @@
     5.4  fun inductive_def defs (((R, T), mixfix), lthy) =
     5.5      let
     5.6        val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
     5.7 -          Inductive.add_inductive_i
     5.8 +        lthy
     5.9 +        |> LocalTheory.conceal
    5.10 +        |> Inductive.add_inductive_i
    5.11              {quiet_mode = false,
    5.12                verbose = ! Toplevel.debug,
    5.13                kind = Thm.internalK,
    5.14 @@ -53,7 +55,7 @@
    5.15              [] (* no parameters *)
    5.16              (map (fn t => (Attrib.empty_binding, t)) defs) (* the intros *)
    5.17              [] (* no special monos *)
    5.18 -            lthy
    5.19 +        ||> LocalTheory.restore_naming lthy
    5.20  
    5.21        val intrs = map2 (requantify lthy (R, T)) defs intrs_gen
    5.22                    
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Oct 28 16:25:26 2009 +0100
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Oct 28 16:25:27 2009 +0100
     6.3 @@ -368,14 +368,18 @@
     6.4          if is_some (try (map (cterm_of thy)) intr_ts) then
     6.5            let
     6.6              val (ind_result, thy') =
     6.7 -              Inductive.add_inductive_global (serial ())
     6.8 +              thy
     6.9 +              |> Sign.map_naming Name_Space.conceal
    6.10 +              |> Inductive.add_inductive_global (serial ())
    6.11                  {quiet_mode = false, verbose = false, kind = Thm.internalK,
    6.12                    alt_name = Binding.empty, coind = false, no_elim = false,
    6.13                    no_ind = false, skip_mono = false, fork_mono = false}
    6.14 -                (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
    6.15 +                (map (fn (s, T) =>
    6.16 +                  ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
    6.17                  pnames
    6.18                  (map (fn x => (Attrib.empty_binding, x)) intr_ts)
    6.19 -                [] thy
    6.20 +                []
    6.21 +              ||> Sign.restore_naming thy
    6.22              val prednames = map (fst o dest_Const) (#preds ind_result)
    6.23              (* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#preds ind_result)) *)
    6.24              (* add constants to my table *)
     7.1 --- a/src/HOL/Tools/inductive.ML	Wed Oct 28 16:25:26 2009 +0100
     7.2 +++ b/src/HOL/Tools/inductive.ML	Wed Oct 28 16:25:27 2009 +0100
     7.3 @@ -592,7 +592,7 @@
     7.4  (** specification of (co)inductive predicates **)
     7.5  
     7.6  fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts monos params cnames_syn ctxt =
     7.7 -  let
     7.8 +  let  (* FIXME proper naming convention: lthy *)
     7.9      val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
    7.10  
    7.11      val argTs = fold (combine (op =) o arg_types_of (length params)) cs [];
    7.12 @@ -649,30 +649,37 @@
    7.13          Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
    7.14        else alt_name;
    7.15  
    7.16 -    val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
    7.17 -      LocalTheory.define Thm.internalK
    7.18 +    val ((rec_const, (_, fp_def)), ctxt') = ctxt
    7.19 +      |> LocalTheory.conceal
    7.20 +      |> LocalTheory.define Thm.internalK
    7.21          ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
    7.22           (Attrib.empty_binding, fold_rev lambda params
    7.23 -           (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
    7.24 +           (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
    7.25 +      ||> LocalTheory.restore_naming ctxt;
    7.26      val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
    7.27        (cterm_of (ProofContext.theory_of ctxt') (list_comb (rec_const, params)));
    7.28 -    val specs = if length cs < 2 then [] else
    7.29 -      map_index (fn (i, (name_mx, c)) =>
    7.30 -        let
    7.31 -          val Ts = arg_types_of (length params) c;
    7.32 -          val xs = map Free (Variable.variant_frees ctxt intr_ts
    7.33 -            (mk_names "x" (length Ts) ~~ Ts))
    7.34 -        in
    7.35 -          (name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs)
    7.36 -            (list_comb (rec_const, params @ make_bool_args' bs i @
    7.37 -              make_args argTs (xs ~~ Ts)))))
    7.38 -        end) (cnames_syn ~~ cs);
    7.39 -    val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt';
    7.40 +    val specs =
    7.41 +      if length cs < 2 then []
    7.42 +      else
    7.43 +        map_index (fn (i, (name_mx, c)) =>
    7.44 +          let
    7.45 +            val Ts = arg_types_of (length params) c;
    7.46 +            val xs = map Free (Variable.variant_frees ctxt intr_ts
    7.47 +              (mk_names "x" (length Ts) ~~ Ts))
    7.48 +          in
    7.49 +            (name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs)
    7.50 +              (list_comb (rec_const, params @ make_bool_args' bs i @
    7.51 +                make_args argTs (xs ~~ Ts)))))
    7.52 +          end) (cnames_syn ~~ cs);
    7.53 +    val (consts_defs, ctxt'') = ctxt'
    7.54 +      |> LocalTheory.conceal
    7.55 +      |> fold_map (LocalTheory.define Thm.internalK) specs
    7.56 +      ||> LocalTheory.restore_naming ctxt';
    7.57      val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
    7.58  
    7.59      val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt'';
    7.60      val ((_, [mono']), ctxt''') =
    7.61 -      LocalTheory.note Thm.internalK (Attrib.empty_binding, [mono]) ctxt'';
    7.62 +      LocalTheory.note Thm.internalK (apfst Binding.conceal Attrib.empty_binding, [mono]) ctxt'';
    7.63  
    7.64    in (ctxt''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
    7.65      list_comb (rec_const, params), preds, argTs, bs, xs)
    7.66 @@ -697,7 +704,8 @@
    7.67      val (intrs', ctxt1) =
    7.68        ctxt |>
    7.69        LocalTheory.notes kind
    7.70 -        (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
    7.71 +        (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
    7.72 +          map (fn th => [([th],
    7.73             [Attrib.internal (K (ContextRules.intro_query NONE)),
    7.74              Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>>
    7.75        map (hd o snd);
     8.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Oct 28 16:25:26 2009 +0100
     8.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Oct 28 16:25:27 2009 +0100
     8.3 @@ -407,7 +407,7 @@
     8.4  fun add_ind_set_def
     8.5      {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
     8.6      cs intros monos params cnames_syn ctxt =
     8.7 -  let
     8.8 +  let (* FIXME proper naming convention: lthy *)
     8.9      val thy = ProofContext.theory_of ctxt;
    8.10      val {set_arities, pred_arities, to_pred_simps, ...} =
    8.11        PredSetConvData.get (Context.Proof ctxt);
    8.12 @@ -419,7 +419,8 @@
    8.13      val new_arities = filter_out
    8.14        (fn (x as Free (_, T), _) => x mem params andalso length (binder_types T) > 1
    8.15          | _ => false) (fold (snd #> infer) intros []);
    8.16 -    val params' = map (fn x => (case AList.lookup op = new_arities x of
    8.17 +    val params' = map (fn x =>
    8.18 +      (case AList.lookup op = new_arities x of
    8.19          SOME fs =>
    8.20            let
    8.21              val T = HOLogic.dest_setT (fastype_of x);
    8.22 @@ -482,11 +483,14 @@
    8.23          cs' intros' monos' params1 cnames_syn' ctxt;
    8.24  
    8.25      (* define inductive sets using previously defined predicates *)
    8.26 -    val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
    8.27 -      (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
    8.28 -         fold_rev lambda params (HOLogic.Collect_const U $
    8.29 -           HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
    8.30 -         (cnames_syn ~~ cs_info ~~ preds)) ctxt1;
    8.31 +    val (defs, ctxt2) = ctxt1
    8.32 +      |> LocalTheory.conceal  (* FIXME ?? *)
    8.33 +      |> fold_map (LocalTheory.define Thm.internalK)
    8.34 +        (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
    8.35 +           fold_rev lambda params (HOLogic.Collect_const U $
    8.36 +             HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
    8.37 +           (cnames_syn ~~ cs_info ~~ preds))
    8.38 +      ||> LocalTheory.restore_naming ctxt1;
    8.39  
    8.40      (* prove theorems for converting predicate to set notation *)
    8.41      val ctxt3 = fold
     9.1 --- a/src/HOL/Tools/recdef.ML	Wed Oct 28 16:25:26 2009 +0100
     9.2 +++ b/src/HOL/Tools/recdef.ML	Wed Oct 28 16:25:27 2009 +0100
     9.3 @@ -263,8 +263,9 @@
     9.4        error ("No termination condition #" ^ string_of_int i ^
     9.5          " in recdef definition of " ^ quote name);
     9.6    in
     9.7 -    Specification.theorem Thm.internalK NONE (K I) (Binding.name bname, atts)
     9.8 -      [] (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
     9.9 +    Specification.theorem Thm.internalK NONE (K I)
    9.10 +      (Binding.conceal (Binding.name bname), atts) []
    9.11 +      (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
    9.12    end;
    9.13  
    9.14  val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const;
    10.1 --- a/src/Pure/Isar/expression.ML	Wed Oct 28 16:25:26 2009 +0100
    10.2 +++ b/src/Pure/Isar/expression.ML	Wed Oct 28 16:25:27 2009 +0100
    10.3 @@ -641,7 +641,8 @@
    10.4        |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
    10.5        |> Sign.declare_const ((bname, predT), NoSyn) |> snd
    10.6        |> PureThy.add_defs false
    10.7 -        [((Binding.map_name Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
    10.8 +        [((Binding.conceal (Binding.map_name Thm.def_name bname), Logic.mk_equals (head, body)),
    10.9 +          [Thm.kind_internal])];
   10.10      val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
   10.11  
   10.12      val cert = Thm.cterm_of defs_thy;
   10.13 @@ -682,7 +683,7 @@
   10.14              thy'
   10.15              |> Sign.mandatory_path (Binding.name_of aname)
   10.16              |> PureThy.note_thmss Thm.internalK
   10.17 -              [((Binding.name introN, []), [([intro], [Locale.unfold_add])])]
   10.18 +              [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])]
   10.19              ||> Sign.restore_naming thy';
   10.20            in (SOME statement, SOME intro, axioms, thy'') end;
   10.21      val (b_pred, b_intro, b_axioms, thy'''') =
   10.22 @@ -696,8 +697,8 @@
   10.23              thy'''
   10.24              |> Sign.mandatory_path (Binding.name_of pname)
   10.25              |> PureThy.note_thmss Thm.internalK
   10.26 -                 [((Binding.name introN, []), [([intro], [Locale.intro_add])]),
   10.27 -                  ((Binding.name axiomsN, []),
   10.28 +                 [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
   10.29 +                  ((Binding.conceal (Binding.name axiomsN), []),
   10.30                      [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
   10.31              ||> Sign.restore_naming thy''';
   10.32          in (SOME statement, SOME intro, axioms, thy'''') end;
   10.33 @@ -753,10 +754,10 @@
   10.34      val asm = if is_some b_statement then b_statement else a_statement;
   10.35  
   10.36      val notes =
   10.37 -      if is_some asm
   10.38 -      then [(Thm.internalK, [((Binding.suffix_name ("_" ^ axiomsN) bname, []),
   10.39 -        [([Assumption.assume (cterm_of thy' (the asm))],
   10.40 -          [(Attrib.internal o K) Locale.witness_add])])])]
   10.41 +      if is_some asm then
   10.42 +        [(Thm.internalK, [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) bname), []),
   10.43 +          [([Assumption.assume (cterm_of thy' (the asm))],
   10.44 +            [(Attrib.internal o K) Locale.witness_add])])])]
   10.45        else [];
   10.46  
   10.47      val notes' = body_elems |>
    11.1 --- a/src/Pure/Isar/locale.ML	Wed Oct 28 16:25:26 2009 +0100
    11.2 +++ b/src/Pure/Isar/locale.ML	Wed Oct 28 16:25:27 2009 +0100
    11.3 @@ -553,7 +553,8 @@
    11.4  fun add_decls add loc decl =
    11.5    ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
    11.6    add_thmss loc Thm.internalK
    11.7 -    [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
    11.8 +    [((Binding.conceal Binding.empty, [Attrib.internal (decl_attrib decl)]),
    11.9 +      [([Drule.dummy_thm], [])])];
   11.10  
   11.11  in
   11.12  
    12.1 --- a/src/Pure/axclass.ML	Wed Oct 28 16:25:26 2009 +0100
    12.2 +++ b/src/Pure/axclass.ML	Wed Oct 28 16:25:27 2009 +0100
    12.3 @@ -311,7 +311,7 @@
    12.4          (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
    12.5        #>> Thm.varifyT
    12.6        #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
    12.7 -      #> PureThy.add_thm ((Binding.name c', thm), [Thm.kind_internal])
    12.8 +      #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [Thm.kind_internal])
    12.9        #> snd
   12.10        #> Sign.restore_naming thy
   12.11        #> pair (Const (c, T))))