1 (* Title: CalcElements/thmC.sml |
|
2 Author: Walther Neuper |
|
3 (c) due to copyright terms |
|
4 |
|
5 TODO: use "ThmC" for renaming identifiers. |
|
6 Probably this structure can be dropped due to improvements of Isabelle. |
|
7 *) |
|
8 signature THEOREM_ISAC = |
|
9 sig |
|
10 (*datatype T = Rule_Def.Thm ..ERROR: cannot get out from Rule_Def.rule*) |
|
11 |
|
12 (*/------- to ThmC.sml ------\*) |
|
13 eqtype thmID |
|
14 type thm' |
|
15 type thm'' |
|
16 |
|
17 val thmID_of_derivation_name: string -> string |
|
18 val thmID_of_derivation_name': thm -> string |
|
19 val thm''_of_thm: thm -> thm'' |
|
20 val thm_of_thm: Rule_Def.rule -> thm |
|
21 |
|
22 val string_of_thmI: thm -> string |
|
23 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
|
24 val thm2str: thm -> string |
|
25 val thms2str : thm list -> string |
|
26 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
|
27 val string_of_thm: thm -> string |
|
28 val string_of_thm': theory -> thm -> string |
|
29 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
|
30 (*/------- to ThmC.sml ------\*) |
|
31 val id_of_thm: Rule_Def.rule -> string |
|
32 (*\------- to ThmC.sml ------/*) |
|
33 end |
|
34 |
|
35 (**) |
|
36 structure ThmC(**): THEOREM_ISAC(**) = |
|
37 struct |
|
38 (**) |
|
39 |
|
40 (*datatype T = Rule_Def.Thm ..ERROR: cannot get out from Rule_Def.rule*) |
|
41 |
|
42 (* TODO CLEANUP Thm: |
|
43 Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end; |
|
44 (b) investigate if ""RS sym" attaches a [.]" still occurs: ThmC.string_of_thmI |
|
45 thmID : type for data from user input + program |
|
46 thmDeriv : type for thy_hierarchy ONLY |
|
47 obsolete types : thm' (SEE "ad thm'"), thm''. |
|
48 revise funs : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm. |
|
49 activate : thmID_of_derivation_name' |
|
50 *) |
|
51 type thmID = string; (* identifier for a thm (the shortest possible identifier) *) |
|
52 type thm' = thmID * UnparseC.cterm';(*WN060610 deprecated in favour of thm''; WN180324: used in TODO review: |
|
53 val thm'2xml : int -> ThmC.thm' -> Celem.xml |
|
54 val assoc_thm': theory -> ThmC.thm' -> thm |
|
55 | Calculate' of ThyC.theory' * string * term * (term * ThmC.thm') |
|
56 *) |
|
57 (* tricky combination of (string, term) for theorems in Isac: |
|
58 * case 1 general: frontend + lucin, e.g. applicable_in..Rewrite: (thmID, _) --> (thmID, thm) |
|
59 by Global_Theory.get_thm, special cases ("add_commute",..) see convert_metaview_to_thmid. |
|
60 * case 2 "sym_..": Global_Theory.get_thm..RS sym |
|
61 * case 3 ad-hoc thm "#..." mk_thm from ad-hoc term (numerals only) in calculate_: |
|
62 from applicable_in..Calculate: opstr --calculate_/adhoc_thm--> (thmID, thm) |
|
63 *) |
|
64 type thm'' = thmID * thm; (* only for transport via libisabelle isac-java <--- ME *) |
|
65 |
|
66 fun thm2str thm = |
|
67 let |
|
68 val t = Thm.prop_of thm |
|
69 val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge")) |
|
70 val ctxt' = Config.put show_markup false ctxt |
|
71 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end; |
|
72 fun thms2str thms = (strs2str o (map thm2str)) thms |
|
73 |
|
74 (*check for [.] as caused by "fun assoc_thm'"*) |
|
75 fun string_of_thm thm = UnparseC.term_to_string' (ThyC.thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm) |
|
76 fun string_of_thm' thy thm = UnparseC.term_to_string' (ThyC.thy2ctxt thy) (Thm.prop_of thm) |
|
77 fun string_of_thmI thm = |
|
78 let |
|
79 val str = (de_quote o string_of_thm) thm |
|
80 val (a, b) = split_nlast (5, Symbol.explode str) |
|
81 in |
|
82 case b of |
|
83 [" ", " ","[", ".", "]"] => implode a |
|
84 | _ => str |
|
85 end |
|
86 |
|
87 fun id_of_thm (Rule_Def.Thm (id, _)) = id (* TODO re-arrange code for rule2str *) |
|
88 | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ rule2str r *)) |
|
89 |
|
90 fun thmID_of_derivation_name dn = last_elem (space_explode "." dn); |
|
91 fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm |
|
92 fun thyID_of_derivation_name dn = hd (space_explode "." dn); |
|
93 fun thm_of_thm (Rule_Def.Thm (_, thm)) = thm (* TODO re-arrange code for rule2str *) |
|
94 | thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ rule2str r *)) |
|
95 fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : thm'' |
|
96 |
|
97 (**)end(**) |
|