author | wneuper <Walther.Neuper@jku.at> |
Wed, 11 Jan 2023 11:38:01 +0100 | |
changeset 60650 | 06ec8abfd3bc |
parent 60648 | 976b99bcfc96 |
permissions | -rw-r--r-- |
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@60650 | 6 |
Here is a minimum of code required for theory Know_Store, |
walther@59919 | 7 |
further code see structure ThmC. |
walther@59858 | 8 |
*) |
walther@59865 | 9 |
signature THEOREM_ISAC_DEF = |
walther@59858 | 10 |
sig |
walther@59874 | 11 |
type T |
walther@59874 | 12 |
eqtype id |
walther@59861 | 13 |
|
Walther@60648 | 14 |
val string_of_thm: Proof.context -> thm -> string |
Walther@60648 | 15 |
val string_of_thms: Proof.context -> 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@59858 | 19 |
end |
walther@59858 | 20 |
|
walther@59858 | 21 |
(**) |
walther@59865 | 22 |
structure ThmC_Def(**): THEOREM_ISAC_DEF(**) = |
walther@59858 | 23 |
struct |
walther@59858 | 24 |
(**) |
walther@59858 | 25 |
|
walther@59887 | 26 |
type id = string; (* key into Know_Store, without point *) |
walther@59874 | 27 |
type T = id * Thm.thm; |
walther@59861 | 28 |
|
Walther@60648 | 29 |
fun string_of_thm ctxt thm = |
Walther@60592 | 30 |
let |
Walther@60592 | 31 |
val t = Thm.prop_of thm |
Walther@60592 | 32 |
val ctxt' = Config.put show_markup false ctxt |
Walther@60592 | 33 |
in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end; |
Walther@60648 | 34 |
fun string_of_thms ctxt thms = (strs2str o (map (string_of_thm ctxt))) thms |
walther@59861 | 35 |
|
walther@59875 | 36 |
fun int_opt_of_string str = |
walther@59871 | 37 |
let |
walther@59871 | 38 |
val ss = Symbol.explode str |
walther@59871 | 39 |
val ss' = case ss of "(" :: s => drop_last s | _ => ss |
walther@59871 | 40 |
val (sign, istr) = case ss' of "-" :: istr => (~1, istr) | _ => (1, ss') |
walther@59871 | 41 |
in |
walther@59871 | 42 |
case Library.read_int istr of (i, []) => SOME (sign * i) | _ => NONE |
walther@59871 | 43 |
end; |
walther@59871 | 44 |
|
walther@59858 | 45 |
(**)end(**) |