From fa9b94a0b78c2538993b95c4ccdd068864a8e28b Mon Sep 17 00:00:00 2001
From: Paul-Walcher <paulwalcher12@gmail.com>
Date: Tue, 11 Jun 2024 10:19:12 +0200
Subject: [PATCH] Added CuboidType

---
 source/DefaultSituationSpace.mmt   |  1 +
 source/MetaTheories.mmt            |  1 +
 source/Scrolls/CuboidScroll.mmt    | 49 ++++++++++++++++++++++++++++++
 source/Scrolls/CuboidType.mmt      | 12 ++++++++
 source/Scrolls/RectangleScroll.mmt |  2 +-
 source/Scrolls/RectangleType.mmt   |  7 +++++
 6 files changed, 71 insertions(+), 1 deletion(-)
 create mode 100644 source/Scrolls/CuboidScroll.mmt
 create mode 100644 source/Scrolls/CuboidType.mmt

diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt
index 6e811f7..8641166 100644
--- a/source/DefaultSituationSpace.mmt
+++ b/source/DefaultSituationSpace.mmt
@@ -28,6 +28,7 @@ theory DefaultSituationSpace =
         include ?ConeVolumeScroll ❙
         include ?TruncatedConeVolumeScroll ❙
         include ?RectangleScroll ❙
+        include ?CuboidScroll ❙
         
 
 
diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt
index 91c3e43..cadaefc 100644
--- a/source/MetaTheories.mmt
+++ b/source/MetaTheories.mmt
@@ -336,6 +336,7 @@ theory FrameworldMeta =
   include ?MetaAnnotations ❙
   include ?FrameITTheories ❙
   include ?RectangleType ❙
+  include ?CuboidType ❙
 
  // include ☞http://mathhub.info/MitM/core/arithmetics?RealArithmetics ❙
 
diff --git a/source/Scrolls/CuboidScroll.mmt b/source/Scrolls/CuboidScroll.mmt
new file mode 100644
index 0000000..c54adba
--- /dev/null
+++ b/source/Scrolls/CuboidScroll.mmt
@@ -0,0 +1,49 @@
+
+/T Miscellaneous scrolls for playing around/testing that don't have a good home yet  ❚
+
+/T Miscellaneous scrolls for playing around/testing that don't have a good home yet  ❚
+namespace http://mathhub.info/FrameIT/frameworld ❚
+fixmeta ?FrameworldMeta ❚
+
+
+theory CuboidScroll =
+    meta ?MetaAnnotations?problemTheory  ?CuboidScroll/Problem ❙
+    meta ?MetaAnnotations?solutionTheory ?CuboidScroll/Solution ❙
+    theory Problem =
+        R: Rectangle
+         ❘ meta ?MetaAnnotations?label "R"
+         ❘ meta ?MetaAnnotations?description "The given rectangle"
+        ❙
+        T: point
+         ❘ meta ?MetaAnnotations?label "T"
+         ❘ meta ?MetaAnnotations?description "The point above the centerpoint of the rectangle"
+        ❙
+
+        rTBA: ⊦ (∠ T,(R _getB),(R _getA)) ≐ 90.0
+         ❘ meta ?MetaAnnotations?label "rTBA"
+         ❘ meta ?MetaAnnotations?description "A right angle between TBA, where B is the point enclosed by T and A"
+        ❙
+
+        rTBC: ⊦ (∠ T,(R _getB),(R _getC)) ≐ 90.0
+         ❘ meta ?MetaAnnotations?label "rTBC"
+         ❘ meta ?MetaAnnotations?description "A right angle between TBC, where B is the point enclosed by T and C"
+        ❙
+
+
+
+
+    ❙
+        
+    ❚
+    theory Solution =
+        include ?CuboidScroll/Problem ❙
+        meta ?MetaAnnotations?label "Cuboid" ❙
+        meta ?MetaAnnotations?description s"Given a rectangle and a top point that lies above the point in the center of the right-angle formed by the squarepoints
+                                            this scroll constructs a cuboid. Additionally you need a proof that there are two right angles between TBC and TBA" ❙
+        ConstructedCuboid : Cuboid
+                ❘ = CuboidCons R T
+                ❘ meta ?MetaAnnotations?label s"Cuboid"
+                ❘ meta ?MetaAnnotations?description s"The constructed Cuboid."
+        ❙
+    ❚
+❚
\ No newline at end of file
diff --git a/source/Scrolls/CuboidType.mmt b/source/Scrolls/CuboidType.mmt
new file mode 100644
index 0000000..eec43f5
--- /dev/null
+++ b/source/Scrolls/CuboidType.mmt
@@ -0,0 +1,12 @@
+namespace http://mathhub.info/FrameIT/frameworld ❚
+fixmeta ur:?LF ❚
+
+theory CuboidType =
+  
+  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  include ?FrameITBasics ❙
+
+  cuboidType : type ❘ # Cuboid ❙
+  cuboidCons : Rectangle ⟶ point  ⟶ Cuboid  ❘ # CuboidCons 1 2 ❙
+  
+❚
\ No newline at end of file
diff --git a/source/Scrolls/RectangleScroll.mmt b/source/Scrolls/RectangleScroll.mmt
index 6cd41ff..06e2ce1 100644
--- a/source/Scrolls/RectangleScroll.mmt
+++ b/source/Scrolls/RectangleScroll.mmt
@@ -23,7 +23,7 @@ theory RectangleScroll =
          ❘ meta ?MetaAnnotations?description "The third point"
         ❙
 
-        rC: ⊦ (∠ A,B,C) ≐ 90.0
+        rABC: ⊦ (∠ A,B,C) ≐ 90.0
          ❘ meta ?MetaAnnotations?label "rC"
          ❘ meta ?MetaAnnotations?description "A right angle between ABC, where B is the point enclosed by A and B"
         ❙
diff --git a/source/Scrolls/RectangleType.mmt b/source/Scrolls/RectangleType.mmt
index becda19..cf15cc6 100644
--- a/source/Scrolls/RectangleType.mmt
+++ b/source/Scrolls/RectangleType.mmt
@@ -9,4 +9,11 @@ theory RectangleType =
   rectangleType : type ❘ # Rectangle ❙
   rectangleCons : point ⟶ point ⟶ point  ⟶ Rectangle  ❘ # RectangleCons 1 2 3 ❙
   
+  getA : Rectangle ⟶ point ❘ # 1 _getA ❙
+  getB : Rectangle ⟶ point ❘ # 1 _getB ❙
+  getC : Rectangle ⟶ point ❘ # 1 _getC ❙
+
+  axiomgetA : {R: Rectangle} ⊦ (RectangleCons A B C) ≐ A ❙
+  axiomgetB : {R: Rectangle} ⊦ (RectangleCons A B C) ≐ B ❙
+  axiomgetC : {R: Rectangle} ⊦ (RectangleCons A B C) ≐ C ❙
 ❚
\ No newline at end of file
-- 
GitLab