From 5a6b36cc128e8096afe1bff0fee4cd1f8c92b934 Mon Sep 17 00:00:00 2001
From: Paul-Walcher <paulwalcher12@gmail.com>
Date: Sat, 15 Jun 2024 10:19:42 +0200
Subject: [PATCH] added SimpleCircle

---
 source/DefaultSituationSpace.mmt      |  1 +
 source/MetaTheories.mmt               |  1 +
 source/Scrolls/CircleType.mmt         | 12 ++++++++
 source/Scrolls/SimpleCircleScroll.mmt | 40 +++++++++++++++++++++++++++
 source/Scrolls/SphereScroll.mmt       | 36 ++++++++++++++++++++++++
 source/Scrolls/SphereType.mmt         | 12 ++++++++
 6 files changed, 102 insertions(+)
 create mode 100644 source/Scrolls/CircleType.mmt
 create mode 100644 source/Scrolls/SimpleCircleScroll.mmt
 create mode 100644 source/Scrolls/SphereScroll.mmt
 create mode 100644 source/Scrolls/SphereType.mmt

diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt
index cc1468e..88876ef 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 3ae26be..23a77a7 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 0000000..2fda840
--- /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 0000000..c447f0d
--- /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 0000000..9ebdb1d
--- /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 0000000..8646497
--- /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
-- 
GitLab