137 subsubsection \<open>Error patterns for differentiation\<close> |
137 subsubsection \<open>Error patterns for differentiation\<close> |
138 |
138 |
139 setup \<open>KEStore_Elems.add_mets @{context} |
139 setup \<open>KEStore_Elems.add_mets @{context} |
140 [Pbl_Met_Hierarchy.update_metpair_PIDE @{theory Diff} ["diff", "differentiate_on_R"] |
140 [Pbl_Met_Hierarchy.update_metpair_PIDE @{theory Diff} ["diff", "differentiate_on_R"] |
141 [("chain-rule-diff-both", |
141 [("chain-rule-diff-both", |
142 [TermC.parse_patt_PIDE @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)", |
142 [TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)", |
143 TermC.parse_patt_PIDE @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)", |
143 TermC.parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)", |
144 TermC.parse_patt_PIDE @{theory Diff} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)", |
144 TermC.parse_patt @{theory Diff} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)", |
145 TermC.parse_patt_PIDE @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u", |
145 TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u", |
146 TermC.parse_patt_PIDE @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"], |
146 TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"], |
147 [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, @{thm diff_ln_chain}, |
147 [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, @{thm diff_ln_chain}, |
148 @{thm diff_exp_chain}])]] |
148 @{thm diff_exp_chain}])]] |
149 \<close> |
149 \<close> |
150 |
150 |
151 setup \<open> |
151 setup \<open> |
167 subsubsection \<open>Error patterns for calculation with rationals\<close> |
167 subsubsection \<open>Error patterns for calculation with rationals\<close> |
168 |
168 |
169 setup \<open>KEStore_Elems.add_mets @{context} |
169 setup \<open>KEStore_Elems.add_mets @{context} |
170 [Pbl_Met_Hierarchy.update_metpair_PIDE @{theory Rational} ["simplification", "of_rationals"] |
170 [Pbl_Met_Hierarchy.update_metpair_PIDE @{theory Rational} ["simplification", "of_rationals"] |
171 [("addition-of-fractions", |
171 [("addition-of-fractions", |
172 [TermC.parse_patt_PIDE @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)", |
172 [TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)", |
173 TermC.parse_patt_PIDE @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)", |
173 TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)", |
174 TermC.parse_patt_PIDE @{theory Rational} "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)", |
174 TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)", |
175 TermC.parse_patt_PIDE @{theory Rational} "?a + (?b /?c)= (?a + ?b)/ ?c", |
175 TermC.parse_patt @{theory Rational} "?a + (?b /?c)= (?a + ?b)/ ?c", |
176 TermC.parse_patt_PIDE @{theory Rational} "?a + (?b /?c)= (?a * ?b)/ ?c"], |
176 TermC.parse_patt @{theory Rational} "?a + (?b /?c)= (?a * ?b)/ ?c"], |
177 [@{thm rat_add}, @{thm rat_add_assoc}, @{thm rat_add1}, @{thm rat_add1_assoc}, |
177 [@{thm rat_add}, @{thm rat_add_assoc}, @{thm rat_add1}, @{thm rat_add1_assoc}, |
178 @{thm rat_add2}, @{thm rat_add2_assoc}, @{thm rat_add3}, @{thm rat_add3_assoc}])]] |
178 @{thm rat_add2}, @{thm rat_add2_assoc}, @{thm rat_add3}, @{thm rat_add3_assoc}])]] |
179 \<close> |
179 \<close> |
180 |
180 |
181 ML \<open> |
181 ML \<open> |