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
namespace http://mathhub.info/FrameIT/frameworld ❚
import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/core/arithmetics ❚
import rules scala://datatypes.LFX.mmt.kwarc.info ❚
fixmeta ?FrameworldMeta ❚
theory RiverScroll =
meta ?MetaAnnotations?problemTheory ?RiverScroll/Problem ❙
meta ?MetaAnnotations?solutionTheory ?RiverScroll/Solution ❙
include ?IfThenElseX ❙
theory funcs =
get_abs : ℝ ⟶ ℝ ❘ = [val : ℝ] (ℝ) ifx (leq_real_lit 0.0 val) thenx val elsex (minus_real_lit val) ❙
get_height : point ⟶ point ⟶ point ⟶ ℝ ❘ = [g, d, c] get_abs (times_real_lit (plus_real_lit (minus_real_lit (scalar_productI g d)) (scalar_productI g c)) (inv_real_lit (sqrt (scalar_productI g g)))) ❙
get_ground_distance : point ⟶ point ⟶ point ⟶ ℝ ❘ = [g, d, c] sqrt (plus_real_lit (scalar_productI (point_subtractI d c) (point_subtractI d c)) (minus_real_lit (times_real_lit (get_height g d c) (get_height g d c)))) ❙
get_abs_v : ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ⟶ ℝ ❘ = [g, d, h, alpha] ([const : ℝ] sqrt (times_real_lit (times_real_lit const const) (inv_real_lit (times_real_lit (-2.0) (plus_real_lit (times_real_lit const (sin alpha)) (times_real_lit g h)))))) (times_real_lit (times_real_lit d g) (inv_real_lit (cos alpha))) ❙
get_v : point ⟶ point ⟶ ℝ ⟶ point ❘ = [c, a, vabs] ([const : point] vec_multI (times_real_lit vabs (inv_real_lit (sqrt (scalar_productI const const)))) const) (point_subtractI c a) ❙
❚
// start position and velocity ❙
theory Problem =
include ?RiverScroll/funcs ❙
A: point ❘ meta ?MetaAnnotations?label "A" ❙
B: point ❘ meta ?MetaAnnotations?label "B" ❙
C: point ❘ meta ?MetaAnnotations?label "C" ❙
D: point ❘ meta ?MetaAnnotations?label "D" ❙
G: point ❘ meta ?MetaAnnotations?label "G" ❙
angleA : Σ α: ℝ. ⊦ ( ∠ B,A,C ) ≐ α ❘
meta ?MetaAnnotations?label s"∠${lverb B A C}" ❘
meta ?MetaAnnotations?description s"Angle at ${lverb A} as enclosed by legs ${lverb A B} and ${lverb A C}" ❙
❚
// the output of the scroll ❙
theory Solution =
include ?RiverScroll/Problem ❙
v: point ❘ = get_v C A (get_abs_v (minus_real_lit (sqrt (scalar_productI G G))) (get_ground_distance G D C) (get_height G D C) (πl angleA)) ❙
meta ?MetaAnnotations?label "RiverScroll" ❙
meta ?MetaAnnotations?description s"River " ❙
❚
❚