14 val string_of_thm: thm -> string |
14 val string_of_thm: thm -> string |
15 val string_of_thms: thm list -> string |
15 val string_of_thms: thm list -> string |
16 |
16 |
17 (* required in ProgLang BEFORE definition in ---------------vvv *) |
17 (* required in ProgLang BEFORE definition in ---------------vvv *) |
18 val int_opt_of_string: string -> int option (* belongs to TermC *) |
18 val int_opt_of_string: string -> int option (* belongs to TermC *) |
19 val numerals_to_Free: thm -> thm (* belongs to ThmC *) |
|
20 val num_to_Free: term -> term (* belongs to TermC *) |
|
21 val uminus_to_string: term -> term (* belongs to TermC *) |
|
22 end |
19 end |
23 |
20 |
24 (**) |
21 (**) |
25 structure ThmC_Def(**): THEOREM_ISAC_DEF(**) = |
22 structure ThmC_Def(**): THEOREM_ISAC_DEF(**) = |
26 struct |
23 struct |
45 val (sign, istr) = case ss' of "-" :: istr => (~1, istr) | _ => (1, ss') |
42 val (sign, istr) = case ss' of "-" :: istr => (~1, istr) | _ => (1, ss') |
46 in |
43 in |
47 case Library.read_int istr of (i, []) => SOME (sign * i) | _ => NONE |
44 case Library.read_int istr of (i, []) => SOME (sign * i) | _ => NONE |
48 end; |
45 end; |
49 |
46 |
50 |
|
51 (** transform Isabelle's binary numerals to "Free (string, T)" **) |
|
52 |
|
53 val num_to_Free = (**)I(* Makarius 100308 *) |
|
54 (** ) |
|
55 let |
|
56 fun dest_num t = |
|
57 (case try HOLogic.dest_number t of |
|
58 SOME (T, i) => SOME (Free (signed_string_of_int i, T)) |
|
59 | NONE => NONE); |
|
60 fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b) |
|
61 | to_str (t as (u1 $ u2)) = |
|
62 (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2) |
|
63 | to_str t = perhaps dest_num t; |
|
64 in to_str end |
|
65 ( **) |
|
66 |
|
67 val uminus_to_string = (**)I |
|
68 (** ) |
|
69 let |
|
70 fun dest_num t = |
|
71 case t of |
|
72 (Const (\<^const_name>\<open>uminus\<close>, _) $ Free (s, T)) => |
|
73 (case int_opt_of_string s of |
|
74 SOME i => SOME (Free (signed_string_of_int (~1 * i), T)) |
|
75 | NONE => NONE) |
|
76 | _ => NONE; |
|
77 fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b) |
|
78 | to_str (t as (u1 $ u2)) = |
|
79 (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2) |
|
80 | to_str t = perhaps dest_num t; |
|
81 in to_str end; |
|
82 ( **) |
|
83 |
|
84 fun numerals_to_Free thm = (**)thm |
|
85 (** ) |
|
86 let |
|
87 val prop = Thm.plain_prop_of thm |
|
88 val prop' = num_to_Free prop; |
|
89 in |
|
90 if prop = prop' then thm |
|
91 else |
|
92 Skip_Proof.make_thm (Thm.theory_of_thm thm) prop' |
|
93 |> Thm.put_name_hint (Thm.get_name_hint thm) |
|
94 end; |
|
95 ( **) |
|
96 |
|
97 (**)end(**) |
47 (**)end(**) |