1.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Sun Jun 30 17:27:34 2013 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Thu Jul 11 16:58:31 2013 +0200
1.3 @@ -1,4 +1,4 @@
1.4 -(* theory collecting all knowledge defined so far
1.5 +(* theory collecting all knowledge defined for the isac mathengine
1.6 WN.11.00
1.7 *)
1.8
1.9 @@ -134,8 +134,14 @@
1.10 ["Isabelle2011-->12"];
1.11 store_thm @{theory "Diff"} "IsacKnowledge" ("diff_pow_chain", prop_of @{thm diff_pow_chain})
1.12 ["Isabelle2011-->12"];
1.13 +store_thm @{theory "Diff"} "IsacKnowledge" ("diff_ln_chain", prop_of @{thm diff_ln_chain})
1.14 + ["Isabelle2011-->12"];
1.15 +store_thm @{theory "Diff"} "IsacKnowledge" ("diff_exp_chain", prop_of @{thm diff_exp_chain})
1.16 + ["Isabelle2011-->12"];
1.17 store_isa ["IsacKnowledge","Diff","Rulesets"] ["Isabelle2011-->12"];
1.18 store_rls @{theory "Diff"} norm_diff ["Isabelle2011-->12"];
1.19 +
1.20 +store_thy @{theory "Test"} ["Isabelle2011-->12"];
1.21 store_isa ["IsacKnowledge","Test","Theorems"] ["Isabelle2011-->12"];
1.22 store_thm @{theory "Test"} "IsacKnowledge" ("radd_left_commute", prop_of @{thm radd_left_commute
1.23 })
1.24 @@ -145,33 +151,33 @@
1.25 ML {*
1.26 insert_errpats ["diff","differentiate_on_R"]
1.27 ([("chain-rule-diff-both",
1.28 - [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
1.29 - parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
1.30 - parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
1.31 - parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
1.32 - parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
1.33 + [parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
1.34 + parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
1.35 + parse_patt @{theory Diff} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
1.36 + parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
1.37 + parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
1.38 [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
1.39 @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list);
1.40
1.41 insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
1.42 ([("fill-d_d-arg",
1.43 - parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
1.44 + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
1.45 ("fill-both-args",
1.46 - parse_patt thy "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
1.47 + parse_patt @{theory Diff} "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
1.48 ("fill-d_d",
1.49 - parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),
1.50 + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),
1.51 ("fill-inner-deriv",
1.52 - parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
1.53 + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
1.54 ("fill-all",
1.55 - parse_patt thy "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list);
1.56 + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list);
1.57
1.58 insert_errpats ["simplification","of_rationals"]
1.59 ([("addition-of-fractions",
1.60 - [parse_patt thy "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)",
1.61 - parse_patt thy "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)",
1.62 - parse_patt thy "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)",
1.63 - parse_patt thy "?a + (?b /?c)= (?a + ?b)/ ?c",
1.64 - parse_patt thy "?a + (?b /?c)= (?a * ?b)/ ?c"],
1.65 + [parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)",
1.66 + parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)",
1.67 + parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)",
1.68 + parse_patt @{theory Rational} "?a + (?b /?c)= (?a + ?b)/ ?c",
1.69 + parse_patt @{theory Rational} "?a + (?b /?c)= (?a * ?b)/ ?c"],
1.70 [@{thm rat_add}, @{thm rat_add_assoc}, @{thm rat_add1},
1.71 @{thm rat_add1_assoc}, @{thm rat_add2}, @{thm rat_add2_assoc},
1.72 @{thm rat_add3}, @{thm rat_add3_assoc}])]: errpat list);
1.73 @@ -181,17 +187,17 @@
1.74 (* TODO insert_errpats overwrites instead of appending
1.75 insert_errpats ["simplification","of_rationals"]
1.76 (("cancel", (*see master thesis gdarocy*)
1.77 - [(*a*)parse_patt thy "(?a + ?b)/?a = ?b",
1.78 - (*b*)parse_patt thy "(?a + ?b)/?b = ?a",
1.79 - (*c*)parse_patt thy "(?a + ?b)/(?b + ?c) = ?a / ?c",
1.80 - (*d*)parse_patt thy "(?a + ?c)/(?b + ?c) = ?a / ?b",
1.81 - (*e*)parse_patt thy "(?a + ?c)/(?b + ?c) = ?a / ?c",
1.82 - (*f*)parse_patt thy "(?a + ?b)/(?c + ?a) = ?b / ?c",
1.83 - (*g*)parse_patt thy "(?a*?b + ?c)/?a = ?b + ?c",
1.84 - (*h*)parse_patt thy "(?a*?b + ?c)/?b = ?a + ?c",
1.85 - (*i*)parse_patt thy "(?a + ?b*?c)/?b = ?a + ?c",
1.86 - (*j*)parse_patt thy "(?a + ?b*?c)/?b = ?a + ?b",
1.87 - (*k*)parse_patt thy "(?a + ?b*?e)/(?c + ?d*?e) = (?a + ?b)/(?c + ?d)"],
1.88 + [(*a*)parse_patt @{theory Rational} "(?a + ?b)/?a = ?b",
1.89 + (*b*)parse_patt @{theory Rational} "(?a + ?b)/?b = ?a",
1.90 + (*c*)parse_patt @{theory Rational} "(?a + ?b)/(?b + ?c) = ?a / ?c",
1.91 + (*d*)parse_patt @{theory Rational} "(?a + ?c)/(?b + ?c) = ?a / ?b",
1.92 + (*e*)parse_patt @{theory Rational} "(?a + ?c)/(?b + ?c) = ?a / ?c",
1.93 + (*f*)parse_patt @{theory Rational} "(?a + ?b)/(?c + ?a) = ?b / ?c",
1.94 + (*g*)parse_patt @{theory Rational} "(?a*?b + ?c)/?a = ?b + ?c",
1.95 + (*h*)parse_patt @{theory Rational} "(?a*?b + ?c)/?b = ?a + ?c",
1.96 + (*i*)parse_patt @{theory Rational} "(?a + ?b*?c)/?b = ?a + ?c",
1.97 + (*j*)parse_patt @{theory Rational} "(?a + ?b*?c)/?b = ?a + ?b",
1.98 + (*k*)parse_patt @{theory Rational} "(?a + ?b*?e)/(?c + ?d*?e) = (?a + ?b)/(?c + ?d)"],
1.99 [@{thm real_times_divide_1_eq}, (*TODO*) @{thm real_times_divide_1_eq}]));
1.100
1.101 val fillpats = [