diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt index 7be9ac6c1131d1814a2c2a54970aae8b88b9980e..3dcc6c0d7a2cd4abaa246ec7fdf7ad0a26a78853 100644 --- a/source/DefaultSituationSpace.mmt +++ b/source/DefaultSituationSpace.mmt @@ -28,6 +28,7 @@ theory DefaultSituationSpace = include ?RectangleScroll ♠include ?CuboidScroll ♠include ?TriangleScroll ♠+ include ?PrismScroll ♠include ?SimpleCircleScroll ♠include ?SphereScroll ♠⚠diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index 10b4921ac62331f69f283eee8ad913a7d1c1a539..038f01f256a2303cacf1474c1aa5d1d098796abb 100644 --- a/source/MetaTheories.mmt +++ b/source/MetaTheories.mmt @@ -318,6 +318,15 @@ theory FrameITCylinder = ⚠+theory PrismType = + include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ♠+ include ☞http://mathhub.info/MitM/core/geometry?Planes ♠+ include ?FrameITBasics ♠+ + prismType : type ☠# Prism ♠+ prismCons : triangle ⟶ point ⟶ Prism ☠# PrismCons 1 2 ♠+⚠+ theory CircleType = include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ♠include ☞http://mathhub.info/MitM/core/geometry?Planes ♠@@ -372,6 +381,7 @@ theory FrameITTheories = include ?FrameITCircle ♠include ?FrameITCone ♠include ?FrameITCylinder ♠+ include ?PrismType ♠include ?CircleType ♠include ?SphereType ♠include ?RectangleType ♠diff --git a/source/Scrolls/PrismScroll.mmt b/source/Scrolls/PrismScroll.mmt new file mode 100644 index 0000000000000000000000000000000000000000..90ec599934e6b0eb2cefd43fae1e912c60321857 --- /dev/null +++ b/source/Scrolls/PrismScroll.mmt @@ -0,0 +1,43 @@ +namespace http://mathhub.info/FrameIT/frameworld ⚠+fixmeta ?FrameworldMeta ⚠+ +theory PrismScroll = + meta ?MetaAnnotations?problemTheory ?PrismScroll/Problem ♠+ meta ?MetaAnnotations?solutionTheory ?PrismScroll/Solution ♠+ + theory Problem = + T: triangle + ☠meta ?MetaAnnotations?label "T" + ☠meta ?MetaAnnotations?description "Triangle" + ♠+ D: point + ☠meta ?MetaAnnotations?label "D" + ☠meta ?MetaAnnotations?description "Point D" + ♠+ dAB: Σ x:℠. ⊦ (d- (triangle_point1 T) D) ≠x + ☠meta ?MetaAnnotations?label s"d${lverb (triangle_point1 T) D}" + ☠meta ?MetaAnnotations?description s"The distance from point ${lverb (triangle_point1 T)} to point ${lverb D}" + ♠+ rDAB: ⊦ (angle_between D (triangle_point1 T) (triangle_point2 T)) ≠90.0 + ☠meta ?MetaAnnotations?label s"r${lverb D}" + ☠meta ?MetaAnnotations?description s"A right angle between ${lverb D,(triangle_point1 T),(triangle_point2 T)}, where ${lverb D} is the point enclosed by ${lverb (triangle_point1 T)} and ${lverb (triangle_point1 T)}" + ♠+ rDAC: ⊦ (angle_between D (triangle_point1 T) (triangle_point3 T)) ≠90.0 + ☠meta ?MetaAnnotations?label s"r${lverb D}" + ☠meta ?MetaAnnotations?description s"A right angle between ${lverb D,(triangle_point1 T),(triangle_point3 T)}, where ${lverb D} is the point enclosed by ${lverb (triangle_point1 T)} and ${lverb (triangle_point3 T)}" + ♠+ ⚠+ + theory Solution = + include ?PrismScroll/Problem ♠+ + meta ?MetaAnnotations?label "Prism" ♠+ meta ?MetaAnnotations?description "Scrolls that takes three points and constructs a Prism." ♠+ + ConstructedPrism : Prism + ☠= (PrismCons T D) + ☠meta ?MetaAnnotations?label "Prism" + ☠meta ?MetaAnnotations?description "The constructed Prism." + ♠+ ⚠+⚠\ No newline at end of file