159 val rhs_of = dest_equals_rhs o Thm.cprop_of; |
159 val rhs_of = dest_equals_rhs o Thm.cprop_of; |
160 |
160 |
161 |
161 |
162 (* thm order: ignores theory context! *) |
162 (* thm order: ignores theory context! *) |
163 |
163 |
164 fun thm_ord (th1, th2) = |
164 fun thm_ord ths = |
165 let |
165 (case Term_Ord.fast_term_ord (apply2 Thm.prop_of ths) of |
166 val {shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = Thm.rep_thm th1; |
166 EQUAL => |
167 val {shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = Thm.rep_thm th2; |
167 (case |
168 in |
168 list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) |
169 (case Term_Ord.fast_term_ord (prop1, prop2) of |
169 (apply2 Thm.tpairs_of ths) |
170 EQUAL => |
170 of |
171 (case list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) (tpairs1, tpairs2) of |
171 EQUAL => |
172 EQUAL => |
172 (case list_ord Term_Ord.fast_term_ord (apply2 Thm.hyps_of ths) of |
173 (case list_ord Term_Ord.fast_term_ord (hyps1, hyps2) of |
173 EQUAL => list_ord Term_Ord.sort_ord (apply2 Thm.shyps_of ths) |
174 EQUAL => list_ord Term_Ord.sort_ord (shyps1, shyps2) |
174 | ord => ord) |
175 | ord => ord) |
175 | ord => ord) |
176 | ord => ord) |
176 | ord => ord); |
177 | ord => ord) |
|
178 end; |
|
179 |
177 |
180 |
178 |
181 (* tables and caches *) |
179 (* tables and caches *) |
182 |
180 |
183 structure Ctermtab = Table(type key = cterm val ord = Term_Ord.fast_term_ord o apply2 Thm.term_of); |
181 structure Ctermtab = Table(type key = cterm val ord = Term_Ord.fast_term_ord o apply2 Thm.term_of); |
238 |
236 |
239 fun plain_prop_of raw_thm = |
237 fun plain_prop_of raw_thm = |
240 let |
238 let |
241 val thm = Thm.strip_shyps raw_thm; |
239 val thm = Thm.strip_shyps raw_thm; |
242 fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]); |
240 fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]); |
243 val {hyps, prop, tpairs, ...} = Thm.rep_thm thm; |
|
244 in |
241 in |
245 if not (null hyps) then |
242 if not (null (Thm.hyps_of thm)) then |
246 err "theorem may not contain hypotheses" |
243 err "theorem may not contain hypotheses" |
247 else if not (null (Thm.extra_shyps thm)) then |
244 else if not (null (Thm.extra_shyps thm)) then |
248 err "theorem may not contain sort hypotheses" |
245 err "theorem may not contain sort hypotheses" |
249 else if not (null tpairs) then |
246 else if not (null (Thm.tpairs_of thm)) then |
250 err "theorem may not contain flex-flex pairs" |
247 err "theorem may not contain flex-flex pairs" |
251 else prop |
248 else Thm.prop_of thm |
252 end; |
249 end; |
253 |
250 |
254 |
251 |
255 (* collections of theorems in canonical order *) |
252 (* collections of theorems in canonical order *) |
256 |
253 |