theory Scratch
  imports Complex_Main
begin

(* Some setup, not part of the problem *)

class scaleC = scaleR +
  fixes scaleC :: "complex \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "*\<^sub>C" 75)
  assumes scaleR_scaleC: "scaleR r = scaleC (complex_of_real r)"

class complex_vector = scaleC + ab_group_add +
  assumes scaleC_add_right: "a *\<^sub>C (x + y) = (a *\<^sub>C x) + (a *\<^sub>C y)"
    and scaleC_add_left: "(a + b) *\<^sub>C x = (a *\<^sub>C x) + (b *\<^sub>C x)"
    and scaleC_scaleC[simp]: "a *\<^sub>C (b *\<^sub>C x) =  (a * b) *\<^sub>C x"
    and scaleC_one[simp]: "1 *\<^sub>C x = x"

class complex_normed_vector = complex_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
  real_normed_vector +
  assumes norm_scaleC [simp]: "norm (scaleC a x) = cmod a * norm x"

subclass (in complex_vector) real_vector
  apply standard by (auto simp add: local.scaleC_add_left local.scaleC_add_right local.scaleR_scaleC)




(* The actual problem: *)

(* Reminder: locale linear is defined as follows in Real_Vector_Spaces *)
(* locale linear = Vector_Spaces.linear "scaleR::_\<Rightarrow>_\<Rightarrow>'a::real_vector" "scaleR::_\<Rightarrow>_\<Rightarrow>'b::real_vector" *)

(* Defining the complex analogue. *)
locale clinear = Vector_Spaces.linear "scaleC::_\<Rightarrow>_\<Rightarrow>'a::complex_vector" "scaleC::_\<Rightarrow>_\<Rightarrow>'b::complex_vector"

(* Any complex linear function is also real linear *)
sublocale clinear \<subseteq> linear
  apply standard by (auto simp add: add scaleR_scaleC scale)

(* And now the local clinear is broken: *)
lemma (in clinear) "True"
(* 
Error message:

Duplicate constant declaration "local.vs1.subspace" vs. "local.vs1.subspace" (line 117 of "~~/src/HOL/Modules.thy")
The above error(s) occurred while activating facts of locale instance
vs1 : module "( *\<^sub>R)"
 *)