272 Thm ("sym_real_mult_assoc", |
272 Thm ("sym_real_mult_assoc", |
273 num_str (@{thm real_mult_assoc} RS @{thm sym})) |
273 num_str (@{thm real_mult_assoc} RS @{thm sym})) |
274 (*Rls_ discard_parentheses *3**), |
274 (*Rls_ discard_parentheses *3**), |
275 Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*) |
275 Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*) |
276 Rls_ separate_bdv2, |
276 Rls_ separate_bdv2, |
277 Calc ("HOL.divide" ,eval_cancel "#divide_e") |
277 Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e") |
278 ], |
278 ], |
279 scr = EmptyScr}:rls; |
279 scr = EmptyScr}:rls; |
280 *} |
280 *} |
281 ML {* |
281 ML {* |
282 (*.simplify an equational system AFTER solving it; |
282 (*.simplify an equational system AFTER solving it; |
290 rules = [Rls_ norm_Rational, |
290 rules = [Rls_ norm_Rational, |
291 Rls_ (*order_add_mult_in*) norm_System (**1**), |
291 Rls_ (*order_add_mult_in*) norm_System (**1**), |
292 Rls_ discard_parentheses, |
292 Rls_ discard_parentheses, |
293 Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*) |
293 Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*) |
294 Rls_ separate_bdv2, |
294 Rls_ separate_bdv2, |
295 Calc ("HOL.divide" ,eval_cancel "#divide_e") |
295 Calc ("Rings.inverse_class.divide" ,eval_cancel "#divide_e") |
296 ], |
296 ], |
297 scr = EmptyScr}:rls; |
297 scr = EmptyScr}:rls; |
298 (* |
298 (* |
299 val simplify_System = |
299 val simplify_System = |
300 append_rls "simplify_System" simplify_System_parenthesized |
300 append_rls "simplify_System" simplify_System_parenthesized |
360 erls = Rls {id="erls_prls_triangular", preconds = [], |
360 erls = Rls {id="erls_prls_triangular", preconds = [], |
361 rew_ord = ("e_rew_ord", e_rew_ord), |
361 rew_ord = ("e_rew_ord", e_rew_ord), |
362 erls = Erls, srls = Erls, calc = [], |
362 erls = Erls, srls = Erls, calc = [], |
363 rules = [(*for precond NTH_CONS ...*) |
363 rules = [(*for precond NTH_CONS ...*) |
364 Calc ("op <",eval_equ "#less_"), |
364 Calc ("op <",eval_equ "#less_"), |
365 Calc ("op +", eval_binop "#add_") |
365 Calc ("Groups.plus_class.plus", eval_binop "#add_") |
366 (*immediately repeated rewrite pushes |
366 (*immediately repeated rewrite pushes |
367 '+' into precondition !*) |
367 '+' into precondition !*) |
368 ], |
368 ], |
369 scr = EmptyScr}, |
369 scr = EmptyScr}, |
370 srls = Erls, calc = [], |
370 srls = Erls, calc = [], |
371 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}), |
371 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}), |
372 Calc ("op +", eval_binop "#add_"), |
372 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
373 Thm ("NTH_NIL",num_str @{thm NTH_NIL}), |
373 Thm ("NTH_NIL",num_str @{thm NTH_NIL}), |
374 Thm ("tl_Cons",num_str @{thm tl_Cons}), |
374 Thm ("tl_Cons",num_str @{thm tl_Cons}), |
375 Thm ("tl_Nil",num_str @{thm tl_Nil}), |
375 Thm ("tl_Nil",num_str @{thm tl_Nil}), |
376 Calc ("EqSystem.occur'_exactly'_in", |
376 Calc ("EqSystem.occur'_exactly'_in", |
377 eval_occur_exactly_in |
377 eval_occur_exactly_in |
389 erls = Rls {id="erls_prls_triangular4", preconds = [], |
389 erls = Rls {id="erls_prls_triangular4", preconds = [], |
390 rew_ord = ("e_rew_ord", e_rew_ord), |
390 rew_ord = ("e_rew_ord", e_rew_ord), |
391 erls = Erls, srls = Erls, calc = [], |
391 erls = Erls, srls = Erls, calc = [], |
392 rules = [(*for precond NTH_CONS ...*) |
392 rules = [(*for precond NTH_CONS ...*) |
393 Calc ("op <",eval_equ "#less_"), |
393 Calc ("op <",eval_equ "#less_"), |
394 Calc ("op +", eval_binop "#add_") |
394 Calc ("Groups.plus_class.plus", eval_binop "#add_") |
395 (*immediately repeated rewrite pushes |
395 (*immediately repeated rewrite pushes |
396 '+' into precondition !*) |
396 '+' into precondition !*) |
397 ], |
397 ], |
398 scr = EmptyScr}, |
398 scr = EmptyScr}, |
399 srls = Erls, calc = [], |
399 srls = Erls, calc = [], |
400 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}), |
400 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}), |
401 Calc ("op +", eval_binop "#add_"), |
401 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
402 Thm ("NTH_NIL",num_str @{thm NTH_NIL}), |
402 Thm ("NTH_NIL",num_str @{thm NTH_NIL}), |
403 Thm ("tl_Cons",num_str @{thm tl_Cons}), |
403 Thm ("tl_Cons",num_str @{thm tl_Cons}), |
404 Thm ("tl_Nil",num_str @{thm tl_Nil}), |
404 Thm ("tl_Nil",num_str @{thm tl_Nil}), |
405 Calc ("EqSystem.occur'_exactly'_in", |
405 Calc ("EqSystem.occur'_exactly'_in", |
406 eval_occur_exactly_in |
406 eval_occur_exactly_in |
456 ("#Find" ,["solution ss'''"]) |
456 ("#Find" ,["solution ss'''"]) |
457 ], |
457 ], |
458 append_rls "prls_2x2_linear_system" e_rls |
458 append_rls "prls_2x2_linear_system" e_rls |
459 [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}), |
459 [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}), |
460 Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}), |
460 Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}), |
461 Calc ("op +", eval_binop "#add_"), |
461 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
462 Calc ("op =",eval_equal "#equal_") |
462 Calc ("op =",eval_equal "#equal_") |
463 ], |
463 ], |
464 SOME "solveSystem e_s v_s", |
464 SOME "solveSystem e_s v_s", |
465 [])); |
465 [])); |
466 *} |
466 *} |
495 ("#Find" ,["solution ss'''"]) |
495 ("#Find" ,["solution ss'''"]) |
496 ], |
496 ], |
497 append_rls "prls_3x3_linear_system" e_rls |
497 append_rls "prls_3x3_linear_system" e_rls |
498 [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}), |
498 [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}), |
499 Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}), |
499 Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}), |
500 Calc ("op +", eval_binop "#add_"), |
500 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
501 Calc ("op =",eval_equal "#equal_") |
501 Calc ("op =",eval_equal "#equal_") |
502 ], |
502 ], |
503 SOME "solveSystem e_s v_s", |
503 SOME "solveSystem e_s v_s", |
504 [])); |
504 [])); |
505 store_pbt |
505 store_pbt |
511 ("#Find" ,["solution ss'''"]) |
511 ("#Find" ,["solution ss'''"]) |
512 ], |
512 ], |
513 append_rls "prls_4x4_linear_system" e_rls |
513 append_rls "prls_4x4_linear_system" e_rls |
514 [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}), |
514 [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}), |
515 Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}), |
515 Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}), |
516 Calc ("op +", eval_binop "#add_"), |
516 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
517 Calc ("op =",eval_equal "#equal_") |
517 Calc ("op =",eval_equal "#equal_") |
518 ], |
518 ], |
519 SOME "solveSystem e_s v_s", |
519 SOME "solveSystem e_s v_s", |
520 [])); |
520 [])); |
521 *} |
521 *} |
670 rew_ord = ("termlessI",termlessI), |
670 rew_ord = ("termlessI",termlessI), |
671 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls |
671 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls |
672 [(*for asm in NTH_CONS ...*) |
672 [(*for asm in NTH_CONS ...*) |
673 Calc ("op <",eval_equ "#less_"), |
673 Calc ("op <",eval_equ "#less_"), |
674 (*2nd NTH_CONS pushes n+-1 into asms*) |
674 (*2nd NTH_CONS pushes n+-1 into asms*) |
675 Calc("op +", eval_binop "#add_") |
675 Calc("Groups.plus_class.plus", eval_binop "#add_") |
676 ], |
676 ], |
677 srls = Erls, calc = [], |
677 srls = Erls, calc = [], |
678 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}), |
678 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}), |
679 Calc("op +", eval_binop "#add_"), |
679 Calc("Groups.plus_class.plus", eval_binop "#add_"), |
680 Thm ("NTH_NIL",num_str @{thm NTH_NIL})], |
680 Thm ("NTH_NIL",num_str @{thm NTH_NIL})], |
681 scr = EmptyScr}; |
681 scr = EmptyScr}; |
682 store_met |
682 store_met |
683 (prep_met thy "met_eqsys_norm_4x4" [] e_metID |
683 (prep_met thy "met_eqsys_norm_4x4" [] e_metID |
684 (["EqSystem","normalize","4x4"], |
684 (["EqSystem","normalize","4x4"], |