Skip to content
Snippets Groups Projects
Commit 365d5258 authored by ComFreek's avatar ComFreek
Browse files

clean up scrolls mmt code

parent 4db27773
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
source/Scrolls/CircleScroll.mmt
+ 47
− 126
View file @ 365d5258
namespace http://mathhub.info/FrameIT/frameworld ❚ namespace http://mathhub.info/FrameIT/frameworld ❚
fixmeta ?FrameworldMeta ❚ fixmeta ?FrameworldMeta ❚
/T This scrolls infers a 2D circle from three dedicated 3D points (the circle's supposed center,
/T one of the supposed circle itself, one in the plane the circle should lie in).
This scrolls calculates a circle based on three points special pooints.
The arguments required:
M - The center of the circle
A - A point on the edge of the circle
B - A point on the plane that the circle is supposed to lie in.
This Scrolls returns:
deduceC - The actual cirlce as a fact
deduceR - The radius of the circle as RadiusFact
deduceR2 - The radius of the circle as DistanceFact
midOnCircle - a proof that M is on the circle
edgeOnCircle - a proof that A is on the circle
❚ ❚
theory CircleScroll = theory CircleScroll =
meta ?MetaAnnotations?problemTheory ?CircleScroll/Problem ❙ meta ?MetaAnnotations?problemTheory ?CircleScroll/Problem ❙
meta ?MetaAnnotations?solutionTheory ?CircleScroll/Solution ❙ meta ?MetaAnnotations?solutionTheory ?CircleScroll/Solution ❙
// the three special points M, A and B ❙ // the three special points M, A and B ❙
theory Problem = theory Problem =
M : point ❘ meta ?MetaAnnotations?label "M" ❙ M : point ❘ meta ?MetaAnnotations?label "M"
A : point ❘ meta ?MetaAnnotations?label "A" ❙ ❘ meta ?MetaAnnotations?description "The circle's center" ❙
B : point ❘ meta ?MetaAnnotations?label "B" ❙ 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." ❙
❚ ❚
// the output of the scroll ❙
theory Solution = theory Solution =
include ?CircleScroll/Problem ❙ include ?CircleScroll/Problem ❙
deduceC: circle
deduceC ❘ = ( pointsToC M A B )
: circle ❘ ❘ meta ?MetaAnnotations?label s"○${lverb M}"
= ( pointsToC M A B ) ❘ ❘ meta ?MetaAnnotations?description "Circle"
meta ?MetaAnnotations?label s"○${lverb M}" ❘
meta ?MetaAnnotations?description "Circle"
❙ ❙
deduceR : Σ x:ℝ . ⊦ ( circleRadius deduceC) ≐ x ❘ deduceR: Σ x:ℝ . ⊦ ( circleRadius deduceC) ≐ x
= ⟨ d- M A , sketch "deduce Radius"⟩ ❘ ❘ = ⟨ d- M A , sketch "deduce Radius"⟩
meta ?MetaAnnotations?label s"r${lverb deduceC}" ❘ ❘ meta ?MetaAnnotations?label s"r${lverb deduceC}"
meta ?MetaAnnotations?description "radius of C" ❘ meta ?MetaAnnotations?description s"radius of ${lverb deduceC} (radius fact)"
❙ ❙
deduceR2 : Σ x:ℝ . ⊦ ( d- A M ) ≐ x ❘ deduceR2: Σ x:ℝ . ⊦ ( d- A M ) ≐ x
= ⟨ d- A M , sketch "deduce Radius2"⟩ ❘ ❘ = ⟨ d- A M , sketch "deduce Radius2"⟩
meta ?MetaAnnotations?label s"${lverb A M}" ❘ ❘ meta ?MetaAnnotations?label s"${lverb A M}"
meta ?MetaAnnotations?description "radius of C" ❘ meta ?MetaAnnotations?description s"radius of ${lverb deduceC} (distance fact)"
❙ ❙
midOnCircle: ⊦ M VonC deduceC
midOnCircle : ⊦ M VonC deduceC ❘ ❘ = midOnC deduceC M
= midOnC deduceC M ❘ ❘ meta ?MetaAnnotations?label s"${lverb M}∈${lverb deduceC}"
meta ?MetaAnnotations?label s"${lverb M}∈${lverb deduceC}" ❘ ❘ meta ?MetaAnnotations?description s"proof of M being on the circle ${lverb deduceC}"
meta ?MetaAnnotations?description "proof of M being on the circle"
❙ ❙
edgeOnCircle: ⊦ A VonC deduceC
edgeOnCircle : ⊦ A VonC deduceC ❘ ❘ meta ?MetaAnnotations?label s"${lverb A}∈${lverb deduceC}"
meta ?MetaAnnotations?label s"${lverb A}∈${lverb deduceC}" ❘ ❘ meta ?MetaAnnotations?description s"proof of A being on the circle ${lverb deduceC}"
meta ?MetaAnnotations?description "proof of A being on the circle" ❙
❙
// the description verbalizes CircleCircumference, hence must come after its declaration ❙ // the description verbalizes CircleCircumference, hence must come after its declaration ❙
meta ?MetaAnnotations?label "CircleScroll" ❙ 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}. " ❙ 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}. " ❙
❚ ❚
❚ ❚
/T
This scrolls calculates the area of a given circle based on the circle and its radius circle:
The arguments required:
C - The circle
radiusC - The actual radius of the circle
This Scrolls returns:
deduceArea - The area of the circle
❚
theory CircleAreaScroll = theory CircleAreaScroll =
meta ?MetaAnnotations?problemTheory ?CircleAreaScroll/Problem ❙ meta ?MetaAnnotations?problemTheory ?CircleAreaScroll/Problem ❙
meta ?MetaAnnotations?solutionTheory ?CircleAreaScroll/Solution ❙ meta ?MetaAnnotations?solutionTheory ?CircleAreaScroll/Solution ❙
theory Problem = theory Problem =
cir : circle ❘ meta ?MetaAnnotations?label "○C" ❙ cir: circle
❘ meta ?MetaAnnotations?label "○C"
radiusC : Σ x:ℝ . ⊦ radius cir ≐ x ❘ ❘ meta ?MetaAnnotations?description s"the circle"
meta ?MetaAnnotations?label "r" ❘
meta ?MetaAnnotations?description s"Radius of the circle ${lverb cir}"
❙ ❙
/T todo: why can't we compute the radius directly from cir? ❙
radiusC: Σ x:ℝ . ⊦ radius cir ≐ x
❘ meta ?MetaAnnotations?label "r"
❘ meta ?MetaAnnotations?description s"radius of the circle ${lverb cir}"
❙
❚ ❚
theory Solution = theory Solution =
include ?CircleAreaScroll/Problem ❙ include ?CircleAreaScroll/Problem ❙
deduceArea deduceArea: Σ x:ℝ . ⊦ areaCirc cir ≐ x
: Σ x:ℝ . ⊦ areaCirc cir ≐ x ❘ ❘ = ⟨ ( (πl radiusC) ⋅ ( πl radiusC) ) ⋅ pi_num , sketch "CircleArea Scroll"⟩
= ⟨ ( (πl radiusC) ⋅ ( πl radiusC) ) ⋅ pi_num , sketch "CircleArea Scroll"⟩ ❘ ❘ meta ?MetaAnnotations?label s"A(${lverb cir})"
meta ?MetaAnnotations?label s"A(${lverb cir})" ❘ ❘ meta ?MetaAnnotations?description s"The area of the circle ${lverb cir}"
meta ?MetaAnnotations?description s"The area of the circle ${lverb cir}" ❙
❙
meta ?MetaAnnotations?label "CircleAreaScroll" ❙ meta ?MetaAnnotations?label "CircleAreaScroll" ❙
meta ?MetaAnnotations?description s" This scroll is calculating the area of the circle ${lverb cir} via the formula A = ${lverb radiusC}⋅ ${lverb radiusC}⋅ pi" ❙ meta ?MetaAnnotations?description s" This scroll is calculating the area of the circle ${lverb cir} via the formula A = ${lverb radiusC}⋅ ${lverb radiusC}⋅ pi" ❙
❚ ❚
❚ ❚
source/Scrolls/ConeVolumeScroll.mmt
+ 0
− 4
View file @ 365d5258
...@@ -2,10 +2,6 @@ namespace http://mathhub.info/FrameIT/frameworld ❚ ...@@ -2,10 +2,6 @@ namespace http://mathhub.info/FrameIT/frameworld ❚
fixmeta ?FrameworldMeta ❚ fixmeta ?FrameworldMeta ❚
/T /T
This scrolls calculates the volume of a cone with a circle as base. This scrolls calculates the volume of a cone with a circle as base.
......
source/Scrolls/CylinderScroll.mmt deleted 100644 → 0
+ 0
− 8
View file @ 4db27773
namespace http://mathhub.info/FrameIT/frameworld ❚
fixmeta ?FrameworldMeta ❚
source/Scrolls/InterceptTheorem.mmt
+ 1
− 3
View file @ 365d5258
...@@ -16,10 +16,8 @@ fixmeta ?FrameworldMeta ❚ ...@@ -16,10 +16,8 @@ fixmeta ?FrameworldMeta ❚
The scroll encodes the InterceptTheorem The scroll encodes the InterceptTheorem
❚ ❚
theory InterceptTheorem = theory InterceptTheorem =
meta ?MetaAnnotations?problemTheory ?InterceptTheorem/Problem ❙ meta ?MetaAnnotations?problemTheory ?InterceptTheorem/Problem ❙
meta ?MetaAnnotations?solutionTheory ?InterceptTheorem/Solution ❙ meta ?MetaAnnotations?solutionTheory ?InterceptTheorem/Solution ❙
theory Problem = theory Problem =
......
source/Scrolls/MiscScrolls.mmt
+ 12
− 15
View file @ 365d5258
...@@ -4,20 +4,18 @@ namespace http://mathhub.info/FrameIT/frameworld ❚ ...@@ -4,20 +4,18 @@ namespace http://mathhub.info/FrameIT/frameworld ❚
fixmeta ?FrameworldMeta ❚ fixmeta ?FrameworldMeta ❚
theory Midpoint = theory Midpoint =
meta ?MetaAnnotations?problemTheory ?Midpoint/Problem ❙ meta ?MetaAnnotations?problemTheory ?Midpoint/Problem ❙
meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution ❙ meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution ❙
theory Problem = theory Problem =
P P: point
: point ❘ ❘ meta ?MetaAnnotations?label "P"
meta ?MetaAnnotations?label "P" ❘ ❘ meta ?MetaAnnotations?description "Some arbitrary input point"
meta ?MetaAnnotations?description "Some arbitrary input point"
❙ ❙
Q Q: point
: point ❘ ❘ meta ?MetaAnnotations?label "Q"
meta ?MetaAnnotations?label "Q" ❘ ❘ meta ?MetaAnnotations?description "Some other arbitrary input point"
meta ?MetaAnnotations?description "Some other arbitrary input point"
❙ ❙
❚ ❚
...@@ -27,11 +25,10 @@ theory Midpoint = ...@@ -27,11 +25,10 @@ theory Midpoint =
meta ?MetaAnnotations?label "MidPoint" ❙ meta ?MetaAnnotations?label "MidPoint" ❙
meta ?MetaAnnotations?description s"Our MidPoint scroll that given two points ${lverb P} and ${lverb Q} computes the midpoint of the line ${lverb P Q}." ❙ meta ?MetaAnnotations?description s"Our MidPoint scroll that given two points ${lverb P} and ${lverb Q} computes the midpoint of the line ${lverb P Q}." ❙
midpoint midpoint: point
: point ❘ ❘ = ⟨0.5 ⋅ (P _x + Q _x), 0.5 ⋅ (P _y + Q _y), 0.5 ⋅ (P _z + Q _z)⟩
= ⟨0.5 ⋅ (P _x + Q _x), 0.5 ⋅ (P _y + Q _y), 0.5 ⋅ (P _z + Q _z)⟩ ❘ ❘ meta ?MetaAnnotations?label s"Mid[${lverb P Q}]"
meta ?MetaAnnotations?label s"Mid[${lverb P Q}]" ❘ ❘ meta ?MetaAnnotations?description s"The midpoint between points ${lverb P} and ${lverb Q}."
meta ?MetaAnnotations?description s"The midpoint between points ${lverb P} and ${lverb Q}."
❙ ❙
❚ ❚
❚ ❚
\ No newline at end of file
source/Scrolls/ParallelLines.mmt
+ 1
− 5
View file @ 365d5258
...@@ -23,14 +23,10 @@ A ------B ...@@ -23,14 +23,10 @@ A ------B
The scroll encodes the InterceptTheorem . The scroll encodes the InterceptTheorem .
❚ ❚
theory ParallelLines = theory ParallelLines =
meta ?MetaAnnotations?problemTheory ?ParallelLines/Problem ❙ meta ?MetaAnnotations?problemTheory ?ParallelLines/Problem ❙
meta ?MetaAnnotations?solutionTheory ?ParallelLines/Solution ❙ meta ?MetaAnnotations?solutionTheory ?ParallelLines/Solution ❙
theory Problem = theory Problem =
A: point ❘ meta ?MetaAnnotations?label "A" ❙ A: point ❘ meta ?MetaAnnotations?label "A" ❙
B: point ❘ meta ?MetaAnnotations?label "B" ❙ B: point ❘ meta ?MetaAnnotations?label "B" ❙
......
source/Scrolls/TriangleScrolls.mmt
+ 4
− 6
View file @ 365d5258
...@@ -25,8 +25,7 @@ theory TriangleProblem = ...@@ -25,8 +25,7 @@ theory TriangleProblem =
theory TriangleProblem_RightAngleAtC = theory TriangleProblem_RightAngleAtC =
include ?TriangleProblem ❙ include ?TriangleProblem ❙
rightAngleC rightAngleC
// : ⊦ ( ∠ B,C,A ) ≐ 90.0 ❘ : ⊦ ( ∠r B C A ) ≐ 90.0 ❘
: ⊦ ( ∠r B C A ) ❘
meta ?MetaAnnotations?label s"⊾${lverb C}" ❘ meta ?MetaAnnotations?label s"⊾${lverb C}" ❘
meta ?MetaAnnotations?description s"${lverb A C} ⟂ ${lverb B C}: right angle at ${lverb C} as enclosed by legs ${lverb A C} and ${lverb B C}." meta ?MetaAnnotations?description s"${lverb A C} ⟂ ${lverb B C}: right angle at ${lverb C} as enclosed by legs ${lverb A C} and ${lverb B C}."
❙ ❙
...@@ -51,7 +50,7 @@ theory TriangleProblem_AngleAtB = ...@@ -51,7 +50,7 @@ theory TriangleProblem_AngleAtB =
❚ ❚
theory AngleSum = theory AngleSum =
meta ?MetaAnnotations?problemTheory ?AngleSum/Problem ❙ meta ?MetaAnnotations?problemTheory ?AngleSum/Problem ❙
meta ?MetaAnnotations?solutionTheory ?AngleSum/Solution ❙ meta ?MetaAnnotations?solutionTheory ?AngleSum/Solution ❙
theory Problem = theory Problem =
...@@ -77,7 +76,7 @@ theory AngleSum = ...@@ -77,7 +76,7 @@ theory AngleSum =
❚ ❚
theory OppositeLen = theory OppositeLen =
meta ?MetaAnnotations?problemTheory ?OppositeLen/Problem ❙ meta ?MetaAnnotations?problemTheory ?OppositeLen/Problem ❙
meta ?MetaAnnotations?solutionTheory ?OppositeLen/Solution ❙ meta ?MetaAnnotations?solutionTheory ?OppositeLen/Solution ❙
theory Problem = theory Problem =
...@@ -109,11 +108,10 @@ theory OppositeLen = ...@@ -109,11 +108,10 @@ theory OppositeLen =
❚ ❚
theory Pythagoras = theory Pythagoras =
meta ?MetaAnnotations?problemTheory ?Pythagoras/Problem ❙ meta ?MetaAnnotations?problemTheory ?Pythagoras/Problem ❙
meta ?MetaAnnotations?solutionTheory ?Pythagoras/Solution ❙ meta ?MetaAnnotations?solutionTheory ?Pythagoras/Solution ❙
theory Problem = theory Problem =
// include ?TriangleScroll_RightAngledProblem ❙
include ?TriangleProblem_RightAngleAtC ❙ include ?TriangleProblem_RightAngleAtC ❙
distanceAC distanceAC
: Σ x:ℝ. ⊦ (d- A C) ≐ x ❘ : Σ x:ℝ. ⊦ (d- A C) ≐ x ❘
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment