neuper@48895
|
1 |
(* theory collecting all knowledge defined for the isac mathengine
|
neuper@42400
|
2 |
WN.11.00
|
neuper@42400
|
3 |
*)
|
neuper@42400
|
4 |
|
neuper@42400
|
5 |
theory Build_Thydata
|
neuper@55460
|
6 |
imports
|
walther@60077
|
7 |
Isac_Knowledge Interpret.Interpret
|
neuper@55408
|
8 |
Test_Build_Thydata (*for test/../build_thydata.sml, thy_hierarchy.sml*)
|
neuper@42400
|
9 |
begin
|
neuper@42400
|
10 |
|
wneuper@59472
|
11 |
subsection \<open>Build <Theory>-Data\<close>
|
wneuper@59472
|
12 |
text \<open>
|
neuper@55405
|
13 |
<Theory>-Data represent Isac's "deductive knowledge" (whereas <Problems> and <Methods>
|
neuper@55405
|
14 |
represent application-oriented and algorithmic knowledge respectively.) <Theory>-Data
|
neuper@55405
|
15 |
comprise theories from ProgLang and from Knowledge.
|
neuper@55405
|
16 |
Note, that for bootstrapping Isac "Build_Thydata" theories are available only
|
wneuper@59352
|
17 |
via "@{theory Pure}" and "Theory.ancestors_of" but not via "Thy_Info_get_theory"
|
neuper@55405
|
18 |
(while the latter is available in Test_Some.thy loaded from session Isac).
|
wneuper@59472
|
19 |
\<close>
|
wneuper@59472
|
20 |
subsubsection \<open>Get and group the theories defined in Isac\<close>
|
wneuper@59472
|
21 |
ML \<open>
|
neuper@55456
|
22 |
(* we don't use "fun isacthys ()" etc HERE,
|
neuper@55456
|
23 |
because Thy_Info.get_theory only works with session Isac, not with Build_Isac.thy *)
|
neuper@55405
|
24 |
val knowledge_parent = @{theory}
|
neuper@55405
|
25 |
val proglang_parent = @{theory ProgLang}
|
neuper@42400
|
26 |
|
neuper@55405
|
27 |
val allthys = Theory.ancestors_of @{theory};
|
wneuper@59335
|
28 |
val allthys = filter_out (member Context.eq_thy (* thys for isac bootstrap *)
|
wneuper@59600
|
29 |
[(*@{theory ProgLang}: required in isacthys' below*) @{theory Interpret}, @{theory MathEngine},
|
wneuper@59600
|
30 |
@{theory BridgeLibisabelle}, knowledge_parent]) allthys (*["Isac_Knowledge", ..., "Isac_Knowledge"]*)
|
neuper@42400
|
31 |
|
wneuper@59592
|
32 |
val isabthys' = (*["Complex_Main", "Taylor", .., "Isac_Knowledge"]*)
|
wneuper@59335
|
33 |
drop ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys);
|
walther@59887
|
34 |
val isacthys' = (*["Isac_Knowledge", "Inverse_Z_Transform", .., "Know_Store"]*)
|
walther@59603
|
35 |
take ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys)
|
walther@59603
|
36 |
|> remove Context.eq_thy @{theory Test_Build_Thydata};
|
neuper@42400
|
37 |
|
wneuper@59592
|
38 |
val knowthys' = (*["Isac_Knowledge", .., "Descript"]*)
|
wneuper@59335
|
39 |
take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys');
|
walther@59887
|
40 |
val progthys' = (*["Auto_Prog", .., "Know_Store"]*)
|
walther@59603
|
41 |
drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys')
|
walther@59866
|
42 |
|> remove Context.eq_thy @{theory BaseDefinitions};
|
walther@59603
|
43 |
\<close>
|
walther@59603
|
44 |
declare[[ML_print_depth = 999]]
|
walther@59603
|
45 |
ML \<open>
|
walther@59880
|
46 |
map Context.theory_name progthys'
|
walther@59603
|
47 |
\<close> ML \<open>
|
wneuper@59472
|
48 |
\<close>
|
neuper@42400
|
49 |
|
wneuper@59472
|
50 |
subsubsection \<open>From rule-sets collect theorems, which have been taken from Isabelle\<close>
|
wneuper@59472
|
51 |
ML \<open>
|
neuper@55484
|
52 |
val isacrlsthms = (*length = 460*)
|
walther@59874
|
53 |
thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : ThmC.T list
|
neuper@42400
|
54 |
|
neuper@55484
|
55 |
val rlsthmsNOTisac = isacrlsthms (*length = 36*)
|
neuper@55405
|
56 |
|> filter (fn (deriv, _) =>
|
walther@59879
|
57 |
member op= (map Context.theory_name isabthys') (ThyC.cut_id deriv))
|
walther@59874
|
58 |
: ThmC.T list
|
wneuper@59472
|
59 |
\<close>
|
neuper@55405
|
60 |
|
wneuper@59472
|
61 |
subsubsection \<open>Collect data in a (key, data) list and insert data into the tree\<close>
|
wneuper@59472
|
62 |
text \<open>
|
neuper@55405
|
63 |
The sequence in the (key, data) list is arbitrary, because insertion using the key
|
neuper@55405
|
64 |
is random. The sequence of the root nodes "IsacKnowledge", "Isabelle"
|
walther@59887
|
65 |
and "IsacScripts" is determined in Know_Store.thy.
|
wneuper@59472
|
66 |
\<close>
|
walther@59621
|
67 |
text \<open>
|
walther@59621
|
68 |
ATTENTION: ===================================================================================
|
walther@59621
|
69 |
the code below does NOT terminate in x86_64_32 mode of Poly/ML 5.8.
|
walther@59621
|
70 |
Nevertheless, Build_Isac.thy should (and can!) be used in this mode,
|
walther@59621
|
71 |
while preferences ML_system_64 = "true" never reaches Build_Isac.thy.
|
walther@59621
|
72 |
==============================================================================================
|
walther@59621
|
73 |
See "etc/preferences".
|
walther@59621
|
74 |
\<close>
|
wneuper@59472
|
75 |
ML \<open>
|
walther@59621
|
76 |
val thydata_list = (* SEE NOTE ABOVE *)
|
neuper@55405
|
77 |
collect_part "IsacKnowledge" knowledge_parent knowthys' @
|
neuper@55405
|
78 |
(map (collect_isab "Isabelle") rlsthmsNOTisac) @
|
neuper@55405
|
79 |
collect_part "IsacScripts" proglang_parent progthys'
|
walther@59917
|
80 |
: (Thy_Write.theID * Thy_Write.thydata) list
|
wneuper@59472
|
81 |
\<close>
|
walther@59614
|
82 |
ML \<open>
|
walther@59880
|
83 |
map Context.theory_name knowthys'
|
walther@59614
|
84 |
\<close> ML \<open>
|
walther@59880
|
85 |
Context.theory_name knowledge_parent
|
walther@59614
|
86 |
\<close> text \<open>
|
walther@59614
|
87 |
collect_part "IsacKnowledge" knowledge_parent knowthys'
|
walther@59614
|
88 |
\<close> ML \<open>
|
walther@59614
|
89 |
"~~~~~ fun collect_part , args:"; val (part, parent, thys) = ("IsacKnowledge", knowledge_parent, knowthys');
|
walther@59614
|
90 |
\<close> ML \<open>
|
walther@59614
|
91 |
val xxx = (flat (map (collect_thms part) thys))
|
walther@59614
|
92 |
\<close> ML \<open> (*isa*)
|
walther@59614
|
93 |
length thys = 32;
|
walther@59614
|
94 |
length xxx = 471
|
walther@59614
|
95 |
\<close> text \<open>
|
walther@59614
|
96 |
(collect_rlss part (KEStore_Elems.get_rlss parent) thys)
|
walther@59614
|
97 |
\<close> text \<open>
|
walther@59614
|
98 |
"~~~~~ fun collect_rlss , args:"; val (part, rlss, thys) = (part, (KEStore_Elems.get_rlss parent), thys);
|
walther@59614
|
99 |
\<close> text \<open>
|
walther@59614
|
100 |
(* Build_Thydata.thy in jedit leads to "Exception- Size raised" <<<===============================
|
walther@59614
|
101 |
=============================== but batch process =============================================
|
walther@59614
|
102 |
~~$ ./bin/isabelle build -o browser_info -v -b Isac
|
walther@59614
|
103 |
=============================== works =========================================================
|
walther@59614
|
104 |
*)
|
walther@59614
|
105 |
KEStore_Elems.get_rlss parent
|
walther@59614
|
106 |
\<close>
|
walther@59614
|
107 |
|
wneuper@59472
|
108 |
setup \<open>KEStore_Elems.add_thes (map (fn (a, b) => (b, a)) thydata_list)\<close>
|
neuper@42429
|
109 |
|
wneuper@59472
|
110 |
section \<open>interface for dialog-authoring\<close>
|
wneuper@59472
|
111 |
subsection \<open>Add error patterns\<close>
|
wneuper@59472
|
112 |
subsubsection \<open>Error patterns for differentiation\<close>
|
neuper@55411
|
113 |
|
wneuper@59472
|
114 |
setup \<open>KEStore_Elems.add_mets
|
walther@59997
|
115 |
[Pbl_Met_Hierarchy.update_metpair @{theory Diff} ["diff", "differentiate_on_R"]
|
s1210629013@55378
|
116 |
[("chain-rule-diff-both",
|
wneuper@59390
|
117 |
[TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
|
wneuper@59390
|
118 |
TermC.parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
|
wneuper@59390
|
119 |
TermC.parse_patt @{theory Diff} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
|
wneuper@59390
|
120 |
TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
|
wneuper@59390
|
121 |
TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
|
s1210629013@55378
|
122 |
[@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, @{thm diff_ln_chain},
|
s1210629013@55378
|
123 |
@{thm diff_exp_chain}])]]
|
wneuper@59472
|
124 |
\<close>
|
neuper@42453
|
125 |
|
wneuper@59472
|
126 |
setup \<open>
|
neuper@55448
|
127 |
KEStore_Elems.insert_fillpats
|
neuper@55448
|
128 |
[(["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"],
|
neuper@55425
|
129 |
([("fill-d_d-arg",
|
wneuper@59390
|
130 |
TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
|
neuper@55425
|
131 |
("fill-both-args",
|
wneuper@59390
|
132 |
TermC.parse_patt @{theory Diff} "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
|
neuper@55425
|
133 |
("fill-d_d",
|
wneuper@59390
|
134 |
TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),
|
neuper@55425
|
135 |
("fill-inner-deriv",
|
wneuper@59390
|
136 |
TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
|
neuper@55425
|
137 |
("fill-all",
|
walther@59909
|
138 |
TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: Error_Pattern_Def.fill_in list))
|
neuper@55425
|
139 |
]
|
wneuper@59472
|
140 |
\<close>
|
neuper@55411
|
141 |
|
wneuper@59472
|
142 |
subsubsection \<open>Error patterns for calculation with rationals\<close>
|
neuper@55411
|
143 |
|
wneuper@59472
|
144 |
setup \<open>KEStore_Elems.add_mets
|
walther@59918
|
145 |
[Pbl_Met_Hierarchy.update_metpair @{theory Rational} ["simplification", "of_rationals"]
|
s1210629013@55378
|
146 |
[("addition-of-fractions",
|
wneuper@59390
|
147 |
[TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)",
|
wneuper@59390
|
148 |
TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)",
|
wneuper@59390
|
149 |
TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)",
|
wneuper@59390
|
150 |
TermC.parse_patt @{theory Rational} "?a + (?b /?c)= (?a + ?b)/ ?c",
|
wneuper@59390
|
151 |
TermC.parse_patt @{theory Rational} "?a + (?b /?c)= (?a * ?b)/ ?c"],
|
s1210629013@55378
|
152 |
[@{thm rat_add}, @{thm rat_add_assoc}, @{thm rat_add1}, @{thm rat_add1_assoc},
|
s1210629013@55378
|
153 |
@{thm rat_add2}, @{thm rat_add2_assoc}, @{thm rat_add3}, @{thm rat_add3_assoc}])]]
|
wneuper@59472
|
154 |
\<close>
|
neuper@42516
|
155 |
|
wneuper@59472
|
156 |
ML \<open>
|
neuper@42516
|
157 |
(*TODO insert_fillpats ["IsacKnowledge", "Rational", "Theorems", "???"]*)
|
neuper@42516
|
158 |
|
neuper@42516
|
159 |
(* TODO insert_errpats overwrites instead of appending
|
walther@59997
|
160 |
insert_errpats ["simplification", "of_rationals"]
|
neuper@42516
|
161 |
(("cancel", (*see master thesis gdarocy*)
|
neuper@48895
|
162 |
[(*a*)parse_patt @{theory Rational} "(?a + ?b)/?a = ?b",
|
neuper@48895
|
163 |
(*b*)parse_patt @{theory Rational} "(?a + ?b)/?b = ?a",
|
neuper@48895
|
164 |
(*c*)parse_patt @{theory Rational} "(?a + ?b)/(?b + ?c) = ?a / ?c",
|
neuper@48895
|
165 |
(*d*)parse_patt @{theory Rational} "(?a + ?c)/(?b + ?c) = ?a / ?b",
|
neuper@48895
|
166 |
(*e*)parse_patt @{theory Rational} "(?a + ?c)/(?b + ?c) = ?a / ?c",
|
neuper@48895
|
167 |
(*f*)parse_patt @{theory Rational} "(?a + ?b)/(?c + ?a) = ?b / ?c",
|
neuper@48895
|
168 |
(*g*)parse_patt @{theory Rational} "(?a*?b + ?c)/?a = ?b + ?c",
|
neuper@48895
|
169 |
(*h*)parse_patt @{theory Rational} "(?a*?b + ?c)/?b = ?a + ?c",
|
neuper@48895
|
170 |
(*i*)parse_patt @{theory Rational} "(?a + ?b*?c)/?b = ?a + ?c",
|
neuper@48895
|
171 |
(*j*)parse_patt @{theory Rational} "(?a + ?b*?c)/?b = ?a + ?b",
|
neuper@48895
|
172 |
(*k*)parse_patt @{theory Rational} "(?a + ?b*?e)/(?c + ?d*?e) = (?a + ?b)/(?c + ?d)"],
|
neuper@42516
|
173 |
[@{thm real_times_divide_1_eq}, (*TODO*) @{thm real_times_divide_1_eq}]));
|
neuper@42516
|
174 |
|
neuper@42445
|
175 |
val fillpats = [
|
neuper@42445
|
176 |
("fill-cancel-left-num",
|
neuper@42445
|
177 |
parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = _ / ?c", "cancel"),
|
neuper@42445
|
178 |
("fill-cancel-left-den",
|
neuper@42445
|
179 |
parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = ?b / _", "cancel"),
|
neuper@42445
|
180 |
("fill-cancel-none",
|
neuper@42445
|
181 |
parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = ?b / ?c", "cancel"),
|
neuper@42445
|
182 |
|
neuper@42445
|
183 |
("fill-cancel-left-add-num1",
|
neuper@42445
|
184 |
parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + ?c) / ?d", "cancel"),
|
neuper@42445
|
185 |
("fill-cancel-left-add-num2",
|
neuper@42445
|
186 |
parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + _) / ?d", "cancel"),
|
neuper@42445
|
187 |
("fill-cancel-left-add-num3",
|
neuper@42445
|
188 |
parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + _) / ?d", "cancel"),
|
neuper@42445
|
189 |
("fill-cancel-left-add-num4",
|
neuper@42445
|
190 |
parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + ?c) / _", "cancel"),
|
neuper@42445
|
191 |
("fill-cancel-left-add-num5",
|
neuper@42445
|
192 |
parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + ?c) / _", "cancel"),
|
neuper@42445
|
193 |
("fill-cancel-left-add-num6",
|
neuper@42445
|
194 |
parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + _) / _", "cancel"),
|
neuper@42445
|
195 |
("fill-cancel-left-add-none",
|
neuper@42445
|
196 |
parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + ?c) / ?d", "cancel"),
|
neuper@42445
|
197 |
|
neuper@42445
|
198 |
("fill-cancel-left-add-den1",
|
neuper@42445
|
199 |
parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
|
neuper@42445
|
200 |
("fill-cancel-left-add-den2",
|
neuper@42445
|
201 |
parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
|
neuper@42445
|
202 |
("fill-cancel-left-add-den3",
|
neuper@42445
|
203 |
parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
|
neuper@42445
|
204 |
("fill-cancel-left-add-den4",
|
neuper@42445
|
205 |
parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
|
neuper@42445
|
206 |
("fill-cancel-left-add-den5",
|
neuper@42445
|
207 |
parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
|
neuper@42445
|
208 |
("fill-cancel-left-add-den6",
|
neuper@42445
|
209 |
parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
|
neuper@42445
|
210 |
("fill-cancel-left-add-none",
|
neuper@42445
|
211 |
parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel")
|
neuper@42445
|
212 |
]: fillpat list;
|
neuper@42445
|
213 |
*)
|
neuper@42445
|
214 |
|
neuper@55462
|
215 |
(* still ununsed; planned for stepToErrorpattern: this is just a reminder...
|
neuper@55435
|
216 |
|
s1210629013@55442
|
217 |
insert_errpatIDs @{theory} ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
|
neuper@42454
|
218 |
(["chain-rule-diff-both", "cancel"]: errpatID list);
|
walther@59997
|
219 |
[[[ERROR *** app_py: not found: ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
|
neuper@55462
|
220 |
since KEStore_Elems.set_ref_thy has been shifted below;
|
neuper@55462
|
221 |
this ERROR will vanish during re-engineering towards KEStore_Elems.]]]
|
neuper@42453
|
222 |
|
neuper@55462
|
223 |
...and all other related rls by hand;
|
neuper@42453
|
224 |
TODO: lift errpattIDs from theorems to respective rls AUTOMATICALLY *)
|
wneuper@59472
|
225 |
\<close>
|
neuper@48886
|
226 |
|
walther@59887
|
227 |
subsection \<open>Generate XML representation from SML (data in Know_Store)\<close>
|
wneuper@59472
|
228 |
text \<open>
|
neuper@55411
|
229 |
See the wiki
|
neuper@55411
|
230 |
http://www.ist.tugraz.at/isac/Generate_representations_for_ISAC_Knowledge#Step_1:_Generate_XML_representation_from_SML
|
neuper@55411
|
231 |
|
neuper@55411
|
232 |
val path = "/tmp/xmldata/";
|
neuper@55411
|
233 |
thy_hierarchy2file (path ^ "thy/");
|
neuper@55411
|
234 |
thes2file (path ^ "thy/");
|
neuper@55411
|
235 |
pbl_hierarchy2file (path ^ "pbl/");
|
neuper@55411
|
236 |
pbls2file (path ^ "pbl/");
|
neuper@55411
|
237 |
met_hierarchy2file (path ^ "met/");
|
neuper@55411
|
238 |
mets2file (path ^ "met/");
|
neuper@55411
|
239 |
|
neuper@55411
|
240 |
Adjust ''val path'' (for details see wiki) and copy line for line
|
neuper@55493
|
241 |
into an ML-block.
|
neuper@55493
|
242 |
Scroll down the Output window and look for potential error messages.
|
wneuper@59472
|
243 |
\<close>
|
neuper@55455
|
244 |
|
wneuper@59472
|
245 |
section \<open>Link KEStore_Elems to completed IsacKnowledge\<close>
|
wneuper@59472
|
246 |
ML \<open>KEStore_Elems.set_ref_thy @{theory}\<close>
|
neuper@55435
|
247 |
|
neuper@42400
|
248 |
end
|