Preserve idents (expression in sublocale).
authorballarin
Wed Dec 10 16:30:33 2008 +0100 (2008-12-10)
changeset 2920662dc8762ec00
parent 29036 df1113d916db
child 29207 a91012d9db21
Preserve idents (expression in sublocale).
src/FOL/ex/NewLocaleTest.thy
src/Pure/Isar/expression.ML
src/Pure/Isar/new_locale.ML
     1.1 --- a/src/FOL/ex/NewLocaleTest.thy	Wed Dec 10 14:45:15 2008 +0100
     1.2 +++ b/src/FOL/ex/NewLocaleTest.thy	Wed Dec 10 16:30:33 2008 +0100
     1.3 @@ -10,7 +10,6 @@
     1.4  
     1.5  ML_val {* set new_locales *}
     1.6  ML_val {* set Toplevel.debug *}
     1.7 -ML_val {* set show_hyps *}
     1.8  
     1.9  
    1.10  typedecl int arities int :: "term"
    1.11 @@ -24,7 +23,7 @@
    1.12    int_minus: "(-x) + x = 0"
    1.13    int_minus2: "-(-x) = x"
    1.14  
    1.15 -text {* Inference of parameter types *}
    1.16 +section {* Inference of parameter types *}
    1.17  
    1.18  locale param1 = fixes p
    1.19  print_locale! param1
    1.20 @@ -44,7 +43,7 @@
    1.21  print_locale! param4
    1.22  
    1.23  
    1.24 -text {* Incremental type constraints *}
    1.25 +subsection {* Incremental type constraints *}
    1.26  
    1.27  locale constraint1 =
    1.28    fixes  prod (infixl "**" 65)
    1.29 @@ -58,7 +57,7 @@
    1.30  print_locale! constraint2
    1.31  
    1.32  
    1.33 -text {* Inheritance *}
    1.34 +section {* Inheritance *}
    1.35  
    1.36  locale semi =
    1.37    fixes prod (infixl "**" 65)
    1.38 @@ -94,7 +93,7 @@
    1.39  print_locale! pert_hom' thm pert_hom'_def
    1.40  
    1.41  
    1.42 -text {* Syntax declarations *}
    1.43 +section {* Syntax declarations *}
    1.44  
    1.45  locale logic =
    1.46    fixes land (infixl "&&" 55)
    1.47 @@ -113,13 +112,13 @@
    1.48  print_locale! use_decl thm use_decl_def
    1.49  
    1.50  
    1.51 -text {* Foundational versions of theorems *}
    1.52 +section {* Foundational versions of theorems *}
    1.53  
    1.54  thm logic.assoc
    1.55  thm logic.lor_def
    1.56  
    1.57  
    1.58 -text {* Defines *}
    1.59 +section {* Defines *}
    1.60  
    1.61  locale logic_def =
    1.62    fixes land (infixl "&&" 55)
    1.63 @@ -149,7 +148,7 @@
    1.64  end
    1.65  
    1.66  
    1.67 -text {* Notes *}
    1.68 +section {* Notes *}
    1.69  
    1.70  (* A somewhat arcane homomorphism example *)
    1.71  
    1.72 @@ -169,7 +168,7 @@
    1.73    by (rule semi_hom_mult)
    1.74  
    1.75  
    1.76 -text {* Theorem statements *}
    1.77 +section {* Theorem statements *}
    1.78  
    1.79  lemma (in lgrp) lcancel:
    1.80    "x ** y = x ** z <-> y = z"
    1.81 @@ -200,7 +199,7 @@
    1.82  print_locale! rgrp
    1.83  
    1.84  
    1.85 -text {* Patterns *}
    1.86 +subsection {* Patterns *}
    1.87  
    1.88  lemma (in rgrp)
    1.89    assumes "y ** x = z ** x" (is ?a)
    1.90 @@ -218,7 +217,7 @@
    1.91  qed
    1.92  
    1.93  
    1.94 -text {* Interpretation between locales: sublocales *}
    1.95 +section {* Interpretation between locales: sublocales *}
    1.96  
    1.97  sublocale lgrp < right: rgrp
    1.98  print_facts
    1.99 @@ -359,7 +358,7 @@
   1.100  print_locale! trivial  (* No instance for y created (subsumed). *)
   1.101  
   1.102  
   1.103 -text {* Sublocale, then interpretation in theory *}
   1.104 +subsection {* Sublocale, then interpretation in theory *}
   1.105  
   1.106  interpretation int: lgrp "op +" "0" "minus"
   1.107  proof unfold_locales
   1.108 @@ -374,7 +373,7 @@
   1.109    (* the latter comes through the sublocale relation *)
   1.110  
   1.111  
   1.112 -text {* Interpretation in theory, then sublocale *}
   1.113 +subsection {* Interpretation in theory, then sublocale *}
   1.114  
   1.115  interpretation (* fol: *) logic "op +" "minus"
   1.116  (* FIXME declaration of qualified names *)
   1.117 @@ -386,10 +385,12 @@
   1.118    assumes assoc: "(x && y) && z = x && (y && z)"
   1.119      and notnot: "-- (-- x) = x"
   1.120  begin
   1.121 -(* FIXME
   1.122 +
   1.123 +(* FIXME interpretation below fails
   1.124  definition lor (infixl "||" 50) where
   1.125    "x || y = --(-- x && -- y)"
   1.126  *)
   1.127 +
   1.128  end
   1.129  
   1.130  sublocale logic < two: logic2
   1.131 @@ -398,7 +399,16 @@
   1.132  thm two.assoc
   1.133  
   1.134  
   1.135 -text {* Interpretation in proofs *}
   1.136 +subsection {* Declarations and sublocale *}
   1.137 +
   1.138 +locale logic_a = logic
   1.139 +locale logic_b = logic
   1.140 +
   1.141 +sublocale logic_a < logic_b
   1.142 +  by unfold_locales
   1.143 +
   1.144 +
   1.145 +section {* Interpretation in proofs *}
   1.146  
   1.147  lemma True
   1.148  proof
     2.1 --- a/src/Pure/Isar/expression.ML	Wed Dec 10 14:45:15 2008 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Wed Dec 10 16:30:33 2008 +0100
     2.3 @@ -410,7 +410,7 @@
     2.4  
     2.5      val fors = prep_vars fixed context |> fst;
     2.6      val ctxt = context |> ProofContext.add_fixes_i fors |> snd;
     2.7 -    val (_, insts', ctxt') = fold prep_inst raw_insts (0, [], NewLocale.clear_local_idents ctxt);
     2.8 +    val (_, insts', ctxt') = fold prep_inst raw_insts (0, [], ctxt);
     2.9      val (_, elems'', ctxt'') = fold prep_elem raw_elems (insts', [], ctxt');
    2.10      val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt'');
    2.11  
    2.12 @@ -484,7 +484,7 @@
    2.13      (* Declare parameters and imported facts *)
    2.14      val context' = context |>
    2.15        ProofContext.add_fixes_i fixed |> snd |>
    2.16 -      NewLocale.clear_local_idents |> fold NewLocale.activate_local_facts deps;
    2.17 +      fold NewLocale.activate_local_facts deps;
    2.18      val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
    2.19    in ((fixed, deps, elems'), (parms, spec, defs)) end;
    2.20  
     3.1 --- a/src/Pure/Isar/new_locale.ML	Wed Dec 10 14:45:15 2008 +0100
     3.2 +++ b/src/Pure/Isar/new_locale.ML	Wed Dec 10 16:30:33 2008 +0100
     3.3 @@ -47,8 +47,7 @@
     3.4    val unfold_attrib: attribute
     3.5    val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
     3.6  
     3.7 -  (* Identifiers and registrations *)
     3.8 -  val clear_local_idents: Proof.context -> Proof.context
     3.9 +  (* Registrations *)
    3.10    val add_global_registration: (string * Morphism.morphism) -> theory -> theory
    3.11    val get_global_registrations: theory -> (string * Morphism.morphism) list
    3.12  
    3.13 @@ -223,12 +222,10 @@
    3.14  fun get_global_idents thy =
    3.15    let val (Ready ids) = (IdentifiersData.get o Context.Theory) thy in ids end;
    3.16  val put_global_idents = Context.theory_map o IdentifiersData.put o Ready;
    3.17 -val clear_global_idents = put_global_idents empty;
    3.18  
    3.19  fun get_local_idents ctxt =
    3.20    let val (Ready ids) = (IdentifiersData.get o Context.Proof) ctxt in ids end;
    3.21  val put_local_idents = Context.proof_map o IdentifiersData.put o Ready;
    3.22 -val clear_local_idents = put_local_idents empty;
    3.23  
    3.24  end;
    3.25