61 |
61 |
62 val (prems, rec_fns) = split_list (List.concat (snd (foldl_map |
62 val (prems, rec_fns) = split_list (List.concat (snd (foldl_map |
63 (fn (j, ((i, (_, _, constrs)), T)) => foldl_map (fn (j, (cname, cargs)) => |
63 (fn (j, ((i, (_, _, constrs)), T)) => foldl_map (fn (j, (cname, cargs)) => |
64 let |
64 let |
65 val Ts = map (typ_of_dtyp descr sorts) cargs; |
65 val Ts = map (typ_of_dtyp descr sorts) cargs; |
66 val tnames = variantlist (DatatypeProp.make_tnames Ts, pnames); |
66 val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts); |
67 val recs = List.filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts); |
67 val recs = List.filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts); |
68 val frees = tnames ~~ Ts; |
68 val frees = tnames ~~ Ts; |
69 |
69 |
70 fun mk_prems vs [] = |
70 fun mk_prems vs [] = |
71 let |
71 let |
169 val rT' = TVar (("'P", 0), HOLogic.typeS); |
169 val rT' = TVar (("'P", 0), HOLogic.typeS); |
170 |
170 |
171 fun make_casedist_prem T (cname, cargs) = |
171 fun make_casedist_prem T (cname, cargs) = |
172 let |
172 let |
173 val Ts = map (typ_of_dtyp descr sorts) cargs; |
173 val Ts = map (typ_of_dtyp descr sorts) cargs; |
174 val frees = variantlist |
174 val frees = Name.variant_list ["P", "y"] (DatatypeProp.make_tnames Ts) ~~ Ts; |
175 (DatatypeProp.make_tnames Ts, ["P", "y"]) ~~ Ts; |
|
176 val free_ts = map Free frees; |
175 val free_ts = map Free frees; |
177 val r = Free ("r" ^ NameSpace.base cname, Ts ---> rT) |
176 val r = Free ("r" ^ NameSpace.base cname, Ts ---> rT) |
178 in (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop |
177 in (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop |
179 (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))), |
178 (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))), |
180 HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ |
179 HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ |