7 begin |
7 begin |
8 |
8 |
9 text {* This theory collects data of theorems and axioms defined and used in ISAC *} |
9 text {* This theory collects data of theorems and axioms defined and used in ISAC *} |
10 |
10 |
11 ML {* |
11 ML {* |
12 writeln ("======= length (KEStore_Elems = " ^ |
12 (*writeln ("======= length (KEStore_Elems = " ^ |
13 (KEStore_Elems.get_mets @{theory} |> count_kestore_ptyps |> string_of_int)); |
13 (KEStore_Elems.get_mets @{theory} |> count_kestore_ptyps |> string_of_int)); |
14 writeln ("======= length (! mets) = " ^ |
14 writeln ("======= length (! mets) = " ^ |
15 (count_kestore_ptyps (! mets) |> string_of_int)); |
15 (count_kestore_ptyps (! mets) |> string_of_int)); |
16 |
16 |
17 (* when creating session Isac see output in ~/.isabelle/../log/Isac *) |
17 (* when creating session Isac see output in ~/.isabelle/../log/Isac *) |
28 writeln "======= begin ! mets ======="; |
28 writeln "======= begin ! mets ======="; |
29 ! mets |> map check_kestore_met |> map writeln; |
29 ! mets |> map check_kestore_met |> map writeln; |
30 writeln "\n\n======= ! mets ordered ======="; |
30 writeln "\n\n======= ! mets ordered ======="; |
31 ! mets |> sort_kestore_met |> sort ptyp_ord |
31 ! mets |> sort_kestore_met |> sort ptyp_ord |
32 |> map check_kestore_met |> enumerate_strings |> sort string_ord |> map writeln; |
32 |> map check_kestore_met |> enumerate_strings |> sort string_ord |> map writeln; |
33 writeln "======= end ! mets ======="; |
33 writeln "======= end ! mets =======";*) |
34 *} |
34 *} |
35 |
35 |
36 ML {* |
36 ML {* |
37 (** set up a list for getting guh + theID for a thm defined in isabelle (and NOT in isac) **) |
37 (** set up a list for getting guh + theID for a thm defined in isabelle (and NOT in isac) **) |
38 |
38 |
168 store_thm @{theory "Test"} "IsacKnowledge" ("radd_left_commute", prop_of @{thm radd_left_commute |
168 store_thm @{theory "Test"} "IsacKnowledge" ("radd_left_commute", prop_of @{thm radd_left_commute |
169 }) |
169 }) |
170 ["Isabelle2011-->12"]; |
170 ["Isabelle2011-->12"]; |
171 (*\========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============/*) |
171 (*\========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============/*) |
172 *} |
172 *} |
173 ML {* |
|
174 insert_errpats ["diff","differentiate_on_R"] |
|
175 ([("chain-rule-diff-both", |
|
176 [parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)", |
|
177 parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)", |
|
178 parse_patt @{theory Diff} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)", |
|
179 parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u", |
|
180 parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"], |
|
181 [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, |
|
182 @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list); |
|
183 *} |
|
184 setup {* KEStore_Elems.add_mets |
173 setup {* KEStore_Elems.add_mets |
185 [update_metpair ["diff","differentiate_on_R"] |
174 [update_metpair ["diff","differentiate_on_R"] |
186 [("chain-rule-diff-both", |
175 [("chain-rule-diff-both", |
187 [parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)", |
176 [parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)", |
188 parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)", |
177 parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)", |
203 parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"), |
192 parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"), |
204 ("fill-inner-deriv", |
193 ("fill-inner-deriv", |
205 parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"), |
194 parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"), |
206 ("fill-all", |
195 ("fill-all", |
207 parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list); |
196 parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list); |
208 |
|
209 insert_errpats ["simplification","of_rationals"] |
|
210 ([("addition-of-fractions", |
|
211 [parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)", |
|
212 parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)", |
|
213 parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)", |
|
214 parse_patt @{theory Rational} "?a + (?b /?c)= (?a + ?b)/ ?c", |
|
215 parse_patt @{theory Rational} "?a + (?b /?c)= (?a * ?b)/ ?c"], |
|
216 [@{thm rat_add}, @{thm rat_add_assoc}, @{thm rat_add1}, |
|
217 @{thm rat_add1_assoc}, @{thm rat_add2}, @{thm rat_add2_assoc}, |
|
218 @{thm rat_add3}, @{thm rat_add3_assoc}])]: errpat list); |
|
219 *} |
197 *} |
220 setup {* KEStore_Elems.add_mets |
198 setup {* KEStore_Elems.add_mets |
221 [update_metpair ["simplification", "of_rationals"] |
199 [update_metpair ["simplification", "of_rationals"] |
222 [("addition-of-fractions", |
200 [("addition-of-fractions", |
223 [parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)", |
201 [parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)", |