28 view src/Pure/isac/IsacKnowledge/Isac.ML @ 37874:331e38464ada |
28 view src/Pure/isac/IsacKnowledge/Isac.ML @ 37874:331e38464ada |
29 date Thu Jul 22 10:45:18 2010 +0200 |
29 date Thu Jul 22 10:45:18 2010 +0200 |
30 |
30 |
31 local |
31 local |
32 val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o |
32 val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o |
33 (map (thms_of_rls o #2 o #2))) (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")); |
33 (map (thms_of_rls o #2 o #2))) (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")); |
34 val isacthms = (flat o (map (thms_of o #2))) (!theory'); |
34 val isacthms = (flat o (map (thms_of o #2))) (!theory'); |
35 in |
35 in |
36 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms); |
36 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms); |
37 end; |
37 end; |
38 *) |
38 *) |
39 val isacrlsthms''''' = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o |
39 val isacrlsthms''''' = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o |
40 (map (thms_of_rls o #2 o #2))) (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) |
40 (map (thms_of_rls o #2 o #2))) (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) |
41 : (thmID * thm) list; |
41 : (thmID * thm) list; |
42 (* THIS IS TOO EXPENSIVE: |
42 (* THIS IS TOO EXPENSIVE: |
43 val all_ListC_thms = Global_Theory.all_thms_of (@{theory "ListC"}); |
43 val all_ListC_thms = Global_Theory.all_thms_of (@{theory "ListC"}); |
44 length all_ListC_thms = 19860 <<<<<-----*) |
44 length all_ListC_thms = 19860 <<<<<-----*) |
45 val isacthys = (union Theory.eq_thy (! knowthys) (! progthys)); |
45 val isacthys = (union Theory.eq_thy (! knowthys) (! progthys)); |
135 map Context.theory_name progthys' = ["Script", "Tools", "ListC"]; (*WN120201 true*) |
135 map Context.theory_name progthys' = ["Script", "Tools", "ListC"]; (*WN120201 true*) |
136 |
136 |
137 "-------- prop_of thm .. Theory.axioms_of ---------------"; |
137 "-------- prop_of thm .. Theory.axioms_of ---------------"; |
138 "-------- prop_of thm .. Theory.axioms_of ---------------"; |
138 "-------- prop_of thm .. Theory.axioms_of ---------------"; |
139 "-------- prop_of thm .. Theory.axioms_of ---------------"; |
139 "-------- prop_of thm .. Theory.axioms_of ---------------"; |
140 val isacrlsthms''''' = (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) |
140 val isacrlsthms''''' = (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) |
141 |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*) |
141 |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*) |
142 |> flat |
142 |> flat |
143 |> map thm_of_thm |
143 |> map thm_of_thm |
144 |> gen_distinct Thm.eq_thm |
144 |> gen_distinct Thm.eq_thm |
145 |> map (` I) |
145 |> map (` I) |
245 subtract Thm.eq_thm (map #2 all_ListC_thms) (map #2 all_Complex_Main_thms); |
245 subtract Thm.eq_thm (map #2 all_ListC_thms) (map #2 all_Complex_Main_thms); |
246 ... because ListC contains no thms, but axioms only. |
246 ... because ListC contains no thms, but axioms only. |
247 "----- so we cannot get isacthms as thm, only as term ---"; |
247 "----- so we cannot get isacthms as thm, only as term ---"; |
248 "----- but we can retain isacrlsthms as thm ---"; |
248 "----- but we can retain isacrlsthms as thm ---"; |
249 *) |
249 *) |
250 val isacrlsthms = (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) |
250 val isacrlsthms = (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) |
251 |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*) |
251 |> map (thms_of_rls o #2 o #2) (*drop manually input id in Thm (id, thm)*) |
252 |> flat |
252 |> flat |
253 |> map thm_of_thm |
253 |> map thm_of_thm |
254 |> gen_distinct Thm.eq_thm |
254 |> gen_distinct Thm.eq_thm |
255 |> map (` I) |
255 |> map (` I) |