278 val names = Term.add_free_names rhs [] |
278 val names = Term.add_free_names rhs [] |
279 in flatten thy lookup_pred rhs (names, []) |
279 in flatten thy lookup_pred rhs (names, []) |
280 |> map (fn (resultt, (_, prems)) => |
280 |> map (fn (resultt, (_, prems)) => |
281 Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt])))) |
281 Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt])))) |
282 end |
282 end |
283 val intr_ts = maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss)) |
283 val intr_tss = map mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss)) |
284 val (intrs, thy') = thy |
284 val (intrs, thy') = thy |
285 |> Sign.add_consts_i |
285 |> Sign.add_consts_i |
286 (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn)) |
286 (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn)) |
287 dst_preds) |
287 dst_preds) |
288 |> fold_map Specification.axiom |
288 |> fold_map Specification.axiom |
289 (map_index (fn (j, (predname, t)) => |
289 (map_index (fn (j, (predname, t)) => |
290 ((Binding.name (Long_Name.base_name predname ^ "_intro_" ^ string_of_int (j + 1)), []), t)) |
290 ((Binding.name (Long_Name.base_name predname ^ "_intro_" ^ string_of_int (j + 1)), []), t)) |
291 (prednames ~~ intr_ts)) |
291 (maps (uncurry (map o pair)) (prednames ~~ intr_tss))) |
292 val specs = map (fn predname => (predname, |
292 val specs = map (fn predname => (predname, |
293 map Drule.export_without_context (filter (Predicate_Compile_Aux.is_intro predname) intrs))) |
293 map Drule.export_without_context (filter (Predicate_Compile_Aux.is_intro predname) intrs))) |
294 dst_prednames |
294 dst_prednames |
295 val thy'' = Fun_Pred.map |
295 val thy'' = Fun_Pred.map |
296 (fold Item_Net.update (map (pairself Logic.varify_global) |
296 (fold Item_Net.update (map (pairself Logic.varify_global) |