--- a/Admin/components/components.sha1 Thu May 18 11:44:42 2023 +0100
+++ b/Admin/components/components.sha1 Mon May 22 12:01:05 2023 +0200
@@ -374,6 +374,7 @@
7056b285af67902b32f5049349a064f073f05860 polyml-5.9-cc80e2b43c38.tar.gz
0c396bd6b46ff11a2432b91aab2be0248bd9b0a4 polyml-5.9.tar.gz
f399ab9ee4a586fddeb6e73ca3605af65a89f969 polyml-5e9c8155ea96.tar.gz
+2cea4dd48bb8b171bc04c9793a55c7fa4c2d96f1 polyml-a5d5fba90286.tar.gz
49f1adfacdd6d29fa9f72035d94a31eaac411a97 polyml-test-0a6ebca445fc.tar.gz
2a8c4421e0a03c0d6ad556b3c36c34eb11568adb polyml-test-1236652ebd55.tar.gz
8e83fb5088cf265902b8da753a8eac5fe3f6a14b polyml-test-159dc81efc3b.tar.gz
--- a/Admin/components/main Thu May 18 11:44:42 2023 +0100
+++ b/Admin/components/main Mon May 22 12:01:05 2023 +0200
@@ -25,7 +25,7 @@
nunchaku-0.5
opam-2.0.7
pdfjs-2.14.305
-polyml-5e9c8155ea96
+polyml-a5d5fba90286
postgresql-42.5.0
prismjs-1.29.0
rsync-3.2.7
--- a/src/Doc/Implementation/Proof.thy Thu May 18 11:44:42 2023 +0100
+++ b/src/Doc/Implementation/Proof.thy Mon May 22 12:01:05 2023 +0200
@@ -270,7 +270,8 @@
cterm list -> Proof.context -> thm list * Proof.context"} \\
@{define_ML Assumption.add_assumes: "
cterm list -> Proof.context -> thm list * Proof.context"} \\
- @{define_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\
+ @{define_ML Assumption.export: "Proof.context -> Proof.context -> thm -> thm"} \\
+ @{define_ML Assumption.export_goal: "Proof.context -> Proof.context -> thm -> thm"} \\
@{define_ML Assumption.export_term: "Proof.context -> Proof.context -> term -> term"} \\
\end{mldecls}
@@ -290,11 +291,12 @@
\<^ML>\<open>Assumption.add_assms\<close> where the export rule performs \<open>\<Longrightarrow>\<hyphen>intro\<close> or
\<open>#\<Longrightarrow>\<hyphen>intro\<close>, depending on goal mode.
- \<^descr> \<^ML>\<open>Assumption.export\<close>~\<open>is_goal inner outer thm\<close> exports result \<open>thm\<close>
- from the \<open>inner\<close> context back into the \<open>outer\<close> one; \<open>is_goal = true\<close> means
- this is a goal context. The result is in HHF normal form. Note that
- \<^ML>\<open>Proof_Context.export\<close> combines \<^ML>\<open>Variable.export\<close> and
- \<^ML>\<open>Assumption.export\<close> in the canonical way.
+ \<^descr> \<^ML>\<open>Assumption.export\<close>~\<open>inner outer thm\<close> exports result \<open>thm\<close> from the
+ \<open>inner\<close> context back into the \<open>outer\<close> one; \<^ML>\<open>Assumption.export_goal\<close>
+ does the same in a goal context (\<^theory_text>\<open>fix/assume/show\<close> in Isabelle/Isar). The
+ result is always in HHF normal form. Note that \<^ML>\<open>Proof_Context.export\<close>
+ combines \<^ML>\<open>Variable.export\<close> and \<^ML>\<open>Assumption.export\<close> in the
+ canonical way.
\<^descr> \<^ML>\<open>Assumption.export_term\<close>~\<open>inner outer t\<close> exports term \<open>t\<close> from the
\<open>inner\<close> context back into the \<open>outer\<close> one. This is analogous to
@@ -318,7 +320,7 @@
val eq' = Thm.symmetric eq;
(*back to original context -- discharges assumption*)
- val r = Assumption.export false ctxt1 ctxt0 eq';
+ val r = Assumption.export ctxt1 ctxt0 eq';
\<close>
text \<open>
--- a/src/Doc/Isar_Ref/Spec.thy Thu May 18 11:44:42 2023 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Mon May 22 12:01:05 2023 +0200
@@ -417,7 +417,7 @@
@@{command declare} (@{syntax thms} + @'and')
\<close>
- \<^descr> \<^theory_text>\<open>declaration d\<close> adds the declaration function \<open>d\<close> of ML type \<^ML_type>\<open>declaration\<close>, to the current local theory under construction. In later
+ \<^descr> \<^theory_text>\<open>declaration d\<close> adds the declaration function \<open>d\<close> of ML type \<^ML_type>\<open>Morphism.declaration\<close>, to the current local theory under construction. In later
application contexts, the function is transformed according to the morphisms
being involved in the interpretation hierarchy.
--- a/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Mon May 22 12:01:05 2023 +0200
@@ -15,7 +15,7 @@
val funs: thm ->
{isolate_conv: morphism -> Proof.context -> cterm list -> cterm -> thm,
whatis: morphism -> cterm -> cterm -> ord,
- simpset: morphism -> Proof.context -> simpset} -> declaration
+ simpset: morphism -> Proof.context -> simpset} -> Morphism.declaration
val match: Proof.context -> cterm -> entry option
end;
--- a/src/HOL/Parity.thy Thu May 18 11:44:42 2023 +0100
+++ b/src/HOL/Parity.thy Mon May 22 12:01:05 2023 +0200
@@ -1311,24 +1311,22 @@
let
val thm = Simplifier.rewrite ctxt ct
in if Thm.is_reflexive thm then NONE else SOME thm end;
- in fn phi =>
- let
- val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
- one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
- one_div_minus_numeral one_mod_minus_numeral
- numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
- numeral_div_minus_numeral numeral_mod_minus_numeral
- div_minus_minus mod_minus_minus Parity.adjust_div_eq of_bool_eq one_neq_zero
- numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
- divmod_cancel divmod_steps divmod_step_def fst_conv snd_conv numeral_One
- case_prod_beta rel_simps Parity.adjust_mod_def div_minus1_right mod_minus1_right
- minus_minus numeral_times_numeral mult_zero_right mult_1_right
- euclidean_size_nat_less_eq_iff euclidean_size_int_less_eq_iff diff_nat_numeral nat_numeral}
- @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]);
- fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
- (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps)
- in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end
- end
+ val simps = @{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
+ one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
+ one_div_minus_numeral one_mod_minus_numeral
+ numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
+ numeral_div_minus_numeral numeral_mod_minus_numeral
+ div_minus_minus mod_minus_minus Parity.adjust_div_eq of_bool_eq one_neq_zero
+ numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
+ divmod_cancel divmod_steps divmod_step_def fst_conv snd_conv numeral_One
+ case_prod_beta rel_simps Parity.adjust_mod_def div_minus1_right mod_minus1_right
+ minus_minus numeral_times_numeral mult_zero_right mult_1_right
+ euclidean_size_nat_less_eq_iff euclidean_size_int_less_eq_iff diff_nat_numeral nat_numeral}
+ @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}];
+ val simpset =
+ HOL_ss |> Simplifier.simpset_map \<^context>
+ (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps);
+ in K (fn ctxt => successful_rewrite (Simplifier.put_simpset simpset ctxt)) end
\<close> \<comment> \<open>
There is space for improvement here: the calculation itself
could be carried out outside the logic, and a generic simproc
--- a/src/HOL/Statespace/state_space.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/HOL/Statespace/state_space.ML Mon May 22 12:01:05 2023 +0200
@@ -228,12 +228,14 @@
else (tracing ("variable not fixed or declared: " ^ name); NONE)
-val get_dist_thm = Symtab.lookup o get_distinctthm;
+fun get_dist_thm context name =
+ Symtab.lookup_list (get_distinctthm context) name
+ |> map (Thm.transfer'' context)
fun get_dist_thm2 ctxt x y =
(let
val dist_thms = [x, y] |> map (#1 o dest_Free)
- |> map (these o get_dist_thm (Context.Proof ctxt)) |> flat;
+ |> maps (get_dist_thm (Context.Proof ctxt));
fun get_paths dist_thm =
let
@@ -331,7 +333,8 @@
val declinfo = get_declinfo context
val tt = get_distinctthm context;
val all_names = comps_of_distinct_thm thm;
- fun upd name = Symtab.map_default (name, [thm]) (insert_distinct_thm thm)
+ val thm0 = Thm.trim_context thm;
+ fun upd name = Symtab.map_default (name, [thm0]) (insert_distinct_thm thm0)
val tt' = tt |> fold upd all_names;
val context' =
--- a/src/HOL/Tools/Function/partial_function.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML Mon May 22 12:01:05 2023 +0200
@@ -6,7 +6,7 @@
signature PARTIAL_FUNCTION =
sig
- val init: string -> term -> term -> thm -> thm -> thm option -> declaration
+ val init: string -> term -> term -> thm -> thm -> thm option -> Morphism.declaration
val mono_tac: Proof.context -> int -> tactic
val add_partial_function: string -> (binding * typ option * mixfix) list ->
Attrib.binding * term -> local_theory -> (term * thm) * local_theory
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon May 22 12:01:05 2023 +0200
@@ -245,9 +245,7 @@
val dummy_thm = Thm.transfer thy Drule.dummy_thm
val restore_lifting_att =
- ([dummy_thm],
- [map (Token.make_string o rpair Position.none)
- ["Lifting.lifting_restore_internal", bundle_name]])
+ ([dummy_thm], [map Token.make_string0 ["Lifting.lifting_restore_internal", bundle_name]])
in
lthy
|> Local_Theory.declaration {syntax = false, pervasive = true}
--- a/src/HOL/Tools/groebner.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/HOL/Tools/groebner.ML Mon May 22 12:01:05 2023 +0200
@@ -781,7 +781,7 @@
in
Simplifier.cert_simproc (Thm.theory_of_thm idl_sub) "poly_eq_simproc"
{lhss = [Thm.term_of (Thm.lhs_of idl_sub)],
- proc = fn _ => fn _ => proc}
+ proc = Morphism.entity (fn _ => fn _ => proc)}
end;
val poly_eq_ss =
--- a/src/Pure/Admin/build_release.scala Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Admin/build_release.scala Mon May 22 12:01:05 2023 +0200
@@ -242,7 +242,7 @@
ssh.write_file(remote_tmp_tar, local_tmp_tar)
val build_command =
- "bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions)
+ "bin/isabelle build -o parallel_proofs=0 -o system_heaps -b -- " + Bash.strings(build_sessions)
def system_apple(b: Boolean): String =
"""{ echo "ML_system_apple = """ + b + """" > "$(bin/isabelle getenv -b ISABELLE_HOME_USER)/etc/preferences"; }"""
--- a/src/Pure/General/basics.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/General/basics.ML Mon May 22 12:01:05 2023 +0200
@@ -32,6 +32,7 @@
val the_default: 'a -> 'a option -> 'a
val perhaps: ('a -> 'a option) -> 'a -> 'a
val merge_options: 'a option * 'a option -> 'a option
+ val join_options: ('a * 'a -> 'a) -> 'a option * 'a option -> 'a option
val eq_option: ('a * 'b -> bool) -> 'a option * 'b option -> bool
(*partiality*)
@@ -94,6 +95,9 @@
fun merge_options (x, y) = if is_some x then x else y;
+fun join_options f (SOME x, SOME y) = SOME (f (x, y))
+ | join_options _ args = merge_options args;
+
fun eq_option eq (SOME x, SOME y) = eq (x, y)
| eq_option _ (NONE, NONE) = true
| eq_option _ _ = false;
--- a/src/Pure/Isar/args.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/args.ML Mon May 22 12:01:05 2023 +0200
@@ -36,15 +36,16 @@
val internal_typ: typ parser
val internal_term: term parser
val internal_fact: thm list parser
- val internal_attribute: (morphism -> attribute) parser
- val internal_declaration: declaration parser
+ val internal_attribute: attribute Morphism.entity parser
+ val internal_declaration: Morphism.declaration_entity parser
val named_source: (Token.T -> Token.src) -> Token.src parser
val named_typ: (string -> typ) -> typ parser
val named_term: (string -> term) -> term parser
val named_fact: (string -> string option * thm list) -> thm list parser
- val named_attribute: (string * Position.T -> morphism -> attribute) ->
- (morphism -> attribute) parser
- val embedded_declaration: (Input.source -> declaration) -> declaration parser
+ val named_attribute: (string * Position.T -> attribute Morphism.entity) ->
+ attribute Morphism.entity parser
+ val embedded_declaration: (Input.source -> Morphism.declaration_entity) ->
+ Morphism.declaration_entity parser
val typ_abbrev: typ context_parser
val typ: typ context_parser
val term: term context_parser
--- a/src/Pure/Isar/attrib.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/attrib.ML Mon May 22 12:01:05 2023 +0200
@@ -49,7 +49,7 @@
val attribute_setup: bstring * Position.T -> Input.source -> string ->
local_theory -> local_theory
val internal: (morphism -> attribute) -> Token.src
- val internal_declaration: declaration -> thms
+ val internal_declaration: Morphism.declaration_entity -> thms
val add_del: attribute -> attribute -> attribute context_parser
val thm: thm context_parser
val thms: thm list context_parser
@@ -169,7 +169,7 @@
val name = #1 (Token.name_of_src src);
val label = Long_Name.qualify Markup.attributeN name;
val att = #1 (Name_Space.get table name) src;
- in Position.setmp_thread_data_label label att end
+ in Position.setmp_thread_data_label label att : attribute end
end;
val attribute = attribute_generic o Context.Proof;
@@ -187,12 +187,19 @@
fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
-(* fact expressions *)
+(* implicit context *)
+
+val trim_context_binding: Attrib.binding -> Attrib.binding =
+ apsnd ((map o map) Token.trim_context);
-val trim_context_binding: Attrib.binding -> Attrib.binding = apsnd (map Token.trim_context_src);
-val trim_context_thms: thms -> thms = (map o apfst o map) Thm.trim_context;
+val trim_context_thms: thms -> thms =
+ map (fn (thms, atts) => (map Thm.trim_context thms, (map o map) Token.trim_context atts));
+
fun trim_context_fact (binding, thms) = (trim_context_binding binding, trim_context_thms thms);
+
+(* fact expressions *)
+
fun global_notes kind facts thy = thy |>
Global_Theory.note_thmss kind (map_facts (map (attribute_global thy)) facts);
@@ -230,23 +237,29 @@
(* internal attribute *)
-val _ = Theory.setup
- (setup (Binding.make ("attribute", \<^here>))
- (Scan.lift Args.internal_attribute >> Morphism.form)
- "internal attribute");
-
-fun internal_name ctxt name =
+fun make_name ctxt name =
Token.make_src (name, Position.none) [] |> check_src ctxt |> hd;
-val internal_attribute_name =
- internal_name (Context.the_local_context ()) "attribute";
+local
+
+val internal_binding = Binding.make ("attribute", \<^here>);
+
+val _ = Theory.setup
+ (setup internal_binding
+ (Scan.lift Args.internal_attribute >> Morphism.form ||
+ Scan.lift Args.internal_declaration >> (Thm.declaration_attribute o K o Morphism.form))
+ "internal attribute");
-fun internal att =
- internal_attribute_name ::
- [Token.make_string ("<attribute>", Position.none) |> Token.assign (SOME (Token.Attribute att))];
+val internal_name = make_name (Context.the_local_context ()) (Binding.name_of internal_binding);
+val internal_arg = Token.make_string0 "<attribute>";
+fun internal_source value = [internal_name, Token.assign (SOME value) internal_arg];
-fun internal_declaration decl =
- [([Drule.dummy_thm], [internal (fn phi => Thm.declaration_attribute (K (decl phi)))])];
+in
+
+fun internal arg = internal_source (Token.Attribute (Morphism.entity arg));
+fun internal_declaration arg = [([Drule.dummy_thm], [internal_source (Token.Declaration arg)])];
+
+end;
(* add/del syntax *)
@@ -426,7 +439,8 @@
fun register binding config thy =
let val name = Sign.full_name thy binding in
thy
- |> setup binding (Scan.lift (scan_config thy config) >> Morphism.form) "configuration option"
+ |> setup binding (Scan.lift (scan_config thy config) >> Morphism.form_entity)
+ "configuration option"
|> Configs.map (Symtab.update (name, config))
end;
@@ -623,23 +637,21 @@
local
-val internal = internal_name (Context.the_local_context ());
+val make_name0 = make_name (Context.the_local_context ());
-val consumes_name = internal "consumes";
-val constraints_name = internal "constraints";
-val cases_open_name = internal "cases_open";
-val case_names_name = internal "case_names";
-val case_conclusion_name = internal "case_conclusion";
-
-fun make_string s = Token.make_string (s, Position.none);
+val consumes_name = make_name0 "consumes";
+val constraints_name = make_name0 "constraints";
+val cases_open_name = make_name0 "cases_open";
+val case_names_name = make_name0 "case_names";
+val case_conclusion_name = make_name0 "case_conclusion";
in
fun consumes i = consumes_name :: Token.make_int i;
fun constraints i = constraints_name :: Token.make_int i;
val cases_open = [cases_open_name];
-fun case_names names = case_names_name :: map make_string names;
-fun case_conclusion (name, names) = case_conclusion_name :: map make_string (name :: names);
+fun case_names names = case_names_name :: map Token.make_string0 names;
+fun case_conclusion (name, names) = case_conclusion_name :: map Token.make_string0 (name :: names);
end;
--- a/src/Pure/Isar/bundle.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/bundle.ML Mon May 22 12:01:05 2023 +0200
@@ -59,13 +59,6 @@
fun extern ctxt = Name_Space.extern ctxt (Name_Space.space_of_table (get_all ctxt));
-fun define_bundle (b, bundle) context =
- let
- val bundle' = Attrib.trim_context_thms bundle;
- val (name, bundles') = Name_Space.define context true (b, bundle') (get_all_generic context);
- val context' = (Data.map o apfst o K) bundles' context;
- in (name, context') end;
-
(* target -- bundle under construction *)
@@ -102,9 +95,24 @@
(** define bundle **)
+(* context and morphisms *)
+
+val trim_context_bundle =
+ map (fn (fact, atts) => (map Thm.trim_context fact, (map o map) Token.trim_context atts));
+
+fun transfer_bundle thy =
+ map (fn (fact, atts) => (map (Thm.transfer thy) fact, (map o map) (Token.transfer thy) atts));
+
fun transform_bundle phi =
map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts));
+fun define_bundle (b, bundle) context =
+ let
+ val (name, bundles') = get_all_generic context
+ |> Name_Space.define context true (b, trim_context_bundle bundle);
+ val context' = (Data.map o apfst o K) bundles' context;
+ in (name, context') end;
+
(* command *)
@@ -116,11 +124,15 @@
val bundle0 = raw_bundle
|> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts));
val bundle =
- Attrib.partial_evaluation ctxt' [(Binding.empty_atts, bundle0)] |> map snd |> flat
- |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);
+ Attrib.partial_evaluation ctxt' [(Binding.empty_atts, bundle0)]
+ |> maps #2
+ |> transform_bundle (Proof_Context.export_morphism ctxt' lthy)
+ |> trim_context_bundle;
in
lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => #2 o define_bundle (Morphism.binding phi binding, transform_bundle phi bundle))
+ (fn phi => fn context =>
+ let val psi = Morphism.set_trim_context'' context phi
+ in #2 (define_bundle (Morphism.binding psi binding, transform_bundle psi bundle) context) end)
end;
in
@@ -200,7 +212,10 @@
local
fun gen_activate notes prep_bundle args ctxt =
- let val decls = maps (prep_bundle ctxt) args in
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val decls = maps (prep_bundle ctxt) args |> transfer_bundle thy;
+ in
ctxt
|> Context_Position.set_visible false
|> notes [(Binding.empty_atts, decls)] |> #2
--- a/src/Pure/Isar/class.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/class.ML Mon May 22 12:01:05 2023 +0200
@@ -157,9 +157,9 @@
val base_morphism = #base_morph oo the_class_data;
fun morphism thy class =
- (case Element.eq_morphism thy (these_defs thy [class]) of
- SOME eq_morph => base_morphism thy class $> eq_morph
- | NONE => base_morphism thy class);
+ Morphism.set_context thy
+ (base_morphism thy class $>
+ Morphism.default (Element.eq_morphism (these_defs thy [class])));
val export_morphism = #export_morph oo the_class_data;
@@ -221,21 +221,23 @@
(c, (class, ((ty, Free v_ty), false)))) params;
val add_class = Graph.new_node (class,
make_class_data (((map o apply2) fst params, base_sort,
- base_morph, export_morph, Option.map Thm.trim_context some_assm_intro,
- Thm.trim_context of_class, Option.map Thm.trim_context some_axiom),
+ Morphism.reset_context base_morph,
+ Morphism.reset_context export_morph,
+ Option.map Thm.trim_context some_assm_intro,
+ Thm.trim_context of_class,
+ Option.map Thm.trim_context some_axiom),
(Thm.item_net, operations)))
#> fold (curry Graph.add_edge class) sups;
in Class_Data.map add_class thy end;
fun activate_defs class thms thy =
- (case Element.eq_morphism thy thms of
+ (case Element.eq_morphism thms of
SOME eq_morph =>
- fold (fn cls => fn thy =>
- Context.theory_map
- (Locale.amend_registration
- {inst = (cls, base_morphism thy cls),
- mixin = SOME (eq_morph, true),
- export = export_morphism thy cls}) thy) (heritage thy [class]) thy
+ fold (fn cls => fn thy' =>
+ (Context.theory_map o Locale.amend_registration)
+ {inst = (cls, base_morphism thy' cls),
+ mixin = SOME (eq_morph, true),
+ export = export_morphism thy' cls} thy') (heritage thy [class]) thy
| NONE => thy);
fun register_operation class (c, t) input_only thy =
@@ -358,7 +360,8 @@
fun target_const class phi0 prmode (b, rhs) lthy =
let
- val export = Variable.export_morphism lthy (Local_Theory.target_of lthy);
+ val export =
+ Morphism.set_context' lthy (Variable.export_morphism lthy (Local_Theory.target_of lthy));
val guess_identity = guess_morphism_identity (b, rhs) export;
val guess_canonical = guess_morphism_identity (b, rhs) (export $> phi0);
in
@@ -478,9 +481,11 @@
fun register_subclass (sub, sup) some_dep_morph some_witn export lthy =
let
val thy = Proof_Context.theory_of lthy;
- val intros = (snd o rules thy) sup :: map_filter I
- [Option.map (Drule.export_without_context_open o Element.conclude_witness lthy) some_witn,
- (fst o rules thy) sub];
+ val conclude_witness =
+ Thm.trim_context o Drule.export_without_context_open o Element.conclude_witness lthy;
+ val intros =
+ (snd o rules thy) sup ::
+ map_filter I [Option.map conclude_witness some_witn, (fst o rules thy) sub];
val classrel =
Goal.prove_sorry_global thy [] [] (Logic.mk_classrel (sub, sup))
(fn {context = ctxt, ...} => EVERY (map (TRYALL o resolve_tac ctxt o single) intros));
--- a/src/Pure/Isar/class_declaration.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/class_declaration.ML Mon May 22 12:01:05 2023 +0200
@@ -31,6 +31,7 @@
val certT = Thm.trim_context_ctyp o Thm.global_ctyp_of thy;
val cert = Thm.trim_context_cterm o Thm.global_cterm_of thy;
+ val conclude_witness = Thm.trim_context o Element.conclude_witness thy_ctxt;
(* instantiation of canonical interpretation *)
val a_tfree = (Name.aT, base_sort);
@@ -67,13 +68,15 @@
val tac = loc_intro_tac
THEN ALLGOALS (Proof_Context.fact_tac thy_ctxt (sup_axioms @ the_list assm_axiom));
in Element.prove_witness thy_ctxt prop tac end) some_prop;
- val some_axiom = Option.map (Element.conclude_witness thy_ctxt) some_witn;
+ val some_axiom = Option.map conclude_witness some_witn;
(* canonical interpretation *)
val base_morph = inst_morph
$> Morphism.binding_morphism "class_binding" (Binding.prefix false (Class.class_prefix class))
$> Element.satisfy_morphism (the_list some_witn);
- val eq_morph = Element.eq_morphism thy (Class.these_defs thy sups);
+ val eq_morph =
+ Element.eq_morphism (Class.these_defs thy sups)
+ |> Option.map (Morphism.set_context thy);
(* assm_intro *)
fun prove_assm_intro thm =
--- a/src/Pure/Isar/code.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/code.ML Mon May 22 12:01:05 2023 +0200
@@ -393,21 +393,23 @@
type data = Any.T Datatab.table;
-fun make_dataref thy =
- (Context.theory_long_name thy,
- Synchronized.var "code data" (NONE : (data * Context.theory_id) option));
+fun make_dataref () =
+ Synchronized.var "code data" (NONE : (data * Context.theory_id) option);
structure Code_Data = Theory_Data
(
type T = specs * (string * (data * Context.theory_id) option Synchronized.var);
- val empty = (empty_specs, make_dataref (Context.the_global_context ()));
+ val empty =
+ (empty_specs, (Context.theory_long_name (Context.the_global_context ()), make_dataref ()));
fun merge ((specs1, dataref), (specs2, _)) =
(merge_specs (specs1, specs2), dataref);
);
fun init_dataref thy =
- if #1 (#2 (Code_Data.get thy)) = Context.theory_long_name thy then NONE
- else SOME ((Code_Data.map o apsnd) (fn _ => make_dataref thy) thy)
+ let val thy_name = Context.theory_long_name thy in
+ if #1 (#2 (Code_Data.get thy)) = thy_name then NONE
+ else SOME ((Code_Data.map o apsnd) (K (thy_name, make_dataref ())) thy)
+ end;
in
@@ -419,7 +421,8 @@
val specs_of : theory -> specs = fst o Code_Data.get;
fun modify_specs f thy =
- Code_Data.map (fn (specs, _) => (f specs, make_dataref thy)) thy;
+ let val thy_name = Context.theory_long_name thy
+ in Code_Data.map (fn (specs, _) => (f specs, (thy_name, make_dataref ()))) thy end;
(* access to data dependent on executable specifications *)
@@ -569,7 +572,7 @@
fun get_abstype_spec thy tyco = case lookup_vs_type_spec thy tyco of
SOME (vs, Abstractor {abs_rep, abstractor, projection, ...}) =>
- (vs, {abs_rep = abs_rep, abstractor = abstractor, projection = projection})
+ (vs, {abs_rep = Thm.transfer thy abs_rep, abstractor = abstractor, projection = projection})
| _ => error ("Not an abstract type: " ^ tyco);
fun get_type_of_constr_or_abstr thy c =
@@ -1014,13 +1017,13 @@
Abstract (snd (constrain_thm thy (fst (typscheme_abs thy abs_thm)) sorts abs_thm), tyco);
fun conclude_cert (Nothing cert_thm) =
- Nothing (Thm.close_derivation \<^here> cert_thm)
+ Nothing (Thm.close_derivation \<^here> cert_thm |> Thm.trim_context)
| conclude_cert (Equations (cert_thm, propers)) =
- Equations (Thm.close_derivation \<^here> cert_thm, propers)
+ Equations (Thm.close_derivation \<^here> cert_thm |> Thm.trim_context, propers)
| conclude_cert (cert as Projection _) =
cert
| conclude_cert (Abstract (abs_thm, tyco)) =
- Abstract (Thm.close_derivation \<^here> abs_thm, tyco);
+ Abstract (Thm.close_derivation \<^here> abs_thm |> Thm.trim_context, tyco);
fun typscheme_of_cert thy (Nothing cert_thm) =
fst (get_head thy cert_thm)
@@ -1057,6 +1060,7 @@
val tyscm = typscheme_of_cert thy cert;
val thms = if null propers then [] else
cert_thm
+ |> Thm.transfer thy
|> Local_Defs.expand [snd (get_head thy cert_thm)]
|> Thm.varifyT_global
|> Conjunction.elim_balanced (length propers);
@@ -1072,7 +1076,7 @@
| equations_of_cert thy (Abstract (abs_thm, tyco)) =
let
val tyscm = typscheme_abs thy abs_thm;
- val (abs, concrete_thm) = concretify_abs thy tyco abs_thm;
+ val (abs, concrete_thm) = concretify_abs thy tyco (Thm.transfer thy abs_thm);
fun abstractions (args, rhs) = (map (pair NONE) args, (SOME abs, rhs));
in
(tyscm, SOME [((abstractions o dest_eqn o Thm.prop_of) concrete_thm,
@@ -1305,20 +1309,10 @@
(* abstract code declarations *)
-local
-
-fun generic_code_declaration strictness lift_phi f x =
- Local_Theory.declaration
- {syntax = false, pervasive = false}
+fun code_declaration strictness lift_phi f x =
+ Local_Theory.declaration {syntax = false, pervasive = false}
(fn phi => Context.mapping (f strictness (lift_phi phi x)) I);
-in
-
-fun silent_code_declaration lift_phi = generic_code_declaration Silent lift_phi;
-fun code_declaration lift_phi = generic_code_declaration Liberal lift_phi;
-
-end;
-
(* types *)
@@ -1363,16 +1357,15 @@
SOME (tyco, (vs, (abstractor as (abs, (_, ty)), (proj, abs_rep)))) =>
thy
|> modify_specs (register_type
- (tyco, (vs, Abstractor {abstractor = abstractor, projection = proj, abs_rep = abs_rep, more_abstract_functions = []}))
+ (tyco, (vs, Abstractor {abstractor = abstractor, projection = proj,
+ abs_rep = Thm.trim_context abs_rep, more_abstract_functions = []}))
#> register_fun_spec proj
(Proj (Logic.varify_types_global (mk_proj tyco vs ty abs proj), (tyco, abs))))
|> register_tyco_for_plugin tyco
| NONE => thy;
val declare_abstype_global = generic_declare_abstype Strict;
-
-val declare_abstype =
- code_declaration Morphism.thm generic_declare_abstype;
+val declare_abstype = code_declaration Liberal Morphism.thm generic_declare_abstype;
(* functions *)
@@ -1422,7 +1415,7 @@
else specs);
fun add_abstract_for (c, (thm, tyco_abs as (tyco, _))) =
- modify_specs (register_fun_spec c (Abstr (Thm.close_derivation \<^here> thm, tyco_abs))
+ modify_specs (register_fun_spec c (Abstr (Thm.close_derivation \<^here> thm |> Thm.trim_context, tyco_abs))
#> map_types (History.modify_entry tyco (add_abstract_function c)))
in
@@ -1445,14 +1438,10 @@
end;
val declare_default_eqns_global = generic_declare_eqns true Silent;
-
-val declare_default_eqns =
- silent_code_declaration (map o apfst o Morphism.thm) (generic_declare_eqns true);
+val declare_default_eqns = code_declaration Silent (map o apfst o Morphism.thm) (generic_declare_eqns true);
val declare_eqns_global = generic_declare_eqns false Strict;
-
-val declare_eqns =
- code_declaration (map o apfst o Morphism.thm) (generic_declare_eqns false);
+val declare_eqns = code_declaration Liberal (map o apfst o Morphism.thm) (generic_declare_eqns false);
val add_eqn_global = generic_add_eqn Strict;
@@ -1463,9 +1452,7 @@
| NONE => thy;
val declare_abstract_eqn_global = generic_declare_abstract_eqn Strict;
-
-val declare_abstract_eqn =
- code_declaration Morphism.thm generic_declare_abstract_eqn;
+val declare_abstract_eqn = code_declaration Liberal Morphism.thm generic_declare_abstract_eqn;
fun declare_aborting_global c =
modify_specs (register_fun_spec c aborting);
--- a/src/Pure/Isar/element.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/element.ML Mon May 22 12:01:05 2023 +0200
@@ -29,6 +29,8 @@
('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
val map_ctxt_attrib: (Token.src -> Token.src) ->
('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt
+ val trim_context_ctxt: context_i -> context_i
+ val transfer_ctxt: theory -> context_i -> context_i
val transform_ctxt: morphism -> context_i -> context_i
val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
@@ -49,8 +51,8 @@
val pretty_witness: Proof.context -> witness -> Pretty.T
val instantiate_normalize_morphism: ctyp TFrees.table * cterm Frees.table -> morphism
val satisfy_morphism: witness list -> morphism
- val eq_term_morphism: theory -> term list -> morphism option
- val eq_morphism: theory -> thm list -> morphism option
+ val eq_term_morphism: term list -> morphism option
+ val eq_morphism: thm list -> morphism option
val init: context_i -> Context.generic -> Context.generic
val activate_i: context_i -> Proof.context -> context_i * Proof.context
val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
@@ -103,6 +105,16 @@
fun map_ctxt_attrib attrib =
map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = I, attrib = attrib};
+val trim_context_ctxt: context_i -> context_i = map_ctxt
+ {binding = I, typ = I, term = I, pattern = I,
+ fact = map Thm.trim_context,
+ attrib = map Token.trim_context};
+
+fun transfer_ctxt thy: context_i -> context_i = map_ctxt
+ {binding = I, typ = I, term = I, pattern = I,
+ fact = map (Thm.transfer thy),
+ attrib = map (Token.transfer thy)};
+
fun transform_ctxt phi = map_ctxt
{binding = Morphism.binding phi,
typ = Morphism.typ phi,
@@ -275,7 +287,8 @@
Witness (t,
Goal.prove ctxt [] [] (mark_witness t)
(fn _ => resolve_tac ctxt [Drule.protectI] 1 THEN tac)
- |> Thm.close_derivation \<^here>);
+ |> Thm.close_derivation \<^here>
+ |> Thm.trim_context);
local
@@ -290,7 +303,9 @@
(map o map) (fn prop => (mark_witness prop, [])) wit_propss @
[map (rpair []) eq_props];
fun after_qed' thmss =
- let val (wits, eqs) = split_last ((map o map) (Thm.close_derivation \<^here>) thmss);
+ let
+ val (wits, eqs) =
+ split_last ((map o map) (Thm.close_derivation \<^here> #> Thm.trim_context) thmss);
in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
in proof after_qed' propss #> refine_witness end;
@@ -322,7 +337,7 @@
end;
fun conclude_witness ctxt (Witness (_, th)) =
- Goal.conclude th
+ Goal.conclude (Thm.transfer' ctxt th)
|> Raw_Simplifier.norm_hhf_protect ctxt
|> Thm.close_derivation \<^here>;
@@ -359,7 +374,7 @@
fun compose_witness (Witness (_, th)) r =
let
- val th' = Goal.conclude th;
+ val th' = Goal.conclude (Thm.transfer (Thm.theory_of_thm r) th);
val A = Thm.cprem_of r 1;
in
Thm.implies_elim
@@ -384,36 +399,42 @@
(* rewriting with equalities *)
(* for activating declarations only *)
-fun eq_term_morphism _ [] = NONE
- | eq_term_morphism thy props =
+fun eq_term_morphism [] = NONE
+ | eq_term_morphism props =
let
- fun decomp_simp prop =
+ fun decomp_simp ctxt prop =
let
- val ctxt = Proof_Context.init_global thy;
val _ = Logic.no_prems prop orelse
error ("Bad conditional rewrite rule " ^ Syntax.string_of_term ctxt prop);
- val lhsrhs = Logic.dest_equals prop
- handle TERM _ => error ("Rewrite rule not a meta-equality " ^ Syntax.string_of_term ctxt prop);
- in lhsrhs end;
+ in
+ Logic.dest_equals prop handle TERM _ =>
+ error ("Rewrite rule not a meta-equality " ^ Syntax.string_of_term ctxt prop)
+ end;
+ fun rewrite_term thy =
+ let val ctxt = Proof_Context.init_global thy
+ in Pattern.rewrite_term thy (map (decomp_simp ctxt) props) [] end;
val phi =
Morphism.morphism "Element.eq_term_morphism"
{binding = [],
typ = [],
- term = [Pattern.rewrite_term thy (map decomp_simp props) []],
- fact = [fn _ => error "Illegal application of Element.eq_term_morphism"]};
+ term = [rewrite_term o Morphism.the_theory],
+ fact = [fn _ => fn _ => error "Illegal application of Element.eq_term_morphism"]};
in SOME phi end;
-fun eq_morphism _ [] = NONE
- | eq_morphism thy thms =
+fun eq_morphism [] = NONE
+ | eq_morphism thms =
let
- (* FIXME proper context!? *)
- fun rewrite th = rewrite_rule (Proof_Context.init_global (Thm.theory_of_thm th)) thms th;
+ val thms0 = map Thm.trim_context thms;
+ fun rewrite_term thy =
+ Raw_Simplifier.rewrite_term thy (map (Thm.transfer thy) thms0) [];
+ fun rewrite thy =
+ Raw_Simplifier.rewrite_rule (Proof_Context.init_global thy) (map (Thm.transfer thy) thms0);
val phi =
Morphism.morphism "Element.eq_morphism"
{binding = [],
typ = [],
- term = [Raw_Simplifier.rewrite_term thy thms []],
- fact = [map rewrite]};
+ term = [rewrite_term o Morphism.the_theory],
+ fact = [map o rewrite o Morphism.the_theory]};
in SOME phi end;
--- a/src/Pure/Isar/expression.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/expression.ML Mon May 22 12:01:05 2023 +0200
@@ -406,8 +406,8 @@
val rewrite_morph = eqns'
|> map (abs_def ctxt')
|> Variable.export_terms ctxt' ctxt
- |> Element.eq_term_morphism (Proof_Context.theory_of ctxt)
- |> the_default Morphism.identity;
+ |> Element.eq_term_morphism
+ |> Morphism.default;
val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns'];
in (i + 1, insts', eqnss', ctxt'') end;
@@ -556,7 +556,7 @@
val exp_typ = Logic.type_map exp_term;
val export' =
Morphism.morphism "Expression.prep_goal"
- {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]};
+ {binding = [], typ = [K exp_typ], term = [K exp_term], fact = [K exp_fact]};
in ((propss, eq_propss, deps, eqnss, export'), goal_ctxt) end;
in
@@ -743,41 +743,41 @@
val ctxt = Proof_Context.init_global thy;
val defs' = map (Thm.cterm_of ctxt #> Assumption.assume ctxt #> Drule.abs_def) defs;
- val (a_pred, a_intro, a_axioms, thy'') =
+ val (a_pred, a_intro, a_axioms, thy2) =
if null exts then (NONE, NONE, [], thy)
else
let
val abinding =
if null ints then binding else Binding.suffix_name ("_" ^ axiomsN) binding;
- val ((statement, intro, axioms), thy') =
+ val ((statement, intro, axioms), thy1) =
thy
|> def_pred abinding parms defs' exts exts';
- val ((_, [intro']), thy'') =
- thy'
+ val ((_, [intro']), thy2) =
+ thy1
|> Sign.qualified_path true abinding
|> Global_Theory.note_thms ""
((Binding.name introN, []), [([intro], [Locale.unfold_add])])
- ||> Sign.restore_naming thy';
- in (SOME statement, SOME intro', axioms, thy'') end;
- val (b_pred, b_intro, b_axioms, thy'''') =
- if null ints then (NONE, NONE, [], thy'')
+ ||> Sign.restore_naming thy1;
+ in (SOME statement, SOME intro', axioms, thy2) end;
+ val (b_pred, b_intro, b_axioms, thy4) =
+ if null ints then (NONE, NONE, [], thy2)
else
let
- val ((statement, intro, axioms), thy''') =
- thy''
+ val ((statement, intro, axioms), thy3) =
+ thy2
|> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
- val ctxt''' = Proof_Context.init_global thy''';
- val ([(_, [intro']), _], thy'''') =
- thy'''
+ val conclude_witness =
+ Drule.export_without_context o Element.conclude_witness (Proof_Context.init_global thy3);
+ val ([(_, [intro']), _], thy4) =
+ thy3
|> Sign.qualified_path true binding
|> Global_Theory.note_thmss ""
[((Binding.name introN, []), [([intro], [Locale.intro_add])]),
((Binding.name axiomsN, []),
- [(map (Drule.export_without_context o Element.conclude_witness ctxt''') axioms,
- [])])]
- ||> Sign.restore_naming thy''';
- in (SOME statement, SOME intro', axioms, thy'''') end;
- in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end;
+ [(map conclude_witness axioms, [])])]
+ ||> Sign.restore_naming thy3;
+ in (SOME statement, SOME intro', axioms, thy4) end;
+ in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy4) end;
end;
@@ -794,7 +794,7 @@
fun defines_to_notes ctxt (Defines defs) =
Notes ("", map (fn (a, (def, _)) =>
(a, [([Assumption.assume ctxt (Thm.cterm_of ctxt def)],
- [(Attrib.internal o K) Locale.witness_add])])) defs)
+ [Attrib.internal (K Locale.witness_add)])])) defs)
| defines_to_notes _ e = e;
val is_hyp = fn Assumes _ => true | Defines _ => true | _ => false;
@@ -846,11 +846,12 @@
if is_some asm then
[("", [((Binding.suffix_name ("_" ^ axiomsN) binding, []),
[([Assumption.assume pred_ctxt (Thm.cterm_of pred_ctxt (the asm))],
- [(Attrib.internal o K) Locale.witness_add])])])]
+ [Attrib.internal (K Locale.witness_add)])])])]
else [];
val notes' =
body_elems
+ |> map (Element.transfer_ctxt thy')
|> map (defines_to_notes pred_ctxt)
|> map (Element.transform_ctxt a_satisfy)
|> (fn elems =>
--- a/src/Pure/Isar/generic_target.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML Mon May 22 12:01:05 2023 +0200
@@ -16,7 +16,7 @@
(*background primitives*)
val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
term list * term list -> local_theory -> (term * thm) * local_theory
- val background_declaration: declaration -> local_theory -> local_theory
+ val background_declaration: Morphism.declaration_entity -> local_theory -> local_theory
val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
val add_foundation_interpretation: (binding * (term * term list) -> Context.generic -> Context.generic) ->
theory -> theory
@@ -25,8 +25,8 @@
val standard_facts: local_theory -> Proof.context -> Attrib.fact list -> Attrib.fact list
val standard_notes: (int * int -> bool) -> string -> Attrib.fact list ->
local_theory -> local_theory
- val standard_declaration: (int * int -> bool) ->
- (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
+ val standard_declaration: (int * int -> bool) -> Morphism.declaration_entity ->
+ local_theory -> local_theory
val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
local_theory -> local_theory
val local_interpretation: Locale.registration ->
@@ -55,7 +55,7 @@
(*theory target operations*)
val theory_abbrev: Syntax.mode -> (binding * mixfix) * term ->
local_theory -> (term * term) * local_theory
- val theory_declaration: declaration -> local_theory -> local_theory
+ val theory_declaration: Morphism.declaration_entity -> local_theory -> local_theory
val theory_registration: Locale.registration -> local_theory -> local_theory
(*locale target primitives*)
@@ -63,14 +63,15 @@
local_theory -> local_theory
val locale_target_abbrev: string -> Syntax.mode ->
(binding * mixfix) -> term -> term list * term list -> local_theory -> local_theory
- val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
+ val locale_target_declaration: string -> bool -> Morphism.declaration_entity ->
+ local_theory -> local_theory
val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
(binding * mixfix) * term -> local_theory -> local_theory
(*locale operations*)
val locale_abbrev: string -> Syntax.mode -> (binding * mixfix) * term ->
local_theory -> (term * term) * local_theory
- val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration ->
+ val locale_declaration: string -> {syntax: bool, pervasive: bool} -> Morphism.declaration_entity ->
local_theory -> local_theory
val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
local_theory -> local_theory
@@ -123,7 +124,7 @@
| same_const (t $ _, t' $ _) = same_const (t, t')
| same_const (_, _) = false;
-fun const_decl phi_pred prmode ((b, mx), rhs) phi context =
+fun const_decl phi_pred prmode ((b, mx), rhs) = Morphism.entity (fn phi => fn context =>
if phi_pred phi then
let
val b' = Morphism.binding phi b;
@@ -149,7 +150,7 @@
SOME c =>
context
|> Context.mapping (Sign.const_alias b' c) (Proof_Context.const_alias b' c)
- |> Morphism.form (Proof_Context.generic_notation true prmode [(rhs', mx)])
+ |> Morphism.form_entity (Proof_Context.generic_notation true prmode [(rhs', mx)])
| NONE =>
context
|> Proof_Context.generic_add_abbrev Print_Mode.internal
@@ -157,9 +158,9 @@
|-> (fn (const as Const (c, _), _) => same_stem ?
(Proof_Context.generic_revert_abbrev (#1 prmode) c #>
same_shape ?
- Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
+ Morphism.form_entity (Proof_Context.generic_notation true prmode [(const, mx)]))))
end
- else context;
+ else context);
@@ -167,18 +168,18 @@
structure Foundation_Interpretations = Theory_Data
(
- type T = (binding * (term * term list) -> Context.generic -> Context.generic) Inttab.table;
- val empty = Inttab.empty;
- val merge = Inttab.merge (K true);
+ type T = ((binding * (term * term list) -> Context.generic -> Context.generic) * stamp) list
+ val empty = [];
+ val merge = Library.merge (eq_snd (op =));
);
fun add_foundation_interpretation f =
- Foundation_Interpretations.map (Inttab.update_new (serial (), f));
+ Foundation_Interpretations.map (cons (f, stamp ()));
fun foundation_interpretation binding_const_params lthy =
let
val interps = Foundation_Interpretations.get (Proof_Context.theory_of lthy);
- val interp = Inttab.fold (fn (_, f) => f binding_const_params) interps;
+ val interp = fold (fn (f, _) => f binding_const_params) interps;
in
lthy
|> Local_Theory.background_theory (Context.theory_map interp)
--- a/src/Pure/Isar/interpretation.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/interpretation.ML Mon May 22 12:01:05 2023 +0200
@@ -98,20 +98,20 @@
let
val factss = thms
|> unflat ((map o map) #1 eqnss)
- |> map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) #1 eqnss);
+ |> map2 (map2 (fn b => fn eq =>
+ (b, [([Morphism.thm export (Thm.transfer' ctxt eq)], [])]))) ((map o map) #1 eqnss);
val (eqnss', ctxt') =
fold_map (fn facts => note Thm.theoremK facts #-> abs_def_rule) factss ctxt;
val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]);
val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule;
+ val transform_witness = Element.transform_witness (Morphism.set_trim_context' ctxt' export');
val deps' =
(deps ~~ witss) |> map (fn ((dep, morph), wits) =>
- (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)));
+ (dep, morph $> Element.satisfy_morphism (map transform_witness wits)));
fun register (dep, eqns) ctxt =
ctxt |> add_registration
{inst = dep,
- mixin =
- Option.map (rpair true)
- (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')),
+ mixin = Option.map (rpair true) (Element.eq_morphism (eqns @ eqns')),
export = export};
in ctxt'' |> fold register (deps' ~~ eqnss') end;
--- a/src/Pure/Isar/local_defs.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/local_defs.ML Mon May 22 12:01:05 2023 +0200
@@ -155,7 +155,7 @@
if t aconv u then (asm, false)
else (Drule.abs_def (Variable.gen_all outer asm), true))
end)));
- in (apply2 (map #1) (List.partition #2 defs_asms), Assumption.export false inner outer th) end;
+ in (apply2 (map #1) (List.partition #2 defs_asms), Assumption.export inner outer th) end;
(*
[xs, xs \<equiv> as]
--- a/src/Pure/Isar/local_theory.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/local_theory.ML Mon May 22 12:01:05 2023 +0200
@@ -34,7 +34,7 @@
val reset_group: local_theory -> local_theory
val standard_morphism: local_theory -> Proof.context -> morphism
val standard_morphism_theory: local_theory -> morphism
- val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
+ val standard_form: local_theory -> Proof.context -> 'a Morphism.entity -> 'a
val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
val raw_theory: (theory -> theory) -> local_theory -> local_theory
val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
@@ -55,7 +55,8 @@
(string * thm list) list * local_theory
val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory
- val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
+ val declaration: {syntax: bool, pervasive: bool} -> Morphism.declaration ->
+ local_theory -> local_theory
val theory_registration: Locale.registration -> local_theory -> local_theory
val locale_dependency: Locale.registration -> local_theory -> local_theory
val pretty: local_theory -> Pretty.T list
@@ -102,7 +103,8 @@
notes: string -> Attrib.fact list -> local_theory -> (string * thm list) list * local_theory,
abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory,
- declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
+ declaration: {syntax: bool, pervasive: bool} -> Morphism.declaration_entity ->
+ local_theory -> local_theory,
theory_registration: Locale.registration -> local_theory -> local_theory,
locale_dependency: Locale.registration -> local_theory -> local_theory,
pretty: local_theory -> Pretty.T list};
@@ -192,9 +194,11 @@
(* standard morphisms *)
fun standard_morphism lthy ctxt =
- Proof_Context.norm_export_morphism lthy ctxt $>
- Morphism.binding_morphism "Local_Theory.standard_binding"
- (Name_Space.transform_binding (Proof_Context.naming_of lthy));
+ Morphism.set_context' lthy
+ (Proof_Context.export_morphism lthy ctxt $>
+ Morphism.thm_morphism' "Local_Theory.standard" (Goal.norm_result o Proof_Context.init_global) $>
+ Morphism.binding_morphism "Local_Theory.standard_binding"
+ (Name_Space.transform_binding (Proof_Context.naming_of lthy)));
fun standard_morphism_theory lthy =
standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
@@ -279,7 +283,7 @@
val define = operation2 #define false;
val define_internal = operation2 #define true;
val notes_kind = operation2 #notes;
-val declaration = operation2 #declaration;
+fun declaration args = operation2 #declaration args o Morphism.entity;
val theory_registration = operation1 #theory_registration;
fun locale_dependency registration =
assert_bottom #> operation1 #locale_dependency registration;
--- a/src/Pure/Isar/locale.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/locale.ML Mon May 22 12:01:05 2023 +0200
@@ -39,7 +39,7 @@
term option * term list ->
thm option * thm option -> thm list ->
Element.context_i list ->
- declaration list ->
+ Morphism.declaration_entity list ->
(string * Attrib.fact list) list ->
(string * morphism) list -> theory -> theory
val locale_space: theory -> Name_Space.T
@@ -59,7 +59,7 @@
(* Storing results *)
val add_facts: string -> string -> Attrib.fact list -> Proof.context -> Proof.context
- val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
+ val add_declaration: string -> bool -> Morphism.declaration_entity -> Proof.context -> Proof.context
(* Activation *)
val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
@@ -107,8 +107,14 @@
type dep = {name: string, morphisms: morphism * morphism, pos: Position.T, serial: serial};
fun eq_dep (dep1: dep, dep2: dep) = #serial dep1 = #serial dep2;
+fun transfer_dep thy ({name, morphisms, pos, serial}: dep) : dep =
+ {name = name, morphisms = apply2 (Morphism.set_context thy) morphisms, pos = pos, serial = serial};
+
fun make_dep (name, morphisms) : dep =
- {name = name, morphisms = morphisms, pos = Position.thread_data (), serial = serial ()};
+ {name = name,
+ morphisms = apply2 Morphism.reset_context morphisms,
+ pos = Position.thread_data (),
+ serial = serial ()};
(*table of mixin lists, per list mixins in reverse order of declaration;
lists indexed by registration/dependency serial,
@@ -120,7 +126,8 @@
val merge_mixins: mixins * mixins -> mixins = Inttab.merge_list (eq_snd op =);
-fun insert_mixin serial' mixin : mixins -> mixins = Inttab.cons_list (serial', (mixin, serial ()));
+fun insert_mixin serial' (morph, b) : mixins -> mixins =
+ Inttab.cons_list (serial', ((Morphism.reset_context morph, b), serial ()));
fun rename_mixin (old, new) (mixins: mixins) =
(case Inttab.lookup mixins old of
@@ -145,7 +152,7 @@
(* dynamic part *)
(*syntax declarations*)
- syntax_decls: (declaration * serial) list,
+ syntax_decls: (Morphism.declaration_entity * serial) list,
(*theorem declarations*)
notes: ((string * Attrib.fact list) * serial) list,
(*locale dependencies (sublocale relation) in reverse order*)
@@ -212,8 +219,10 @@
thy |> Locales.map (Name_Space.define (Context.Theory thy) true
(binding,
mk_locale ((parameters, spec, (apply2 o Option.map) Thm.trim_context intros,
- map Thm.trim_context axioms, hyp_spec),
- ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
+ map Thm.trim_context axioms,
+ map Element.trim_context_ctxt hyp_spec),
+ ((map (fn decl => (Morphism.entity_reset_context decl, serial ())) syntax_decls,
+ map (fn (a, facts) => ((a, map Attrib.trim_context_fact facts), serial ())) notes),
(map (fn (name, morph) => make_dep (name, (morph, Morphism.identity))) dependencies,
Inttab.empty)))) #> snd);
(* FIXME Morphism.identity *)
@@ -233,15 +242,17 @@
fun axioms_of thy = map (Thm.transfer thy) o #axioms o the_locale thy;
fun instance_of thy name morph = params_of thy name |>
- map (Morphism.term morph o Free o #1);
+ map (Morphism.term (Morphism.set_context thy morph) o Free o #1);
fun specification_of thy = #spec o the_locale thy;
-fun hyp_spec_of thy = #hyp_spec o the_locale thy;
+fun hyp_spec_of thy = map (Element.transfer_ctxt thy) o #hyp_spec o the_locale thy;
+
+fun dependencies_of thy = map (transfer_dep thy) o #dependencies o the_locale thy;
-fun dependencies_of thy = #dependencies o the_locale thy;
-
-fun mixins_of thy name serial = lookup_mixins (#mixins (the_locale thy name)) serial;
+fun mixins_of thy name serial =
+ lookup_mixins (#mixins (the_locale thy name)) serial
+ |> (map o apfst o apfst) (Morphism.set_context thy);
(* Print instance and qualifiers *)
@@ -395,7 +406,10 @@
fun add_reg thy export (name, morph) =
let
- val reg = {morphisms = (morph, export), pos = Position.thread_data (), serial = serial ()};
+ val reg =
+ {morphisms = (Morphism.reset_context morph, Morphism.reset_context export),
+ pos = Position.thread_data (),
+ serial = serial ()};
val id = (name, instance_of thy name (morph $> export));
in (map_registrations o apfst) (Idtab.insert (K false) (id, reg)) end;
@@ -485,34 +499,35 @@
val _ = trace "syntax" (name, morph) context;
val thy = Context.theory_of context;
val {syntax_decls, ...} = the_locale thy name;
+ val form_syntax_decl =
+ Morphism.form o Morphism.transform morph o Morphism.entity_set_context thy;
in
- context
- |> fold_rev (fn (decl, _) => decl morph) syntax_decls
+ fold_rev (form_syntax_decl o #1) syntax_decls context
handle ERROR msg => activate_err msg "syntax" (name, morph) context
end;
-fun activate_notes activ_elem transfer context export' (name, morph) input =
+fun activate_notes activ_elem context export' (name, morph) input =
let
val thy = Context.theory_of context;
val mixin =
(case export' of
NONE => Morphism.identity
| SOME export => collect_mixins context (name, morph $> export) $> export);
- val morph' = transfer input $> morph $> mixin;
+ val morph' = Morphism.set_context thy (morph $> mixin);
val notes' = map (Element.transform_ctxt morph') (lazy_notes thy name);
in
(notes', input) |-> fold (fn elem => fn res =>
- activ_elem (Element.transform_ctxt (transfer res) elem) res)
+ activ_elem (Element.transfer_ctxt thy elem) res)
end handle ERROR msg => activate_err msg "facts" (name, morph) context;
-fun activate_notes_trace activ_elem transfer context export' (name, morph) context' =
+fun activate_notes_trace activ_elem context export' (name, morph) context' =
let
val _ = trace "facts" (name, morph) context';
in
- activate_notes activ_elem transfer context export' (name, morph) context'
+ activate_notes activ_elem context export' (name, morph) context'
end;
-fun activate_all name thy activ_elem transfer (marked, input) =
+fun activate_all name thy activ_elem (marked, input) =
let
val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name;
val input' = input |>
@@ -522,7 +537,7 @@
(case asm of SOME A => activ_elem (Assumes [(Binding.empty_atts, [(A, [])])]) | _ => I) |>
(not (null defs) ?
activ_elem (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs)));
- val activate = activate_notes activ_elem transfer (Context.Theory thy) NONE;
+ val activate = activate_notes activ_elem (Context.Theory thy) NONE;
in
roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
end;
@@ -535,8 +550,8 @@
|> Context_Position.set_visible_generic false
|> pair (Idents.get context)
|> roundup (Context.theory_of context)
- (activate_notes_trace init_element Morphism.transfer_morphism'' context export)
- (the_default Morphism.identity export) dep
+ (activate_notes_trace init_element context export)
+ (Morphism.default export) dep
|-> Idents.put
|> Context_Position.restore_visible_generic context;
@@ -556,7 +571,7 @@
context
|> Context_Position.set_visible_generic false
|> pair empty_idents
- |> activate_all name thy init_element Morphism.transfer_morphism''
+ |> activate_all name thy init_element
|-> (fn marked' => Idents.put (merge_idents (marked, marked')))
|> Context_Position.restore_visible_generic context
|> Context.proof_of
@@ -647,11 +662,11 @@
val stored_notes = ((kind, map Attrib.trim_context_fact facts), serial ());
val applied_notes = make_notes kind facts;
- fun apply_notes morph = applied_notes |> fold (fn elem => fn context =>
- let val elem' = Element.transform_ctxt (Morphism.transfer_morphism'' context $> morph) elem
- in Element.init elem' context end);
- val apply_registrations = Context.theory_map (fn context =>
- fold_rev (apply_notes o #2) (registrations_of context loc) context);
+ fun apply_notes morph = applied_notes |> fold (fn elem => fn thy =>
+ let val elem' = Element.transform_ctxt (Morphism.set_context thy morph) elem
+ in Context.theory_map (Element.init elem') thy end);
+ fun apply_registrations thy =
+ fold_rev (apply_notes o #2) (registrations_of (Context.Theory thy) loc) thy;
in
ctxt
|> Attrib.local_notes kind facts |> #2
@@ -660,9 +675,11 @@
end;
fun add_declaration loc syntax decl =
- syntax ?
- Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
- #> add_facts loc "" [(Binding.empty_atts, Attrib.internal_declaration decl)];
+ let val decl0 = Morphism.entity_reset_context decl in
+ syntax ?
+ Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl0, serial ())))
+ #> add_facts loc "" [(Binding.empty_atts, Attrib.internal_declaration decl0)]
+ end;
(*** Reasoning about locales ***)
@@ -732,7 +749,7 @@
| cons_elem (elem as Lazy_Notes _) = show_facts ? cons elem
| cons_elem elem = cons elem;
val elems =
- activate_all name thy cons_elem (K (Morphism.transfer_morphism thy)) (empty_idents, [])
+ activate_all name thy cons_elem (empty_idents, [])
|> snd |> rev
|> tap consolidate_notes
|> map force_notes;
--- a/src/Pure/Isar/method.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/method.ML Mon May 22 12:01:05 2023 +0200
@@ -335,8 +335,9 @@
ML_Lex.read_source source @ ML_Lex.read ")))")
|> the_tactic;
in
- fn phi => set_tactic (fn _ => Context.setmp_generic_context (SOME context) (tac phi))
- end)) >> (fn decl => Morphism.form (the_tactic (Morphism.form decl context))));
+ Morphism.entity (fn phi =>
+ set_tactic (fn _ => Context.setmp_generic_context (SOME context) (tac phi)))
+ end)) >> (fn decl => Morphism.form_entity (the_tactic (Morphism.form decl context))));
(* method facts *)
@@ -606,11 +607,17 @@
map (fn (a, bs) => (Proof_Context.get_fact ctxt a, map prep_att bs)) xthms;
val facts =
Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)]
- |> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K attribute)]), bs));
+ |> map (fn (_, bs) =>
+ ((Binding.empty, [Attrib.internal (K attribute)]), Attrib.trim_context_thms bs));
- fun decl phi =
- Context.mapping I init #>
- Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd;
+ val decl =
+ Morphism.entity (fn phi => fn context =>
+ let val psi = Morphism.set_context'' context phi in
+ context
+ |> Context.mapping I init
+ |> Attrib.generic_notes "" (Attrib.transform_facts psi facts)
+ |> snd
+ end);
val modifier_report =
(#1 (Token.range_of modifier_toks),
--- a/src/Pure/Isar/proof.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/proof.ML Mon May 22 12:01:05 2023 +0200
@@ -477,7 +477,7 @@
in
result
|> map (Raw_Simplifier.norm_hhf result_ctxt #> protect_prems)
- |> Proof_Context.goal_export result_ctxt goal_ctxt
+ |> Proof_Context.export_goal result_ctxt goal_ctxt
|> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state)
end;
@@ -1096,7 +1096,7 @@
let
val ctxt' = context_of state';
val export0 =
- Assumption.export false result_ctxt (Proof_Context.augment result_text ctxt') #>
+ Assumption.export result_ctxt (Proof_Context.augment result_text ctxt') #>
fold_rev (fn (x, v) => Thm.forall_intr_name (x, Thm.cterm_of params_ctxt v)) params #>
Raw_Simplifier.norm_hhf_protect ctxt';
val export = map export0 #> Variable.export result_ctxt ctxt';
--- a/src/Pure/Isar/proof_context.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/proof_context.ML Mon May 22 12:01:05 2023 +0200
@@ -102,10 +102,10 @@
val standard_typ_check: Proof.context -> typ list -> typ list
val standard_term_check_finish: Proof.context -> term list -> term list
val standard_term_uncheck: Proof.context -> term list -> term list
- val goal_export: Proof.context -> Proof.context -> thm list -> thm list
+ val export_: {goal: bool} -> Proof.context -> Proof.context -> thm list -> thm list
val export: Proof.context -> Proof.context -> thm list -> thm list
+ val export_goal: Proof.context -> Proof.context -> thm list -> thm list
val export_morphism: Proof.context -> Proof.context -> morphism
- val norm_export_morphism: Proof.context -> Proof.context -> morphism
val auto_bind_goal: term list -> Proof.context -> Proof.context
val auto_bind_facts: term list -> Proof.context -> Proof.context
val simult_matches: Proof.context -> term * term list -> (indexname * term) list
@@ -839,21 +839,17 @@
(** export results **)
-fun common_export is_goal inner outer =
- map (Assumption.export is_goal inner outer) #>
+fun export_ goal inner outer =
+ map (Assumption.export_ goal inner outer) #>
Variable.export inner outer;
-val goal_export = common_export true;
-val export = common_export false;
+val export = export_{goal = false};
+val export_goal = export_{goal = true};
fun export_morphism inner outer =
Assumption.export_morphism inner outer $>
Variable.export_morphism inner outer;
-fun norm_export_morphism inner outer =
- export_morphism inner outer $>
- Morphism.thm_morphism "Proof_Context.norm_export" (Goal.norm_result outer);
-
(** term bindings **)
--- a/src/Pure/Isar/spec_rules.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/spec_rules.ML Mon May 22 12:01:05 2023 +0200
@@ -117,7 +117,7 @@
{pos = pos, name = name, rough_classification = rough_classification, terms = terms,
rules = map f rules};
-structure Rules = Generic_Data
+structure Data = Generic_Data
(
type T = spec_rule Item_Net.T;
val empty : T = Item_Net.init eq_spec #terms;
@@ -132,9 +132,9 @@
val thy = Context.theory_of context;
val transfer = Global_Theory.transfer_theories thy;
fun imported spec =
- imports |> exists (fn thy => Item_Net.member (Rules.get (Context.Theory thy)) spec);
+ imports |> exists (fn thy => Item_Net.member (Data.get (Context.Theory thy)) spec);
in
- Item_Net.content (Rules.get context)
+ Item_Net.content (Data.get context)
|> filter_out imported
|> (map o map_spec_rules) transfer
end;
@@ -148,7 +148,7 @@
(* retrieve *)
fun retrieve_generic context =
- Item_Net.retrieve (Rules.get context)
+ Item_Net.retrieve (Data.get context)
#> (map o map_spec_rules) (Thm.transfer'' context);
val retrieve = retrieve_generic o Context.Proof;
@@ -158,27 +158,28 @@
(* add *)
fun add b rough_classification terms rules lthy =
- let val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules) in
+ let
+ val n = length terms;
+ val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules);
+ in
lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => fn context =>
let
+ val psi = Morphism.set_trim_context'' context phi;
val pos = Position.thread_data ();
- val name = Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding phi b);
+ val name = Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding psi b);
val (terms', rules') =
- map (Thm.transfer (Context.theory_of context)) thms0
- |> Morphism.fact phi
- |> chop (length terms)
- |>> map (Thm.term_of o Drule.dest_term)
- ||> map Thm.trim_context;
+ chop n (Morphism.fact psi thms0)
+ |>> map (Thm.term_of o Drule.dest_term);
in
- context |> (Rules.map o Item_Net.update)
+ context |> (Data.map o Item_Net.update)
{pos = pos, name = name, rough_classification = rough_classification,
terms = terms', rules = rules'}
end)
end;
fun add_global b rough_classification terms rules thy =
- thy |> (Context.theory_map o Rules.map o Item_Net.update)
+ thy |> (Context.theory_map o Data.map o Item_Net.update)
{pos = Position.thread_data (),
name = Sign.full_name thy b,
rough_classification = rough_classification,
--- a/src/Pure/Isar/specification.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/specification.ML Mon May 22 12:01:05 2023 +0200
@@ -259,21 +259,19 @@
val ((lhs, (_, raw_th)), lthy2) = lthy
|> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
- val th = prove lthy2 raw_th;
- val lthy3 = lthy2 |> Spec_Rules.add name Spec_Rules.equational [lhs] [th];
+ val ([(def_name, [th])], lthy3) = lthy2
+ |> Local_Theory.notes [((name, atts), [([prove lthy2 raw_th], [])])];
- val ([(def_name, [th'])], lthy4) = lthy3
- |> Local_Theory.notes [((name, atts), [([th], [])])];
+ val lthy4 = lthy3
+ |> Spec_Rules.add name Spec_Rules.equational [lhs] [th]
+ |> Code.declare_default_eqns [(th, true)];
- val lthy5 = lthy4
- |> Code.declare_default_eqns [(th', true)];
-
- val lhs' = Morphism.term (Local_Theory.target_morphism lthy5) lhs;
+ val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
val _ =
- Proof_Display.print_consts int (Position.thread_data ()) lthy5
+ Proof_Display.print_consts int (Position.thread_data ()) lthy4
(Frees.defined (Frees.build (Frees.add_frees lhs'))) [(x, T)];
- in ((lhs, (def_name, th')), lthy5) end;
+ in ((lhs, (def_name, th)), lthy4) end;
fun definition xs ys As B = gen_def check_spec_open (K I) xs ys As B false;
val definition_cmd = gen_def read_spec_open Attrib.check_src;
--- a/src/Pure/Isar/token.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/Isar/token.ML Mon May 22 12:01:05 2023 +0200
@@ -29,8 +29,8 @@
Typ of typ |
Term of term |
Fact of string option * thm list |
- Attribute of morphism -> attribute |
- Declaration of declaration |
+ Attribute of attribute Morphism.entity |
+ Declaration of Morphism.declaration_entity |
Files of file Exn.result list |
Output of XML.body option
val pos_of: T -> Position.T
@@ -82,7 +82,8 @@
val get_name: T -> name_value option
val declare_maxidx: T -> Proof.context -> Proof.context
val map_facts: (string option -> thm list -> thm list) -> T -> T
- val trim_context_src: src -> src
+ val trim_context: T -> T
+ val transfer: theory -> T -> T
val transform: morphism -> T -> T
val init_assignable: T -> T
val assign: value option -> T -> T
@@ -103,6 +104,7 @@
val print_properties: Keyword.keywords -> Properties.T -> string
val make: (int * int) * string -> Position.T -> T * Position.T
val make_string: string * Position.T -> T
+ val make_string0: string -> T
val make_int: int -> T list
val make_src: string * Position.T -> T list -> src
type 'a parser = T list -> 'a * T list
@@ -196,8 +198,8 @@
Typ of typ |
Term of term |
Fact of string option * thm list | (*optional name for dynamic fact, i.e. fact "variable"*)
- Attribute of morphism -> attribute |
- Declaration of declaration |
+ Attribute of attribute Morphism.entity |
+ Declaration of Morphism.declaration_entity |
Files of file Exn.result list |
Output of XML.body option;
@@ -484,7 +486,33 @@
| Fact (a, ths) => Fact (a, f a ths)
| _ => v));
-val trim_context_src = (map o map_facts) (K (map Thm.trim_context));
+
+(* implicit context *)
+
+local
+
+fun context thm_context morphism_context attribute_context declaration_context =
+ let
+ fun token_context tok = map_value
+ (fn Source src => Source (map token_context src)
+ | Fact (a, ths) => Fact (a, map thm_context ths)
+ | Name (a, phi) => Name (a, morphism_context phi)
+ | Attribute a => Attribute (attribute_context a)
+ | Declaration a => Declaration (declaration_context a)
+ | v => v) tok;
+ in token_context end;
+
+in
+
+val trim_context =
+ context Thm.trim_context Morphism.reset_context
+ Morphism.entity_reset_context Morphism.entity_reset_context;
+
+fun transfer thy =
+ context (Thm.transfer thy) (Morphism.set_context thy)
+ (Morphism.entity_set_context thy) (Morphism.entity_set_context thy);
+
+end;
(* transform *)
@@ -744,6 +772,8 @@
val pos' = Position.no_range_position pos;
in Token ((x, (pos', pos')), y, z) end;
+fun make_string0 s = make_string (s, Position.none);
+
val make_int = explode Keyword.empty_keywords Position.none o signed_string_of_int;
fun make_src a args = make_string a :: args;
@@ -758,8 +788,9 @@
(* wrapped syntax *)
-fun syntax_generic scan src context =
+fun syntax_generic scan src0 context =
let
+ val src = map (transfer (Context.theory_of context)) src0;
val (name, pos) = name_of_src src;
val old_reports = maps reports_of_value src;
val args1 = map init_assignable (args_of_src src);
--- a/src/Pure/assumption.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/assumption.ML Mon May 22 12:01:05 2023 +0200
@@ -17,8 +17,10 @@
val local_prems_of: Proof.context -> Proof.context -> thm list
val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
val add_assumes: cterm list -> Proof.context -> thm list * Proof.context
- val export: bool -> Proof.context -> Proof.context -> thm -> thm
val export_term: Proof.context -> Proof.context -> term -> term
+ val export_: {goal: bool} -> Proof.context -> Proof.context -> thm -> thm
+ val export: Proof.context -> Proof.context -> thm -> thm
+ val export_goal: Proof.context -> Proof.context -> thm -> thm
val export_morphism: Proof.context -> Proof.context -> morphism
end;
@@ -128,24 +130,32 @@
(* export *)
-fun export is_goal inner outer =
+fun export_term inner outer =
+ fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
+
+fun export_thm is_goal inner outer =
+ fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer);
+
+fun export_{goal} inner outer =
Raw_Simplifier.norm_hhf_protect inner #>
- fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
+ export_thm goal inner outer #>
Raw_Simplifier.norm_hhf_protect outer;
-fun export_term inner outer =
- fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
+val export = export_{goal = false};
+val export_goal = export_{goal = true};
fun export_morphism inner outer =
let
- val thm = export false inner outer;
+ val export0 = export_thm false inner outer;
+ fun thm thy =
+ let val norm = norm_hhf_protect (Proof_Context.init_global thy)
+ in norm #> export0 #> norm end;
val term = export_term inner outer;
val typ = Logic.type_map term;
in
- Morphism.transfer_morphism' inner $>
- Morphism.transfer_morphism' outer $>
Morphism.morphism "Assumption.export"
- {binding = [], typ = [typ], term = [term], fact = [map thm]}
+ {binding = [], typ = [K typ], term = [K term], fact = [map o thm o Morphism.the_theory]}
+ |> Morphism.set_context (Proof_Context.theory_of inner)
end;
end;
--- a/src/Pure/context.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/context.ML Mon May 22 12:01:05 2023 +0200
@@ -65,6 +65,7 @@
val certificate_theory_id: certificate -> theory_id
val eq_certificate: certificate * certificate -> bool
val join_certificate: certificate * certificate -> certificate
+ val join_certificate_theory: theory * theory -> theory
(*generic context*)
datatype generic = Theory of theory | Proof of Proof.context
val theory_tracing: bool Unsynchronized.ref
@@ -627,16 +628,24 @@
| eq_certificate (Certificate_Id thy_id1, Certificate_Id thy_id2) = eq_thy_id (thy_id1, thy_id2)
| eq_certificate _ = false;
+fun err_join (thy_id1, thy_id2) =
+ error ("Cannot join unrelated theory certificates " ^
+ display_name thy_id1 ^ " and " ^ display_name thy_id2);
+
fun join_certificate (cert1, cert2) =
let val (thy_id1, thy_id2) = apply2 certificate_theory_id (cert1, cert2) in
if eq_thy_id (thy_id1, thy_id2) then (case cert1 of Certificate _ => cert1 | _ => cert2)
else if proper_subthy_id (thy_id2, thy_id1) then cert1
else if proper_subthy_id (thy_id1, thy_id2) then cert2
- else
- error ("Cannot join unrelated theory certificates " ^
- display_name thy_id1 ^ " and " ^ display_name thy_id2)
+ else err_join (thy_id1, thy_id2)
end;
+fun join_certificate_theory (thy1, thy2) =
+ let val (thy_id1, thy_id2) = apply2 theory_id (thy1, thy2) in
+ if subthy_id (thy_id2, thy_id1) then thy1
+ else if proper_subthy_id (thy_id1, thy_id2) then thy2
+ else err_join (thy_id1, thy_id2)
+ end;
(*** generic context ***)
--- a/src/Pure/drule.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/drule.ML Mon May 22 12:01:05 2023 +0200
@@ -75,7 +75,7 @@
val eta_contraction_rule: thm -> thm
val norm_hhf_eq: thm
val norm_hhf_eqs: thm list
- val is_norm_hhf: term -> bool
+ val is_norm_hhf: {protect: bool} -> term -> bool
val norm_hhf: theory -> term -> term
val norm_hhf_cterm: Proof.context -> cterm -> cterm
val protect: cterm -> cterm
@@ -669,15 +669,19 @@
val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq);
val norm_hhf_eqs = [norm_hhf_eq, sort_constraint_eq];
-fun is_norm_hhf (Const ("Pure.sort_constraint", _)) = false
- | is_norm_hhf (Const ("Pure.imp", _) $ _ $ (Const ("Pure.all", _) $ _)) = false
- | is_norm_hhf (Abs _ $ _) = false
- | is_norm_hhf (t $ u) = is_norm_hhf t andalso is_norm_hhf u
- | is_norm_hhf (Abs (_, _, t)) = is_norm_hhf t
- | is_norm_hhf _ = true;
+fun is_norm_hhf {protect} =
+ let
+ fun is_norm (Const ("Pure.sort_constraint", _)) = false
+ | is_norm (Const ("Pure.imp", _) $ _ $ (Const ("Pure.all", _) $ _)) = false
+ | is_norm (Const ("Pure.prop", _) $ t) = protect orelse is_norm t
+ | is_norm (Abs _ $ _) = false
+ | is_norm (t $ u) = is_norm t andalso is_norm u
+ | is_norm (Abs (_, _, t)) = is_norm t
+ | is_norm _ = true;
+ in is_norm end;
fun norm_hhf thy t =
- if is_norm_hhf t then t
+ if is_norm_hhf {protect = false} t then t
else Pattern.rewrite_term thy [norm_hhf_prop] [] t;
fun norm_hhf_cterm ctxt raw_ct =
@@ -685,7 +689,7 @@
val thy = Proof_Context.theory_of ctxt;
val ct = Thm.transfer_cterm thy raw_ct;
val t = Thm.term_of ct;
- in if is_norm_hhf t then ct else Thm.cterm_of ctxt (norm_hhf thy t) end;
+ in if is_norm_hhf {protect = false} t then ct else Thm.cterm_of ctxt (norm_hhf thy t) end;
(* var indexes *)
--- a/src/Pure/ex/Def.thy Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/ex/Def.thy Mon May 22 12:01:05 2023 +0200
@@ -25,12 +25,12 @@
(* context data *)
-type def = {lhs: term, mk_eq: morphism -> thm};
+type def = {lhs: term, eq: thm};
val eq_def : def * def -> bool = op aconv o apply2 #lhs;
-fun transform_def phi ({lhs, mk_eq}: def) =
- {lhs = Morphism.term phi lhs, mk_eq = Morphism.transform phi mk_eq};
+fun transform_def phi ({lhs, eq}: def) =
+ {lhs = Morphism.term phi lhs, eq = Morphism.thm phi eq};
structure Data = Generic_Data
(
@@ -40,12 +40,11 @@
);
fun declare_def lhs eq lthy =
- let
- val eq0 = Thm.trim_context eq;
- val def: def = {lhs = lhs, mk_eq = fn phi => Morphism.thm phi eq0};
- in
+ let val def0: def = {lhs = lhs, eq = Thm.trim_context eq} in
lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => (Data.map o Item_Net.update) (transform_def phi def))
+ (fn phi => fn context =>
+ let val psi = Morphism.set_trim_context'' context phi
+ in (Data.map o Item_Net.update) (transform_def psi def0) context end)
end;
fun get_def ctxt ct =
@@ -53,15 +52,10 @@
val thy = Proof_Context.theory_of ctxt;
val data = Data.get (Context.Proof ctxt);
val t = Thm.term_of ct;
- fun match_def {lhs, mk_eq} =
+ fun match_def {lhs, eq} =
if Pattern.matches thy (lhs, t) then
- let
- val inst = Thm.match (Thm.cterm_of ctxt lhs, ct);
- val eq =
- Morphism.form mk_eq
- |> Thm.transfer thy
- |> Thm.instantiate inst;
- in SOME eq end
+ let val inst = Thm.match (Thm.cterm_of ctxt lhs, ct)
+ in SOME (Thm.instantiate inst (Thm.transfer thy eq)) end
else NONE;
in Item_Net.retrieve_matching data t |> get_first match_def end;
--- a/src/Pure/goal.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/goal.ML Mon May 22 12:01:05 2023 +0200
@@ -221,7 +221,7 @@
res
|> Thm.close_derivation \<^here>
|> Conjunction.elim_balanced (length props)
- |> map (Assumption.export false ctxt' ctxt)
+ |> map (Assumption.export ctxt' ctxt)
|> Variable.export ctxt' ctxt
|> map Drule.zero_var_indexes
end;
@@ -311,7 +311,7 @@
fun norm_hhf_tac ctxt =
resolve_tac ctxt [Drule.asm_rl] (*cheap approximation -- thanks to builtin Logic.flatten_params*)
THEN' SUBGOAL (fn (t, i) =>
- if Drule.is_norm_hhf t then all_tac
+ if Drule.is_norm_hhf {protect = false} t then all_tac
else rewrite_goal_tac ctxt Drule.norm_hhf_eqs i);
--- a/src/Pure/morphism.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/morphism.ML Mon May 22 12:01:05 2023 +0200
@@ -9,7 +9,6 @@
signature BASIC_MORPHISM =
sig
type morphism
- type declaration = morphism -> Context.generic -> Context.generic
val $> : morphism * morphism -> morphism
end
@@ -17,12 +16,18 @@
sig
include BASIC_MORPHISM
exception MORPHISM of string * exn
+ val the_theory: theory option -> theory
+ val set_context: theory -> morphism -> morphism
+ val set_context': Proof.context -> morphism -> morphism
+ val set_context'': Context.generic -> morphism -> morphism
+ val reset_context: morphism -> morphism
val morphism: string ->
- {binding: (binding -> binding) list,
- typ: (typ -> typ) list,
- term: (term -> term) list,
- fact: (thm list -> thm list) list} -> morphism
+ {binding: (theory option -> binding -> binding) list,
+ typ: (theory option -> typ -> typ) list,
+ term: (theory option -> term -> term) list,
+ fact: (theory option -> thm list -> thm list) list} -> morphism
val is_identity: morphism -> bool
+ val is_empty: morphism -> bool
val pretty: morphism -> Pretty.T
val binding: morphism -> binding -> binding
val binding_prefix: morphism -> (string * bool) list
@@ -32,18 +37,36 @@
val thm: morphism -> thm -> thm
val cterm: morphism -> cterm -> cterm
val identity: morphism
+ val default: morphism option -> morphism
val compose: morphism -> morphism -> morphism
- val transform: morphism -> (morphism -> 'a) -> morphism -> 'a
- val form: (morphism -> 'a) -> 'a
+ type 'a entity
+ val entity: (morphism -> 'a) -> 'a entity
+ val entity_reset_context: 'a entity -> 'a entity
+ val entity_set_context: theory -> 'a entity -> 'a entity
+ val entity_set_context': Proof.context -> 'a entity -> 'a entity
+ val entity_set_context'': Context.generic -> 'a entity -> 'a entity
+ val transform: morphism -> 'a entity -> 'a entity
+ val transform_reset_context: morphism -> 'a entity -> 'a entity
+ val form: 'a entity -> 'a
+ val form_entity: (morphism -> 'a) -> 'a
+ type declaration = morphism -> Context.generic -> Context.generic
+ type declaration_entity = (Context.generic -> Context.generic) entity
val binding_morphism: string -> (binding -> binding) -> morphism
+ val typ_morphism': string -> (theory -> typ -> typ) -> morphism
val typ_morphism: string -> (typ -> typ) -> morphism
+ val term_morphism': string -> (theory -> term -> term) -> morphism
val term_morphism: string -> (term -> term) -> morphism
+ val fact_morphism': string -> (theory -> thm list -> thm list) -> morphism
val fact_morphism: string -> (thm list -> thm list) -> morphism
+ val thm_morphism': string -> (theory -> thm -> thm) -> morphism
val thm_morphism: string -> (thm -> thm) -> morphism
val transfer_morphism: theory -> morphism
val transfer_morphism': Proof.context -> morphism
val transfer_morphism'': Context.generic -> morphism
val trim_context_morphism: morphism
+ val set_trim_context: theory -> morphism -> morphism
+ val set_trim_context': Proof.context -> morphism -> morphism
+ val set_trim_context'': Context.generic -> morphism -> morphism
val instantiate_frees_morphism: ctyp TFrees.table * cterm Frees.table -> morphism
val instantiate_morphism: ctyp TVars.table * cterm Vars.table -> morphism
end;
@@ -53,30 +76,53 @@
(* named functions *)
-type 'a funs = (string * ('a -> 'a)) list;
+type 'a funs = (string * (theory option -> 'a -> 'a)) list;
exception MORPHISM of string * exn;
-fun app (name, f) x = f x
+fun app context (name, f) x = f context x
handle exn =>
if Exn.is_interrupt exn then Exn.reraise exn else raise MORPHISM (name, exn);
-fun apply fs = fold_rev app fs;
+
+(* optional context *)
+
+fun the_theory (SOME thy) = thy
+ | the_theory NONE = raise Fail "Morphism lacks theory context";
+
+fun join_transfer (SOME thy) = Thm.join_transfer thy
+ | join_transfer NONE = I;
+
+val join_context = join_options Context.join_certificate_theory;
(* type morphism *)
datatype morphism = Morphism of
- {names: string list,
+ {context: theory option,
+ names: string list,
binding: binding funs,
typ: typ funs,
term: term funs,
fact: thm list funs};
-type declaration = morphism -> Context.generic -> Context.generic;
+fun rep (Morphism args) = args;
+
+fun apply which phi =
+ let val args = rep phi
+ in fold_rev (app (#context args)) (which args) end;
+
+fun put_context context (Morphism {context = _, names, binding, typ, term, fact}) =
+ Morphism {context = context, names = names, binding = binding, typ = typ, term = term, fact = fact};
+
+val set_context = put_context o SOME;
+val set_context' = set_context o Proof_Context.theory_of;
+val set_context'' = set_context o Context.theory_of;
+val reset_context = put_context NONE;
fun morphism a {binding, typ, term, fact} =
Morphism {
+ context = NONE,
names = if a = "" then [] else [a],
binding = map (pair a) binding,
typ = map (pair a) typ,
@@ -84,18 +130,20 @@
fact = map (pair a) fact};
(*syntactic test only!*)
-fun is_identity (Morphism {names, binding, typ, term, fact}) =
+fun is_identity (Morphism {context = _, names, binding, typ, term, fact}) =
null names andalso null binding andalso null typ andalso null term andalso null fact;
-fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names));
+fun is_empty phi = is_none (#context (rep phi)) andalso is_identity phi;
+
+fun pretty phi = Pretty.enum ";" "{" "}" (map Pretty.str (rev (#names (rep phi))));
val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
-fun binding (Morphism {binding, ...}) = apply binding;
+val binding = apply #binding;
fun binding_prefix morph = Binding.name "x" |> binding morph |> Binding.prefix_of;
-fun typ (Morphism {typ, ...}) = apply typ;
-fun term (Morphism {term, ...}) = apply term;
-fun fact (Morphism {fact, ...}) = apply fact;
+val typ = apply #typ;
+val term = apply #term;
+fun fact phi = map (join_transfer (#context (rep phi))) #> apply #fact phi;
val thm = singleton o fact;
val cterm = Drule.cterm_rule o thm;
@@ -104,36 +152,73 @@
val identity = morphism "" {binding = [], typ = [], term = [], fact = []};
-fun compose
- (Morphism {names = names1, binding = binding1, typ = typ1, term = term1, fact = fact1})
- (Morphism {names = names2, binding = binding2, typ = typ2, term = term2, fact = fact2}) =
- Morphism {
- names = names1 @ names2,
- binding = binding1 @ binding2,
- typ = typ1 @ typ2,
- term = term1 @ term2,
- fact = fact1 @ fact2};
+val default = the_default identity;
+
+fun compose phi1 phi2 =
+ if is_empty phi1 then phi2
+ else if is_empty phi2 then phi1
+ else
+ let
+ val {context = context1, names = names1, binding = binding1,
+ typ = typ1, term = term1, fact = fact1} = rep phi1;
+ val {context = context2, names = names2, binding = binding2,
+ typ = typ2, term = term2, fact = fact2} = rep phi2;
+ in
+ Morphism {
+ context = join_context (context1, context2),
+ names = names1 @ names2,
+ binding = binding1 @ binding2,
+ typ = typ1 @ typ2,
+ term = term1 @ term2,
+ fact = fact1 @ fact2}
+ end;
fun phi1 $> phi2 = compose phi2 phi1;
-fun transform phi f = fn psi => f (phi $> psi);
-fun form f = f identity;
+
+(* abstract entities *)
+
+datatype 'a entity = Entity of (morphism -> 'a) * morphism;
+fun entity f = Entity (f, identity);
+
+fun entity_morphism g (Entity (f, phi)) = Entity (f, g phi);
+fun entity_reset_context a = entity_morphism reset_context a;
+fun entity_set_context thy a = entity_morphism (set_context thy) a;
+fun entity_set_context' ctxt a = entity_morphism (set_context' ctxt) a;
+fun entity_set_context'' context a = entity_morphism (set_context'' context) a;
+
+fun transform phi = entity_morphism (compose phi);
+fun transform_reset_context phi = entity_morphism (reset_context o compose phi);
+
+fun form (Entity (f, phi)) = f phi;
+fun form_entity f = f identity;
+
+type declaration = morphism -> Context.generic -> Context.generic;
+type declaration_entity = (Context.generic -> Context.generic) entity;
(* concrete morphisms *)
-fun binding_morphism a binding = morphism a {binding = [binding], typ = [], term = [], fact = []};
-fun typ_morphism a typ = morphism a {binding = [], typ = [typ], term = [], fact = []};
-fun term_morphism a term = morphism a {binding = [], typ = [], term = [term], fact = []};
-fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [fact]};
-fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [map thm]};
+fun binding_morphism a binding = morphism a {binding = [K binding], typ = [], term = [], fact = []};
+fun typ_morphism' a typ = morphism a {binding = [], typ = [typ o the_theory], term = [], fact = []};
+fun typ_morphism a typ = morphism a {binding = [], typ = [K typ], term = [], fact = []};
+fun term_morphism' a term = morphism a {binding = [], typ = [], term = [term o the_theory], fact = []};
+fun term_morphism a term = morphism a {binding = [], typ = [], term = [K term], fact = []};
+fun fact_morphism' a fact = morphism a {binding = [], typ = [], term = [], fact = [fact o the_theory]};
+fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [K fact]};
+fun thm_morphism' a thm = morphism a {binding = [], typ = [], term = [], fact = [map o thm o the_theory]};
+fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [K (map thm)]};
-val transfer_morphism = thm_morphism "transfer" o Thm.join_transfer;
+fun transfer_morphism thy = fact_morphism "transfer" I |> set_context thy;
val transfer_morphism' = transfer_morphism o Proof_Context.theory_of;
val transfer_morphism'' = transfer_morphism o Context.theory_of;
val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context;
+fun set_trim_context thy phi = set_context thy phi $> trim_context_morphism;
+val set_trim_context' = set_trim_context o Proof_Context.theory_of;
+val set_trim_context'' = set_trim_context o Context.theory_of;
+
(* instantiate *)
@@ -148,9 +233,9 @@
{binding = [],
typ =
if TFrees.is_empty instT then []
- else [Term_Subst.instantiateT_frees instT],
- term = [Term_Subst.instantiate_frees (instT, inst)],
- fact = [map (Thm.instantiate_frees (cinstT, cinst))]}
+ else [K (Term_Subst.instantiateT_frees instT)],
+ term = [K (Term_Subst.instantiate_frees (instT, inst))],
+ fact = [K (map (Thm.instantiate_frees (cinstT, cinst)))]}
end;
fun instantiate_morphism (cinstT, cinst) =
@@ -164,9 +249,9 @@
{binding = [],
typ =
if TVars.is_empty instT then []
- else [Term_Subst.instantiateT instT],
- term = [Term_Subst.instantiate (instT, inst)],
- fact = [map (Thm.instantiate (cinstT, cinst))]}
+ else [K (Term_Subst.instantiateT instT)],
+ term = [K (Term_Subst.instantiate (instT, inst))],
+ fact = [K (map (Thm.instantiate (cinstT, cinst)))]}
end;
end;
--- a/src/Pure/raw_simplifier.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/raw_simplifier.ML Mon May 22 12:01:05 2023 +0200
@@ -36,7 +36,7 @@
type simproc
val eq_simproc: simproc * simproc -> bool
val cert_simproc: theory -> string ->
- {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option} -> simproc
+ {lhss: term list, proc: (Proof.context -> cterm -> thm option) Morphism.entity} -> simproc
val transform_simproc: morphism -> simproc -> simproc
val simpset_of: Proof.context -> simpset
val put_simpset: simpset -> Proof.context -> Proof.context
@@ -709,7 +709,7 @@
Simproc of
{name: string,
lhss: term list,
- proc: morphism -> Proof.context -> cterm -> thm option,
+ proc: (Proof.context -> cterm -> thm option) Morphism.entity,
stamp: stamp};
fun eq_simproc (Simproc {stamp = stamp1, ...}, Simproc {stamp = stamp2, ...}) = stamp1 = stamp2;
@@ -721,7 +721,7 @@
Simproc
{name = name,
lhss = map (Morphism.term phi) lhss,
- proc = Morphism.transform phi proc,
+ proc = Morphism.transform_reset_context phi proc,
stamp = stamp};
local
@@ -1423,11 +1423,11 @@
local
-fun gen_norm_hhf ss ctxt0 th0 =
+fun gen_norm_hhf protect ss ctxt0 th0 =
let
val (ctxt, th) = Thm.join_transfer_context (ctxt0, th0);
val th' =
- if Drule.is_norm_hhf (Thm.prop_of th) then th
+ if Drule.is_norm_hhf protect (Thm.prop_of th) then th
else
Conv.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th;
in th' |> Thm.adjust_maxidx_thm ~1 |> Variable.gen_all ctxt end;
@@ -1445,8 +1445,8 @@
in
-val norm_hhf = gen_norm_hhf hhf_ss;
-val norm_hhf_protect = gen_norm_hhf hhf_protect_ss;
+val norm_hhf = gen_norm_hhf {protect = false} hhf_ss;
+val norm_hhf_protect = gen_norm_hhf {protect = true} hhf_protect_ss;
end;
--- a/src/Pure/simplifier.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/simplifier.ML Mon May 22 12:01:05 2023 +0200
@@ -128,7 +128,8 @@
val ctxt' = fold Proof_Context.augment lhss ctxt;
val lhss' = Variable.export_terms ctxt' ctxt lhss;
in
- cert_simproc (Proof_Context.theory_of ctxt) name {lhss = lhss', proc = proc}
+ cert_simproc (Proof_Context.theory_of ctxt) name
+ {lhss = lhss', proc = Morphism.entity proc}
end;
local
@@ -161,28 +162,27 @@
local
-fun make_cong ctxt = Thm.close_derivation \<^here> o Thm.reflexive
- o Thm.cterm_of ctxt o Logic.varify_global o list_comb;
-
-fun add_cong (const_binding, (const, target_params)) gthy =
- if null target_params
- then gthy
+fun add_foundation_cong (binding, (const, target_params)) gthy =
+ if null target_params then gthy
else
let
- val cong = make_cong (Context.proof_of gthy) (const, target_params)
- val cong_binding = Binding.qualify_name true const_binding "cong"
+ val thy = Context.theory_of gthy;
+ val cong =
+ list_comb (const, target_params)
+ |> Logic.varify_global
+ |> Thm.global_cterm_of thy
+ |> Thm.reflexive
+ |> Thm.close_derivation \<^here>;
+ val cong_binding = Binding.qualify_name true binding "cong";
in
gthy
- |> Attrib.generic_notes Thm.theoremK
- [((cong_binding, []), [([cong], [])])]
- |> snd
+ |> Attrib.generic_notes Thm.theoremK [((cong_binding, []), [([cong], [])])]
+ |> #2
end;
-in
+val _ = Theory.setup (Generic_Target.add_foundation_interpretation add_foundation_cong);
-val _ = Theory.setup (Generic_Target.add_foundation_interpretation add_cong);
-
-end;
+in end;
@@ -311,8 +311,8 @@
val add_del =
(Args.del -- Args.colon >> K (op delsimprocs) ||
Scan.option (Args.add -- Args.colon) >> K (op addsimprocs))
- >> (fn f => fn simproc => fn phi => Thm.declaration_attribute
- (K (Raw_Simplifier.map_ss (fn ctxt => f (ctxt, [transform_simproc phi simproc])))));
+ >> (fn f => fn simproc => Morphism.entity (fn phi => Thm.declaration_attribute
+ (K (Raw_Simplifier.map_ss (fn ctxt => f (ctxt, [transform_simproc phi simproc]))))));
in
--- a/src/Pure/variable.ML Thu May 18 11:44:42 2023 +0100
+++ b/src/Pure/variable.ML Mon May 22 12:01:05 2023 +0200
@@ -583,9 +583,8 @@
val term = singleton (export_terms inner outer);
val typ = Logic.type_map term;
in
- Morphism.transfer_morphism' inner $>
- Morphism.transfer_morphism' outer $>
- Morphism.morphism "Variable.export" {binding = [], typ = [typ], term = [term], fact = [fact]}
+ Morphism.morphism "Variable.export"
+ {binding = [], typ = [K typ], term = [K term], fact = [K fact]}
end;