diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt index 864116653796a48bf83baf65987719c7fe8e2a37..cc1468e7a3b6768efb32d05cc33f319f7b681bc5 100644 --- a/source/DefaultSituationSpace.mmt +++ b/source/DefaultSituationSpace.mmt @@ -7,8 +7,8 @@ theory DefaultSituationSpace = include ?SupplementaryAngles ♠include ?OppositeLen ♠include ?AngleSum ♠- // include ?ParallelLines ♠- // include ?InterceptTheorem ♠+ // include ?ParallelLines ♠+ // include ?InterceptTheorem ♠include ?Pythagoras♠include ?CylinderVolumeScroll♠include ?CircleLineAngleToAngleScroll♠@@ -17,18 +17,18 @@ theory DefaultSituationSpace = include ?Test ♠include ?CircleScroll ♠- include ?MuchBetterCircleScroll ♠include ?BouncingScroll ♠include ?WBouncingScroll ♠include ?W3DBouncingScroll ♠include ?T3DBouncingScroll ♠- // include ?SinOppositeLeg ♠+ // include ?SinOppositeLeg ♠include ?CircleLineAngleScroll ♠include ?CircleAreaScroll ♠include ?ConeVolumeScroll ♠include ?TruncatedConeVolumeScroll ♠include ?RectangleScroll ♠include ?CuboidScroll ♠+ include ?TriangleScroll ♠diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index cadaefccdcec5a30bffbe0fc8cac11ef685b8da1..3ae26be43561448283f2f3df4eaa7d2381a01254 100644 --- a/source/MetaTheories.mmt +++ b/source/MetaTheories.mmt @@ -337,6 +337,7 @@ theory FrameworldMeta = include ?FrameITTheories ♠include ?RectangleType ♠include ?CuboidType ♠+ include ?TriangleType ♠// include ☞http://mathhub.info/MitM/core/arithmetics?RealArithmetics ♠diff --git a/source/Scrolls/MuchBetterCircleScroll.mmt b/source/Scrolls/MuchBetterCircleScroll.mmt deleted file mode 100644 index 5cef9d7644786d471cdf62d1e198c6ba829e9f09..0000000000000000000000000000000000000000 --- a/source/Scrolls/MuchBetterCircleScroll.mmt +++ /dev/null @@ -1,61 +0,0 @@ -namespace http://mathhub.info/FrameIT/frameworld ⚠-fixmeta ?FrameworldMeta ⚠- -/T This scrolls infers a 2D circle from three dedicated 3D points (the circle's supposed center, - one of the supposed circle itself, one in the plane the circle should lie in). -⚠-theory MuchBetterCircleScroll = - meta ?MetaAnnotations?problemTheory ?MuchBetterCircleScroll/Problem ♠- meta ?MetaAnnotations?solutionTheory ?MuchBetterCircleScroll/Solution ♠- - // the three special points M, A and B ♠- theory Problem = - M : point ☠meta ?MetaAnnotations?label "M" - ☠meta ?MetaAnnotations?description "The circle's center" ♠- A : point ☠meta ?MetaAnnotations?label "A" - ☠meta ?MetaAnnotations?description "A point on the circle" ♠- B : point ☠meta ?MetaAnnotations?label "B" - ☠meta ?MetaAnnotations?description "A point within the plane the circle should lie in." ♠- radiusC: Σ x:℠. ⊦ (d- M A ≠x) ∨ (d- A M) - ☠meta ?MetaAnnotations?label "r" - ☠meta ?MetaAnnotations?description s"radius of the circle ${lverb cir}" - ♠- ⚠- - theory Solution = - include ?MuchBetterCircleScroll/Problem ♠- - deduceC: circle - ☠= ( pointsToC M A B ) - ☠meta ?MetaAnnotations?label s"○${lverb M}" - ☠meta ?MetaAnnotations?description "Circle" - ♠- - deduceR: Σ x:℠. ⊦ ( circleRadius deduceC) ≠x - ☠= ⟨ d- M A , sketch "deduce Radius"⟩ - ☠meta ?MetaAnnotations?label s"r${lverb deduceC}" - ☠meta ?MetaAnnotations?description s"radius of ${lverb deduceC} (radius fact)" b - ♠- - deduceR2: Σ x:℠. ⊦ ( d- A M ) ≠x - ☠= ⟨ d- A M , sketch "deduce Radius2"⟩ - ☠meta ?MetaAnnotations?label s"${lverb A M}" - ☠meta ?MetaAnnotations?description s"radius of ${lverb deduceC} (distance fact)" - ♠- - midOnCircle: ⊦ M VonC deduceC - ☠= midOnC deduceC M - ☠meta ?MetaAnnotations?label s"${lverb M}∈${lverb deduceC}" - ☠meta ?MetaAnnotations?description s"proof of M being on the circle ${lverb deduceC}" - ♠- - edgeOnCircle: ⊦ A VonC deduceC - ☠meta ?MetaAnnotations?label s"${lverb A}∈${lverb deduceC}" - ☠meta ?MetaAnnotations?description s"proof of A being on the circle ${lverb deduceC}" - ♠- - // the description verbalizes CircleCircumference, hence must come after its declaration ♠- meta ?MetaAnnotations?label "CircleScroll" ♠- meta ?MetaAnnotations?description s"Calculating a circle defined by the middle ${lverb M}, an edge point ${lverb A} and a point on the circle plane ${lverb B}. " ♠- ⚠-⚠\ No newline at end of file diff --git a/source/Scrolls/TriangleScroll.mmt b/source/Scrolls/TriangleScroll.mmt new file mode 100644 index 0000000000000000000000000000000000000000..913f431cab0d9de567dc0a2d493454a5feb91d96 --- /dev/null +++ b/source/Scrolls/TriangleScroll.mmt @@ -0,0 +1,35 @@ +namespace http://mathhub.info/FrameIT/frameworld ⚠+fixmeta ?FrameworldMeta ⚠+ +theory TriangleScroll = + meta ?MetaAnnotations?problemTheory ?TriangleScroll/Problem ♠+ meta ?MetaAnnotations?solutionTheory ?TriangleScroll/Solution ♠+ + theory Problem = + A: point + ☠meta ?MetaAnnotations?label "A" + ☠meta ?MetaAnnotations?description "The first point" + ♠+ B: point + ☠meta ?MetaAnnotations?label "B" + ☠meta ?MetaAnnotations?description "The second point" + ♠+ C: point + ☠meta ?MetaAnnotations?label "C" + ☠meta ?MetaAnnotations?description "The third point" + ♠+ ⚠+ + theory Solution = + include ?TriangleScroll/Problem ♠+ + meta ?MetaAnnotations?label "Triangle" ♠+ meta ?MetaAnnotations?description s"Scrolls that takes three points and constructs a triangle." ♠+ + ConstructedTriangle : Triangle + ☠= TriangleCons A B C + ☠meta ?MetaAnnotations?label s"Triangle" + ☠meta ?MetaAnnotations?description s"The constructed Triangle." + ♠+ ⚠+⚠\ No newline at end of file diff --git a/source/Scrolls/TriangleType.mmt b/source/Scrolls/TriangleType.mmt new file mode 100644 index 0000000000000000000000000000000000000000..da5f198502f2b3781e28c433a85190dd5bdfa169 --- /dev/null +++ b/source/Scrolls/TriangleType.mmt @@ -0,0 +1,10 @@ +namespace http://mathhub.info/FrameIT/frameworld ⚠+fixmeta ur:?LF ⚠+ +theory TriangleType = + include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ♠+ include ?FrameITBasics ♠+ + triangleType : type ☠# Triangle ♠+ triangleCons : point ⟶ point ⟶ point ⟶ Triangle ☠# TriangleCons 1 2 3 ♠+⚠\ No newline at end of file