equal
deleted
inserted
replaced
17 val string_of_thms: thm list -> string |
17 val string_of_thms: thm list -> string |
18 val id_of_thm: thm -> id |
18 val id_of_thm: thm -> id |
19 val of_thm: thm -> T |
19 val of_thm: thm -> T |
20 val from_rule : Rule.rule -> T |
20 val from_rule : Rule.rule -> T |
21 val member': id list -> Rule.rule -> bool |
21 val member': id list -> Rule.rule -> bool |
22 |
|
23 val numerals_to_Free: thm -> thm |
|
24 |
22 |
25 val is_sym: id -> bool |
23 val is_sym: id -> bool |
26 val thm_from_thy: theory -> ThmC_Def.id -> thm |
24 val thm_from_thy: theory -> ThmC_Def.id -> thm |
27 |
25 |
28 val revert_sym_rule: theory -> Rule.rule -> Rule.rule |
26 val revert_sym_rule: theory -> Rule.rule -> Rule.rule |
65 \<close> |
63 \<close> |
66 fun member' thmIDs thm = (member op = thmIDs (Rule.thm_id thm)) |
64 fun member' thmIDs thm = (member op = thmIDs (Rule.thm_id thm)) |
67 handle ERROR _ => false |
65 handle ERROR _ => false |
68 |
66 |
69 |
67 |
70 (** convert Isabelle's numerals to ISAC's specific format, LEGACY **) |
|
71 |
|
72 val numerals_to_Free = ThmC_Def.numerals_to_Free; (* numeral \<rightarrow> Free ("int", T) *) |
|
73 |
|
74 |
|
75 (** handle symmetric equalities, generated by deriving input terms **) |
68 (** handle symmetric equalities, generated by deriving input terms **) |
76 |
69 |
77 fun is_sym id = |
70 fun is_sym id = |
78 case Symbol.explode id of "s" :: "y" :: "m" :: "_" :: _ => true |
71 case Symbol.explode id of "s" :: "y" :: "m" :: "_" :: _ => true |
79 | _ => false; |
72 | _ => false; |
89 fun thm_from_thy thy thmid = |
82 fun thm_from_thy thy thmid = |
90 case Symbol.explode thmid of |
83 case Symbol.explode thmid of |
91 "s" :: "y" :: "m" :: "_" :: "#" :: _ => |
84 "s" :: "y" :: "m" :: "_" :: "#" :: _ => |
92 raise ERROR ("thm_from_thy not impl.for " ^ thmid) |
85 raise ERROR ("thm_from_thy not impl.for " ^ thmid) |
93 | "s" :: "y" :: "m" :: "_" :: id => |
86 | "s" :: "y" :: "m" :: "_" :: id => |
94 ((numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym |
87 ((Global_Theory.get_thm thy) (implode id)) RS sym |
95 | "#" :: _ => |
88 | "#" :: _ => |
96 raise ERROR ("thm_from_thy not impl.for " ^ thmid) |
89 raise ERROR ("thm_from_thy not impl.for " ^ thmid) |
97 | _ => |
90 | _ => |
98 thmid |> Global_Theory.get_thm thy |> numerals_to_Free |
91 thmid |> Global_Theory.get_thm thy |
99 |
92 |
100 fun dest_eq_concl thm = |
93 fun dest_eq_concl thm = |
101 (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) thm of |
94 (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) thm of |
102 NONE => raise THM ("dest_eq_concl: conclusion needs to be HOL equality", 0, [thm]) |
95 NONE => raise THM ("dest_eq_concl: conclusion needs to be HOL equality", 0, [thm]) |
103 | SOME eq => eq); |
96 | SOME eq => eq); |
177 val {name, dynamic, thms, ...} = Facts.retrieve context facts (xname, pos); |
170 val {name, dynamic, thms, ...} = Facts.retrieve context facts (xname, pos); |
178 val thm = |
171 val thm = |
179 if dynamic then error ("Bad dynamic fact " ^ quote name ^ Position.here pos) |
172 if dynamic then error ("Bad dynamic fact " ^ quote name ^ Position.here pos) |
180 else Facts.the_single (name, pos) thms; |
173 else Facts.the_single (name, pos) thms; |
181 val (xname', thm') = if symmetric then (sym_prefix ^ xname, thm RS sym) else (xname, thm); |
174 val (xname', thm') = if symmetric then (sym_prefix ^ xname, thm RS sym) else (xname, thm); |
182 in Rule.Thm (xname', numerals_to_Free thm') end; |
175 in Rule.Thm (xname', thm') end; |
183 |
176 |
184 fun antiquotation binding sym = |
177 fun antiquotation binding sym = |
185 ML_Antiquotation.value_embedded binding |
178 ML_Antiquotation.value_embedded binding |
186 (Scan.lift Args.embedded_position >> (fn name => |
179 (Scan.lift Args.embedded_position >> (fn name => |
187 "ThmC.make_rule ML_context " ^ Bool.toString sym ^ |
180 "ThmC.make_rule ML_context " ^ Bool.toString sym ^ |