1 (* theory collecting all knowledge defined for the isac mathengine
9 text {* This theory collects data of theorems and axioms defined and used in ISAC *}
12 writeln ("======= length (KEStore_Elems = " ^
13 string_of_int (length (KEStore_Elems.get_calcs @{theory})));
14 writeln ("======= length (! calclist') = " ^
15 string_of_int (length (! calclist')));
17 (* when creating session Isac see output in ~/.isabelle/../log/Isac *)
18 writeln "======= begin KEStore_Elems.get_calcs @{theory} =======";
19 KEStore_Elems.get_calcs @{theory}
20 |> map string_of_calc |> map writeln;
21 writeln "======= KEStore_Elems.get_calcs @{theory} ordered =======";
22 KEStore_Elems.get_calcs @{theory}
23 |> map string_of_calc |> enumerate_strings |> sort string_ord |> map writeln;
24 writeln "======= end KEStore_Elems.get_calcs @{theory} =======";
26 (* use a diff-tool for comparing KEStore_Elems.get_rlss <--> ! xxx *)
27 writeln "======= begin ! calclist' =======";
28 ! calclist' |> rev (*!!!!!*)
29 |> map string_of_calc |> map writeln;
30 writeln "======= ! calclist' ordered =======";
31 ! calclist' |> rev (*!!!!!*)
32 |> map string_of_calc |> enumerate_strings |> sort string_ord |> map writeln;
33 writeln "======= end ! calclist' =======";
37 (** set up a list for getting guh + theID for a thm defined in isabelle (and NOT in isac) **)
40 val first_ProgLang_thy = @{theory ListC}
41 val first_Knowledge_thy = @{theory Delete} (*see WN120321.TODO rearrange theories*)
42 val allthys = (*!!! @{theory} :: ..START WITH Isac.thy..*) Theory.ancestors_of @{theory};
44 drop ((find_index (curry Theory.eq_thy first_ProgLang_thy) allthys) + 1, allthys);
46 take ((find_index (curry Theory.eq_thy first_ProgLang_thy) allthys) + 1, allthys);
48 take ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1, isacthys');
49 val progthys' = (*WN120321.TODO rearrange theories -------vvv*)
50 drop ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1 +3, isacthys');
52 val isacrlsthms = (KEStore_Elems.get_rlss @{theory})
53 |> map (thms_of_rls o #2 o #2)
56 |> gen_distinct Thm.eq_thm
58 |> map (apfst Thm.get_name_hint)
59 |> map (apsnd prop_of) (*this adapts to Theory.axioms_of*)
60 : (thmDeriv * term) list;
62 (flat o (map Theory.axioms_of)) isacthys': (thmDeriv * term) list;
64 isabthys := isabthys';
65 knowthys := knowthys';
66 progthys := progthys';
67 theory' := rev ((map Context.theory_name isacthys') ~~ isacthys'); (*WN120320 easy to remove*)
68 val rlsthmsNOTisac = gen_diff eq_thmI' (isacrlsthms, isacthms);
70 (*WN120319: since num_str destoys derivation_name, we hardcode rlsthmsNOTisac:
72 --- OLD compute rlsthmsNOTisac by eq_thmID ---
73 --- compute val rlsthmsNOTisac ---
74 for improvements (###sym_* etc)
77 [("HOL.refl", (prop_of o num_str) @{thm refl}),
78 ("Fun.o_apply", (prop_of o num_str) @{thm o_apply}),
79 (*/------------these are not found in ListC.thy, because they are no axioms---\*)
80 ("ListC.LENGTH.LENGTH_CONS", (prop_of o num_str) @{thm LENGTH_CONS}),
81 ("ListC.LENGTH.LENGTH_NIL", (prop_of o num_str) @{thm LENGTH_NIL}),
82 (*\------------these are not found in ListC.thy, because they are no axioms---/*)
83 ("List.take_Nil", (prop_of o num_str) @{thm take_Nil}),
84 ("List.take_Cons", (prop_of o num_str) @{thm take_Cons}),
85 ("List.if_True", (prop_of o num_str) @{thm if_True}),
86 ("HOL.if_False", (prop_of o num_str) @{thm if_False}),
87 (*###("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")*)
88 ("Rings.semiring_class.distrib_right", (prop_of o num_str) @{thm distrib_right}),
89 ("Rings.semiring_class.distrib_left", (prop_of o num_str) @{thm distrib_left}),
90 (*###("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2")*)
91 (*###("sym_realpow_addI", "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)")*)
92 ("Groups.monoid_mult_class.mult_1_right", (prop_of o num_str) @{thm mult_1_right}),
93 (*("sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1")*)
94 ("Groups.monoid_mult_class.mult_1_left", (prop_of o num_str) @{thm mult_1_left}),
95 ("Rings.mult_zero_class.mult_zero_left", (prop_of o num_str) @{thm mult_zero_left}),
96 ("Rings.mult_zero_class.mult_zero_right", (prop_of o num_str) @{thm mult_zero_right}),
97 ("Groups.monoid_add_class.add_0_left", (prop_of o num_str) @{thm add_0_left}),
98 ("Groups.monoid_add_class.add_0_right", (prop_of o num_str) @{thm add_0_right}),
99 ("Rings.division_ring_class.divide_zero_left", (prop_of o num_str) @{thm divide_zero_left}),
100 (*###("sym_mult_assoc", "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1")*)
101 ("RealDef.order_refl", (prop_of o num_str) @{thm order_refl}),
102 ("Groups.group_add_class.minus_minus", (prop_of o num_str) @{thm minus_minus}),
103 ("RealDef.mult_commute", (prop_of o num_str) @{thm mult_commute }),
104 ("RealDef.mult_assoc", (prop_of o num_str) @{thm mult_assoc}),
105 ("Groups.ab_semigroup_add_class.add_commute", (prop_of o num_str) @{thm add_commute}),
106 ("Groups.ab_semigroup_add_class.add_left_commute", (prop_of o num_str) @{thm add_left_commute}),
107 ("Groups.semigroup_add_class.add_assoc", (prop_of o num_str) @{thm add_assoc}),
108 ("Rings.ring_class.minus_mult_left", (prop_of o num_str) @{thm minus_mult_left}),
109 ("Groups.group_add_class.right_minus", (prop_of o num_str) @{thm right_minus}),
110 (*###("sym_add_assoc", "?a1 + (?b1 + ?c1) = ?a1 + ?b1 + ?c1"),*)
111 ("Rings.ring_class.left_diff_distrib", (prop_of o num_str) @{thm left_diff_distrib}),
112 ("Rings.ring_class.right_diff_distrib", (prop_of o num_str) @{thm right_diff_distrib}),
113 ("Rings.division_ring_class.minus_divide_left", (prop_of o num_str) @{thm minus_divide_left}),
114 ("Rings.division_ring_class.times_divide_eq_right", (prop_of o num_str) @{thm times_divide_eq_right}),
115 ("Fields.field_class.times_divide_eq_left", (prop_of o num_str) @{thm times_divide_eq_left}),
116 ("Fields.field_inverse_zero_class.divide_divide_eq_left", (prop_of o num_str) @{thm divide_divide_eq_left}),
117 ("Fields.field_inverse_zero_class.divide_divide_eq_right", (prop_of o num_str) @{thm divide_divide_eq_right}),
118 ("Rings.division_ring_class.divide_1", (prop_of o num_str) @{thm divide_1}),
119 ("Rings.division_ring_class.add_divide_distrib", (prop_of o num_str) @{thm add_divide_distrib }),
120 (*###("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1")*)
121 (* thms in Scripts: *)
122 ("Int.divide_minus1", (prop_of o num_str) @{thm divide_minus1}),
123 ("Groups.group_add_class.neg_equal_iff_equal", (prop_of o num_str) @{thm neg_equal_iff_equal})]
124 : (thmDeriv * term) list;
126 (*.set up the list using 'val first_isac_thy' (see ListC.thy).*)
127 (*isab_thm_thy := make_isab rlsthmsNOTisac isabthys;*)
128 isab_thm_thy := rlsthmsNOTisac; (*WN120320 remove ref*)
130 (*.create the hierarchy of theory elements from IsacKnowledge
131 including thms from Isabelle used in rls;
132 elements store_*d in any *.thy are not overwritten.*)
134 (*========== inhibit exn WN130616: ME_Isa: thy 'Script' not in system =======
135 WN130620: instead of building thehier correctly, the elements required for tests
136 are inserted at "=== inhibit exn WN130620 (1.4.1) below: fill thehier ==="
137 according to (1.4.1) below.
139 thehier := the_hier (! thehier) (collect_thydata ()); (*ME_Isa: thy 'Script' not in system*)
140 tracing("----------------------------------\n" ^
141 "*** insert: not found ... IS OK : \n" ^
142 "comes from fill_parents \n" ^
143 "----------------------------------\n");
144 ========== inhibit exn WN130616: ME_Isa: thy 'Script' not in system =======*)
147 text {* interface for dialog-authoring *}
150 (*/========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============\*)
151 store_thy @{theory "Diff"} ["Isabelle2011-->12"];
152 store_isa ["IsacKnowledge","Diff","Theorems"] ["Isabelle2011-->12"];
153 store_thm @{theory "Diff"} "IsacKnowledge" ("diff_sin_chain", prop_of @{thm diff_sin_chain})
154 ["Isabelle2011-->12"];
155 store_thm @{theory "Diff"} "IsacKnowledge" ("diff_cos_chain", prop_of @{thm diff_cos_chain})
156 ["Isabelle2011-->12"];
157 store_thm @{theory "Diff"} "IsacKnowledge" ("diff_pow_chain", prop_of @{thm diff_pow_chain})
158 ["Isabelle2011-->12"];
159 store_thm @{theory "Diff"} "IsacKnowledge" ("diff_ln_chain", prop_of @{thm diff_ln_chain})
160 ["Isabelle2011-->12"];
161 store_thm @{theory "Diff"} "IsacKnowledge" ("diff_exp_chain", prop_of @{thm diff_exp_chain})
162 ["Isabelle2011-->12"];
163 store_isa ["IsacKnowledge","Diff","Rulesets"] ["Isabelle2011-->12"];
164 store_rls @{theory "Diff"} norm_diff ["Isabelle2011-->12"];
166 store_thy @{theory "Test"} ["Isabelle2011-->12"];
167 store_isa ["IsacKnowledge","Test","Theorems"] ["Isabelle2011-->12"];
168 store_thm @{theory "Test"} "IsacKnowledge" ("radd_left_commute", prop_of @{thm radd_left_commute
170 ["Isabelle2011-->12"];
171 (*\========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============/*)
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);
184 insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
186 parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
188 parse_patt @{theory Diff} "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
190 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 * _", "chain-rule-diff-both"),
194 parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list);
196 insert_errpats ["simplification","of_rationals"]
197 ([("addition-of-fractions",
198 [parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)",
199 parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)",
200 parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)",
201 parse_patt @{theory Rational} "?a + (?b /?c)= (?a + ?b)/ ?c",
202 parse_patt @{theory Rational} "?a + (?b /?c)= (?a * ?b)/ ?c"],
203 [@{thm rat_add}, @{thm rat_add_assoc}, @{thm rat_add1},
204 @{thm rat_add1_assoc}, @{thm rat_add2}, @{thm rat_add2_assoc},
205 @{thm rat_add3}, @{thm rat_add3_assoc}])]: errpat list);
207 (*TODO insert_fillpats ["IsacKnowledge", "Rational", "Theorems", "???"]*)
209 (* TODO insert_errpats overwrites instead of appending
210 insert_errpats ["simplification","of_rationals"]
211 (("cancel", (*see master thesis gdarocy*)
212 [(*a*)parse_patt @{theory Rational} "(?a + ?b)/?a = ?b",
213 (*b*)parse_patt @{theory Rational} "(?a + ?b)/?b = ?a",
214 (*c*)parse_patt @{theory Rational} "(?a + ?b)/(?b + ?c) = ?a / ?c",
215 (*d*)parse_patt @{theory Rational} "(?a + ?c)/(?b + ?c) = ?a / ?b",
216 (*e*)parse_patt @{theory Rational} "(?a + ?c)/(?b + ?c) = ?a / ?c",
217 (*f*)parse_patt @{theory Rational} "(?a + ?b)/(?c + ?a) = ?b / ?c",
218 (*g*)parse_patt @{theory Rational} "(?a*?b + ?c)/?a = ?b + ?c",
219 (*h*)parse_patt @{theory Rational} "(?a*?b + ?c)/?b = ?a + ?c",
220 (*i*)parse_patt @{theory Rational} "(?a + ?b*?c)/?b = ?a + ?c",
221 (*j*)parse_patt @{theory Rational} "(?a + ?b*?c)/?b = ?a + ?b",
222 (*k*)parse_patt @{theory Rational} "(?a + ?b*?e)/(?c + ?d*?e) = (?a + ?b)/(?c + ?d)"],
223 [@{thm real_times_divide_1_eq}, (*TODO*) @{thm real_times_divide_1_eq}]));
226 ("fill-cancel-left-num",
227 parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = _ / ?c", "cancel"),
228 ("fill-cancel-left-den",
229 parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = ?b / _", "cancel"),
231 parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = ?b / ?c", "cancel"),
233 ("fill-cancel-left-add-num1",
234 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + ?c) / ?d", "cancel"),
235 ("fill-cancel-left-add-num2",
236 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + _) / ?d", "cancel"),
237 ("fill-cancel-left-add-num3",
238 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + _) / ?d", "cancel"),
239 ("fill-cancel-left-add-num4",
240 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + ?c) / _", "cancel"),
241 ("fill-cancel-left-add-num5",
242 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + ?c) / _", "cancel"),
243 ("fill-cancel-left-add-num6",
244 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + _) / _", "cancel"),
245 ("fill-cancel-left-add-none",
246 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + ?c) / ?d", "cancel"),
248 ("fill-cancel-left-add-den1",
249 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
250 ("fill-cancel-left-add-den2",
251 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
252 ("fill-cancel-left-add-den3",
253 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
254 ("fill-cancel-left-add-den4",
255 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
256 ("fill-cancel-left-add-den5",
257 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
258 ("fill-cancel-left-add-den6",
259 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
260 ("fill-cancel-left-add-none",
261 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel")
265 (* still ununsed; planned for stepToErrorpattern: this is just a reminder... *)
267 insert_errpatIDs ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
268 (["chain-rule-diff-both", "cancel"]: errpatID list);
270 (* ...and all other related rls by hand;
271 TODO: lift errpattIDs from theorems to respective rls AUTOMATICALLY *)
274 section {* Plans for updating isac from Isabelle2011 to Isabelle2012 and Isabelle2013 *}
275 subsection {* (1) problem analysis *}
276 subsubsection {* (1.1) "Unsynchronized.ref" are not conformant with parallel Isabelle *}
278 "Unsynchronized.ref" make "Test_Isac.thy" unreliable, too: in Isabelle2009-2
279 a (bad) trick with "check_unsynchronized_ref ()" was a way out;
280 however, this trick doesn't work anymore in Isabelle2011
281 (remarkably, "Interpret/calchead.sml" sometimes has an error, sometimes not
282 when cutting/pasting check_unsynchronized_ref in Isabelle2011;
283 but this is permanently without errors in Isabelle2012).
285 The major cases of "Unsynchronized.ref" are those in "~~/src/Tools/isac/calcelems.sml",
286 thehier, ptyps, mets, theory', rew_ord', ruleset'-->KEStore_Elems.add_rlss\get_rlss,
288 which shall be handled by "Theory_Data", see
289 "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml".
291 The transition from the above "Unsynchronized.ref" to "Theory_Data" is a task
292 to be scheduled for several days. An exception is "thehier", see (1.2) (1.3) below.
295 subsubsection {* (1.2) Removing "Unsynchronized.ref" depends on special cases *}
297 The difficulties in removing "Unsynchronized.ref" differ largely:
298 * Rational.thy will be cleared by Diana Meindl's GCD_Poly.thy, this is easy;
299 * other cases seem easy to clear, too
300 * clearing "thehier" became harder from Isabelle2009-2 to Isabelle2011;
301 for instance, isac's Context has been broken already there, because
302 essential functions from Isabelle2009-2 were dropped in Isabelle2011,
303 see for instance "fun context_thy".
304 Another obstacle for this case also seems "fun num_str".
306 So (1.2) depends on (1.3).
309 subsubsection {* (1.3) isac's numerals are not conformant with Isabelle *}
311 In 2002 isac already strived for floating point numbers. Since that time
312 isac represents numerals as "Free", see below (*1*). These experiments are
313 unsatisfactory with respect to logical soundness.
314 Since Isabelle now has started to care about floating point numbers, it is high
315 time to adopt these together with the other numerals. Isabelle2012/13's numerals
316 are different from Isabelle2011, see "test/Tools/isac/ProgLang/termC.sml".
318 The transition from "Free" to standard numerals is a task to be scheduled for
319 several weeks. The urgency of this task follows from the experience,
320 that (1.2) for "thehier" is very hard, because "num_str" seems to destroy
321 some of the long identifiers of theorems which would tremendously simplify
322 building a hierarchy of theorems according to (1.2), see (*2*) below.
324 ML {*(*1*) Free ("123.456", HOLogic.realT) *}
326 val unknown = filter ((curry op= "??.unknown") o fst) isacrlsthms;
327 unknown |> nth 1 |> snd |> term_to_string''' @{theory};
328 unknown |> nth 2 |> snd |> term_to_string''' @{theory};
329 (*but these seem ok:*)
330 Thm.get_name_hint @{thm add_0};
331 Thm.get_name_hint (num_str @{thm add_0});
334 subsubsection {* (1.4) "axioms" are a legacy feature disappearing soon *}
336 isac works with (many!) rewrite rules, which are defined as "axioms" since Isabelle2002
337 and before: isac saved time by not proving any theorem.
338 We have the message "Legacy feature! Old 'axioms' command -- use 'axiomatization' instead"
339 for some time; Isabelle2013 still accepts it.
340 This task affects collection of rewrite rules in "thehier".
343 subsection {* (2) possible solutions *}
344 subsubsection {* (2.1) Tackle (1.1) (1.2) (1.3) (1.4) already in Isabelle2011 *}
346 Advantage: we have a perfect "Test_Isac.thy" in all transitions Isabelle2011-->12-->13
347 Disadvantage: (1.3) would require effort twice: Isabelle2011-->12 and 12-->13,
348 because numerals in Isabelle2011 are quite different from Isabelle2012/13.
351 subsubsection {* (2.2) Transition Isabelle2011-->12 with minimal effort *}
353 Postpone (1.1) (1.2) (1.3) (1.4) and
354 * (1.4.1) manually insert those elements into "thehier" which are required for tests
355 * make "Test_Isac.thy" perform equivalenty on Isabelle2011 and on Isabelle2012
356 (and then on Isabelle2013).
357 This might enforce to outcomment tests in Isabelle2011 marked "Isabelle2011-->12"
360 * the transition Isabelle2011-->12 can be accomplished within few days,
361 and hopefully Isabelle2012-->13 in the same way
362 * student projects (which seem independent of the outcommented tests "Isabelle2011-->12")
363 can start immediately
365 * we do not yet know details about the transition Isabelle2012-->13,
366 which might be very different from Isabelle2011-->12
367 * some tests are outcommented;
368 However, if new regression tests come from new student project,
369 these provisionally do not concern "thehier".