257 end; |
257 end; |
258 |
258 |
259 |
259 |
260 (**** declare rules for converting predicates to sets ****) |
260 (**** declare rules for converting predicates to sets ****) |
261 |
261 |
262 fun add ctxt thm {to_set_simps, to_pred_simps, set_arities, pred_arities} = |
262 fun add ctxt thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) = |
263 case prop_of thm of |
263 case prop_of thm of |
264 Const ("Trueprop", _) $ (Const ("op =", Type (_, [T, _])) $ lhs $ rhs) => |
264 Const ("Trueprop", _) $ (Const ("op =", Type (_, [T, _])) $ lhs $ rhs) => |
265 (case body_type T of |
265 (case body_type T of |
266 Type ("bool", []) => |
266 Type ("bool", []) => |
267 let |
267 let |
282 | _ => error "member symbol on right-hand side expected") |
282 | _ => error "member symbol on right-hand side expected") |
283 | _ => (strip_comb rhs, NONE)) |
283 | _ => (strip_comb rhs, NONE)) |
284 in |
284 in |
285 case (name_type_of h, name_type_of h') of |
285 case (name_type_of h, name_type_of h') of |
286 (SOME (s, T), SOME (s', T')) => |
286 (SOME (s, T), SOME (s', T')) => |
287 (case Symtab.lookup set_arities s' of |
287 if exists (fn (U, _) => |
288 NONE => () |
288 Sign.typ_instance thy (T', U) andalso |
289 | SOME xs => if exists (fn (U, _) => |
289 Sign.typ_instance thy (U, T')) |
290 Sign.typ_instance thy (T', U) andalso |
290 (Symtab.lookup_list set_arities s') |
291 Sign.typ_instance thy (U, T')) xs |
291 then |
292 then |
292 (warning ("Ignoring conversion rule for operator " ^ s'); tab) |
293 error ("Clash of conversion rules for operator " ^ s') |
293 else |
294 else (); |
294 {to_set_simps = thm :: to_set_simps, |
295 {to_set_simps = thm :: to_set_simps, |
295 to_pred_simps = |
296 to_pred_simps = |
296 mk_to_pred_eq h fs fs' T' thm :: to_pred_simps, |
297 mk_to_pred_eq h fs fs' T' thm :: to_pred_simps, |
297 set_arities = Symtab.insert_list op = (s', |
298 set_arities = Symtab.insert_list op = (s', |
298 (T', (map (AList.lookup op = fs) ts', fs'))) set_arities, |
299 (T', (map (AList.lookup op = fs) ts', fs'))) set_arities, |
299 pred_arities = Symtab.insert_list op = (s, |
300 pred_arities = Symtab.insert_list op = (s, |
300 (T, (pfs, fs'))) pred_arities} |
301 (T, (pfs, fs'))) pred_arities}) |
|
302 | _ => error "set / predicate constant expected" |
301 | _ => error "set / predicate constant expected" |
303 end |
302 end |
304 | _ => error "equation between predicates expected") |
303 | _ => error "equation between predicates expected") |
305 | _ => error "equation expected"; |
304 | _ => error "equation expected"; |
306 |
305 |