1 (* Title: Tools/isac/Knowledge/Build_Thydata.thy
2 Author: Walther Neuper, JKU Linz
3 (c) due to copyright terms
5 Collect all knowledge defined for the isac mathengine
11 Test_Build_Thydata (*for test/../build_thydata.sml, thy_hierarchy.sml*)
14 subsection \<open>Build <Theory>-Data\<close>
16 <Theory>-Data represent Isac's "deductive knowledge" (whereas <Problems> and <Methods>
17 represent application-oriented and algorithmic knowledge respectively.) <Theory>-Data
18 comprise theories from ProgLang and from Knowledge.
20 Note that under normal circumstances, theories are only available from the given formal
21 context, not the global theory database (\<^ML_structure>\<open>Thy_Info\<close>). The following
22 operations always work:
24 \<^item> \<^ML>\<open>@{theory Pure}\<close>, \<^ML>\<open>@{theory Main}\<close>, \<^ML>\<open>@{theory Complex_Main}\<close>
25 \<^item> \<^ML>\<open>Theory.ancestors_of\<close>, or better \<^ML>\<open>Theory.nodes_of\<close>
26 \<^item> \<^ML>\<open>Context.get_theory\<close> for situations of explicit name-lookup (short or long)
28 In contrast, old-style \<^ML>\<open>Thy_Info.get_theory\<close> requires a finished logic image, for
29 example in \<^file>\<open>$ISABELLE_ISAC_TEST/Tools/isac/Test_Some.thy\<close> loaded from session Isac.
31 Note on planned improvements (WN):
32 All theories below ML_structure\<open>MathEngine\<close> in the sessiongraph
33 can be considered as Isac's version of Pure: the respective code handles items
34 declared later between \<^ML>\<open>@{theory Base_Tools}\<close> and \<^ML>\<open>@{theory Isac_Knowledge}\<close>.
35 These items are contained in the ML_structure\<open>Context\<close> in current Isabelle,
36 thus all ML_structure\<open>KEStore_Elems\<close> can be replaced by more native Isabelle mechanisms --
38 \<^item> \<^ML>\<open>KEStore_Elems.add_pbls\<close> and \<^ML>\<open>KEStore_Elems.get_pbls\<close>,
39 handling a tree of \<^ML_type>\<open>Problem.T\<close>
40 \<^item> \<^ML>\<open>KEStore_Elems.add_mets\<close> and \<^ML>\<open>KEStore_Elems.get_mets\<close>,
41 handling a tree of \<^ML_type>\<open>MethodC.T\<close>
42 where both trees have a structure independent from the dependency graph
43 between \<^ML>\<open>@{theory Base_Tools}\<close> and \<^ML>\<open>@{theory Isac_Knowledge}\<close>.
46 subsubsection \<open>Get and group the theories defined in Isac\<close>
48 (* we don't use "fun isacthys ()" etc HERE,
49 because Thy_Info.get_theory only works with session Isac, not with Build_Isac.thy *)
50 val knowledge_parent = @{theory}
51 val proglang_parent = @{theory ProgLang}
53 val allthys = Theory.ancestors_of @{theory};
54 val allthys = filter_out (member Context.eq_thy (* thys for isac bootstrap *)
55 [(*@{theory ProgLang}: required in isacthys' below*) @{theory Interpret}, @{theory MathEngine},
56 @{theory BridgeLibisabelle}, knowledge_parent]) allthys (*["Isac_Knowledge", ..., "Isac_Knowledge"]*)
58 val isabthys' = (*["Complex_Main", "Taylor", .., "Isac_Knowledge"]*)
59 drop ((find_index (curry Context.eq_thy ThyC.last_isabelle_thy) allthys), allthys);
60 val isacthys' = (*["Isac_Knowledge", "Inverse_Z_Transform", .., "Know_Store"]*)
61 take ((find_index (curry Context.eq_thy ThyC.last_isabelle_thy) allthys), allthys)
62 |> remove Context.eq_thy @{theory Test_Build_Thydata};
64 val knowthys' = (*["Isac_Knowledge", .., "Input_Descript"]*)
65 take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys');
66 val progthys' = (*["Auto_Prog", .., "Know_Store"]*)
67 drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys')
68 |> remove Context.eq_thy @{theory BaseDefinitions};
70 declare[[ML_print_depth = 999]]
76 subsubsection \<open>From rule-sets collect theorems, which have been taken from Isabelle\<close>
78 val isacrlsthms = (*length = 460*)
79 Thy_Hierarchy.thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : ThmC.T list
81 val rlsthmsNOTisac = isacrlsthms (*length = 36*)
82 |> filter (fn (deriv, _) =>
83 member op= (map Context.theory_name isabthys') (ThyC.cut_id deriv))
87 subsubsection \<open>Collect data in a (key, data) list and insert data into the tree\<close>
89 The sequence in the (key, data) list is arbitrary, because insertion using the key
90 is random. The sequence of the root nodes "IsacKnowledge", "Isabelle"
91 and "IsacScripts" is determined in Know_Store.thy.
94 ATTENTION: ===================================================================================
95 the code below does NOT terminate in x86_64_32 mode of Poly/ML 5.8.
96 Nevertheless, Build_Isac.thy should (and can!) be used in this mode,
97 while preferences ML_system_64 = "true" never reaches Build_Isac.thy.
98 ==============================================================================================
99 See "etc/preferences".
102 val thydata_list = (* SEE NOTE ABOVE *)
103 Thy_Hierarchy.collect_part "IsacKnowledge" knowledge_parent knowthys' @
104 (map (Thy_Hierarchy.collect_isab "Isabelle") rlsthmsNOTisac) @
105 Thy_Hierarchy.collect_part "IsacScripts" proglang_parent progthys'
106 : (Thy_Write.theID * Thy_Write.thydata) list
109 map Context.theory_name knowthys'
111 Context.theory_name knowledge_parent
112 \<close> text \<open>
113 collect_part "IsacKnowledge" knowledge_parent knowthys'
115 "~~~~~ fun collect_part , args:"; val (part, parent, thys) = ("IsacKnowledge", knowledge_parent, knowthys');
117 val xxx = (flat (map (Thy_Hierarchy.collect_thms part) thys))
118 \<close> ML \<open> (*isa*)
121 \<close> text \<open>
122 (collect_rlss part (KEStore_Elems.get_rlss parent) thys)
123 \<close> text \<open>
124 "~~~~~ fun collect_rlss , args:"; val (part, rlss, thys) = (part, (KEStore_Elems.get_rlss parent), thys);
125 \<close> text \<open>
126 (* Build_Thydata.thy in jedit leads to "Exception- Size raised" <<<===============================
127 =============================== but batch process =============================================
128 ~~$ ./bin/isabelle build -o browser_info -v -b Isac
129 =============================== works =========================================================
131 KEStore_Elems.get_rlss parent
134 setup \<open>KEStore_Elems.add_thes (map (fn (a, b) => (b, a)) thydata_list)\<close>
136 section \<open>interface for dialog-authoring\<close>
137 subsection \<open>Add error patterns\<close>
138 subsubsection \<open>Error patterns for differentiation\<close>
140 setup \<open>KEStore_Elems.add_mets @{context}
141 [Pbl_Met_Hierarchy.update_metpair @{theory Diff} ["diff", "differentiate_on_R"]
142 [("chain-rule-diff-both",
143 [TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
144 TermC.parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
145 TermC.parse_patt @{theory Diff} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)",
146 TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
147 TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
148 [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, @{thm diff_ln_chain},
149 @{thm diff_exp_chain}])]]
153 KEStore_Elems.insert_fillpats
154 [(["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"],
156 TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
158 TermC.parse_patt @{theory Diff} "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
160 TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),
162 TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
164 TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: Error_Pattern_Def.fill_in list))
168 subsubsection \<open>Error patterns for calculation with rationals\<close>
170 setup \<open>KEStore_Elems.add_mets @{context}
171 [Pbl_Met_Hierarchy.update_metpair @{theory Rational} ["simplification", "of_rationals"]
172 [("addition-of-fractions",
173 [TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)",
174 TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)",
175 TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)",
176 TermC.parse_patt @{theory Rational} "?a + (?b /?c)= (?a + ?b)/ ?c",
177 TermC.parse_patt @{theory Rational} "?a + (?b /?c)= (?a * ?b)/ ?c"],
178 [@{thm rat_add}, @{thm rat_add_assoc}, @{thm rat_add1}, @{thm rat_add1_assoc},
179 @{thm rat_add2}, @{thm rat_add2_assoc}, @{thm rat_add3}, @{thm rat_add3_assoc}])]]
183 (*TODO insert_fillpats ["IsacKnowledge", "Rational", "Theorems", "???"]*)
185 (* TODO insert_errpats overwrites instead of appending
186 insert_errpats ["simplification", "of_rationals"]
187 (("cancel", (*see master thesis gdarocy*)
188 [(*a*)parse_patt @{theory Rational} "(?a + ?b)/?a = ?b",
189 (*b*)parse_patt @{theory Rational} "(?a + ?b)/?b = ?a",
190 (*c*)parse_patt @{theory Rational} "(?a + ?b)/(?b + ?c) = ?a / ?c",
191 (*d*)parse_patt @{theory Rational} "(?a + ?c)/(?b + ?c) = ?a / ?b",
192 (*e*)parse_patt @{theory Rational} "(?a + ?c)/(?b + ?c) = ?a / ?c",
193 (*f*)parse_patt @{theory Rational} "(?a + ?b)/(?c + ?a) = ?b / ?c",
194 (*g*)parse_patt @{theory Rational} "(?a*?b + ?c)/?a = ?b + ?c",
195 (*h*)parse_patt @{theory Rational} "(?a*?b + ?c)/?b = ?a + ?c",
196 (*i*)parse_patt @{theory Rational} "(?a + ?b*?c)/?b = ?a + ?c",
197 (*j*)parse_patt @{theory Rational} "(?a + ?b*?c)/?b = ?a + ?b",
198 (*k*)parse_patt @{theory Rational} "(?a + ?b*?e)/(?c + ?d*?e) = (?a + ?b)/(?c + ?d)"],
199 [@{thm real_times_divide_1_eq}, (*TODO*) @{thm real_times_divide_1_eq}]));
202 ("fill-cancel-left-num",
203 parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = _ / ?c", "cancel"),
204 ("fill-cancel-left-den",
205 parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = ?b / _", "cancel"),
207 parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = ?b / ?c", "cancel"),
209 ("fill-cancel-left-add-num1",
210 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + ?c) / ?d", "cancel"),
211 ("fill-cancel-left-add-num2",
212 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + _) / ?d", "cancel"),
213 ("fill-cancel-left-add-num3",
214 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + _) / ?d", "cancel"),
215 ("fill-cancel-left-add-num4",
216 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + ?c) / _", "cancel"),
217 ("fill-cancel-left-add-num5",
218 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + ?c) / _", "cancel"),
219 ("fill-cancel-left-add-num6",
220 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + _) / _", "cancel"),
221 ("fill-cancel-left-add-none",
222 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + ?c) / ?d", "cancel"),
224 ("fill-cancel-left-add-den1",
225 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
226 ("fill-cancel-left-add-den2",
227 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
228 ("fill-cancel-left-add-den3",
229 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
230 ("fill-cancel-left-add-den4",
231 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
232 ("fill-cancel-left-add-den5",
233 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
234 ("fill-cancel-left-add-den6",
235 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
236 ("fill-cancel-left-add-none",
237 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel")
241 (* still ununsed; planned for stepToErrorpattern: this is just a reminder...
243 insert_errpatIDs @{theory} ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
244 (["chain-rule-diff-both", "cancel"]: errpatID list);
245 [[[ERROR *** app_py: not found: ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
246 since KEStore_Elems.set_ref_thy has been shifted below;
247 this ERROR will vanish during re-engineering towards KEStore_Elems.]]]
249 ...and all other related rls by hand;
250 TODO: lift errpattIDs from theorems to respective rls AUTOMATICALLY *)
253 section \<open>Link KEStore_Elems to completed IsacKnowledge\<close>
254 ML \<open>KEStore_Elems.set_ref_thy @{theory}\<close>