48 end; |
48 end; |
49 |
49 |
50 |
50 |
51 (** transform Isabelle's binary numerals to "Free (string, T)" **) |
51 (** transform Isabelle's binary numerals to "Free (string, T)" **) |
52 |
52 |
53 val num_to_Free = (* Makarius 100308 *) |
53 val num_to_Free = (**)I(* Makarius 100308 *) |
|
54 (** ) |
54 let |
55 let |
55 fun dest_num t = |
56 fun dest_num t = |
56 (case try HOLogic.dest_number t of |
57 (case try HOLogic.dest_number t of |
57 SOME (T, i) => SOME (Free (signed_string_of_int i, T)) |
58 SOME (T, i) => SOME (Free (signed_string_of_int i, T)) |
58 | NONE => NONE); |
59 | NONE => NONE); |
59 fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b) |
60 fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b) |
60 | to_str (t as (u1 $ u2)) = |
61 | to_str (t as (u1 $ u2)) = |
61 (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2) |
62 (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2) |
62 | to_str t = perhaps dest_num t; |
63 | to_str t = perhaps dest_num t; |
63 in to_str end |
64 in to_str end |
|
65 ( **) |
64 |
66 |
65 val uminus_to_string = |
67 val uminus_to_string = (**)I |
|
68 (** ) |
66 let |
69 let |
67 fun dest_num t = |
70 fun dest_num t = |
68 case t of |
71 case t of |
69 (Const ("Groups.uminus_class.uminus", _) $ Free (s, T)) => |
72 (Const ("Groups.uminus_class.uminus", _) $ Free (s, T)) => |
70 (case int_opt_of_string s of |
73 (case int_opt_of_string s of |
74 fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b) |
77 fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b) |
75 | to_str (t as (u1 $ u2)) = |
78 | to_str (t as (u1 $ u2)) = |
76 (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2) |
79 (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2) |
77 | to_str t = perhaps dest_num t; |
80 | to_str t = perhaps dest_num t; |
78 in to_str end; |
81 in to_str end; |
|
82 ( **) |
79 |
83 |
80 fun numerals_to_Free thm = |
84 fun numerals_to_Free thm = (**)thm |
|
85 (** ) |
81 let |
86 let |
82 val prop = Thm.plain_prop_of thm |
87 val prop = Thm.plain_prop_of thm |
83 val prop' = num_to_Free prop; |
88 val prop' = num_to_Free prop; |
84 in |
89 in |
85 if prop = prop' then thm |
90 if prop = prop' then thm |
86 else |
91 else |
87 Skip_Proof.make_thm (Thm.theory_of_thm thm) prop' |
92 Skip_Proof.make_thm (Thm.theory_of_thm thm) prop' |
88 |> Thm.put_name_hint (Thm.get_name_hint thm) |
93 |> Thm.put_name_hint (Thm.get_name_hint thm) |
89 end; |
94 end; |
|
95 ( **) |
90 |
96 |
91 (**)end(**) |
97 (**)end(**) |