111 fun make_ind_prem k T (cname, cargs) = |
111 fun make_ind_prem k T (cname, cargs) = |
112 let |
112 let |
113 fun mk_prem ((DtRec k, s), T) = HOLogic.mk_Trueprop |
113 fun mk_prem ((DtRec k, s), T) = HOLogic.mk_Trueprop |
114 (make_pred k T $ Free (s, T)) |
114 (make_pred k T $ Free (s, T)) |
115 | mk_prem ((DtType ("fun", [_, DtRec k]), s), T' as Type ("fun", [T, U])) = |
115 | mk_prem ((DtType ("fun", [_, DtRec k]), s), T' as Type ("fun", [T, U])) = |
116 HOLogic.mk_Trueprop (HOLogic.all_const T $ |
116 (Const (InductivePackage.inductive_forall_name, |
117 Abs ("x", T, make_pred k U $ (Free (s, T') $ Bound 0))); |
117 [T --> HOLogic.boolT] ---> HOLogic.boolT) $ |
|
118 Abs ("x", T, make_pred k U $ (Free (s, T') $ Bound 0))) |> HOLogic.mk_Trueprop; |
118 |
119 |
119 val recs = filter is_rec_type cargs; |
120 val recs = filter is_rec_type cargs; |
120 val Ts = map (typ_of_dtyp descr' sorts) cargs; |
121 val Ts = map (typ_of_dtyp descr' sorts) cargs; |
121 val recTs' = map (typ_of_dtyp descr' sorts) recs; |
122 val recTs' = map (typ_of_dtyp descr' sorts) recs; |
122 val tnames = variantlist (make_tnames Ts, pnames); |
123 val tnames = variantlist (make_tnames Ts, pnames); |