Newer
Older
// import rules scala://rules.frameit.mmt.kwarc.info ❚
/T MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls ❚
theory MetaAnnotations =
include ☞http://mathhub.info/MitM/Foundation?Strings ❙
label ❙
description ❙
problemTheory ❙
solutionTheory❙
/T Example usages:
- `lverb A`, where A refers to a symbol
- `lverb A B`, a shorthand for `concat (lverb A) (lverb B)`; works for arbitrary number of arguments
❙
label_verbalization_of # lverb ❙
description_verbalization_of # dverb ❙
❚
include ?FrameITBasics ❙
// simple 2d Point theory. ❙
Point2D : type ❘ # point2d ❙
Point2Dmk : ℝ ⟶ ℝ ⟶ point2d ❘ # mkpoint2d 1 2 ❙
XPoint2D : point2d ⟶ ℝ ❘ # p2x 1 ❙
XPoint2DAxiom : {x,y} ⊦ ( p2x (mkpoint2d x y ) ≐ x ) ❘ role Simplify❙
YPoint2D : point2d ⟶ ℝ ❘ # p2y 1 ❙
YPoint2DAxiom : {x,y} ⊦ ( p2y (mkpoint2d x y ) ) ≐ y ❘ role Simplify ❙
❚
theory FrameITBasics =
include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
// Basics for FrameIT theories ❙
// a lot of Simplify roles, so the scrolls get simplified accordingly ❙
axiomrealNumbersNeutralLeft : {x: ℝ } ⊦ 1.0 ⋅ x ≐ x ❘ role Simplify ❙
axiomrealNumbersNeutralRight : {x: ℝ } ⊦ x ⋅ 1.0 ≐ x ❘ role Simplify ❙
axiomBasepoint2 : {p1,p2} ⊦ from (from p1 to p2) ≐ p1 ❘ role Simplify ❙
axiomTargetpoint2 : {p1,p2} ⊦ to (from p1 to p2) ≐ p2 ❘ role Simplify ❙
PlaneBaseAxiom12 : {v, w, b } ⊦ Pbase (Ppara b v w ) ≐ b ❘ role Simplify ❙
PlaneBaseAxiomNormal2 : { v, b } ⊦ ( Pbase ( Ppn b v ) ) ≐ b ❘ role Simplify ❙
normalAxiom12 : { v, w, b } ⊦ ( Pnormal ( Ppara b v w ) ) ≐ ( normalize ( v Vcross w ) ) ❘ role Simplify ❙
normalAxiom22 : { v, b } ⊦ ( Pnormal ( Ppn b v ) ) ≐ ( norm ( v ) ) ❘ role Simplify ❙
rightAngle : point ⟶ point ⟶ point ⟶ bool ❘ # ∠r 1 2 3 ❙
epsi = 0.000000000004626 ❙
// early on there where problems with those functions. They might not be required anymore ❙
multiplyPointScalar : ℝ ⟶ point ⟶ point ❘ = [a, P ] ⟨a ⋅ ( P _x ) , a ⋅ (P _y ), a ⋅ (P _z )⟩ ❘ # 1 rdotp 2 prec 22 ❙
addPointPoint : point ⟶ point ⟶ point ❘ = [Q,P ] ⟨ ( Q _x ) + ( P _x ) , ( Q _y ) + (P _y ), ( Q _z ) + (P _z )⟩ ❘ # 1 p+p 2 prec 12 ❙
subtractPointPoint : point ⟶ point ⟶ point ❘ = [Q,P ] ⟨ ( Q _x ) - ( P _x ) , ( Q _y ) - (P _y ), ( Q _z ) - (P _z )⟩ ❘ # 1 p-p 2 prec 12 ❙
directionLine : line ⟶ point ❘ = [l] ( to l ) p-p ( from l ) ❘ # directionL 1 ❙
// added those, because sometimes you cant use certain operations in scrolls? Maybe this bug is fixed by now? ❙
useRoot : ℝ ⟶ ℝ ❘ = [a] √ a ❘ # doRoot 1 ❙
absValue : ℝ ⟶ ℝ ❘ = [a] √ (real_pow a 2.0 ) ❘ # doAbs 1 ❙
useDiv : ℝ ⟶ ℝ ⟶ ℝ ❘ = [a,b] a / b ❘ # doDiv 1 2 ❙
useInv : ℝ ⟶ ℝ ❘ = [a] inv a ❘ # doInv 1 ❙ // trying to make inv work ❙
useExpo : ℝ ⟶ ℝ ⟶ ℝ ❘ = [a,b] real_pow a b ❘ # doExpo 1 2 ❙
// projection and distance function for planes ❙
helperFunctionForProjection : plane ⟶ point ⟶ ℝ ❘ = [e, p] ( < ( Pnormal e ) , ( planeBase e ) > - < ( Pnormal e ) , p > ) / ( < ( Pnormal e ) , ( Pnormal e ) > ) ❘ # helperT 1 2 prec 1 ❙
orthogonalProjectionPointToPlane : plane ⟶ point ⟶ point ❘ = [e,p] p p+p ( ( helperT e p ) rdotp( Pnormal e ) ) ❘ # orthogProjPointToPlane 1 2 prec 1 ❙
distancePlanePoint : plane ⟶ point ⟶ ℝ ❘ = [e,p] ( doAbs ( < Pnormal e , p > - < Pnormal e , Pbase e > ) ) / ( | Pnormal e | + epsi ) ❘ # distPlP 1 2 prec 1 ❙
// functions to calculate the angle between a plane and a line ❙
anglePlaneLineCalc : point ⟶ point ⟶ ℝ ❘ = [v,w] asin ( < v,w > / ( (|v| ⋅ |w|) + epsi )) ❘ # plcalc 1 2 prec 1 ❙
anglePlaneLine : plane ⟶ line ⟶ ℝ ❘ = [e,l] plcalc ( Pnormal e ) ( directionL l ) ❘ # ∠pl 1 2 prec 1 ❙
radToDegree : ℝ ⟶ ℝ ❘ = [r] ( r / pi_num ) ⋅ 180.0 ❘ # radToDegree 1 prec 1 ❙
// obvious proofs that sometimes are required ❙
lineOnProofFrom: {l } ⊦ ( from l ) on l ❘ # fromOnProofLine 1 ❙
lineOnProofTo: {l } ⊦ ( to l ) on l ❘ # toOnProofLine 1 ❙
normalizeSafe: point ⟶ point ❘ = [v] (1.0 / ( | v | + epsi )) ⋅⋅ v ❘ # normS 1 ❙
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
❚
theory FrameITRectangles =
include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
include ?FrameITBasics ❙
// used for parallelLineTheorem ❙
isRectangle : point ⟶ point ⟶ point ⟶ point ⟶ bool ❘ = [p1, p2 , p3, p4] ( rightAngle p1 p2 p3) ∧ ( rightAngle p2 p3 p4) ∧ ( rightAngle p3 p4 p1) ∧ ( rightAngle p4 p1 p2) ❘ # isRect 1 2 3 4 ❙
rectangleProof : {p1,p2,p3,p4} { proof1 : ⊦ rightAngle p1 p2 p3 } { proof2 : ⊦ rightAngle p2 p3 p4 } { proof3 : ⊦ rightAngle p3 p4 p1 } { proof4 : ⊦ rightAngle p4 p1 p2 } ⊦ isRect p1 p2 p3 p4 ❘ # isRectProof 5 6 7 8 ❙
axiomRectParallelOne : {p1,p2,p3,p4} { proof1 : ⊦ isRect p1 p2 p3 p4 } ⊦ paraL (from p1 to p2) (from p3 to p4) ❙
axiomRectParallelOneAdjusted : {g1,g2,p1,p2,p3,p4} { proof1 : ⊦ isRect p1 p2 p3 p4 } { proof_p1_on_g1 : ⊦ p1 on g1 } { proof_p2_on_g1 : ⊦ p2 on g1 } { proof_p3_on_g2 : ⊦ p3 on g2 } { proof_p4_on_g2 : ⊦ p4 on g2 } ⊦ paraL g1 g2 ❘ # axiomRectParallel 7 8 9 10 11 ❙
axiomRectParallelADBC: {g1: line,g2: line,p1: point,p2: point,p3: point,p4: point} { proof1 : ⊦ isRect p1 p2 p3 p4 } { proof_p1_on_g1 : ⊦ p1 on g1 } { proof_p4_on_g1 : ⊦ p4 on g1 } { proof_p2_on_g2 : ⊦ p2 on g2 } { proof_p3_on_g2 : ⊦ p3 on g2 } ⊦ paraL g1 g2 ❘ # axRectParallelADBC 7 8 9 10 11 ❙
// tried to define a rectangle type ❙
// TODO maybe delete ❙
rectangle_type : type ❘ # rect ❙
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
mkRectangle : { A: point , B : point, C : point , D : point } ( ⊦ isRect A B C D ) ⟶ rect ❘ # mkRect 1 2 3 4 5 ❙
cornerA : rect ⟶ point ❘ # rectA 1 ❙
cornerB : rect ⟶ point ❘ # rectB 1 ❙
cornerC : rect ⟶ point ❘ # rectC 1 ❙
cornerD : rect ⟶ point ❘ # rectD 1 ❙
rectSideAD : rect ⟶ line ❘ # rectAD 1 ❙
rectSideBC : rect ⟶ line ❘ # rectBC 1 ❙
axiomCornerA : {A,B,C,D,p} ⊦ ( cornerA ( mkRectangle A B C D p ) ≐ A ) ❘ role Simplify ❙
axiomCornerB : {A,B,C,D,p} ⊦ ( cornerB ( mkRectangle A B C D p ) ≐ B ) ❘ role Simplify ❙
axiomCornerC : {A,B,C,D,p} ⊦ ( cornerC ( mkRectangle A B C D p ) ≐ C ) ❘ role Simplify ❙
axiomCornerD : {A,B,C,D,p} ⊦ ( cornerD ( mkRectangle A B C D p ) ≐ D ) ❘ role Simplify ❙
axiomSideAD : {A,B,C,D,p} ⊦ ( rectSideAD ( mkRectangle A B C D p ) ≐ ( from A to D ) ) ❘ role Simplify ❙
axiomSideBC : {A,B,C,D,p} ⊦ ( rectSideBC ( mkRectangle A B C D p ) ≐ ( from B to C ) ) ❘ role Simplify ❙
rectParalleABCD : {r: rect } ⊦ ( paraL ( from ( cornerA r ) to ( cornerB r ) ) ( from ( cornerC r) to ( cornerD r ) ) ) ❘ # rParalleABCD 1 ❙
// rect_paralle_AD_BC : {r: rect } ⊦ ( paraL ( from ( corner_A r ) to ( corner_D r ) ) ( from ( corner_B r) to ( corner_C r ) ) ) ❘ # r_paralle_AD_BC 1 ❙
rectParalleADBC : {r: rect } ⊦ ( paraL ( rectSideAD r ) ( rectSideBC r ) ) ❘ # rParalleADBC 1 ❙
rectParallADBCProof2 : {r: rect, ad: line, bc: line, p1 : ⊦ ( rectSideAD r ) ≐ ad , p2 : ⊦ ( rectSideBC r ) ≐ bc } ⊦ paraL ad bc ❘ # parallelADBCProofv2 1 2 3 %I4 %I5 ❙
❚
theory FrameITTriangles =
include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
include ?FrameITBasics ❙
// some theories for triangles ❙
// TODO maybe delete ❙
// triangle rules we need to simplify terms ... ❙
axiomAtriangle : {a,b,c} ⊦ ( _A ( Δ a b c ) ) ≐ a ❘ role Simplify ❙
axiomBtriangle : {a,b,c} ⊦ ( _B ( Δ a b c ) ) ≐ b ❘ role Simplify ❙
axiomCtriangle : {a,b,c} ⊦ ( _C ( Δ a b c ) ) ≐ c ❘ role Simplify ❙
triangleToPlane2: triangle ⟶ plane ❘ = [t] ( Ppara ( _A t ) ( ( _A t ) p-p ( _B t ) ) ( ( _A t ) p-p ( _C t ) ) ) ❘ # Pof2Δ 1 ❙
// additional triangle rules ❙
// Mittelsenkrechten und deren Schnittpunkt ❙
trianglePerpendicularBisectorAB3D : triangle ⟶ line ❘ = [t] from ( 0.5 rdotp ( ( _A t ) p+p ( _B t ) ) ) to ( ( 0.5 rdotp ( ( _A t ) p+p ( _B t ) ) ) p+p ( ( Pnormal ( Pof2Δ t ) ) Vcross ( ( _B t ) p-p ( _A t ) ) ) ) ❘ # bisecTriAB3D 1 ❙
trianglePerpendicularBisectorBC3D : triangle ⟶ line ❘ = [t] from ( 0.5 rdotp ( ( _B t ) p+p ( _C t ) ) ) to ( ( 0.5 rdotp ( ( _B t ) p+p ( _C t ) ) ) p+p ( ( Pnormal ( Pof2Δ t ) ) Vcross ( ( _C t ) p-p ( _B t ) ) ) ) ❘ # bisecTriBC3D 1 ❙
trianglePerpendicularBisectorCA3D : triangle ⟶ line ❘ = [t] from ( 0.5 rdotp ( ( _C t ) p+p ( _A t ) ) ) to ( ( 0.5 rdotp ( ( _C t ) p+p ( _A t ) ) ) p+p ( ( Pnormal ( Pof2Δ t ) ) Vcross ( ( _A t ) p-p ( _C t ) ) ) ) ❘ # bisecTriCA3D 1 ❙
trianglePerpendicularBisectorIntersectAxiom : { t } ⊦ colL ( bisecTriAB3D t ) ( bisecTriBC3D t) ❘ # perpBisIntersectAxiomABBC 1 ❙
cramerRuleIntersection : point ⟶ point ⟶ point ⟶ ℝ ❘ = [c,u,v] ( (-1.0 ⋅ ( c _x ) ⋅ ( v _y ) ) + ( ( c _y ) ⋅ ( v _x ) ) ) / ( epsi + ( (-1.0 ⋅ ( u _x ) ⋅ ( v _y ) ) + ( ( u _y ) ⋅ ( v _x ) )) ) ❘ # CramerRuleIntersection 1 2 3 ❙
// This function shouldn't be necessary. But due to some weird bug, the server will crash without it. ❙
wrapCramerRuleIntersectionForIntersectingBisectors : line ⟶ line ⟶ ℝ ❘ = [l,h] ( cramerRuleIntersection ( ( from l ) p-p ( from h ) ) ( directionL l ) ( directionL h ) ) ❘ # CramerRuleIntersectionLines 1 2 ❙
intersectionTwoLines : line ⟶ line ⟶ point ❘ = [l,h] ( from l ) p+p ( ( CramerRuleIntersectionLines l h ) rdotp ( directionL l ) ) ❘ # intersectTwoLinesActualPoint 1 2 ❙
triangleMidPoint : triangle ⟶ point ❘ = [t] intersectTwoLinesActualPoint ( bisecTriAB3D t ) ( bisecTriBC3D t) ❘ # midTriangle3D 1 ❙
triangleMidPointWrapper : point ⟶ point ⟶ point ⟶ point ❘ = [p1,p2,p3] midTriangle3D ( Δ A B C ) ❘ # midTriangle3DWrap 1 2 3 ❙
❚
theory FrameITCircle =
include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
include ?FrameITBasics ❙
circleType3D : type ❘ # circle ❙
xcircleType3D : type ❘ # xcircle ❘ = plane × point × ℝ ❙
xcircleMidPoint: xcircle ⟶ point ❘ # xmid 1 ❘ = [c] πl (πr c) ❙
// circle constructor taking a plane ( the circle lies in ) a point (middle) and a real number (radius) ❙
circle3D : plane ⟶ point ⟶ ℝ ⟶ circle ❘ # mkCirc3D 1 2 3 ❙
circleMidPoint : circle ⟶ point ❘ # mid 1 ❙
circleRadius : circle ⟶ ℝ ❘ # radius 1 ❙
circlePlane : circle ⟶ plane ❘ # planeCircle 1 ❙
axiomMidPoint : {e,p,r} ⊦ mid (mkCirc3D e p r) ≐ p ❘ role Simplify ❙
axiomPlane : {e,p,r} ⊦ planeCircle (mkCirc3D e p r) ≐ e ❘ role Simplify ❙
axiomRadius : {e,p,r} ⊦ radius (mkCirc3D e p r) ≐ r ❘ role Simplify ❙
pointOnCircle : circle ⟶ point ⟶ bool ❘ = [c,p] ( p VonP ( planeCircle c ) ) ∧ ( leq_real_lit ( d-p ( mid c ) ) ( radius c ) ) ❘ # 2 VonC 1 ❙
midAlwaysOnCircle : {c: circle, m: point, p: ⊦ ( mid c ) ≐ m } ⊦ m VonC c ❘ # midOnC 1 2 %I3 ❙
areaCircle : circle ⟶ ℝ ❘ = [c] ( real_pow ( radius c) 2.0 ) ⋅ pi_num ❘ # areaCirc 1 ❙
circumCircle : circle ⟶ ℝ ❘ = [c] 2.0 ⋅ ( radius c ) ⋅ pi_num ❘ # circCirc 1 ❙
angleCircleLine : circle ⟶ line ⟶ ℝ ❘ = [c,l] radToDegree ( plcalc ( Pnormal ( planeCircle c ) ) ( directionL l ) ) ❘ # ∠cl 1 2 prec 1 ❙
orthogonalCircleLine : circle ⟶ line ⟶ bool ❘ # orthogCL 1 2 ❙
pointsToPlaneNormal : point ⟶ point ⟶ point ⟶ plane ❘ = [p1,p2,p3] Ppn p1 ( normalizeSafe ( (p2 p-p p1 ) Vcross ( p3 p-p p1) ) ) ❘ # pToPlane 1 2 3 ❙
wrap3EdgePointsToPlaneParametric : point ⟶ point ⟶ point ⟶ plane ❘ = [p1,p2,p3 ] Ppara p1 (p2 p-p p1 ) ( p3 p-p p1) ❘ # pointsToPlanePara 1 2 3 ❙
parallelCircles: circle ⟶ circle ⟶ bool ❘ # paraCirc 1 2 ❙
proofParallelCircles : {c1: circle, c2:circle, ab: line, p1: ⊦ orthogCL c1 ab , p2: ⊦ orthogCL c2 ab } ⊦ paraCirc c1 c2 ❘ # axParaCirc 1 2 3 4 5 ❙
equalityCircles: circle ⟶ circle ⟶ bool ❘ # equalCirc 1 2 ❙
unequalityCircles : circle ⟶ circle ⟶ bool ❘ # unequalCirc 1 2 ❙
helperXyZ : point ⟶ point ⟶ ℝ ❘ = [a,b] | a -- b | ❘ # helpxyz 1 2 ❙
pointsToCircleChecker : { M : point, A : point, B : point, MAsum: ℝ, MBsum: ℝ, ABsum: ℝ , p1 : ⊦ ( MAsum ≠ 0 ) , p2 : ⊦ ( MBsum ≠ 0 ) , p3 : ⊦ ( ABsum ≠ 0 ) } circle ❘ = [A,B,C,p1,p2,p3,p4,p5,p6] mkCirc3D ( pToPlane M A B ) M (d- M A) ❘ # pointsToCCheck 1 2 3 4 5 6 %I7 %I8 %I9 ❙
pointsToCircleCheckerTest : { M : point, A : point, B : point, MAsum: ℝ, MBsum: ℝ, ABsum: ℝ , p1 : ⊦ ( MAsum ≠ 0.0 ), p2 : ⊦ ( MBsum ≠ 0.0 ) , p3 : ⊦ ( ABsum ≠ 0.0 ) } circle ❘ = [M,A,B,p4,p5,p6,p7,p8,p9] mkCirc3D ( pToPlane M A B ) M (d- M A) ❘ # pointsToCChecktest 1 2 3 4 5 6 %I7 %I8 %I9 ❙
pointsToCircleWrapper : point ⟶ point ⟶ point ⟶ circle ❘ = [M,A,B] pointsToCChecktest M A B (helpxyz M A) ( helpxyz M B ) ( helpxyz A B ) ❘ # pointsToC 1 2 3 ❙
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
❚
theory FrameITCone =
include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
include ?FrameITBasics ❙
include ?FrameITCircle ❙
circleConeType : type ❘ # cone ❙
circleConeOf : circle ⟶ point ⟶ cone ❘ # planeC 1 apex 2 ❙
circleConeApex : cone ⟶ point ❘ # coneApex 1 prec 1 ❙
circleConePlane : cone ⟶ circle ❘ # conePl 1 prec 1 ❙
axiomConeApex : {c, p} ⊦ coneApex ( planeC c apex p ) ≐ p ❘ role Simplify ❙
axiomConePlane : {c,p} ⊦ conePl ( planeC c apex p ) ≐ c ❘ role Simplify ❙
coneHeightProjection : cone ⟶ point ❘ = [c] orthogProjPointToPlane ( planeCircle ( conePl c ) ) ( coneApex c ) ❘ # coneHeightOnBaseProj 1 prec 1 ❙
coneHeightLine : cone ⟶ line ❘ = [c] from ( coneApex c) to ( coneHeightOnBaseProj c ) ❘ # heightLineC 1 prec 1 ❙
coneHeightLength : cone ⟶ ℝ ❘ = [c] d- ( coneApex c) ( coneHeightOnBaseProj c ) ❘ # heightLengthC 1 prec 1 ❙
// distance_apex_plane : cone ⟶ ℝ ❘ = [c] ( do_abs ( < Pnormal ( circle_plane ( cone_plane c ) ) , cone_apex c > - < Pnormal ( circle_plane ( cone_plane c ) ) , Pbase ( circle_plane ( cone_plane c ) ) > ) ) / ( | Pnormal ( circle_plane ( cone_plane c ) ) | ) ❘ # dist_p_s 1 prec 1 ❙
distApexPlane : cone ⟶ ℝ ❘ = [c] distPlP ( circlePlane ( conePl c ) ) ( coneApex c ) ❘ # distPS 1 prec 1 ❙
volumeCone : cone ⟶ ℝ ❘ = [c] ( areaCirc ( conePl c) ) ⋅ ( distPS c) / 3.0 ❘ # volCone 1 prec 1 ❙
baseAreaCone : cone ⟶ ℝ ❘ = [c] ( areaCirc ( conePl c ) ) ❘ # baseAreaC 1 prec 1 ❙
// truncated cones ❙
truncatedConeType : type ❘ # tcone ❙
mkTruncatedCone : {c1: circle, c2: circle, proofUnEqual: ( ⊦ unequalCirc c1 c2) } ( ⊦ paraCirc c1 c2 ) ⟶ tcone ❘ # mkTcone 1 2 3 4 ❙
truncatedConeBase : tcone ⟶ circle ❘ # tconeBase 1 ❙
truncatedConeTop : tcone ⟶ circle ❘ # tconeTop 1 ❙
axiomTruncatedConeBase : {c1, c2,p1, p2} ⊦ tconeBase ( mkTcone c1 c2 p1 p2) ≐ c1 ❘ role Simplify ❙
axiomTruncatedConeTop : {c1, c2,p1, p2} ⊦ tconeTop ( mkTcone c1 c2 p1 p2) ≐ c2 ❘ role Simplify ❙
// swapped top and base should be fine tho❙
truncatedConeHeight : tcone ⟶ ℝ ❘ = [tc] distPlP ( circlePlane ( tconeBase tc ) ) ( mid ( tconeTop tc ) ) ❘ # tconeHeight 1 ❙
truncatedConeArea : tcone ⟶ ℝ ❘ = [tc] ( areaCirc ( tconeBase tc ) ) + ( ( ( radius ( tconeTop tc ) ) ⋅ ( radius ( tconeBase tc ) ) ) ⋅ pi_num ) + ( areaCirc ( tconeTop tc ) ) ❘ # tconeArea 1 ❙
truncatedConeVolume : tcone ⟶ ℝ ❘ = [tc] ( 1.0 / 3.0 ) ⋅ (tconeHeight tc) ⋅ ( tconeArea tc ) ❘ # tconeVol 1 ❙
❚
theory FrameITCylinder =
include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
include ?FrameITBasics ❙
include ?FrameITCircle ❙
cylinderType : type ❘ # cyl ❙
mkCylinder : {c1: circle, c2: circle, proofEqual: ( ⊦ equalCirc c1 c2) } ( ⊦ paraCirc c1 c2 ) ⟶ cyl ❘ # mkCyl 1 2 3 4 ❙
cylinderBase : cyl ⟶ circle ❘ # cylBase 1 ❙
cylinderTop : cyl ⟶ circle ❘ # cylTop 1 ❙
axCylBase : {c1, c2, p1, p2} ⊦ cylBase ( mkCyl c1 c2 p1 p2) ≐ c1 ❘ role Simplify ❙
axCylTop : {c1, c2, p1, p2} ⊦ cylTop ( mkCyl c1 c2 p1 p2) ≐ c2 ❘ role Simplify ❙
cylinderArea : cyl ⟶ ℝ ❘ = [c] areaCirc ( cylBase c) ❘ # cylArea 1 prec 1 ❙
cylinderHeight : cyl ⟶ ℝ ❘ = [c] d- ( mid ( cylBase c) ) ( mid ( cylTop c) ) ❘ # cylHeight 1 prec 1 ❙
cylinderVolume : cyl ⟶ ℝ ❘ = [c] (cylHeight c) ⋅ ( cylArea c ) ❘ # cylVol 1 ❙
❚
theory FrameITTheories =
include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
include ?FrameITTriangles ❙
include ?FrameITRectangles ❙
include ?FrameITCircle ❙
include ?FrameITCone ❙
include ?FrameITCylinder ❙
makeCircleOf3EdgePoints : point ⟶ point ⟶ point ⟶ circle ❘ = [p1,p2,p3 ] mkCirc3D ( Ppara p1 (p2 p-p p1) ( p3 p-p p1) ) ( midTriangle3D ( Δ p1 p2 p3 ) ) ( d- ( midTriangle3D ( Δ p1 p2 p3 ) ) p1 ) ❘ # mkCirc3P3D 1 2 3 ❙
❚
/T The meta theory to use for situation theories, scroll problem, and scroll solution theories ❚
theory FrameworldMeta =
include ?MetaAnnotations ❙
// include ☞http://mathhub.info/MitM/core/arithmetics?RealArithmetics ❙
// include ☞http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma ❙
// include ☞http://mathhub.info/MitM/Foundation?Strings ❙
// include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
// include ☞http://mathhub.info/MitM/core/geometry?Planes ❙