tuned variable names of bindings; conceal predicate constants
authorhaftmann
Fri Oct 30 13:59:52 2009 +0100 (2009-10-30)
changeset 33360f7d9c5e5d2f9
parent 33359 8b673ae1bf39
child 33361 1f18de40b43f
tuned variable names of bindings; conceal predicate constants
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Oct 30 13:59:51 2009 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Oct 30 13:59:52 2009 +0100
     1.3 @@ -611,7 +611,7 @@
     1.4    else raise Match);
     1.5  
     1.6  (* define one predicate including its intro rule and axioms
     1.7 -   - bname: predicate name
     1.8 +   - binding: predicate name
     1.9     - parms: locale parameters
    1.10     - defs: thms representing substitutions from defines elements
    1.11     - ts: terms representing locale assumptions (not normalised wrt. defs)
    1.12 @@ -619,9 +619,9 @@
    1.13     - thy: the theory
    1.14  *)
    1.15  
    1.16 -fun def_pred bname parms defs ts norm_ts thy =
    1.17 +fun def_pred binding parms defs ts norm_ts thy =
    1.18    let
    1.19 -    val name = Sign.full_name thy bname;
    1.20 +    val name = Sign.full_name thy binding;
    1.21  
    1.22      val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
    1.23      val env = Term.add_free_names body [];
    1.24 @@ -639,9 +639,9 @@
    1.25      val ([pred_def], defs_thy) =
    1.26        thy
    1.27        |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
    1.28 -      |> Sign.declare_const ((bname, predT), NoSyn) |> snd
    1.29 +      |> Sign.declare_const ((Binding.conceal binding, predT), NoSyn) |> snd
    1.30        |> PureThy.add_defs false
    1.31 -        [((Binding.conceal (Binding.map_name Thm.def_name bname),
    1.32 +        [((Binding.conceal (Binding.map_name Thm.def_name binding),
    1.33              Logic.mk_equals (head, body)), [])];
    1.34      val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
    1.35  
    1.36 @@ -667,7 +667,7 @@
    1.37  
    1.38  (* main predicate definition function *)
    1.39  
    1.40 -fun define_preds pname parms (((exts, exts'), (ints, ints')), defs) thy =
    1.41 +fun define_preds binding parms (((exts, exts'), (ints, ints')), defs) thy =
    1.42    let
    1.43      val defs' = map (cterm_of thy #> Assumption.assume #> Drule.abs_def) defs;
    1.44  
    1.45 @@ -675,13 +675,13 @@
    1.46        if null exts then (NONE, NONE, [], thy)
    1.47        else
    1.48          let
    1.49 -          val aname = if null ints then pname else Binding.suffix_name ("_" ^ axiomsN) pname;
    1.50 +          val abinding = if null ints then binding else Binding.suffix_name ("_" ^ axiomsN) binding;
    1.51            val ((statement, intro, axioms), thy') =
    1.52              thy
    1.53 -            |> def_pred aname parms defs' exts exts';
    1.54 +            |> def_pred abinding parms defs' exts exts';
    1.55            val (_, thy'') =
    1.56              thy'
    1.57 -            |> Sign.mandatory_path (Binding.name_of aname)
    1.58 +            |> Sign.mandatory_path (Binding.name_of abinding)
    1.59              |> PureThy.note_thmss Thm.internalK
    1.60                [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])]
    1.61              ||> Sign.restore_naming thy';
    1.62 @@ -692,10 +692,10 @@
    1.63          let
    1.64            val ((statement, intro, axioms), thy''') =
    1.65              thy''
    1.66 -            |> def_pred pname parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
    1.67 +            |> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
    1.68            val (_, thy'''') =
    1.69              thy'''
    1.70 -            |> Sign.mandatory_path (Binding.name_of pname)
    1.71 +            |> Sign.mandatory_path (Binding.name_of binding)
    1.72              |> PureThy.note_thmss Thm.internalK
    1.73                   [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
    1.74                    ((Binding.conceal (Binding.name axiomsN), []),
    1.75 @@ -723,9 +723,9 @@
    1.76    | defines_to_notes _ e = e;
    1.77  
    1.78  fun gen_add_locale prep_decl
    1.79 -    bname raw_predicate_bname raw_import raw_body thy =
    1.80 +    binding raw_predicate_binding raw_import raw_body thy =
    1.81    let
    1.82 -    val name = Sign.full_name thy bname;
    1.83 +    val name = Sign.full_name thy binding;
    1.84      val _ = Locale.defined thy name andalso
    1.85        error ("Duplicate definition of locale " ^ quote name);
    1.86  
    1.87 @@ -733,17 +733,17 @@
    1.88        prep_decl raw_import I raw_body (ProofContext.init thy);
    1.89      val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
    1.90  
    1.91 -    val predicate_bname =
    1.92 -      if Binding.is_empty raw_predicate_bname then bname
    1.93 -      else raw_predicate_bname;
    1.94 +    val predicate_binding =
    1.95 +      if Binding.is_empty raw_predicate_binding then binding
    1.96 +      else raw_predicate_binding;
    1.97      val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
    1.98 -      define_preds predicate_bname parms text thy;
    1.99 +      define_preds predicate_binding parms text thy;
   1.100  
   1.101      val extraTs = subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
   1.102      val _ =
   1.103        if null extraTs then ()
   1.104        else warning ("Additional type variable(s) in locale specification " ^
   1.105 -        quote (Binding.str_of bname));
   1.106 +        quote (Binding.str_of binding));
   1.107  
   1.108      val a_satisfy = Element.satisfy_morphism a_axioms;
   1.109      val b_satisfy = Element.satisfy_morphism b_axioms;
   1.110 @@ -755,7 +755,7 @@
   1.111  
   1.112      val notes =
   1.113        if is_some asm then
   1.114 -        [(Thm.internalK, [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) bname), []),
   1.115 +        [(Thm.internalK, [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
   1.116            [([Assumption.assume (cterm_of thy' (the asm))],
   1.117              [(Attrib.internal o K) Locale.witness_add])])])]
   1.118        else [];
   1.119 @@ -772,7 +772,7 @@
   1.120      val axioms = map Element.conclude_witness b_axioms;
   1.121  
   1.122      val loc_ctxt = thy'
   1.123 -      |> Locale.register_locale bname (extraTs, params)
   1.124 +      |> Locale.register_locale binding (extraTs, params)
   1.125            (asm, rev defs) (a_intro, b_intro) axioms ([], []) (rev notes) (rev deps')
   1.126        |> TheoryTarget.init (SOME name)
   1.127        |> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes';