equal
deleted
inserted
replaced
122 fun mk_argT (T, (_, (co, contra))) = |
122 fun mk_argT (T, (_, (co, contra))) = |
123 replicate (bool_num co + bool_num contra) (T --> T) |
123 replicate (bool_num co + bool_num contra) (T --> T) |
124 val Ts' = maps mk_argT (Ts ~~ variances) |
124 val Ts' = maps mk_argT (Ts ~~ variances) |
125 val T = Type (tyco, Ts); |
125 val T = Type (tyco, Ts); |
126 val lhs = list_comb (Const (mapper, Ts' ---> T --> T), |
126 val lhs = list_comb (Const (mapper, Ts' ---> T --> T), |
127 map (HOLogic.mk_id o domain_type) Ts'); |
127 map (HOLogic.id_const o domain_type) Ts'); |
128 in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, HOLogic.mk_id T) end; |
128 in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, HOLogic.id_const T) end; |
129 |
129 |
130 val comp_apply = Simpdata.mk_eq @{thm o_apply}; |
130 val comp_apply = Simpdata.mk_eq @{thm o_apply}; |
131 val id_def = Simpdata.mk_eq @{thm id_def}; |
131 val id_def = Simpdata.mk_eq @{thm id_def}; |
132 |
132 |
133 fun make_compositionality ctxt thm = |
133 fun make_compositionality ctxt thm = |