1432 ("make_rat_poly_with_parentheses", |
1432 ("make_rat_poly_with_parentheses", |
1433 (Context.theory_name @{theory}, prep_rls' make_rat_poly_with_parentheses))]\<close> |
1433 (Context.theory_name @{theory}, prep_rls' make_rat_poly_with_parentheses))]\<close> |
1434 |
1434 |
1435 subsection \<open>problems\<close> |
1435 subsection \<open>problems\<close> |
1436 setup \<open>KEStore_Elems.add_pbts |
1436 setup \<open>KEStore_Elems.add_pbts |
1437 [(Specify.prep_pbt thy "pbl_simp_poly" [] Celem.e_pblID |
1437 [(Specify.prep_pbt thy "pbl_simp_poly" [] Spec.e_pblID |
1438 (["polynomial","simplification"], |
1438 (["polynomial","simplification"], |
1439 [("#Given" ,["Term t_t"]), |
1439 [("#Given" ,["Term t_t"]), |
1440 ("#Where" ,["t_t is_polyexp"]), |
1440 ("#Where" ,["t_t is_polyexp"]), |
1441 ("#Find" ,["normalform n_n"])], |
1441 ("#Find" ,["normalform n_n"])], |
1442 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*) |
1442 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*) |
1448 |
1448 |
1449 partial_function (tailrec) simplify :: "real \<Rightarrow> real" |
1449 partial_function (tailrec) simplify :: "real \<Rightarrow> real" |
1450 where |
1450 where |
1451 "simplify term = ((Rewrite_Set ''norm_Poly'') term)" |
1451 "simplify term = ((Rewrite_Set ''norm_Poly'') term)" |
1452 setup \<open>KEStore_Elems.add_mets |
1452 setup \<open>KEStore_Elems.add_mets |
1453 [Specify.prep_met thy "met_simp_poly" [] Celem.e_metID |
1453 [Specify.prep_met thy "met_simp_poly" [] Spec.e_metID |
1454 (["simplification","for_polynomials"], |
1454 (["simplification","for_polynomials"], |
1455 [("#Given" ,["Term t_t"]), |
1455 [("#Given" ,["Term t_t"]), |
1456 ("#Where" ,["t_t is_polyexp"]), |
1456 ("#Where" ,["t_t is_polyexp"]), |
1457 ("#Find" ,["normalform n_n"])], |
1457 ("#Find" ,["normalform n_n"])], |
1458 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, |
1458 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, |