From 1b032d3af8bc823cba4e6508e80431c457df0534 Mon Sep 17 00:00:00 2001
From: Marius Kern <mariusskern@gmail.com>
Date: Thu, 27 Jun 2024 16:41:10 +0200
Subject: [PATCH] Prism added

---
 source/DefaultSituationSpace.mmt |  1 +
 source/MetaTheories.mmt          | 10 ++++++++
 source/Scrolls/PrismScroll.mmt   | 43 ++++++++++++++++++++++++++++++++
 3 files changed, 54 insertions(+)
 create mode 100644 source/Scrolls/PrismScroll.mmt

diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt
index 7be9ac6..3dcc6c0 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 10b4921..038f01f 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 0000000..90ec599
--- /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
-- 
GitLab