Methods intro_locales and unfold_locales apply to both old and new locales.
authorballarin
Mon Dec 01 13:43:32 2008 +0100 (2008-12-01)
changeset 289277e631979922f
parent 28926 530b83967c82
child 28928 bbc600e2276c
child 28936 f1647bf418f5
child 28939 08004ce1b167
Methods intro_locales and unfold_locales apply to both old and new locales.
src/FOL/ex/NewLocaleTest.thy
src/Pure/Isar/locale.ML
src/Pure/Isar/new_locale.ML
     1.1 --- a/src/FOL/ex/NewLocaleTest.thy	Mon Dec 01 12:17:04 2008 +0100
     1.2 +++ b/src/FOL/ex/NewLocaleTest.thy	Mon Dec 01 13:43:32 2008 +0100
     1.3 @@ -167,7 +167,7 @@
     1.4  
     1.5  sublocale lgrp < right: rgrp
     1.6  print_facts
     1.7 -proof new_unfold_locales
     1.8 +proof unfold_locales
     1.9    {
    1.10      fix x
    1.11      have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
    1.12 @@ -196,7 +196,7 @@
    1.13  (* circular interpretation *)
    1.14  
    1.15  sublocale rgrp < left: lgrp
    1.16 -proof new_unfold_locales
    1.17 +proof unfold_locales
    1.18    {
    1.19      fix x
    1.20      have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
    1.21 @@ -225,7 +225,7 @@
    1.22      and trans: "[| x << y; y << z |] ==> x << z"
    1.23  
    1.24  sublocale order < dual: order "%x y. y << x"
    1.25 -  apply new_unfold_locales apply (rule refl) apply (blast intro: trans)
    1.26 +  apply unfold_locales apply (rule refl) apply (blast intro: trans)
    1.27    done
    1.28  
    1.29  print_locale! order  (* Only two instances of order. *)
    1.30 @@ -244,7 +244,7 @@
    1.31  end
    1.32  
    1.33  sublocale order_with_def < dual: order' "op >>"
    1.34 -  apply new_unfold_locales
    1.35 +  apply unfold_locales
    1.36    unfolding greater_def
    1.37    apply (rule refl) apply (blast intro: trans)
    1.38    done
    1.39 @@ -291,14 +291,14 @@
    1.40  end
    1.41  
    1.42  sublocale trivial < x: trivial x _
    1.43 -  apply new_unfold_locales using Q by fast
    1.44 +  apply unfold_locales using Q by fast
    1.45  
    1.46  print_locale! trivial
    1.47  
    1.48  context trivial begin thm x.Q [where ?x = True] end
    1.49  
    1.50  sublocale trivial < y: trivial Q Q
    1.51 -  by new_unfold_locales
    1.52 +  by unfold_locales
    1.53    (* Succeeds since previous interpretation is more general. *)
    1.54  
    1.55  print_locale! trivial  (* No instance for y created (subsumed). *)
     2.1 --- a/src/Pure/Isar/locale.ML	Mon Dec 01 12:17:04 2008 +0100
     2.2 +++ b/src/Pure/Isar/locale.ML	Mon Dec 01 13:43:32 2008 +0100
     2.3 @@ -2043,15 +2043,6 @@
     2.4      Method.intros_tac (wits @ intros) facts st
     2.5    end;
     2.6  
     2.7 -val _ = Context.>> (Context.map_theory
     2.8 -  (Method.add_methods
     2.9 -    [("intro_locales",
    2.10 -      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
    2.11 -      "back-chain introduction rules of locales without unfolding predicates"),
    2.12 -     ("unfold_locales",
    2.13 -      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
    2.14 -      "back-chain all introduction rules of locales")]));
    2.15 -
    2.16  end;
    2.17  
    2.18  
     3.1 --- a/src/Pure/Isar/new_locale.ML	Mon Dec 01 12:17:04 2008 +0100
     3.2 +++ b/src/Pure/Isar/new_locale.ML	Mon Dec 01 13:43:32 2008 +0100
     3.3 @@ -385,11 +385,13 @@
     3.4  
     3.5  val _ = Context.>> (Context.map_theory
     3.6    (Method.add_methods
     3.7 -    [("new_intro_locales",
     3.8 -      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
     3.9 +    [("intro_locales",
    3.10 +      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt ORELSE'
    3.11 +        Locale.intro_locales_tac false ctxt)),
    3.12        "back-chain introduction rules of locales without unfolding predicates"),
    3.13 -     ("new_unfold_locales",
    3.14 -      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
    3.15 +     ("unfold_locales",
    3.16 +      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt ORELSE'
    3.17 +        Locale.intro_locales_tac true ctxt)),
    3.18        "back-chain all introduction rules of locales")]));
    3.19  
    3.20