diff --git a/source/Scrolls/RiverScroll.mmt b/source/Scrolls/RiverScroll.mmt new file mode 100644 index 0000000000000000000000000000000000000000..ecbd6870b6658cc3cd057dc21998fc2b09370d16 --- /dev/null +++ b/source/Scrolls/RiverScroll.mmt @@ -0,0 +1,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 " â™ + âš +âš \ No newline at end of file