7 begin |
7 begin |
8 |
8 |
9 text {* This theory collects data of theorems and axioms defined and used in ISAC *} |
9 text {* This theory collects data of theorems and axioms defined and used in ISAC *} |
10 |
10 |
11 ML {* |
11 ML {* |
12 (** set up a list for getting guh + theID for a thm (defined in isabelle) **) |
12 (** set up a list for getting guh + theID for a thm defined in isabelle (and NOT in isac) **) |
13 |
13 |
14 (*local*) |
14 (*local*) |
15 val first_ProgLang_thy = @{theory ListC} |
15 val first_ProgLang_thy = @{theory ListC} |
16 val first_Knowledge_thy = @{theory Delete} (*see WN120321.TODO rearrange theories*) |
16 val first_Knowledge_thy = @{theory Delete} (*see WN120321.TODO rearrange theories*) |
17 val allthys = (*!!! @{theory} :: ..START WITH Isac.thy..*) Theory.ancestors_of @{theory}; |
17 val allthys = (*!!! @{theory} :: ..START WITH Isac.thy..*) Theory.ancestors_of @{theory}; |
39 isabthys := isabthys'; |
39 isabthys := isabthys'; |
40 knowthys := knowthys'; |
40 knowthys := knowthys'; |
41 progthys := progthys'; |
41 progthys := progthys'; |
42 theory' := rev ((map Context.theory_name isacthys') ~~ isacthys'); (*WN120320 easy to remove*) |
42 theory' := rev ((map Context.theory_name isacthys') ~~ isacthys'); (*WN120320 easy to remove*) |
43 val rlsthmsNOTisac = gen_diff eq_thmI' (isacrlsthms, isacthms); |
43 val rlsthmsNOTisac = gen_diff eq_thmI' (isacrlsthms, isacthms); |
44 (*end;*) |
44 (*end;(*local*)*) |
45 (*WN120319: since num_str destoys derivation_name, we hardcode rlsthmsNOTisac: |
45 (*WN120319: since num_str destoys derivation_name, we hardcode rlsthmsNOTisac: |
46 see tests |
46 see tests |
47 --- OLD compute rlsthmsNOTisac by eq_thmID --- |
47 --- OLD compute rlsthmsNOTisac by eq_thmID --- |
48 --- compute val rlsthmsNOTisac --- |
48 --- compute val rlsthmsNOTisac --- |
49 for improvements (###sym_* etc) |
49 for improvements (###sym_* etc) |
107 |
107 |
108 (*.create the hierarchy of theory elements from IsacKnowledge |
108 (*.create the hierarchy of theory elements from IsacKnowledge |
109 including thms from Isabelle used in rls; |
109 including thms from Isabelle used in rls; |
110 elements store_*d in any *.thy are not overwritten.*) |
110 elements store_*d in any *.thy are not overwritten.*) |
111 |
111 |
112 thehier := the_hier (! thehier) (collect_thydata ()); |
112 (*========== inhibit exn WN130616: ME_Isa: thy 'Script' not in system =======*) |
|
113 thehier := the_hier (! thehier) (collect_thydata ()); (*ME_Isa: thy 'Script' not in system*) |
113 tracing("----------------------------------\n" ^ |
114 tracing("----------------------------------\n" ^ |
114 "*** insert: not found ... IS OK : \n" ^ |
115 "*** insert: not found ... IS OK : \n" ^ |
115 "comes from fill_parents \n" ^ |
116 "comes from fill_parents \n" ^ |
116 "----------------------------------\n"); |
117 "----------------------------------\n"); |
117 *} |
118 *} |
118 |
119 |
119 text {* interface for dialog-authoring *} |
120 text {* interface for dialog-authoring *} |
120 |
121 |
121 ML {* |
122 ML {* |
|
123 (*========== inhibit exn WN130616: |
|
124 get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"] ======= |
122 insert_errpats ["diff","differentiate_on_R"] |
125 insert_errpats ["diff","differentiate_on_R"] |
123 ([("chain-rule-diff-both", |
126 ([("chain-rule-diff-both", |
124 [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)", |
127 [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)", |
125 parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)", |
128 parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)", |
126 parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)", |
129 parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)", |
217 insert_errpatIDs ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"] |
220 insert_errpatIDs ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"] |
218 (["chain-rule-diff-both", "cancel"]: errpatID list); |
221 (["chain-rule-diff-both", "cancel"]: errpatID list); |
219 |
222 |
220 (* ...and all other related rls by hand; |
223 (* ...and all other related rls by hand; |
221 TODO: lift errpattIDs from theorems to respective rls AUTOMATICALLY *) |
224 TODO: lift errpattIDs from theorems to respective rls AUTOMATICALLY *) |
|
225 ========== inhibit exn WN130616: |
|
226 get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"] =======*) |
222 *} |
227 *} |
223 |
228 ML {*"test"*} |
224 end |
229 end |