author haftmann Mon, 31 May 2021 20:27:45 +0000 changeset 73793 26c0ccf17f31 parent 73792 a1086aebcd78 child 73794 e75635a0bafd child 73795 8893e0ed263a child 73832 9db620f007fa
more accurate export morphism enables proper instantiation by interpretation
 src/HOL/Library/Saturated.thy file | annotate | diff | comparison | revisions src/Pure/Isar/class.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/Library/Saturated.thy	Sat May 29 13:42:26 2021 +0100
+++ b/src/HOL/Library/Saturated.thy	Mon May 31 20:27:45 2021 +0000
@@ -123,9 +123,7 @@
qed
qed
show "1 * a = a"
-    apply (metis One_nat_def len_gt_0 less_Suc0 less_zeroE linorder_not_less min.absorb_iff1 min_nat_of_len_of nat_mult_1_right mult.commute)
-    done
+    by (simp add: sat_eq_iff min_def not_le not_less)
show "(a + b) * c = a * c + b * c"
proof(cases "c = 0")
case True thus ?thesis by (simp add: sat_eq_iff)
@@ -207,31 +205,18 @@
instantiation sat :: (len) "{Inf, Sup}"
begin

-definition "Inf = (semilattice_neutr_set.F min top :: 'a sat set \<Rightarrow> 'a sat)"
-definition "Sup = (semilattice_neutr_set.F max bot :: 'a sat set \<Rightarrow> 'a sat)"
+global_interpretation Inf_sat: semilattice_neutr_set min \<open>top :: 'a sat\<close>
+  defines Inf_sat = Inf_sat.F
+  by standard (simp add: min_def)
+
+global_interpretation Sup_sat: semilattice_neutr_set max \<open>bot :: 'a sat\<close>
+  defines Sup_sat = Sup_sat.F
+  by standard (simp add: max_def bot.extremum_unique)

instance ..

end

-interpretation Inf_sat: semilattice_neutr_set min "top :: 'a::len sat"
-  rewrites "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
-proof -
-  show "semilattice_neutr_set min (top :: 'a sat)"
-    by standard (simp add: min_def)
-  show "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
-qed
-
-interpretation Sup_sat: semilattice_neutr_set max "bot :: 'a::len sat"
-  rewrites "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
-proof -
-  show "semilattice_neutr_set max (bot :: 'a sat)"
-    by standard (simp add: max_def bot.extremum_unique)
-  show "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
-qed
-
instance sat :: (len) complete_lattice
proof
fix x :: "'a sat"```
```--- a/src/Pure/Isar/class.ML	Sat May 29 13:42:26 2021 +0100
+++ b/src/Pure/Isar/class.ML	Mon May 31 20:27:45 2021 +0000
@@ -272,7 +272,7 @@

fun make_rewrite t c_ty =
let
-    val (vs, t') = strip_abs t;
+    val vs = strip_abs_vars t;
val vts = map snd vs
|> Name.invent_names Name.context Name.uu
|> map (fn (v, T) => Var ((v, 0), T));
@@ -444,7 +444,7 @@
let
val thy = Proof_Context.theory_of lthy;
val preprocess = perhaps (try (Pattern.rewrite_term_top thy (these_unchecks thy [class]) []));
-    val (global_rhs, (extra_tfrees, (type_params, term_params))) =
+    val (global_rhs, (_, (_, term_params))) =
Generic_Target.export_abbrev lthy preprocess rhs;
val mx' = Generic_Target.check_mixfix_global (b, null term_params) mx;
in
@@ -665,6 +665,14 @@
else error ("Missing instance proof for type " ^ quote (Proof_Context.markup_type lthy tyco)));
in lthy end;

+fun registration thy_ctxt {inst, mixin, export} lthy =
+  lthy
+      {inst = inst,
+       mixin = mixin,
+       export = export \$> Proof_Context.export_morphism lthy thy_ctxt}
+         (*handle fixed types variables on target context properly*);
+
fun instantiation (tycos, vs, sort) thy =
let
val _ = if null tycos then error "At least one arity must be given" else ();
@@ -710,7 +718,7 @@
notes = Generic_Target.notes Generic_Target.theory_target_notes,
abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
declaration = K Generic_Target.theory_declaration,