theory Scratch
  imports Main
begin

locale Endo =
  fixes f :: \<open>'a \<Rightarrow> 'a\<close>
  assumes \<open>f=f\<close>
begin
  definition ff where \<open>ff \<equiv> f\<circ>f\<close>
end

locale EndoCopy =
  fixes h :: \<open>'a \<Rightarrow> 'a\<close>
  assumes \<open>h=h\<close>
begin
  definition hh where \<open>hh \<equiv> h\<circ>h\<close>
end

locale CommutingEndos = Endo f for f :: \<open>'a \<Rightarrow> 'a\<close> +
  fixes g :: \<open>'a \<Rightarrow> 'a\<close>
  assumes \<open>f \<circ> g = g \<circ> f\<close>
begin

definition gg :: \<open>'a \<Rightarrow> 'a\<close> where \<open>gg = g \<circ> g\<close>

end

definition p1 :: \<open>nat \<Rightarrow> nat\<close> where \<open>p1 \<equiv> (+) 1\<close>

definition p2 :: \<open>nat \<Rightarrow> nat\<close> where \<open>p2 \<equiv> (+) 2\<close>

definition p3 :: \<open>nat \<Rightarrow> nat\<close> where \<open>p3 \<equiv> (+) 3\<close>

sublocale CommutingEndos \<subseteq> EndoCopy \<open>ff \<circ> gg\<close>
  by (simp add: EndoCopy.intro)

global_interpretation I0: Endo \<open>p1\<close>
  defines x = \<open>I0.ff\<close>
  by (simp add: Endo.intro p1_def)

thm I0.ff_def (* OK: x \<equiv> p1 \<circ> p1 *)

global_interpretation I1: CommutingEndos p1 p2
  rewrites \<open>Endo.ff p1 = x\<close>
  defines y = \<open>I1.hh\<close>
      and z = \<open>I1.gg\<close>
   apply (simp add: CommutingEndos_axioms.intro CommutingEndos_def Endo.intro o_def p1_def p2_def)
  apply (simp only: flip: x_def)
  done

thm I1.gg_def (* OK: z = p2 \<circ> p2 *)
thm z_def     (* z \<equiv> CommutingEndos.gg p2 *)

term \<open>EndoCopy.hh (x \<circ> z)\<close>

ML_val \<open>\<^term>\<open>I1.hh\<close>\<close>

thm I1.hh_def (* BAD: I1.hh \<equiv> Endo.ff p1 \<circ> z \<circ> (Endo.ff p1 \<circ> z) *)
thm y_def     (* BAD: y \<equiv> EndoCopy.hh (Endo.ff p1 \<circ> CommutingEndos.gg p2) *)

export_code y in OCaml (* No code equation for y *)

(* Can force it manually, but I thought the point of global_interpretation is that
   this manual fiddling is not necessary: *)
thm y_def[folded z_def, simplified I1.hh_def, folded x_def] (* y \<equiv> x \<circ> z \<circ> (x \<circ> z) *)
declare y_def[folded z_def, simplified I1.hh_def, folded x_def, code]

export_code y in OCaml (* OK *)

(* Manually adding a `rewrites` clause does not help either, unfortunately: *)
global_interpretation I2: CommutingEndos p1 p3
  rewrites \<open>Endo.ff p1 = x\<close>
  defines y' = \<open>I2.hh\<close>
      and z' = \<open>I2.gg\<close>
  by (auto simp add: CommutingEndos_axioms.intro CommutingEndos_def Endo.intro o_def
    p1_def p3_def x_def)

thm I2.gg_def  (* OK: z' = p3 \<circ> p3 *)
thm z'_def     (* z \<equiv> CommutingEndos.gg p3 *)

thm I2.hh_def (* Better, but still not expected: I1.gg \<equiv>  x \<circ> z' \<circ> (x \<circ> z')
                 Need LHS to be folded into y'! *)
thm y'_def     (* BAD: y \<equiv> EndoCopy.hh (Endo.ff p1 \<circ> CommutingEndos.gg p3) *)

export_code y' in OCaml (* No code equation for y *)

(* Similar hacking still needed *)
thm y'_def[folded x_def z'_def, simplified I2.hh_def] (* y' \<equiv> x \<circ> z' \<circ> (x \<circ> z') *)
lemmas y'_def[folded x_def z'_def, simplified I2.hh_def, code]

export_code y' in OCaml (* OK *)

end