equal
deleted
inserted
replaced
68 val tnames = make_tnames Ts; |
68 val tnames = make_tnames Ts; |
69 val frees = map Free (tnames ~~ Ts); |
69 val frees = map Free (tnames ~~ Ts); |
70 val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts); |
70 val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts); |
71 in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq |
71 in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq |
72 (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')), |
72 (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')), |
73 foldr1 (HOLogic.mk_binop @{const_name "op &"}) |
73 foldr1 (HOLogic.mk_binop @{const_name HOL.conj}) |
74 (map HOLogic.mk_eq (frees ~~ frees'))))) |
74 (map HOLogic.mk_eq (frees ~~ frees'))))) |
75 end; |
75 end; |
76 in |
76 in |
77 map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) []) |
77 map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) []) |
78 (hd descr) (take (length (hd descr)) (get_rec_types descr' sorts)) |
78 (hd descr) (take (length (hd descr)) (get_rec_types descr' sorts)) |
147 end; |
147 end; |
148 |
148 |
149 val prems = maps (fn ((i, (_, _, constrs)), T) => |
149 val prems = maps (fn ((i, (_, _, constrs)), T) => |
150 map (make_ind_prem i T) constrs) (descr' ~~ recTs); |
150 map (make_ind_prem i T) constrs) (descr' ~~ recTs); |
151 val tnames = make_tnames recTs; |
151 val tnames = make_tnames recTs; |
152 val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"}) |
152 val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj}) |
153 (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T)) |
153 (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T)) |
154 (descr' ~~ recTs ~~ tnames))) |
154 (descr' ~~ recTs ~~ tnames))) |
155 |
155 |
156 in Logic.list_implies (prems, concl) end; |
156 in Logic.list_implies (prems, concl) end; |
157 |
157 |