diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt index 3dcc6c0d7a2cd4abaa246ec7fdf7ad0a26a78853..29994d4683200734697d089eccb11007ee1a5139 100644 --- a/source/DefaultSituationSpace.mmt +++ b/source/DefaultSituationSpace.mmt @@ -31,5 +31,6 @@ theory DefaultSituationSpace = include ?PrismScroll ♠include ?SimpleCircleScroll ♠include ?SphereScroll ♠+ include ?CylinderScroll ♠⚠⚠diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index 6a830ccba8812df2dd44a7d70159fabf63a672ca..c9dceb29975ec1fd9be2cc56f96ac062cab07657 100644 --- a/source/MetaTheories.mmt +++ b/source/MetaTheories.mmt @@ -377,10 +377,10 @@ theory CylinderType = include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ♠include ☞http://mathhub.info/MitM/core/geometry?Planes ♠include ?FrameITBasics ♠- include ?FrameITCircle ♠cylinderType : type ☠# Cylinder ♠- cylinderCons : circle ⟶ point ⟶ Cylinder ☠# CylinderCons 1 2 ♠+ // takes a midpoint, a point on the edge of the base-circle plane, as well as a point in the base-circle plane, and a point directly above the midpoint ♠+ cylinderCons : point ⟶ point ⟶ point ⟶ point ⟶ Cylinder ☠# CylinderCons 1 2 3 4 ♠⚠theory FrameITTheories = @@ -396,6 +396,7 @@ theory FrameITTheories = include ?SphereType ♠include ?RectangleType ♠include ?CuboidType ♠+ include ?CylinderType ♠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 ♠⚠diff --git a/source/Scrolls/CylinderScroll.mmt b/source/Scrolls/CylinderScroll.mmt new file mode 100644 index 0000000000000000000000000000000000000000..20149f58c95f9f3d458463da648955492ce4ebfa --- /dev/null +++ b/source/Scrolls/CylinderScroll.mmt @@ -0,0 +1,40 @@ +namespace http://mathhub.info/FrameIT/frameworld ⚠+fixmeta ?FrameworldMeta ⚠+ + +theory CylinderScroll = + meta ?MetaAnnotations?problemTheory ?CylinderScroll/Problem ♠+ meta ?MetaAnnotations?solutionTheory ?CylinderScroll/Solution ♠+ theory Problem = + + M: point + ☠meta ?MetaAnnotations?label "M" + ☠meta ?MetaAnnotations?description "The point in the middle of the bottom circle-plane" + ♠+ E: point + ☠meta ?MetaAnnotations?label "E" + ☠meta ?MetaAnnotations?description "The point on the edge of the bottom-circle-plane" + ♠+ P: point + ☠meta ?MetaAnnotations?label "P" + ☠meta ?MetaAnnotations?description "A point in the bottom-circle-plane" + ♠+ T: point + ☠meta ?MetaAnnotations?label "T" + ☠meta ?MetaAnnotations?description "The point directly above the point M" + ♠+ + + + ⚠+ theory Solution = + include ?CylinderScroll/Problem ♠+ meta ?MetaAnnotations?label "Cylinder" ♠+ meta ?MetaAnnotations?description s"Given four points: Three points that form the bottom-plane and one directly above this scroll constructs a cylinder" ♠+ ConstructedCylinder: Cylinder + ☠= ( CylinderCons M E P T ) + ☠meta ?MetaAnnotations?label s"Cylinder" + ☠meta ?MetaAnnotations?description s"The constructed Cylinder." + ♠+ ⚠+⚠\ No newline at end of file