1127 case trm of |
1127 case trm of |
1128 Abs (x, T, t) => Abs (x, T, f t) |
1128 Abs (x, T, t) => Abs (x, T, f t) |
1129 | _ => f trm |
1129 | _ => f trm |
1130 *} |
1130 *} |
1131 |
1131 |
|
1132 |
1132 (* FIXME: assumes always the typ is qty! *) |
1133 (* FIXME: assumes always the typ is qty! *) |
|
1134 (* FIXME: if there are more than one quotient, then you have to look up the relation *) |
1133 ML {* |
1135 ML {* |
1134 fun my_reg rel trm = |
1136 fun my_reg rel trm = |
1135 case trm of |
1137 case trm of |
1136 Abs (x, T, t) => |
1138 Abs (x, T, t) => |
1137 let |
1139 let |
1138 val ty1 = fastype_of trm |
1140 val ty1 = fastype_of trm |
1139 in |
1141 in |
1140 (mk_babs ty1 T) $ (mk_resp T $ rel) $ (my_reg rel t) |
1142 (mk_babs ty1 T) $ (mk_resp T $ rel) $ (Abs (x, T, my_reg rel t)) |
1141 end |
1143 end |
1142 | Const (@{const_name "All"}, U) $ t => |
1144 | Const (@{const_name "All"}, ty) $ t => |
1143 let |
1145 let |
1144 val ty1 = fastype_of t |
1146 val ty1 = domain_type ty |
1145 val ty2 = domain_type ty1 |
1147 val ty2 = domain_type ty1 |
1146 in |
1148 in |
1147 (mk_ball ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t) |
1149 (mk_ball ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t) |
1148 end |
1150 end |
1149 | Const (@{const_name "Ex"}, U) $ t => |
1151 | Const (@{const_name "Ex"}, ty) $ t => |
1150 let |
1152 let |
1151 val ty1 = fastype_of t |
1153 val ty1 = domain_type ty |
1152 val ty2 = domain_type ty1 |
1154 val ty2 = domain_type ty1 |
1153 in |
1155 in |
1154 (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t) |
1156 (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t) |
1155 end |
1157 end |
1156 | t1 $ t2 => (my_reg rel t1) $ (my_reg rel t2) |
1158 | t1 $ t2 => (my_reg rel t1) $ (my_reg rel t2) |