namespace http://mathhub.info/MitM/Foundation/Units ❚
import fnd http://mathhub.info/MitM/Foundation ❚
import rules scala://rules.mitm.mmt.kwarc.info ❚

//   http://mathhub.info/MMT/physics-units?QEBase ❚

theory Units : fnd:?Logic =
	include ☞http://mathhub.info/MitM/Foundation?RealLiterals ❙
	include ?Dimensions ❙
	
	unit : dimension ⟶ type ❙
	QE : dimension ⟶ type ❙
	
  	/T Dimensionless Quantity Expressions are real numbers ❙
  	NoneIsReal : ⊦ QE DimNone ≐≐ real_lit ❙
  	rule rules?NoneIsReal ❙
  	
	unitappl : {d : dimension} real_lit ⟶ unit d ⟶ QE d ❘ # 2 of 3 ❘ ## 2 3❙ // test... ❙
  	  
  	scalar : {X} QE X ⟶ real_lit ❘ # scalar 2 ❙
  	scalar_commutes : {X : dimension,r, u : unit X} ⊦ scalar (r of u) ≐ r ❘ role Simplify ❙
  	unitof : {X} QE X ⟶ unit X ❘ # unitof 2 ❙
  	unitof_commutes : {X : dimension,r, u : unit X} ⊦ unitof (r of u) ≐ u ❘ role Simplify ❙
	
	
	lift : {din : dimension, dout : dimension, f : ℝ ⟶ ℝ, u : unit din ⟶ unit dout}QE din ⟶ QE dout ❘ # unit_lift 3 4 ❘
		= [din,dout,f,u] [x] (f (scalar x)) of (u (unitof x)) ❙
	
	UnitTimes : {d1, d2} unit d1 ⟶ unit d2 ⟶ unit (d1 *' d2) ❘ # 3 *'' 4 ❙
	UnitDiv : {d1, d2} unit d1 ⟶ unit d2 ⟶ unit (d1 /' d2) ❘ # 3 /'' 4 ❙
	
	rule rules?UnitEq ❙
❚

theory QEBase : fnd:?Logic =
  /T A base Theory for dimensions ❙
  include ?Units ❙
  include ?DimensionsExtended❙

  /T Multiplying with numbers ❙
  // QENMul : {x : dimension} real_lit ⟶ QE x ⟶ QE x ❘ # 2 . 3 ❙

  /T Dividing by numbers ❙
  // QENDiv : {x : dimension} QE x ⟶ real_lit ⟶ QE x ❘ # 2 /. 3 ❙

  /T Multiplying quantity expressions with each other. ❙
  QEMul : {x : dimension} {y: dimension} QE x ⟶ QE y ⟶ QE (x *' y) ❘ # 3 ⋅ 4 ❙
  
  /T Dividing quantity expressions with each other. ❙
  QEDiv : {x : dimension} {y: dimension} QE x ⟶ QE y ⟶ QE (x /' y) ❘ # 3 / 4 ❙

  /T Adding quantity expressions (maintains dimension). ❙
  QEAdd : {x : dimension} QE x ⟶ QE x ⟶ QE x ❘ # 2 ++ 3 ❙
  
  QESubtract : {x: dimension} QE x ⟶ QE x ⟶ QE x ❘ # 2 - 3 ❙
  
  QEMinus : {x: dimension} QE x ⟶ QE x ❘ # ~ 2 ❙
  
  QEEExp : QE DimNone ⟶ QE DimNone ❘ # exp 1 ❙

  QEExp : QE DimNone ⟶ QE DimNone ⟶ QE DimNone ❘ # 1 ↑ 2 ❙
  
  QEELog : QE DimNone ⟶ QE DimNone ❘ # ln 1 ❙

  QELog : QE DimNone ⟶ QE DimNone ⟶ QE DimNone ❘ # log 1 2 ❙
❚

theory Field : fnd:?Logic =
  include ?QEBase❙
  
  // For now, it'll be assumed space is of Length dimension by default, 
  but that will have to be specified later for differntiating and integrating
  over fields defined on space of an arbitrary variable dimension❙

  space : type ❙
  spaceDim: dimension ❘ = Length ❙

  field : dimension ⟶ type ❘ = [d]	space ⟶ QE d ❙

	FieldAdd : {d: dimension} field d  ⟶ field d  ⟶ field d ❘ # 2 .+ 3 ❘
	         = [d,f1,f2] [s] (f1 s) ++ (f2 s) ❙
	FieldSubtract : {d: dimension} field d ⟶ field d  ⟶ field d ❘ # 2 .- 3 ❘
	         = [d,f1,f2] [s] (f1 s) - (f2 s) ❙
	FieldMul : {d1: dimension, d2: dimension} field d1 ⟶ field d2  ⟶ field (d1 *' d2) ❘ # 3 .* 4 ❘
	         = [d1,d2,f1,f2] [s] (f1 s) ⋅ (f2 s) ❙
	FieldDiv : {d1: dimension, d2: dimension} field d1 ⟶ field d2  ⟶ field (d1 /' d2) ❘ # 3 ./ 4 ❘
	         = [d1,d2,f1,f2] [s] (f1 s) / (f2 s) ❙
	FieldMinus : {d: dimension} field d  ⟶ field d ❘ # .~ 2 ❘
	         = [d,f] [s] ~ (f s) ❙
	         
	FieldEExp : field DimNone ⟶ field DimNone ❘ # exp. 1 ❘
					 = [f] [s] exp (f s) ❙
					 
	FieldExp : field DimNone ⟶ field DimNone ⟶ field DimNone ❘ # 1 .↑ 2 ❘
					 = [f1,f2] [s] (f1 s) ↑ (f2 s) ❙
					 
	FieldLog : field DimNone ⟶ field DimNone ⟶ field DimNone ❘ # log. 1 2 ❘
					 = [f1,f2] [s] log (f1 s) (f2 s) ❙
					 
	FieldELog : field DimNone ⟶ field DimNone ❘ # ln. 1 ❘
					 = [f] [s] ln (f s) ❙

	FieldEq  : {d: dimension} field d ⟶ field d  ⟶ prop ❘ # 2 .≐ 3 prec -5 ❘
	         = [d,f1,f2] ∀ [s] (f1 s) ≐ (f2 s) ❙
	         
	FieldInteg : {d} field d ⟶ field (d *' spaceDim) ❘ # ∑. 2 ❙
  
  FieldDeriv : {d} field d ⟶ field (d /' spaceDim) ❘ # Δ. 2 ❙
❚