--- a/src/Doc/Implementation/Local_Theory.thy Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Doc/Implementation/Local_Theory.thy Sun Nov 01 16:54:49 2020 +0100
@@ -91,7 +91,7 @@
text %mlref \<open>
\begin{mldecls}
@{index_ML_type local_theory: Proof.context} \\
- @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex]
+ @{index_ML Named_Target.init: "string list -> string -> theory -> local_theory"} \\[1ex]
@{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
local_theory -> (term * (string * thm)) * local_theory"} \\
@{index_ML Local_Theory.note: "Attrib.binding * thm list ->
@@ -104,7 +104,7 @@
context data. Subtyping means that any value \<open>lthy:\<close>~\<^ML_type>\<open>local_theory\<close>
can be also used with operations on expecting a regular \<open>ctxt:\<close>~\<^ML_type>\<open>Proof.context\<close>.
- \<^descr> \<^ML>\<open>Named_Target.init\<close>~\<open>before_exit name thy\<close> initializes a local theory
+ \<^descr> \<^ML>\<open>Named_Target.init\<close>~\<open>includes name thy\<close> initializes a local theory
derived from the given background theory. An empty name refers to a \<^emph>\<open>global
theory\<close> context, and a non-empty name refers to a @{command locale} or
@{command class} context (a fully-qualified internal name is expected here).
--- a/src/HOL/Library/Perm.thy Sun Nov 01 15:31:41 2020 +0100
+++ b/src/HOL/Library/Perm.thy Sun Nov 01 16:54:49 2020 +0100
@@ -730,7 +730,7 @@
subsection \<open>Swaps\<close>
-lift_definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> 'a perm" ("\<langle>_\<leftrightarrow>_\<rangle>")
+lift_definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> 'a perm" ("\<langle>_ \<leftrightarrow> _\<rangle>")
is "\<lambda>a b. Fun.swap a b id"
proof
fix a b :: 'a
@@ -741,37 +741,37 @@
qed simp
lemma apply_swap_simp [simp]:
- "\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> a = b"
- "\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> b = a"
+ "\<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> a = b"
+ "\<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> b = a"
by (transfer; simp)+
lemma apply_swap_same [simp]:
- "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> \<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> c = c"
+ "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> \<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> c = c"
by transfer simp
lemma apply_swap_eq_iff [simp]:
- "\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> c = a \<longleftrightarrow> c = b"
- "\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> c = b \<longleftrightarrow> c = a"
+ "\<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> c = a \<longleftrightarrow> c = b"
+ "\<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> c = b \<longleftrightarrow> c = a"
by (transfer; auto simp add: Fun.swap_def)+
lemma swap_1 [simp]:
- "\<langle>a\<leftrightarrow>a\<rangle> = 1"
+ "\<langle>a \<leftrightarrow> a\<rangle> = 1"
by transfer simp
lemma swap_sym:
- "\<langle>b\<leftrightarrow>a\<rangle> = \<langle>a\<leftrightarrow>b\<rangle>"
+ "\<langle>b \<leftrightarrow> a\<rangle> = \<langle>a \<leftrightarrow> b\<rangle>"
by (transfer; auto simp add: Fun.swap_def)+
lemma swap_self [simp]:
- "\<langle>a\<leftrightarrow>b\<rangle> * \<langle>a\<leftrightarrow>b\<rangle> = 1"
+ "\<langle>a \<leftrightarrow> b\<rangle> * \<langle>a \<leftrightarrow> b\<rangle> = 1"
by transfer (simp add: Fun.swap_def fun_eq_iff)
lemma affected_swap:
- "a \<noteq> b \<Longrightarrow> affected \<langle>a\<leftrightarrow>b\<rangle> = {a, b}"
+ "a \<noteq> b \<Longrightarrow> affected \<langle>a \<leftrightarrow> b\<rangle> = {a, b}"
by transfer (auto simp add: Fun.swap_def)
lemma inverse_swap [simp]:
- "inverse \<langle>a\<leftrightarrow>b\<rangle> = \<langle>a\<leftrightarrow>b\<rangle>"
+ "inverse \<langle>a \<leftrightarrow> b\<rangle> = \<langle>a \<leftrightarrow> b\<rangle>"
by transfer (auto intro: inv_equality simp: Fun.swap_def)
@@ -793,14 +793,14 @@
bundle no_permutation_syntax
begin
- no_notation swap ("\<langle>_\<leftrightarrow>_\<rangle>")
+ no_notation swap ("\<langle>_ \<leftrightarrow> _\<rangle>")
no_notation cycle ("\<langle>_\<rangle>")
no_notation "apply" (infixl "\<langle>$\<rangle>" 999)
end
bundle permutation_syntax
begin
- notation swap ("\<langle>_\<leftrightarrow>_\<rangle>")
+ notation swap ("\<langle>_ \<leftrightarrow> _\<rangle>")
notation cycle ("\<langle>_\<rangle>")
notation "apply" (infixl "\<langle>$\<rangle>" 999)
end
--- a/src/HOL/ROOT Sun Nov 01 15:31:41 2020 +0100
+++ b/src/HOL/ROOT Sun Nov 01 16:54:49 2020 +0100
@@ -681,6 +681,7 @@
Simps_Case_Conv_Examples
Sketch_and_Explore
Sorting_Algorithms_Examples
+ Specifications_with_bundle_mixins
Sqrt
Sqrt_Script
Sudoku
--- a/src/HOL/Statespace/state_space.ML Sun Nov 01 15:31:41 2020 +0100
+++ b/src/HOL/Statespace/state_space.ML Sun Nov 01 16:54:49 2020 +0100
@@ -134,13 +134,13 @@
fun add_locale name expr elems thy =
thy
- |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems
+ |> Expression.add_locale (Binding.name name) (Binding.name name) [] expr elems
|> snd
|> Local_Theory.exit;
fun add_locale_cmd name expr elems thy =
thy
- |> Expression.add_locale_cmd (Binding.name name) Binding.empty (expression_no_pos expr) elems
+ |> Expression.add_locale_cmd (Binding.name name) Binding.empty [] (expression_no_pos expr) elems
|> snd
|> Local_Theory.exit;
@@ -298,7 +298,7 @@
fun add_declaration name decl thy =
thy
- |> Named_Target.init name
+ |> Named_Target.init [] name
|> (fn lthy => Local_Theory.declaration {syntax = true, pervasive = false} (decl lthy) lthy)
|> Local_Theory.exit_global;
--- a/src/HOL/ex/Perm_Fragments.thy Sun Nov 01 15:31:41 2020 +0100
+++ b/src/HOL/ex/Perm_Fragments.thy Sun Nov 01 16:54:49 2020 +0100
@@ -6,13 +6,14 @@
imports "HOL-Library.Perm" "HOL-Library.Dlist"
begin
-unbundle permutation_syntax
-
-
text \<open>On cycles\<close>
+context
+ includes permutation_syntax
+begin
+
lemma cycle_prod_list:
- "\<langle>a # as\<rangle> = prod_list (map (\<lambda>b. \<langle>a\<leftrightarrow>b\<rangle>) (rev as))"
+ "\<langle>a # as\<rangle> = prod_list (map (\<lambda>b. \<langle>a \<leftrightarrow> b\<rangle>) (rev as))"
by (induct as) simp_all
lemma cycle_append [simp]:
@@ -21,11 +22,11 @@
case (3 b c as)
then have "\<langle>a # (b # as) @ bs\<rangle> = \<langle>a # bs\<rangle> * \<langle>a # b # as\<rangle>"
by simp
- then have "\<langle>a # as @ bs\<rangle> * \<langle>a\<leftrightarrow>b\<rangle> =
- \<langle>a # bs\<rangle> * \<langle>a # as\<rangle> * \<langle>a\<leftrightarrow>b\<rangle>"
+ then have "\<langle>a # as @ bs\<rangle> * \<langle>a \<leftrightarrow> b\<rangle> =
+ \<langle>a # bs\<rangle> * \<langle>a # as\<rangle> * \<langle>a \<leftrightarrow> b\<rangle>"
by (simp add: ac_simps)
- then have "\<langle>a # as @ bs\<rangle> * \<langle>a\<leftrightarrow>b\<rangle> * \<langle>a\<leftrightarrow>b\<rangle> =
- \<langle>a # bs\<rangle> * \<langle>a # as\<rangle> * \<langle>a\<leftrightarrow>b\<rangle> * \<langle>a\<leftrightarrow>b\<rangle>"
+ then have "\<langle>a # as @ bs\<rangle> * \<langle>a \<leftrightarrow> b\<rangle> * \<langle>a \<leftrightarrow> b\<rangle> =
+ \<langle>a # bs\<rangle> * \<langle>a # as\<rangle> * \<langle>a \<leftrightarrow> b\<rangle> * \<langle>a \<leftrightarrow> b\<rangle>"
by simp
then have "\<langle>a # as @ bs\<rangle> = \<langle>a # bs\<rangle> * \<langle>a # as\<rangle>"
by (simp add: ac_simps)
@@ -39,15 +40,15 @@
proof (induct as rule: cycle.induct)
case (3 a b as)
from affected_times
- have "affected (\<langle>a # as\<rangle> * \<langle>a\<leftrightarrow>b\<rangle>)
- \<subseteq> affected \<langle>a # as\<rangle> \<union> affected \<langle>a\<leftrightarrow>b\<rangle>" .
+ have "affected (\<langle>a # as\<rangle> * \<langle>a \<leftrightarrow> b\<rangle>)
+ \<subseteq> affected \<langle>a # as\<rangle> \<union> affected \<langle>a \<leftrightarrow> b\<rangle>" .
moreover from 3
have "affected (\<langle>a # as\<rangle>) \<subseteq> insert a (set as)"
by simp
moreover
- have "affected \<langle>a\<leftrightarrow>b\<rangle> \<subseteq> {a, b}"
+ have "affected \<langle>a \<leftrightarrow> b\<rangle> \<subseteq> {a, b}"
by (cases "a = b") (simp_all add: affected_swap)
- ultimately have "affected (\<langle>a # as\<rangle> * \<langle>a\<leftrightarrow>b\<rangle>)
+ ultimately have "affected (\<langle>a # as\<rangle> * \<langle>a \<leftrightarrow> b\<rangle>)
\<subseteq> insert a (insert b (set as))"
by blast
then show ?case by auto
@@ -75,7 +76,7 @@
case (snoc cs c)
with distinct have "distinct (a # b # cs @ [c])"
by simp
- then have **: "\<langle>a\<leftrightarrow>b\<rangle> * \<langle>c\<leftrightarrow>a\<rangle> = \<langle>c\<leftrightarrow>a\<rangle> * \<langle>c\<leftrightarrow>b\<rangle>"
+ then have **: "\<langle>a \<leftrightarrow> b\<rangle> * \<langle>c \<leftrightarrow> a\<rangle> = \<langle>c \<leftrightarrow> a\<rangle> * \<langle>c \<leftrightarrow> b\<rangle>"
by transfer (auto simp add: comp_def Fun.swap_def)
with snoc * show ?thesis
by (simp add: mult.assoc [symmetric])
@@ -109,7 +110,7 @@
definition fixate :: "'a \<Rightarrow> 'a perm \<Rightarrow> 'a perm"
where
- "fixate a f = (if a \<in> affected f then f * \<langle>apply (inverse f) a\<leftrightarrow>a\<rangle> else f)"
+ "fixate a f = (if a \<in> affected f then f * \<langle>inverse f \<langle>$\<rangle> a \<leftrightarrow> a\<rangle> else f)"
lemma affected_fixate_trivial:
assumes "a \<notin> affected f"
@@ -258,6 +259,11 @@
where
"cycles f = map (\<lambda>a. trace a f) (seeds f)"
+end
+
+
+text \<open>Misc\<close>
+
lemma (in comm_monoid_list_set) sorted_list_of_set:
assumes "finite A"
shows "list.F (map h (sorted_list_of_set A)) = set.F h A"
@@ -269,9 +275,6 @@
by (simp)
qed
-
-text \<open>Misc\<close>
-
primrec subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
"subtract [] ys = ys"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Specifications_with_bundle_mixins.thy Sun Nov 01 16:54:49 2020 +0100
@@ -0,0 +1,60 @@
+theory Specifications_with_bundle_mixins
+ imports "HOL-Library.Perm"
+begin
+
+locale involutory =
+ includes permutation_syntax
+ fixes f :: \<open>'a perm\<close>
+ assumes involutory: \<open>\<And>x. f \<langle>$\<rangle> (f \<langle>$\<rangle> x) = x\<close>
+begin
+
+lemma
+ \<open>f * f = 1\<close>
+ using involutory
+ by (simp add: perm_eq_iff apply_sequence)
+
+end
+
+context involutory
+begin
+
+thm involutory (*syntax from permutation_syntax only present in locale specification and initial block*)
+
+end
+
+
+class at_most_two_elems =
+ includes permutation_syntax
+ assumes swap_distinct: \<open>a \<noteq> b \<Longrightarrow> \<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> c \<noteq> c\<close>
+begin
+
+lemma
+ \<open>card (UNIV :: 'a set) \<le> 2\<close>
+proof (rule ccontr)
+ fix a :: 'a
+ assume \<open>\<not> card (UNIV :: 'a set) \<le> 2\<close>
+ then have c0: \<open>card (UNIV :: 'a set) \<ge> 3\<close>
+ by simp
+ then have [simp]: \<open>finite (UNIV :: 'a set)\<close>
+ using card.infinite by fastforce
+ from c0 card_Diff1_le [of UNIV a]
+ have ca: \<open>card (UNIV - {a}) \<ge> 2\<close>
+ by simp
+ then obtain b where \<open>b \<in> (UNIV - {a})\<close>
+ by (metis all_not_in_conv card.empty card_2_iff' le_zero_eq)
+ with ca card_Diff1_le [of \<open>UNIV - {a}\<close> b]
+ have cb: \<open>card (UNIV - {a, b}) \<ge> 1\<close> and \<open>a \<noteq> b\<close>
+ by simp_all
+ then obtain c where \<open>c \<in> (UNIV - {a, b})\<close>
+ by (metis One_nat_def all_not_in_conv card.empty le_zero_eq nat.simps(3))
+ then have \<open>a \<noteq> c\<close> \<open>b \<noteq> c\<close>
+ by auto
+ with swap_distinct [of a b c] show False
+ by (simp add: \<open>a \<noteq> b\<close>)
+qed
+
+end
+
+thm swap_distinct (*syntax from permutation_syntax only present in class specification and initial block*)
+
+end
\ No newline at end of file
--- a/src/Pure/Isar/class_declaration.ML Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/Isar/class_declaration.ML Sun Nov 01 16:54:49 2020 +0100
@@ -6,9 +6,9 @@
signature CLASS_DECLARATION =
sig
- val class: binding -> class list ->
+ val class: binding -> string list -> class list ->
Element.context_i list -> theory -> string * local_theory
- val class_cmd: binding -> xstring list ->
+ val class_cmd: binding -> (xstring * Position.T) list -> xstring list ->
Element.context list -> theory -> string * local_theory
val prove_subclass: tactic -> class ->
local_theory -> local_theory
@@ -108,9 +108,10 @@
(* reading and processing class specifications *)
-fun prep_class_elems prep_decl thy sups raw_elems =
+fun prep_class_elems prep_decl ctxt sups raw_elems =
let
(* user space type system: only permits 'a type variable, improves towards 'a *)
+ val thy = Proof_Context.theory_of ctxt;
val algebra = Sign.classes_of thy;
val inter_sort = curry (Sorts.inter_sort algebra);
val proto_base_sort =
@@ -165,7 +166,7 @@
#> Class.redeclare_operations thy sups
#> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (K singleton_fixate));
val ((raw_supparams, _, raw_inferred_elems, _), _) =
- Proof_Context.init_global thy
+ ctxt
|> Context.proof_map (Syntax_Phases.term_check 0 "unify_params" (K unify_params))
|> prep_decl raw_supexpr init_class_body raw_elems;
fun filter_element (Element.Fixes []) = NONE
@@ -205,13 +206,13 @@
val cert_class_elems = prep_class_elems Expression.cert_declaration;
val read_class_elems = prep_class_elems Expression.cert_read_declaration;
-fun prep_class_spec prep_class prep_class_elems thy raw_supclasses raw_elems =
+fun prep_class_spec prep_class prep_include prep_class_elems ctxt raw_supclasses raw_includes raw_elems =
let
- val thy_ctxt = Proof_Context.init_global thy;
+ val thy = Proof_Context.theory_of ctxt;
(* prepare import *)
val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
- val sups = Sign.minimize_sort thy (map (prep_class thy_ctxt) raw_supclasses);
+ val sups = Sign.minimize_sort thy (map (prep_class ctxt) raw_supclasses);
val _ =
(case filter_out (Class.is_class thy) sups of
[] => ()
@@ -225,11 +226,13 @@
else ();
(* infer types and base sort *)
- val (base_sort, supparam_names, supexpr, inferred_elems) = prep_class_elems thy sups raw_elems;
+ val includes = map (prep_include ctxt) raw_includes;
+ val includes_ctxt = Bundle.includes includes ctxt;
+ val (base_sort, supparam_names, supexpr, inferred_elems) = prep_class_elems includes_ctxt sups raw_elems;
val sup_sort = inter_sort base_sort sups;
(* process elements as class specification *)
- val class_ctxt = Class.begin sups base_sort thy_ctxt;
+ val class_ctxt = Class.begin sups base_sort includes_ctxt;
val ((_, _, syntax_elems, _), _) = class_ctxt
|> Expression.cert_declaration supexpr I inferred_elems;
fun check_vars e vs =
@@ -250,10 +253,10 @@
| fork_syn x = pair x;
val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
- in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (elems, global_syntax)) end;
+ in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (includes, elems, global_syntax)) end;
-val cert_class_spec = prep_class_spec (K I) cert_class_elems;
-val read_class_spec = prep_class_spec Proof_Context.read_class read_class_elems;
+val cert_class_spec = prep_class_spec (K I) (K I) cert_class_elems;
+val read_class_spec = prep_class_spec Proof_Context.read_class Bundle.check read_class_elems;
(* class establishment *)
@@ -313,15 +316,16 @@
#> pair (param_map, params, assm_axiom)))
end;
-fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
+fun gen_class prep_class_spec b raw_includes raw_supclasses raw_elems thy =
let
val class = Sign.full_name thy b;
val prefix = Binding.qualify true "class";
- val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
- prep_class_spec thy raw_supclasses raw_elems;
+ val ctxt = Proof_Context.init_global thy;
+ val (((sups, supparam_names), (supsort, base_sort, supexpr)), (includes, elems, global_syntax)) =
+ prep_class_spec ctxt raw_supclasses raw_includes raw_elems;
in
thy
- |> Expression.add_locale b (prefix b) supexpr elems
+ |> Expression.add_locale b (prefix b) includes supexpr elems
|> snd |> Local_Theory.exit_global
|> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
|-> (fn (param_map, params, assm_axiom) =>
@@ -334,7 +338,7 @@
#> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
#> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
|> snd
- |> Named_Target.init class
+ |> Named_Target.init includes class
|> pair class
end;
--- a/src/Pure/Isar/experiment.ML Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/Isar/experiment.ML Sun Nov 01 16:54:49 2020 +0100
@@ -29,7 +29,7 @@
val experiment_name = Binding.name ("experiment" ^ serial_string ()) |> Binding.concealed;
val lthy =
thy
- |> add_locale experiment_name Binding.empty ([], []) elems
+ |> add_locale experiment_name Binding.empty [] ([], []) elems
|-> (Local_Theory.background_theory o Data.map o Symtab.insert_set);
val (scope, naming) =
Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
--- a/src/Pure/Isar/expression.ML Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/Isar/expression.ML Sun Nov 01 16:54:49 2020 +0100
@@ -32,9 +32,9 @@
val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
* Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
- val add_locale: binding -> binding ->
+ val add_locale: binding -> binding -> string list ->
expression_i -> Element.context_i list -> theory -> string * local_theory
- val add_locale_cmd: binding -> binding ->
+ val add_locale_cmd: binding -> binding -> (xstring * Position.T) list ->
expression -> Element.context list -> theory -> string * local_theory
(* Processing of locale expressions *)
@@ -796,15 +796,20 @@
val is_hyp = fn Assumes _ => true | Defines _ => true | _ => false;
-fun gen_add_locale prep_decl
- binding raw_predicate_binding raw_import raw_body thy =
+fun gen_add_locale prep_include prep_decl
+ binding raw_predicate_binding raw_includes raw_import raw_body thy =
let
val name = Sign.full_name thy binding;
val _ = Locale.defined thy name andalso
error ("Duplicate definition of locale " ^ quote name);
+ val ctxt = Proof_Context.init_global thy;
+ val includes = map (prep_include ctxt) raw_includes;
+
val ((fixed, deps, body_elems, _), (parms, ctxt')) =
- prep_decl raw_import I raw_body (Proof_Context.init_global thy);
+ ctxt
+ |> Bundle.includes includes
+ |> prep_decl raw_import I raw_body;
val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
val extraTs =
@@ -857,15 +862,15 @@
val loc_ctxt = thy'
|> Locale.register_locale binding (extraTs, params)
(asm, rev defs) (a_intro, b_intro) axioms hyp_spec [] (rev notes) (rev deps')
- |> Named_Target.init name
+ |> Named_Target.init includes name
|> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
in (name, loc_ctxt) end;
in
-val add_locale = gen_add_locale cert_declaration;
-val add_locale_cmd = gen_add_locale read_declaration;
+val add_locale = gen_add_locale (K I) cert_declaration;
+val add_locale_cmd = gen_add_locale Bundle.check read_declaration;
end;
--- a/src/Pure/Isar/interpretation.ML Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/Isar/interpretation.ML Sun Nov 01 16:54:49 2020 +0100
@@ -191,7 +191,7 @@
fun gen_global_sublocale prep_loc prep_interpretation
raw_locale expression raw_defs thy =
let
- val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
+ val lthy = Named_Target.init [] (prep_loc thy raw_locale) thy;
fun setup_proof after_qed =
Element.witness_proof_eqs
(fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
--- a/src/Pure/Isar/named_target.ML Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/Isar/named_target.ML Sun Nov 01 16:54:49 2020 +0100
@@ -11,7 +11,7 @@
val locale_of: local_theory -> string option
val bottom_locale_of: local_theory -> string option
val class_of: local_theory -> string option
- val init: string -> theory -> local_theory
+ val init: string list -> string -> theory -> local_theory
val theory_init: theory -> local_theory
val theory_map: (local_theory -> local_theory) -> theory -> theory
val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) ->
@@ -115,24 +115,25 @@
| setup_context (Locale locale) = Locale.init locale
| setup_context (Class class) = Class.init class;
-fun init ident thy =
+fun init includes ident thy =
let
val target = target_of_ident thy ident;
in
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),
+ setup = setup_context target #> Data.put (SOME target) #> Bundle.includes includes,
conclude = I}
(operations target)
+ |> not (null includes) ? Local_Theory.mark_brittle
end;
-val theory_init = init "";
+val theory_init = init [] "";
fun theory_map g = theory_init #> g #> Local_Theory.exit_global;
fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f;
-fun reinit lthy = init (ident_of lthy);
+fun reinit lthy = init [] (ident_of lthy);
end;
--- a/src/Pure/Isar/parse_spec.ML Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/Isar/parse_spec.ML Sun Nov 01 16:54:49 2020 +0100
@@ -127,7 +127,10 @@
Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
Parse.$$$ "defines" || Parse.$$$ "notes";
-val class_expression = plus1_unless locale_keyword Parse.class;
+val locale_keyword' =
+ Parse.$$$ "includes" || locale_keyword;
+
+val class_expression = plus1_unless locale_keyword' Parse.class;
val locale_expression =
let
@@ -135,7 +138,7 @@
val expr1 =
locale_prefix -- expr2 --
instance >> (fn ((p, l), i) => (l, (p, i)));
- val expr0 = plus1_unless locale_keyword expr1;
+ val expr0 = plus1_unless locale_keyword' expr1;
in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
val context_element = Parse.group (fn () => "context element") loc_element;
--- a/src/Pure/Isar/target_context.ML Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/Isar/target_context.ML Sun Nov 01 16:54:49 2020 +0100
@@ -6,7 +6,8 @@
signature TARGET_CONTEXT =
sig
- val context_begin_named_cmd: xstring * Position.T -> theory -> local_theory
+ val context_begin_named_cmd: (xstring * Position.T) list -> xstring * Position.T ->
+ theory -> local_theory
val end_named_cmd: local_theory -> Context.generic
val switch_named_cmd: (xstring * Position.T) option -> Context.generic ->
(local_theory -> Context.generic) * local_theory
@@ -18,28 +19,33 @@
structure Target_Context: TARGET_CONTEXT =
struct
-fun context_begin_named_cmd ("-", _) thy = Named_Target.theory_init thy
- | context_begin_named_cmd target thy = Named_Target.init (Locale.check thy target) thy;
+fun prep_includes thy =
+ map (Bundle.check (Proof_Context.init_global thy));
+
+fun context_begin_named_cmd raw_includes ("-", _) thy =
+ Named_Target.init (prep_includes thy raw_includes) "" thy
+ | context_begin_named_cmd raw_includes name thy =
+ Named_Target.init (prep_includes thy raw_includes) (Locale.check thy name) thy;
val end_named_cmd = Context.Theory o Local_Theory.exit_global;
fun switch_named_cmd NONE (Context.Theory thy) =
- (Context.Theory o Local_Theory.exit_global, Named_Target.theory_init thy)
+ (end_named_cmd, Named_Target.theory_init thy)
| switch_named_cmd (SOME name) (Context.Theory thy) =
- (Context.Theory o Local_Theory.exit_global, context_begin_named_cmd name thy)
+ (end_named_cmd, context_begin_named_cmd [] name thy)
| 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_nonbrittle) lthy);
+ (context_begin_named_cmd [] name o Local_Theory.exit_global_nonbrittle) lthy);
-fun includes raw_incls lthy =
- Bundle.includes (map (Bundle.check lthy) raw_incls) lthy;
+fun includes raw_includes lthy =
+ Bundle.includes (map (Bundle.check lthy) raw_includes) lthy;
-fun context_begin_nested_cmd raw_incls raw_elems gthy =
+fun context_begin_nested_cmd raw_includes raw_elems gthy =
gthy
|> Context.cases Named_Target.theory_init Local_Theory.assert
- |> includes raw_incls
+ |> includes raw_includes
|> Expression.read_declaration ([], []) I raw_elems
|> (#4 o fst)
|> Local_Theory.begin_nested
--- a/src/Pure/Pure.thy Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/Pure.thy Sun Nov 01 16:54:49 2020 +0100
@@ -627,7 +627,7 @@
val _ =
Outer_Syntax.command \<^command_keyword>\<open>context\<close> "begin local theory context"
((Parse.name_position
- >> (fn name => Toplevel.begin_main_target true (Target_Context.context_begin_named_cmd name)) ||
+ >> (fn name => Toplevel.begin_main_target true (Target_Context.context_begin_named_cmd [] name)) ||
Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
>> (fn (incls, elems) => Toplevel.begin_nested_target (Target_Context.context_begin_nested_cmd incls elems)))
--| Parse.begin);
@@ -646,18 +646,21 @@
ML \<open>
local
+val locale_context_elements =
+ Scan.optional Parse_Spec.includes [] -- Scan.repeat1 Parse_Spec.context_element;
+
val locale_val =
Parse_Spec.locale_expression --
- Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
- Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
+ Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! locale_context_elements) ([], []) ||
+ locale_context_elements >> pair ([], []);
val _ =
Outer_Syntax.command \<^command_keyword>\<open>locale\<close> "define named specification context"
(Parse.binding --
- Scan.optional (\<^keyword>\<open>=\<close> |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
- >> (fn ((name, (expr, elems)), begin) =>
+ Scan.optional (\<^keyword>\<open>=\<close> |-- Parse.!!! locale_val) (([], []), ([], [])) -- Parse.opt_begin
+ >> (fn ((name, (expr, (includes, elems))), begin) =>
Toplevel.begin_main_target begin
- (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
+ (Expression.add_locale_cmd name Binding.empty includes expr elems #> snd)));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>experiment\<close> "open private specification context"
@@ -706,17 +709,20 @@
ML \<open>
local
+val class_context_elements =
+ Scan.optional Parse_Spec.includes [] -- Scan.repeat1 Parse_Spec.context_element;
+
val class_val =
Parse_Spec.class_expression --
- Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
- Scan.repeat1 Parse_Spec.context_element >> pair [];
+ Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! class_context_elements) ([], []) ||
+ class_context_elements >> pair [];
val _ =
Outer_Syntax.command \<^command_keyword>\<open>class\<close> "define type class"
- (Parse.binding -- Scan.optional (\<^keyword>\<open>=\<close> |-- class_val) ([], []) -- Parse.opt_begin
- >> (fn ((name, (supclasses, elems)), begin) =>
+ (Parse.binding -- Scan.optional (\<^keyword>\<open>=\<close> |-- class_val) ([], ([], [])) -- Parse.opt_begin
+ >> (fn ((name, (supclasses, (includes, elems))), begin) =>
Toplevel.begin_main_target begin
- (Class_Declaration.class_cmd name supclasses elems #> snd)));
+ (Class_Declaration.class_cmd name includes supclasses elems #> snd)));
val _ =
Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>subclass\<close> "prove a subclass relation"
--- a/src/Pure/ROOT.ML Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/ROOT.ML Sun Nov 01 16:54:49 2020 +0100
@@ -260,6 +260,7 @@
(*local theories and targets*)
ML_file "Isar/locale.ML";
ML_file "Isar/generic_target.ML";
+ML_file "Isar/bundle.ML";
ML_file "Isar/overloading.ML";
ML_file "axclass.ML";
ML_file "Isar/class.ML";
@@ -267,10 +268,8 @@
ML_file "Isar/expression.ML";
ML_file "Isar/interpretation.ML";
ML_file "Isar/class_declaration.ML";
-ML_file "Isar/bundle.ML";
ML_file "Isar/target_context.ML";
ML_file "Isar/experiment.ML";
-
ML_file "simplifier.ML";
ML_file "Tools/plugin.ML";