author | Walther Neuper <neuper@ist.tugraz.at> |
Mon, 11 Oct 2010 12:55:40 +0200 | |
branch | isac-update-Isa09-2 |
changeset 38057 | 293a30867f15 |
parent 38015 | 67ba02dffacc |
child 38058 | ad0485155c0e |
permissions | -rw-r--r-- |
neuper@37906 | 1 |
(* theory collecting all knowledge defined so far |
neuper@37906 | 2 |
WN.11.00 |
neuper@37906 | 3 |
*) |
neuper@37906 | 4 |
|
neuper@37954 | 5 |
theory Isac imports PolyMinus PolyEq Vect DiffApp Biegelinie AlgEin |
neuper@37954 | 6 |
(*InsSort +*) Test begin |
neuper@37906 | 7 |
|
neuper@37954 | 8 |
text {* dependencies alternative to those defined by R.Lang during his thesis: |
neuper@37906 | 9 |
|
neuper@37906 | 10 |
Poly Root |
neuper@37906 | 11 |
|\__________ | |
neuper@37906 | 12 |
| \ | |
neuper@37906 | 13 |
| Rational | |
neuper@37906 | 14 |
| | | |
neuper@37906 | 15 |
PolyEq RatEq RootEq |
neuper@37906 | 16 |
\ / \ / |
neuper@37906 | 17 |
\ / \ / |
neuper@37906 | 18 |
RatPolyEq RatRootEq etc. |
neuper@37954 | 19 |
*} |
neuper@37954 | 20 |
|
neuper@37954 | 21 |
ML {* |
neuper@38057 | 22 |
(**set up a list for getting guh + theID for a thm (defined in isabelle).**) |
neuper@37954 | 23 |
|
neuper@38002 | 24 |
(*local*) |
neuper@38057 | 25 |
val allthys = @{theory} :: Theory.ancestors_of @{theory}; |
neuper@38057 | 26 |
val isabthys = Theory.ancestors_of first_isac_thy; |
neuper@38057 | 27 |
val isacthys = subtract Theory.eq_thy isabthys allthys; |
neuper@38003 | 28 |
|
neuper@38002 | 29 |
val isacrlsthms = ((map (apsnd prop_of)) o |
neuper@38002 | 30 |
(gen_distinct eq_thmI) o (map rep_thm_G') o flat o |
neuper@37954 | 31 |
(map (thms_of_rls o #2 o #2))) (!ruleset'); |
neuper@38002 | 32 |
val isacthms = |
neuper@38002 | 33 |
(flat o (map Theory.axioms_of)) isacthys : (thmID * term) list; |
neuper@38002 | 34 |
(*in*) |
neuper@38057 | 35 |
theory' := (map Context.theory_name isacthys) ~~ isacthys; |
neuper@38003 | 36 |
val rlsthmsNOTisac = gen_diff eq_thmI' (isacrlsthms, isacthms); |
neuper@38002 | 37 |
(*end;*) |
neuper@37954 | 38 |
|
neuper@37954 | 39 |
(*.set up the list using 'val first_isac_thy' (see ListC.ML).*) |
neuper@38002 | 40 |
isab_thm_thy := make_isab rlsthmsNOTisac isabthys; |
neuper@37954 | 41 |
|
neuper@37954 | 42 |
(*.create the hierarchy of theory elements from IsacKnowledge |
neuper@37954 | 43 |
including thms from Isabelle used in rls; |
neuper@38057 | 44 |
elements store_*d in any *.thy are not overwritten.*) |
neuper@37954 | 45 |
|
neuper@37954 | 46 |
thehier := the_hier (!thehier) (collect_thydata ()); |
neuper@38015 | 47 |
tracing("----------------------------------\n" ^ |
neuper@37954 | 48 |
"*** insert: not found ... IS OK : \n" ^ |
neuper@37954 | 49 |
"comes from fill_parents \n" ^ |
neuper@37954 | 50 |
"----------------------------------\n"); |
neuper@38057 | 51 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
neuper@38057 | 52 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |
neuper@37954 | 53 |
*} |
neuper@37954 | 54 |
|
neuper@37954 | 55 |
end |