equal
deleted
inserted
replaced
473 |
473 |
474 partial_function (tailrec) simplify :: "real \<Rightarrow> real" |
474 partial_function (tailrec) simplify :: "real \<Rightarrow> real" |
475 where |
475 where |
476 "simplify t_t = ( |
476 "simplify t_t = ( |
477 (Repeat( |
477 (Repeat( |
478 (Try (Rewrite_Set ''ordne_alphabetisch'')) @@ |
478 (Try (Rewrite_Set ''ordne_alphabetisch'')) #> |
479 (Try (Rewrite_Set ''fasse_zusammen'')) @@ |
479 (Try (Rewrite_Set ''fasse_zusammen'')) #> |
480 (Try (Rewrite_Set ''verschoenere''))) |
480 (Try (Rewrite_Set ''verschoenere''))) |
481 ) t_t)" |
481 ) t_t)" |
482 setup \<open>KEStore_Elems.add_mets |
482 setup \<open>KEStore_Elems.add_mets |
483 [Specify.prep_met thy "met_simp_poly_minus" [] Celem.e_metID |
483 [Specify.prep_met thy "met_simp_poly_minus" [] Celem.e_metID |
484 (["simplification","for_polynomials","with_minus"], |
484 (["simplification","for_polynomials","with_minus"], |
507 |
507 |
508 partial_function (tailrec) simplify2 :: "real \<Rightarrow> real" |
508 partial_function (tailrec) simplify2 :: "real \<Rightarrow> real" |
509 where |
509 where |
510 "simplify2 t_t = ( |
510 "simplify2 t_t = ( |
511 (Repeat( |
511 (Repeat( |
512 (Try (Rewrite_Set ''klammern_aufloesen'')) @@ |
512 (Try (Rewrite_Set ''klammern_aufloesen'')) #> |
513 (Try (Rewrite_Set ''ordne_alphabetisch'')) @@ |
513 (Try (Rewrite_Set ''ordne_alphabetisch'')) #> |
514 (Try (Rewrite_Set ''fasse_zusammen'')) @@ |
514 (Try (Rewrite_Set ''fasse_zusammen'')) #> |
515 (Try (Rewrite_Set ''verschoenere''))) |
515 (Try (Rewrite_Set ''verschoenere''))) |
516 ) t_t)" |
516 ) t_t)" |
517 setup \<open>KEStore_Elems.add_mets |
517 setup \<open>KEStore_Elems.add_mets |
518 [Specify.prep_met thy "met_simp_poly_parenth" [] Celem.e_metID |
518 [Specify.prep_met thy "met_simp_poly_parenth" [] Celem.e_metID |
519 (["simplification","for_polynomials","with_parentheses"], |
519 (["simplification","for_polynomials","with_parentheses"], |
529 |
529 |
530 partial_function (tailrec) simplify3 :: "real \<Rightarrow> real" |
530 partial_function (tailrec) simplify3 :: "real \<Rightarrow> real" |
531 where |
531 where |
532 "simplify3 t_t = ( |
532 "simplify3 t_t = ( |
533 (Repeat( |
533 (Repeat( |
534 (Try (Rewrite_Set ''klammern_ausmultiplizieren'')) @@ |
534 (Try (Rewrite_Set ''klammern_ausmultiplizieren'')) #> |
535 (Try (Rewrite_Set ''discard_parentheses'')) @@ |
535 (Try (Rewrite_Set ''discard_parentheses'')) #> |
536 (Try (Rewrite_Set ''ordne_monome'')) @@ |
536 (Try (Rewrite_Set ''ordne_monome'')) #> |
537 (Try (Rewrite_Set ''klammern_aufloesen'')) @@ |
537 (Try (Rewrite_Set ''klammern_aufloesen'')) #> |
538 (Try (Rewrite_Set ''ordne_alphabetisch'')) @@ |
538 (Try (Rewrite_Set ''ordne_alphabetisch'')) #> |
539 (Try (Rewrite_Set ''fasse_zusammen'')) @@ |
539 (Try (Rewrite_Set ''fasse_zusammen'')) #> |
540 (Try (Rewrite_Set ''verschoenere''))) |
540 (Try (Rewrite_Set ''verschoenere''))) |
541 ) t_t)" |
541 ) t_t)" |
542 setup \<open>KEStore_Elems.add_mets |
542 setup \<open>KEStore_Elems.add_mets |
543 [Specify.prep_met thy "met_simp_poly_parenth_mult" [] Celem.e_metID |
543 [Specify.prep_met thy "met_simp_poly_parenth_mult" [] Celem.e_metID |
544 (["simplification","for_polynomials","with_parentheses_mult"], |
544 (["simplification","for_polynomials","with_parentheses_mult"], |
563 let |
563 let |
564 e_e = Take e_e; |
564 e_e = Take e_e; |
565 e_e = Substitute w_w e_e |
565 e_e = Substitute w_w e_e |
566 in ( |
566 in ( |
567 Repeat ( |
567 Repeat ( |
568 (Try (Repeat (Calculate ''TIMES''))) @@ |
568 (Try (Repeat (Calculate ''TIMES''))) #> |
569 (Try (Repeat (Calculate ''PLUS'' ))) @@ |
569 (Try (Repeat (Calculate ''PLUS'' ))) #> |
570 (Try (Repeat (Calculate ''MINUS'')))) |
570 (Try (Repeat (Calculate ''MINUS'')))) |
571 ) e_e)" |
571 ) e_e)" |
572 setup \<open>KEStore_Elems.add_mets |
572 setup \<open>KEStore_Elems.add_mets |
573 [Specify.prep_met thy "met_probe_poly" [] Celem.e_metID |
573 [Specify.prep_met thy "met_probe_poly" [] Celem.e_metID |
574 (["probe","fuer_polynom"], |
574 (["probe","fuer_polynom"], |