71 "----------- fun collect_isab_thys ----------------------"; |
71 "----------- fun collect_isab_thys ----------------------"; |
72 val ancestors = Theory.ancestors_of @{theory "Complex_Main"}; |
72 val ancestors = Theory.ancestors_of @{theory "Complex_Main"}; |
73 val isabthms = (flat o (map Theory.axioms_of)) ancestors; |
73 val isabthms = (flat o (map Theory.axioms_of)) ancestors; |
74 |
74 |
75 val isacrules = (flat o (map (thms_of_rls o #2 o #2))) |
75 val isacrules = (flat o (map (thms_of_rls o #2 o #2))) |
76 (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")); |
76 (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")); |
77 (*thms from rulesets*) |
77 (*thms from rulesets*) |
78 (*=== inhibit exn AK110725 ============================================================= |
78 (*=== inhibit exn AK110725 ============================================================= |
79 val isacrlsthms = ((map rep_thm_G') o flat o |
79 val isacrlsthms = ((map rep_thm_G') o flat o |
80 (map (PureThy.all_thms_of_rls o #2 o #2))) |
80 (map (PureThy.all_thms_of_rls o #2 o #2))) |
81 (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")); |
81 (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")); |
82 length isacrlsthms; |
82 length isacrlsthms; |
83 (*takes a few seconds... |
83 (*takes a few seconds... |
84 val isacrlsthms = gen_distinct eq_thmI isacrlsthms; |
84 val isacrlsthms = gen_distinct eq_thmI isacrlsthms; |
85 length isacrlsthms; |
85 length isacrlsthms; |
86 "----- theorems used in isac's rulesets -----vvvvvvvvvvvvvvvvvvvvv"; |
86 "----- theorems used in isac's rulesets -----vvvvvvvvvvvvvvvvvvvvv"; |
157 ((op mem) o swap) (dropthys', "Isac"); |
157 ((op mem) o swap) (dropthys', "Isac"); |
158 curry ((op mem) o swap); |
158 curry ((op mem) o swap); |
159 curry ((op mem) o swap) dropthys' "Isac"; |
159 curry ((op mem) o swap) dropthys' "Isac"; |
160 val ancestors_rls = |
160 val ancestors_rls = |
161 filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory')) |
161 filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory')) |
162 (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))); |
162 (rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))); |
163 |
163 |
164 take (10, map #1 ancestors_rls) = |
164 take (10, map #1 ancestors_rls) = |
165 ["expand_binomtest", "make_polytest", "rearrange_assoc", "ac_plus_times", "norm_equation", |
165 ["expand_binomtest", "make_polytest", "rearrange_assoc", "ac_plus_times", "norm_equation", |
166 "matches", "isolate_bdv", "isolate_root", "tval_rls", "Test_simplify"]; (*..all rls in each*) |
166 "matches", "isolate_bdv", "isolate_root", "tval_rls", "Test_simplify"]; (*..all rls in each*) |
167 |
167 |
168 (* WN120523 popped up again ?!?!? |
168 (* WN120523 popped up again ?!?!? |
169 if length (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) <> length ancestors_rls then () |
169 if length (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) <> length ancestors_rls then () |
170 else error "rewtools.sml: diff.behav. in thy_containing_rls 2 ERRATICAL?"; |
170 else error "rewtools.sml: diff.behav. in thy_containing_rls 2 ERRATICAL?"; |
171 *) |
171 *) |
172 |
172 |
173 val rls' = "norm_Poly"; |
173 val rls' = "norm_Poly"; |
174 case assoc (ancestors_rls, rls') of |
174 case assoc (ancestors_rls, rls') of |
189 map #1 dropthys = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin"]; (*= true WN120410*) |
189 map #1 dropthys = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin"]; (*= true WN120410*) |
190 |
190 |
191 val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list; |
191 val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list; |
192 val ancestors_rls = |
192 val ancestors_rls = |
193 filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory')) |
193 filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory')) |
194 (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))); |
194 (rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))); |
195 |
195 |
196 case assoc (ancestors_rls, rls') of |
196 case assoc (ancestors_rls, rls') of |
197 SOME ("Poly", Seq {id = "norm_Poly", ...}) => () |
197 SOME ("Poly", Seq {id = "norm_Poly", ...}) => () |
198 | _ => error "thy_containing_rls changed 2"; |
198 | _ => error "thy_containing_rls changed 2"; |
199 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*) |
199 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*) |
216 "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem", "Integrate", |
216 "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem", "Integrate", |
217 "Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq", "RootEq", |
217 "Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq", "RootEq", |
218 "LinEq", "Root", "Equation", "Rational", "Poly", "Simplify"] (*, "Atools", ..*) |
218 "LinEq", "Root", "Equation", "Rational", "Poly", "Simplify"] (*, "Atools", ..*) |
219 then () else error "thy_containing_cal changed ancestors_rls for Atools"; |
219 then () else error "thy_containing_cal changed ancestors_rls for Atools"; |
220 |
220 |
221 Thy_Info.get_theory thy' |> KEStore_Elems.get_calcs |> rev; |
221 Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev; |
222 Thy_Info.get_theory thy' |> KEStore_Elems.get_calcs |> rev |> map #1; |
222 Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev |> map #1; |
223 Thy_Info.get_theory thy' |> KEStore_Elems.get_calcs |> rev |> map (#1 : calc -> string); |
223 Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev |> map (#1 : calc -> string); |
224 |
224 |
225 val ancestors_cal = |
225 val ancestors_cal = |
226 filter_out ((curry ((op mem) o swap) dropthys') o (#1 : calc -> string)) |
226 filter_out ((curry ((op mem) o swap) dropthys') o (#1 : calc -> string)) |
227 (Thy_Info.get_theory thy' |> KEStore_Elems.get_calcs |> rev); |
227 (Thy_Info.get_theory thy' |> Test_KEStore_Elems.get_calcs |> rev); |
228 |
228 |
229 if thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "plus") |
229 if thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "plus") |
230 (*WN120410: SHOULD BE = ("IsacKnowledge", "Atools")*) |
230 (*WN120410: SHOULD BE = ("IsacKnowledge", "Atools")*) |
231 then () else error "(wrong) thy_containing_cal 'Biegelinie' 'PLUS' changed"; |
231 then () else error "(wrong) thy_containing_cal 'Biegelinie' 'PLUS' changed"; |
232 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*) |
232 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*) |