equal
deleted
inserted
replaced
143 case (rty, qty) of |
143 case (rty, qty) of |
144 (Type (s, tys), Type (s', tys')) => |
144 (Type (s, tys), Type (s', tys')) => |
145 if s = s' |
145 if s = s' |
146 then |
146 then |
147 let |
147 let |
148 val exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s ^ ")") |
148 val exc = LIFT_MATCH ("mk_resp_arg (no relation map function found for type " ^ s ^ ")") |
149 val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exc |
149 val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exc |
150 val args = map (mk_resp_arg ctxt) (tys ~~ tys') |
150 val args = map (mk_resp_arg ctxt) (tys ~~ tys') |
151 in |
151 in |
152 list_comb (Const (relmap, dummyT), args) |
152 list_comb (Const (relmap, dummyT), args) |
153 end |
153 end |
186 fun qnt_typ ty = domain_type (domain_type ty) |
186 fun qnt_typ ty = domain_type (domain_type ty) |
187 |
187 |
188 |
188 |
189 (* produces a regularized version of rtrm *) |
189 (* produces a regularized version of rtrm *) |
190 (* *) |
190 (* *) |
191 (* - the result still contains dummyTs *) |
191 (* - the result might contain dummyTs *) |
192 (* *) |
192 (* *) |
193 (* - for regularisation we do not need any *) |
193 (* - for regularisation we do not need any *) |
194 (* special treatment of bound variables *) |
194 (* special treatment of bound variables *) |
195 |
195 |
196 fun regularize_trm ctxt (rtrm, qtrm) = |
196 fun regularize_trm ctxt (rtrm, qtrm) = |
226 |
226 |
227 | (* in this case we just check whether the given equivalence relation is correct *) |
227 | (* in this case we just check whether the given equivalence relation is correct *) |
228 (rel, Const (@{const_name "op ="}, ty')) => |
228 (rel, Const (@{const_name "op ="}, ty')) => |
229 let |
229 let |
230 val exc = LIFT_MATCH "regularise (relation mismatch)" |
230 val exc = LIFT_MATCH "regularise (relation mismatch)" |
231 val rel_ty = (fastype_of rel) handle TERM _ => raise exc |
231 val rel_ty = fastype_of rel |
232 val rel' = mk_resp_arg ctxt (domain_type rel_ty, domain_type ty') |
232 val rel' = mk_resp_arg ctxt (domain_type rel_ty, domain_type ty') |
233 in |
233 in |
234 if rel' aconv rel then rtrm else raise exc |
234 if rel' aconv rel then rtrm else raise exc |
235 end |
235 end |
236 |
236 |
256 let |
256 let |
257 val thy = ProofContext.theory_of ctxt |
257 val thy = ProofContext.theory_of ctxt |
258 val qtrm_str = Syntax.string_of_term ctxt qtrm |
258 val qtrm_str = Syntax.string_of_term ctxt qtrm |
259 val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)") |
259 val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)") |
260 val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)") |
260 val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)") |
261 val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1 |
261 val rtrm' = #rconst (qconsts_lookup thy qtrm) handle NotFound => raise exc1 |
262 in |
262 in |
263 if Pattern.matches thy (rtrm', rtrm) |
263 if Pattern.matches thy (rtrm', rtrm) |
264 then rtrm else raise exc2 |
264 then rtrm else raise exc2 |
265 end |
265 end |
266 end |
266 end |