equal
deleted
inserted
replaced
75 (*** Prove the simultaneous induction rule ***) |
75 (*** Prove the simultaneous induction rule ***) |
76 |
76 |
77 (*Make distinct predicates for each inductive set*) |
77 (*Make distinct predicates for each inductive set*) |
78 |
78 |
79 (*Sigmas and Cartesian products may nest ONLY to the right!*) |
79 (*Sigmas and Cartesian products may nest ONLY to the right!*) |
80 fun mk_pred_typ (t $ A $ B) = |
80 fun mk_pred_typ (t $ A $ Abs(_,_,B)) = |
81 if t = Pr.sigma then iT --> mk_pred_typ B |
81 if t = Pr.sigma then iT --> mk_pred_typ B |
82 else iT --> oT |
82 else iT --> oT |
83 | mk_pred_typ _ = iT --> oT |
83 | mk_pred_typ _ = iT --> oT |
84 |
84 |
85 (*Given a recursive set and its domain, return the "fsplit" predicate |
85 (*Given a recursive set and its domain, return the "fsplit" predicate |