# HG changeset patch # User wenzelm # Date 1256743527 -3600 # Node ID ba9f52f56356b90441e771793bb2b64f67079946 # Parent 1bdc3c732fdd867b8c727ae5d8781392f1998362 conceal internal bindings; diff -r 1bdc3c732fdd -r ba9f52f56356 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Wed Oct 28 16:25:26 2009 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Wed Oct 28 16:25:27 2009 +0100 @@ -567,13 +567,16 @@ val rep_set_names'' = map (Sign.full_bname thy3) rep_set_names'; val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) = - Inductive.add_inductive_global (serial ()) + thy3 + |> Sign.map_naming Name_Space.conceal + |> Inductive.add_inductive_global (serial ()) {quiet_mode = false, verbose = false, kind = Thm.internalK, alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false} (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn)) (rep_set_names' ~~ recTs')) - [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy3; + [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] + ||> Sign.restore_naming thy3; (**** Prove that representing set is closed under permutation ****) @@ -1508,15 +1511,17 @@ ([], [], [], [], 0); val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) = - thy10 |> - Inductive.add_inductive_global (serial ()) + thy10 + |> Sign.map_naming Name_Space.conceal + |> Inductive.add_inductive_global (serial ()) {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK, alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) (map dest_Free rec_fns) - (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||> - PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct"); + (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] + ||> PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct") + ||> Sign.restore_naming thy10; (** equivariance **) diff -r 1bdc3c732fdd -r ba9f52f56356 src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Oct 28 16:25:26 2009 +0100 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Oct 28 16:25:27 2009 +0100 @@ -153,13 +153,17 @@ (descr' ~~ recTs ~~ rec_sets') ([], 0); val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) = - Inductive.add_inductive_global (serial ()) + thy0 + |> Sign.map_naming Name_Space.conceal + |> Inductive.add_inductive_global (serial ()) {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK, alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true, skip_mono = true, fork_mono = false} (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) (map dest_Free rec_fns) - (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] thy0; + (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] + ||> Sign.restore_naming thy0 + ||> Theory.checkpoint; (* prove uniqueness and termination of primrec combinators *) diff -r 1bdc3c732fdd -r ba9f52f56356 src/HOL/Tools/Datatype/datatype_rep_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Wed Oct 28 16:25:26 2009 +0100 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Wed Oct 28 16:25:27 2009 +0100 @@ -170,12 +170,16 @@ ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names'); val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) = - Inductive.add_inductive_global (serial ()) + thy1 + |> Sign.map_naming Name_Space.conceal + |> Inductive.add_inductive_global (serial ()) {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK, alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false} (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') [] - (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy1; + (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] + ||> Sign.restore_naming thy1 + ||> Theory.checkpoint; (********************************* typedef ********************************) diff -r 1bdc3c732fdd -r ba9f52f56356 src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Wed Oct 28 16:25:26 2009 +0100 +++ b/src/HOL/Tools/Function/function_core.ML Wed Oct 28 16:25:27 2009 +0100 @@ -488,7 +488,9 @@ |> Syntax.check_term lthy val ((f, (_, f_defthm)), lthy) = - LocalTheory.define Thm.internalK ((Binding.name (function_name fname), mixfix), ((Binding.name fdefname, []), f_def)) lthy + LocalTheory.define Thm.internalK + ((Binding.name (function_name fname), mixfix), + ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy in ((f, f_defthm), lthy) end diff -r 1bdc3c732fdd -r ba9f52f56356 src/HOL/Tools/Function/inductive_wrap.ML --- a/src/HOL/Tools/Function/inductive_wrap.ML Wed Oct 28 16:25:26 2009 +0100 +++ b/src/HOL/Tools/Function/inductive_wrap.ML Wed Oct 28 16:25:27 2009 +0100 @@ -39,7 +39,9 @@ fun inductive_def defs (((R, T), mixfix), lthy) = let val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) = - Inductive.add_inductive_i + lthy + |> LocalTheory.conceal + |> Inductive.add_inductive_i {quiet_mode = false, verbose = ! Toplevel.debug, kind = Thm.internalK, @@ -53,7 +55,7 @@ [] (* no parameters *) (map (fn t => (Attrib.empty_binding, t)) defs) (* the intros *) [] (* no special monos *) - lthy + ||> LocalTheory.restore_naming lthy val intrs = map2 (requantify lthy (R, T)) defs intrs_gen diff -r 1bdc3c732fdd -r ba9f52f56356 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Oct 28 16:25:26 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Oct 28 16:25:27 2009 +0100 @@ -368,14 +368,18 @@ if is_some (try (map (cterm_of thy)) intr_ts) then let val (ind_result, thy') = - Inductive.add_inductive_global (serial ()) + thy + |> Sign.map_naming Name_Space.conceal + |> Inductive.add_inductive_global (serial ()) {quiet_mode = false, verbose = false, kind = Thm.internalK, alt_name = Binding.empty, coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} - (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds))) + (map (fn (s, T) => + ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds))) pnames (map (fn x => (Attrib.empty_binding, x)) intr_ts) - [] thy + [] + ||> Sign.restore_naming thy val prednames = map (fst o dest_Const) (#preds ind_result) (* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#preds ind_result)) *) (* add constants to my table *) diff -r 1bdc3c732fdd -r ba9f52f56356 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Wed Oct 28 16:25:26 2009 +0100 +++ b/src/HOL/Tools/inductive.ML Wed Oct 28 16:25:27 2009 +0100 @@ -592,7 +592,7 @@ (** specification of (co)inductive predicates **) fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts monos params cnames_syn ctxt = - let + let (* FIXME proper naming convention: lthy *) val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp}; val argTs = fold (combine (op =) o arg_types_of (length params)) cs []; @@ -649,30 +649,37 @@ Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn)) else alt_name; - val ((rec_const, (_, fp_def)), ctxt') = ctxt |> - LocalTheory.define Thm.internalK + val ((rec_const, (_, fp_def)), ctxt') = ctxt + |> LocalTheory.conceal + |> LocalTheory.define Thm.internalK ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn), (Attrib.empty_binding, fold_rev lambda params - (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))); + (Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) + ||> LocalTheory.restore_naming ctxt; val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def]) (cterm_of (ProofContext.theory_of ctxt') (list_comb (rec_const, params))); - val specs = if length cs < 2 then [] else - map_index (fn (i, (name_mx, c)) => - let - val Ts = arg_types_of (length params) c; - val xs = map Free (Variable.variant_frees ctxt intr_ts - (mk_names "x" (length Ts) ~~ Ts)) - in - (name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs) - (list_comb (rec_const, params @ make_bool_args' bs i @ - make_args argTs (xs ~~ Ts))))) - end) (cnames_syn ~~ cs); - val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt'; + val specs = + if length cs < 2 then [] + else + map_index (fn (i, (name_mx, c)) => + let + val Ts = arg_types_of (length params) c; + val xs = map Free (Variable.variant_frees ctxt intr_ts + (mk_names "x" (length Ts) ~~ Ts)) + in + (name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs) + (list_comb (rec_const, params @ make_bool_args' bs i @ + make_args argTs (xs ~~ Ts))))) + end) (cnames_syn ~~ cs); + val (consts_defs, ctxt'') = ctxt' + |> LocalTheory.conceal + |> fold_map (LocalTheory.define Thm.internalK) specs + ||> LocalTheory.restore_naming ctxt'; val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs); val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt''; val ((_, [mono']), ctxt''') = - LocalTheory.note Thm.internalK (Attrib.empty_binding, [mono]) ctxt''; + LocalTheory.note Thm.internalK (apfst Binding.conceal Attrib.empty_binding, [mono]) ctxt''; in (ctxt''', rec_name, mono', fp_def', map (#2 o #2) consts_defs, list_comb (rec_const, params), preds, argTs, bs, xs) @@ -697,7 +704,8 @@ val (intrs', ctxt1) = ctxt |> LocalTheory.notes kind - (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ map (fn th => [([th], + (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ + map (fn th => [([th], [Attrib.internal (K (ContextRules.intro_query NONE)), Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>> map (hd o snd); diff -r 1bdc3c732fdd -r ba9f52f56356 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Wed Oct 28 16:25:26 2009 +0100 +++ b/src/HOL/Tools/inductive_set.ML Wed Oct 28 16:25:27 2009 +0100 @@ -407,7 +407,7 @@ fun add_ind_set_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono} cs intros monos params cnames_syn ctxt = - let + let (* FIXME proper naming convention: lthy *) val thy = ProofContext.theory_of ctxt; val {set_arities, pred_arities, to_pred_simps, ...} = PredSetConvData.get (Context.Proof ctxt); @@ -419,7 +419,8 @@ val new_arities = filter_out (fn (x as Free (_, T), _) => x mem params andalso length (binder_types T) > 1 | _ => false) (fold (snd #> infer) intros []); - val params' = map (fn x => (case AList.lookup op = new_arities x of + val params' = map (fn x => + (case AList.lookup op = new_arities x of SOME fs => let val T = HOLogic.dest_setT (fastype_of x); @@ -482,11 +483,14 @@ cs' intros' monos' params1 cnames_syn' ctxt; (* define inductive sets using previously defined predicates *) - val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK) - (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding, - fold_rev lambda params (HOLogic.Collect_const U $ - HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3)))))) - (cnames_syn ~~ cs_info ~~ preds)) ctxt1; + val (defs, ctxt2) = ctxt1 + |> LocalTheory.conceal (* FIXME ?? *) + |> fold_map (LocalTheory.define Thm.internalK) + (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding, + fold_rev lambda params (HOLogic.Collect_const U $ + HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3)))))) + (cnames_syn ~~ cs_info ~~ preds)) + ||> LocalTheory.restore_naming ctxt1; (* prove theorems for converting predicate to set notation *) val ctxt3 = fold diff -r 1bdc3c732fdd -r ba9f52f56356 src/HOL/Tools/recdef.ML --- a/src/HOL/Tools/recdef.ML Wed Oct 28 16:25:26 2009 +0100 +++ b/src/HOL/Tools/recdef.ML Wed Oct 28 16:25:27 2009 +0100 @@ -263,8 +263,9 @@ error ("No termination condition #" ^ string_of_int i ^ " in recdef definition of " ^ quote name); in - Specification.theorem Thm.internalK NONE (K I) (Binding.name bname, atts) - [] (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy + Specification.theorem Thm.internalK NONE (K I) + (Binding.conceal (Binding.name bname), atts) [] + (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy end; val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const; diff -r 1bdc3c732fdd -r ba9f52f56356 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Wed Oct 28 16:25:26 2009 +0100 +++ b/src/Pure/Isar/expression.ML Wed Oct 28 16:25:27 2009 +0100 @@ -641,7 +641,8 @@ |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], []) |> Sign.declare_const ((bname, predT), NoSyn) |> snd |> PureThy.add_defs false - [((Binding.map_name Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])]; + [((Binding.conceal (Binding.map_name Thm.def_name bname), Logic.mk_equals (head, body)), + [Thm.kind_internal])]; val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head; val cert = Thm.cterm_of defs_thy; @@ -682,7 +683,7 @@ thy' |> Sign.mandatory_path (Binding.name_of aname) |> PureThy.note_thmss Thm.internalK - [((Binding.name introN, []), [([intro], [Locale.unfold_add])])] + [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])] ||> Sign.restore_naming thy'; in (SOME statement, SOME intro, axioms, thy'') end; val (b_pred, b_intro, b_axioms, thy'''') = @@ -696,8 +697,8 @@ thy''' |> Sign.mandatory_path (Binding.name_of pname) |> PureThy.note_thmss Thm.internalK - [((Binding.name introN, []), [([intro], [Locale.intro_add])]), - ((Binding.name axiomsN, []), + [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]), + ((Binding.conceal (Binding.name axiomsN), []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])] ||> Sign.restore_naming thy'''; in (SOME statement, SOME intro, axioms, thy'''') end; @@ -753,10 +754,10 @@ val asm = if is_some b_statement then b_statement else a_statement; val notes = - if is_some asm - then [(Thm.internalK, [((Binding.suffix_name ("_" ^ axiomsN) bname, []), - [([Assumption.assume (cterm_of thy' (the asm))], - [(Attrib.internal o K) Locale.witness_add])])])] + if is_some asm then + [(Thm.internalK, [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) bname), []), + [([Assumption.assume (cterm_of thy' (the asm))], + [(Attrib.internal o K) Locale.witness_add])])])] else []; val notes' = body_elems |> diff -r 1bdc3c732fdd -r ba9f52f56356 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Wed Oct 28 16:25:26 2009 +0100 +++ b/src/Pure/Isar/locale.ML Wed Oct 28 16:25:27 2009 +0100 @@ -553,7 +553,8 @@ fun add_decls add loc decl = ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #> add_thmss loc Thm.internalK - [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])]; + [((Binding.conceal Binding.empty, [Attrib.internal (decl_attrib decl)]), + [([Drule.dummy_thm], [])])]; in diff -r 1bdc3c732fdd -r ba9f52f56356 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Wed Oct 28 16:25:26 2009 +0100 +++ b/src/Pure/axclass.ML Wed Oct 28 16:25:27 2009 +0100 @@ -311,7 +311,7 @@ (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const')) #>> Thm.varifyT #-> (fn thm => add_inst_param (c, tyco) (c'', thm) - #> PureThy.add_thm ((Binding.name c', thm), [Thm.kind_internal]) + #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [Thm.kind_internal]) #> snd #> Sign.restore_naming thy #> pair (Const (c, T))))