src/HOL/Cardinals/Ordinal_Arithmetic.thy

   fixes r s
   assumes rWELL: "Well_order r"
   and     sWELL: "Well_order s"
 begin
 
-interpretation r!: wo_rel r by unfold_locales (rule rWELL)
-interpretation s!: wo_rel s by unfold_locales (rule sWELL)
+interpretation r: wo_rel r by unfold_locales (rule rWELL)
+interpretation s: wo_rel s by unfold_locales (rule sWELL)
 
 abbreviation "SUPP \<equiv> support r.zero (Field s)"
 abbreviation "FINFUNC \<equiv> FinFunc r s"
 lemmas FINFUNCD = FinFuncD[of _ r s]
 

   let ?f = "map_sum id f"
   from *(1) have "inj_on ?f (Field ?L)" unfolding Field_osum inj_on_def by fastforce
   moreover
   from *(2,4) have "compat ?L ?R ?f" unfolding compat_def osum_def map_prod_def by fastforce
   moreover
-  interpret t!: wo_rel t by unfold_locales (rule t)
-  interpret rt!: wo_rel ?R by unfold_locales (rule osum_Well_order[OF r t])
+  interpret t: wo_rel t by unfold_locales (rule t)
+  interpret rt: wo_rel ?R by unfold_locales (rule osum_Well_order[OF r t])
   from *(3) have "ofilter ?R (?f ` Field ?L)"
     unfolding t.ofilter_def rt.ofilter_def Field_osum image_Un image_image under_def
     by (auto simp: osum_def intro!: imageI) (auto simp: Field_def)
   ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f]
     by (auto intro: osum_Well_order r s t)

   from *(1) have "inj_on ?f (Field ?L)" unfolding Field_oprod inj_on_def by fastforce
   moreover
   from *(2,4) the_inv_into_f_f[OF *(1)] have "compat ?L ?R ?f" unfolding compat_def oprod_def
     by auto (metis well_order_on_domain t, metis well_order_on_domain s)
   moreover
-  interpret t!: wo_rel t by unfold_locales (rule t)
-  interpret rt!: wo_rel ?R by unfold_locales (rule oprod_Well_order[OF r t])
+  interpret t: wo_rel t by unfold_locales (rule t)
+  interpret rt: wo_rel ?R by unfold_locales (rule oprod_Well_order[OF r t])
   from *(3) have "ofilter ?R (?f ` Field ?L)"
     unfolding t.ofilter_def rt.ofilter_def Field_oprod under_def
     by (auto simp: oprod_def image_iff) (fast | metis r well_order_on_domain)+
   ultimately have "embed ?L ?R ?f" using embed_iff_compat_inj_on_ofilter[of ?L ?R ?f]
     by (auto intro: oprod_Well_order r s t)

 
 lemma oexp_monoR:
   assumes "oone <o r" "s <o t"
   shows   "r ^o s <o r ^o t" (is "?L <o ?R")
 proof -
-  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
-  interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t)
-  interpret rexpt!: wo_rel "r ^o t" by unfold_locales (rule rt.oexp_Well_order)
-  interpret r!: wo_rel r by unfold_locales (rule r)
-  interpret s!: wo_rel s by unfold_locales (rule s)
-  interpret t!: wo_rel t by unfold_locales (rule t)
+  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
+  interpret rt: wo_rel2 r t by unfold_locales (rule r, rule t)
+  interpret rexpt: wo_rel "r ^o t" by unfold_locales (rule rt.oexp_Well_order)
+  interpret r: wo_rel r by unfold_locales (rule r)
+  interpret s: wo_rel s by unfold_locales (rule s)
+  interpret t: wo_rel t by unfold_locales (rule t)
   have "Field r \<noteq> {}" by (metis assms(1) internalize_ordLess not_psubset_empty)
   moreover
   { assume "Field r = {r.zero}"
     hence "r = {(r.zero, r.zero)}" using refl_onD[OF r.REFL, of r.zero] unfolding Field_def by auto
     hence "r =o oone" by (metis oone_ordIso ordIso_symmetric)

 
 lemma oexp_monoL:
   assumes "r \<le>o s"
   shows   "r ^o t \<le>o s ^o t"
 proof -
-  interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t)
-  interpret st!: wo_rel2 s t by unfold_locales (rule s, rule t)
-  interpret r!: wo_rel r by unfold_locales (rule r)
-  interpret s!: wo_rel s by unfold_locales (rule s)
-  interpret t!: wo_rel t by unfold_locales (rule t)
+  interpret rt: wo_rel2 r t by unfold_locales (rule r, rule t)
+  interpret st: wo_rel2 s t by unfold_locales (rule s, rule t)
+  interpret r: wo_rel r by unfold_locales (rule r)
+  interpret s: wo_rel s by unfold_locales (rule s)
+  interpret t: wo_rel t by unfold_locales (rule t)
   show ?thesis
   proof (cases "t = {}")
     case True thus ?thesis using r s unfolding ordLeq_def2 underS_def by auto
   next
     case False thus ?thesis

 
 lemma ordLeq_oexp2:
   assumes "oone <o r"
   shows   "s \<le>o r ^o s"
 proof -
-  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
-  interpret r!: wo_rel r by unfold_locales (rule r)
-  interpret s!: wo_rel s by unfold_locales (rule s)
+  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
+  interpret r: wo_rel r by unfold_locales (rule r)
+  interpret s: wo_rel s by unfold_locales (rule s)
   from assms well_order_on_domain[OF r] obtain x where
     x: "x \<in> Field r" "r.zero \<in> Field r" "x \<noteq> r.zero"
     unfolding ordLess_def oone_def embedS_def[abs_def] bij_betw_def embed_def under_def
     by (auto simp: image_def)
        (metis (lifting) equals0D mem_Collect_eq r.zero_in_Field singletonI)

   assumes "wo_rel.max_fun_diff (s +o t) (case_sum f1 g1) (case_sum f2 g2) = Inl x"
     "case_sum f1 g1 \<noteq> case_sum f2 g2"
     "case_sum f1 g1 \<in> FinFunc r (s +o t)" "case_sum f2 g2 \<in> FinFunc r (s +o t)"
   shows "wo_rel.max_fun_diff s f1 f2 = x" (is ?P) "g1 = g2" (is ?Q)
 proof -
-  interpret st!: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
-  interpret s!: wo_rel s by unfold_locales (rule s)
-  interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
+  interpret st: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
+  interpret s: wo_rel s by unfold_locales (rule s)
+  interpret rst: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
   from assms(1) have *: "st.isMaxim {a \<in> Field (s +o t). case_sum f1 g1 a \<noteq> case_sum f2 g2 a} (Inl x)"
     using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp
   hence "s.isMaxim {a \<in> Field s. f1 a \<noteq> f2 a} x"
     unfolding st.isMaxim_def s.isMaxim_def Field_osum by (auto simp: osum_def)
   thus ?P unfolding s.max_fun_diff_def by (rule s.maxim_equality)

   assumes "wo_rel.max_fun_diff (s +o t) (case_sum f1 g1) (case_sum f2 g2) = Inr x"
     "case_sum f1 g1 \<noteq> case_sum f2 g2"
     "case_sum f1 g1 \<in> FinFunc r (s +o t)" "case_sum f2 g2 \<in> FinFunc r (s +o t)"
   shows "wo_rel.max_fun_diff t g1 g2 = x" (is ?P) "g1 \<noteq> g2" (is ?Q)
 proof -
-  interpret st!: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
-  interpret t!: wo_rel t by unfold_locales (rule t)
-  interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
+  interpret st: wo_rel "s +o t" by unfold_locales (rule osum_Well_order[OF s t])
+  interpret t: wo_rel t by unfold_locales (rule t)
+  interpret rst: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
   from assms(1) have *: "st.isMaxim {a \<in> Field (s +o t). case_sum f1 g1 a \<noteq> case_sum f2 g2 a} (Inr x)"
     using rst.isMaxim_max_fun_diff[OF assms(2-4)] by simp
   hence "t.isMaxim {a \<in> Field t. g1 a \<noteq> g2 a} x"
     unfolding st.isMaxim_def t.isMaxim_def Field_osum by (auto simp: osum_def)
   thus ?P ?Q unfolding t.max_fun_diff_def fun_eq_iff
     by (auto intro: t.maxim_equality simp: t.isMaxim_def)
 qed
 
 lemma oexp_osum: "r ^o (s +o t) =o (r ^o s) *o (r ^o t)" (is "?R =o ?L")
 proof (rule ordIso_symmetric)
-  interpret rst!: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
-  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
-  interpret rt!: wo_rel2 r t by unfold_locales (rule r, rule t)
+  interpret rst: wo_rel2 r "s +o t" by unfold_locales (rule r, rule osum_Well_order[OF s t])
+  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
+  interpret rt: wo_rel2 r t by unfold_locales (rule r, rule t)
   let ?f = "\<lambda>(f, g). case_sum f g"
   have "bij_betw ?f (Field ?L) (Field ?R)"
   unfolding bij_betw_def rst.Field_oexp rs.Field_oexp rt.Field_oexp Field_oprod proof (intro conjI)
     show "inj_on ?f (FinFunc r s \<times> FinFunc r t)" unfolding inj_on_def
       by (auto simp: fun_eq_iff split: sum.splits)

 
 lemma rev_curr_FinFunc:
   assumes Field: "Field r \<noteq> {}"
   shows "rev_curr ` (FinFunc r (s *o t)) = FinFunc (r ^o s) t"
 proof safe
-  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
-  interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
+  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
+  interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   fix g assume g: "g \<in> FinFunc r (s *o t)"
   hence "finite (rst.SUPP (rev_curr g))" "\<forall>x \<in> Field t. finite (rs.SUPP (rev_curr g x))"
     unfolding FinFunc_def Field_oprod rs.Field_oexp Func_def fin_support_def support_def
       rs.zero_oexp[OF Field] rev_curr_def by (auto simp: fun_eq_iff rs.const_def elim!: finite_surj)
   with g show "rev_curr g \<in> FinFunc (r ^o s) t"
     unfolding FinFunc_def Field_oprod rs.Field_oexp Func_def
     by (auto simp: rev_curr_def fin_support_def)
 next
-  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
-  interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
+  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
+  interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   fix fg assume *: "fg \<in> FinFunc (r ^o s) t"
   let ?g = "\<lambda>(a, b). if (a, b) \<in> Field (s *o t) then fg b a else undefined"
   show "fg \<in> rev_curr ` FinFunc r (s *o t)"
   proof (rule image_eqI[of _ _ ?g])
     show "fg = rev_curr ?g"

   assumes Field: "Field r \<noteq> {}" and "f \<noteq> g" "f \<in> FinFunc r (s *o t)" "g \<in> FinFunc r (s *o t)"
   defines "m \<equiv> wo_rel.max_fun_diff t (rev_curr f) (rev_curr g)"
   shows "wo_rel.max_fun_diff (s *o t) f g =
     (wo_rel.max_fun_diff s (rev_curr f m) (rev_curr g m), m)"
 proof -
-  interpret st!: wo_rel "s *o t" by unfold_locales (rule oprod_Well_order[OF s t])
-  interpret s!: wo_rel s by unfold_locales (rule s)
-  interpret t!: wo_rel t by unfold_locales (rule t)
-  interpret r_st!: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
-  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
-  interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
+  interpret st: wo_rel "s *o t" by unfold_locales (rule oprod_Well_order[OF s t])
+  interpret s: wo_rel s by unfold_locales (rule s)
+  interpret t: wo_rel t by unfold_locales (rule t)
+  interpret r_st: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
+  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
+  interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   from fun_unequal_in_support[OF assms(2), of "Field (s *o t)" "Field r" "Field r"] assms(3,4)
     have diff1: "rev_curr f \<noteq> rev_curr g"
       "rev_curr f \<in> FinFunc (r ^o s) t" "rev_curr g \<in> FinFunc (r ^o s) t" using rev_curr_FinFunc[OF Field]
     unfolding fun_eq_iff rev_curr_def[abs_def] FinFunc_def support_def Field_oprod
     by auto fast

 qed
 
 lemma oexp_oexp: "(r ^o s) ^o t =o r ^o (s *o t)" (is "?R =o ?L")
 proof (cases "r = {}")
   case True
-  interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
-  interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
+  interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
+  interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
   show ?thesis
   proof (cases "s = {} \<or> t = {}")
     case True with `r = {}` show ?thesis
       by (auto simp: oexp_empty[OF oexp_Well_order[OF Well_order_empty s]]
         intro!: ordIso_transitive[OF ordIso_symmetric[OF oone_ordIso] oone_ordIso]

 next
   case False
   hence Field: "Field r \<noteq> {}" by (metis Field_def Range_empty_iff Un_empty)
   show ?thesis
   proof (rule ordIso_symmetric)
-    interpret r_st!: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
-    interpret rs!: wo_rel2 r s by unfold_locales (rule r, rule s)
-    interpret rst!: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
+    interpret r_st: wo_rel2 r "s *o t" by unfold_locales (rule r, rule oprod_Well_order[OF s t])
+    interpret rs: wo_rel2 r s by unfold_locales (rule r, rule s)
+    interpret rst: wo_rel2 "r ^o s" t by unfold_locales (rule oexp_Well_order[OF r s], rule t)
     have bij: "bij_betw rev_curr (Field ?L) (Field ?R)"
     unfolding bij_betw_def r_st.Field_oexp rst.Field_oexp Field_oprod proof (intro conjI)
       show "inj_on rev_curr (FinFunc r (s *o t))"
         unfolding inj_on_def FinFunc_def Func_def Field_oprod rs.Field_oexp rev_curr_def[abs_def]
         by (auto simp: fun_eq_iff) metis