486 coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono} |
486 coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono} |
487 cs' intros' monos' params1 cnames_syn' lthy; |
487 cs' intros' monos' params1 cnames_syn' lthy; |
488 |
488 |
489 (* define inductive sets using previously defined predicates *) |
489 (* define inductive sets using previously defined predicates *) |
490 val (defs, lthy2) = lthy1 |
490 val (defs, lthy2) = lthy1 |
491 |> Local_Theory.concealed (* FIXME ?? *) |
491 |> Proof_Context.concealed (* FIXME ?? *) |
492 |> fold_map Local_Theory.define |
492 |> fold_map Local_Theory.define |
493 (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []), |
493 (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []), |
494 fold_rev lambda params (HOLogic.Collect_const U $ |
494 fold_rev lambda params (HOLogic.Collect_const U $ |
495 HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3)))))) |
495 HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3)))))) |
496 (cnames_syn ~~ cs_info ~~ preds)) |
496 (cnames_syn ~~ cs_info ~~ preds)) |
497 ||> Local_Theory.restore_naming lthy1; |
497 ||> Proof_Context.restore_naming lthy1; |
498 |
498 |
499 (* prove theorems for converting predicate to set notation *) |
499 (* prove theorems for converting predicate to set notation *) |
500 val lthy3 = fold |
500 val lthy3 = fold |
501 (fn (((p, c as Free (s, _)), (fs, U, Ts)), (_, (_, def))) => fn lthy => |
501 (fn (((p, c as Free (s, _)), (fs, U, Ts)), (_, (_, def))) => fn lthy => |
502 let val conv_thm = |
502 let val conv_thm = |