471 val (defs, lthy2) = lthy1 |
471 val (defs, lthy2) = lthy1 |
472 |> fold_map Local_Theory.define |
472 |> fold_map Local_Theory.define |
473 (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []), |
473 (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []), |
474 fold_rev lambda params (HOLogic.Collect_const U $ |
474 fold_rev lambda params (HOLogic.Collect_const U $ |
475 HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3)))))) |
475 HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3)))))) |
476 (cnames_syn ~~ cs_info ~~ preds)) |
476 (cnames_syn ~~ cs_info ~~ preds)); |
477 ||> Proof_Context.restore_naming lthy1; |
|
478 |
477 |
479 (* prove theorems for converting predicate to set notation *) |
478 (* prove theorems for converting predicate to set notation *) |
480 val lthy3 = fold |
479 val lthy3 = fold |
481 (fn (((p, c as Free (s, _)), (fs, U, Ts)), (_, (_, def))) => fn lthy => |
480 (fn (((p, c as Free (s, _)), (fs, U, Ts)), (_, (_, def))) => fn lthy => |
482 let val conv_thm = |
481 let val conv_thm = |