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