equal
deleted
inserted
replaced
119 |
119 |
120 A = B ----> (R ===> R) A B |
120 A = B ----> (R ===> R) A B |
121 |
121 |
122 for more complicated types of A and B |
122 for more complicated types of A and B |
123 *) |
123 *) |
|
124 |
|
125 (* instantiates TVars so that the term is of type ty *) |
|
126 fun force_typ thy trm ty = |
|
127 let |
|
128 val trm_ty = fastype_of trm |
|
129 val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty |
|
130 in |
|
131 map_types (Envir.subst_type ty_inst) trm |
|
132 end |
124 |
133 |
125 (* builds the aggregate equivalence relation *) |
134 (* builds the aggregate equivalence relation *) |
126 (* that will be the argument of Respects *) |
135 (* that will be the argument of Respects *) |
127 fun mk_resp_arg ctxt (rty, qty) = |
136 fun mk_resp_arg ctxt (rty, qty) = |
128 let |
137 let |
145 else |
154 else |
146 let |
155 let |
147 val SOME qinfo = quotdata_lookup_thy thy s' |
156 val SOME qinfo = quotdata_lookup_thy thy s' |
148 (* FIXME: check in this case that the rty and qty *) |
157 (* FIXME: check in this case that the rty and qty *) |
149 (* FIXME: correspond to each other *) |
158 (* FIXME: correspond to each other *) |
150 val (s, _) = dest_Const (#rel qinfo) |
159 |
151 (* FIXME: the relation should only be the string *) |
160 (* we need to instantiate the TVars in the relation *) |
152 (* FIXME: and the type needs to be calculated as below; *) |
161 val thy = ProofContext.theory_of ctxt |
153 (* FIXME: maybe one should actually have a term *) |
162 val forced_rel = force_typ thy (#rel qinfo) (rty --> rty --> @{typ bool}) |
154 (* FIXME: and one needs to force it to have this type *) |
|
155 in |
163 in |
156 Const (s, rty --> rty --> @{typ bool}) |
164 forced_rel |
157 end |
165 end |
158 | _ => HOLogic.eq_const dummyT |
166 | _ => HOLogic.eq_const rty |
159 (* FIXME: check that the types correspond to each other? *) |
167 (* FIXME: check that the types correspond to each other? *) |
160 end |
168 end |
161 |
169 |
162 val mk_babs = Const (@{const_name Babs}, dummyT) |
170 val mk_babs = Const (@{const_name Babs}, dummyT) |
163 val mk_ball = Const (@{const_name Ball}, dummyT) |
171 val mk_ball = Const (@{const_name Ball}, dummyT) |