1210 |
1210 |
1211 fun mk_resp_arg lthy (rty, qty) = |
1211 fun mk_resp_arg lthy (rty, qty) = |
1212 let |
1212 let |
1213 val thy = ProofContext.theory_of lthy |
1213 val thy = ProofContext.theory_of lthy |
1214 in |
1214 in |
1215 case (rty, qty) of |
1215 if rty = qty |
1216 (Type (s, tys), Type (s', tys')) => |
1216 then HOLogic.eq_const rty |
|
1217 else |
|
1218 case (rty, qty) of |
|
1219 (Type (s, tys), Type (s', tys')) => |
1217 if s = s' |
1220 if s = s' |
1218 then let |
1221 then let |
|
1222 val _ = tracing ("maps lookup for " ^ s) |
|
1223 val _ = tracing (Syntax.string_of_typ lthy rty) |
|
1224 val _ = tracing (Syntax.string_of_typ lthy qty) |
1219 val SOME map_info = maps_lookup thy s |
1225 val SOME map_info = maps_lookup thy s |
1220 val args = map (mk_resp_arg lthy) (tys ~~ tys') |
1226 val args = map (mk_resp_arg lthy) (tys ~~ tys') |
1221 in |
1227 in |
1222 list_comb (Const (#relfun map_info, dummyT), args) |
1228 list_comb (Const (#relfun map_info, dummyT), args) |
1223 end |
1229 end |
1261 case (trm1, trm2) of |
1267 case (trm1, trm2) of |
1262 (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t') |
1268 (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t') |
1263 | _ => f trm1 trm2 |
1269 | _ => f trm1 trm2 |
1264 |
1270 |
1265 (* the major type of All and Ex quantifiers *) |
1271 (* the major type of All and Ex quantifiers *) |
1266 fun qnt_typ ty = domain_type (domain_type ty) |
1272 fun qnt_typ ty = domain_type (domain_type ty) |
1267 *} |
1273 *} |
1268 |
1274 |
1269 (* |
1275 (* |
1270 Regularizing an rtrm means: |
1276 Regularizing an rtrm means: |
1271 - quantifiers over a type that needs lifting are replaced by |
1277 - quantifiers over a type that needs lifting are replaced by |
1303 else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm |
1309 else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm |
1304 end |
1310 end |
1305 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
1311 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
1306 let |
1312 let |
1307 val subtrm = apply_subt (REGULARIZE_trm lthy) t t' |
1313 val subtrm = apply_subt (REGULARIZE_trm lthy) t t' |
|
1314 val _ = tracing "quantor types All" |
|
1315 val _ = tracing (Syntax.string_of_typ lthy ty) |
|
1316 val _ = tracing (Syntax.string_of_typ lthy ty') |
1308 in |
1317 in |
1309 if ty = ty' |
1318 if ty = ty' |
1310 then Const (@{const_name "All"}, ty) $ subtrm |
1319 then Const (@{const_name "All"}, ty) $ subtrm |
1311 else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
1320 else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
1312 end |
1321 end |
1313 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
1322 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
1314 let |
1323 let |
1315 val subtrm = apply_subt (REGULARIZE_trm lthy) t t' |
1324 val subtrm = apply_subt (REGULARIZE_trm lthy) t t' |
|
1325 val _ = tracing "quantor types Ex" |
|
1326 val _ = tracing (Syntax.string_of_typ lthy ty) |
|
1327 val _ = tracing (Syntax.string_of_typ lthy ty') |
1316 in |
1328 in |
1317 if ty = ty' |
1329 if ty = ty' |
1318 then Const (@{const_name "Ex"}, ty) $ subtrm |
1330 then Const (@{const_name "Ex"}, ty) $ subtrm |
1319 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
1331 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
1320 end |
1332 end |
1321 (* FIXME: Why is there a case for equality? Is it correct? *) |
1333 (* FIXME: should be replaced when fully applied? then 2nd argument *) |
1322 | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') => |
1334 | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') => |
1323 let |
1335 let |
1324 val subtrm = REGULARIZE_trm lthy t t' |
1336 val subtrm = REGULARIZE_trm lthy t t' |
1325 in |
1337 in |
1326 if ty = ty' |
1338 if ty = ty' |