--- a/src/HOL/Library/Word.thy Sun Dec 20 20:14:05 2020 +0100
+++ b/src/HOL/Library/Word.thy Sun Dec 20 20:49:43 2020 +0100
@@ -3227,7 +3227,8 @@
\<comment> \<open>\<open>unat_arith_tac\<close>: tactic to reduce word arithmetic to \<open>nat\<close>, try to solve via \<open>arith\<close>\<close>
ML \<open>
val unat_arith_simpset =
- @{context}
+ @{context} (* TODO: completely explicitly determined simpset *)
+ |> fold Simplifier.del_simp @{thms unsigned_of_nat unsigned_of_int}
|> fold Simplifier.add_simp @{thms unat_arith_simps}
|> fold Splitter.add_split @{thms if_split_asm}
|> fold Simplifier.add_cong @{thms power_False_cong}
--- a/src/Pure/Isar/interpretation.ML Sun Dec 20 20:14:05 2020 +0100
+++ b/src/Pure/Isar/interpretation.ML Sun Dec 20 20:49:43 2020 +0100
@@ -156,13 +156,16 @@
(* interpretation in local theories *)
+val add_registration_local_theory =
+ Named_Target.revoke_reinitializability oo Locale.add_registration_local_theory;
+
fun interpretation expression =
generic_interpretation cert_interpretation Element.witness_proof_eqs
- Local_Theory.notes_kind Locale.add_registration_local_theory expression [];
+ Local_Theory.notes_kind add_registration_local_theory expression [];
fun interpretation_cmd expression =
generic_interpretation read_interpretation Element.witness_proof_eqs
- Local_Theory.notes_kind Locale.add_registration_local_theory expression [];
+ Local_Theory.notes_kind add_registration_local_theory expression [];
(* interpretation into global theories *)
@@ -219,7 +222,7 @@
fun register_or_activate lthy =
if Named_Target.is_theory lthy
then Local_Theory.theory_registration
- else Locale.add_registration_local_theory;
+ else add_registration_local_theory;
fun gen_isar_interpretation prep_interpretation expression lthy =
generic_interpretation prep_interpretation Element.witness_proof_eqs
--- a/src/Pure/Isar/local_theory.ML Sun Dec 20 20:14:05 2020 +0100
+++ b/src/Pure/Isar/local_theory.ML Sun Dec 20 20:49:43 2020 +0100
@@ -24,7 +24,6 @@
type operations
val assert: local_theory -> local_theory
val level: Proof.context -> int
- val revoke_reinitializability: local_theory -> local_theory
val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
val background_naming_of: local_theory -> Name_Space.naming
val map_background_naming: (Name_Space.naming -> Name_Space.naming) ->
@@ -69,7 +68,6 @@
conclude: local_theory -> Proof.context} -> operations -> theory -> local_theory
val exit: local_theory -> Proof.context
val exit_global: local_theory -> theory
- val exit_global_reinitializable: local_theory -> theory
val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
val begin_nested: local_theory -> Binding.scope * local_theory
@@ -105,12 +103,11 @@
{background_naming: Name_Space.naming,
operations: operations,
conclude: Proof.context -> Proof.context,
- reinitializable: bool,
target: Proof.context};
-fun make_lthy (background_naming, operations, conclude, reinitializable, target) : lthy =
+fun make_lthy (background_naming, operations, conclude, target) : lthy =
{background_naming = background_naming, operations = operations,
- conclude = conclude, reinitializable = reinitializable, target = target};
+ conclude = conclude, target = target};
(* context data *)
@@ -150,16 +147,16 @@
fun map_top f =
assert #>
- Data.map (fn {background_naming, operations, conclude, reinitializable, target} :: parents =>
- make_lthy (f (background_naming, operations, conclude, reinitializable, target)) :: parents);
+ Data.map (fn {background_naming, operations, conclude, target} :: parents =>
+ make_lthy (f (background_naming, operations, conclude, target)) :: parents);
fun reset lthy = #target (top_of lthy) |> Data.put (Data.get lthy);
fun map_contexts f lthy =
let val n = level lthy in
lthy |> (Data.map o map_index)
- (fn (i, {background_naming, operations, conclude, reinitializable, target}) =>
- make_lthy (background_naming, operations, conclude, reinitializable,
+ (fn (i, {background_naming, operations, conclude, target}) =>
+ make_lthy (background_naming, operations, conclude,
target
|> Context_Position.set_visible false
|> f (n - i - 1)
@@ -168,26 +165,13 @@
end;
-(* reinitializable context -- implicit for nested structures *)
-
-fun revoke_reinitializability lthy =
- if level lthy = 1 then
- map_top (fn (background_naming, operations, conclude, _, target) =>
- (background_naming, operations, conclude, false, target)) lthy
- else lthy;
-
-fun assert_reinitializable lthy =
- if #reinitializable (top_of lthy) then lthy
- else error "Non-reinitializable local theory context";
-
-
(* naming for background theory *)
val background_naming_of = #background_naming o top_of;
fun map_background_naming f =
- map_top (fn (background_naming, operations, conclude, reinitializable, target) =>
- (f background_naming, operations, conclude, reinitializable, target));
+ map_top (fn (background_naming, operations, conclude, target) =>
+ (f background_naming, operations, conclude, target));
val restore_background_naming = map_background_naming o K o background_naming_of;
@@ -353,8 +337,7 @@
(* main target *)
fun init_target background_naming conclude operations target =
- Data.map (K [make_lthy
- (background_naming, operations, conclude, true, target)]) target
+ Data.map (K [make_lthy (background_naming, operations, conclude, target)]) target
fun init {background_naming, setup, conclude} operations thy =
thy
@@ -366,7 +349,6 @@
fun exit lthy = exit_of lthy (assert_bottom lthy);
val exit_global = Proof_Context.theory_of o exit;
-val exit_global_reinitializable = exit_global o assert_reinitializable;
fun exit_result decl (x, lthy) =
let
@@ -389,7 +371,7 @@
val _ = assert lthy;
val (scope, target) = Proof_Context.new_scope lthy;
val entry = make_lthy (background_naming_of lthy, operations_of lthy,
- Proof_Context.restore_naming lthy, true, target);
+ Proof_Context.restore_naming lthy, target);
val lthy' = Data.map (cons entry) target;
in (scope, lthy') end;
--- a/src/Pure/Isar/locale.ML Sun Dec 20 20:14:05 2020 +0100
+++ b/src/Pure/Isar/locale.ML Sun Dec 20 20:49:43 2020 +0100
@@ -615,16 +615,13 @@
val add_registration_theory = Local_Theory.raw_theory o add_registration_theory';
-fun add_registration_local_theory' registration lthy =
+fun add_registration_local_theory registration lthy =
let val n = Local_Theory.level lthy in
lthy
|> Local_Theory.map_contexts (fn level =>
level = n - 1 ? Context.proof_map (add_registration registration))
end;
-fun add_registration_local_theory registration =
- Local_Theory.revoke_reinitializability #> add_registration_local_theory' registration
-
fun add_registration_proof registration ctxt = ctxt
|> Proof_Context.set_stmt false
|> Context.proof_map (add_registration registration)
@@ -658,7 +655,7 @@
fun add_dependency loc registration =
Local_Theory.raw_theory (add_dependency' loc registration)
- #> add_registration_local_theory' registration;
+ #> add_registration_local_theory registration;
(*** Storing results ***)
--- a/src/Pure/Isar/named_target.ML Sun Dec 20 20:14:05 2020 +0100
+++ b/src/Pure/Isar/named_target.ML Sun Dec 20 20:49:43 2020 +0100
@@ -16,7 +16,8 @@
val theory_map: (local_theory -> local_theory) -> theory -> theory
val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) ->
theory -> 'b * theory
- val reinit: local_theory -> theory -> local_theory
+ val revoke_reinitializability: local_theory -> local_theory
+ val exit_global_reinitialize: local_theory -> (theory -> local_theory) * theory
end;
structure Named_Target: NAMED_TARGET =
@@ -48,11 +49,11 @@
structure Data = Proof_Data
(
- type T = target option;
+ type T = (target * bool) option;
fun init _ = NONE;
);
-val get_bottom_target = Data.get;
+val get_bottom_target = Option.map fst o Data.get;
fun get_target lthy =
if Local_Theory.level lthy = 1
@@ -72,6 +73,9 @@
val class_of = class_of_target o get_target;
+fun is_reinitializable lthy =
+ Local_Theory.level lthy = 1 andalso (the_default false o Option.map snd o Data.get) lthy;
+
(* operations *)
@@ -115,6 +119,11 @@
| setup_context (Locale locale) = Locale.init locale
| setup_context (Class class) = Class.init class;
+fun setup target includes =
+ setup_context target
+ #> Data.put (SOME (target, null includes))
+ #> Bundle.includes includes;
+
fun init includes ident thy =
let
val target = target_of_ident thy ident;
@@ -122,10 +131,9 @@
thy
|> Local_Theory.init
{background_naming = Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident),
- setup = setup_context target #> Data.put (SOME target) #> Bundle.includes includes,
+ setup = setup target includes,
conclude = I}
(operations target)
- |> not (null includes) ? Local_Theory.revoke_reinitializability
end;
val theory_init = init [] "";
@@ -134,6 +142,11 @@
fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f;
-fun reinit lthy = init [] (ident_of lthy);
+val revoke_reinitializability = (Data.map o Option.map o apsnd) (K false);
+
+fun exit_global_reinitialize lthy =
+ if is_reinitializable lthy
+ then (init [] (ident_of lthy), Local_Theory.exit_global lthy)
+ else error "Non-reinitializable local theory context";
end;
--- a/src/Pure/Isar/target_context.ML Sun Dec 20 20:14:05 2020 +0100
+++ b/src/Pure/Isar/target_context.ML Sun Dec 20 20:49:43 2020 +0100
@@ -36,8 +36,12 @@
| switch_named_cmd NONE (Context.Proof lthy) =
(Context.Proof o Local_Theory.reset, lthy)
| switch_named_cmd (SOME name) (Context.Proof lthy) =
- (Context.Proof o Named_Target.reinit lthy o Local_Theory.exit_global,
- (context_begin_named_cmd [] name o Local_Theory.exit_global_reinitializable) lthy);
+ let
+ val (reinit, thy) = Named_Target.exit_global_reinitialize lthy
+ in
+ (Context.Proof o reinit o Local_Theory.exit_global,
+ context_begin_named_cmd [] name thy)
+ end;
fun includes raw_includes lthy =
Bundle.includes (map (Bundle.check lthy) raw_includes) lthy;