Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
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}. " ❙
❚
❚