diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt index cc1468e7a3b6768efb32d05cc33f319f7b681bc5..88876efaaf1c69e971f6698367736642eeb88526 100644 --- a/source/DefaultSituationSpace.mmt +++ b/source/DefaultSituationSpace.mmt @@ -29,6 +29,7 @@ theory DefaultSituationSpace = include ?RectangleScroll ♠include ?CuboidScroll ♠include ?TriangleScroll ♠+ include ?SimpleCircleScroll ♠diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index 3ae26be43561448283f2f3df4eaa7d2381a01254..23a77a7a928f380052dbbe33e379d0094ccd5a3d 100644 --- a/source/MetaTheories.mmt +++ b/source/MetaTheories.mmt @@ -338,6 +338,7 @@ theory FrameworldMeta = include ?RectangleType ♠include ?CuboidType ♠include ?TriangleType ♠+ include ?CircleType ♠// include ☞http://mathhub.info/MitM/core/arithmetics?RealArithmetics ♠diff --git a/source/Scrolls/CircleType.mmt b/source/Scrolls/CircleType.mmt new file mode 100644 index 0000000000000000000000000000000000000000..2fda840962d384422cc2441ddfa2d5137a83f425 --- /dev/null +++ b/source/Scrolls/CircleType.mmt @@ -0,0 +1,12 @@ +namespace http://mathhub.info/FrameIT/frameworld ⚠+fixmeta ?FrameworldMeta ⚠+ +theory CircleType = + + include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ♠+ include ?FrameITBasics ♠+ + circleType : type ☠# Circle ♠+ circleCons : point ⟶ point ⟶ point ⟶ Circle ☠# CircleCons 1 2 3 ♠+ +⚠\ No newline at end of file diff --git a/source/Scrolls/SimpleCircleScroll.mmt b/source/Scrolls/SimpleCircleScroll.mmt new file mode 100644 index 0000000000000000000000000000000000000000..c447f0d03b4a0d090d43d8a1925e0312d24a1b79 --- /dev/null +++ b/source/Scrolls/SimpleCircleScroll.mmt @@ -0,0 +1,40 @@ +namespace http://mathhub.info/FrameIT/frameworld ⚠+fixmeta ?FrameworldMeta ⚠+ + +theory SimpleCircleScroll = + meta ?MetaAnnotations?problemTheory ?SimpleCircleScroll/Problem ♠+ meta ?MetaAnnotations?solutionTheory ?SimpleCircleScroll/Solution ♠+ + theory Problem = + + M: point + ☠meta ?MetaAnnotations?label "M" + ☠meta ?MetaAnnotations?description "The midpoint of the circle" + ♠+ A: point + ☠meta ?MetaAnnotations?label "A" + ☠meta ?MetaAnnotations?description "The edge point of the circle" + ♠+ B: point + ☠meta ?MetaAnnotations?label "T" + ☠meta ?MetaAnnotations?description "A point on the plane of the circle" + ♠+ + + + + + ⚠+ theory Solution = + include ?SimpleCircleScroll/Problem ♠+ meta ?MetaAnnotations?label "Circle" ♠+ meta ?MetaAnnotations?description s"Takes a midpoint, a point on the edge of the circle and a point on the plane of it to construct a circle" ♠+ + ConstructedCircle : Circle + ☠= ( CircleCons M A B ) + ☠meta ?MetaAnnotations?label s"Circle" + ☠meta ?MetaAnnotations?description s"The constructed circle" + ♠+ ⚠+⚠\ No newline at end of file diff --git a/source/Scrolls/SphereScroll.mmt b/source/Scrolls/SphereScroll.mmt new file mode 100644 index 0000000000000000000000000000000000000000..9ebdb1d19fcb9291e38c829b89f89de96c968ed9 --- /dev/null +++ b/source/Scrolls/SphereScroll.mmt @@ -0,0 +1,36 @@ +namespace http://mathhub.info/FrameIT/frameworld ⚠+fixmeta ?FrameworldMeta ⚠+ + +theory SphereScroll = + meta ?MetaAnnotations?problemTheory ?SphereScroll/Problem ♠+ meta ?MetaAnnotations?solutionTheory ?SphereScroll/Solution ♠+ + theory Problem = + + C: circle + ☠meta ?MetaAnnotations?label "C" + ☠meta ?MetaAnnotations?description "center-circle" + ♠+ T: point + ☠meta ?MetaAnnotations?label "T" + ☠meta ?MetaAnnotations?description "The top point above the center circle. Has to be parallel to the normal or the normal" + ♠+ + + + + + ⚠+ theory Solution = + include ?SphereScroll/Problem ♠+ meta ?MetaAnnotations?label "Sphere" ♠+ meta ?MetaAnnotations?description s"Takes a circle and a point parallel to the normal, then constructs a Sphere." ♠+ + ConstructedRectangle : Rectangle + ☠= ( SphereCons C T ) + ☠meta ?MetaAnnotations?label s"Sphere" + ☠meta ?MetaAnnotations?description s"The constructed Sphere." + ♠+ ⚠+⚠\ No newline at end of file diff --git a/source/Scrolls/SphereType.mmt b/source/Scrolls/SphereType.mmt new file mode 100644 index 0000000000000000000000000000000000000000..86464975d37baf45803f94d402123df0a7c7376e --- /dev/null +++ b/source/Scrolls/SphereType.mmt @@ -0,0 +1,12 @@ +namespace http://mathhub.info/FrameIT/frameworld ⚠+fixmeta ?FrameworldMeta ⚠+ +theory SphereType = + + include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ♠+ include ?FrameITBasics ♠+ + sphereType : type ☠# Sphere ♠+ sphereCons : circle ⟶ point ⟶ Sphere ☠# SphereCons 1 2 ♠+ +⚠\ No newline at end of file