1 (* Title: BaseDefinitions/thmC-def.sml
3 (c) due to copyright terms
5 Probably this structure can be dropped due to improved reflection in Isabelle.
7 signature THEOREM_ISAC_DEF =
13 val id_of_thm: Rule_Def.rule -> string
14 val string_of_thmI: thm -> string
15 val thmID_of_derivation_name: string -> string
16 val thmID_of_derivation_name': thm -> string
17 val thm''_of_thm: thm -> thm''
18 val thm_of_thm: Rule_Def.rule -> thm
20 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
21 val thm2str: thm -> string
22 val thms2str : thm list -> string
23 val string_of_thm': theory -> thm -> string
24 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
25 val string_of_thm: thm -> string
26 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
30 structure ThmC_Def(**): THEOREM_ISAC_DEF(**) =
35 Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end;
36 (b) investigate if ""RS sym" attaches a [.]" still occurs: ThmC_Def.string_of_thmI
37 thmID : type for data from user input + program
38 thmDeriv : type for thy_hierarchy ONLY
39 obsolete types : thm' (SEE "ad thm'"), thm''.
40 revise funs : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm.
41 activate : thmID_of_derivation_name'
43 type thmID = string; (* identifier for a thm (the shortest possible identifier) *)
45 ad thm': there are two kinds of theorems ...
46 (1) defined in isabelle
47 (2) not known, eg. calc_thm, instantiated rls
48 the latter have a thmid "#..."
49 and thus outside isa we ALWAYS transport both (thmID, ThmC_Def.string_of_thmI)
50 and have a special assoc_thm / assoc_rls in this interface
52 type thm' = thmID * UnparseC.term_as_string;(*WN060610 deprecated in favour of thm''; WN180324: used in TODO review:
53 val thm'2xml : int -> ThmC_Def.thm' -> Celem.xml
54 val assoc_thm': theory -> ThmC_Def.thm' -> thm
55 | Calculate' of ThyC.theory' * string * term * (term * ThmC_Def.thm')
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)
64 type thm'' = thmID * thm; (* only for transport via libisabelle isac-java <--- ME *)
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
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 =
79 val str = (de_quote o string_of_thm) thm
80 val (a, b) = split_nlast (5, Symbol.explode str)
83 [" ", " ","[", ".", "]"] => implode a
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 *))
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 thm_of_thm (Rule_Def.Thm (_, thm)) = thm (* TODO re-arrange code for rule2str *)
93 | thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ rule2str r *))
94 fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : thm''