# HG changeset patch # User wenzelm # Date 1684062049 -7200 # Node ID 1828b174768e9cbe96baa2a44b1255912ca25f64 # Parent 6200555461c65450da22182b40aa9b4364672cec proper Thm.trim_context / Thm.transfer; diff -r 6200555461c6 -r 1828b174768e src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Sun May 14 12:34:49 2023 +0200 +++ b/src/Pure/Isar/class.ML Sun May 14 13:00:49 2023 +0200 @@ -478,9 +478,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)); diff -r 6200555461c6 -r 1828b174768e src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Sun May 14 12:34:49 2023 +0200 +++ b/src/Pure/Isar/class_declaration.ML Sun May 14 13:00:49 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,13 @@ 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 thy (Class.these_defs thy sups |> map Thm.trim_context); (* assm_intro *) fun prove_assm_intro thm = diff -r 6200555461c6 -r 1828b174768e src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Sun May 14 12:34:49 2023 +0200 +++ b/src/Pure/Isar/element.ML Sun May 14 13:00:49 2023 +0200 @@ -275,7 +275,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 +291,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 +325,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 +362,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 diff -r 6200555461c6 -r 1828b174768e src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Sun May 14 12:34:49 2023 +0200 +++ b/src/Pure/Isar/expression.ML Sun May 14 13:00:49 2023 +0200 @@ -766,15 +766,15 @@ val ((statement, intro, axioms), thy''') = thy'' |> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred); - val ctxt''' = Proof_Context.init_global thy'''; + val conclude_witness = + Drule.export_without_context o Element.conclude_witness (Proof_Context.init_global thy'''); val ([(_, [intro']), _], thy'''') = thy''' |> 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, - [])])] + [(map conclude_witness 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; @@ -851,6 +851,7 @@ val notes' = body_elems + |> map (Element.transform_ctxt (Morphism.transfer_morphism thy')) |> map (defines_to_notes pred_ctxt) |> map (Element.transform_ctxt a_satisfy) |> (fn elems => diff -r 6200555461c6 -r 1828b174768e src/Pure/Isar/interpretation.ML --- a/src/Pure/Isar/interpretation.ML Sun May 14 12:34:49 2023 +0200 +++ b/src/Pure/Isar/interpretation.ML Sun May 14 13:00:49 2023 +0200 @@ -98,7 +98,8 @@ 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, [])]); diff -r 6200555461c6 -r 1828b174768e src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Sun May 14 12:34:49 2023 +0200 +++ b/src/Pure/Isar/locale.ML Sun May 14 13:00:49 2023 +0200 @@ -212,8 +212,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.transform_ctxt Morphism.trim_context_morphism) hyp_spec), + ((map (fn decl => (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 *)