WN060901 while 'programming' Biegelinie2

-----------------------------------------------------------------------------

# you call a script the first time and get the message

"(*** actual arg(s) missing for '["(#Find, (Funktionen, funs_))"]' i.e. should be 'copy-named' by '*_._'"

!!! THE (#Find, (Funktionen, funs_)) IS NOT COPYNAMED BY funs___ !!!3*_!!!

see biegelinie.sml

-----------------------------------------------------------------------------

# you run a script the first time and get the message

"*** generate1: not impl.for Empty_Tac_"

#1# set trace_script:=true;

!!! the first tactic in a script must be "Take", "Subproblem" (no "init_form")

    OR Rewrite* ("init_form")

-----------------------------------------------------------------------------

# pay attention to ";" between statements within "let":

this script with missing ";" at the last but one line

   "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \

   \ (let b1_ = nth_ 1 rb_;                                         \

   \      fs_ = filter (sameFunId (lhs b1_)) funs_;                 \

   \      (e1_::bool) =                                             \

   \             (SubProblem (Biegelinie_,[makeFunctionTo,equation],\

   \                          [Equation,fromFunction])              \

   \                          [bool_ (hd fs_), bool_ b1_]);         \

   \      b2_ = nth_ 2 rb_;                                         \

   ..."

would lead to

   @@@ next   leaf 'nth_ 2 rb_' ---> Expr 'y L = 0'

   @@@ next   leaf 'filter (sameFunId (lhs b2_)) funs_' ---> Expr '[y x =

    c_4 + c_3 * x +

    1 / (-1 * EI) *

    (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]'

   @@@ next   leaf 'SubProblem

    (Biegelinie_, [makeFunctionTo, equation], [Equation, fromFunction])

    [bool_ (hd fs_), bool_ b2_] b3_ =

   nth_ 3 rb_' ---> Expr 'SubProblem

    (Biegelinie_, [makeFunctionTo, equation], [Equation, fromFunction])

    [bool_

      (y x =

       c_4 + c_3 * x +

       1 / (-1 * EI) *

       (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)),

     bool_ (y L = 0)]

    b3_ =

   (M_b 0 = 0)'

without type errors at 3rd "@@@ next   leaf 'SubProblem...b3_ = ..." !!!

=============================================================================

WN070406 while 'programming' Rechnen

-----------------------------------------------------------------------------

the specification of an example should use Isac.thy !!!

here we had dI'=AlgEin.thy, and norm_Rational stopped, causing nxt = Empty_Tac:

#  rls: norm_Rational on: L = 1 + 2 + 3

##  rls: discard_minus_ on: L = 1 + 2 + 3

###  try thm: real_diff_minus

###  try thm: sym_real_mult_minus1

##  rls: rat_mult_poly on: L = 1 + 2 + 3

###  try thm: rat_mult_poly_l

###  try thm: rat_mult_poly_r

##  rls: make_rat_poly_with_parentheses on: L = 1 + 2 + 3

###  rls: discard_minus_ on: L = 1 + 2 + 3

####  try thm: real_diff_minus

####  try thm: sym_real_mult_minus1

###  rls: expand_poly_rat_ on: L = 1 + 2 + 3

####  try thm: real_plus_binom_pow4_poly

####  try thm: real_plus_binom_pow5_poly

####  try thm: real_plus_binom_pow2_poly

####  try thm: real_plus_binom_pow3_poly

####  try thm: real_plus_minus_binom1_p_p

####  try thm: real_plus_minus_binom2_p_p

####  try thm: real_add_mult_distrib_poly

####  try thm: real_add_mult_distrib2_poly

####  try thm: realpow_multI_poly

####  try thm: realpow_pow

###  try calc: op *'

###  rls: order_mult_rls_ on: L = 1 + 2 + 3

####  rls: order_mult_ on: L = 1 + 2 + 3

#######  rls: e_rls-is_multUnordered on: 1 + 2 + 3 is_multUnordered

########  try calc: Poly.is'_multUnordered'

val f = Form' (FormKF (~1, EdUndef, ...)) : mout

val nxt = ("Empty_Tac", Empty_Tac) : tac'_

-----------------------------------------------------------------------------

the pattern for eval_xxx must include the function-constant of the predicate,

because this is required for rewriting by 'xxx _ = value'

-----------------------------------------------------------------------------