(def-theory-instance vector-spaces-over-rr
    (source vector-spaces)
    (target h-o-real-arithmetic)
    (translation fields-to-rr)
    (renamer vs-renamer))

(def-overloading +  (h-o-real-arithmetic +) (vector-spaces-over-rr ++))

(def-overloading *  (h-o-real-arithmetic *) (vector-spaces-over-rr **))

(def-constant sub_vv 
    "lambda(x,y:uu,x+[-1]*y)"
    (theory vector-spaces-over-rr))

(def-algebraic-processor vector-space-algebraic-processor
    (language vector-spaces-over-rr)
    (base ((operations
	      (+ ++)
	      (* **)
	      (sub sub_vv)
	      (zero v0))))
    (coefficient rr-algebraic-processor))

(def-overloading sub (h-o-real-arithmetic sub) (vector-spaces-over-rr sub_vv))

(def-theorem sub-lemma-for-processor 
    "forall(y,x:uu,x-y=x+v0-y)"
    (theory vector-spaces-over-rr)
    (proof
      (
        direct-inference-strategy
        unfold-defined-constants
        (force-substitution "x+(v0+[-1]*y)" "x+v0+[-1]*y" (0))
        (apply-macete-with-minor-premises %vector-zero-identity)
        (apply-macete-with-minor-premises %vector-plus-associativity)
        )))

(def-theorem ()
    "forall(x:uu,x+v0-x=v0)"
    (theory vector-spaces-over-rr)
    (proof
      (
        direct-and-antecedent-inference-strategy
        unfold-defined-constants
        (force-substitution "x+(v0+[-1]*x)" "x+v0+[-1]*x" (0))
        (apply-macete-with-minor-premises %vector-zero-identity)
        (force-substitution "x+[-1]*x" "(1+[-1])*x" (0))
        (force-substitution "(1+[-1])" "0" (0))
        (apply-macete-with-minor-premises tr%scalar-multiplication-by-zero)
        simplify
        (apply-macete-with-minor-premises %vector-times-right-distributivity)
        (apply-macete-with-minor-premises %scalar-multiplication-by-one)
        (apply-macete-with-minor-premises %vector-plus-associativity)
        )))

(def-theory-processors vector-spaces-over-rr
  (algebraic-simplifier (vector-space-algebraic-processor ** ++ sub_vv))
  (algebraic-term-comparator vector-space-algebraic-processor))

(def-language normed-linear-space-language
    (embedded-language vector-spaces-over-rr-language)
    (constants
      (norm "[uu,rr]")))

(def-theory normed-linear-spaces 
    (language normed-linear-space-language)
    (component-theories vector-spaces-over-rr)
    (axioms
      (norm-totality
        "total_q{norm,[uu, rr]}" d-r-convergence transportable-macete)
      (positivity-of-norm
        "forall(x:uu, 0<=norm(x))" transportable-macete)
      (norm-zero
        "forall(x:uu, norm(x)=0 iff x = v0)" transportable-macete)
      (norm-scalar-multiplication
        "forall(x:uu, a:rr, norm(a**x) = abs(a) * norm(x))" transportable-macete)
      (norm-triangle-inequality
        "forall(x,y:uu, norm(x++y) <= norm(x) + norm(y))" transportable-macete)))

(def-theorem ()
    "forall(x,y,z:uu,norm(x+[-1]*z)<=norm(x+[-1]*y)+norm(y+[-1]*z))"
    (theory normed-linear-spaces)
    (proof
      (
      
        (force-substitution "x+[-1]*z" "(x+[-1]*y)+(y+[-1]*z)" (0))
        (apply-macete-with-minor-premises norm-triangle-inequality)
        simplify
        )))

(def-theorem ()
    "forall(x,y,z:uu, norm([-1]*z+x)<=norm([-1]*z+y)+norm(x+[-1]*y))"
    (theory normed-linear-spaces)
    (proof
      (
        (force-substitution "[-1]*z+x" "([-1]*z+y)+(x+[-1]*y)" (0))
        (apply-macete-with-minor-premises norm-triangle-inequality)
        simplify
        )))

(def-theorem ()
    "forall(x,y:uu,norm(x+[-1]*y)=norm([-1]*x+y))"
    (theory normed-linear-spaces)
    (proof
      (
        (force-substitution "x+[-1]*y" "[-1]*([-1]*x+y)" (0))
        (apply-macete-with-minor-premises norm-scalar-multiplication)
        (apply-macete-with-minor-premises absolute-value-non-positive)
        simplify
        simplify
        )))

(def-theorem ()
    "forall(x,y:uu,x=y iff norm(x+[-1]*y)=0)"
    (theory normed-linear-spaces)
    (proof 
      (
        (apply-macete-with-minor-premises norm-zero)
        simplify
        )))

(def-theory-ensemble-instances
  metric-spaces 
  force-under-quick-load
  (target-theories normed-linear-spaces normed-linear-spaces)
  (multiples 1 2)
  (theory-interpretation-check using-simplification)
  (sorts (pp uu uu))
  (constants (dist "lambda(x,y:uu, norm(x-y))" "lambda(x,y:uu, norm(x-y))")))

(def-theory-ensemble-overloadings metric-spaces (1 2))

(def-theorem closed-balls-are-defined 
  "forall(b:uu,r:rr,#(ball(b,r)))"
  (theory normed-linear-spaces)
  (usages d-r-convergence)
  (proof 
    (
      unfold-defined-constants
      simplify-insistently
      )))

(def-theorem open-balls-are-defined 
  "forall(b:uu,r:rr,#(open%ball(b,r)))"
  (theory normed-linear-spaces)
  (usages d-r-convergence)
  (proof 
    (
      
      unfold-defined-constants
      simplify-insistently
      
      )))

(def-theorem ()
    "norm(v0)=0"
    (usages rewrite)
    (theory normed-linear-spaces)
    (proof
      (
        (apply-macete-with-minor-premises norm-zero)
        )))

(def-theorem norm-continuity-lemma 
    "forall(x,y,z:uu, norm(x)-norm(y)<=norm(x-y))"
    (theory normed-linear-spaces)
    (proof
      (
        (force-substitution "norm(x)-norm(y)<=norm(x-y)" "norm((x-y)+y)<=norm(x-y)+norm(y)" (0))
        (apply-macete-with-minor-premises norm-triangle-inequality)
        simplify
        )))

(def-theorem vs-addition-of-fractions-left  
    "forall(a,b:rr,u,y:uu,a/b*u + y == (1/b)*(a*u+b*y))"
    (proof
      (
        (apply-macete-with-minor-premises %vector-times-left-distributivity)
        (force-substitution "1/b*(b*y)" "(1/b*b)*y" (0))
        direct-and-antecedent-inference-strategy
        (case-split ("b=0"))
        simplify
        simplify
        (apply-macete-with-minor-premises %vector-times-associativity)
        ))
    (theory vector-spaces-over-rr))

(def-theorem vs-addition-of-fractions-right  
  "forall(a,b:rr,u,y:uu, y+a/b*u == (1/b)*(a*u+b*y))"
  (proof
      (
        (apply-macete-with-minor-premises %vector-times-left-distributivity)
        (force-substitution "1/b*(b*y)" "(1/b*b)*y" (0))
        direct-and-antecedent-inference-strategy
        (case-split ("b=0"))
        simplify
        simplify
        (apply-macete-with-minor-premises %vector-times-associativity)
        ))
  (theory vector-spaces-over-rr))

(def-theorem sub-replacement 
    "forall(x,y:uu,x-y=x+[-1]*y)"
    (proof
      (
        simplify
        ))
    (theory vector-spaces-over-rr))

(def-theorem vector-times-associativity-left 
    "forall(a,b:rr,x:uu,a*(b*x)=(a*b)*x)"
    (proof
      (
        simplify
        ))
    (theory vector-spaces-over-rr))

(def-compound-macete ns-fractional-expression-manipulation 
    (repeat
        vs-addition-of-fractions-right
        vs-addition-of-fractions-left
        sub-replacement
        vector-times-associativity-left
        norm-scalar-multiplication))