107 ML \<open> |
107 ML \<open> |
108 val ansatz_rls = prep_rls'( |
108 val ansatz_rls = prep_rls'( |
109 Rule_Def.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
109 Rule_Def.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
110 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
110 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
111 rules = |
111 rules = |
112 [Rule.Thm ("ansatz_2nd_order",TermC.num_str @{thm ansatz_2nd_order}), |
112 [Rule.Thm ("ansatz_2nd_order",ThmC.numerals_to_Free @{thm ansatz_2nd_order}), |
113 Rule.Thm ("ansatz_3rd_order",TermC.num_str @{thm ansatz_3rd_order}) |
113 Rule.Thm ("ansatz_3rd_order",ThmC.numerals_to_Free @{thm ansatz_3rd_order}) |
114 ], |
114 ], |
115 scr = Rule.EmptyScr}); |
115 scr = Rule.EmptyScr}); |
116 |
116 |
117 val equival_trans = prep_rls'( |
117 val equival_trans = prep_rls'( |
118 Rule_Def.Repeat {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
118 Rule_Def.Repeat {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
119 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
119 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
120 rules = |
120 rules = |
121 [Rule.Thm ("equival_trans_2nd_order",TermC.num_str @{thm equival_trans_2nd_order}), |
121 [Rule.Thm ("equival_trans_2nd_order",ThmC.numerals_to_Free @{thm equival_trans_2nd_order}), |
122 Rule.Thm ("equival_trans_3rd_order",TermC.num_str @{thm equival_trans_3rd_order}) |
122 Rule.Thm ("equival_trans_3rd_order",ThmC.numerals_to_Free @{thm equival_trans_3rd_order}) |
123 ], |
123 ], |
124 scr = Rule.EmptyScr}); |
124 scr = Rule.EmptyScr}); |
125 |
125 |
126 val multiply_ansatz = prep_rls'( |
126 val multiply_ansatz = prep_rls'( |
127 Rule_Def.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
127 Rule_Def.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
128 erls = Rule_Set.Empty, |
128 erls = Rule_Set.Empty, |
129 srls = Rule_Set.Empty, calc = [], errpatts = [], |
129 srls = Rule_Set.Empty, calc = [], errpatts = [], |
130 rules = |
130 rules = |
131 [Rule.Thm ("multiply_2nd_order",TermC.num_str @{thm multiply_2nd_order}) |
131 [Rule.Thm ("multiply_2nd_order",ThmC.numerals_to_Free @{thm multiply_2nd_order}) |
132 ], |
132 ], |
133 scr = Rule.EmptyScr}); |
133 scr = Rule.EmptyScr}); |
134 \<close> |
134 \<close> |
135 |
135 |
136 text \<open>store the rule set for math engine\<close> |
136 text \<open>store the rule set for math engine\<close> |
171 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), |
171 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), |
172 (*2nd NTH_CONS pushes n+-1 into asms*) |
172 (*2nd NTH_CONS pushes n+-1 into asms*) |
173 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")], |
173 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")], |
174 srls = Rule_Set.Empty, calc = [], errpatts = [], |
174 srls = Rule_Set.Empty, calc = [], errpatts = [], |
175 rules = [ |
175 rules = [ |
176 Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}), |
176 Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}), |
177 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"), |
177 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"), |
178 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}), |
178 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}), |
179 Rule.Num_Calc("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"), |
179 Rule.Num_Calc("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"), |
180 Rule.Num_Calc("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"), |
180 Rule.Num_Calc("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"), |
181 Rule.Num_Calc("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in"), |
181 Rule.Num_Calc("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in"), |
182 Rule.Num_Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"), |
182 Rule.Num_Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"), |
183 Rule.Num_Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"), |
183 Rule.Num_Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"), |