update

source/units/dimensions.mmt

+namespace http://mathhub.info/MitM/Foundation/Units ❚
+
+import rules scala://rules.mitm.mmt.kwarc.info ❚
+
+theory Dimensions : ur:?LF = 
+
+  /T An SI Dimension. ❙
+  dimension : type❙
+  
+  include http://mathhub.info/MitM/Foundation?IntLiterals ❙
+  
+  /T A normalized representation used for equality reasoning etc. ❙
+  NormedDimension : ℤ ⟶ ℤ ⟶ ℤ ⟶ ℤ ⟶ ℤ ⟶ ℤ ⟶ ℤ ⟶ dimension ❙
+
+  /T We want the actual dimensions as a dimension. ❙
+  /T We use the SI base dimensions for this. ❙
+  Length : dimension ❘ // = NormedDimension 1 0 0 0 0 0 0❙
+  Time : dimension❘ // = NormedDimension 0 1 0 0 0 0 0❙
+  Mass : dimension❘ // = NormedDimension 0 0 1 0 0 0 0❙
+  Amount : dimension❘ // = NormedDimension 0 0 0 1 0 0 0❙
+  Temperature : dimension❘ // = NormedDimension 0 0 0 0 1 0 0❙
+  Current : dimension❘ // = NormedDimension 0 0 0 0 0 1 0❙
+  LuminousIntensity : dimension❘ // = NormedDimension 0 0 0 0 0 0 1 ❙
+  DimNone : dimension❘ // = NormedDimension 0 0 0 0 0 0 0 ❙
+
+  /T Now we want to make even more dimensions. ❙
+  DimTimes: dimension ⟶ dimension ⟶ dimension ❘ # 1 *' 2 ❙
+  DimDiv: dimension ⟶ dimension ⟶ dimension ❘ # 1 /' 2 ❙
+  
+  rule rules?DimEq ❙
+❚
+
+theory DimensionsExtended : ur:?LF =
+  include ?Dimensions❙
+
+  // Dimensionless stuff❙
+  Information : dimension ❘= DimNone❙
+
+  // Velocity, Accelleration ❙
+  Velocity : dimension ❘= Length /' Time❙
+  Acceleration : dimension ❘= Velocity /' Time❙
+
+  // Area and Volume❙
+  Area : dimension ❘= Length *' Length❙
+  Volume : dimension ❘= Area *' Length❙
+  
+  // Densities ❙
+  VolumeDensity : dimension ❘= DimNone /' Volume ❘  // # Density //?? ❙
+  AreaDensity : dimension ❘= DimNone /' Area❙
+  LineDensity : dimension ❘= DimNone /' Length❙
+
+  // Force and Pressure❙                   
+  Force : dimension ❘= Mass *' Acceleration❙
+  Pressure : dimension ❘= Force /' Area❙
+
+  // Electric Charge and Charge Densities❙
+  ElectricCharge : dimension ❘= Current *' Time ❙
+  ElectricChargeVolumeDensity : dimension ❘= ElectricCharge *' VolumeDensity ❘ # ElectricChargeDensity❙
+  ElectricChargeAreaDensity : dimension ❘= ElectricCharge *' AreaDensity ❘ # ElectricChargeSurfaceDensity❙
+  ElectricChargeLineDensity : dimension ❘= ElectricCharge *' LineDensity❙
+  
+  // Energy and Power❙
+  Energy : dimension ❘= Force *' Length ❙
+  Power : dimension ❘= Energy /' Time❙
+  
+  // Basic Electrostatic Units❙
+  ElectricPotential : dimension ❘= Energy /' ElectricCharge ❘ # Voltage❙
+  ElectricDisplacement : dimension ❘ = ElectricCharge /' Area ❙ 
+  ElectricCurrentDensity : dimension ❘= Current *' AreaDensity ❘ # Polarization ❘ // # CurrentDensity ❙
+  ElectricField : dimension ❘ = Voltage /' Length ❘ # ElectricFieldIntensity ❙
+  
+  // Other Electrical Units❙
+  ElectricalResistance : dimension ❘ = Voltage /' Current ❙
+  ElectricalResistivity : dimension ❘ = ElectricalResistance *' Area /' Length ❙
+  ElectricalConductivity : dimension ❘ = DimNone /' ElectricalResistivity ❙ 
+  ElectricFlux : dimension ❘ = Voltage *' Length ❙ 
+  ElectricalCapacitance : dimension ❘ = ElectricCharge /' Voltage ❙
+  ElectricalPermittivity : dimension ❘ = ElectricalCapacitance /' Length ❙
+  ElectricalMobility : dimension ❘ = Velocity /' ElectricField ❙
+  
+  IonRecombination : dimension ❘ = Volume /' Time ❙
+
+  // Magnetism // Hoping we don't need that for now
+  
+  // Heat-related , cf. Thermistor example❙
+  Heat : dimension ❘ = Energy ❙ 
+	// ThermalConductivity : dimension ❘ = Energy /' Length /' Temperature ❙ // TODO Name clash with quantities.mmt ❙
+	ThermalHeatFlux : dimension ❘ = Energy /' Area ❙ 
+  
+❚
\ No newline at end of file

source/units/quantityExpressions.mmt

+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 ❙
+❚
\ No newline at end of file

source/units/units.mmt

+namespace http://mathhub.info/MitM/Foundation/Units ❚
+
+theory SIUnits : ?QEBase =
+  // include ?InformationBase❙
+  
+  NormedUnit : {a,b,c,d,e,f,g}unit (NormedDimension a b c d e f g) ❘ # NormedUnit 1 2 3 4 5 6 7 ❙
+
+  Meter : unit Length ❘ // = NormedUnit 1 0 0 0 0 0 0 ❙
+  Second : unit Time❘ // = NormedUnit 0 1 0 0 0 0 0❙
+  Kilogram : unit Mass❘ # kg ❘ // = NormedUnit 0 0 1 0 0 0 0❙
+  Mole : unit Amount ❘ // = NormedUnit 0 0 0 1 0 0 0❙
+  Kelvin : unit Temperature❘ // = NormedUnit 0 0 0 0 1 0 0❙
+  Ampere: unit Current❘ // = NormedUnit 0 0 0 0 0 1 0❙
+  Candela : unit LuminousIntensity ❘ // = NormedUnit 0 0 0 0 0 0 1 ❙
+  Scalar : unit DimNone ❘ // = NormedUnit 0 0 0 0 0 0 0 ❙
+❚
+
+theory UnitsExtended : ?DimensionsExtended =
+	include ?SIUnits ❙
+	
+	bit : unit Information ❘ = Scalar ❙
+	
+	m2 : unit Area ❘ = Meter *'' Meter ❘ # m² ❙
+	m3 : unit Volume ❘ = m² *'' Meter ❘ # m³ ❙
+	
+	mps : unit Velocity ❘ = Meter /'' Second ❙
+	mpss : unit Acceleration ❘ = Meter /'' (Second *'' Second) ❙
+	
+	newton : unit Force ❘ = kg *'' mpss ❘ # N ❙
+	pascal : unit Pressure ❘ = N /'' m² ❘ # Pa ❙
+	
+	joule : unit Energy ❘ = N *'' Meter ❙
+❚
\ No newline at end of file