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@59874
|
9 |
type T
|
walther@59874
|
10 |
eqtype id
|
walther@59861
|
11 |
|
walther@59875
|
12 |
val make_thm: theory -> term -> thm (* required for Calculate.thy *)
|
walther@59861
|
13 |
|
walther@59875
|
14 |
val string_of_thm: thm -> string
|
walther@59875
|
15 |
val string_of_thms: thm list -> string
|
walther@59871
|
16 |
|
walther@59875
|
17 |
(* required in ProgLang BEFORE definition in ---------------vvv *)
|
walther@59875
|
18 |
val int_opt_of_string: string -> int option (* belongs to TermC *)
|
walther@59875
|
19 |
val numerals_to_Free: thm -> thm (* belongs to ThmC *)
|
walther@59875
|
20 |
val num_to_Free: term -> term (* belongs to TermC *)
|
walther@59875
|
21 |
val uminus_to_string: term -> term (* belongs to TermC *)
|
walther@59874
|
22 |
|
walther@59858
|
23 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
walther@59874
|
24 |
(*NONE*)
|
walther@59858
|
25 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
walther@59874
|
26 |
(*NONE*)
|
walther@59858
|
27 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
walther@59858
|
28 |
end
|
walther@59858
|
29 |
|
walther@59858
|
30 |
(**)
|
walther@59865
|
31 |
structure ThmC_Def(**): THEOREM_ISAC_DEF(**) =
|
walther@59858
|
32 |
struct
|
walther@59858
|
33 |
(**)
|
walther@59858
|
34 |
|
walther@59874
|
35 |
type id = string; (* key into KEStore, without point *)
|
walther@59874
|
36 |
type T = id * Thm.thm;
|
walther@59861
|
37 |
|
walther@59875
|
38 |
fun make_thm thy t = Thm.make_thm (Thm.global_cterm_of thy t);
|
walther@59858
|
39 |
|
walther@59875
|
40 |
fun string_of_thm thm =
|
walther@59874
|
41 |
let
|
walther@59874
|
42 |
val t = Thm.prop_of thm
|
walther@59874
|
43 |
val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))
|
walther@59874
|
44 |
val ctxt' = Config.put show_markup false ctxt
|
walther@59874
|
45 |
in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
|
walther@59875
|
46 |
fun string_of_thms thms = (strs2str o (map string_of_thm)) thms
|
walther@59861
|
47 |
|
walther@59875
|
48 |
fun int_opt_of_string str =
|
walther@59871
|
49 |
let
|
walther@59871
|
50 |
val ss = Symbol.explode str
|
walther@59871
|
51 |
val ss' = case ss of "(" :: s => drop_last s | _ => ss
|
walther@59871
|
52 |
val (sign, istr) = case ss' of "-" :: istr => (~1, istr) | _ => (1, ss')
|
walther@59871
|
53 |
in
|
walther@59871
|
54 |
case Library.read_int istr of (i, []) => SOME (sign * i) | _ => NONE
|
walther@59871
|
55 |
end;
|
walther@59871
|
56 |
|
walther@59871
|
57 |
|
walther@59874
|
58 |
(** transform Isabelle's binary numerals to "Free (string, T)" **)
|
walther@59874
|
59 |
|
walther@59875
|
60 |
val num_to_Free = (* Makarius 100308 *)
|
walther@59871
|
61 |
let
|
walther@59871
|
62 |
fun dest_num t =
|
walther@59871
|
63 |
(case try HOLogic.dest_number t of
|
walther@59872
|
64 |
SOME (T, i) => SOME (Free (signed_string_of_int i, T))
|
walther@59871
|
65 |
| NONE => NONE);
|
walther@59871
|
66 |
fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b)
|
walther@59871
|
67 |
| to_str (t as (u1 $ u2)) =
|
walther@59872
|
68 |
(case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2)
|
walther@59871
|
69 |
| to_str t = perhaps dest_num t;
|
walther@59871
|
70 |
in to_str end
|
walther@59875
|
71 |
|
walther@59871
|
72 |
val uminus_to_string =
|
walther@59871
|
73 |
let
|
walther@59871
|
74 |
fun dest_num t =
|
walther@59871
|
75 |
case t of
|
walther@59871
|
76 |
(Const ("Groups.uminus_class.uminus", _) $ Free (s, T)) =>
|
walther@59875
|
77 |
(case int_opt_of_string s of
|
walther@59871
|
78 |
SOME i => SOME (Free (signed_string_of_int (~1 * i), T))
|
walther@59871
|
79 |
| NONE => NONE)
|
walther@59871
|
80 |
| _ => NONE;
|
walther@59871
|
81 |
fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b)
|
walther@59871
|
82 |
| to_str (t as (u1 $ u2)) =
|
walther@59871
|
83 |
(case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2)
|
walther@59871
|
84 |
| to_str t = perhaps dest_num t;
|
walther@59871
|
85 |
in to_str end;
|
walther@59875
|
86 |
|
walther@59871
|
87 |
fun numerals_to_Free thm =
|
walther@59871
|
88 |
let
|
walther@59871
|
89 |
val (deriv,
|
walther@59871
|
90 |
{cert = cert, tags = tags, maxidx = maxidx, shyps = shyps,
|
walther@59871
|
91 |
hyps = hyps, tpairs = tpairs, prop = prop}) = Thm.rep_thm_G thm
|
walther@59875
|
92 |
val prop' = num_to_Free prop;
|
walther@59871
|
93 |
in Thm.assbl_thm deriv cert tags maxidx shyps hyps tpairs prop' end;
|
walther@59871
|
94 |
|
walther@59858
|
95 |
(**)end(**)
|